------------------------------ MODULE IPOFifo_pqs ------------------------------
(***************************************************************************)
(* This module defines the abstract program IPOFifo_pqs described in       *)
(* Section 7.6.3 of "A Science of Concurrent Programs" by Leslie Lamport.  *)
(* This program is obtained by obtained by adding auxiliary variables to   *)
(* program IPOFifo defined in module IIPOFifo, The module also defines the *)
(* refinement mapping under which IPOFifi_pqs implements program IFifo of  *)
(* module IFifo.                                                           *)
(*                                                                         *)
(* Here are the three auxiliary variables, in the order in which they are  *)
(* added.                                                                  *)
(*                                                                         *)
(*  Prophecy Variable p                                                    *)
(*  --------------------                                                   *)
(* The prophecy sequence variable p is explained in Section 7.6.3.1 of the *)
(* boook.  It predicts the order in which the elements of elts will be     *)
(* dequeued--that is, the sequence of elements that will be dequeued by an *)
(* EndPODeq action.  A prediction is appended to p when an element is      *)
(* added to elts.  Note that p is a sequence of data, identifier pairs not *)
(* just a sequencce of data items.  It predicts the element that the       *)
(* EndPODeq action removes from elts, not just the data value the Dequeue  *)
(* operation returns.                                                      *)
(*                                                                         *)
(* Like most prophecy variables, most of the the predictions p can make    *)
(* can't possibly be right.  Sometimes their impossibility can be          *)
(* determined even when the prophecy is made.  Logically, that makes no    *)
(* difference.  An impossible prediction just prevents dequeue operations  *)
(* from performing their EndPODeq actions.  Such prophecies would be ruled *)
(* out by a fairness requirement on the EndPODeq action.                   *)
(*                                                                         *)
(*  History Variable qBar                                                  *)
(*  ----------------------                                                 *)
(* As described in Section 7.6.3.2, qBar is a sequence of datums (elements *)
(* of Data \X Ids that equals pg \o eb , where pg is the sequence of       *)
(* datums that can be removed from the set elts by dequeue operations even *)
(* if no further enqueue operations are initiated, and eb is a (hopefully  *)
(* empty) sequence of datums in elts that can never be removed from elts   *)
(* by any dequeue operation.                                               *)
(*                                                                         *)
(*                     -------------                                       *)
(*                                                                         *)
(* Here is a description of how the hisory variable qBar is added that I   *)
(* wrote before writing the book.  It's more detailed than the one in the  *)
(* book, and I'm leaving it here because it might help some readers to     *)
(* understand its definition.                                              *)
(*                                                                         *)
(* The value of qBar is a sequence of elements that is approximately the   *)
(* value that the refinement mapping assigns to the variable `queue' of    *)
(* Fifo (except it contains not just the Data values that are in `queue'   *)
(* but also the identifier associated with that data value).  It is not    *)
(* exactly the value that implements `queue' because elements aren't added *)
(* to it at the right time.  (Stuttering variables will be added later to  *)
(* allow defining a refinement mapping that adds the elements to `queue'   *)
(* at the right time.)                                                     *)
(*                                                                         *)
(* To see how to construct qBar, let's pretend we know the entire infinite *)
(* sequence PP of predictions that will be made by the prophecy variable   *)
(* P.  Call PP correct iff it permits a behavior with infinitely many      *)
(* Dequeue operations (and hence infinitely many Enqueue operations).  If  *)
(* PP is correct, then p must always be a subsequence of PP of length      *)
(* equal to the number of elements in elt.  We construct qBar so that, in  *)
(* this case, it is the largest prefix of p all of whose elements are      *)
(* already in elts.  For example, suppose PP equals p1, p2, \ldots.        *)
(* Initially elts = {} and p = qBar = << >>.  Consider the following       *)
(* sequence of BeginPOEnq and EndPODeq actions, with the values they add   *)
(* or remove from elts, and the values of elts, p, and qBar they produce.  *)
(* (We can ignore the EndPOEnq and BeginPODeq actions.)                    *)
(*                                                                         *)
(*   BeginPOEnq of p2: elts = {p2}, p = <<p1>>, qBar = << >>               *)
(*                                                                         *)
(*   BeginPOEnq of p1: elts = {p1, p2}, p = <<p1, p2>>, qBar = <<p1,p2>>   *)
(*                                                                         *)
(*   EndPODeq of p2: elts = {p2}, p = <<p2>>, qBar = <<p2>>                *)
(*                                                                         *)
(*   BeginPOEnq of p7: elts = {p2, p7}, p = <<p2, p3>>, qBar = <<p2>>      *)
(*                                                                         *)
(* Note that two elements have been appended to qBar at the same time.     *)
(* Since Fifo appends elements to `queue' one at a time, we will need a    *)
(* stuttering variable to add an extra step so that under the refinement   *)
(* mapping they are added one at a time to `queue'.                        *)
(*                                                                         *)
(* If PP is correct, then the elements p3, ...  , p7 must be enqueued (not *)
(* necessarily in that order) before p7 can be dequeued.  But p controls   *)
(* only the order in which EndPODeq_p actions can dequeue elements.  It    *)
(* doesn't restrict EndPODeq_p actions.  Suppose the EndPOEnq_p action for *)
(* the BeginPOEnq_p action that enqueued p7 is now executed.  Since that   *)
(* action has to implement the EndDeq action of Fifo (because it changes   *)
(* the interface variable enq the way the EndDeq action does), p7 must be  *)
(* appended to qBar before the EndPODeq action occurs.  (We will use a     *)
(* stuttering variable to add the necessary step.)                         *)
(*                                                                         *)
(* At that point, it's still possible for p2 to be dequeued, but any       *)
(* further dequeueing should be impossible.  Therefore, PP is not correct. *)
(* Let's see why further dequeueing is impossible.  Since the predictions  *)
(* of PP determine what elements can be dequeued, for further dequeueing   *)
(* to occur, p3 must be the next element dequeued.  This means that p3     *)
(* must be enqueued and added to elts.  However, p7 is still in elts and   *)
(* its EndPOEnq operation has occcurred, so p7 \prec p3 must hold.  This   *)
(* implies that p7 must be dequeued before p3 is, something that the       *)
(* predictions of PP do not predict.  So, p3 and any elements other than   *)
(* p2 (which is in qBar) can never be dequeued and hence never removed     *)
(* from qBar.  So elements can keep being enqueued and appended to qBar by *)
(* the EndPOEnq actions, but once p2 is dequeued (if it ever is) no        *)
(* further dequeue operations can finish.                                  *)
(*                                                                         *)
(* The value of qBar always equals the concatenation of these two          *)
(* sequences (either or both of which could be empty) of elements in elts: *)
(*                                                                         *)
(*     Dequeueable: A prefix of the predictions in p that                  *)
(*                  could at that point be dequeued by a sequence          *)
(*                  of EndPODeq actions.                                   *)
(*                                                                         *)
(*     Nondequeuable: A sequence of elements of elts that cannot be        *)
(*                    dequeued by a sequence of EndPODeq actions,          *)
(*                    and were added to elts by an Enqueue operation       *)
(*                    that has completed.                                  *)
(*                                                                         *)
(* A sequence of predictions can be dequeued if it satisfies the following *)
(* two conditions:                                                         *)
(*                                                                         *)
(*     - Each of them predicts an element that is currently in elts.       *)
(*                                                                         *)
(*     - No two of them predict the same element.                          *)
(*                                                                         *)
(*     - If el1 is in the sequence of predictions and el2 \prec el1 for    *)
(*       some el2 \in elts, then el2 must be in the sequence and precede   *)
(*       el1 in it.                                                        *)
(*                                                                         *)
(* An element e in elts is appended to the Nondequable part of qBar by the *)
(* EndPOEnq_p action of the enqueue operation that added e to elts if e is *)
(* not already in qBar.  (If e is already in qBar, it must be in the       *)
(* Dequeueable part.) It has to be in qBar at that point because the       *)
(* EndPOEnq_p action must implement the EndEnq action of Fifo, and that    *)
(* value is in `queue' when the `EndEnq' step occurs.  (A stuttering step  *)
(* must be added before the EndPOEnq action so that, under the refinement  *)
(* mapping, the value is added to `queue' before that step.)               *)
(*                                                                         *)
(* A BeginPOEnq action that adds e should append e to qBar iff             *)
(*                                                                         *)
(* (1) The Nondequeueable part of qBar is empty and                        *)
(*                                                                         *)
(* (2) Appending e to qBar makes qBar a prefix of sequence p of            *)
(*     predictions that is dequeueable.                                    *)
(*                                                                         *)
(* Condition (2) holds iff (1) holds and                                   *)
(*                                                                         *)
(* (a) e is the prediction in the new value of p (the value after          *)
(*     execution of the BeginPOEnq action) that comes immediately after    *)
(*     the prefix of p that equals qBar, and                               *)
(*                                                                         *)
(* (b) there is no element ee in elt that is not in qBar such that         *)
(*     ee \prec e.                                                         *)
(*                                                                         *)
(* However, condition (b) is impossible if (1) holds, since ee \prec e can *)
(* hold iff the EndPOEnq action of the enqueue operation that added ee to  *)
(* elts has already occurred.  But since ee is not in qBar, it was not in  *)
(* qBar when that action occurred, so the action would have appended ee to *)
(* the Nondequeueable part of qBar, contradicting (1).  Therefore the      *)
(* EndPOEnq action that adds e to elts must append it to the end of qBar   *)
(* iff conditions (1) and (2a) hold.                                       *)
(*                                                                         *)
(* We saw in the example above that enqueueing p1 caused both p1 and p2 to *)
(* be appended to qBar.  In general, when the Nondequeueable part of qBar  *)
(* is empty, appending any element e to qBar should also cause the next    *)
(* element in p to be appended to qBar if it is in elts.  Therefore, if    *)
(* condition (1) holds, a BeginPOEnq action should set qBar to qBar \o     *)
(* seq, where seq is the maximal subsequence of p that follows the prefix  *)
(* qBar of p.                                                              *)
(*                                                                         *)
(* Finally, because the dequeueable prefix of qBar can be defined as a     *)
(* state function, there's no need to keep it in a history variable.       *)
(* Instead of adding the history variable qBar, we add a history variable  *)
(* h whose value is the nondequeueable suffix of qBar.  We can then        *)
(* consider qBar to be a state function whose value equals the dequeueable *)
(* prefix of p and the sequence q.                                         *)
(*                                                                         *)
(*                         ----------------------                          *)
(*                                                                         *)
(*  Stuttering Variable s                                                  *)
(*  ---------------------                                                  *)
(* As explained in Section 7.6.3.3, we need to add stuttering steps in     *)
(* three places to POFifo_pq to be able to define a refinement mapping     *)
(* under which POFifo implements Fifo:                                     *)
(*                                                                         *)
(* - Immediately before an EndPODeq_pq step we need to add one             *)
(*   stuttering step.                                                      *)
(*                                                                         *)
(* - immediately before an EndPOEnq step that appends an element to        *)
(*   qBar not in pg,  we need to execute one stuttering step.              *)
(*                                                                         *)
(* - Immediately after a BeginPOEnq_pq step we need to add as one          *)
(*    stuttering step for every element added to qBar.  That is, a number  *)
(*    of stuttering steps equal to amount by which the BeginPOEnq step     *)
(*    increases the length of qBar.                                        *)
(*                                                                         *)
(* We can add the required number of stuttering steps after every          *)
(* BeginPOEnq_pq step with a stuttering variable s as follows.             *)
(*                                                                         *)
(* 1.  The condition s = 0 is conjoined to the initial-state predicate.    *)
(*                                                                         *)
(* 2.  Replace the BeginPOEnq_pq(e) action by                              *)
(*                                                                         *)
(*       \/ (s = 0) /\ BeginPOEnq_pq(e) /\ (s' = exp)                      *)
(*       \/ (s > 0) /\ (s' = s-1) /\ UNCHANGED POv_pq                      *)
(*                                                                         *)
(*    where the expression exp is the number of  stuttering steps to       *)
(*    be added.                                                            *)
(*                                                                         *)
(* 3.  Replace each of the other three subactions A of PONext_pq by        *)
(*                                                                         *)
(*       (s = 0) /\ A /\ (s' = s)                                          *)
(*                                                                         *)
(* We can add a single stuttering step before every EndPOEnq_pq(d) step    *)
(* with a stuttering variable s in the same way, except replacing step 2   *)
(* by:                                                                     *)
(*                                                                         *)
(* 2.  \/ /\ (s = 0) /\ ENABLED EndPODeq_pq(d)                             *)
(*        /\ (s' = 1) /\ UNCHANGED POv_pq                                  *)
(*     \/ /\ (s = 1)                                                       *)
(*        /\ EndPODeq_pq(d) /\ (s' = 0)                                    *)
(*                                                                         *)
(* We need a stuttering step before an EndPOEnq_pq(e) step iff the step    *)
(* appends an element to q.  It doesn't hurt always to add the step, since *)
(* an extra stuttering step does no harm.  However, it's a bit more        *)
(* convenient not to do that.  We can add the stuttering step iff          *)
(* necessary by replacing step 2 with:                                     *)
(*                                                                         *)
(* 2.  \/ /\ (s = 0) /\ ENABLED EndPOEnq_pq(e)                             *)
(*        /\ IF ... THEN (s' = 1) /\ UNCHANGED POv_pq                      *)
(*                  ELSE EndPOEnq(e) /\ (s' = s)                           *)
(*     \/ /\ (s = 1)                                                       *)
(*        /\ EndPOEnq_pq(e) /\ (s' = 0)                                    *)
(*                                                                         *)
(* In order to use those stuttering steps in defining the refinement       *)
(* mapping, we want the stuttering variable to contain information about   *)
(* the action to which it's adding stuttering steps.  Those could be added *)
(* later with another history variable, but they can be put directly into  *)
(* s by making s a tuple one component of which is doing the counting down *)
(* and the other components are storing the information.  One such piece   *)
(* of information is the process taking the stuttering steps.              *)
(*                                                                         *)
(* Instead of adding these three kinds of stuttering steps with three      *)
(* different variables, we use a single stuttering variable with a         *)
(* component that indicates what kind of action it's adding the steps to.  *)
(***************************************************************************)
EXTENDS IPOFifo, Integers, Sequences, TLC

(***************************************************************************)
(* We will need the assumption on NoData to implement the constant of the  *)
(* same name in Fifo.                                                      *)
(***************************************************************************)
CONSTANT NoData
ASSUME  NoData \notin Data

(****************************************************************************
If I were writing this for myself, I would probably add these three
auxiliary variables all at once.  However, for pedagogical reasons, we
will add them one at a time to obtain three different abstract
programs.  We first add the prophecy variable p to POFifo to obtain the
abstract program POFifo_p.
****************************************************************************)
VARIABLE p
POv_p == <<POv, p>>

POTypeOK_p == POTypeOK /\ (p \in Seq(Datums))

POInit_p == POInit /\ p = << >>

BeginPOEnq_p(e) == /\ BeginPOEnq(e)
                   /\ \E el \in Datums : p' = Append(p, el)

EndPOEnq_p(e) ==  EndPOEnq(e) /\ (p' = p)

BeginPODeq_p(d) == BeginPODeq(d) /\ (p' = p)

(***************************************************************************)
(* The rules for adding a prophecy sequence variable would require us to   *)
(* define EndPODeq_p(d) by rewriting the definition of EndPODeq(d) to have *)
(* the form                                                                *)
(*                                                                         *)
(*    EndPODeq(d) == \E el \in Datums : A(el,d)                            *)
(*                                                                         *)
(* and defining                                                            *)
(*                                                                         *)
(*    EndPODeq_p(d) == A(p[1], d) /\ (p' = Tail(p))                        *)
(*                                                                         *)
(* We can do this by definining A(el,d) to be                              *)
(*                                                                         *)
(*    EndPODeq(d) /\ (elts' = elts \ {el})                                 *)
(*                                                                         *)
(* This definition of A(el,d) yields the following definition of           *)
(* EndPODeq_p(d).                                                          *)
(***************************************************************************)
EndPODeq_p(d) ==  EndPODeq(d) /\ (elts' = elts \ {p[1]}) /\ (p' = Tail(p))

PONext_p == \/ \E e \in EnQers : BeginPOEnq_p(e)  \/ EndPOEnq_p(e)
            \/ \E d \in DeQers : BeginPODeq_p(d)  \/ EndPODeq_p(d)
 
POFifo_p == POInit_p /\ [][PONext_p]_POv_p
-----------------------------------------------------------------------------
(***************************************************************************)
(* We next add the history variable qBar.  First we define the dequeueable *)
(* prefix pg of p.  Remember that it is the largest prefix satisfying this *)
(* condition:                                                              *)
(*                                                                         *)
(*     - Each element of it is in elts.                                    *)
(*                                                                         *)
(*     - No two of them predict the same element.                          *)
(*                                                                         *)
(*     - If el1 is in the prefix and el2 \prec el1 for some el2 \in elts,  *)
(*       then el2 must precede el1 in the prefix                           *)
(*                                                                         *)
(* It's tricky to get the definition right, so to check it I gave two two  *)
(* definitions.  The first comes directly from this definition, the second *)
(* is a recursive definition that is more efficiently executed by TLC.     *)
(* (Checking them against one another revealed several errors in both of   *)
(* them before they agreed.) The first definition requires the definition  *)
(* of SetMax(S) to be the maximum of a set of integers, defined to equal 0 *)
(* if S is the empty set.                                                  *)
(***************************************************************************)
SetMax(S) == IF S = {} THEN 0 ELSE CHOOSE n \in S : \A m \in S : n >= m

prefix(seq, n) == [j \in 1..n |-> seq[j]]

canDeque(seq) == \A i \in 1..Len(seq) :
                     /\ p[i] \in elts
                     /\ \A j \in 1..(i-1)  : p[j] # p[i]
                     /\ \A e \in elts:
                           e \prec p[i] => \E j \in 1..(i-1) : e = p[j]

                              
pg == LET n == SetMax({m \in 1..Len(p) : canDeque(prefix(p,m))})
      IN  prefix(p,n)
          
(***************************************************************************)
(* The state predicate pgE is defined by the recursive definition of pg    *)
(* that is more efficiently executed by TLC.  It evaluates maxdq(n,S)      *)
(* recursively, starting with maxdq(0,{}), and reaching maxdq(n,S) for n > *)
(* 0 iff the first n elements of p are dequeueable, where S is the set of  *)
(* elements in p.  The recursion stops when n is the length of p or        *)
(* element n+1 of p is not dequeueable.                                    *)
(*                                                                         *)
(* When model checking the program, we have TLC substitute pgE for pg.     *)
(***************************************************************************)
pgE == LET RECURSIVE maxdq(_,_)
               maxdq(n,S) == IF n = Len(p) 
                             THEN n
                             ELSE LET e == p[n+1]
                                  IN  IF /\ e \in elts \ S
                                         /\ \A ee \in elts \ (S \cup {e}) : 
                                                ~(ee \prec e)
                                        THEN maxdq(n+1, S \cup {e})
                                        ELSE n
          IN [i \in 1..maxdq(0,{}) |-> p[i]]
 
(***************************************************************************)
(* Define appendToH(e) the formula that, when executing an EndPOEnq(e)     *)
(* action, is true iff that action should append the datum enqueued by     *)
(* enqueuer e to q.  This is the case iff that datum is in elts but is not *)
(* in the sequence pg.                                                     *)
(***************************************************************************)
appendToH(e) == /\ adding[e] \in elts
                /\ \A i \in 1..Len(pg) : pg[i] # adding[e]
              
VARIABLE qBar

POv_pq == <<POv, p, qBar>>

POTypeOK_pq == POTypeOK_p /\ (qBar \in Seq(Datums))

POInit_pq == POInit_p /\ (qBar = << >>)

BeginPOEnq_pq(e) == BeginPOEnq_p(e) /\  (qBar'=qBar)

EndPOEnq_pq(e) ==  /\ EndPOEnq_p(e) 
                   /\ qBar' = IF appendToH(e)
                             THEN Append(qBar, adding[e])
                             ELSE qBar 

BeginPODeq_pq(d) == BeginPODeq_p(d) /\ (qBar' = qBar)

EndPODeq_pq(d) == EndPODeq_p(d) /\ (qBar' = qBar)

PONext_pq == \/ \E e \in EnQers : BeginPOEnq_pq(e)  \/ EndPOEnq_pq(e)
             \/ \E d \in DeQers : BeginPODeq_pq(d)  \/ EndPODeq_pq(d)
 
IPOFifo_pq == POInit_pq /\ [][PONext_pq]_POv_pq
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now add stuttering variable s as described above.  Instead of        *)
(* writing an expression ENABLED A for the two actions A having a          *)
(* stuttering step added before them, I have "evaluated" that ENABLED      *)
(* expression.                                                             *)
(***************************************************************************)
VARIABLE s

POv_pqs == <<POv, p, qBar, s>>

POTypeOK_pqs == /\ POTypeOK_pq 
                /\ s \in {<<0>>} \cup (Nat \X {"BeginEnq"} \X EnQers)  
                           \cup (Nat \X {"EndEnq"} \X EnQers)
                           \cup (Nat \X {"EndDeq"} \X DeQers \X Datums)

POInit_pqs == POInit_pq /\ (s = <<0>>)

BeginPOEnq_pqs(e) == \/ /\ s[1] = 0
                        /\ BeginPOEnq_pq(e) 
                        /\ s' = <<Len(pg') - Len(pg), "BeginEnq", e>>
                     \/ /\ (s[1] > 0) /\ (s[2] = "BeginEnq") /\ (s[3] = e)
                        /\ (s' = <<s[1] - 1, "BeginEnq", e>>) 
                        /\ UNCHANGED POv_pq

EndPOEnq_pqs(e) ==  \/ /\ (s[1] = 0) /\ (enq[e] # Done)
                       /\  IF appendToH(e)
                             THEN  /\ s' = <<1, "EndEnq", e>>
                                   /\ UNCHANGED POv_pq
                             ELSE  /\ EndPOEnq_pq(e)
                                   /\ s' = s
                    \/ /\ (s[1] = 1) /\ (s[2] = "EndEnq")  /\ (s[3] = e)
                       /\ EndPOEnq_pq(e)
                       /\ s' = <<0>>

BeginPODeq_pqs(d) ==  (s[1] = 0) /\ BeginPODeq_pq(d)  /\ (s' = s)

EndPODeq_pqs(d) == \/ /\ (s[1] = 0) /\ (deq[d] = Busy) /\  (pg # << >>)
                      /\ s' = <<1, "EndDeq", d (*, Head(pg) *)>> 
                      /\ UNCHANGED POv_pq
                   \/ /\ (s[1] = 1) /\ (s[2] = "EndDeq")  /\ (s[3] = d)    
                      /\ EndPODeq_pq(d) 
                      /\ s' = <<0>>

PONext_pqs == \/ \E e \in EnQers : BeginPOEnq_pqs(e)  \/ EndPOEnq_pqs(e)
              \/ \E d \in DeQers : BeginPODeq_pqs(d)  \/ EndPODeq_pqs(d)
 
IPOFifo_pqs == POInit_pqs /\ [][PONext_pqs]_POv_pqs
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the state function queueBar, deqInnerBar, and enqInnerBar *)
(* so that POFifo_pqs implements Fifo under a refinement mapping that      *)
(* implements the internal variables queue, deqInner, and enqInner with    *)
(* these state functions.                                                  *)
(*                                                                         *)
(* First, we define the sequence queuE of elements whose data values       *)
(* define queueBar.  It equals qBar, except that:                          *)
(*                                                                         *)
(* - When adding stuttering steps after BeginPOEnq_pq, the elements at the *)
(*   end of pg have to be appended one at a time by those stuttering       *)
(*   steps.                                                                *)
(*                                                                         *)
(* - The head of pg has to be removed by the stutterng step added          *)
(*   before EndPODeq_pq.                                                   *)
(*                                                                         *)
(* - The last element of qBar has to be appended by a stuttering step      *)
(*   added before EndPOEnq_pq.                                             *)
(***************************************************************************)
queuE ==
   (IF s[1] > 0 
      THEN IF s[2] = "BeginEnq"
             THEN  [i \in 1..(Len(pg) - s[1]) |-> pg[i]]
             ELSE IF s[2] = "EndDeq"
                    THEN Tail(pg)
                    ELSE pg
      ELSE pg)  
   \o 
   (IF (s[1] > 0) /\ (s[2] = "EndEnq")
      THEN Append(qBar, adding[s[3]])
      ELSE qBar )

queueBar == [i \in 1..Len(queuE) |-> queuE[i][1]]

(***************************************************************************)
(* The state predicates deqInnerBar and enqInnerBar that are substituted   *)
(* for variables deq and enq of the Fifo program by the refinement mapping *)
(* are defined so that they make deq and enq change their values the way   *)
(* they are supposed to when queueBar changes.  I found it straightforward *)
(* to write the definitions, but having the model checker to find errors   *)
(* helped.                                                                 *)
(***************************************************************************)
deqInnerBar == [d \in DeQers |->
                  IF deq[d] = Busy
                    THEN IF (s[1] > 0) /\ (s[2] = "EndDeq") /\ (s[3] = d)
                           THEN Head(pg)[1]
                           ELSE NoData
                    ELSE deq[d] ]

                    
enqInnerBar == [e \in EnQers |-> 
                  IF \/ enq[e] = Done
                     \/ \E i \in 1..Len(queuE) : adding[e] = queuE[i]
                     \/ adding[e] \notin elts
                     \/ (s[1] > 0) /\ (s[2]="EndDeq") /\ (adding[e]=Head(p))
                        (***************************************************)
                        (* This disjunct is needed because there is one    *)
                        (* case in which the stuttering step after         *)
                        (* BeginPOEnq(e) that implements the DoEnq(e) of   *)
                        (* IFifo has occurred, the EndPOEnq(e) step has    *)
                        (* not occurred, and adding[e] is neither in elts  *)
                        (* nor in queuE.  That's when the stuttering step  *)
                        (* before the EndPODeq(d) step that dequeues       *)
                        (* adding[e] has occurred, removing adding[e] from *)
                        (* queuE, but the following EndPODeq(d) step has   *)
                        (* not occurred.  In such a state, only this       *)
                        (* conjunct of the IF condition is true.           *)
                        (***************************************************) 
                    THEN Done
                    ELSE Busy]
 
 (**************************************************************************)
 (* Finally, we define F!IFifo to equal IFifo WITH queue <- queueBar, ...  *)
 (* and assert that IPOFifo_pqs implies F!Fifo.                            *)
 (**************************************************************************)
 F == INSTANCE IFifo WITH queue <- queueBar, deqInner <- deqInnerBar,
                            enqInner <- enqInnerBar
                            
 THEOREM IPOFifo_pqs => F!IFifo          
 

=============================================================================
