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

Abilities and timing: evidence scope

An ability can exist, be active, have a trigger opportunity and be permitted to start at different times. Begin with abilities and use, then use the ability reference and additional rules to identify the relevant contract.

Preserve each permission boundary

The full profile distinguishes source identity, controller, executor, costs, instruction order, pending instances, priority and caller return. A source that leaves play can have a detached continuation without receiving every permission of a live object. A completed option and two consecutive passes also produce different priority outcomes.

The isolated priority teaching model investigates one optional-use window with supplied child and checkpoint providers. It does not replace the full profile’s ability, conditional-instance or interrupt contracts.

Result classes matter

Some configurations evaluate prepared timing or instruction assertions. Others explore bounded protocol state. The configured specification and evidence class identify that difference. A self-loop fixture is not a stateful driver merely because its module name refers to a procedure.

For each result, read the supplied legality, activity, payment, current-effect and completion witnesses. No fairness or progress theorem is implied unless that exact property and assumption appear in the record.

What the controls distinguish

The family negative control alters one named ability/timing contract and reaches its intended assertion failure. The priority tutorial’s actor-return, old-pass and wrong-caller controls answer their own narrower questions. Exact ordinary companions and definition overrides identify the tested changes.

Source counterpart preservation and selected finite graph agreement do not establish every argument domain or every branch’s execution. Information projections, effect interpretation, external scheduler behavior and unrestricted ability providers remain explicit boundaries. These results do not constitute a complete engine or universal timing theorem.

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

Completed finite check: no counterexample trace was produced.

Checked properties: ProceduresInvariant9, EventuallyReturns9.

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": "AbilityProceduresMC.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
Activity, legality, current-effect, payment and exact caller/child completion witnesses are supplied in the selected model; external ability interpretation is outside scope.
Fairness
SpecProcedures9 == InitProcedures9 /\ [][NextProcedures9]_q9p /\ WF_q9p(WorkProcedures9)
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 106, "generated": 198, "queue": 0}
Configured behavior
SpecProcedures9
Deadlock check
Disabled
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-ability-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 AbilityProceduresMC.cfg AbilityProceduresMC

reference-profile/ref-interrupt-condition-ordinary: success; actual TLC exit 0.

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

Checked properties: Block9Assertions.

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": "InterruptConditionVariantMC-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": 1536, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
Activity, legality, current-effect, payment and exact caller/child completion witnesses are supplied in the selected model; external ability interpretation is outside scope.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 12, "generated": 24, "queue": 0}
Configured behavior
Spec9
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 -Xmx1536m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ref-interrupt-condition-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 InterruptConditionVariantMC-ordinary.cfg InterruptConditionVariantMC

reference-profile/ref-interrupt-condition-defective: safety-counterexample; actual TLC exit 12.

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

Checked properties: Block9Assertions.

Input revision
2
Evidence class
prepared-assertions
Failed observation or property
Block9Assertions
Input manifest SHA-256
f0df4091a373122a9be4ccfaa3bc6895bce2df003eea077feea02800dfa7a4c3
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"configuration": "InterruptConditionVariantMC-defective.cfg", "constants": [["AbilityIsInterrupt9 <- DefectBodyInterruptConditionVariant"]], "definition_overrides": {"AbilityIsInterrupt9": "DefectBodyInterruptConditionVariant"}, "fingerprint_polynomial": 0, "finite_domain": "Exact initial-state, constructor and fixture definitions in this hash-bound module closure.", "heap_mib": 1536, "max_seconds": 90, "seed": 1, "workers": 1}
Assumptions
Activity, legality, current-effect, payment and exact caller/child completion witnesses are supplied in the selected model; external ability interpretation is outside scope.
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
null
Configured behavior
Spec9
Deadlock check
Enabled
State constraints
None
Action constraints
None
Configured constants
[["AbilityIsInterrupt9 <- DefectBodyInterruptConditionVariant"]]
Definition overrides
{"AbilityIsInterrupt9": "DefectBodyInterruptConditionVariant"}
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-interrupt-condition-ordinary.

Reproduce this check and inspect its exact inputs
java -XX:+PerfDisableSharedMem -XX:+UseParallelGC -XX:ActiveProcessorCount=2 -Xmx1536m -Xss8m -DTLA-Library=. -Dformalwiki.capture=capture.json -Dformalwiki.run=ref-interrupt-condition-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 InterruptConditionVariantMC-defective.cfg InterruptConditionVariantMC

All associated configurations

Result

Class

Outcome

ref-ability-checks

prepared-assertions

success

ref-ability-procedures

finite-state-exploration

success

ref-action-completion-reaction

finite-state-exploration

success

ref-action-cost-reaction

finite-state-exploration

success

ref-additional-checks

prepared-assertions

success

ref-additional-procedures

finite-state-exploration

success

ref-commitment-probes

prepared-assertions

success

ref-commitment-publication

finite-state-exploration

success

ref-interrupt-condition-defective

prepared-assertions

safety-counterexample

ref-interrupt-condition-ordinary

prepared-assertions

success

ref-persistent-checks

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.