------------------------------ MODULE Fischer ------------------------------
(***************************************************************************)
(* This module contains defines the formula Fischer, which describes       *)
(* Fischers algorithm of Sections 5.2.1 - 5.2.3 of "A Science of Computer  *)
(* Programming" by Leslie Lamport.  TLC can be used to check that this     *)
(* algorithm satisfies mutual exclusion, as well as the invariant in       *)
(* formula (5.2) that is needed to reason about liveness.  However,        *)
(* liveness is not considered.                                             *)
(*                                                                         *)
(* Since TLC cannot handle real numbers, thie module defines a             *)
(* discrete-time version of Fischer's algorithm in which the set Times of  *)
(* all possible times is a set of natural numbers.                         *)
(***************************************************************************)
EXTENDS Integers 

CONSTANT Procs, delta, epsilon, Times

(***************************************************************************)
(* We assume that Times is a subset of the set Nat of natural numbers, and *)
(* delta and epsilon are natural numbers.  And we let all behaviors begin  *)
(* at time 0.  The discrete-time version of Fischer's algorithm is         *)
(* obtained by letting Time equal Nat.  Letting Time be a finite interval  *)
(* of natural numbers produces a finite-state model on which TLC can check *)
(* invariants.                                                             *)
(***************************************************************************)
ASSUME /\ {delta, epsilon} \subseteq Nat
       /\ Times \subseteq Nat 

(***************************************************************************)
(* We define none to be some unspecified value that is not in Proce.       *)
(***************************************************************************)
none == CHOOSE n : n \notin Procs

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

          
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

Fischer == Init /\ [][Next]_v 
----------------------------------------------------------------------------
(***************************************************************************)
(* We define the formula Inv consisting of the conjunction of a            *)
(* type-correctness invariant TypeOK and the formula at the beginning of   *)
(* Section 5.2.2 asserting three properties.  TLC can check that Inv is an *)
(* inductive invariant for small models (a small set Time and few          *)
(* processes).                                                             *)
(***************************************************************************)        
TypeOK == /\ x \in Procs \cup {none}
          /\ pc \in [Procs -> {"ncs", "wait", "w1", "w2", "cs", "exit"}]
          /\ rt \in [Procs -> Times]
          /\ now \in Times

Inv == /\ 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)

(***************************************************************************)
(* We define the mutual exclusion invariant Mutex.  TLAPS easily proves    *)
(* that Inv implies Mutex, so the invariance of Inv implies that Fischer's *)
(* algorithm satisfies mutual exclusion.                                   *)
(***************************************************************************)
Mutex == \A p, q \in Procs : (p # q) => {pc[p], pc[q]} # {"cs"}

INSTANCE TLAPS
THEOREM Inv => Mutex
BY DEF Inv, TypeOK, Mutex
-----------------------------------------------------------------------------
(***************************************************************************)
(* Finally, we define LInv to be the invariant that is the conjunction of  *)
(* Inv with the invariant formula (5.2).  TLC can check that it is an      *)
(* inductive invariant.                                                    *)
(***************************************************************************)
LInv == /\ Inv
        /\ (x # none) => (pc[x] \in {"w2", "cs", "exit"})


=============================================================================
\* Modification History
\* Last modified Mon Oct 14 17:17:10 CEST 2024 by lamport
\* Created Wed Aug 03 18:14:42 PDT 2022 by lamport
