From 46fb36cdeff9cd9d7efb2151ae86b5677144df68 Mon Sep 17 00:00:00 2001 From: Daniel T <30197399+danwt@users.noreply.github.com> Date: Sat, 30 Oct 2021 16:43:31 +0100 Subject: [PATCH] Daniel/integration tests improvements (#111) * Use java 16 zulu in Apalache cmd * Adds a TLDR comment explaining integration test practice * renames tests/integration/tla to tests/integration/resource * Deletes body of tests/integration/main.rs * Impl basics of framework json file config * Adds integration test (parse) * Fixes docstr comment for TestListCli struct * Improves 2 comments in tla::mod.rs * Adds numbers step runner test file * Adds Numbers test config * Partially impl integration test main.rs * Removes test_batch_list.json * Impl integration test framework MVP * Adds self.recalculate to init of NumberSystem::init * Refactor the integration tests * Adds 2 small comments to integration/main.rs * Changes the CLI to require a --write arg to write to disk * Fixes a typo in tla_file_suite.rs * Adds IBC_ics02 parse test * Adds expect_status field to CLI test * Fixes file format for written parse * Adds shlex crate dev dependency (shell parsing) * Adds CliParseError to error.rs * Adds deserialize trait to CliStatus * Adds cli integration test support (status only) * Adds name, description fields to integration tests * Implements basic integration testing * Adds model checker runtime configuration to integration tests * Give error in case test not found (with integration test) Fixes #108 * Adds test for test name matching correctness * Adds TrafficCrossing parse tests * Defines an IntegrationTestError * Uses IntegrationTestError * Adds multi trace integration tests for Indices * Removes cli parse error from modelator/Error * Impl automatic conversions for IntegrationTestError * Ammend naming of next, init in Indices test * Adds 2PossibleTrace integration test * Ignore deadlock message in Apalache log * Integration tests pass * Adds 2 extra tests for Numbers test * Adds additional TrafficCrossing cli test * Removes Apalache 16zulu java cmd * Adds Apalache M1 mac java usage * Impl parallel testing Note: does not yet lock .modelator directory * Better doc parallel integration tests * Reorganize code in tests/integration/common * Removes commented out cache code * Protect jar download in setup with mutex * Delete apalache m1 mac cmd * use thiserror attributes * removed some boxes * make clippy happy * sort dep list * bump clap-beta version for successful compilation * fix cargo doc warning * Fix array len clamp in cmd_output * use start_with instead of taking a slice and checking equiality * maintain checker exit code * less multi-threading to fix integration tests * remove multithreading from integration tests Co-authored-by: Daniel Tisdall Co-authored-by: Ranadeep Biswas --- modelator/Cargo.toml | 11 +- modelator/examples/auto_complete.rs | 28 +- modelator/src/artifact/tla_file_suite.rs | 2 +- modelator/src/cli/mod.rs | 82 +++- modelator/src/cli/output.rs | 8 +- modelator/src/jar.rs | 4 +- modelator/src/lib.rs | 32 +- modelator/src/main.rs | 2 +- .../src/model/checker/apalache/cmd_output.rs | 31 +- modelator/src/model/checker/apalache/mod.rs | 24 +- modelator/src/model/checker/mod.rs | 11 +- modelator/src/model/checker/tlc/mod.rs | 15 +- modelator/src/model/language/tla/mod.rs | 16 +- modelator/src/step_runner.rs | 7 +- modelator/src/test_util.rs | 4 +- modelator/tests/integration/common.rs | 104 +++++ modelator/tests/integration/error.rs | 42 ++ modelator/tests/integration/main.rs | 440 +++++------------- .../integration/resource/2PossibleTraces.cfg | 2 + .../integration/resource/2PossibleTraces.json | 33 ++ .../integration/resource/2PossibleTraces.tla | 30 ++ .../resource/2PossibleTracesTests.tla | 9 + .../tests/integration/resource/IBC_ics02.json | 15 + .../{tla => resource}/IBC_ics02.tla | 0 .../integration/{tla => resource}/Indices.cfg | 0 .../tests/integration/resource/Indices.json | 42 ++ .../integration/{tla => resource}/Indices.tla | 0 .../{tla => resource}/IndicesBalances.tla | 0 .../{tla => resource}/IndicesBalancesExec.tla | 0 .../IndicesBalancesHistoryTests.tla | 4 +- .../IndicesBalancesTests.tla | 4 +- .../{tla => resource}/IndicesExec.tla | 0 .../{tla => resource}/IndicesHistoryTests.tla | 4 +- .../{tla => resource}/IndicesTests.cfg | 4 +- .../{tla => resource}/IndicesTests.tla | 4 +- .../integration/{tla => resource}/Numbers.cfg | 0 .../tests/integration/resource/Numbers.json | 111 +++++ .../integration/{tla => resource}/Numbers.tla | 0 .../{tla => resource}/NumbersAMaxBMaxTest.tla | 0 .../{tla => resource}/NumbersAMaxBMinTest.tla | 0 .../{tla => resource}/NumbersAMinBMaxTest.tla | 0 .../integration/resource/TrafficCrossing.json | 51 ++ .../{tla => resource}/TrafficCrossing.tla | 0 .../TrafficCrossingHistoryTest.cfg | 0 .../TrafficCrossingHistoryTest.tla | 0 .../{tla => resource}/TrafficCrossingTest.cfg | 0 .../{tla => resource}/TrafficCrossingTest.tla | 0 modelator/tests/integration/resource/mod.rs | 1 + .../tests/integration/resource/numbers.rs | 74 +++ .../tests/integration/resource/smoke.json | 5 + 50 files changed, 799 insertions(+), 457 deletions(-) create mode 100644 modelator/tests/integration/common.rs create mode 100644 modelator/tests/integration/error.rs create mode 100644 modelator/tests/integration/resource/2PossibleTraces.cfg create mode 100644 modelator/tests/integration/resource/2PossibleTraces.json create mode 100644 modelator/tests/integration/resource/2PossibleTraces.tla create mode 100644 modelator/tests/integration/resource/2PossibleTracesTests.tla create mode 100644 modelator/tests/integration/resource/IBC_ics02.json rename modelator/tests/integration/{tla => resource}/IBC_ics02.tla (100%) rename modelator/tests/integration/{tla => resource}/Indices.cfg (100%) create mode 100644 modelator/tests/integration/resource/Indices.json rename modelator/tests/integration/{tla => resource}/Indices.tla (100%) rename modelator/tests/integration/{tla => resource}/IndicesBalances.tla (100%) rename modelator/tests/integration/{tla => resource}/IndicesBalancesExec.tla (100%) rename modelator/tests/integration/{tla => resource}/IndicesBalancesHistoryTests.tla (98%) rename modelator/tests/integration/{tla => resource}/IndicesBalancesTests.tla (97%) rename modelator/tests/integration/{tla => resource}/IndicesExec.tla (100%) rename modelator/tests/integration/{tla => resource}/IndicesHistoryTests.tla (98%) rename modelator/tests/integration/{tla => resource}/IndicesTests.cfg (59%) rename modelator/tests/integration/{tla => resource}/IndicesTests.tla (97%) rename modelator/tests/integration/{tla => resource}/Numbers.cfg (100%) create mode 100644 modelator/tests/integration/resource/Numbers.json rename modelator/tests/integration/{tla => resource}/Numbers.tla (100%) rename modelator/tests/integration/{tla => resource}/NumbersAMaxBMaxTest.tla (100%) rename modelator/tests/integration/{tla => resource}/NumbersAMaxBMinTest.tla (100%) rename modelator/tests/integration/{tla => resource}/NumbersAMinBMaxTest.tla (100%) create mode 100644 modelator/tests/integration/resource/TrafficCrossing.json rename modelator/tests/integration/{tla => resource}/TrafficCrossing.tla (100%) rename modelator/tests/integration/{tla => resource}/TrafficCrossingHistoryTest.cfg (100%) rename modelator/tests/integration/{tla => resource}/TrafficCrossingHistoryTest.tla (100%) rename modelator/tests/integration/{tla => resource}/TrafficCrossingTest.cfg (100%) rename modelator/tests/integration/{tla => resource}/TrafficCrossingTest.tla (100%) create mode 100644 modelator/tests/integration/resource/mod.rs create mode 100644 modelator/tests/integration/resource/numbers.rs create mode 100644 modelator/tests/integration/resource/smoke.json diff --git a/modelator/Cargo.toml b/modelator/Cargo.toml index f9b8b2fa..a2ea3fff 100644 --- a/modelator/Cargo.toml +++ b/modelator/Cargo.toml @@ -15,23 +15,24 @@ authors = [ ] [dependencies] -clap = "=3.0.0-beta.4" +clap = "=3.0.0-beta.5" hex = "0.4.3" +lazy_static = "1.4.0" nom = "7.0.0" +once_cell = "1.8.0" rayon = "1.5.1" +regex = "1.5" serde = { version = "1.0.130", features = ["derive"] } serde_json = "1.0.67" sha2 = "0.9.8" tempfile = "3.2.0" thiserror = "1.0.29" tracing = "0.1.26" -regex = "1.5" -lazy_static = "1.4.0" tracing-subscriber = "0.2.20" ureq = "2.2.0" [dev-dependencies] -clap_generate = "=3.0.0-beta.4" -once_cell = "1.8.0" +clap_generate = "=3.0.0-beta.5" quickcheck = "1.0.3" quickcheck_macros = "1.0.0" +shlex = "1.1.0" diff --git a/modelator/examples/auto_complete.rs b/modelator/examples/auto_complete.rs index 62d962a3..fdc99325 100644 --- a/modelator/examples/auto_complete.rs +++ b/modelator/examples/auto_complete.rs @@ -1,15 +1,15 @@ -use clap::{App, ArgEnum}; -use clap::{Clap, IntoApp}; +use clap::ArgEnum; +use clap::{IntoApp, Parser}; +use clap_generate::generate; use clap_generate::generators::{Bash, Elvish, Fish, PowerShell, Zsh}; -use clap_generate::{generate, Generator}; -#[derive(Debug, Clap)] +#[derive(Debug, Parser)] struct Cli { #[clap(arg_enum)] generator: ShellName, } -#[derive(Debug, ArgEnum)] +#[derive(Debug, Clone, ArgEnum)] enum ShellName { Bash, Elvish, @@ -18,20 +18,18 @@ enum ShellName { Zsh, } -fn print_completions(app: &mut App) { - generate::(app, app.get_name().to_string(), &mut std::io::stdout()); -} - fn main() { let cli = Cli::parse(); - let mut modelator_app = modelator::cli::App::into_app(); + let mut app = modelator::cli::App::into_app(); + let app_name = app.get_name().to_owned(); eprintln!("Generating completion file for {:?}...", cli.generator); + match cli.generator { - ShellName::Bash => print_completions::(&mut modelator_app), - ShellName::Elvish => print_completions::(&mut modelator_app), - ShellName::Fish => print_completions::(&mut modelator_app), - ShellName::Powershell => print_completions::(&mut modelator_app), - ShellName::Zsh => print_completions::(&mut modelator_app), + ShellName::Bash => generate(Bash, &mut app, app_name, &mut std::io::stdout()), + ShellName::Elvish => generate(Elvish, &mut app, app_name, &mut std::io::stdout()), + ShellName::Fish => generate(Fish, &mut app, app_name, &mut std::io::stdout()), + ShellName::Powershell => generate(PowerShell, &mut app, app_name, &mut std::io::stdout()), + ShellName::Zsh => generate(Zsh, &mut app, app_name, &mut std::io::stdout()), } } diff --git a/modelator/src/artifact/tla_file_suite.rs b/modelator/src/artifact/tla_file_suite.rs index 7effb529..e5a8005b 100644 --- a/modelator/src/artifact/tla_file_suite.rs +++ b/modelator/src/artifact/tla_file_suite.rs @@ -39,7 +39,7 @@ fn find_dependencies(tla_module_path: impl AsRef) -> Result = crate::model::language::Tla::extract_test_names( tla_file_suite.tla_file.file_contents_backing(), )? .into_iter() - .filter(|test_name| allow_test_name(test_name, &self.test)); + .filter(|test_name| allow_test_name(test_name, &self.test)) + .collect(); + + if test_names.is_empty() { + return Err(Error::NoTestFound(format!( + "No test found in {}. [tla module name: {}, test pattern: {}]", + tla_file_suite.tla_file.module_name(), + tla_file_suite.tla_file.module_name(), + &self.test + ))); + }; let res = { let mut res: BTreeMap, Error>> = BTreeMap::new(); @@ -141,10 +162,22 @@ impl TraceCli { "Tla::tla_trace_to_json_trace output {}", json_trace ); - write_json_trace_to_file(&file_name_to_write, &json_trace) + if self.write { + write_json_trace_to_file(&file_name_to_write, &json_trace) + } else { + Ok(json!({ + "json_trace_content": json_trace.as_string() + })) + } } OutputFormat::Tla => { - write_tla_trace_to_file(&file_name_to_write, &trace) + if self.write { + write_tla_trace_to_file(&file_name_to_write, &trace) + } else { + Ok(json!({ + "tla_trace_content": trace.as_string() + })) + } } } }) @@ -159,7 +192,7 @@ impl TraceCli { } } -#[derive(Clap, Debug)] +#[derive(Parser, Debug)] enum Module { /// Parse TLA+ files. Parse(ParseCli), @@ -183,15 +216,15 @@ impl Module { } /// A struct that generates a CLI for `modelator` using [`clap`]. -#[derive(Clap, Debug)] +#[derive(Parser, Debug)] #[clap( name = crate_name!(), author, about, version, - setting = AppSettings::ColoredHelp, setting = AppSettings::InferSubcommands )] +#[clap(color = ColorChoice::Auto)] pub struct App { #[clap(subcommand)] module: Module, @@ -203,7 +236,7 @@ impl App { } } -#[derive(Debug, ArgEnum)] +#[derive(Debug, Clone, ArgEnum)] enum OutputFormat { Tla, Json, @@ -233,10 +266,11 @@ fn json_list_generated_tests(test_files: Vec<(PathBuf, PathBuf)>) -> Result Result { // Apalache changes the module name in the output file so we use it directly here. - let path = Path::new(tla_file.module_name()); + let file_name = format!("{}.tla", tla_file.module_name()); + let path = Path::new(&file_name); tla_file.try_write_to_file(path)?; Ok(json!({ - "tla_file": crate::util::absolute_path(path), + "tla_filepath": crate::util::absolute_path(path), })) } @@ -245,7 +279,7 @@ fn write_tla_trace_to_file(test_name: &str, tla_trace: &TlaTrace) -> Result Result>(modelator_dir: P) -> Result<(), Error> { +pub(crate) fn download_jars_if_necessary>(modelator_dir: P) -> Result<(), Error> { // get all existing jars let existing_jars = existing_jars(&modelator_dir)?; // compute jars that are missing @@ -103,7 +103,7 @@ pub(crate) fn download_jars>(modelator_dir: P) -> Result<(), Erro std::fs::create_dir(&modelator_dir)?; // try to download jars again - return download_jars(modelator_dir); + return download_jars_if_necessary(modelator_dir); } } Ok(()) diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs index c8549f0f..bd146a6d 100644 --- a/modelator/src/lib.rs +++ b/modelator/src/lib.rs @@ -70,6 +70,11 @@ use std::path::{Path, PathBuf}; use rayon::iter::{IntoParallelIterator, ParallelIterator}; use tempfile::tempdir; +use once_cell::sync::Lazy; +use std::sync::Mutex; + +static FILE_SYSTEM_MUTEX: Lazy> = Lazy::new(Mutex::default); + /// Wraps the data from running test(s), allowing more convenient access to the results. pub struct TestReport { test_name_to_trace_execution_result: BTreeMap>>, @@ -77,7 +82,7 @@ pub struct TestReport { impl TestReport { /// Returns true iff no test failed - pub fn is_ok(&self) -> bool { + pub fn no_test_failed(&self) -> bool { !self .test_name_to_trace_execution_result .values() @@ -151,13 +156,21 @@ impl ModelatorRuntime { ); } - // create modelator dir (if it doens't already exist) + self.ensure_dependencies_exist_on_filesystem()?; + + Ok(()) + } + + fn ensure_dependencies_exist_on_filesystem(&self) -> Result<(), Error> { + let _guard = FILE_SYSTEM_MUTEX.lock(); + + // create modelator dir if it doesn't already exist if !self.dir.as_path().is_dir() { std::fs::create_dir_all(&self.dir)?; } // download missing jars - jar::download_jars(&self.dir)?; + jar::download_jars_if_necessary(&self.dir)?; tracing::trace!("modelator setup completed"); Ok(()) @@ -173,8 +186,8 @@ impl ModelatorRuntime { /// # Examples /// /// ``` - /// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file_path = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file_path = "tests/integration/resource/Numbers.cfg"; /// let runtime = modelator::ModelatorRuntime::default(); /// let trace_results = runtime.traces(tla_tests_file_path, tla_config_file_path).unwrap(); /// println!("{:?}", trace_results); @@ -265,6 +278,7 @@ impl ModelatorRuntime { /// fn initial_step(&mut self, step: NumbersStep) -> Result<(), String> { /// self.a = step.a; /// self.b = step.b; + /// self.recalculate(); /// Ok(()) /// } /// @@ -292,8 +306,8 @@ impl ModelatorRuntime { /// /// // To run your system against a TLA+ test, just point to the corresponding TLA+ files. /// fn test() { - /// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file_path = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file_path = "tests/integration/resource/Numbers.cfg"; /// let runtime = modelator::ModelatorRuntime::default(); /// let mut system = NumberSystem::default(); /// assert!(runtime.run_tla_steps(tla_tests_file_path, tla_config_file_path, &mut system).is_ok()); @@ -401,8 +415,8 @@ impl ModelatorRuntime { /// /// // To run your system against a TLA+ test, just point to the corresponding TLA+ files. /// fn main() { - /// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMaxTest.tla"; - /// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file_path = "tests/integration/resource/NumbersAMaxBMaxTest.tla"; + /// let tla_config_file_path = "tests/integration/resource/Numbers.cfg"; /// let runtime = modelator::ModelatorRuntime::default(); /// /// // We create a system under test diff --git a/modelator/src/main.rs b/modelator/src/main.rs index 0d1df8c2..88165070 100644 --- a/modelator/src/main.rs +++ b/modelator/src/main.rs @@ -1,4 +1,4 @@ -use clap::Clap; +use clap::Parser; pub fn main() { let cli_app = modelator::cli::App::parse(); diff --git a/modelator/src/model/checker/apalache/cmd_output.rs b/modelator/src/model/checker/apalache/cmd_output.rs index d4cdf641..ee0fe9bd 100644 --- a/modelator/src/model/checker/apalache/cmd_output.rs +++ b/modelator/src/model/checker/apalache/cmd_output.rs @@ -3,10 +3,11 @@ use crate::Error; use serde::Serialize; use std::fmt; #[allow(clippy::upper_case_acronyms)] -#[derive(Debug, Serialize, PartialEq)] +#[derive(Debug, Clone, Serialize, PartialEq)] pub(crate) struct CmdOutput { pub(crate) stdout: String, pub(crate) stderr: String, + pub(crate) status: Option, } impl fmt::Display for CmdOutput { @@ -37,6 +38,11 @@ fn parse_filename(line: &str) -> String { } } +fn is_deadlock_line(line: &str) -> bool { + // This log message appears in a spurious case https://github.com/informalsystems/apalache/issues/1040 + line.starts_with("Found a deadlock. No SMT model.") +} + fn is_error_line(line: &str) -> bool { //Searching for strings of this form //Len is 14 @@ -45,7 +51,8 @@ fn is_error_line(line: &str) -> bool { return false; } let substr = &line[(line.len() - 14)..(line.len() - 12)]; - substr == "E@" + // Exclude the deadlock error. + substr == "E@" && !is_deadlock_line(line) } impl CmdOutput { @@ -60,7 +67,7 @@ impl CmdOutput { /// Try to get a list of counterexample filenames from stdout. If other Apalache errors are found then /// return a Result pub(crate) fn parse_counterexample_filenames(&self) -> Result, Error> { - let unparsed_lines: Vec = match self.non_counterexample_error() { + let raw_lines_that_must_be_parsed: Vec = match self.non_counterexample_error() { Some(err) => Err(Error::ApalacheFailure(err)), None => Ok(self .apalache_stdout_error_lines() @@ -68,7 +75,7 @@ impl CmdOutput { .filter(|line| is_counterexample_line(line)) .collect()), }?; - Ok(unparsed_lines + Ok(raw_lines_that_must_be_parsed .iter() .map(|line| parse_filename(line)) .collect()) @@ -78,10 +85,7 @@ impl CmdOutput { match (self.stdout.is_empty(), self.stderr.is_empty()) { (true, true) => Some(ApalacheError { summary: "stdout and stderr both empty".to_owned(), - output: CmdOutput { - stdout: self.stdout.clone(), - stderr: self.stderr.clone(), - }, + output: self.clone(), }), (false, true) => { let non_counterexample_error_lines: Vec = self @@ -95,19 +99,13 @@ impl CmdOutput { false => Some(ApalacheError { summary: "Non counterexample errors found in stdout:\n".to_owned() + &non_counterexample_error_lines.join("\n"), - output: CmdOutput { - stdout: self.stdout.clone(), - stderr: self.stderr.clone(), - }, + output: self.clone(), }), } } _ => Some(ApalacheError { summary: "stderr not empty".to_owned(), - output: CmdOutput { - stdout: self.stdout.clone(), - stderr: self.stderr.clone(), - }, + output: self.clone(), }), } } @@ -160,6 +158,7 @@ EXITCODE: ERROR (12) let output = CmdOutput { stdout: to_parse.to_owned(), stderr: "".to_owned(), + status: Some(12), }; let res = output.parse_counterexample_filenames().unwrap(); let expect = vec!["counterexample1.tla", "counterexample2.tla"]; diff --git a/modelator/src/model/checker/apalache/mod.rs b/modelator/src/model/checker/apalache/mod.rs index 120bfc79..d1dff1b7 100644 --- a/modelator/src/model/checker/apalache/mod.rs +++ b/modelator/src/model/checker/apalache/mod.rs @@ -33,8 +33,8 @@ impl Apalache { /// use modelator::ModelatorRuntime; /// use std::convert::TryFrom; /// - /// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file = "tests/integration/resource/Numbers.cfg"; /// let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap(); /// /// let mut tests = Tla::generate_tests(&tla_suite).unwrap(); @@ -56,14 +56,6 @@ impl Apalache { runtime ); - // TODO: disabling cache for now; see https://github.com/informalsystems/modelator/issues/46 - // load cache and check if the result is cached - // let mut cache = TlaTraceCache::new(runtime)?; - // let cache_key = TlaTraceCache::key(&tla_file, &tla_config_file)?; - // if let Some(value) = cache.get(&cache_key)? { - // return Ok(value); - // } - let tdir = tempfile::tempdir()?; try_write_to_dir(&tdir, input_artifacts)?; @@ -122,9 +114,6 @@ impl Apalache { .filter_map(Result::ok) .collect(); - // TODO: disabling cache for now; see https://github.com/informalsystems/modelator/issues/46 - // cache trace and then return it - //cache.insert(cache_key, &trace)?; Ok(( traces, ModelCheckerStdout::from_string(&apalache_output.stdout)?, @@ -143,7 +132,7 @@ impl Apalache { /// use modelator::ModelatorRuntime; /// use std::convert::TryFrom; /// - /// let tla_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; + /// let tla_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; /// let tla_file_suite = TlaFileSuite::from_tla_path(tla_file).unwrap(); /// /// let runtime = ModelatorRuntime::default(); @@ -195,10 +184,15 @@ fn run_apalache(mut cmd: Command) -> Result { // get apalache stdout and stderr let stdout = crate::util::cmd_output_to_string(&output.stdout); let stderr = crate::util::cmd_output_to_string(&output.stderr); + let status = output.status.code(); tracing::debug!("Apalache stdout:\n{}", stdout); tracing::debug!("Apalache stderr:\n{}", stderr); - Ok(CmdOutput { stdout, stderr }) + Ok(CmdOutput { + stdout, + stderr, + status, + }) } fn check_cmd>( diff --git a/modelator/src/model/checker/mod.rs b/modelator/src/model/checker/mod.rs index 4dc42085..ff8784d4 100644 --- a/modelator/src/model/checker/mod.rs +++ b/modelator/src/model/checker/mod.rs @@ -12,6 +12,8 @@ use std::env; use std::path::{Path, PathBuf}; use std::str::FromStr; +use serde::Deserialize; + const DEFAULT_TRACES_PER_TEST: usize = 1; /// Set of options to select the model checker to be used and configure them. @@ -50,6 +52,12 @@ impl ModelCheckerRuntime { self.log = log.as_ref().to_path_buf(); self } + + /// Set the maximum number of traces to try to generate for a single test. + pub fn traces_per_test(mut self, n: usize) -> Self { + self.traces_per_test = n; + self + } } impl Default for ModelCheckerRuntime { @@ -64,7 +72,8 @@ impl Default for ModelCheckerRuntime { } /// Configuration option to select the model checker to be used. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Deserialize)] +#[serde(rename_all = "snake_case")] pub enum ModelChecker { /// Option representing the [TLC](https://github.com/tlaplus/tlaplus) model /// checker. diff --git a/modelator/src/model/checker/tlc/mod.rs b/modelator/src/model/checker/tlc/mod.rs index 137ff013..4b9936f4 100644 --- a/modelator/src/model/checker/tlc/mod.rs +++ b/modelator/src/model/checker/tlc/mod.rs @@ -25,8 +25,8 @@ impl Tlc { /// use modelator::ModelatorRuntime; /// use std::convert::TryFrom; /// - /// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file = "tests/integration/resource/Numbers.cfg"; /// let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap(); /// /// let mut tests = Tla::generate_tests(&tla_suite).unwrap(); @@ -43,14 +43,6 @@ impl Tlc { let tla_config_file = &tla_file_suite.tla_config_file; tracing::debug!("Tlc::test {} {} {:?}", tla_file, tla_config_file, runtime); - // TODO: disabling cache for now; see https://github.com/informalsystems/modelator/issues/46 - // load cache and check if the result is cached - // let mut cache = TlaTraceCache::new(runtime)?; - // let cache_key = TlaTraceCache::key(&tla_file, &tla_config_file)?; - // if let Some(value) = cache.get(&cache_key)? { - // return Ok(value); - // } - let tdir = tempfile::tempdir()?; try_write_to_dir(&tdir, tla_file_suite)?; @@ -91,9 +83,6 @@ impl Tlc { )); } - // TODO: disabling cache for now; see https://github.com/informalsystems/modelator/issues/46 - // cache trace and then return it - //cache.insert(cache_key, &trace)?; Ok((traces, tlc_log)) } _ => { diff --git a/modelator/src/model/language/tla/mod.rs b/modelator/src/model/language/tla/mod.rs index 920b41b6..fa705078 100644 --- a/modelator/src/model/language/tla/mod.rs +++ b/modelator/src/model/language/tla/mod.rs @@ -30,8 +30,8 @@ impl Tla { /// use modelator::ModelatorRuntime; /// use std::convert::TryFrom; /// - /// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file = "tests/integration/resource/Numbers.cfg"; /// let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap(); /// /// let mut tests = Tla::generate_tests(&tla_suite).unwrap(); @@ -59,8 +59,8 @@ impl Tla { /// use modelator::model::language::Tla; /// use std::convert::TryFrom; /// - /// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - /// let tla_config_file = "tests/integration/tla/Numbers.cfg"; + /// let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + /// let tla_config_file = "tests/integration/resource/Numbers.cfg"; /// let tla_suite = TlaFileSuite::from_tla_and_config_paths(tla_tests_file, tla_config_file).unwrap(); /// let mut tests = Tla::generate_tests(&tla_suite).unwrap(); /// println!("{:?}", tests); @@ -106,9 +106,6 @@ impl Tla { Ok(names .iter() .filter_map(|name| { - // consider this as a test name if: - // - it starts/ends Test - // - it's not commented out let is_test = name.starts_with("Test") || name.ends_with("Test"); let is_commented_out = name.starts_with("\\*") || name.starts_with("(*"); if is_test && !is_commented_out { @@ -234,6 +231,7 @@ EXTENDS {} negated_test_name, test_name, match view_operator { + // Write an additional operator that corresponds the view to the specific negated test operator Some(name) => format!("ViewForTestNeg == {}", name), _ => "".to_owned(), } @@ -282,7 +280,7 @@ My4Op let res = extract_operator_names(content); match res { Ok(v) => assert_eq!(expect, v), - Err(_) => assert!(false), + Err(_) => panic!(), }; } @@ -344,7 +342,7 @@ My4Test let res = Tla::extract_test_names(content); match res { Ok(v) => assert_eq!(expect, v), - Err(_) => assert!(false), + Err(_) => panic!(), }; } } diff --git a/modelator/src/step_runner.rs b/modelator/src/step_runner.rs index e7b9521a..ae02e3c8 100644 --- a/modelator/src/step_runner.rs +++ b/modelator/src/step_runner.rs @@ -70,6 +70,7 @@ mod tests { fn initial_step(&mut self, step: NumbersStep) -> Result<(), String> { self.a = step.a; self.b = step.b; + self.recalculate(); Ok(()) } @@ -96,12 +97,12 @@ mod tests { #[test] fn test_step_runner() { - let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; - let tla_config_file = "tests/integration/tla/Numbers.cfg"; + let tla_tests_file = "tests/integration/resource/NumbersAMaxBMinTest.tla"; + let tla_config_file = "tests/integration/resource/Numbers.cfg"; let runtime = crate::ModelatorRuntime::default(); let mut runner = NumberSystem::default(); assert!(runtime .run_tla_steps(tla_tests_file, tla_config_file, &mut runner) - .map_or_else(|_| false, |v| v.is_ok()),); + .map_or_else(|_| false, |v| v.no_test_failed()),); } } diff --git a/modelator/src/test_util.rs b/modelator/src/test_util.rs index b2fbddce..c4eac3d9 100644 --- a/modelator/src/test_util.rs +++ b/modelator/src/test_util.rs @@ -1,10 +1,12 @@ +use serde::Deserialize; + const MAX_NUMBER: u64 = 6; /// Example system under test (SUT). /// Allows to modify the two variables, a and b, /// if they do not exceed the `MAX_NUMBER`. /// Maintains also the sum and product of the variables. #[allow(missing_docs)] -#[derive(Debug, Clone, Copy, PartialEq)] +#[derive(Debug, Clone, Copy, PartialEq, Deserialize)] pub struct NumberSystem { pub a: u64, pub b: u64, diff --git a/modelator/tests/integration/common.rs b/modelator/tests/integration/common.rs new file mode 100644 index 00000000..194b82c9 --- /dev/null +++ b/modelator/tests/integration/common.rs @@ -0,0 +1,104 @@ +use crate::error::IntegrationTestError; +use modelator::model::checker::ModelCheckerWorkers; +use modelator::model::checker::{ModelChecker, ModelCheckerRuntime}; +use modelator::ModelatorRuntime; +use serde::Deserialize; +use serde_json::Value as JsonValue; +use shlex; +use std::fmt::Debug; +use std::fs; +use std::path::PathBuf; + +pub fn resource_path(suffix: &str) -> PathBuf { + static ROOT_DIR: &str = "tests/integration"; + PathBuf::new().join(ROOT_DIR).join("resource").join(suffix) +} + +/// Take the cli cmd string and split it to mimic the result of std::env::args_os() +pub fn mimic_os_args(cmd: &str) -> Vec { + // Delegate to a crate because parsing command line strings is non trivial + shlex::split(cmd).unwrap() +} + +/// Arguments to be passed to a step runner testing function +pub struct StepRunnerArgs { + pub modelator_runtime: ModelatorRuntime, + pub test_function_name: String, + pub tla_tests_filepath: PathBuf, + pub tla_config_filepath: PathBuf, + pub expect: JsonValue, +} + +#[derive(Debug, Deserialize, Clone)] +pub struct ModelCheckerRuntimeConfig { + model_checker: ModelChecker, + workers: String, + traces_per_test: String, +} + +impl ModelCheckerRuntimeConfig { + pub fn to_model_checker_runtime(&self) -> ModelCheckerRuntime { + use std::str::FromStr; + ModelCheckerRuntime::default() + .workers(ModelCheckerWorkers::from_str(&self.workers).unwrap()) + .model_checker(self.model_checker) + .traces_per_test(self.traces_per_test.parse::().unwrap()) + } +} + +#[derive(Debug, Deserialize, Clone)] +#[serde(tag = "type")] +#[serde(rename_all = "snake_case")] +pub enum TestContent { + Cli { + cmd: String, + expect_status: String, + }, + StepRunner { + test_function: String, + tla_tests_filename: String, + tla_config_filename: String, + model_checker_runtime: ModelCheckerRuntimeConfig, + expect: JsonValue, + }, +} + +#[derive(Debug, Deserialize, Clone)] +#[serde(rename_all = "snake_case")] +pub struct Test { + pub name: String, + pub description: String, + pub content: TestContent, +} + +pub type StepRunnerTestFn = fn(StepRunnerArgs) -> Result<(), IntegrationTestError>; + +#[derive(Debug)] +pub struct TestBatch { + pub config: TestBatchConfig, + pub step_runner: Option>, +} + +pub struct TestBatchResourceBundle { + /// filename of .json config in /resource + pub config_filename: &'static str, + /// look up a step runner test function by name + pub step_runner: Option>, +} + +#[derive(Debug, Deserialize, Clone)] +pub struct TestBatchConfig { + pub name: String, + pub description: String, + pub tests: Vec, +} + +impl TestBatchConfig { + pub fn load(filename: &str) -> Result { + let path = resource_path(filename); + let content = fs::read_to_string(path) + .unwrap_or_else(|_| panic!("Unable to read contents of a {} file", filename)); + let ret: TestBatchConfig = serde_json::from_str(&content)?; + Ok(ret) + } +} diff --git a/modelator/tests/integration/error.rs b/modelator/tests/integration/error.rs new file mode 100644 index 00000000..73e7ee0a --- /dev/null +++ b/modelator/tests/integration/error.rs @@ -0,0 +1,42 @@ +use crate::common::{Test, TestBatchConfig}; +use thiserror::Error; + +/// Set of possible errors that can occur when running an integration test +#[derive(Error, Debug)] +pub enum IntegrationTestError { + /// An error in the integration test is itself incorrectly specified + #[error("The integration test is itself incorrectly specified: {0}")] + FaultyTest(String), + + /// An error in the case the expected value is wrong + #[error("Unexpected value from running test: expect {0}, actual {1}")] + ExpectedValueMismatch(String, String), + + /// An error in the case that modelator returns an error + #[error("Modelator returned an error: {0}")] + Modelator(#[from] modelator::Error), + + /// An error in the case that clap returns an error + #[error("Clap returned an error: {0}")] + Clap(#[from] clap::Error), + + /// An error in the case that serde returns an error + #[error("Serde returned an error: {0}")] + Serde(#[from] serde_json::Error), +} + +#[derive(Error, Debug)] +#[error( + "Test '{0}' in batch '{1}' failed. [name:{2}, batch_name:{3}, description:{4}] Error: {5}", + test.name, + batch_config.name, + test.name, + batch_config.name, + batch_config.description, + error_str +)] +pub struct IntegrationTestFailure { + pub error_str: String, + pub test: Test, + pub batch_config: TestBatchConfig, +} diff --git a/modelator/tests/integration/main.rs b/modelator/tests/integration/main.rs index 62b25387..bfb61e2a 100644 --- a/modelator/tests/integration/main.rs +++ b/modelator/tests/integration/main.rs @@ -1,344 +1,130 @@ -// We follow the approach proposed in the following link for integration tests: -// https://matklad.github.io/2021/02/27/delete-cargo-integration-tests.html - -use modelator::artifact::JsonTrace; -use modelator::cli::{App, CliStatus}; -use modelator::test_util::NumberSystem; -use modelator::{ - model::checker::{ModelChecker, ModelCheckerRuntime}, - Error, ModelatorRuntime, -}; -use modelator::{ActionHandler, EventRunner, EventStream, StateHandler}; -use once_cell::sync::Lazy; -use serde::Deserialize; -use serde_json::Value as JsonValue; -use std::path::{Path, PathBuf}; -use std::sync::Mutex; - -#[derive(Default, Debug, PartialEq)] -struct Numbers { - a: i64, - b: i64, -} - -#[derive(Debug, Clone, Deserialize, PartialEq)] -struct A { - a: u64, -} -#[derive(Debug, Clone, Deserialize, PartialEq)] -struct B { - b: u64, -} - -#[derive(Debug, Clone, Deserialize)] -enum Action { - None, - IncreaseA, - IncreaseB, -} - -impl StateHandler for NumberSystem { - fn init(&mut self, state: A) { - self.a = state.a - } - fn read(&self) -> A { - A { a: self.a } - } -} -impl StateHandler for NumberSystem { - fn init(&mut self, state: B) { - self.b = state.b - } - fn read(&self) -> B { - B { b: self.b } - } -} - -impl ActionHandler for NumberSystem { - type Outcome = String; - - fn handle(&mut self, action: Action) -> Self::Outcome { - let result_to_outcome = |res| match res { - Ok(()) => "OK".to_string(), - Err(s) => s, - }; - match action { - Action::None => result_to_outcome(Ok(())), - Action::IncreaseA => result_to_outcome(self.increase_a(1)), - Action::IncreaseB => result_to_outcome(self.increase_b(2)), - } - } +pub mod common; +pub mod error; +mod resource; + +use clap::Parser; +use common::*; +use error::{IntegrationTestError, IntegrationTestFailure}; +use modelator::ModelatorRuntime; +use resource::numbers; + +/// Register integration tests here by specifying a config file path and +/// (optionally) a handler for step runner tests. +fn test_batch_resources() -> Vec { + vec![ + TestBatchResourceBundle { + config_filename: "smoke.json", + step_runner: None, + }, + TestBatchResourceBundle { + config_filename: "IBC_ics02.json", + step_runner: None, + }, + TestBatchResourceBundle { + config_filename: "Indices.json", + step_runner: None, + }, + TestBatchResourceBundle { + config_filename: "2PossibleTraces.json", + step_runner: None, + }, + TestBatchResourceBundle { + config_filename: "Numbers.json", + step_runner: Some(Box::new(numbers::test)), + }, + TestBatchResourceBundle { + config_filename: "TrafficCrossing.json", + step_runner: None, + }, + ] } #[test] -fn event_runner() { - let events = EventStream::new() - .init(A { a: 0 }) - .init(B { b: 0 }) - .action(Action::IncreaseA) - .action(Action::IncreaseB) - .check(|state: A| assert!(state.a == 1)) - .check(|state: B| assert!(state.b == 2)); - - let mut system = NumberSystem::default(); - let mut runner = EventRunner::new() - .with_state::() - .with_state::() - .with_action::(); - let result = runner.run(&mut system, &mut events.into_iter()); - println!("{:?}", result); - assert!(result.is_ok()); -} - -// TODO: This test succeeds when run separately, -// and fails interchangeably with TLC test when run via `cargo test` -// Seems to be related to https://github.com/informalsystems/modelator/issues/43 -// -// #[test] -// fn json_event_runner() { -// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; -// let tla_config_file = "tests/integration/tla/Numbers.cfg"; -// let options = modelator::Options::default(); - -// let mut runner = Runner::::new() -// .with_state::() -// .with_state::() -// .with_action::(); - -// assert!(run(tla_tests_file, tla_config_file, &options, &mut runner).is_ok()); -// } - -const TLA_DIR: &str = "tests/integration/tla"; +/// This is the single, master, integration test +fn integration_test() { + // We follow the approach proposed in the following link for integration tests: + // https://matklad.github.io/2021/02/27/delete-cargo-integration-tests.html + // TLDR: use exactly 1 integration test in tests/integration/ -// we use this lock to make sure that the tlc & apalache tests are not run in -// parallel -static LOCK: Lazy> = Lazy::new(Mutex::default); + // Use to match a single test / + let pattern = ""; -#[test] -fn tlc() { - let _guard = LOCK.lock(); - if let Err(e) = all_tests(ModelChecker::Tlc) { - panic!("{}", e); - } -} + let do_run_test = |batch_name, test_name| { + pattern.is_empty() || format!("{}/{}", batch_name, test_name) == pattern + }; -#[test] -fn apalache() { - let _guard = LOCK.lock(); - if let Err(e) = all_tests(ModelChecker::Apalache) { - panic!("{}", e); + match load_test_batches() { + // Run each batch in parallel + // For each batch, run each test in the batch in parallel + // Use rayon::try_for_each to bubble up Result::Err value(s) + // In the case of multiple failed tests, only 1 will non-deterministically win the race to bubble up + Ok(batches) => match batches.iter().try_for_each(|batch| { + batch.config.tests.iter().try_for_each(|test: &Test| { + match do_run_test(&batch.config.name, &test.name) { + true => run_single_test(batch, &test.content).map_err(|err| { + IntegrationTestFailure { + error_str: err.to_string(), + batch_config: batch.config.clone(), + test: test.clone(), + } + }), + false => Ok(()), + } + }) + }) { + Ok(()) => (), + Err(err) => panic!("{}", err), + }, + Err(err) => panic!("{}", err), } } -fn all_tests(model_checker: ModelChecker) -> Result<(), Error> { - // create modelator options - let model_checker_runtime = ModelCheckerRuntime::default().model_checker(model_checker); - let options = ModelatorRuntime::default().model_checker_runtime(model_checker_runtime); - - // create all tests - let tests = vec![ - numbers_a_max_b_min_test(), - numbers_a_min_b_max_test(), - numbers_a_max_b_max_test(), - ]; - - for (tla_tests_file, tla_config_file, expected) in tests { - for (tla_tests_file, tla_config_file) in - absolute_and_relative_paths(tla_tests_file, tla_config_file) - { - let mut system = NumberSystem::default(); - let mut runner = EventRunner::new() - .with_state::() - .with_state::() - .with_action::(); - - // generate traces using Rust API - let mut traces = { - let all_traces = options.traces(&tla_tests_file, &tla_config_file)?; - let mut values: Vec, Error>> = - all_traces.into_values().collect(); - values.remove(0) - }?; - - // extract single trace - assert_eq!(traces.len(), 1, "a single trace should have been generated"); - let trace = traces.pop().unwrap(); - - let result = runner.run(&mut system, &mut EventStream::from(trace).into_iter()); - assert!(result.is_ok()); - assert_eq!(system, expected); - - // TODO: disabling these tests for now, as they do not integrate well - // with running model checkers in a temporary directory - // See https://github.com/informalsystems/modelator/issues/47 - // - // // generate traces using CLI - // let mut traces = cli_traces(&tla_tests_file, &tla_config_file, &options)?; - // // extract single trace - // assert_eq!(traces.len(), 1, "a single trace should have been generated"); - // let trace = traces.pop().unwrap(); - // assert_eq!(trace, expected); - - // // parse file if apalache and simply assert it works - // if model_checker == ModelChecker::Apalache { - // use std::convert::TryFrom; - // let tla_tests_file = TlaFile::try_from(tla_tests_file).unwrap(); - // let tla_parsed_file = - // modelator::module::Apalache::parse(tla_tests_file, &options).unwrap(); - // std::fs::remove_file(tla_parsed_file.path()).unwrap(); - // } +fn run_single_test( + batch: &TestBatch, + test_content: &TestContent, +) -> Result<(), IntegrationTestError> { + match test_content { + TestContent::Cli { cmd, expect_status } => { + let os_args = mimic_os_args(cmd); + let cli_app = modelator::cli::App::try_parse_from(os_args)?; + let result = cli_app.run(); + let actual = serde_json::to_string(&result.status).unwrap(); + // The actual status is a double quoted string so add quotes + let expect = format!("\"{}\"", expect_status); + match expect == actual { + true => Ok(()), + false => Err(IntegrationTestError::ExpectedValueMismatch(expect, actual)), + } } + TestContent::StepRunner { + test_function, + tla_tests_filename, + tla_config_filename, + expect, + model_checker_runtime, + } => batch.step_runner.as_ref().unwrap()(StepRunnerArgs { + test_function_name: test_function.to_owned(), + tla_tests_filepath: resource_path(tla_tests_filename), + tla_config_filepath: resource_path(tla_config_filename), + expect: expect.to_owned(), + modelator_runtime: ModelatorRuntime::default() + .model_checker_runtime(model_checker_runtime.to_model_checker_runtime()), + }), } - Ok(()) } -// TODO: remove because deprecated in current CLI -#[allow(dead_code)] -fn cli_traces>( - tla_tests_file: P, - tla_config_file: P, - options: &ModelatorRuntime, -) -> Result, Error> { - use clap::Clap; - // run CLI to generate tests - let cli_output = App::parse_from(&[ - "modelator", - "tla", - "generate-tests", - &tla_tests_file.as_ref().to_string_lossy().to_string(), - &tla_config_file.as_ref().to_string_lossy().to_string(), - ]) - .run(); - assert_eq!(cli_output.status, CliStatus::Success); - let tests = cli_output - .result - .as_array() - .unwrap() - .iter() - .map(|json_entry| { - let test = json_entry.as_object().unwrap(); - ( - test.get("tla_file").unwrap().as_str().unwrap(), - test.get("tla_config_file").unwrap().as_str().unwrap(), - ) - }) - .collect::>(); +/// Loads the .json files registered in test_batch_resources and creates test batches +fn load_test_batches() -> Result, IntegrationTestError> { + let mut ret = Vec::new(); + for resource_bundle in test_batch_resources() { + let config = TestBatchConfig::load(resource_bundle.config_filename)?; - // run CLI to run the model checker configured on each tla test - // needless collect is allowed because the we need to read - // the artifacts before they are removed - #[allow(clippy::needless_collect)] - let traces = tests - .iter() - .map(|(tla_file, tla_config_file)| { - let module = match options.model_checker_runtime.model_checker { - ModelChecker::Tlc => "tlc", - ModelChecker::Apalache => "apalache", - }; - App::parse_from(&["modelator", module, "test", tla_file, tla_config_file]).run() - }) - .map(|cli_output| { - assert_eq!(cli_output.status, CliStatus::Success); - cli_output - .result - .as_object() - .unwrap() - .get("tla_trace_file") - .unwrap() - .as_str() - .unwrap() - .to_owned() - }) - .collect::>(); + let batch = TestBatch { + config, + step_runner: resource_bundle.step_runner, + }; - // cleanup test files created - for (tla_file, tla_config_file) in tests { - std::fs::remove_file(tla_file).unwrap(); - std::fs::remove_file(tla_config_file).unwrap(); + ret.push(batch); } - - // run CLI to convert each tla trace to json - let traces = traces - .into_iter() - .map(|tla_trace_file| { - App::parse_from(&[ - "modelator", - "tla", - "tla-trace-to-json-trace", - &tla_trace_file, - ]) - .run() - }) - .map(|cli_output| { - assert_eq!(cli_output.status, CliStatus::Success); - cli_output - .result - .as_object() - .unwrap() - .get("json_trace_file") - .unwrap() - .as_str() - .unwrap() - .to_owned() - }) - .map(|json_trace_file| { - let json_trace = std::fs::read_to_string(json_trace_file).unwrap(); - serde_json::from_str::>(&json_trace) - .unwrap() - .into() - }) - .collect::>(); - Ok(traces) -} - -fn absolute_and_relative_paths( - tla_tests_file: &'static str, - tla_config_file: &'static str, -) -> Vec<(PathBuf, PathBuf)> { - // compute path to tla dir - let tla_dir = Path::new(TLA_DIR); - let relative_tla_tests_file = tla_dir.join(tla_tests_file); - let relative_tla_config_file = tla_dir.join(tla_config_file); - let absolute_tla_tests_file = relative_tla_tests_file.canonicalize().unwrap(); - let absolute_tla_config_file = relative_tla_config_file.canonicalize().unwrap(); - vec![ - (relative_tla_tests_file, relative_tla_config_file), - (absolute_tla_tests_file, absolute_tla_config_file), - ] -} - -fn numbers_a_max_b_min_test() -> (&'static str, &'static str, NumberSystem) { - let tla_tests_file = "NumbersAMaxBMinTest.tla"; - let tla_config_file = "Numbers.cfg"; - let expected = NumberSystem { - a: 6, - b: 0, - sum: 6, - prod: 0, - }; - (tla_tests_file, tla_config_file, expected) -} - -fn numbers_a_min_b_max_test() -> (&'static str, &'static str, NumberSystem) { - let tla_tests_file = "NumbersAMinBMaxTest.tla"; - let tla_config_file = "Numbers.cfg"; - let expected = NumberSystem { - a: 0, - b: 6, - sum: 6, - prod: 0, - }; - (tla_tests_file, tla_config_file, expected) -} - -fn numbers_a_max_b_max_test() -> (&'static str, &'static str, NumberSystem) { - let tla_tests_file = "NumbersAMaxBMaxTest.tla"; - let tla_config_file = "Numbers.cfg"; - let expected = NumberSystem { - a: 6, - b: 6, - sum: 12, - prod: 36, - }; - (tla_tests_file, tla_config_file, expected) + Ok(ret) } diff --git a/modelator/tests/integration/resource/2PossibleTraces.cfg b/modelator/tests/integration/resource/2PossibleTraces.cfg new file mode 100644 index 00000000..647db035 --- /dev/null +++ b/modelator/tests/integration/resource/2PossibleTraces.cfg @@ -0,0 +1,2 @@ +INIT Init +NEXT Next \ No newline at end of file diff --git a/modelator/tests/integration/resource/2PossibleTraces.json b/modelator/tests/integration/resource/2PossibleTraces.json new file mode 100644 index 00000000..4eec0f8c --- /dev/null +++ b/modelator/tests/integration/resource/2PossibleTraces.json @@ -0,0 +1,33 @@ +{ + "name": "2PossibleTraces", + "description": "", + "tests": [ + { + "name": "generate 1", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace tests/integration/resource/2PossibleTracesTests.tla tests/integration/resource/2PossibleTraces.cfg", + "expect_status": "success" + } + }, + { + "name": "generate 2", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace -n 2 tests/integration/resource/2PossibleTracesTests.tla tests/integration/resource/2PossibleTraces.cfg", + "expect_status": "success" + } + }, + { + "name": "try to generate 3", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace -n 3 tests/integration/resource/2PossibleTracesTests.tla tests/integration/resource/2PossibleTraces.cfg", + "expect_status": "success" + } + } + ] +} \ No newline at end of file diff --git a/modelator/tests/integration/resource/2PossibleTraces.tla b/modelator/tests/integration/resource/2PossibleTraces.tla new file mode 100644 index 00000000..c1c9a1fb --- /dev/null +++ b/modelator/tests/integration/resource/2PossibleTraces.tla @@ -0,0 +1,30 @@ +------------------------------------ MODULE 2PossibleTraces ----------------------------- +(* +There should be only two possible paths for x to reach 3 +0 -> 1 -> 3 +0 -> 2 -> 3 +*) + +EXTENDS Integers, FiniteSets, Sequences, TLC + +VARIABLES + \* @type: Int; + x + +\* @type: () => Bool; +Init == x = 0 + +ZeroToOne == x = 0 /\ x' = 1 +ZeroToTwo == x = 0 /\ x' = 2 +OneToThree == x = 1 /\ x' = 3 +TwoToThree == x = 2 /\ x' = 3 +ThreePlus == 2 < x /\ x' = x + 1 + +Next == + \/ ZeroToOne + \/ ZeroToTwo + \/ OneToThree + \/ TwoToThree + \/ ThreePlus + +=============================================================================== diff --git a/modelator/tests/integration/resource/2PossibleTracesTests.tla b/modelator/tests/integration/resource/2PossibleTracesTests.tla new file mode 100644 index 00000000..14ea1dbc --- /dev/null +++ b/modelator/tests/integration/resource/2PossibleTracesTests.tla @@ -0,0 +1,9 @@ +------------------------------ MODULE 2PossibleTracesTests -------------------------------- + +EXTENDS 2PossibleTraces + +TestIsThree == x = 3 + +View == x + +=============================================================================== \ No newline at end of file diff --git a/modelator/tests/integration/resource/IBC_ics02.json b/modelator/tests/integration/resource/IBC_ics02.json new file mode 100644 index 00000000..768e76dd --- /dev/null +++ b/modelator/tests/integration/resource/IBC_ics02.json @@ -0,0 +1,15 @@ +{ + "name": "IBC_ics02", + "description": "", + "tests": [ + { + "name": "", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator parse tests/integration/resource/IBC_ics02.tla", + "expect_status": "success" + } + } + ] +} \ No newline at end of file diff --git a/modelator/tests/integration/tla/IBC_ics02.tla b/modelator/tests/integration/resource/IBC_ics02.tla similarity index 100% rename from modelator/tests/integration/tla/IBC_ics02.tla rename to modelator/tests/integration/resource/IBC_ics02.tla diff --git a/modelator/tests/integration/tla/Indices.cfg b/modelator/tests/integration/resource/Indices.cfg similarity index 100% rename from modelator/tests/integration/tla/Indices.cfg rename to modelator/tests/integration/resource/Indices.cfg diff --git a/modelator/tests/integration/resource/Indices.json b/modelator/tests/integration/resource/Indices.json new file mode 100644 index 00000000..17b3802e --- /dev/null +++ b/modelator/tests/integration/resource/Indices.json @@ -0,0 +1,42 @@ +{ + "name": "Indices", + "description": "", + "tests": [ + { + "name": "match non existing test", + "description": "Trying to trace a test that doesn't exist should fail", + "content": { + "type": "cli", + "cmd": "modelator trace -t TestNotExist tests/integration/resource/IndicesHistoryTests.tla tests/integration/resource/IndicesTests.cfg", + "expect_status": "error" + } + }, + { + "name": "match one test", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace -t Test2Claim tests/integration/resource/IndicesHistoryTests.tla tests/integration/resource/IndicesTests.cfg", + "expect_status": "success" + } + }, + { + "name": "use tlc", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace -m tlc -t TestClaim tests/integration/resource/IndicesTests.tla tests/integration/resource/IndicesTests.cfg", + "expect_status": "success" + } + }, + { + "name": "generate many traces", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace -n 5 tests/integration/resource/IndicesTests.tla tests/integration/resource/IndicesTests.cfg", + "expect_status": "success" + } + } + ] +} \ No newline at end of file diff --git a/modelator/tests/integration/tla/Indices.tla b/modelator/tests/integration/resource/Indices.tla similarity index 100% rename from modelator/tests/integration/tla/Indices.tla rename to modelator/tests/integration/resource/Indices.tla diff --git a/modelator/tests/integration/tla/IndicesBalances.tla b/modelator/tests/integration/resource/IndicesBalances.tla similarity index 100% rename from modelator/tests/integration/tla/IndicesBalances.tla rename to modelator/tests/integration/resource/IndicesBalances.tla diff --git a/modelator/tests/integration/tla/IndicesBalancesExec.tla b/modelator/tests/integration/resource/IndicesBalancesExec.tla similarity index 100% rename from modelator/tests/integration/tla/IndicesBalancesExec.tla rename to modelator/tests/integration/resource/IndicesBalancesExec.tla diff --git a/modelator/tests/integration/tla/IndicesBalancesHistoryTests.tla b/modelator/tests/integration/resource/IndicesBalancesHistoryTests.tla similarity index 98% rename from modelator/tests/integration/tla/IndicesBalancesHistoryTests.tla rename to modelator/tests/integration/resource/IndicesBalancesHistoryTests.tla index feb4f0e9..c1270563 100644 --- a/modelator/tests/integration/tla/IndicesBalancesHistoryTests.tla +++ b/modelator/tests/integration/resource/IndicesBalancesHistoryTests.tla @@ -24,14 +24,14 @@ VARIABLES \* This predicate extends the Init predicate with history tracking -TestInit == +InitForTest == /\ Init /\ nsteps = 0 /\ history = [ n \in {0} |-> [ action |-> action, actionOutcome |-> actionOutcome, balances |-> balances ]] \* This predicate extends the Next predicate with history tracking -TestNext == +NextForTest == /\ Next /\ nsteps' = nsteps + 1 /\ history' = [ n \in DOMAIN history \union {nsteps'} |-> diff --git a/modelator/tests/integration/tla/IndicesBalancesTests.tla b/modelator/tests/integration/resource/IndicesBalancesTests.tla similarity index 97% rename from modelator/tests/integration/tla/IndicesBalancesTests.tla rename to modelator/tests/integration/resource/IndicesBalancesTests.tla index 952a7128..84821beb 100644 --- a/modelator/tests/integration/tla/IndicesBalancesTests.tla +++ b/modelator/tests/integration/resource/IndicesBalancesTests.tla @@ -20,8 +20,8 @@ EXTENDS IndicesBalancesExec \* @type: <>; View == << action.type, actionOutcome >> -TestInit == Init -TestNext == Next +InitForTest == Init +NextForTest == Next TestClaim == action.type = "Claim" diff --git a/modelator/tests/integration/tla/IndicesExec.tla b/modelator/tests/integration/resource/IndicesExec.tla similarity index 100% rename from modelator/tests/integration/tla/IndicesExec.tla rename to modelator/tests/integration/resource/IndicesExec.tla diff --git a/modelator/tests/integration/tla/IndicesHistoryTests.tla b/modelator/tests/integration/resource/IndicesHistoryTests.tla similarity index 98% rename from modelator/tests/integration/tla/IndicesHistoryTests.tla rename to modelator/tests/integration/resource/IndicesHistoryTests.tla index 07be6e62..b03d7896 100644 --- a/modelator/tests/integration/tla/IndicesHistoryTests.tla +++ b/modelator/tests/integration/resource/IndicesHistoryTests.tla @@ -24,14 +24,14 @@ VARIABLES \* This predicate extends the Init predicate with history tracking -TestInit == +InitForTest == /\ Init /\ nsteps = 0 /\ history = [ n \in {0} |-> [ action |-> action, actionOutcome |-> actionOutcome]] \* This predicate extends the Next predicate with history tracking -TestNext == +NextForTest == /\ Next /\ nsteps' = nsteps + 1 /\ history' = [ n \in DOMAIN history \union {nsteps'} |-> diff --git a/modelator/tests/integration/tla/IndicesTests.cfg b/modelator/tests/integration/resource/IndicesTests.cfg similarity index 59% rename from modelator/tests/integration/tla/IndicesTests.cfg rename to modelator/tests/integration/resource/IndicesTests.cfg index 88a916de..0fae5db8 100644 --- a/modelator/tests/integration/tla/IndicesTests.cfg +++ b/modelator/tests/integration/resource/IndicesTests.cfg @@ -2,5 +2,5 @@ CONSTANTS NUM_USERS = 4 NUM_INDICES = 4 -INIT TestInit -NEXT TestNext +INIT InitForTest +NEXT NextForTest diff --git a/modelator/tests/integration/tla/IndicesTests.tla b/modelator/tests/integration/resource/IndicesTests.tla similarity index 97% rename from modelator/tests/integration/tla/IndicesTests.tla rename to modelator/tests/integration/resource/IndicesTests.tla index 7dec1a13..aa246a0f 100644 --- a/modelator/tests/integration/tla/IndicesTests.tla +++ b/modelator/tests/integration/resource/IndicesTests.tla @@ -20,8 +20,8 @@ EXTENDS IndicesExec \* @type: <>; View == << action.type, actionOutcome >> -TestInit == Init -TestNext == Next +InitForTest == Init +NextForTest == Next TestClaim == action.type = "Claim" diff --git a/modelator/tests/integration/tla/Numbers.cfg b/modelator/tests/integration/resource/Numbers.cfg similarity index 100% rename from modelator/tests/integration/tla/Numbers.cfg rename to modelator/tests/integration/resource/Numbers.cfg diff --git a/modelator/tests/integration/resource/Numbers.json b/modelator/tests/integration/resource/Numbers.json new file mode 100644 index 00000000..e05335bf --- /dev/null +++ b/modelator/tests/integration/resource/Numbers.json @@ -0,0 +1,111 @@ +{ + "name": "Numbers", + "description": "", + "tests": [ + { + "name": "", + "description": "", + "content": { + "type": "step_runner", + "test_function": "default", + "tla_tests_filename": "NumbersAMaxBMaxTest.tla", + "tla_config_filename": "Numbers.cfg", + "model_checker_runtime": { + "model_checker": "apalache", + "workers": "auto", + "traces_per_test": "1" + }, + "expect": { + "a": 6, + "b": 6, + "sum": 12, + "prod": 36 + } + } + }, + { + "name": "", + "description": "", + "content": { + "type": "step_runner", + "test_function": "default", + "tla_tests_filename": "NumbersAMaxBMinTest.tla", + "tla_config_filename": "Numbers.cfg", + "model_checker_runtime": { + "model_checker": "apalache", + "workers": "auto", + "traces_per_test": "1" + }, + "expect": { + "a": 6, + "b": 0, + "sum": 6, + "prod": 0 + } + } + }, + { + "name": "", + "description": "", + "content": { + "type": "step_runner", + "test_function": "default", + "tla_tests_filename": "NumbersAMinBMaxTest.tla", + "tla_config_filename": "Numbers.cfg", + "model_checker_runtime": { + "model_checker": "apalache", + "workers": "auto", + "traces_per_test": "1" + }, + "expect": { + "a": 0, + "b": 6, + "sum": 6, + "prod": 0 + } + } + }, + { + "name": "", + "description": "", + "content": { + "type": "step_runner", + "test_function": "default", + "tla_tests_filename": "NumbersAMinBMaxTest.tla", + "tla_config_filename": "Numbers.cfg", + "model_checker_runtime": { + "model_checker": "apalache", + "workers": "auto", + "traces_per_test": "2" + }, + "expect": { + "a": 0, + "b": 6, + "sum": 6, + "prod": 0 + } + } + }, + { + "name": "", + "description": "", + "content": { + "type": "step_runner", + "test_function": "default", + "tla_tests_filename": "NumbersAMinBMaxTest.tla", + "tla_config_filename": "Numbers.cfg", + "model_checker_runtime": { + "model_checker": "tlc", + "workers": "auto", + "traces_per_test": "1" + }, + "expect": { + "a": 0, + "b": 6, + "sum": 6, + "prod": 0 + } + } + } + ] +} \ No newline at end of file diff --git a/modelator/tests/integration/tla/Numbers.tla b/modelator/tests/integration/resource/Numbers.tla similarity index 100% rename from modelator/tests/integration/tla/Numbers.tla rename to modelator/tests/integration/resource/Numbers.tla diff --git a/modelator/tests/integration/tla/NumbersAMaxBMaxTest.tla b/modelator/tests/integration/resource/NumbersAMaxBMaxTest.tla similarity index 100% rename from modelator/tests/integration/tla/NumbersAMaxBMaxTest.tla rename to modelator/tests/integration/resource/NumbersAMaxBMaxTest.tla diff --git a/modelator/tests/integration/tla/NumbersAMaxBMinTest.tla b/modelator/tests/integration/resource/NumbersAMaxBMinTest.tla similarity index 100% rename from modelator/tests/integration/tla/NumbersAMaxBMinTest.tla rename to modelator/tests/integration/resource/NumbersAMaxBMinTest.tla diff --git a/modelator/tests/integration/tla/NumbersAMinBMaxTest.tla b/modelator/tests/integration/resource/NumbersAMinBMaxTest.tla similarity index 100% rename from modelator/tests/integration/tla/NumbersAMinBMaxTest.tla rename to modelator/tests/integration/resource/NumbersAMinBMaxTest.tla diff --git a/modelator/tests/integration/resource/TrafficCrossing.json b/modelator/tests/integration/resource/TrafficCrossing.json new file mode 100644 index 00000000..bc401e31 --- /dev/null +++ b/modelator/tests/integration/resource/TrafficCrossing.json @@ -0,0 +1,51 @@ +{ + "name": "TrafficCrossing", + "description": "", + "tests": [ + { + "name": "", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator parse tests/integration/resource/TrafficCrossing.tla", + "expect_status": "success" + } + }, + { + "name": "", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator parse tests/integration/resource/TrafficCrossingTest.tla", + "expect_status": "success" + } + }, + { + "name": "", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator parse tests/integration/resource/TrafficCrossingHistoryTest.tla", + "expect_status": "success" + } + }, + { + "name": "", + "description": "", + "content": { + "type": "cli", + "cmd": "modelator trace tests/integration/resource/TrafficCrossingTest.tla tests/integration/resource/TrafficCrossingTest.cfg", + "expect_status": "success" + } + }, + { + "name": "", + "description": "An annotation should be required", + "content": { + "type": "cli", + "cmd": "modelator trace tests/integration/resource/TrafficCrossingHistoryTest.tla tests/integration/resource/TrafficCrossingHistoryTest.cfg", + "expect_status": "error" + } + } + ] +} \ No newline at end of file diff --git a/modelator/tests/integration/tla/TrafficCrossing.tla b/modelator/tests/integration/resource/TrafficCrossing.tla similarity index 100% rename from modelator/tests/integration/tla/TrafficCrossing.tla rename to modelator/tests/integration/resource/TrafficCrossing.tla diff --git a/modelator/tests/integration/tla/TrafficCrossingHistoryTest.cfg b/modelator/tests/integration/resource/TrafficCrossingHistoryTest.cfg similarity index 100% rename from modelator/tests/integration/tla/TrafficCrossingHistoryTest.cfg rename to modelator/tests/integration/resource/TrafficCrossingHistoryTest.cfg diff --git a/modelator/tests/integration/tla/TrafficCrossingHistoryTest.tla b/modelator/tests/integration/resource/TrafficCrossingHistoryTest.tla similarity index 100% rename from modelator/tests/integration/tla/TrafficCrossingHistoryTest.tla rename to modelator/tests/integration/resource/TrafficCrossingHistoryTest.tla diff --git a/modelator/tests/integration/tla/TrafficCrossingTest.cfg b/modelator/tests/integration/resource/TrafficCrossingTest.cfg similarity index 100% rename from modelator/tests/integration/tla/TrafficCrossingTest.cfg rename to modelator/tests/integration/resource/TrafficCrossingTest.cfg diff --git a/modelator/tests/integration/tla/TrafficCrossingTest.tla b/modelator/tests/integration/resource/TrafficCrossingTest.tla similarity index 100% rename from modelator/tests/integration/tla/TrafficCrossingTest.tla rename to modelator/tests/integration/resource/TrafficCrossingTest.tla diff --git a/modelator/tests/integration/resource/mod.rs b/modelator/tests/integration/resource/mod.rs new file mode 100644 index 00000000..de7c6ffb --- /dev/null +++ b/modelator/tests/integration/resource/mod.rs @@ -0,0 +1 @@ +pub mod numbers; diff --git a/modelator/tests/integration/resource/numbers.rs b/modelator/tests/integration/resource/numbers.rs new file mode 100644 index 00000000..f58285ff --- /dev/null +++ b/modelator/tests/integration/resource/numbers.rs @@ -0,0 +1,74 @@ +use crate::common::StepRunnerArgs; +use crate::error::IntegrationTestError; + +use modelator::test_util::NumberSystem; +use serde::Deserialize; + +#[derive(Debug, Clone, Deserialize)] +#[serde(rename_all = "camelCase")] +struct NumbersStep { + a: u64, + b: u64, + action: Action, + action_outcome: String, +} + +// We also define the abstract actions: do nothing / increase a / increase b. +#[derive(Debug, Clone, Deserialize)] +enum Action { + None, + IncreaseA, + IncreaseB, +} + +impl modelator::step_runner::StepRunner for NumberSystem { + fn initial_step(&mut self, step: NumbersStep) -> Result<(), String> { + self.a = step.a; + self.b = step.b; + self.recalculate(); + Ok(()) + } + + // how to handle all subsequent steps + fn next_step(&mut self, step: NumbersStep) -> Result<(), String> { + // Execute the action, and check the outcome + let res = match step.action { + Action::None => Ok(()), + Action::IncreaseA => self.increase_a(1), + Action::IncreaseB => self.increase_b(2), + }; + let outcome = match res { + Ok(()) => "OK".to_string(), + Err(s) => s, + }; + assert_eq!(outcome, step.action_outcome); + + // Check that the system state matches the state of the model + assert_eq!(self.a, step.a); + assert_eq!(self.b, step.b); + + Ok(()) + } +} + +pub fn test(args: StepRunnerArgs) -> Result<(), IntegrationTestError> { + match args.test_function_name.as_str() { + "default" => { + let mut system = NumberSystem::default(); + + args.modelator_runtime.run_tla_steps( + args.tla_tests_filepath, + args.tla_config_filepath, + &mut system, + )?; + + let expect: NumberSystem = serde_json::value::from_value(args.expect)?; + + assert_eq!(system, expect); + Ok(()) + } + _ => Err(IntegrationTestError::FaultyTest( + "Wrong test_function name given as argument to numbers.rs test".into(), + )), + } +} diff --git a/modelator/tests/integration/resource/smoke.json b/modelator/tests/integration/resource/smoke.json new file mode 100644 index 00000000..e1a92786 --- /dev/null +++ b/modelator/tests/integration/resource/smoke.json @@ -0,0 +1,5 @@ +{ + "name": "smoke", + "description": "This json file is only used to test the implementation of the integration test framework", + "tests": [] +} \ No newline at end of file