refactor TraceRunner trait

informalsystems · Nov 16, 2023 · 2fb5a95 · 2fb5a95
1 parent bcb5e41
commit 2fb5a95
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 14 deletions.
diff --git a/Code/itf/src/mbt.rs b/Code/itf/src/mbt.rs
@@ -1,30 +1,29 @@
 use std::fmt::Debug;
 
 pub trait TraceRunner {
-    type ActualState;
+    type Sut;
     type Result;
 
     type ExpectedState: Debug;
     type Error: Debug;
 
-    fn init(&mut self, expected: &Self::ExpectedState) -> Result<Self::ActualState, Self::Error>;
+    fn init(&mut self, expected: &Self::ExpectedState) -> Result<Self::Sut, Self::Error>;
 
     fn step(
         &mut self,
-        state: &mut Self::ActualState,
+        state: &mut Self::Sut,
         expected_state: &Self::ExpectedState,
     ) -> Result<Self::Result, Self::Error>;
 
     fn result_invariant(
         &self,
-        state: &Self::ActualState,
         result: &Self::Result,
         expected_state: &Self::ExpectedState,
     ) -> Result<bool, Self::Error>;
 
     fn state_invariant(
         &self,
-        actual_state: &Self::ActualState,
+        state: &Self::Sut,
         expected_state: &Self::ExpectedState,
     ) -> Result<bool, Self::Error>;
 
@@ -40,7 +39,7 @@ pub trait TraceRunner {
                 println!("🟢 step: {}", i);
                 let result = self.step(&mut sut_state, state)?;
                 assert!(
-                    self.result_invariant(&sut_state, &result, state)?,
+                    self.result_invariant(&result, state)?,
                     "🔴 result invariant failed at step {}",
                     i
                 );

diff --git a/Code/itf/tests/votekeeper.rs b/Code/itf/tests/votekeeper.rs
@@ -42,24 +42,21 @@ struct VoteKeeperRunner {
 }
 
 impl TraceRunner for VoteKeeperRunner {
-    type ActualState = VoteKeeper<TestContext>;
+    type Sut = VoteKeeper<TestContext>;
     type Result = Option<Message<<<TestContext as Context>::Value as Value>::Id>>;
 
     type ExpectedState = ItfState;
     type Error = ();
 
-    fn init(
-        &mut self,
-        expected_state: &Self::ExpectedState,
-    ) -> Result<Self::ActualState, Self::Error> {
+    fn init(&mut self, expected_state: &Self::ExpectedState) -> Result<Self::Sut, Self::Error> {
         // Obtain the initial total_weight from the first state in the model.
         let total_weight: Weight = from_itf(&expected_state.bookkeeper.total_weight).unwrap();
         Ok(VoteKeeper::new(total_weight))
     }
 
     fn step(
         &mut self,
-        state: &mut Self::ActualState,
+        state: &mut Self::Sut,
         expected_state: &Self::ExpectedState,
     ) -> Result<Self::Result, Self::Error> {
         // Build step to execute.
@@ -84,7 +81,6 @@ impl TraceRunner for VoteKeeperRunner {
 
     fn result_invariant(
         &self,
-        _state: &Self::ActualState,
         result: &Self::Result,
         expected_state: &Self::ExpectedState,
     ) -> Result<bool, Self::Error> {
@@ -127,7 +123,7 @@ impl TraceRunner for VoteKeeperRunner {
 
     fn state_invariant(
         &self,
-        _actual_state: &Self::ActualState,
+        _state: &Self::Sut,
         _expected_state: &Self::ExpectedState,
     ) -> Result<bool, Self::Error> {
         Ok(true)