Skip to content

Instantly share code, notes, and snippets.

@pjmolina

pjmolina/DCSA.tla

Created May 30, 2017 09:31
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pjmolina/8133fbbaaffd488ee31596e373aa5db5 to your computer and use it in GitHub Desktop.
Save pjmolina/8133fbbaaffd488ee31596e373aa5db5 to your computer and use it in GitHub Desktop.
Download ZIP
Sample of TLA + PlusCalc algorithm from http://lamport.azurewebsites.net/tla/DCAS.tla
Raw
DCSA.tla
------------------------------- MODULE DCAS ---------------------------------
EXTENDS Naturals, Sequences, TLC, FiniteSets
(***************************************************************************)
(* Last and Front are like Head and Tail, except for the back (right-hand *)
(* end) rather than the front (left-hand) end of the sequence/list/queue. *)
(***************************************************************************)
Last(q) == q[Len(q)]
Front(q) == [i \in 1..(Len(q)-1) |-> q[i]]
(***************************************************************************)
(* Here are the constant parameters of the algorithm. *)
(***************************************************************************)
CONSTANTS Val, \* The set of all values that can be enqueued
Address, \* The set of heap addresses
Dummy, \* The address of the dummy node
Procs \* The set of all processes (threads)
ASSUME Dummy \in Address
null == CHOOSE n: n \notin Address
(*************************************************************************)
(* Defines null to be an arbitrary value that is not a heap address. *)
(*************************************************************************)
Node == [R : Address \cup {null}, L : Address \cup {null}, V : Val]
(*************************************************************************)
(* This defines the set of all nodes (the Node type). It asserts that *)
(* an element of Node is a record with R and L fields that are either *)
(* addresses or null, and a V field that is a Val or null. *)
(* *)
(* This definition would be used in a type-correctness invariant, which *)
(* I didn't bother to write and check. (The model checker should find *)
(* any type errors during execution when it tries to evaluate a function *)
(* on an element not in its domain--for example, evaluating an *)
(* expression exp.c when exp is not a record with a c field.) *)
(*************************************************************************)
DummyNode == [R |-> Dummy, L |-> Dummy, V |-> null]
(*************************************************************************)
(* The dummy node (whose address is Dummy). *)
(*************************************************************************)
InitNode == [R |-> null, L |-> null, V |-> null]
(*
--algorithm Snark {
(***************************************************************************)
(* The global variables, and their initial values. *)
(***************************************************************************)
variables
LeftHat = Dummy,
RightHat = Dummy,
(***********************************************************************)
(* LeftHat and RightHat are from the original algorithm. *)
(***********************************************************************)
Heap = [a \in Address |-> IF a = Dummy THEN DummyNode ELSE InitNode],
(***********************************************************************)
(* The heap, which is an array indexed by addresses. Initially *)
(* Heap[Dummy] = DummyNode and Heap[i] = InitNode for all addresses *)
(* i other than Dummy. *)
(***********************************************************************)
freeList = Address \ {Dummy},
(***********************************************************************)
(* The set of addresses of free heap elements. *)
(***********************************************************************)
rVal = [p \in Procs |-> "okay"],
(***********************************************************************)
(* rVal[p] is the last value returned by a procedure call n process *)
(* p. The initial value doesn't matter, but it needs to be an array *)
(* (function) indexed by (with domain) Procs. *)
(***********************************************************************)
queue = << >> ,
sVal = [p \in Procs |-> TRUE] ;
(***********************************************************************)
(* These are the dummy variables introduced to check the algorithm. *)
(***********************************************************************)
macro New(result) {
(*************************************************************************)
(* A macro that represents the C code "result = new Node()". I *)
(* originally intended to have a garbage-collection process, but I *)
(* decided it wasn't likely to help detect errors. So, I just let the *)
(* system just run out of heap. *)
(*************************************************************************)
if (freeList # {}) {
result := CHOOSE a \in freeList : TRUE ;
freeList := freeList \ {result} ;
} else result := null
}
macro DCAS(result, addr1, addr2, old1, old2, new1, new2) {
if ( (addr1 = old1) /\
(addr2 = old2)) {
addr1 := new1 ||
addr2 := new2 ;
result := TRUE;
} else result := FALSE; }
procedure pushRight(v)
variables nd, rh, rhR, lh, temp; {
L2: New(nd) ;
if (nd = null) { rVal[self] := "full"; L3: return } ;
L4: Heap[nd].R := Dummy ||
Heap[nd].V := v ;
L6: while (TRUE) {
rh := RightHat;
L8: rhR := Heap[rh].R;
L9: if (rhR = rh) {
Heap[nd].L := Dummy;
lh := LeftHat; \* this statement should have been labeled
L12: DCAS(temp, RightHat, LeftHat, rh, lh, nd, nd) ;
if (temp) {
queue := queue \o <<Heap[nd].V>> ;
rVal[self] := "okay"; L13: return}
} else {
L15: Heap[nd].L := rh;
L16: DCAS(temp, RightHat, Heap[rh].R, rh, rhR, nd, nd) ;
if (temp) {
queue := queue \o <<Heap[nd].V>> ;
rVal[self] := "okay"; L17: return }
} } }
procedure popRight()
variables rh, lh, rhL, temp, result; {
M2: while (TRUE) {
rh := RightHat;
sVal[self] := (queue = << >>) ;
M4: lh := LeftHat;
M5: if (Heap[rh].R = rh) {
assert sVal[self] \/ (queue = << >>) ;
rVal[self] := "empty"; return ;} ;
M6: if (rh = lh) {
DCAS(temp, RightHat, LeftHat, rh, lh, Dummy, Dummy) ;
if (temp) {
sVal[self] := Last(queue) ;
queue := Front(queue) ;
M8: rVal[self] := Heap[rh].V ;
assert rVal[self] = sVal[self]; return;}
} else {
M10: rhL := Heap[rh].L ;
M11: DCAS(temp, RightHat, Heap[rh].L, rh, rhL, rhL, rh) ;
if (temp) {
sVal[self] := Last(queue) ;
queue := Front(queue) ;
M12: result := Heap[rh].V;
assert result = sVal[self] ;
M13: Heap[rh].R := Dummy ||
Heap[rh].V := null;
rVal[self] := result ; return ;
} } } }
procedure pushLeft(v)
variables nd, rh, lhL, lh, temp; {
N2: New(nd) ;
if (nd = null) {rVal[self] := "full"; N1a: return ;} ;
N4: Heap[nd].L := Dummy ||
Heap[nd].V := v;
N6: while (TRUE) {
lh := LeftHat;
N8: lhL := Heap[lh].L;
if (lhL = lh) {
N10: Heap[nd].R := Dummy;
N11: rh := RightHat;
N12: DCAS(temp, LeftHat, RightHat, lh, rh, nd, nd) ;
if (temp) {
queue := <<Heap[nd].V>> \o queue ;
rVal[self] := "okay"; N13: return;}
} else {
N15: Heap[nd].R := lh;
N16: DCAS(temp, LeftHat, Heap[lh].L, lh, lhL, nd, nd) ;
if (temp) {
queue := <<Heap[nd].V>> \o queue ;
rVal[self] := "okay"; N17: return }
} } }
procedure popLeft()
variables rh, lh, lhR, temp, result; {
O2: while (TRUE) {
lh := LeftHat;
sVal[self] := (queue = << >>) ;
O4: rh := RightHat;
O5: if (Heap[lh].L = lh) {
assert sVal[self] \/ (queue = << >>) ;
rVal[self] := "empty"; return ;} ;
O6: if (lh = rh) {
DCAS(temp, LeftHat, RightHat, lh, rh, Dummy, Dummy) ;
if (temp) {
sVal[self] := Head(queue) ;
queue := Tail(queue) ;
O8: rVal[self] := Heap[lh].V;
assert rVal[self] = sVal[self] ;
return; }
} else {
O10: lhR := Heap[lh].R;
O11: DCAS(temp, LeftHat, Heap[lh].R, lh, lhR, lhR, lh) ;
if (temp) {
sVal[self] := Head(queue) ;
queue := Tail(queue) ;
O12: result := Heap[lh].V;
assert result = sVal[self] ;
O13: Heap[lh].L := Dummy ||
Heap[lh].V := null;
rVal[self] := result; return ;
} } } }
process (test \in Procs)
(*************************************************************************)
(* A process just nondeterministically calls one of the four procedures, *)
(* using a nondeterministically chosen element of Val as the push *)
(* procedures' arguments. *)
(*************************************************************************)
{
T1: while(TRUE) {
either \* push
with (pushedVal \in Val) {
either call pushLeft(pushedVal) or call pushRight(pushedVal)} ;
or \* pop
either call popLeft() or call popRight() ;
}
} }
*)
\* BEGIN TRANSLATION
\* Procedure variable nd of procedure pushRight at line 104 col 15 changed to nd_
\* Procedure variable rh of procedure pushRight at line 104 col 19 changed to rh_
\* Procedure variable lh of procedure pushRight at line 104 col 28 changed to lh_
\* Procedure variable temp of procedure pushRight at line 104 col 32 changed to temp_
\* Procedure variable rh of procedure popRight at line 129 col 12 changed to rh_p
\* Procedure variable lh of procedure popRight at line 129 col 16 changed to lh_p
\* Procedure variable temp of procedure popRight at line 129 col 25 changed to temp_p
\* Procedure variable result of procedure popRight at line 129 col 31 changed to result_
\* Procedure variable rh of procedure pushLeft at line 159 col 16 changed to rh_pu
\* Procedure variable lh of procedure pushLeft at line 159 col 25 changed to lh_pu
\* Procedure variable temp of procedure pushLeft at line 159 col 29 changed to temp_pu
\* Parameter v of procedure pushRight at line 103 col 21 changed to v_
VARIABLES LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, pc, stack, v_,
nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result
vars == << LeftHat, RightHat, Heap, freeList, rVal, queue, sVal, pc, stack,
v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v,
nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ LeftHat = Dummy
/\ RightHat = Dummy
/\ Heap = [a \in Address |-> IF a = Dummy THEN DummyNode ELSE InitNode]
/\ freeList = Address \ {Dummy}
/\ rVal = [p \in Procs |-> "okay"]
/\ queue = << >>
/\ sVal = [p \in Procs |-> TRUE]
(* Procedure pushRight *)
/\ v_ = [ self \in ProcSet |-> {}]
/\ nd_ = [ self \in ProcSet |-> {}]
/\ rh_ = [ self \in ProcSet |-> {}]
/\ rhR = [ self \in ProcSet |-> {}]
/\ lh_ = [ self \in ProcSet |-> {}]
/\ temp_ = [ self \in ProcSet |-> {}]
(* Procedure popRight *)
/\ rh_p = [ self \in ProcSet |-> {}]
/\ lh_p = [ self \in ProcSet |-> {}]
/\ rhL = [ self \in ProcSet |-> {}]
/\ temp_p = [ self \in ProcSet |-> {}]
/\ result_ = [ self \in ProcSet |-> {}]
(* Procedure pushLeft *)
/\ v = [ self \in ProcSet |-> {}]
/\ nd = [ self \in ProcSet |-> {}]
/\ rh_pu = [ self \in ProcSet |-> {}]
/\ lhL = [ self \in ProcSet |-> {}]
/\ lh_pu = [ self \in ProcSet |-> {}]
/\ temp_pu = [ self \in ProcSet |-> {}]
(* Procedure popLeft *)
/\ rh = [ self \in ProcSet |-> {}]
/\ lh = [ self \in ProcSet |-> {}]
/\ lhR = [ self \in ProcSet |-> {}]
/\ temp = [ self \in ProcSet |-> {}]
/\ result = [ self \in ProcSet |-> {}]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in Procs -> "T1"]
L2(self) == /\ pc[self] = "L2"
/\ IF freeList # {}
THEN /\ nd_' = [nd_ EXCEPT ![self] = CHOOSE a \in freeList : TRUE]
/\ freeList' = freeList \ {nd_'[self]}
ELSE /\ nd_' = [nd_ EXCEPT ![self] = null]
/\ UNCHANGED freeList
/\ IF nd_'[self] = null
THEN /\ rVal' = [rVal EXCEPT ![self] = "full"]
/\ pc' = [pc EXCEPT ![self] = "L3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "L4"]
/\ UNCHANGED rVal
/\ UNCHANGED << LeftHat, RightHat, Heap, queue, sVal, stack, v_,
rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p,
result_, v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh,
lhR, temp, result >>
L3(self) == /\ pc[self] = "L3"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_]
/\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_]
/\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR]
/\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_]
/\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_]
/\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
L4(self) == /\ pc[self] = "L4"
/\ Heap' = [Heap EXCEPT ![nd_[self]].R = Dummy,
![nd_[self]].V = v_[self]]
/\ pc' = [pc EXCEPT ![self] = "L6"]
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
L6(self) == /\ pc[self] = "L6"
/\ rh_' = [rh_ EXCEPT ![self] = RightHat]
/\ pc' = [pc EXCEPT ![self] = "L8"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
L8(self) == /\ pc[self] = "L8"
/\ rhR' = [rhR EXCEPT ![self] = Heap[rh_[self]].R]
/\ pc' = [pc EXCEPT ![self] = "L9"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
L9(self) == /\ pc[self] = "L9"
/\ IF rhR[self] = rh_[self]
THEN /\ Heap' = [Heap EXCEPT ![nd_[self]].L = Dummy]
/\ lh_' = [lh_ EXCEPT ![self] = LeftHat]
/\ pc' = [pc EXCEPT ![self] = "L12"]
ELSE /\ pc' = [pc EXCEPT ![self] = "L15"]
/\ UNCHANGED << Heap, lh_ >>
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, temp_, rh_p, lh_p, rhL,
temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu,
rh, lh, lhR, temp, result >>
L12(self) == /\ pc[self] = "L12"
/\ IF (RightHat = rh_[self]) /\
(LeftHat = lh_[self])
THEN /\ /\ LeftHat' = nd_[self]
/\ RightHat' = nd_[self]
/\ temp_' = [temp_ EXCEPT
![self] = TRUE]
ELSE /\ temp_' = [temp_ EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, RightHat >>
/\ IF temp_'[self]
THEN /\ queue' = queue \o <<Heap[nd_[self]].V>>
/\ rVal' = [rVal EXCEPT ![self] = "okay"]
/\ pc' = [pc EXCEPT ![self] = "L13"]
ELSE /\ pc' = [pc EXCEPT ![self] = "L6"]
/\ UNCHANGED << rVal, queue >>
/\ UNCHANGED << Heap, freeList, sVal, stack, v_, nd_, rh_, rhR,
lh_, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
L13(self) == /\ pc[self] = "L13"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_]
/\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_]
/\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR]
/\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_]
/\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_]
/\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
L15(self) == /\ pc[self] = "L15"
/\ Heap' = [Heap EXCEPT ![nd_[self]].L = rh_[self]]
/\ pc' = [pc EXCEPT ![self] = "L16"]
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
L16(self) == /\ pc[self] = "L16"
/\ IF (RightHat = rh_[self]) /\
((Heap[rh_[self]].R) = rhR[self])
THEN /\ /\ Heap' = [Heap EXCEPT ![rh_[self]].R = nd_[self]]
/\ RightHat' = nd_[self]
/\ temp_' = [temp_ EXCEPT
![self] = TRUE]
ELSE /\ temp_' = [temp_ EXCEPT
![self] = FALSE]
/\ UNCHANGED << RightHat, Heap >>
/\ IF temp_'[self]
THEN /\ queue' = queue \o <<Heap'[nd_[self]].V>>
/\ rVal' = [rVal EXCEPT ![self] = "okay"]
/\ pc' = [pc EXCEPT ![self] = "L17"]
ELSE /\ pc' = [pc EXCEPT ![self] = "L6"]
/\ UNCHANGED << rVal, queue >>
/\ UNCHANGED << LeftHat, freeList, sVal, stack, v_, nd_, rh_, rhR,
lh_, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
L17(self) == /\ pc[self] = "L17"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd_' = [nd_ EXCEPT ![self] = Head(stack[self]).nd_]
/\ rh_' = [rh_ EXCEPT ![self] = Head(stack[self]).rh_]
/\ rhR' = [rhR EXCEPT ![self] = Head(stack[self]).rhR]
/\ lh_' = [lh_ EXCEPT ![self] = Head(stack[self]).lh_]
/\ temp_' = [temp_ EXCEPT ![self] = Head(stack[self]).temp_]
/\ v_' = [v_ EXCEPT ![self] = Head(stack[self]).v_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, rh_p, lh_p, rhL, temp_p, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
pushRight(self) == L2(self) \/ L3(self) \/ L4(self) \/ L6(self)
\/ L8(self) \/ L9(self) \/ L12(self) \/ L13(self)
\/ L15(self) \/ L16(self) \/ L17(self)
M2(self) == /\ pc[self] = "M2"
/\ rh_p' = [rh_p EXCEPT ![self] = RightHat]
/\ sVal' = [sVal EXCEPT ![self] = (queue = << >>)]
/\ pc' = [pc EXCEPT ![self] = "M4"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
stack, v_, nd_, rh_, rhR, lh_, temp_, lh_p, rhL,
temp_p, result_, v, nd, rh_pu, lhL, lh_pu, temp_pu,
rh, lh, lhR, temp, result >>
M4(self) == /\ pc[self] = "M4"
/\ lh_p' = [lh_p EXCEPT ![self] = LeftHat]
/\ pc' = [pc EXCEPT ![self] = "M5"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
M5(self) == /\ pc[self] = "M5"
/\ IF Heap[rh_p[self]].R = rh_p[self]
THEN /\ Assert(sVal[self] \/ (queue = << >>),
"Failure of assertion at line line 135, column 13.")
/\ rVal' = [rVal EXCEPT ![self] = "empty"]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh_p' = [rh_p EXCEPT
![self] = Head(stack[self]).rh_p]
/\ lh_p' = [lh_p EXCEPT
![self] = Head(stack[self]).lh_p]
/\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL]
/\ temp_p' = [temp_p EXCEPT
![self] = Head(stack[self]).temp_p]
/\ result_' = [result_ EXCEPT
![self] = Head(stack[self]).result_]
/\ stack' = [stack EXCEPT
![self] = Tail(stack[self])]
ELSE /\ pc' = [pc EXCEPT ![self] = "M6"]
/\ UNCHANGED << rVal, stack, rh_p, lh_p, rhL, temp_p,
result_ >>
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_,
nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL,
lh_pu, temp_pu, rh, lh, lhR, temp, result >>
M6(self) == /\ pc[self] = "M6"
/\ IF rh_p[self] = lh_p[self]
THEN /\ IF (RightHat = rh_p[self]) /\
(LeftHat = lh_p[self])
THEN /\ /\ LeftHat' = Dummy
/\ RightHat' = Dummy
/\ temp_p' = [temp_p EXCEPT
![self] = TRUE]
ELSE /\ temp_p' = [temp_p EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, RightHat >>
/\ IF temp_p'[self]
THEN /\ sVal' = [sVal EXCEPT ![self] = Last(queue)]
/\ queue' = Front(queue)
/\ pc' = [pc EXCEPT
![self] = "M8"]
ELSE /\ pc' = [pc EXCEPT
![self] = "M2"]
/\ UNCHANGED << queue, sVal >>
ELSE /\ pc' = [pc EXCEPT ![self] = "M10"]
/\ UNCHANGED << LeftHat, RightHat, queue, sVal, temp_p >>
/\ UNCHANGED << Heap, freeList, rVal, stack, v_, nd_, rh_, rhR,
lh_, temp_, rh_p, lh_p, rhL, result_, v, nd, rh_pu,
lhL, lh_pu, temp_pu, rh, lh, lhR, temp, result >>
M10(self) == /\ pc[self] = "M10"
/\ rhL' = [rhL EXCEPT ![self] = Heap[rh_p[self]].L]
/\ pc' = [pc EXCEPT ![self] = "M11"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
M11(self) == /\ pc[self] = "M11"
/\ IF (RightHat = rh_p[self]) /\
((Heap[rh_p[self]].L) = rhL[self])
THEN /\ /\ Heap' = [Heap EXCEPT ![rh_p[self]].L = rh_p[self]]
/\ RightHat' = rhL[self]
/\ temp_p' = [temp_p EXCEPT
![self] = TRUE]
ELSE /\ temp_p' = [temp_p EXCEPT
![self] = FALSE]
/\ UNCHANGED << RightHat, Heap >>
/\ IF temp_p'[self]
THEN /\ sVal' = [sVal EXCEPT ![self] = Last(queue)]
/\ queue' = Front(queue)
/\ pc' = [pc EXCEPT ![self] = "M12"]
ELSE /\ pc' = [pc EXCEPT ![self] = "M2"]
/\ UNCHANGED << queue, sVal >>
/\ UNCHANGED << LeftHat, freeList, rVal, stack, v_, nd_, rh_, rhR,
lh_, temp_, rh_p, lh_p, rhL, result_, v, nd,
rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR, temp,
result >>
M12(self) == /\ pc[self] = "M12"
/\ result_' = [result_ EXCEPT ![self] = Heap[rh_p[self]].V]
/\ Assert(result_'[self] = sVal[self],
"Failure of assertion at line line 151, column 11.")
/\ pc' = [pc EXCEPT ![self] = "M13"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
M13(self) == /\ pc[self] = "M13"
/\ Heap' = [Heap EXCEPT ![rh_p[self]].R = Dummy,
![rh_p[self]].V = null]
/\ rVal' = [rVal EXCEPT ![self] = result_[self]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh_p' = [rh_p EXCEPT ![self] = Head(stack[self]).rh_p]
/\ lh_p' = [lh_p EXCEPT ![self] = Head(stack[self]).lh_p]
/\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL]
/\ temp_p' = [temp_p EXCEPT ![self] = Head(stack[self]).temp_p]
/\ result_' = [result_ EXCEPT ![self] = Head(stack[self]).result_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, freeList, queue, sVal, v_, nd_,
rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
M8(self) == /\ pc[self] = "M8"
/\ rVal' = [rVal EXCEPT ![self] = Heap[rh_p[self]].V]
/\ Assert(rVal'[self] = sVal[self],
"Failure of assertion at line line 143, column 11.")
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh_p' = [rh_p EXCEPT ![self] = Head(stack[self]).rh_p]
/\ lh_p' = [lh_p EXCEPT ![self] = Head(stack[self]).lh_p]
/\ rhL' = [rhL EXCEPT ![self] = Head(stack[self]).rhL]
/\ temp_p' = [temp_p EXCEPT ![self] = Head(stack[self]).temp_p]
/\ result_' = [result_ EXCEPT ![self] = Head(stack[self]).result_]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_,
nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL,
lh_pu, temp_pu, rh, lh, lhR, temp, result >>
popRight(self) == M2(self) \/ M4(self) \/ M5(self) \/ M6(self)
\/ M10(self) \/ M11(self) \/ M12(self) \/ M13(self)
\/ M8(self)
N2(self) == /\ pc[self] = "N2"
/\ IF freeList # {}
THEN /\ nd' = [nd EXCEPT ![self] = CHOOSE a \in freeList : TRUE]
/\ freeList' = freeList \ {nd'[self]}
ELSE /\ nd' = [nd EXCEPT ![self] = null]
/\ UNCHANGED freeList
/\ IF nd'[self] = null
THEN /\ rVal' = [rVal EXCEPT ![self] = "full"]
/\ pc' = [pc EXCEPT ![self] = "N1a"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N4"]
/\ UNCHANGED rVal
/\ UNCHANGED << LeftHat, RightHat, Heap, queue, sVal, stack, v_,
nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p,
result_, v, rh_pu, lhL, lh_pu, temp_pu, rh, lh,
lhR, temp, result >>
N1a(self) == /\ pc[self] = "N1a"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd]
/\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu]
/\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL]
/\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu]
/\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu]
/\ v' = [v EXCEPT ![self] = Head(stack[self]).v]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, rh, lh, lhR, temp, result >>
N4(self) == /\ pc[self] = "N4"
/\ Heap' = [Heap EXCEPT ![nd[self]].L = Dummy,
![nd[self]].V = v[self]]
/\ pc' = [pc EXCEPT ![self] = "N6"]
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
N6(self) == /\ pc[self] = "N6"
/\ lh_pu' = [lh_pu EXCEPT ![self] = LeftHat]
/\ pc' = [pc EXCEPT ![self] = "N8"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL,
temp_pu, rh, lh, lhR, temp, result >>
N8(self) == /\ pc[self] = "N8"
/\ lhL' = [lhL EXCEPT ![self] = Heap[lh_pu[self]].L]
/\ IF lhL'[self] = lh_pu[self]
THEN /\ pc' = [pc EXCEPT ![self] = "N10"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N15"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, rh_pu, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
N10(self) == /\ pc[self] = "N10"
/\ Heap' = [Heap EXCEPT ![nd[self]].R = Dummy]
/\ pc' = [pc EXCEPT ![self] = "N11"]
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
N11(self) == /\ pc[self] = "N11"
/\ rh_pu' = [rh_pu EXCEPT ![self] = RightHat]
/\ pc' = [pc EXCEPT ![self] = "N12"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
N12(self) == /\ pc[self] = "N12"
/\ IF (LeftHat = lh_pu[self]) /\
(RightHat = rh_pu[self])
THEN /\ /\ LeftHat' = nd[self]
/\ RightHat' = nd[self]
/\ temp_pu' = [temp_pu EXCEPT
![self] = TRUE]
ELSE /\ temp_pu' = [temp_pu EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, RightHat >>
/\ IF temp_pu'[self]
THEN /\ queue' = <<Heap[nd[self]].V>> \o queue
/\ rVal' = [rVal EXCEPT ![self] = "okay"]
/\ pc' = [pc EXCEPT ![self] = "N13"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N6"]
/\ UNCHANGED << rVal, queue >>
/\ UNCHANGED << Heap, freeList, sVal, stack, v_, nd_, rh_, rhR,
lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v,
nd, rh_pu, lhL, lh_pu, rh, lh, lhR, temp, result >>
N13(self) == /\ pc[self] = "N13"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd]
/\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu]
/\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL]
/\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu]
/\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu]
/\ v' = [v EXCEPT ![self] = Head(stack[self]).v]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, rh, lh, lhR, temp, result >>
N15(self) == /\ pc[self] = "N15"
/\ Heap' = [Heap EXCEPT ![nd[self]].R = lh_pu[self]]
/\ pc' = [pc EXCEPT ![self] = "N16"]
/\ UNCHANGED << LeftHat, RightHat, freeList, rVal, queue, sVal,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lh, lhR, temp, result >>
N16(self) == /\ pc[self] = "N16"
/\ IF (LeftHat = lh_pu[self]) /\
((Heap[lh_pu[self]].L) = lhL[self])
THEN /\ /\ Heap' = [Heap EXCEPT ![lh_pu[self]].L = nd[self]]
/\ LeftHat' = nd[self]
/\ temp_pu' = [temp_pu EXCEPT
![self] = TRUE]
ELSE /\ temp_pu' = [temp_pu EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, Heap >>
/\ IF temp_pu'[self]
THEN /\ queue' = <<Heap'[nd[self]].V>> \o queue
/\ rVal' = [rVal EXCEPT ![self] = "okay"]
/\ pc' = [pc EXCEPT ![self] = "N17"]
ELSE /\ pc' = [pc EXCEPT ![self] = "N6"]
/\ UNCHANGED << rVal, queue >>
/\ UNCHANGED << RightHat, freeList, sVal, stack, v_, nd_, rh_,
rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_,
v, nd, rh_pu, lhL, lh_pu, rh, lh, lhR, temp,
result >>
N17(self) == /\ pc[self] = "N17"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ nd' = [nd EXCEPT ![self] = Head(stack[self]).nd]
/\ rh_pu' = [rh_pu EXCEPT ![self] = Head(stack[self]).rh_pu]
/\ lhL' = [lhL EXCEPT ![self] = Head(stack[self]).lhL]
/\ lh_pu' = [lh_pu EXCEPT ![self] = Head(stack[self]).lh_pu]
/\ temp_pu' = [temp_pu EXCEPT ![self] = Head(stack[self]).temp_pu]
/\ v' = [v EXCEPT ![self] = Head(stack[self]).v]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, rh, lh, lhR, temp, result >>
pushLeft(self) == N2(self) \/ N1a(self) \/ N4(self) \/ N6(self)
\/ N8(self) \/ N10(self) \/ N11(self) \/ N12(self)
\/ N13(self) \/ N15(self) \/ N16(self) \/ N17(self)
O2(self) == /\ pc[self] = "O2"
/\ lh' = [lh EXCEPT ![self] = LeftHat]
/\ sVal' = [sVal EXCEPT ![self] = (queue = << >>)]
/\ pc' = [pc EXCEPT ![self] = "O4"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p, lh_p,
rhL, temp_p, result_, v, nd, rh_pu, lhL, lh_pu,
temp_pu, rh, lhR, temp, result >>
O4(self) == /\ pc[self] = "O4"
/\ rh' = [rh EXCEPT ![self] = RightHat]
/\ pc' = [pc EXCEPT ![self] = "O5"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL,
lh_pu, temp_pu, lh, lhR, temp, result >>
O5(self) == /\ pc[self] = "O5"
/\ IF Heap[lh[self]].L = lh[self]
THEN /\ Assert(sVal[self] \/ (queue = << >>),
"Failure of assertion at line line 190, column 9.")
/\ rVal' = [rVal EXCEPT ![self] = "empty"]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh]
/\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh]
/\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR]
/\ temp' = [temp EXCEPT
![self] = Head(stack[self]).temp]
/\ result' = [result EXCEPT
![self] = Head(stack[self]).result]
/\ stack' = [stack EXCEPT
![self] = Tail(stack[self])]
ELSE /\ pc' = [pc EXCEPT ![self] = "O6"]
/\ UNCHANGED << rVal, stack, rh, lh, lhR, temp, result >>
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_,
nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p,
result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >>
O6(self) == /\ pc[self] = "O6"
/\ IF lh[self] = rh[self]
THEN /\ IF (LeftHat = lh[self]) /\
(RightHat = rh[self])
THEN /\ /\ LeftHat' = Dummy
/\ RightHat' = Dummy
/\ temp' = [temp EXCEPT
![self] = TRUE]
ELSE /\ temp' = [temp EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, RightHat >>
/\ IF temp'[self]
THEN /\ sVal' = [sVal EXCEPT ![self] = Head(queue)]
/\ queue' = Tail(queue)
/\ pc' = [pc EXCEPT
![self] = "O8"]
ELSE /\ pc' = [pc EXCEPT
![self] = "O2"]
/\ UNCHANGED << queue, sVal >>
ELSE /\ pc' = [pc EXCEPT ![self] = "O10"]
/\ UNCHANGED << LeftHat, RightHat, queue, sVal, temp >>
/\ UNCHANGED << Heap, freeList, rVal, stack, v_, nd_, rh_, rhR,
lh_, temp_, rh_p, lh_p, rhL, temp_p, result_, v,
nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR,
result >>
O10(self) == /\ pc[self] = "O10"
/\ lhR' = [lhR EXCEPT ![self] = Heap[lh[self]].R]
/\ pc' = [pc EXCEPT ![self] = "O11"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL,
lh_pu, temp_pu, rh, lh, temp, result >>
O11(self) == /\ pc[self] = "O11"
/\ IF (LeftHat = lh[self]) /\
((Heap[lh[self]].R) = lhR[self])
THEN /\ /\ Heap' = [Heap EXCEPT ![lh[self]].R = lh[self]]
/\ LeftHat' = lhR[self]
/\ temp' = [temp EXCEPT
![self] = TRUE]
ELSE /\ temp' = [temp EXCEPT
![self] = FALSE]
/\ UNCHANGED << LeftHat, Heap >>
/\ IF temp'[self]
THEN /\ sVal' = [sVal EXCEPT ![self] = Head(queue)]
/\ queue' = Tail(queue)
/\ pc' = [pc EXCEPT ![self] = "O12"]
ELSE /\ pc' = [pc EXCEPT ![self] = "O2"]
/\ UNCHANGED << queue, sVal >>
/\ UNCHANGED << RightHat, freeList, rVal, stack, v_, nd_, rh_,
rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p, result_,
v, nd, rh_pu, lhL, lh_pu, temp_pu, rh, lh, lhR,
result >>
O12(self) == /\ pc[self] = "O12"
/\ result' = [result EXCEPT ![self] = Heap[lh[self]].V]
/\ Assert(result'[self] = sVal[self],
"Failure of assertion at line line 207, column 11.")
/\ pc' = [pc EXCEPT ![self] = "O13"]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal, stack, v_, nd_, rh_, rhR, lh_, temp_, rh_p,
lh_p, rhL, temp_p, result_, v, nd, rh_pu, lhL,
lh_pu, temp_pu, rh, lh, lhR, temp >>
O13(self) == /\ pc[self] = "O13"
/\ Heap' = [Heap EXCEPT ![lh[self]].L = Dummy,
![lh[self]].V = null]
/\ rVal' = [rVal EXCEPT ![self] = result[self]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh]
/\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh]
/\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR]
/\ temp' = [temp EXCEPT ![self] = Head(stack[self]).temp]
/\ result' = [result EXCEPT ![self] = Head(stack[self]).result]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, freeList, queue, sVal, v_, nd_,
rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p,
result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >>
O8(self) == /\ pc[self] = "O8"
/\ rVal' = [rVal EXCEPT ![self] = Heap[lh[self]].V]
/\ Assert(rVal'[self] = sVal[self],
"Failure of assertion at line line 198, column 9.")
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ rh' = [rh EXCEPT ![self] = Head(stack[self]).rh]
/\ lh' = [lh EXCEPT ![self] = Head(stack[self]).lh]
/\ lhR' = [lhR EXCEPT ![self] = Head(stack[self]).lhR]
/\ temp' = [temp EXCEPT ![self] = Head(stack[self]).temp]
/\ result' = [result EXCEPT ![self] = Head(stack[self]).result]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, queue, sVal, v_,
nd_, rh_, rhR, lh_, temp_, rh_p, lh_p, rhL, temp_p,
result_, v, nd, rh_pu, lhL, lh_pu, temp_pu >>
popLeft(self) == O2(self) \/ O4(self) \/ O5(self) \/ O6(self) \/ O10(self)
\/ O11(self) \/ O12(self) \/ O13(self) \/ O8(self)
T1(self) == /\ pc[self] = "T1"
/\ \/ /\ \E pushedVal \in Val:
\/ /\ /\ stack' = [stack EXCEPT
![self] = << [ procedure |-> "pushLeft",
pc |-> "T1",
nd |-> nd[self],
rh_pu |-> rh_pu[self],
lhL |-> lhL[self],
lh_pu |-> lh_pu[self],
temp_pu |-> temp_pu[self],
v |-> v[self] ] >>
\o stack[self]]
/\ v' = [v EXCEPT ![self] = pushedVal]
/\ nd' = [nd EXCEPT ![self] = {}]
/\ rh_pu' = [rh_pu EXCEPT
![self] = {}]
/\ lhL' = [lhL EXCEPT ![self] = {}]
/\ lh_pu' = [lh_pu EXCEPT
![self] = {}]
/\ temp_pu' = [temp_pu EXCEPT
![self] = {}]
/\ pc' = [pc EXCEPT ![self] = "N2"]
/\ UNCHANGED <<v_, nd_, rh_, rhR, lh_, temp_>>
\/ /\ /\ stack' = [stack EXCEPT
![self] = << [ procedure |-> "pushRight",
pc |-> "T1",
nd_ |-> nd_[self],
rh_ |-> rh_[self],
rhR |-> rhR[self],
lh_ |-> lh_[self],
temp_ |-> temp_[self],
v_ |-> v_[self] ] >>
\o stack[self]]
/\ v_' = [v_ EXCEPT ![self] = pushedVal]
/\ nd_' = [nd_ EXCEPT ![self] = {}]
/\ rh_' = [rh_ EXCEPT ![self] = {}]
/\ rhR' = [rhR EXCEPT ![self] = {}]
/\ lh_' = [lh_ EXCEPT ![self] = {}]
/\ temp_' = [temp_ EXCEPT
![self] = {}]
/\ pc' = [pc EXCEPT ![self] = "L2"]
/\ UNCHANGED <<v, nd, rh_pu, lhL, lh_pu, temp_pu>>
/\ UNCHANGED <<rh_p, lh_p, rhL, temp_p, result_, rh, lh, lhR, temp, result>>
\/ /\ \/ /\ stack' = [stack EXCEPT
![self] = << [ procedure |-> "popLeft",
pc |-> "T1",
rh |-> rh[self],
lh |-> lh[self],
lhR |-> lhR[self],
temp |-> temp[self],
result |-> result[self] ] >>
\o stack[self]]
/\ rh' = [rh EXCEPT ![self] = {}]
/\ lh' = [lh EXCEPT ![self] = {}]
/\ lhR' = [lhR EXCEPT
![self] = {}]
/\ temp' = [temp EXCEPT
![self] = {}]
/\ result' = [result EXCEPT
![self] = {}]
/\ pc' = [pc EXCEPT ![self] = "O2"]
/\ UNCHANGED <<rh_p, lh_p, rhL, temp_p, result_>>
\/ /\ stack' = [stack EXCEPT
![self] = << [ procedure |-> "popRight",
pc |-> "T1",
rh_p |-> rh_p[self],
lh_p |-> lh_p[self],
rhL |-> rhL[self],
temp_p |-> temp_p[self],
result_ |-> result_[self] ] >>
\o stack[self]]
/\ rh_p' = [rh_p EXCEPT
![self] = {}]
/\ lh_p' = [lh_p EXCEPT
![self] = {}]
/\ rhL' = [rhL EXCEPT
![self] = {}]
/\ temp_p' = [temp_p EXCEPT
![self] = {}]
/\ result_' = [result_ EXCEPT
![self] = {}]
/\ pc' = [pc EXCEPT ![self] = "M2"]
/\ UNCHANGED <<rh, lh, lhR, temp, result>>
/\ UNCHANGED <<v_, nd_, rh_, rhR, lh_, temp_, v, nd, rh_pu, lhL, lh_pu, temp_pu>>
/\ UNCHANGED << LeftHat, RightHat, Heap, freeList, rVal, queue,
sVal >>
test(self) == T1(self)
Next == (\E self \in ProcSet: \/ pushRight(self) \/ popRight(self)
\/ pushLeft(self) \/ popLeft(self))
\/ (\E self \in Procs: test(self))
\/ (* Disjunct to prevent deadlock on termination *)
(\A self \in ProcSet: pc[self] = "Done" /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
Symmetry == Permutations(Address \ {Dummy}) \cup Permutations(Procs)
(*************************************************************************)
(* I originally intended to use TLC's symmetry reduction but I forgot to *)
(* add the SYMMETRY statement to the configuration file. To make it *)
(* work with this version of the spec, it's necessary to initialize the *)
(* variables with values of the correct "type". (I initialized the *)
(* variables in the original version in order to slightly reduced the *)
(* state space.) *)
(*************************************************************************)
Liveness == \A p \in Procs : []<> (pc[p] = "T1")
(*************************************************************************)
(* This liveness property essentially asserts that every procedure call *)
(* returns. *)
(*************************************************************************)
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment