On this page

Priority evidence¶

Exact checks for input revision 1. Review status is shown per result.

Each passing result is bounded to its configuration. A legal witness and a defective-variant counterexample answer different questions.

alternate-holder¶

priority/alternate-holder: safety-counterexample; actual TLC exit 12.

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Checked properties: TypeOK, FreshCalls, FreshReceipts, SuspendedCallerCannotAct, ReturnStaysWithActor, ExactCallerReceipt, TwoConsecutivePasses, ReadyPassMarker, StaleReturnRejected.

Input revision: 1
Evidence class: finite-state-exploration
Failed observation or property: ReturnStaysWithActor
Input manifest SHA-256: 04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa
Tool SHA-256: 5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds: {"MaxCalls": 2, "MaxReceipts": 10, "maximum_child_depth": 1}
Assumptions: None declared
Fairness: None declared
Constraints: None declared
Review: accepted
Exploration counts: {"distinct": 11, "generated": 11, "queue": 1}
Configured behavior: Spec
Deadlock check: Disabled
State constraints: None
Action constraints: None
Configured constants: [["MaxCalls", "2"], ["MaxReceipts", "10"], ["Defect", "\"AlternateHolder\""]]
Definition overrides: None
Symmetry: None
State view: None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

Ordinary companion: priority/ordinary.

Reproduce this check and inspect its exact inputs

java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=alternate-holder -Dformalwiki.input=04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config PriorityAlternateHolder.cfg PriorityMC

adapter-compile.stderr · PROJECT-DOCUMENT
adapter-compile.stdout · PROJECT-DOCUMENT
adapter-src/FormalWikiOverrides.java · MIT
adapter-src/FormalWikiTrace.java · MIT
adapter-src/FormalWikiTrace.tla · CC0-1.0
capture.json · PROJECT-DOCUMENT
execution-tool.py · MIT
inputs/PriorityAlternateHolder.cfg · CC0-1.0
inputs/PriorityMC.cfg · CC0-1.0
inputs/PriorityMC.tla · CC0-1.0
inputs/PriorityProtocol.tla · CC0-1.0
inputs/PriorityStickyPass.cfg · CC0-1.0
inputs/PriorityWrongCaller.cfg · CC0-1.0
inputs/inputs.json · PROJECT-DOCUMENT
stderr.log · PROJECT-DOCUMENT
stdout.log · PROJECT-DOCUMENT
execution.json · PROJECT-DOCUMENT
Normalized typed trace · PROJECT-DOCUMENT
Independent evidence review: priority-teaching-evidence-review-r1 · PROJECT-DOCUMENT

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Complete captured sequence

The complete ordered sequence stays available below. “Changed” compares adjacent captured states; a change of representation alone is identified separately.

State 1

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Open", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 1, phase \|-> "NeedCheckpoint", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {}]	Initial value

State 2

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 1, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Checkpoint", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 2, phase \|-> "Ready", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {1}]	Changed

State 3

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "Begin", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Resolving", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 4

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 1, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildSuspend", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Paused", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 5

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 1, childComplete \|-> TRUE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildComplete", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Paused", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 6

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "B", lastActor \|-> "A", lastEvent \|-> "Return", lastReturn \|-> [actor \|-> "A", call \|-> 1, child \|-> 1, childrenReturned \|-> TRUE, complete \|-> TRUE, drained \|-> TRUE, id \|-> 2, reception \|-> 1, transaction \|-> 1, window \|-> 1], nextCall \|-> 2, nextReceipt \|-> 3, phase \|-> "NeedCheckpoint", previousPass \|-> FALSE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 1, actualChild \|-> 1, actualReception \|-> 1, actualTransaction \|-> 1, actualWindow \|-> 1, expectedCall \|-> 1, expectedChild \|-> 1, expectedReception \|-> 1, expectedTransaction \|-> 1, expectedWindow \|-> 1], transaction \|-> 0, usedCalls \|-> {1}, usedReceipts \|-> {1, 2}]	Changed

Captured edges:

State 1 → state 2 (forward): Checkpoint
State 2 → state 3 (forward): Act
State 3 → state 4 (forward): Suspend
State 4 → state 5 (forward): ChildComplete
State 5 → state 6 (forward): Return

Download the normalized typed trace. Raw execution receipt.

ordinary¶

priority/ordinary: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, FreshCalls, FreshReceipts, SuspendedCallerCannotAct, ReturnStaysWithActor, ExactCallerReceipt, TwoConsecutivePasses, ReadyPassMarker, StaleReturnRejected.

Input revision: 1
Evidence class: finite-state-exploration
Failed observation or property: None; completed check
Input manifest SHA-256: 04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa
Tool SHA-256: 5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds: {"MaxCalls": 2, "MaxReceipts": 10, "maximum_child_depth": 1}
Assumptions: None declared
Fairness: None declared
Constraints: None declared
Review: accepted
Exploration counts: {"distinct": 48, "generated": 49, "queue": 0}
Configured behavior: Spec
Deadlock check: Disabled
State constraints: None
Action constraints: None
Configured constants: [["MaxCalls", "2"], ["MaxReceipts", "10"], ["Defect", "\"None\""]]
Definition overrides: None
Symmetry: None
State view: None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

No counterexample trace was produced.

Reproduce this check and inspect its exact inputs

java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ordinary -Dformalwiki.input=04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config PriorityMC.cfg PriorityMC

adapter-compile.stderr · PROJECT-DOCUMENT
adapter-compile.stdout · PROJECT-DOCUMENT
adapter-src/FormalWikiOverrides.java · MIT
adapter-src/FormalWikiTrace.java · MIT
adapter-src/FormalWikiTrace.tla · CC0-1.0
capture.json · PROJECT-DOCUMENT
execution-tool.py · MIT
inputs/PriorityAlternateHolder.cfg · CC0-1.0
inputs/PriorityMC.cfg · CC0-1.0
inputs/PriorityMC.tla · CC0-1.0
inputs/PriorityProtocol.tla · CC0-1.0
inputs/PriorityStickyPass.cfg · CC0-1.0
inputs/PriorityWrongCaller.cfg · CC0-1.0
inputs/inputs.json · PROJECT-DOCUMENT
stderr.log · PROJECT-DOCUMENT
stdout.log · PROJECT-DOCUMENT
execution.json · PROJECT-DOCUMENT
Normalized typed trace · PROJECT-DOCUMENT
Independent evidence review: priority-teaching-evidence-review-r1 · PROJECT-DOCUMENT

Completed finite check: no counterexample trace was produced.

No counterexample trace. A completed check does not supply an example execution.

Download the normalized typed trace. Raw execution receipt.

sticky-pass¶

priority/sticky-pass: safety-counterexample; actual TLC exit 12.

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Checked properties: TypeOK, FreshCalls, FreshReceipts, SuspendedCallerCannotAct, ReturnStaysWithActor, ExactCallerReceipt, TwoConsecutivePasses, StaleReturnRejected.

Input revision: 1
Evidence class: finite-state-exploration
Failed observation or property: TwoConsecutivePasses
Input manifest SHA-256: 04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa
Tool SHA-256: 5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds: {"MaxCalls": 2, "MaxReceipts": 10, "maximum_child_depth": 1}
Assumptions: None declared
Fairness: None declared
Constraints: None declared
Review: accepted
Exploration counts: {"distinct": 20, "generated": 20, "queue": 2}
Configured behavior: Spec
Deadlock check: Disabled
State constraints: None
Action constraints: None
Configured constants: [["MaxCalls", "2"], ["MaxReceipts", "10"], ["Defect", "\"KeepPass\""]]
Definition overrides: None
Symmetry: None
State view: None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

Ordinary companion: priority/ordinary.

Reproduce this check and inspect its exact inputs

java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=sticky-pass -Dformalwiki.input=04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config PriorityStickyPass.cfg PriorityMC

adapter-compile.stderr · PROJECT-DOCUMENT
adapter-compile.stdout · PROJECT-DOCUMENT
adapter-src/FormalWikiOverrides.java · MIT
adapter-src/FormalWikiTrace.java · MIT
adapter-src/FormalWikiTrace.tla · CC0-1.0
capture.json · PROJECT-DOCUMENT
execution-tool.py · MIT
inputs/PriorityAlternateHolder.cfg · CC0-1.0
inputs/PriorityMC.cfg · CC0-1.0
inputs/PriorityMC.tla · CC0-1.0
inputs/PriorityProtocol.tla · CC0-1.0
inputs/PriorityStickyPass.cfg · CC0-1.0
inputs/PriorityWrongCaller.cfg · CC0-1.0
inputs/inputs.json · PROJECT-DOCUMENT
stderr.log · PROJECT-DOCUMENT
stdout.log · PROJECT-DOCUMENT
execution.json · PROJECT-DOCUMENT
Normalized typed trace · PROJECT-DOCUMENT
Independent evidence review: priority-teaching-evidence-review-r1 · PROJECT-DOCUMENT

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Complete captured sequence

The complete ordered sequence stays available below. “Changed” compares adjacent captured states; a change of representation alone is identified separately.

State 1

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Open", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 1, phase \|-> "NeedCheckpoint", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {}]	Initial value

State 2

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 1, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Checkpoint", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 2, phase \|-> "Ready", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {1}]	Changed

State 3

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 1, holder \|-> "B", lastActor \|-> "None", lastEvent \|-> "Pass", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 2, phase \|-> "NeedCheckpoint", previousPass \|-> TRUE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {1}]	Changed

State 4

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 2, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 1, holder \|-> "B", lastActor \|-> "None", lastEvent \|-> "Checkpoint", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 3, phase \|-> "Ready", previousPass \|-> TRUE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {1, 2}]	Changed

State 5

Variable	Value	Change
state	[busyActor \|-> "B", call \|-> 1, checkpoint \|-> 2, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 1, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "Begin", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 3, phase \|-> "Resolving", previousPass \|-> TRUE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1, 2}]	Changed

State 6

Variable	Value	Change
state	[busyActor \|-> "B", call \|-> 1, checkpoint \|-> 2, child \|-> 1, childComplete \|-> FALSE, consecutivePasses \|-> 1, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildSuspend", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 3, phase \|-> "Paused", previousPass \|-> TRUE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1, 2}]	Changed

State 7

Variable	Value	Change
state	[busyActor \|-> "B", call \|-> 1, checkpoint \|-> 2, child \|-> 1, childComplete \|-> TRUE, consecutivePasses \|-> 1, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildComplete", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 3, phase \|-> "Paused", previousPass \|-> TRUE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1, 2}]	Changed

State 8

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "B", lastActor \|-> "B", lastEvent \|-> "Return", lastReturn \|-> [actor \|-> "B", call \|-> 1, child \|-> 1, childrenReturned \|-> TRUE, complete \|-> TRUE, drained \|-> TRUE, id \|-> 3, reception \|-> 2, transaction \|-> 1, window \|-> 1], nextCall \|-> 2, nextReceipt \|-> 4, phase \|-> "NeedCheckpoint", previousPass \|-> TRUE, reception \|-> 3, returnAudit \|-> [actualCall \|-> 1, actualChild \|-> 1, actualReception \|-> 2, actualTransaction \|-> 1, actualWindow \|-> 1, expectedCall \|-> 1, expectedChild \|-> 1, expectedReception \|-> 2, expectedTransaction \|-> 1, expectedWindow \|-> 1], transaction \|-> 0, usedCalls \|-> {1}, usedReceipts \|-> {1, 2, 3}]	Changed

State 9

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 4, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "B", lastActor \|-> "B", lastEvent \|-> "Checkpoint", lastReturn \|-> [actor \|-> "B", call \|-> 1, child \|-> 1, childrenReturned \|-> TRUE, complete \|-> TRUE, drained \|-> TRUE, id \|-> 3, reception \|-> 2, transaction \|-> 1, window \|-> 1], nextCall \|-> 2, nextReceipt \|-> 5, phase \|-> "Ready", previousPass \|-> TRUE, reception \|-> 3, returnAudit \|-> [actualCall \|-> 1, actualChild \|-> 1, actualReception \|-> 2, actualTransaction \|-> 1, actualWindow \|-> 1, expectedCall \|-> 1, expectedChild \|-> 1, expectedReception \|-> 2, expectedTransaction \|-> 1, expectedWindow \|-> 1], transaction \|-> 0, usedCalls \|-> {1}, usedReceipts \|-> {1, 2, 3, 4}]	Changed

State 10

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 1, holder \|-> "None", lastActor \|-> "B", lastEvent \|-> "Pass", lastReturn \|-> [actor \|-> "B", call \|-> 1, child \|-> 1, childrenReturned \|-> TRUE, complete \|-> TRUE, drained \|-> TRUE, id \|-> 3, reception \|-> 2, transaction \|-> 1, window \|-> 1], nextCall \|-> 2, nextReceipt \|-> 5, phase \|-> "Closed", previousPass \|-> TRUE, reception \|-> 3, returnAudit \|-> [actualCall \|-> 1, actualChild \|-> 1, actualReception \|-> 2, actualTransaction \|-> 1, actualWindow \|-> 1, expectedCall \|-> 1, expectedChild \|-> 1, expectedReception \|-> 2, expectedTransaction \|-> 1, expectedWindow \|-> 1], transaction \|-> 0, usedCalls \|-> {1}, usedReceipts \|-> {1, 2, 3, 4}]	Changed

Captured edges:

State 1 → state 2 (forward): Checkpoint
State 2 → state 3 (forward): Pass
State 3 → state 4 (forward): Checkpoint
State 4 → state 5 (forward): Act
State 5 → state 6 (forward): Suspend
State 6 → state 7 (forward): ChildComplete
State 7 → state 8 (forward): Return
State 8 → state 9 (forward): Checkpoint
State 9 → state 10 (forward): Pass

Download the normalized typed trace. Raw execution receipt.

wrong-caller¶

priority/wrong-caller: safety-counterexample; actual TLC exit 12.

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Checked properties: TypeOK, FreshCalls, FreshReceipts, SuspendedCallerCannotAct, ReturnStaysWithActor, ExactCallerReceipt, TwoConsecutivePasses, ReadyPassMarker, StaleReturnRejected.

Input revision: 1
Evidence class: finite-state-exploration
Failed observation or property: ExactCallerReceipt
Input manifest SHA-256: 04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa
Tool SHA-256: 5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds: {"MaxCalls": 2, "MaxReceipts": 10, "maximum_child_depth": 1}
Assumptions: None declared
Fairness: None declared
Constraints: None declared
Review: accepted
Exploration counts: {"distinct": 11, "generated": 11, "queue": 1}
Configured behavior: Spec
Deadlock check: Disabled
State constraints: None
Action constraints: None
Configured constants: [["MaxCalls", "2"], ["MaxReceipts", "10"], ["Defect", "\"WrongCaller\""]]
Definition overrides: None
Symmetry: None
State view: None

This evidence applies to the exact configured finite model. It is not an unbounded proof or an implementation conformance result.

Download this package’s source and reproduction bundle.

Ordinary companion: priority/ordinary.

Reproduce this check and inspect its exact inputs

java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx512m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=wrong-caller -Dformalwiki.input=04133ab1081702b4cce15176241db1644c4ae12d305408b232f0a078b55597fa -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config PriorityWrongCaller.cfg PriorityMC

adapter-compile.stderr · PROJECT-DOCUMENT
adapter-compile.stdout · PROJECT-DOCUMENT
adapter-src/FormalWikiOverrides.java · MIT
adapter-src/FormalWikiTrace.java · MIT
adapter-src/FormalWikiTrace.tla · CC0-1.0
capture.json · PROJECT-DOCUMENT
execution-tool.py · MIT
inputs/PriorityAlternateHolder.cfg · CC0-1.0
inputs/PriorityMC.cfg · CC0-1.0
inputs/PriorityMC.tla · CC0-1.0
inputs/PriorityProtocol.tla · CC0-1.0
inputs/PriorityStickyPass.cfg · CC0-1.0
inputs/PriorityWrongCaller.cfg · CC0-1.0
inputs/inputs.json · PROJECT-DOCUMENT
stderr.log · PROJECT-DOCUMENT
stdout.log · PROJECT-DOCUMENT
execution.json · PROJECT-DOCUMENT
Normalized typed trace · PROJECT-DOCUMENT
Independent evidence review: priority-teaching-evidence-review-r1 · PROJECT-DOCUMENT

Deliberately defective variant: this retained counterexample belongs to the named negative control.

Complete captured sequence

The complete ordered sequence stays available below. “Changed” compares adjacent captured states; a change of representation alone is identified separately.

State 1

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Open", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 1, phase \|-> "NeedCheckpoint", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {}]	Initial value

State 2

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 1, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "None", lastEvent \|-> "Checkpoint", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 1, nextReceipt \|-> 2, phase \|-> "Ready", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 0, usedCalls \|-> {}, usedReceipts \|-> {1}]	Changed

State 3

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "Begin", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Resolving", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 4

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 1, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildSuspend", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Paused", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 5

Variable	Value	Change
state	[busyActor \|-> "A", call \|-> 1, checkpoint \|-> 1, child \|-> 1, childComplete \|-> TRUE, consecutivePasses \|-> 0, holder \|-> "None", lastActor \|-> "None", lastEvent \|-> "ChildComplete", lastReturn \|-> [actor \|-> "None", call \|-> 0, child \|-> 0, childrenReturned \|-> FALSE, complete \|-> FALSE, drained \|-> FALSE, id \|-> 0, reception \|-> 0, transaction \|-> 0, window \|-> 0], nextCall \|-> 2, nextReceipt \|-> 2, phase \|-> "Paused", previousPass \|-> FALSE, reception \|-> 1, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 0, actualReception \|-> 0, actualTransaction \|-> 0, actualWindow \|-> 0, expectedCall \|-> 0, expectedChild \|-> 0, expectedReception \|-> 0, expectedTransaction \|-> 0, expectedWindow \|-> 0], transaction \|-> 1, usedCalls \|-> {1}, usedReceipts \|-> {1}]	Changed

State 6

Variable	Value	Change
state	[busyActor \|-> "None", call \|-> 0, checkpoint \|-> 0, child \|-> 0, childComplete \|-> FALSE, consecutivePasses \|-> 0, holder \|-> "A", lastActor \|-> "A", lastEvent \|-> "Return", lastReturn \|-> [actor \|-> "A", call \|-> 0, child \|-> 1, childrenReturned \|-> TRUE, complete \|-> TRUE, drained \|-> TRUE, id \|-> 2, reception \|-> 1, transaction \|-> 1, window \|-> 1], nextCall \|-> 2, nextReceipt \|-> 3, phase \|-> "NeedCheckpoint", previousPass \|-> FALSE, reception \|-> 2, returnAudit \|-> [actualCall \|-> 0, actualChild \|-> 1, actualReception \|-> 1, actualTransaction \|-> 1, actualWindow \|-> 1, expectedCall \|-> 1, expectedChild \|-> 1, expectedReception \|-> 1, expectedTransaction \|-> 1, expectedWindow \|-> 1], transaction \|-> 0, usedCalls \|-> {1}, usedReceipts \|-> {1, 2}]	Changed

Captured edges:

State 1 → state 2 (forward): Checkpoint
State 2 → state 3 (forward): Act
State 3 → state 4 (forward): Suspend
State 4 → state 5 (forward): ChildComplete
State 5 → state 6 (forward): Return

Download the normalized typed trace. Raw execution receipt.