diff --git a/.changelog/unreleased/improvements/1249-update-modelator.md b/.changelog/unreleased/improvements/1249-update-modelator.md new file mode 100644 index 0000000000..7912ece5fd --- /dev/null +++ b/.changelog/unreleased/improvements/1249-update-modelator.md @@ -0,0 +1,3 @@ +- Update Modelator to 0.2.0 ([#1249]) + +[#1249]: https://github.com/informalsystems/ibc-rs/pull/1249 diff --git a/Cargo.lock b/Cargo.lock index add8c920d0..899da78200 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1728,16 +1728,21 @@ dependencies = [ [[package]] name = "modelator" -version = "0.1.0" -source = "git+https://github.com/informalsystems/modelator?rev=99f656fa8b3cf46a2aa0b6513e4e140d1778c4bd#99f656fa8b3cf46a2aa0b6513e4e140d1778c4bd" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ab4fd1c35db4a1c20a729d779b04d7d3f02a0091cec676d0f95755427a91a2e" dependencies = [ "clap", + "hex", "nom", "serde", "serde_json", + "sha2", + "tempfile", "thiserror", "tracing", "tracing-subscriber 0.2.19", + "ureq", ] [[package]] @@ -3610,6 +3615,22 @@ version = "0.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a156c684c91ea7d62626509bce3cb4e1d9ed5c4d978f7b4352658f96a4c26b4a" +[[package]] +name = "ureq" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2475a6781e9bc546e7b64f4013d2f4032c8c6a40fcffd7c6f4ee734a890972ab" +dependencies = [ + "base64", + "chunked_transfer", + "log", + "once_cell", + "rustls", + "url", + "webpki", + "webpki-roots", +] + [[package]] name = "url" version = "2.2.2" diff --git a/modules/Cargo.toml b/modules/Cargo.toml index 2e534eee97..39e986709d 100644 --- a/modules/Cargo.toml +++ b/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" } diff --git a/modules/tests/mbt.rs b/modules/tests/mbt.rs index 97903618f7..4165aa02f5 100644 --- a/modules/tests/mbt.rs +++ b/modules/tests/mbt.rs @@ -1,7 +1,7 @@ mod runner; -use modelator::{run, TestError}; -use runner::{step::Step, IbcTestRunner}; +use modelator::{run_tla_steps, ModelChecker, TestError}; +use runner::IbcTestRunner; #[test] fn mbt() { @@ -12,12 +12,14 @@ fn mbt() { } } -fn run_tests() -> Result<(), TestError> { +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(()) } diff --git a/modules/tests/runner/mod.rs b/modules/tests/runner/mod.rs index 0571b8807f..798abd8459 100644 --- a/modules/tests/runner/mod.rs +++ b/modules/tests/runner/mod.rs @@ -52,7 +52,6 @@ impl IbcTestRunner { } /// Create a `MockContext` for a given `chain_id`. - /// Panic if a context for `chain_id` already exists. pub fn init_chain_context(&mut self, chain_id: String, initial_height: u64) { let chain_id = Self::chain_id(chain_id); // never GC blocks @@ -63,7 +62,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 +435,8 @@ impl IbcTestRunner { } } -impl modelator::runner::TestRunner for IbcTestRunner { - fn initial_step(&mut self, step: Step) -> bool { +impl modelator::step_runner::StepRunner 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,10 +447,10 @@ impl modelator::runner::TestRunner 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 { + fn next_step(&mut self, step: Step) -> Result<(), String> { let result = self.apply(step.action); let outcome_matches = match step.action_outcome { ActionOutcome::None => panic!("unexpected action outcome"), @@ -499,6 +498,10 @@ impl modelator::runner::TestRunner 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()) + } } }