Fixing a few specs and the parse tests (#383)

* update two specs with the new syntax

* fix parse tests

* fix the error message

* address Shon's comments

* fix the error message

* remove json-diff

Author: konnov

examples/LamportMutex/LamportMutex.tnt

@@ -44,11 +44,11 @@ module LamportMutex {
   val Message = Set(AckMessage, RelMessage).union(Clock.map(c => ReqMessage(c)))
 
   action Init = all {
-      clock <- Proc.mapBy(p => 0),
-      req <- Proc.mapBy(p => Proc.mapBy(q => 0)),
-      ack <- Proc.mapBy(p => Set()),
-      network <- Proc.mapBy(p => Proc.mapBy(q => List())),
-      crit <- Set(),
+      clock' = Proc.mapBy(p => 0),
+      req' = Proc.mapBy(p => Proc.mapBy(q => 0)),
+      ack' = Proc.mapBy(p => Set()),
+      network' = Proc.mapBy(p => Proc.mapBy(q => List())),
+      crit' = Set(),
   }
 
   /* beats(p,q) is true if process p believes that its request has higher
@@ -73,11 +73,11 @@ module LamportMutex {
   // Process p requests access to critical section.
   action Request(p) = all {
     req.get(p).get(p) == 0,
-    req <- req.setBy(p, r => r.setBy(p, c => clock.get(p))),
-    network <- network.setBy(p, n => Broadcast(p, ReqMessage(clock.get(p)))),
-    ack <- ack.set(p,Set(p)),
-    clock <- clock,
-    crit <- crit,
+    req' = req.setBy(p, r => r.setBy(p, c => clock.get(p))),
+    network' = network.setBy(p, n => Broadcast(p, ReqMessage(clock.get(p)))),
+    ack' = ack.set(p,Set(p)),
+    clock' = clock,
+    crit' = crit,
   }
 
   // Process p receives a request from q and acknowledges it.
@@ -87,79 +87,81 @@ module LamportMutex {
     val c = m.clock
     all {
       m.mtype == "req",
-      req <- req.setBy(p, a => a.setBy(q, b => c)),
-      clock <- clock.setBy(p, a => if (c > a) c + 1 else a + 1),
-      network <- network.setBy(q, a => a.setBy(p, b => b.tail()))
+      req' = req.setBy(p, a => a.setBy(q, b => c)),
+      clock' = clock.setBy(p, a => if (c > a) c + 1 else a + 1),
+      network' = network.setBy(q, a => a.setBy(p, b => b.tail()))
                         .setBy(p, a => a.setBy(q, b => b.append(AckMessage))),
     },
-    ack <- ack,
-    crit <- crit,
+    ack' = ack,
+    crit' = crit,
   }
 
   // Process p receives an acknowledgement from q. 
   action ReceiveAck(p, q) = all {
     network.get(p).get(q) != List(),
     val m = network.get(p).get(q).head() all {
       m.mtype == "ack",
-      network <- network.setBy(p, a => a.setBy(q, b => b.tail())),
-      ack <- ack.setBy(p, a => a.union(Set(q))),
+      network' = network.setBy(p, a => a.setBy(q, b => b.tail())),
+      ack' = ack.setBy(p, a => a.union(Set(q))),
     },
-    clock <- clock,
-    req <- req,
-    crit <- crit,
+    clock' = clock,
+    req' = req,
+    crit' = crit,
   }
 
   // Process p enters the critical section.
   action Enter(p) = all {
     ack.get(p) == Proc,
     Proc.forall(q => beats(p, q)),
-    crit <- crit.union(Set(p)),
-    clock <- clock,
-    req <- req,
-    ack <- ack,
-    network <- network,
+    crit' = crit.union(Set(p)),
+    clock' = clock,
+    req' = req,
+    ack' = ack,
+    network' = network,
   }
 
   // Process p exits the critical section and notifies other processes.
   action Exit(p) = all {
     p.in(crit),
-    crit <- crit.exclude(Set(p)),
-    network <- network.set(p, Broadcast(p, RelMessage)),
-    req <- req.setBy(p, r => r.set(p, 0)),
-    ack <- ack.set(p, Set()),
-    clock <- clock,
+    crit' = crit.exclude(Set(p)),
+    network' = network.set(p, Broadcast(p, RelMessage)),
+    req' = req.setBy(p, r => r.set(p, 0)),
+    ack' = ack.set(p, Set()),
+    clock' = clock,
   }
 
   // Process p receives a release notification from q.
   action ReceiveRelease(p,q) = all {
     network.get(p).get(q) != List(),
     val m = network.get(p).get(q).head() all {
       m.mtype == "rel",
-      req <- req.setBy(p, r => r.set(q, 0)),
-      network <- network.setBy(p, a => a.setBy(q, b => b.tail())),
+      req' = req.setBy(p, r => r.set(q, 0)),
+      network' = network.setBy(p, a => a.setBy(q, b => b.tail())),
     },
-    clock <- clock,
-    ack <- ack,
-    crit <- crit,
+    clock' = clock,
+    ack' = ack,
+    crit' = crit,
   }
 
   // Next-state relation.
-  action Next = any {
-    Proc.guess(p => any {
+  action Next = {
+    nondet p = oneOf(Proc)
+    any {
       Request(p),
       Enter(p),
       Exit(p),
-    }),
-    Proc.guess(p => Proc.guess(q => any {
-      ReceiveRequest(p,q),
-      ReceiveAck(p,q),
-      ReceiveRelease(p,q),
-    })),
-  } 
+      nondet q = oneOf(Proc)
+      any {
+        ReceiveRequest(p,q),
+        ReceiveAck(p,q),
+        ReceiveRelease(p,q),
+      }
+    }
+  }  
 
   /* A state constraint that is useful for validating the specification
      using finite-state model checking. */
-  val ClockConstraint = Proc.forall(p => clock.get(p) <= maxClock)
+  val ClockConstraint = Proc.forall(p => (clock.get(p) <= maxClock))
 
   /* No channel ever contains more than three messages. In fact, no channel
      ever contains more than one message of the same type, as proved below.*/

examples/Paxos/Paxos.tnt

@@ -101,18 +101,18 @@ val TypeOK = and {
 }
 
 action Init = all {
-    maxBal  <- Acceptor.mapBy(_ => -1),
-    maxVBal <- Acceptor.mapBy(_ => -1),
-    maxVal  <- Acceptor.mapBy(_ => None),
-    msgs    <- Set(),
+    maxBal'  = Acceptor.mapBy(_ => -1),
+    maxVBal' = Acceptor.mapBy(_ => -1),
+    maxVal'  = Acceptor.mapBy(_ => None),
+    msgs'    = Set(),
 }
 
 /***************************************************************************)
 (* The actions.  We begin with the subaction (an action that will be used  *)
 (* to define the actions that make up the next-state action.               *)
 (***************************************************************************/
 action Send(m) = {
-  msgs <- msgs.union(Set(m))
+    msgs' = msgs.union(Set(m))
 }
 
 /***************************************************************************)
@@ -123,8 +123,8 @@ action Send(m) = {
 (***************************************************************************/
 action Phase1a(b) = all {
     Send({ tag: "1a", bal: b }),
-    maxVBal <- maxVBal,
-    maxVal <- maxVal,
+    maxVBal' = maxVBal,
+    maxVal'  = maxVal,
 }
 
 /***************************************************************************)
@@ -134,15 +134,15 @@ action Phase1a(b) = all {
 (* maxVBal[a] and maxVal[a].                                               *)
 (***************************************************************************/
 action Phase1b(a) = {
-    msgs.filter(m => m.tag == "1a")
-        .guess(m => all {
-          m.bal > maxBal.get(a),
-          maxBal <- maxBal.set(a, m.bal),
-          Send({ tag: "1b", acc: a, bal: m.bal, 
-                   mbal: maxVBal.get(a), mval: maxVal.get(a) }),
-          maxVBal <- maxVBal,
-          maxVal <- maxVal,
-    })
+    nondet m = msgs.filter(m2 => m2.tag == "1a").oneOf()
+    all {
+        m.bal > maxBal.get(a),
+        Send({ tag: "1b", acc: a, bal: m.bal, 
+                 mbal: maxVBal.get(a), mval: maxVal.get(a) }),
+        maxBal' = maxBal.set(a, m.bal),
+        maxVBal' = maxVBal,
+        maxVal'  = maxVal,
+    }
 }
 
 /***************************************************************************)
@@ -184,8 +184,8 @@ action Phase2a(b, v) = all {
     }
   ),
   Send({ tag: "2a", bal: b, value: v }),
-  maxVBal <- maxVBal,
-  maxVal <- maxVal,
+  maxVBal' = maxVBal,
+  maxVal'  = maxVal,
 }
 
 /***************************************************************************)
@@ -197,15 +197,16 @@ action Phase2a(b, v) = all {
 (* phase 2b message announcing its vote.  It also sets maxBal[a] to the    *)
 (* message's.  ballot number                                               *)
 (***************************************************************************/
-action Phase2b(a) = msgs.filter(m => m.tag == "2a")
-                        .guess(m => all {
-                              m.bal >= maxBal.get(a),
-                              maxBal  <- maxBal.set(a, m.bal),
-                              maxVBal <- maxVBal.set(a, m.bal),
-                              maxVal  <- maxVal.set(a, m.value),
-                              Send({ tag: "2b", acc: a,
-                                       bal: m.bal, value: m.value }),
-})
+action Phase2b(a) = {
+  nondet m = msgs.filter(m2 => m2.tag == "2a").oneOf()
+  all {
+    m.bal >= maxBal.get(a),
+    Send({ tag: "2b", acc: a, bal: m.bal, value: m.value }),
+    maxBal'  = maxBal.set(a, m.bal),
+    maxVBal' = maxVBal.set(a, m.bal),
+    maxVal'  = maxVal.set(a, m.value),
+  }
+}
 
 /***************************************************************************)
 (* In an implementation, there will be learner processes that learn from   *)
@@ -217,17 +218,20 @@ action Phase2b(a) = msgs.filter(m => m.tag == "2a")
 (* Below are defined the next-state action and the complete spec.          *)
 (***************************************************************************/
 action Next = any {
-    all {
-      Ballot.guess(b => any {
-                        Phase1a(b),
-                        Value.guess(v => Phase2a(b, v)),
-                   }),
-      maxBal <- maxBal,
+  all {
+    nondet b = oneOf(Ballot)
+    any {
+      Phase1a(b),
+      nondet v = oneOf(Value)
+      Phase2a(b, v)
     },
-    Acceptor.guess(a => any {
-      Phase1b(a),
-      Phase2b(a),
-    }),
+    maxBal' = maxBal,
+  },
+  nondet a = oneOf(Acceptor)
+  any {
+    Phase1b(a),
+    Phase2b(a),
+  }
 }
 
 temporal Spec = Init and always(stutter(Next, vars))

examples/Paxos/Voting.tnt

@@ -164,8 +164,8 @@ THEOREM ShowsSafety ==
 (* straightforward.                                                        *)
 (***************************************************************************/
 action Init = all {
-  votes  <- Acceptor.mapBy(_ => Set()),
-  maxBal <- Acceptor.mapBy(_ => -1),
+  votes'  = Acceptor.mapBy(_ => Set()),
+  maxBal' = Acceptor.mapBy(_ => -1),
 }
 
 
@@ -177,8 +177,8 @@ action Init = all {
 (***************************************************************************/
 action IncreaseMaxBal(a, b) = all {
   b > maxBal.get(a),
-  maxBal <- maxBal.set(a, b),
-  votes <- votes,
+  maxBal' = maxBal.set(a, b),
+  votes'  = votes,
 }
 
 /***************************************************************************)
@@ -196,20 +196,23 @@ action VoteFor(a, b, v) = all {
          votes.get(c).forall( vt => (vt._1 == b) implies (vt._2 == v) )
     ),
     Quorum.exists( Q => ShowsSafeAt(Q, b, v) ),
-    votes  <- votes.setBy(a, old => old.union(Set((b, v))) ),
-    maxBal <- maxBal.set(a, b),
+    votes'  = votes.setBy(a, old => old.union(Set((b, v))) ),
+    maxBal' = maxBal.set(a, b),
 }
 
 
 /***************************************************************************)
 (* The next-state action and the invariant.                                *)
 (***************************************************************************/
-action Next =
-    tuples(Acceptor, Ballot).guess((a, b) => any {
-            IncreaseMaxBal(a, b),
-            Value.guess(v => VoteFor(a, b, v)),
-        }
-    )
+action Next = {
+    nondet a = oneOf(Acceptor)
+    nondet b = oneOf(Ballot)
+    any {
+      IncreaseMaxBal(a, b),
+      nondet v = oneOf(Value)
+      VoteFor(a, b, v),
+    }
+}
 
 temporal Spec = Init and always(stutter(Next, (votes, maxBal)))