updated syntax to Quint 0.14.4

informalsystems · Nov 8, 2023 · d02f187 · d02f187
1 parent 76218ca
commit d02f187
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt
@@ -106,7 +106,7 @@ type ConsResult = {
 
 type ConsensusEvent = str
 
-val consensusEvents = Set(
+val ConsensusEvents = Set(
     "NewHeight",			// Setups the state-machine for a single-height execution
     "NewRound",              		// Start a new round, not as proposer.
     "NewRoundProposer", 		// Start a new round as proposer with the proposed Value.

diff --git a/Specs/Quint/consensustest.qnt b/Specs/Quint/consensustest.qnt
@@ -45,7 +45,7 @@ action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value
 }
 
 action step = any {
-    nondet name = oneOf(consensusEvents)
+    nondet name = oneOf(ConsensusEvents)
     nondet height = 1//oneOf(1.to(4))
     nondet round = 0//oneOf(1.to(4))
     nondet value = oneOf(Set("block 1", "block 2", "block 3"))

diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt
@@ -38,11 +38,15 @@ val Steps = Set("Prevote", "Precommit")
 
 val AllFaultyVotes : Set[VoteMsg_t] = 
     tuples(Faulty, Heights, Rounds, Values, Steps)
-    .map((p, h, r, v, s) => { src: p, height: h, round: r, id: v, step: s })
+    .map(t => { src: t._1, height: t._2, round: t._3, id: t._4, step: t._5 })
+
+// val AllFaultyVotes : Set[VoteMsg_t] = 
+//     tuples(Faulty, Heights, Rounds, Values, Steps)
+//     .map((p, h, r, v, s) => { src: p, height: h, round: r, id: v, step: s })
 
 val AllFaultyProposals : Set[ProposeMsg_t] =
     tuples(Faulty, Heights, Rounds, Values, RoundsOrNil)
-    .map((p, h, r, v, vr) => { src: p, height: h, round: r, proposal: v, validRound: vr })
+    .map(t => { src: t._1, height: t._2, round: t._3, proposal: t._4, validRound: t._5 })
 
 
 // Global State
@@ -61,10 +65,10 @@ action unchangedAll = all {
     _hist' = _hist
 }
 
-val AgreementInv = tuples(Correct, Correct).forall((p,q) => 
-    (system.get(p).es.chain != List() and system.get(q).es.chain != List())
+val AgreementInv = tuples(Correct, Correct).forall(p => 
+    (system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List())
         implies
-            system.get(p).es.chain[0] == system.get(q).es.chain[0])
+            system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0])
 
 // Actions
 action init = all {