p99 Sample TLA+ code

README.md

Steps to Run

1. Download the VSCode Extension (https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide)
2. Put WireAsync.tla and WireAsync.cfg in the same file
3. Run VSCode command TLA+ > Check Model With TLC

WireAsync.cfg

SPECIFICATION Spec
CONSTANTS 
    People = {alice, bob}
    MaxStartingBalance = 10
    MaxWires = 2

INVARIANT NoOverdrafts

CHECK_DEADLOCK FALSE

WireAsync.tla

---- MODULE WireAsync ----
EXTENDS Integers
CONSTANT People, MaxStartingBalance, MaxWires
ASSUME People # {}
ASSUME MaxStartingBalance >= 0
ASSUME MaxWires >= 0

set ++ x == set \union {x}
set -- x == set \ {x}

(*--algorithm WirePlusCal {
variables
    acct \in [People -> 0..MaxStartingBalance];
    wireset = {};


define {
    NoOverdrafts ==
        \A p \in People:
            acct[p] >= 0
}


fair process (ResolveWire = "ResolveWire") {
  Resolve:
    while (TRUE) { 
      with (wire \in wireset) { 
            acct[wire.from] := @ - wire.amnt ||
            acct[wire.to] := @ + wire.amnt;
            wireset := wireset -- wire; 
      };
    };
};

process (CreateWire = "CreateWire")
variable i = 0;
{ 
Create:
  while (i < MaxWires) { 
    with (from \in People,
 to \in People,
 amnt \in 0..acct[from]) { 
        wireset := wireset ++ [from |-> from, to |-> to, amnt |-> amnt, id |-> i];
        i := i + 1;
    };
  };            
};

} *)
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-bd5f77c1f1b06f9e24f9c0871f9f860a
VARIABLES pc, acct, wireset

(* define statement *)
NoOverdrafts ==
    \A p \in People:
        acct[p] >= 0

VARIABLE i

vars == << pc, acct, wireset, i >>

ProcSet == {"ResolveWire"} \cup {"CreateWire"}

Init == (* Global variables *)
        /\ acct \in [People -> 0..MaxStartingBalance]
        /\ wireset = {}
        (* Process CreateWire *)
        /\ i = 0
        /\ pc = [self \in ProcSet |-> CASE self = "ResolveWire" -> "Resolve"
                                        [] self = "CreateWire" -> "Create"]

Resolve == /\ pc["ResolveWire"] = "Resolve"
           /\ \E wire \in wireset:
                /\ acct' = [acct EXCEPT ![wire.from] = @ - wire.amnt,
                                        ![wire.to] = @ + wire.amnt]
                /\ wireset' = wireset -- wire
           /\ pc' = [pc EXCEPT !["ResolveWire"] = "Resolve"]
           /\ i' = i

ResolveWire == Resolve

Create == /\ pc["CreateWire"] = "Create"
          /\ IF i < MaxWires
                THEN /\ \E from \in People:
                          \E to \in People:
                            \E amnt \in 0..acct[from]:
                              /\ wireset' = wireset ++ [from |-> from, to |-> to, amnt |-> amnt, id |-> i]
                              /\ i' = i + 1
                     /\ pc' = [pc EXCEPT !["CreateWire"] = "Create"]
                ELSE /\ pc' = [pc EXCEPT !["CreateWire"] = "Done"]
                     /\ UNCHANGED << wireset, i >>
          /\ acct' = acct

CreateWire == Create

Next == ResolveWire \/ CreateWire

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(ResolveWire)

\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-2f53ab644b787acec938cf18f57abc19
                                                                                                 
                                                                                                 
                                                                                                 
                                                                                                 ====