spec: Renaming and cleanup (#94)

* Remove ITF trace

* Rename executor to driver

* Rename output of votekeeper to `VoteKeeperOutput`

* Rename `Event` to `ConsensusInput`

* Rename `ProposeMsg_t` to `Proposal_t` and `VoteMsg_t` to `Vote_t`

* Cleanup

* Rename `PendingEvent` to `PendingInput`

* Fix last remaining instances of `result and `event`

* Fix ITF structs

* Cleanup in Rust code

Code/itf/src/votekeeper.rs

@@ -41,7 +41,7 @@ pub struct RoundVotes {
     pub round: Round,
     pub prevotes: VoteCount,
     pub precommits: VoteCount,
-    pub emitted_events: HashSet<ExecutorEvent>,
+    pub emitted_outputs: HashSet<VoteKeeperOutput>,
     #[serde(with = "As::<HashMap<Same, Integer>>")]
     pub votes_addresses_weights: HashMap<Address, Weight>,
 }
@@ -57,7 +57,7 @@ pub struct VoteCount {
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Hash)]
-pub struct ExecutorEvent {
+pub struct VoteKeeperOutput {
     #[serde(with = "As::<Integer>")]
     pub round: Round,
     pub name: String,
@@ -69,7 +69,7 @@ pub struct State {
     #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::bookkeeper")]
     pub bookkeeper: Bookkeeper,
     #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::lastEmitted")]
-    pub last_emitted: ExecutorEvent,
+    pub last_emitted: VoteKeeperOutput,
     #[serde(rename = "voteBookkeeperTest::voteBookkeeperSM::weightedVote")]
     #[serde(with = "As::<(Same, Integer, Integer)>")]
     pub weighted_vote: (Vote, Weight, Round),

Code/itf/tests/votekeeper/runner.rs

@@ -123,23 +123,23 @@ impl ItfRunner for VoteKeeperRunner {
 
             let actual_round = actual_state.per_round().get(&Round::new(round)).unwrap();
 
-            let expected_events = &expected_round.emitted_events;
-            let actual_events = actual_round.emitted_msgs();
+            let expected_outputs = &expected_round.emitted_outputs;
+            let actual_outputs = actual_round.emitted_outputs();
 
             assert_eq!(
-                actual_events.len(),
-                expected_events.len(),
+                actual_outputs.len(),
+                expected_outputs.len(),
                 "number of emitted events"
             );
 
             let mut event_count = HashMap::new();
 
-            for event in expected_events {
+            for event in expected_outputs {
                 let count = event_count.entry(event.name.clone()).or_insert(0);
                 *count += 1;
             }
 
-            for event in actual_events {
+            for event in actual_outputs {
                 let event_name = match event {
                     Output::PolkaValue(_) => "PolkaValue".into(),
                     Output::PrecommitValue(_) => "PrecommitValue".into(),

Code/vote/src/keeper.rs

@@ -25,7 +25,7 @@ where
 {
     votes: RoundVotes<Ctx::Address, ValueId<Ctx>>,
     addresses_weights: RoundWeights<Ctx::Address>,
-    emitted_msgs: BTreeSet<Output<ValueId<Ctx>>>,
+    emitted_outputs: BTreeSet<Output<ValueId<Ctx>>>,
 }
 
 impl<Ctx> PerRound<Ctx>
@@ -36,7 +36,7 @@ where
         Self {
             votes: RoundVotes::new(),
             addresses_weights: RoundWeights::new(),
-            emitted_msgs: BTreeSet::new(),
+            emitted_outputs: BTreeSet::new(),
         }
     }
 
@@ -48,8 +48,8 @@ where
         &self.addresses_weights
     }
 
-    pub fn emitted_msgs(&self) -> &BTreeSet<Output<ValueId<Ctx>>> {
-        &self.emitted_msgs
+    pub fn emitted_outputs(&self) -> &BTreeSet<Output<ValueId<Ctx>>> {
+        &self.emitted_outputs
     }
 }
 
@@ -62,7 +62,7 @@ where
         Self {
             votes: self.votes.clone(),
             addresses_weights: self.addresses_weights.clone(),
-            emitted_msgs: self.emitted_msgs.clone(),
+            emitted_outputs: self.emitted_outputs.clone(),
         }
     }
 }
@@ -76,7 +76,7 @@ where
         f.debug_struct("PerRound")
             .field("votes", &self.votes)
             .field("addresses_weights", &self.addresses_weights)
-            .field("emitted_msgs", &self.emitted_msgs)
+            .field("emitted_outputs", &self.emitted_outputs)
             .finish()
     }
 }
@@ -144,7 +144,7 @@ where
 
             if skip_round {
                 let msg = Output::SkipRound(vote.round());
-                round.emitted_msgs.insert(msg.clone());
+                round.emitted_outputs.insert(msg.clone());
                 return Some(msg);
             }
         }
@@ -160,8 +160,8 @@ where
         let msg = threshold_to_output(vote.vote_type(), vote.round(), threshold);
 
         match msg {
-            Some(msg) if !round.emitted_msgs.contains(&msg) => {
-                round.emitted_msgs.insert(msg.clone());
+            Some(msg) if !round.emitted_outputs.contains(&msg) => {
+                round.emitted_outputs.insert(msg.clone());
                 Some(msg)
             }
             _ => None,

Specs/Quint/Makefile

@@ -1,7 +1,7 @@
 parse:
 	npx @informalsystems/quint parse asyncModelsTest.qnt
 	npx @informalsystems/quint parse consensusTest.qnt
-	npx @informalsystems/quint parse executor.qnt
+	npx @informalsystems/quint parse driver.qnt
 	npx @informalsystems/quint parse statemachineTest.qnt
 	npx @informalsystems/quint parse voteBookkeeperTest.qnt
 .PHONY: parse