Checkmate-Escrow/specs/tla/MatchStateMachine.cfg at main · darkcode123456/Checkmate-Escrow · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
\* Model 1 — immediate completion (DisputePeriod = 0).
\*
\* Exercises the submit_result -> Completed -> claim_vested_payout route, plus
\* cancellation, expiry and pause/resume. Two matches are enough to catch any
\* cross-match interference (per-match state is indexed, so a third adds states
\* without adding behaviours).

SPECIFICATION Spec

CONSTANTS
    Matches = {"m1", "m2"}
    Players = {"p1", "p2"}
    Stake = 1
    DisputePeriod = 0
    Timeout = 2
    MaxLedger = 3

INVARIANTS
    TypeOK
    AtMostOneRelease
    NotBothPlayersWin
    AtMostOneWinner
    WinnersMatchOutcome
    NoOutcomeBeforeCompletion
    EscrowMatchesDeposits
    OnlyDepositorsArePaid
    PlayingImpliesFullyFunded
    NoPayoutWithoutFullFunding
    PendingMatchIsNeverPaused

PROPERTIES
    TerminalIsFinal
    ReleaseIsMonotonic
    PausedIsOnlyLeftByResume
    OutcomeIsStable