Checkmate-Escrow/specs/tla/MatchStateMachineDeferred.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 2 — deferred completion (DisputePeriod > 0).
\*
\* Exercises the submit_result -> PendingResult -> finalize_match route and the
\* dispute-resolution route that can overturn the oracle. The clock runs far
\* enough past the dispute deadline for finalisation to become enabled, which is
\* what makes the "two payout routes cannot both fire" check meaningful.

SPECIFICATION Spec

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

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

PROPERTIES
    TerminalIsFinal
    ReleaseIsMonotonic
    PausedIsOnlyLeftByResume
    OutcomeIsStable