Skip to content

Commit ca1d1a7

Browse files
dranovdranov
committed
feat: identify which properties were violated
1 parent 90d91d3 commit ca1d1a7

File tree

2 files changed

+225
-50
lines changed

2 files changed

+225
-50
lines changed

‎ProofWidgets/Demos/TraceDisplay.lean‎

Lines changed: 165 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@ def exampleNoViolation : Json := json% {"termination_reason": {"kind": "explored
1010

1111
#displayTrace exampleNoViolation
1212

13-
def exampleViolation : Json := json% {"violation_kind": "safety_failure",
13+
def ringViolation : Json := json% {"violation":
14+
{"violates": ["single_leader", "leader_greatest"], "kind": "safety_failure"},
1415
"trace":
1516
{"theory":
1617
{"baaaa":
@@ -49,19 +50,108 @@ def exampleViolation : Json := json% {"violation_kind": "safety_failure",
4950
{"transition": {"send": {"next": 2, "n": 1}},
5051
"index": 2,
5152
"fields": {"pending": [[0, 1], [1, 2]], "leader": []}},
52-
{"transition": {"recv": {"sender": 0, "next": 2, "n": 1}},
53+
{"transition": {"send": {"next": 3, "n": 2}},
5354
"index": 3,
54-
"fields": {"pending": [[0, 1], [1, 2]], "leader": [1]}},
55-
{"transition": {"recv": {"sender": 1, "next": 3, "n": 2}},
55+
"fields": {"pending": [[0, 1], [1, 2], [2, 3]], "leader": []}},
56+
{"transition": {"send": {"next": 4, "n": 3}},
5657
"index": 4,
57-
"fields": {"pending": [[0, 1], [1, 2]], "leader": [1, 2]}}]},
58+
"fields": {"pending": [[0, 1], [1, 2], [2, 3], [3, 4]], "leader": []}},
59+
{"transition": {"send": {"next": 0, "n": 4}},
60+
"index": 5,
61+
"fields":
62+
{"pending": [[0, 1], [1, 2], [2, 3], [3, 4], [4, 0]], "leader": []}},
63+
{"transition": {"recv": {"sender": 0, "next": 2, "n": 1}},
64+
"index": 6,
65+
"fields": {"pending": [[1, 2], [2, 3], [3, 4], [4, 0]], "leader": [1]}},
66+
{"transition": {"recv": {"sender": 1, "next": 3, "n": 2}},
67+
"index": 7,
68+
"fields": {"pending": [[2, 3], [3, 4], [4, 0]], "leader": [1, 2]}},
69+
{"transition": {"recv": {"sender": 2, "next": 4, "n": 3}},
70+
"index": 8,
71+
"fields": {"pending": [[3, 4], [4, 0]], "leader": [1, 2, 3]}},
72+
{"transition": {"recv": {"sender": 3, "next": 0, "n": 4}},
73+
"index": 9,
74+
"fields": {"pending": [[4, 0]], "leader": [1, 2, 3, 4]}},
75+
{"transition": {"recv": {"sender": 4, "next": 1, "n": 0}},
76+
"index": 10,
77+
"fields": {"pending": [], "leader": [0, 1, 2, 3, 4]}}]},
78+
"state_fingerprint": "16335755120522489119",
5879
"result": "found_violation"}
5980

81+
#displayTrace ringViolation
82+
83+
def exampleViolation : Json := json% {"violation":
84+
{"violates": ["single_leader", "leader_greatest"], "kind": "safety_failure"},
85+
"trace":
86+
{"theory":
87+
{"baaaa":
88+
[[0, 0, 0],
89+
[0, 1, 0],
90+
[0, 2, 0],
91+
[0, 3, 0],
92+
[0, 4, 0],
93+
[1, 0, 0],
94+
[1, 1, 0],
95+
[1, 2, 0],
96+
[1, 3, 0],
97+
[1, 4, 0],
98+
[2, 0, 0],
99+
[2, 1, 0],
100+
[2, 2, 0],
101+
[2, 3, 0],
102+
[2, 4, 0],
103+
[3, 0, 0],
104+
[3, 1, 0],
105+
[3, 2, 0],
106+
[3, 3, 0],
107+
[3, 4, 0],
108+
[4, 0, 0],
109+
[4, 1, 0],
110+
[4, 2, 0],
111+
[4, 3, 0],
112+
[4, 4, 0]]},
113+
"states":
114+
[{"transition": "after_init",
115+
"index": 0,
116+
"fields": {"pending": [], "leader": []}},
117+
{"transition": {"send": {"next": 1, "n": 0}},
118+
"index": 1,
119+
"fields": {"pending": [[0, 1]], "leader": []}},
120+
{"transition": {"send": {"next": 2, "n": 1}},
121+
"index": 2,
122+
"fields": {"pending": [[0, 1], [1, 2]], "leader": []}},
123+
{"transition": {"send": {"next": 3, "n": 2}},
124+
"index": 3,
125+
"fields": {"pending": [[0, 1], [1, 2], [2, 3]], "leader": []}},
126+
{"transition": {"send": {"next": 4, "n": 3}},
127+
"index": 4,
128+
"fields": {"pending": [[0, 1], [1, 2], [2, 3], [3, 4]], "leader": []}},
129+
{"transition": {"send": {"next": 0, "n": 4}},
130+
"index": 5,
131+
"fields":
132+
{"pending": [[0, 1], [1, 2], [2, 3], [3, 4], [4, 0]], "leader": []}},
133+
{"transition": {"recv": {"sender": 0, "next": 2, "n": 1}},
134+
"index": 6,
135+
"fields": {"pending": [[1, 2], [2, 3], [3, 4], [4, 0]], "leader": [1]}},
136+
{"transition": {"recv": {"sender": 1, "next": 3, "n": 2}},
137+
"index": 7,
138+
"fields": {"pending": [[2, 3], [3, 4], [4, 0]], "leader": [1, 2]}},
139+
{"transition": {"recv": {"sender": 2, "next": 4, "n": 3}},
140+
"index": 8,
141+
"fields": {"pending": [[3, 4], [4, 0]], "leader": [1, 2, 3]}},
142+
{"transition": {"recv": {"sender": 3, "next": 0, "n": 4}},
143+
"index": 9,
144+
"fields": {"pending": [[4, 0]], "leader": [1, 2, 3, 4]}},
145+
{"transition": {"recv": {"sender": 4, "next": 1, "n": 0}},
146+
"index": 10,
147+
"fields": {"pending": [], "leader": [0, 1, 2, 3, 4]}}]},
148+
"state_fingerprint": "16335755120522489119",
149+
"result": "found_violation"}
60150

61151
#displayTrace exampleViolation
62152

63153

64-
def exampleDeadlock : Json := json% {"violation_kind": "deadlock",
154+
def exampleDeadlock : Json := json% {"violation": {"kind": "deadlock"},
65155
"trace":
66156
{"theory": {"none": 0},
67157
"states":
@@ -360,6 +450,75 @@ def exampleDeadlock : Json := json% {"violation_kind": "deadlock",
360450
[2, "Mutex.states_IndT.check_has_woken"]],
361451
"locked": false,
362452
"has_woken": [1]}}]},
453+
"state_fingerprint": "4263100916297288679",
363454
"result": "found_violation"}
364455

365456
#displayTrace exampleDeadlock
457+
458+
459+
def exampleNoViolationTrace : Json := json% {
460+
"trace":
461+
{"theory":
462+
{"baaaa":
463+
[[0, 0, 0],
464+
[0, 1, 0],
465+
[0, 2, 0],
466+
[0, 3, 0],
467+
[0, 4, 0],
468+
[1, 0, 0],
469+
[1, 1, 0],
470+
[1, 2, 0],
471+
[1, 3, 0],
472+
[1, 4, 0],
473+
[2, 0, 0],
474+
[2, 1, 0],
475+
[2, 2, 0],
476+
[2, 3, 0],
477+
[2, 4, 0],
478+
[3, 0, 0],
479+
[3, 1, 0],
480+
[3, 2, 0],
481+
[3, 3, 0],
482+
[3, 4, 0],
483+
[4, 0, 0],
484+
[4, 1, 0],
485+
[4, 2, 0],
486+
[4, 3, 0],
487+
[4, 4, 0]]},
488+
"states":
489+
[{"transition": "after_init",
490+
"index": 0,
491+
"fields": {"pending": [], "leader": []}},
492+
{"transition": {"send": {"next": 1, "n": 0}},
493+
"index": 1,
494+
"fields": {"pending": [[0, 1]], "leader": []}},
495+
{"transition": {"send": {"next": 2, "n": 1}},
496+
"index": 2,
497+
"fields": {"pending": [[0, 1], [1, 2]], "leader": []}},
498+
{"transition": {"send": {"next": 3, "n": 2}},
499+
"index": 3,
500+
"fields": {"pending": [[0, 1], [1, 2], [2, 3]], "leader": []}},
501+
{"transition": {"send": {"next": 4, "n": 3}},
502+
"index": 4,
503+
"fields": {"pending": [[0, 1], [1, 2], [2, 3], [3, 4]], "leader": []}},
504+
{"transition": {"send": {"next": 0, "n": 4}},
505+
"index": 5,
506+
"fields":
507+
{"pending": [[0, 1], [1, 2], [2, 3], [3, 4], [4, 0]], "leader": []}},
508+
{"transition": {"recv": {"sender": 0, "next": 2, "n": 1}},
509+
"index": 6,
510+
"fields": {"pending": [[1, 2], [2, 3], [3, 4], [4, 0]], "leader": [1]}},
511+
{"transition": {"recv": {"sender": 1, "next": 3, "n": 2}},
512+
"index": 7,
513+
"fields": {"pending": [[2, 3], [3, 4], [4, 0]], "leader": [1, 2]}},
514+
{"transition": {"recv": {"sender": 2, "next": 4, "n": 3}},
515+
"index": 8,
516+
"fields": {"pending": [[3, 4], [4, 0]], "leader": [1, 2, 3]}},
517+
{"transition": {"recv": {"sender": 3, "next": 0, "n": 4}},
518+
"index": 9,
519+
"fields": {"pending": [[4, 0]], "leader": [1, 2, 3, 4]}},
520+
{"transition": {"recv": {"sender": 4, "next": 1, "n": 0}},
521+
"index": 10,
522+
"fields": {"pending": [], "leader": [0, 1, 2, 3, 4]}}]}}
523+
524+
#displayTrace exampleNoViolationTrace

‎widget/src/traceDisplay.tsx‎

Lines changed: 60 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,11 @@ type Trace = ParsedState[];
1212

1313
type ViolationKind = "safety_failure" | "deadlock";
1414

15+
interface Violation {
16+
kind: ViolationKind;
17+
violates?: string[]; // Array of violated property names (only present for safety_failure)
18+
}
19+
1520
interface EarlyTerminationCondition {
1621
kind: "found_violating_state" | "deadlock_occurred" | "reached_depth_bound";
1722
depth?: number;
@@ -34,13 +39,18 @@ interface TraceData {
3439
type ModelCheckingResult =
3540
| {
3641
result: "found_violation";
37-
violation_kind: ViolationKind;
42+
violation: Violation;
3843
trace: TraceData | null;
3944
}
4045
| {
4146
result: "no_violation_found";
4247
explored_states: number;
4348
termination_reason: TerminationReason;
49+
trace?: TraceData | null;
50+
}
51+
| {
52+
// Trace-only data without a result (for displaying execution traces)
53+
trace: TraceData;
4454
};
4555

4656
interface ModelCheckerViewProps {
@@ -418,17 +428,22 @@ const TheorySection: React.FC<{ theory: Record<string, unknown> }> = ({ theory }
418428
/** Header showing the result status with appropriate icon */
419429
const ResultHeader: React.FC<{
420430
resultType: "found_violation" | "no_violation_found";
421-
violationKind?: ViolationKind;
431+
violation?: Violation;
422432
exploredStates?: number;
423433
terminationReason?: TerminationReason;
424-
}> = ({ resultType, violationKind, exploredStates, terminationReason }) => {
425-
if (resultType === "found_violation") {
426-
const icon = violationKind === "deadlock" ? "🔒" : "⚠️";
427-
const label = violationKind === "deadlock" ? "Deadlock Detected" : "Safety Violation Found";
434+
}> = ({ resultType, violation, exploredStates, terminationReason }) => {
435+
if (resultType === "found_violation" && violation) {
436+
const icon = violation.kind === "deadlock" ? "🔒" : "⚠️";
437+
const label = violation.kind === "deadlock" ? "Deadlock Detected" : "Safety Violation Found";
428438
return (
429439
<div className="result-header result-violation">
430440
<span className="result-icon">{icon}</span>
431441
<span className="result-label">{label}</span>
442+
{violation.kind === "safety_failure" && violation.violates && violation.violates.length > 0 && (
443+
<div className="result-details">
444+
<strong>Violated properties:</strong> {violation.violates.join(", ")}
445+
</div>
446+
)}
432447
</div>
433448
);
434449
}
@@ -860,13 +875,10 @@ const ModelCheckerView: React.FC<ModelCheckerViewProps> = ({
860875

861876
const prettyJson = JSON.stringify(result, null, 2);
862877

863-
// Extract trace and theory for violation results
864-
const trace = result.result === "found_violation" && result.trace
865-
? traceDataToStates(result.trace)
866-
: [];
867-
const theory: Record<string, unknown> | undefined = result.result === "found_violation"
868-
? result.trace?.theory
869-
: undefined;
878+
// Extract trace and theory from results (works for all result types)
879+
const traceData = result.trace;
880+
const trace = traceData ? traceDataToStates(traceData) : [];
881+
const theory: Record<string, unknown> | undefined = traceData?.theory;
870882

871883
return (
872884
<>
@@ -887,42 +899,46 @@ const ModelCheckerView: React.FC<ModelCheckerViewProps> = ({
887899
</div>
888900
) : (
889901
<>
890-
{result.result === "no_violation_found" ? (
891-
<ResultHeader
892-
resultType="no_violation_found"
893-
exploredStates={result.explored_states}
894-
terminationReason={result.termination_reason}
895-
/>
896-
) : (
902+
{'result' in result && (
897903
<>
898-
<ResultHeader
899-
resultType="found_violation"
900-
violationKind={result.violation_kind}
901-
/>
902-
903-
{theory && <TheorySection theory={theory} />}
904-
905-
{trace.length > 0 ? (
906-
<>
907-
<div className={`mc-trace ${isVertical ? "vertical" : "horizontal"}`}>
908-
{trace.map((s: ParsedState, idx: number) => {
909-
const prev = idx > 0 ? trace[idx - 1].fields : undefined;
910-
const changes = diffChanges(prev, s.fields);
911-
return <StateCard key={s.index} st={s} changes={changes} />;
912-
})}
913-
</div>
914-
915-
<div className="mc-summary">
916-
<strong>Summary:</strong> {trace.length} states in trace
917-
</div>
918-
</>
904+
{result.result === "no_violation_found" ? (
905+
<ResultHeader
906+
resultType="no_violation_found"
907+
exploredStates={result.explored_states}
908+
terminationReason={result.termination_reason}
909+
/>
919910
) : (
920-
<div className="mc-summary">
921-
<strong>No trace available</strong>
922-
</div>
911+
<ResultHeader
912+
resultType="found_violation"
913+
violation={result.violation}
914+
/>
923915
)}
924916
</>
925917
)}
918+
919+
{theory && <TheorySection theory={theory} />}
920+
921+
{trace.length > 0 ? (
922+
<>
923+
<div className={`mc-trace ${isVertical ? "vertical" : "horizontal"}`}>
924+
{trace.map((s: ParsedState, idx: number) => {
925+
const prev = idx > 0 ? trace[idx - 1].fields : undefined;
926+
const changes = diffChanges(prev, s.fields);
927+
return <StateCard key={s.index} st={s} changes={changes} />;
928+
})}
929+
</div>
930+
931+
<div className="mc-summary">
932+
<strong>Summary:</strong> {trace.length} states in trace
933+
</div>
934+
</>
935+
) : (
936+
'result' in result && result.result === "found_violation" && (
937+
<div className="mc-summary">
938+
<strong>No trace available</strong>
939+
</div>
940+
)
941+
)}
926942
</>
927943
)}
928944
</div>

0 commit comments

Comments
 (0)