lib/machine/src/explore/temporal.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const explore = @import("root.zig");
2 const fault = @import("../fault/root.zig");
3 const std = @import("std");
4
5 pub const SequenceError = error{
6 CapacityExceeded,
7 SequenceClosed,
8 VirtualTimeRegressed,
9 };
10
11 pub fn Sequence(comptime capacity_value: explore.EventCapacity) type {
12 return struct {
13 storage: [capacity.events]explore.Event = undefined,
14 count: u16 = 0,
15 state: explore.TraceState = .open,
16
17 const Self = @This();
18
19 pub const capacity: explore.EventCapacity = capacity_value;
20 pub const Error: type = SequenceError;
21
22 pub fn append(
23 self: *Self,
24 virtual_time_tick: u64,
25 value: explore.EventValue,
26 ) Error!void {
27 self.assertValid();
28 if (self.state != .open) return error.SequenceClosed;
29 if (self.count == self.storage.len) {
30 self.state = .incomplete;
31 return error.CapacityExceeded;
32 }
33 if (self.count > 0 and
34 virtual_time_tick < self.storage[self.count - 1].virtual_time_tick)
35 {
36 return error.VirtualTimeRegressed;
37 }
38 self.storage[self.count] = .{
39 .sequence = self.count,
40 .virtual_time_tick = virtual_time_tick,
41 .value = value,
42 };
43 self.count += 1;
44 self.assertValid();
45 }
46
47 pub fn finish(
48 self: *Self,
49 completion: explore.TraceCompletion,
50 ) error{SequenceClosed}!void {
51 self.assertValid();
52 if (self.state != .open) return error.SequenceClosed;
53 self.state = switch (completion) {
54 .exhausted => .exhausted,
55 .incomplete => .incomplete,
56 };
57 self.assertValid();
58 }
59
60 pub fn events(self: *const Self) []const explore.Event {
61 self.assertValid();
62 return self.storage[0..self.count];
63 }
64
65 pub fn traceState(self: *const Self) explore.TraceState {
66 self.assertValid();
67 return self.state;
68 }
69
70 fn assertValid(self: *const Self) void {
71 std.debug.assert(self.count <= self.storage.len);
72 std.debug.assert(self.count <= capacity.events);
73 }
74 };
75 }
76
77 pub fn evaluateSafety(sequence: anytype, rule: explore.Safety) explore.PropertyEvaluation {
78 const events = sequence.events();
79 const declaration = findDeclaration(events, rule.property) orelse
80 return evaluation(rule.property, .incomplete, .declaration_missing, null);
81 if (declaration.value.kind != .safety or declaration.value.bound != null) {
82 return evaluation(
83 rule.property,
84 .incomplete,
85 .declaration_mismatch,
86 declaration.sequence,
87 );
88 }
89 for (events[declaration.offset + 1 ..]) |event| {
90 if (matches(rule.forbidden, event)) {
91 return evaluation(
92 rule.property,
93 .violated,
94 .forbidden_event,
95 event.sequence,
96 );
97 }
98 }
99 return switch (sequence.traceState()) {
100 .exhausted => evaluation(rule.property, .holds, .satisfied, null),
101 .open, .incomplete => evaluation(
102 rule.property,
103 .incomplete,
104 .trace_incomplete,
105 null,
106 ),
107 };
108 }
109
110 pub fn evaluateLiveness(
111 sequence: anytype,
112 rule: explore.BoundedLiveness,
113 ) explore.PropertyEvaluation {
114 const events = sequence.events();
115 const declaration = findDeclaration(events, rule.property) orelse
116 return evaluation(rule.property, .incomplete, .declaration_missing, null);
117 if (declaration.value.kind != .bounded_liveness or
118 declaration.value.bound == null or
119 !std.meta.eql(declaration.value.bound.?, rule.bound))
120 {
121 return evaluation(
122 rule.property,
123 .incomplete,
124 .declaration_mismatch,
125 declaration.sequence,
126 );
127 }
128 return evaluateTriggers(
129 events,
130 declaration.offset + 1,
131 sequence.traceState(),
132 rule,
133 );
134 }
135
136 const Declaration = struct {
137 offset: usize,
138 sequence: u16,
139 value: explore.PropertyDeclaration,
140 };
141
142 fn findDeclaration(events: []const explore.Event, property: explore.SemanticId) ?Declaration {
143 for (events, 0..) |event, offset| {
144 switch (event.value) {
145 .property_declaration => |value| if (value.id == property) {
146 return .{
147 .offset = offset,
148 .sequence = event.sequence,
149 .value = value,
150 };
151 },
152 else => {},
153 }
154 }
155 return null;
156 }
157
158 fn evaluateTriggers(
159 events: []const explore.Event,
160 first: usize,
161 state: explore.TraceState,
162 rule: explore.BoundedLiveness,
163 ) explore.PropertyEvaluation {
164 var trigger_seen = false;
165 var pending: ?u16 = null;
166 for (events[first..], first..) |event, offset| {
167 if (!matches(rule.trigger, event)) continue;
168 trigger_seen = true;
169 switch (findResponse(events, offset, rule)) {
170 .satisfied => {},
171 .violated => |witness| return evaluation(
172 rule.property,
173 .violated,
174 .bound_exceeded,
175 witness,
176 ),
177 .pending => pending = pending orelse event.sequence,
178 }
179 }
180 if (!trigger_seen) {
181 return evaluation(rule.property, .unreached, .trigger_not_seen, null);
182 }
183 if (pending) |witness| {
184 if (state == .exhausted) {
185 return evaluation(
186 rule.property,
187 .violated,
188 .response_missing,
189 witness,
190 );
191 }
192 return evaluation(
193 rule.property,
194 .incomplete,
195 .trace_incomplete,
196 witness,
197 );
198 }
199 return if (state == .exhausted)
200 evaluation(rule.property, .holds, .satisfied, null)
201 else
202 evaluation(rule.property, .incomplete, .trace_incomplete, null);
203 }
204
205 const Response = union(enum) {
206 satisfied,
207 violated: u16,
208 pending,
209 };
210
211 fn findResponse(
212 events: []const explore.Event,
213 trigger_offset: usize,
214 rule: explore.BoundedLiveness,
215 ) Response {
216 const trigger = events[trigger_offset];
217 if (matches(rule.response, trigger)) return .satisfied;
218 for (events[trigger_offset + 1 ..]) |candidate| {
219 if (withinBound(trigger, candidate, rule.bound) and
220 matches(rule.response, candidate))
221 {
222 return .satisfied;
223 }
224 if (pastBound(trigger, candidate, rule.bound)) {
225 return .{ .violated = candidate.sequence };
226 }
227 }
228 return .pending;
229 }
230
231 fn withinBound(
232 trigger: explore.Event,
233 candidate: explore.Event,
234 bound: explore.Bound,
235 ) bool {
236 std.debug.assert(candidate.sequence >= trigger.sequence);
237 std.debug.assert(candidate.virtual_time_tick >= trigger.virtual_time_tick);
238 return switch (bound) {
239 .steps => |steps| candidate.sequence - trigger.sequence <= steps,
240 .virtual_time => |ticks| {
241 return candidate.virtual_time_tick - trigger.virtual_time_tick <= ticks;
242 },
243 };
244 }
245
246 fn pastBound(
247 trigger: explore.Event,
248 candidate: explore.Event,
249 bound: explore.Bound,
250 ) bool {
251 return !withinBound(trigger, candidate, bound);
252 }
253
254 pub fn matches(pattern: explore.Pattern, event: explore.Event) bool {
255 return switch (pattern) {
256 .event_class => |class| class == eventClass(event.value),
257 .input => |kind| switch (event.value) {
258 .controlled_input => |value| kind == std.meta.activeTag(value.value),
259 else => false,
260 },
261 .schedule => |kind| switch (event.value) {
262 .schedule_choice => |value| kind == std.meta.activeTag(value.value),
263 else => false,
264 },
265 .topology => |kind| switch (event.value) {
266 .topology_choice => |value| kind == std.meta.activeTag(value.value),
267 else => false,
268 },
269 .observation => |id| switch (event.value) {
270 .observation => |value| id == value.id,
271 else => false,
272 },
273 .property_declaration => |id| switch (event.value) {
274 .property_declaration => |value| id == value.id,
275 else => false,
276 },
277 .property_evaluation => |expected| matchEvaluation(expected, event.value),
278 .fault => |kind| matchFault(kind, event.value),
279 .diagnostic => |id| switch (event.value) {
280 .diagnostic => |value| id == value.id,
281 else => false,
282 },
283 .external_admission => |source| switch (event.value) {
284 .external_admission => |value| source == value.origin.source,
285 else => false,
286 },
287 .operation => |expected| matchOperation(expected, event.value),
288 };
289 }
290
291 fn eventClass(value: explore.EventValue) explore.EventClass {
292 return switch (value) {
293 .controlled_input => .controlled_input,
294 .schedule_choice => .schedule_choice,
295 .topology_choice => .topology_choice,
296 .observation => .observation,
297 .property_declaration => .property_declaration,
298 .property_evaluation => .property_evaluation,
299 .injected_fault => .injected_fault,
300 .diagnostic => .diagnostic,
301 .external_admission => .external_admission,
302 .operation => .operation,
303 };
304 }
305
306 fn matchEvaluation(expected: explore.EvaluationPattern, value: explore.EventValue) bool {
307 return switch (value) {
308 .property_evaluation => |actual| actual.id == expected.id and
309 (expected.verdict == null or actual.verdict == expected.verdict.?),
310 else => false,
311 };
312 }
313
314 fn matchFault(kind: fault.Kind, value: explore.EventValue) bool {
315 return switch (value) {
316 .injected_fault => |generated| switch (generated.action) {
317 .healthy => false,
318 .inject => |actual| actual == kind,
319 .persist => |actual| actual == kind,
320 .recover => false,
321 },
322 else => false,
323 };
324 }
325
326 fn matchOperation(expected: explore.OperationPattern, value: explore.EventValue) bool {
327 return switch (value) {
328 .operation => |actual| actual.id == expected.id and
329 (expected.outcome == null or actual.outcome == expected.outcome.?),
330 else => false,
331 };
332 }
333
334 fn evaluation(
335 property: explore.SemanticId,
336 verdict: explore.Verdict,
337 reason: explore.EvaluationReason,
338 witness: ?u16,
339 ) explore.PropertyEvaluation {
340 return .{
341 .id = property,
342 .verdict = verdict,
343 .reason = reason,
344 .witness = witness,
345 };
346 }