Update modelator to 0.2.0

modules/Cargo.toml

@@ -56,7 +56,7 @@ optional = true
 env_logger = "0.9.0"
 tracing-subscriber = "0.2.19"
 test-env-log = { version = "0.2.7", features = ["trace"] }
-modelator = { git = "https://github.com/informalsystems/modelator", rev = "99f656fa8b3cf46a2aa0b6513e4e140d1778c4bd" }
+modelator = "0.2.0"
 tendermint-rpc = { version = "=0.21.0", features = ["http-client", "websocket-client"] }
 tendermint-testgen = { version = "=0.21.0" } # Needed for generating (synthetic) light blocks.
 sha2 = { version = "0.9.3" }

modules/tests/mbt.rs

@@ -1,7 +1,7 @@
 mod runner;
 
-use modelator::{run, TestError};
-use runner::{step::Step, IbcTestRunner};
+use modelator::{ModelChecker, TestError, run_tla_steps};
+use runner::IbcTestRunner;
 
 #[test]
 fn mbt() {
@@ -12,12 +12,14 @@ fn mbt() {
     }
 }
 
-fn run_tests() -> Result<(), TestError<IbcTestRunner, Step>> {
+fn run_tests() -> Result<(), TestError> {
     // run the test
     let tla_tests_file = "tests/support/model_based/IBCTests.tla";
     let tla_config_file = "tests/support/model_based/IBCTests.cfg";
-    let runner = IbcTestRunner::new();
-    run(tla_tests_file, tla_config_file, runner)?;
+    let mut opts = modelator::Options::default();
+    opts.model_checker_options.model_checker = ModelChecker::Tlc;
+    let mut runner = IbcTestRunner::new();
+    run_tla_steps(tla_tests_file, tla_config_file, &opts, &mut runner)?;
 
     Ok(())
 }

modules/tests/runner/mod.rs

@@ -63,7 +63,7 @@ impl IbcTestRunner {
             max_history_size,
             Height::new(Self::revision(), initial_height),
         );
-        assert!(self.contexts.insert(chain_id, ctx).is_none());
+        self.contexts.insert(chain_id, ctx);
     }
 
     /// Returns a reference to the `MockContext` of a given `chain_id`.
@@ -436,8 +436,8 @@ impl IbcTestRunner {
     }
 }
 
-impl modelator::runner::TestRunner<Step> for IbcTestRunner {
-    fn initial_step(&mut self, step: Step) -> bool {
+impl modelator::step_runner::StepRunner<Step> for IbcTestRunner {
+    fn initial_step(&mut self, step: Step) -> Result<(), String> {
         assert_eq!(step.action, Action::None, "unexpected action type");
         assert_eq!(
             step.action_outcome,
@@ -448,11 +448,11 @@ impl modelator::runner::TestRunner<Step> for IbcTestRunner {
         for (chain_id, chain) in step.chains {
             self.init_chain_context(chain_id, chain.height);
         }
-        true
+        Ok(())
     }
 
-    fn next_step(&mut self, step: Step) -> bool {
-        let result = self.apply(step.action);
+    fn next_step(&mut self, step: Step) -> Result<(), String> {
+        let result = self.apply(step.clone().action);
         let outcome_matches = match step.action_outcome {
             ActionOutcome::None => panic!("unexpected action outcome"),
             ActionOutcome::Ics02CreateOk => result.is_ok(),
@@ -499,6 +499,10 @@ impl modelator::runner::TestRunner<Step> for IbcTestRunner {
             ActionOutcome::Ics03ConnectionOpenConfirmOk => result.is_ok(),
         };
         // also check the state of chains
-        outcome_matches && self.validate_chains() && self.check_chain_states(step.chains)
+        if outcome_matches && self.validate_chains() && self.check_chain_states(step.chains) {
+            Ok(())
+        } else {
+            Err("next_step did not conclude successfully".into())
+        }
     }
 }