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

Turns and objectives: evidence scope

A counter reaching a threshold and a procedure recording an outcome are separate events. The turn lesson and turn reference explain the phase and checkpoint boundaries that connect them.

Read each seat’s schedule

The profile assigns different actions and opportunities to its two seats. Its selected checks include prepared turn assertions, transition procedures and composed timing scenarios. A pointwise phase calculation must not be described as exploring a complete turn.

For an explored model, inspect its initial phase, bounded action opportunities, supplied procedures and stopping conditions. A finite schedule may exhaust its selected work without demonstrating universal progress. Fairness exists only where the configuration or specification explicitly supplies it.

Outcome recording has a boundary

Objective points contribute to a total under the appropriate current context. The outcome is then recognized at the modeled ending boundary. Moving a card, changing its value or meeting a progress requirement does not silently execute every later permission, payment or checkpoint.

The full reference retains those separate source contracts. The result associated with a contract does not establish that every possible objective or dynamic value source was exercised.

What the control distinguishes

The family control deliberately alters the selected turn/objective behavior and fails its named assertion. Its exact override and ordinary companion identify the comparison. A successful prepared example and a successful transition exploration support different conclusions even when both exit successfully.

The retained finite graph comparisons concern complete state/initial/labelled-transition content for the selected models. They do not establish all possible instance sizes, a complete game engine, balance or eventual completion under an arbitrary external scheduler.

Selected results

The records below show an ordinary finite configuration and the explicit control pair where applicable. Each record retains its own class and review status. The full list follows.

reference-profile/ref-objective-checks: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, PhysicalUniqueness, HostIntegrity, ObjectiveAssertions, ObjectiveCompleted.

Input revision
2
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "ObjectiveChecksMC.cfg", "constants": [["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- ObjectiveCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"]], "definition_overrides": {"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "ObjectiveCommands", "InitialState": "DummyInitial"}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
The selected phase schedule, objective values and completion/checkpoint providers are supplied exactly; no complete-game or arbitrary-scheduler progress claim is made.
Fairness
ObjectiveSpec == ObjectiveInit /\ [][ObjectiveNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 20, "generated": 30, "queue": 0}
Configured behavior
ObjectiveSpec
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["CardData <- Data"], ["InitialState <- DummyInitial"], ["Commands <- ObjectiveCommands"], ["CardOverride <- NoOverride"], ["CheckpointOverrideAllowed <- NoCheckpointOverride"]]
Definition overrides
{"CardData": "Data", "CardOverride": "NoOverride", "CheckpointOverrideAllowed": "NoCheckpointOverride", "Commands": "ObjectiveCommands", "InitialState": "DummyInitial"}
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=ref-objective-checks -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config ObjectiveChecksMC.cfg ObjectiveChecksMC

reference-profile/ref-turn-handoff-ordinary: success; actual TLC exit 0.

Prepared assertions: the listed calculations passed for these selected inputs; no exhaustive arithmetic theorem is claimed.

Checked properties: Block5Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
None; completed check
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "TurnHandoffVariantMC-ordinary.cfg", "constants": [], "definition_overrides": {}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
The selected phase schedule, objective values and completion/checkpoint providers are supplied exactly; no complete-game or arbitrary-scheduler progress claim is made.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 7, "generated": 14, "queue": 0}
Configured behavior
Spec5
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[]
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=ref-turn-handoff-ordinary -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config TurnHandoffVariantMC-ordinary.cfg TurnHandoffVariantMC

reference-profile/ref-turn-handoff-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: Block5Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
Block5Assertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "TurnHandoffVariantMC-defective.cfg", "constants": [["TurnOtherPlayer5 <- DefectBodyTurnHandoffVariant"]], "definition_overrides": {"TurnOtherPlayer5": "DefectBodyTurnHandoffVariant"}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 512, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
The selected phase schedule, objective values and completion/checkpoint providers are supplied exactly; no complete-game or arbitrary-scheduler progress claim is made.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec5
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["TurnOtherPlayer5 <- DefectBodyTurnHandoffVariant"]]
Definition overrides
{"TurnOtherPlayer5": "DefectBodyTurnHandoffVariant"}
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: reference-profile/ref-turn-handoff-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=ref-turn-handoff-defective -Dformalwiki.input=f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -suppressMessages 2216,2217,2218 -metadir states -postCondition FormalWikiTrace!Capture -config TurnHandoffVariantMC-defective.cfg TurnHandoffVariantMC

All associated configurations

Result

Class

Outcome

ref-objective-checks

finite-state-exploration

success

ref-scheduler-checks

prepared-assertions

success

ref-side-a-turn-timing

finite-state-exploration

success

ref-side-b-turn-timing

finite-state-exploration

success

ref-turn-checks

prepared-assertions

success

ref-turn-handoff-defective

prepared-assertions

safety-counterexample

ref-turn-handoff-ordinary

prepared-assertions

success

ref-turn-procedures

finite-state-exploration

success

Follow an associated result for its exact source, configuration, bounds, warnings, complete trace when one exists, and reproduction bundle. An association identifies scope; it does not measure individual source-branch reachability.