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

Payment evidence

Exact checks for input revision 3. 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.

arithmetic

payment/arithmetic: success; actual TLC exit 0.

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

Checked properties: ArithmeticExamples.

Input revision
3
Evidence class
prepared-assertions
Failed observation or property
None; completed check
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"prepared_examples": 6}
Assumptions
None declared
Fairness
None declared
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 6, "generated": 12, "queue": 0}
Configured behavior
Spec
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=arithmetic -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config CostAlgebraMC.cfg CostAlgebraMC

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

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

Download the normalized typed trace. Raw execution receipt.

late-use-positive

payment/late-use-positive: safety-counterexample; actual TLC exit 12.

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

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
UseRecorded
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 2, "initial_funds": 3, "late_use": true, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 2, "generated": 2, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "2"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "TRUE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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: payment/ordinary-positive.

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=late-use-positive -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config late-use-positive.cfg AtomicPayment

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
available3Initial value
declinedFALSEInitial value
paidFALSEInitial value
pendingFALSEInitial value

State 2

VariableValueChange
available1Changed
declinedFALSEUnchanged
paidFALSEUnchanged
pendingTRUEChanged

Captured edges:

  • State 1 → state 2 (forward): Pay

Download the normalized typed trace. Raw execution receipt.

late-use-zero

payment/late-use-zero: safety-counterexample; actual TLC exit 12.

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

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
UseRecorded
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 0, "initial_funds": 3, "late_use": true, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 2, "generated": 2, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "0"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "TRUE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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: payment/ordinary-zero.

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=late-use-zero -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config late-use-zero.cfg AtomicPayment

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
available3Initial value
declinedFALSEInitial value
paidFALSEInitial value
pendingFALSEInitial value

State 2

VariableValueChange
available3Unchanged
declinedFALSEUnchanged
paidFALSEUnchanged
pendingTRUEChanged

Captured edges:

  • State 1 → state 2 (forward): Pay

Download the normalized typed trace. Raw execution receipt.

ordinary-insufficient

payment/ordinary-insufficient: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment, Completion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 2, "initial_funds": 1, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 2, "generated": 2, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "1"], ["BaseCost", "2"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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-insufficient -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config ordinary-insufficient.cfg AtomicPayment

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.

ordinary-positive

payment/ordinary-positive: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment, Completion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 2, "initial_funds": 3, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 4, "generated": 4, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "2"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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-positive -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config ordinary-positive.cfg AtomicPayment

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.

ordinary-zero

payment/ordinary-zero: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment, Completion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 0, "initial_funds": 3, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 4, "generated": 4, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "0"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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-zero -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config ordinary-zero.cfg AtomicPayment

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.

witness-positive

payment/witness-positive: witness; actual TLC exit 12.

Legal witness: a deliberate observation condition stops this run after the requested legal behavior.

Checked properties: StopBeforeCompletion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
StopBeforeCompletion
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 2, "initial_funds": 3, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 4, "generated": 4, "queue": 1}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "2"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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.

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=witness-positive -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config witness-positive.cfg PaymentWitnessMC

Legal witness: a deliberate observation condition stops this run after the requested legal behavior.

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
available3Initial value
declinedFALSEInitial value
paidFALSEInitial value
pendingFALSEInitial value

State 2

VariableValueChange
available1Changed
declinedFALSEUnchanged
paidTRUEChanged
pendingTRUEChanged

State 3

VariableValueChange
available1Unchanged
declinedFALSEUnchanged
paidTRUEUnchanged
pendingFALSEChanged

Captured edges:

  • State 1 → state 2 (forward): Pay
  • State 2 → state 3 (forward): Complete

Download the normalized typed trace. Raw execution receipt.

witness-zero

payment/witness-zero: witness; actual TLC exit 12.

Legal witness: a deliberate observation condition stops this run after the requested legal behavior.

Checked properties: StopBeforeCompletion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
StopBeforeCompletion
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 0, "initial_funds": 3, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 4, "generated": 4, "queue": 1}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "3"], ["BaseCost", "0"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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.

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=witness-zero -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config witness-zero.cfg PaymentWitnessMC

Legal witness: a deliberate observation condition stops this run after the requested legal behavior.

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
available3Initial value
declinedFALSEInitial value
paidFALSEInitial value
pendingFALSEInitial value

State 2

VariableValueChange
available3Unchanged
declinedFALSEUnchanged
paidTRUEChanged
pendingTRUEChanged

State 3

VariableValueChange
available3Unchanged
declinedFALSEUnchanged
paidTRUEUnchanged
pendingFALSEChanged

Captured edges:

  • State 1 → state 2 (forward): Pay
  • State 2 → state 3 (forward): Complete

Download the normalized typed trace. Raw execution receipt.

zero-empty-wallet

payment/zero-empty-wallet: success; actual TLC exit 0.

Completed finite check: no counterexample trace was produced.

Checked properties: TypeOK, UseRecorded, PaymentIsExact, DeclineIsUnpaid, AdmissionMatchesWallet, NoDoublePayment, Completion.

Input revision
3
Evidence class
finite-state-exploration
Failed observation or property
None; completed check
Input manifest SHA-256
f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97
Tool SHA-256
5bd7b64db99ae4c6c35f290de5e809c0ee41af43f8699cf696099ffb6452b1e2
Bounds
{"base_cost": 0, "initial_funds": 0, "late_use": false, "single_attempt": true}
Assumptions
A single supported wallet payment; no general cost interpreter.; Completion fairness applies only to this finite teaching model.
Fairness
WF_vars(Complete): continuously enabled completion cannot be postponed forever.
Constraints
None declared
Review
accepted
Exploration counts
{"distinct": 4, "generated": 4, "queue": 0}
Configured behavior
Spec
Deadlock check
Disabled
State constraints
None
Action constraints
None
Configured constants
[["InitialFunds", "0"], ["BaseCost", "0"], ["Increases <- EmptyModifiers"], ["Reductions <- EmptyModifiers"], ["LateUse", "FALSE"]]
Definition overrides
{"Increases": "EmptyModifiers", "Reductions": "EmptyModifiers"}
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=zero-empty-wallet -Dformalwiki.input=f25d31eca9f7d00b9561f2e29e15e615f25726e4a7790a562cfd7b700f5f9e97 -Dtlc2.overrides.TLCOverrides=FormalWikiOverrides -cp tools/tla2tools.jar:adapter tlc2.TLC -workers 1 -seed 1 -fp 0 -noGenerateSpecTE -metadir states -postCondition FormalWikiTrace!Capture -config zero-empty-wallet.cfg AtomicPayment

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.