Formal Card-Game Systems
r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Identity 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.

implicit-follow

identity/implicit-follow: safety-counterexample; actual TLC exit 12.

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

Checked properties: TypeOK, LivePastSeparated, FreshAllocation, UniquePhysicalItems, StationaryObjectFrame, NoImplicitRetarget, RenewalClearsMarks, RetiredReferenceIsNotLive.

Input revision
1
Evidence class
finite-state-exploration
Failed observation or property
NoImplicitRetarget
Input manifest SHA-256
7b551331382b7a65fb4dcca7ffbef38cfa953807befbb2472bd9039fe2f73b7b
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"MaxOccurrence": 4, "physical_items": 2, "positions": 2}
Assumptions
None declared
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 2, "generated": 4, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["MaxOccurrence", "4"], ["ImplicitFollow", "TRUE"]]
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: identity/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=implicit-follow -Dformalwiki.input=7b551331382b7a65fb4dcca7ffbef38cfa953807befbb2472bd9039fe2f73b7b -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config IdentityImplicitFollow.cfg IdentityMC

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

VariableValueChange
state[explicitLineage |-> <<1>>, live |-> function {1 :> [area |-> "Display", marks |-> {"UseBound"}, physical |-> "item-a", position |-> 1], 2 :> [area |-> "Display", marks |-> {}, physical |-> "item-b", position |-> 2]}, next |-> 3, past |-> function {}, reference |-> 1, successors |-> function {}]Initial value

State 2

VariableValueChange
state[explicitLineage |-> <<1>>, live |-> function {2 :> [area |-> "Display", marks |-> {}, physical |-> "item-b", position |-> 2], 3 :> [area |-> "Private", marks |-> {}, physical |-> "item-a", position |-> 1]}, next |-> 4, past |-> function {1 :> [area |-> "Display", marks |-> {"UseBound"}, physical |-> "item-a", position |-> 1]}, reference |-> 3, successors |-> function {1 :> 3}]Changed

Captured edges:

  • State 1 → state 2 (forward): MoveItem

Download the normalized typed trace. Raw execution receipt.

ordinary

identity/ordinary: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, LivePastSeparated, FreshAllocation, UniquePhysicalItems, StationaryObjectFrame, NoImplicitRetarget, RenewalClearsMarks, RetiredReferenceIsNotLive, StableHistory.

Input revision
1
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
7b551331382b7a65fb4dcca7ffbef38cfa953807befbb2472bd9039fe2f73b7b
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"MaxOccurrence": 4, "physical_items": 2, "positions": 2}
Assumptions
None declared
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 58, "generated": 197, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["MaxOccurrence", "4"], ["ImplicitFollow", "FALSE"]]
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=7b551331382b7a65fb4dcca7ffbef38cfa953807befbb2472bd9039fe2f73b7b -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config IdentityMC.cfg IdentityMC

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.