------------------------------ MODULE Fischer ------------------------------
EXTENDS Integers, TLC

CONSTANT Procs, delta, epsilon, Times
ASSUME /\ {delta, epsilon} \subseteq Nat
       /\ Times \subseteq Nat

none == CHOOSE n : n \notin Procs

VARIABLE x, pc, rt, now
v == <<x, pc, rt, now>>

TypeOK == /\ x \in Procs \cup {none}
          /\ pc \in [Procs -> {"ncs", "wait", "w1", "w2", "cs", "exit"}]
          /\ rt \in [Procs -> Times]
          /\ now \in Times
          
Init == /\ x = none
        /\ pc = [p \in Procs |-> "wait"]
        /\ rt = [p \in Procs |-> 0]
        /\ now = 0

Ncs(p) == /\ pc[p] = "ncs"
              /\ pc' = [pc EXCEPT ![p] = "wait"]
              /\ UNCHANGED <<x, rt, now>>
                     
Wait(p) == /\ pc[p] = "wait"
               /\ x  = none
               /\ rt' = [rt EXCEPT ![p] = now]
               /\ pc' = [pc EXCEPT ![p] = "w1"]
               /\ UNCHANGED <<x, now>>
           
          
W1(p) == /\ pc[p] = "w1"
             /\ x' = p
             /\ rt' = [rt EXCEPT ![p] = now]
             /\ pc' = [pc EXCEPT ![p] = "w2"]
             /\ now' = now

W2(p) == /\ pc[p] = "w2"
             /\ now - rt[p] >= epsilon
             /\ pc' = [pc EXCEPT ![p] = IF x = p THEN "cs" ELSE "wait"]
             /\ UNCHANGED <<x, rt, now>>

Cs(p) == /\ pc[p] = "cs"
             /\ pc' = [pc EXCEPT ![p] = "exit"]      
             /\ UNCHANGED <<x, rt, now>>
             
Exit(p) == /\ pc[p] = "exit"
               /\ x' = none
               /\ pc' = [pc EXCEPT ![p] = "ncs"]      
               /\ UNCHANGED <<rt, now>>
            
Time == /\ now' \in {t \in Times : t > now}
            /\ \A p \in Procs : (pc[p] = "w1") => (now' =< rt[p]+delta)
            /\ UNCHANGED <<x, pc, rt>>

PNext(p) == Ncs(p) \/ Wait(p) \/ W1(p) \/ W2(p) \/ Cs(p) \/ Exit(p)

Next == \/ \E p \in Procs : PNext(p)
        \/ Time

Fairness == SF_v(Time) /\ \A p \in Procs : WF_v((pc[p] # "ncs") /\ PNext(p))

Spec == Init /\ [][Next]_v /\ Fairness   
        
Invariant == /\ TypeOK
             /\ \A p \in Procs : 
                   /\ (pc[p] = "w1") => (now \in rt[p] .. (rt[p]+delta))
                   /\ (pc[p] \in {"cs", "exit"}) => 
                          (x = p) /\ \A j \in Procs : pc[j] # "w1"
                   /\ (pc[p] = "w2") /\ (x = p) => 
                        \A q \in Procs : (pc[q] = "w1") => 
                                           (rt[q] + delta) < (rt[p] + epsilon)

Mutex == \A p, q \in Procs : (p # q) => {pc[p], pc[q]} # {"cs"}

INSTANCE TLAPS
THEOREM Invariant => Mutex
BY DEF Invariant, TypeOK, Mutex

LInv == (x # none) => (pc[x] \in {"w2", "cs", "exit"})

StarvationFree == (\E p \in Procs : pc[p] = "wait") ~> 
                         \/ \E p \in Procs : pc[p] = "cs"
                         \/ \A t \in Times : now >= t  
=============================================================================
\* Modification History
\* Last modified Mon Oct 14 11:56:16 CEST 2024 by lamport
\* Created Wed Aug 03 18:14:42 PDT 2022 by lamport
