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 <[email protected]>
Co-authored-by: Ranadeep Biswas <[email protected]>

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"

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<G: Generator>(app: &mut App) {
-    generate::<G, _>(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::<Bash>(&mut modelator_app),
-        ShellName::Elvish => print_completions::<Elvish>(&mut modelator_app),
-        ShellName::Fish => print_completions::<Fish>(&mut modelator_app),
-        ShellName::Powershell => print_completions::<PowerShell>(&mut modelator_app),
-        ShellName::Zsh => print_completions::<Zsh>(&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()),
     }
 }

modelator/src/artifact/tla_file_suite.rs

@@ -39,7 +39,7 @@ fn find_dependencies(tla_module_path: impl AsRef<std::path::Path>) -> Result<Vec
     let current_directory = tla_module_path
         .as_ref()
         .parent()
-        .expect("expected a final componenet")
+        .expect("expected a final component")
         .to_path_buf();
 
     let content = crate::util::try_read_file_contents(tla_module_path)?;

modelator/src/cli/mod.rs

@@ -11,20 +11,23 @@ use crate::artifact::{Artifact, JsonTrace, TlaFile, TlaFileSuite, TlaTrace};
 use crate::model::checker::ModelChecker;
 use crate::Error;
 use clap::{crate_authors, crate_description, crate_license, crate_name, crate_version};
-use clap::{AppSettings, ArgEnum, ArgSettings, Clap, Subcommand, ValueHint};
+use clap::{AppSettings, ArgEnum, ArgSettings, ColorChoice, Parser, Subcommand, ValueHint};
 use serde_json::{json, Value as JsonValue};
 use std::path::Path;
 
 /// Re-exports.
 pub use output::{CliOutput, CliStatus};
 
 /// Parse TLA+ files with Apalache.
-#[derive(Debug, Clap)]
-#[clap(setting = AppSettings::ColoredHelp)]
+#[derive(Debug, Parser)]
+#[clap(color = ColorChoice::Auto)]
 pub struct ParseCli {
     /// TLA+ file with test cases.
     #[clap(parse(from_os_str), value_hint = ValueHint::FilePath)]
     tla_module: PathBuf,
+    /// Whether or not to write the output file
+    #[clap(long)]
+    write: bool,
 }
 
 impl ParseCli {
@@ -33,13 +36,18 @@ impl ParseCli {
         let tla_file = TlaFileSuite::from_tla_path(&self.tla_module)?;
         let res = crate::model::checker::Apalache::parse(&tla_file, &runtime)?;
         tracing::debug!("Apalache::parse output {}", res.0);
-        write_parsed_tla_file_to_file(&res.0)
+        if self.write {
+            write_parsed_tla_file_to_file(&res.0)
+        } else {
+            Ok(json!({
+                "tla_file_content": res.0.as_string(),
+            }))
+        }
     }
 }
 
-/// Parse TLA+ files with Apalache.
-#[derive(Debug, Clap)]
-#[clap(setting = AppSettings::ColoredHelp)]
+#[derive(Debug, Parser)]
+/// List the tests in a TLA file
 pub struct TestListCli {
     /// TLA+ file with test cases.
     #[clap(parse(from_os_str), value_hint = ValueHint::FilePath)]
@@ -58,28 +66,31 @@ impl TestListCli {
 }
 
 /// Test models with Apalache/TLC
-#[derive(Debug, Clap)]
-#[clap(setting = AppSettings::ColoredHelp)]
+#[derive(Debug, Parser)]
+#[clap(color = ColorChoice::Auto)]
 pub struct TraceCli {
     /// test name
     #[clap(short, long, default_value = "@all")]
     test: String,
-    /// TODO: derive ArgEnum for ModelChecker enum
+    // TODO: derive ArgEnum for ModelChecker enum
     /// Checker name
     #[clap(short, long, possible_values = &["apalache", "tlc"], default_value = "apalache")]
     model_checker: ModelChecker,
     /// output format
     #[clap(short, long, arg_enum, default_value = "json")]
     format: OutputFormat,
-    /// The number of traces to generate for a single test.
-    #[clap(short, long, default_value = "0")]
+    /// The maximum number of traces to generate for a single test.
+    #[clap(short, long, default_value = "1")]
     num_traces: usize,
     /// TLA+ file with test cases.
     #[clap(parse(from_os_str), value_hint = ValueHint::FilePath)]
     tla_module: PathBuf,
     /// TLA+ config file with CONSTANTS, INIT and NEXT.
     #[clap(parse(from_os_str), value_hint = ValueHint::FilePath)]
     tla_config: PathBuf,
+    /// Whether or not to write output files
+    #[clap(long)]
+    write: bool,
 }
 
 impl TraceCli {
@@ -93,11 +104,21 @@ impl TraceCli {
         let tla_file_suite =
             TlaFileSuite::from_tla_and_config_paths(&self.tla_module, &self.tla_config)?;
 
-        let test_names = crate::model::language::Tla::extract_test_names(
+        let test_names: Vec<String> = 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<String, Result<Vec<JsonValue>, 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<Json
 
 fn write_parsed_tla_file_to_file(tla_file: &TlaFile) -> Result<JsonValue, Error> {
     // 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<Json
     let path = Path::new(&file_name);
     tla_trace.try_write_to_file(path)?;
     Ok(json!({
-        "tla_trace_file": crate::util::absolute_path(&path),
+        "tla_trace_filepath": crate::util::absolute_path(&path),
     }))
 }
 
@@ -254,6 +288,6 @@ fn write_json_trace_to_file(test_name: &str, json_trace: &JsonTrace) -> Result<J
     let path = Path::new(&file_name);
     json_trace.try_write_to_file(path)?;
     Ok(json!({
-        "json_trace_file": crate::util::absolute_path(&path),
+        "json_trace_filepath": crate::util::absolute_path(&path),
     }))
 }

modelator/src/cli/output.rs

@@ -1,11 +1,11 @@
 // This module is inspired by what's in:
 // https://github.com/informalsystems/ibc-rs/blob/ad827a94e5c84ceb1af764a255dd1821d7852fef/relayer-cli/src/conclude.rs
 use crate::Error;
+use serde::Deserialize;
 use serde::Serialize;
 use serde_json::Value as JsonValue;
 
 /// Struct representing the output of `modelator` CLI.
-/// See [`super::CliOptions`].
 #[derive(Serialize, Debug)]
 pub struct CliOutput {
     /// The return status
@@ -51,13 +51,11 @@ impl CliOutput {
 }
 
 /// Represents the exit status of any CLI command
-#[derive(Serialize, Debug, PartialEq, Eq, Clone, Copy)]
+#[derive(Serialize, Debug, PartialEq, Eq, Clone, Copy, Deserialize)]
+#[serde(rename_all = "snake_case")]
 pub enum CliStatus {
     /// An exit status representing success.
-    #[serde(rename(serialize = "success"))]
     Success,
-
     /// An exit status representing an error.
-    #[serde(rename(serialize = "error"))]
     Error,
 }

modelator/src/jar.rs

@@ -72,7 +72,7 @@ impl Jar {
     }
 }
 
-pub(crate) fn download_jars<P: AsRef<Path>>(modelator_dir: P) -> Result<(), Error> {
+pub(crate) fn download_jars_if_necessary<P: AsRef<Path>>(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<P: AsRef<Path>>(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(())