lib/machine/src/explore/distributed/property.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 const explore = @import("../root.zig");
 2 const std = @import("std");
 3 const types = @import("types.zig");
 4 
 5 pub const quorum_rule: explore.Safety = .{
 6     .property = types.Property.commit_quorum.id(),
 7     .forbidden = .{ .observation = types.Semantic.unbacked_commit.id() },
 8 };
 9 
10 pub const freshness_rule: explore.Safety = .{
11     .property = types.Property.accept_freshness.id(),
12     .forbidden = .{ .observation = types.Semantic.stale_accept.id() },
13 };
14 
15 pub const declarations = [_]explore.PropertyDeclaration{
16     .{ .id = quorum_rule.property, .kind = .safety, .bound = null },
17     .{ .id = freshness_rule.property, .kind = .safety, .bound = null },
18 };
19 
20 pub const Verdicts = [declarations.len]explore.PropertyEvaluation;
21 
22 pub fn declare(sequence: *types.Events, tick: u64) types.Error!void {
23     for (declarations) |declaration| {
24         sequence.append(tick, .{
25             .property_declaration = declaration,
26         }) catch |failure| switch (failure) {
27             error.CapacityExceeded => return error.TraceCapacityExceeded,
28             error.SequenceClosed, error.VirtualTimeRegressed => unreachable,
29         };
30     }
31 }
32 
33 pub fn evaluate(sequence: *const types.Events) Verdicts {
34     return .{
35         explore.evaluateSafety(sequence, quorum_rule),
36         explore.evaluateSafety(sequence, freshness_rule),
37     };
38 }
39 
40 pub fn violation(verdicts: Verdicts) ?explore.PropertyEvaluation {
41     for (verdicts) |verdict| {
42         if (verdict.verdict == .violated) return verdict;
43     }
44     return null;
45 }
46 
47 pub fn unexplained(verdicts: Verdicts) bool {
48     for (verdicts) |verdict| {
49         switch (verdict.reason) {
50             .declaration_missing, .declaration_mismatch => return true,
51             else => {},
52         }
53     }
54     return false;
55 }
56 
57 comptime {
58     std.debug.assert(declarations.len == 2);
59     std.debug.assert(declarations[0].id != declarations[1].id);
60     for (declarations) |declaration| {
61         std.debug.assert(declaration.kind == .safety);
62         std.debug.assert(declaration.bound == null);
63     }
64 }