This is the result of running TLC on the DCAS spec, annotated with
some explanation.  It was run with a configuration file specifying the
following instance.

   Val     <- {v1}
   Address <- {a1, a2, a3, a4}
   Dummy   <- a1
   Procs   <- {p1, p2} 

I added comments beginning with "----->" to indicate the actions that
represent a procedure call and return.  You should be able to
understand the trace knowing that

-    /\ nd = (p1 :> a2 @@ p2 :> null)

   indicates that value of nd is the function (array) with domain 
   (index set) {p1, p2} that maps p1 to a2 and p2 to null.  

- The variable pc is added by the translation, where pc[p] = "X"
  means that control in process p is at label X.  Look at how
  the value of pc changed to determine what part of which process's
  code executed a step.

- Because TLA+ does not have local variables, the translator must
  do renaming to eliminate duplicate local variable and procedure parameter
  names.  It did the following renamings for the this algorithm.

    Variable  nd      of procedure  pushRight  changed to  nd_
    Variable  rh      of procedure  pushRight  changed to  rh_
    Variable  lh      of procedure  pushRight  changed to  lh_
    Variable  temp    of procedure  pushRight  changed to  temp_
    Variable  rh      of procedure  popRight   changed to  rh_p
    Variable  lh      of procedure  popRight   changed to  lh_p
    Variable  temp    of procedure  popRight   changed to  temp_p
    Variable  result  of procedure  popRight   changed to  result_
    Variable  rh      of procedure  pushLeft   changed to  rh_pu
    Variable  lh      of procedure  pushLeft   changed to  lh_pu
    Variable  temp    of procedure  pushLeft   changed to  temp_pu
    Parameter v       of procedure  pushRight  changed to  v_


c:\users\lamport\papers\pluscal\dcas\tla>java -mx500m tlc.TLC -cleanup DCAS         
TLC Version 2.0 of January 16, 2006
Model-checking
Parsing file DCAS.tla
Parsing file C:\users\lamport\tla\tools\tla\tlasany\StandardModules\Naturals.tla
Parsing file C:\users\lamport\tla\tools\tla\tlasany\StandardModules\Sequences.tla
Parsing file C:\users\lamport\tla\tools\tla\tlasany\StandardModules\TLC.tla
Parsing file C:\users\lamport\tla\tools\tla\tlasany\StandardModules\FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module FiniteSets
Semantic processing of module DCAS
Finished computing initial states: 1 distinct state generated.
Error: Attempted to apply the operator overridden by the java method
public static tlc.value.Value tlc.module.TLC.Assert(tlc.value.Value,tlc.value.Value),
but it produced the following error:
The first argument of Assert evaluated to FALSE; the second argument was:
"Failure of assertion at line line 199, column 9."


The behavior up to this point is:
STATE 1: <Initial predicate>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "T1" @@ p2 :> "T1")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {a2, a3}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> null, V |-> null] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> <<  >> @@ p2 :> <<  >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)


-----> p1 calls pushLeft

STATE 2: <Action line 876, col 13 to line 961, col 99 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N2" @@ p2 :> "T1")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {a2, a3}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> null, V |-> null] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> <<  >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 3: <Action line 589, col 13 to line 603, col 82 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N4" @@ p2 :> "T1")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {a3}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> null, V |-> null] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> <<  >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 4: <Action line 618, col 13 to line 625, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "T1")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {a3}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> <<  >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)


-----> p2 calls pushRight


STATE 5: <Action line 876, col 13 to line 961, col 99 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L2")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {a3}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 6: <Action line 301, col 13 to line 315, col 84 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L4")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> null, L |-> null, V |-> null] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 7: <Action line 331, col 13 to line 338, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L6")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> null, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 8: <Action line 340, col 13 to line 346, col 78 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L8")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> null, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 9: <Action line 348, col 13 to line 354, col 78 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L9")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> null, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 10: <Action line 356, col 13 to line 366, col 79 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a1
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a1
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L12")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> a1)
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = <<  >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 11: <Action line 368, col 14 to line 387, col 76 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N6" @@ p2 :> "L13")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> TRUE)
/\ lh_ = (p1 :> {} @@ p2 :> a1)
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 12: <Action line 627, col 13 to line 633, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N8" @@ p2 :> "L13")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> TRUE)
/\ lh_ = (p1 :> {} @@ p2 :> a1)
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 13: <Action line 635, col 13 to line 643, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N15" @@ p2 :> "L13")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> TRUE)
/\ lh_ = (p1 :> {} @@ p2 :> a1)
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> null, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 14: <Action line 694, col 14 to line 700, col 78 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N16" @@ p2 :> "L13")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> a3)
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> TRUE)
/\ lh_ = (p1 :> {} @@ p2 :> a1)
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> a1)
/\ rh_ = (p1 :> {} @@ p2 :> a1)
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> v1)
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", v_ |-> {}, nd_ |-> {}, rh_ |-> {}, rhR |-> {}, lh_ |-> {}, temp_ |-> {}, procedure |-> "pushRight"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)


-----> p2 returns "okay"

STATE 15: <Action line 389, col 14 to line 401, col 76 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N16" @@ p2 :> "T1")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> <<  >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)


-----> p2 calls popLeft


STATE 16: <Action line 876, col 13 to line 961, col 99 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> {})
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N16" @@ p2 :> "O2")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> TRUE)

STATE 17: <Action line 740, col 13 to line 747, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a3
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N16" @@ p2 :> "O4")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a1, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> FALSE)

STATE 18: <Action line 702, col 14 to line 721, col 79 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> a2 @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> v1 @@ p2 :> {})
/\ pc = (p1 :> "N17" @@ p2 :> "O4")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> a1 @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> a3 @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> TRUE @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", v |-> {}, nd |-> {}, rh_pu |-> {}, lhL |-> {}, lh_pu |-> {}, temp_pu |-> {}, procedure |-> "pushLeft"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> FALSE)


-----> p1 returns "okay"


STATE 19: <Action line 723, col 14 to line 734, col 79 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "T1" @@ p2 :> "O4")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> {})
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = ( p1 :> <<  >> @@
  p2 :>
      << [ pc |-> "T1",
           rh |-> {},
           lh |-> {},
           lhR |-> {},
           temp |-> {},
           result |-> {},
           procedure |-> "popLeft" ] >> )
/\ sVal = (p1 :> TRUE @@ p2 :> FALSE)

STATE 20: <Action line 749, col 13 to line 755, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "T1" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = ( p1 :> <<  >> @@
  p2 :>
      << [ pc |-> "T1",
           rh |-> {},
           lh |-> {},
           lhR |-> {},
           temp |-> {},
           result |-> {},
           procedure |-> "popLeft" ] >> )
/\ sVal = (p1 :> TRUE @@ p2 :> FALSE)


-----> p1 calls popRight

STATE 21: <Action line 876, col 13 to line 961, col 99 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> {} @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M2" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> TRUE @@ p2 :> FALSE)

STATE 22: <Action line 450, col 13 to line 457, col 79 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M4" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> {} @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> FALSE @@ p2 :> FALSE)

STATE 23: <Action line 459, col 13 to line 465, col 77 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M5" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> a2 @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> FALSE @@ p2 :> FALSE)

STATE 24: <Action line 467, col 13 to line 489, col 85 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M6" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> a2 @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> FALSE @@ p2 :> FALSE)

STATE 25: <Action line 491, col 13 to line 514, col 80 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M10" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> a2 @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> {} @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> FALSE @@ p2 :> FALSE)

STATE 26: <Action line 516, col 14 to line 522, col 78 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a3
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M11" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> a2 @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> a2 @@ p2 :> {})
/\ queue = << v1, v1 >>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a2, V |-> v1] )
/\ temp_p = (p1 :> {} @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> FALSE @@ p2 :> FALSE)

STATE 27: <Action line 524, col 14 to line 543, col 80 of module DCAS>
/\ lh = (p1 :> {} @@ p2 :> a3)
/\ LeftHat = a2
/\ nd = (p1 :> {} @@ p2 :> {})
/\ RightHat = a2
/\ rVal = (p1 :> "okay" @@ p2 :> "okay")
/\ rh_p = (p1 :> a3 @@ p2 :> {})
/\ result_ = (p1 :> {} @@ p2 :> {})
/\ v = (p1 :> {} @@ p2 :> {})
/\ pc = (p1 :> "M12" @@ p2 :> "O5")
/\ rh_pu = (p1 :> {} @@ p2 :> {})
/\ nd_ = (p1 :> {} @@ p2 :> {})
/\ temp = (p1 :> {} @@ p2 :> {})
/\ rh = (p1 :> {} @@ p2 :> a3)
/\ lh_p = (p1 :> a2 @@ p2 :> {})
/\ lhL = (p1 :> {} @@ p2 :> {})
/\ lhR = (p1 :> {} @@ p2 :> {})
/\ temp_ = (p1 :> {} @@ p2 :> {})
/\ lh_ = (p1 :> {} @@ p2 :> {})
/\ lh_pu = (p1 :> {} @@ p2 :> {})
/\ rhL = (p1 :> a2 @@ p2 :> {})
/\ queue = <<v1>>
/\ rhR = (p1 :> {} @@ p2 :> {})
/\ rh_ = (p1 :> {} @@ p2 :> {})
/\ result = (p1 :> {} @@ p2 :> {})
/\ v_ = (p1 :> {} @@ p2 :> {})
/\ temp_pu = (p1 :> {} @@ p2 :> {})
/\ freeList = {}
/\ Heap = ( a1 :> [R |-> a1, L |-> a1, V |-> null] @@
  a2 :> [R |-> a3, L |-> a1, V |-> v1] @@
  a3 :> [R |-> a1, L |-> a3, V |-> v1] )
/\ temp_p = (p1 :> TRUE @@ p2 :> {})
/\ stack = (p1 :> << [pc |-> "T1", rh_p |-> {}, lh_p |-> {}, rhL |-> {}, temp_p |-> {}, result_ |-> {}, procedure |-> "popRight"] >> @@ p2 :> << [pc |-> "T1", rh |-> {}, lh |-> {}, lhR |-> {}, temp |-> {}, result |-> {}, procedure |-> "popLeft"] >>)
/\ sVal = (p1 :> v1 @@ p2 :> FALSE)


-----> p2 can now return the value "empty".

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 757, column 16 to line 757, column 30 in DCAS
1. Line 758, column 16 to line 773, column 84 in DCAS
2. Line 759, column 27 to line 760, column 84 in DCAS


65810 states generated, 33439 distinct states found, 5240 states left on queue.
The depth of the complete state graph search is 28.