tla_plus_concurrent_counter

tla

VARIABLES counter, pc

(* define statement *)
AllDone == \A t \in Threads : pc[t] = "Done"

Correct == AllDone => counter = ThreadCount

VARIABLE localCounter

vars == << counter, pc, localCounter >>

ProcSet == (1..ThreadCount)

Init == (* Global variables *)
        /\ counter = 0
        (* Process counter_ *)
        /\ localCounter = [self \in 1..ThreadCount |-> 0]
        /\ pc = [self \in ProcSet |-> "Load"]

Load(self) == /\ pc[self] = "Load"
              /\ localCounter' = [localCounter EXCEPT ![self] = counter]
              /\ pc' = [pc EXCEPT ![self] = "Inc"]
              /\ UNCHANGED counter

Inc(self) == /\ pc[self] = "Inc"
             /\ counter' = localCounter[self] + 1
             /\ pc' = [pc EXCEPT ![self] = "Done"]
             /\ UNCHANGED localCounter

counter_(self) == Load(self) \/ Inc(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in 1..ThreadCount: counter_(self))
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")