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

Traversal and inspection: evidence scope

A traversal, a site inspection and an individual item inspection have distinct frames and return conditions. Start with the lesson and inspection reference before interpreting their checks.

Keep the nested procedures distinct

The full profile retains traversal position, approach and encounter steps, inspection selection and individual-item opportunities. A parent can be waiting while a child has ended but still owes its final reactions or return. A stored target also needs a live-object and permission check at the point where it is used.

The selected configurations include prepared assertions, bounded procedures and composed timing scenarios. Inspect the actual specification and property list to see which result class applies. The evidence does not turn every selector fixture into a stateful traversal driver.

Selection and observation require authority

Candidate presentation, lawful viewers, random selection, explicit participant choices and supplied exceptions are inputs to their respective contracts. An internal identity is broader than the information a participant may inspect. A public count does not authorize reading a concealed item’s metadata.

The ordinary checks cover only their selected objects, layouts, orders, histories and provider responses. They do not implement every external selection or effect provider.

What the control distinguishes

The family control alters one named traversal/inspection rule. Its intended diagnostic is evidence of sensitivity to that defect at the configured inputs. Ordinary companions and explicit definition overrides keep that comparison inspectable. The retained counterexample belongs to the defective variant; it is not an invented ordinary play sequence.

Source preservation, finite correspondence and measured exploration remain separate claims. Branch anchors without individual execution measurements are identified as retained but unexercised. There is no general hidden-information theorem, arbitrary-layout proof or complete-game qualification in these results.

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-inspection-procedures: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: InspectionesInvariant7, EventuallyReturns7.

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": "InspectionProceduresMC.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
Layouts, orders, current object references, lawful views and selection/effect providers are the exact finite fixtures; these do not grant broader observation rights.
Fairness
SpecInspectiones7 == InitInspectiones7 /\ [][NextInspectiones7]_q7 /\ WF_q7(NextInspectiones7)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 15493, "generated": 16017, "queue": 0}
Configured behavior
SpecInspectiones7
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-inspection-procedures -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 InspectionProceduresMC.cfg InspectionProceduresMC

reference-profile/ref-traversal-identity-ordinary: success; actual TLC exit 0.

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

Checked properties: Block6Assertions.

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": "TraversalIdentityVariantMC-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
Layouts, orders, current object references, lawful views and selection/effect providers are the exact finite fixtures; these do not grant broader observation rights.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 9, "generated": 18, "queue": 0}
Configured behavior
Spec6
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-traversal-identity-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 TraversalIdentityVariantMC-ordinary.cfg TraversalIdentityVariantMC

reference-profile/ref-traversal-identity-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: Block6Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
Block6Assertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "TraversalIdentityVariantMC-defective.cfg", "constants": [["TraversalDirectEdge6 <- DefectBodyTraversalIdentityVariant"]], "definition_overrides": {"TraversalDirectEdge6": "DefectBodyTraversalIdentityVariant"}, "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
Layouts, orders, current object references, lawful views and selection/effect providers are the exact finite fixtures; these do not grant broader observation rights.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec6
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["TraversalDirectEdge6 <- DefectBodyTraversalIdentityVariant"]]
Definition overrides
{"TraversalDirectEdge6": "DefectBodyTraversalIdentityVariant"}
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-traversal-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=ref-traversal-identity-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 TraversalIdentityVariantMC-defective.cfg TraversalIdentityVariantMC

All associated configurations

Result

Class

Outcome

ref-inspection-checks

prepared-assertions

success

ref-inspection-procedures

finite-state-exploration

success

ref-inspection-timing

finite-state-exploration

success

ref-inspection-timing-assertions

prepared-assertions

success

ref-item-timing

finite-state-exploration

success

ref-item-timing-assertions

prepared-assertions

success

ref-traversal-checks

prepared-assertions

success

ref-traversal-identity-defective

prepared-assertions

safety-counterexample

ref-traversal-identity-ordinary

prepared-assertions

success

ref-traversal-procedures

finite-state-exploration

success

ref-traversal-timing

finite-state-exploration

success

ref-traversal-timing-assertions

prepared-assertions

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.