-------------------------------- MODULE IFifo --------------------------------
(***************************************************************************)
(* A standard linearizable specification of a Fifo queue with a set EnQers *)
(* of processes that perform Enqueue operations and a set of DeQers        *)
(* processes that perform Dequeue operations.  Linearizability means that  *)
(* each of these two operations are performed by a sequence of three       *)
(* atomic actions:                                                         *)
(*                                                                         *)
(*    - A Begin action that modifies the interface variables and, for      *)
(*      an Enqueue operation, provides the value to be enqueued.           *)
(*                                                                         *)
(*    - A Do action that changes only internal variables and performs      *)
(*      the Enqueue or Dequeue operation to the queue, whose contents are  *)
(*      described by an internal variable.                                 *)
(*                                                                         *)
(*    - An End action that modifies the interface variables and, for       *)
(*      a Dequeue operation, returns the value dequeued.                   *)
(***************************************************************************)
EXTENDS Integers, Sequences, TLC

CONSTANTS EnQers, DeQers, \* The sets of enqueuer and dequeuer processes.
          Data,           \* The set of data items that can be enqueued
          NoData,         \* An arbitrary value not an element of Data.
          Done, Busy      \* Two arbitrary values, signifying an operation's
                          \* status.

ASSUME /\ Done     \notin Data
       /\ Busy     \notin Data
       /\ NoData   \notin Data

(***************************************************************************)
(* The variables:                                                          *)
(*                                                                         *)
(*    - enq and deq are the interface variables that are changed by the    *)
(*      Begin and End actions as follows:                                  *)
(*                                                                         *)
(*        deq[d]: Set to Busy by BeginDeq(d) and to the dequeued value     *)
(*                by EndDeq(d)                                             *)
(*                                                                         *)
(*        enq[e]: Set by BeginEnq(e) to the value to be enqueued, and to   *)
(*                Done by EndEnq(d)                                        *)
(*                                                                         *)
(*    - queue is the internal variable holding the contents of the queue.  *)
(*                                                                         *)
(*    - enqInner and deqInner are internal variables that hold the state   *)
(*      of a process during an operation as follows:                       *)
(*                                                                         *)
(*        deqInner[d]:  Set to NoData by BeginDeq(d) and to the dequeued   *)
(*                      value by DoDeq(d).                                 *)
(*                                                                         *)
(*        enqInner[e]:  Set by BeginEnq(e) to Busy, and by DoEnq(e) to     *)
(*                      Done.                                              *)
(***************************************************************************)
VARIABLES enq, deq, queue, enqInner, deqInner
vars == <<enq, deq, queue, enqInner, deqInner>>

TypeOK == /\ enq \in [EnQers -> Data \cup {Done}]
          /\ deq \in [DeQers -> Data \cup {Busy}]
          /\ queue \in Seq(Data)
          /\ enqInner \in [EnQers -> {Done, Busy}]
          /\ deqInner \in [DeQers -> Data \cup {NoData}]

Init == /\ enq = [e \in EnQers |-> Done]
        /\ deq \in [DeQers -> Data]
        /\ queue = << >>
        /\ enqInner = [e \in EnQers |-> Done] 
        /\ deqInner = deq
        
BeginEnq(e) == /\ enq[e] = Done 
               /\ \E D \in Data : enq' = [enq EXCEPT ![e] = D]
               /\ enqInner' = [enqInner EXCEPT ![e] = Busy]
               /\ UNCHANGED <<deq, queue, deqInner>>
               
DoEnq(e) == /\ enqInner[e] = Busy
            /\ queue' = Append(queue, enq[e])
            /\  enqInner' = [enqInner EXCEPT ![e] = Done]
            /\ UNCHANGED <<deq, enq, deqInner>>
            
EndEnq(e) == /\ enq[e] # Done
             /\ enqInner[e] = Done
             /\ enq' = [enq EXCEPT ![e] =  Done]
             /\ UNCHANGED <<deq, queue, enqInner, deqInner>>

BeginDeq(d) == /\ deq[d] # Busy
               /\ deq' = [deq EXCEPT ![d] =  Busy] 
               /\ deqInner' = [deqInner EXCEPT ![d] =  NoData]
               /\ UNCHANGED <<enq, queue, enqInner>>
               
DoDeq(d) == /\ deq[d] = Busy
            /\ deqInner[d] = NoData
            /\ queue # << >>
            /\ deqInner' = [deqInner EXCEPT ![d] =  Head(queue)]
            /\ queue' = Tail(queue)
            /\ UNCHANGED <<enq, deq, enqInner>>

EndDeq(d) == /\ deq[d] = Busy
             /\ deqInner[d] # NoData
             /\ deq' = [deq EXCEPT ![d] = deqInner[d]]
             /\ UNCHANGED <<enq, queue, enqInner, deqInner>>
             
Next == \/ \E e \in EnQers : BeginEnq(e) \/ DoEnq(e) \/ EndEnq(e)
        \/ \E d \in DeQers : BeginDeq(d) \/ DoDeq(d) \/ EndDeq(d)
        
IFifo == Init /\ [][Next]_vars

Liveness == /\ \A e \in EnQers : WF_vars(DoEnq(e) \/ EndEnq(e))
            /\ \A d \in DeQers : WF_vars(DoDeq(d) \/ EndDeq(d))
            
ILiveFifo == IFifo /\ Liveness
=============================================================================
\* Modification History
\* Last modified Sat Oct 19 11:36:27 CEST 2024 by lamport
\* Created Thu Sep 15 06:53:21 PDT 2022 by lamport
