Rename NewRoundStep to UnstartedStep in the specs

informalsystems · Dec 18, 2023 · b294769 · b294769
1 parent 099f4d9
commit b294769
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git a/Code/itf/src/types.rs b/Code/itf/src/types.rs
@@ -70,8 +70,8 @@ pub struct Vote {
 pub enum Step {
     #[serde(rename = "NoStep")]
     None,
-    #[serde(rename = "NewRoundStep")]
-    NewRound,
+    #[serde(rename = "UnstartedStep")]
+    Unstarted,
     #[serde(rename = "ProposeStep")]
     Propose,
     #[serde(rename = "PrevoteStep")]
@@ -86,7 +86,7 @@ impl Step {
     pub fn to_round_step(&self) -> Option<RoundStep> {
         match self {
             Step::None => None,
-            Step::NewRound => Some(RoundStep::Unstarted),
+            Step::Unstarted => Some(RoundStep::Unstarted),
             Step::Propose => Some(RoundStep::Propose),
             Step::Prevote => Some(RoundStep::Prevote),
             Step::Precommit => Some(RoundStep::Precommit),

diff --git a/Code/itf/tests/consensus/runner.rs b/Code/itf/tests/consensus/runner.rs
@@ -279,7 +279,7 @@ impl ItfRunner for ConsensusRunner {
         } else {
             assert_eq!(Some(actual.step), expected.state.step.to_round_step());
 
-            if expected.state.step == Step::NewRound {
+            if expected.state.step == Step::Unstarted {
                 // In the spec, the new round comes from the input, it's not in the state.
                 assert_eq!(
                     actual.round.as_i64(),

diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt
@@ -125,8 +125,8 @@ module consensus {
         | NewRoundProposerCInput(round_value) =>
             val r = round_value._1
             val v = round_value._2
-            if (not(state.step.in(Set(NewRoundStep, NoStep))))
-                state.toErrorOutput("state is not NewRoundStep or initial step")
+            if (not(state.step.in(Set(UnstartedStep, NoStep))))
+                state.toErrorOutput("state is not Unstarted or initial step")
             else if (r <= state.round)
                 state.toErrorOutput("new round is not bigger than current round")
             else
@@ -139,8 +139,8 @@ module consensus {
         // line 11.20
         // TODO: discuss comment "ev.round must match state.round"
         | NewRoundCInput(r) =>
-            if (not(state.step.in(Set(NewRoundStep, NoStep))))
-                state.toErrorOutput("state is not NewRoundStep or initial step")
+            if (not(state.step.in(Set(UnstartedStep, NoStep))))
+                state.toErrorOutput("state is not Unstarted or initial step")
             else if (r <= state.round)
                 state.toErrorOutput("new round is not bigger than current round")
             else
@@ -255,7 +255,7 @@ module consensus {
         | RoundSkipCInput(r) => 
             if (r > state.round)
                 state
-                    .with("step", NewRoundStep)
+                    .with("step", UnstartedStep)
                     .toSkipRoundOutput(r)
             else state.toErrorOutput("RoundSkipCInput for round not bigger than current round")
 
@@ -288,8 +288,8 @@ module consensus {
                 // TODO: here we should call newRound. For this we would need to know whether
                 // we are proposer for next round.
                 state
-                    // CHECK: setting the step to NewRound was added to match the code behavior
-                    .with("step", NewRoundStep)
+                    // CHECK: setting the step to UnstartedStep was added to match the code behavior
+                    .with("step", UnstartedStep)
                     .toSkipRoundOutput(state.round + 1)
             else state.toErrorOutput("TimeoutPrecommitCInput")
 

diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt
@@ -101,7 +101,7 @@ module consensusTest {
         .then(_assert(output == TimeoutOutput((0, PrecommitTimeout))))
 
         .then(fireInput(TimeoutPrecommitCInput((2, 0))))
-        .then(_assert(output == SkipRoundOutput(1) and state.step == NewRoundStep))
+        .then(_assert(output == SkipRoundOutput(1) and state.step == UnstartedStep))
 
         .then(fireInput(NewRoundCInput(1)))
         .then(_assert(output == TimeoutOutput((1, ProposeTimeout))))

diff --git a/Specs/Quint/types.qnt b/Specs/Quint/types.qnt
@@ -33,7 +33,7 @@ module types {
     // Steps in a round
     type Step =
         | NoStep
-        | NewRoundStep
+        | UnstartedStep
         | ProposeStep
         | PrevoteStep
         | PrecommitStep