From 540f89f660dbb7116c8af9b358db3cd331c01c2b Mon Sep 17 00:00:00 2001 From: Daniel Tisdall Date: Tue, 24 Aug 2021 14:02:47 +0100 Subject: [PATCH 1/4] Squashed commit of the following: commit ee4c1dc4edba2ea3f69cda4188874f5e15a799c7 Author: Daniel Tisdall Date: Tue Aug 24 13:59:35 2021 +0100 Adds todos to Apalache and Tlc mod.rs's commit 97e62608f4988cac1841310e6c927c7dac9bbe9b Author: Daniel Tisdall Date: Tue Aug 24 13:48:17 2021 +0100 Removes todo in tla module generate_test commit e250158d692cbdcbe95d1439f3b16bcb57b128da Author: Daniel Tisdall Date: Tue Aug 24 13:48:01 2021 +0100 Clarifies file path var names in cli commit 5fae1aa2c8740dc64375f80b16878419bf2f8958 Author: Daniel Tisdall Date: Tue Aug 24 13:30:45 2021 +0100 Partially refactors the use of TlaFile in tla module commit b3f74f15fe07468596d072b6c2949a1767cab30b Author: Daniel Tisdall Date: Tue Aug 24 13:11:41 2021 +0100 TlaFile now saves content and filename internally commit e964abd64fb32456a7472371847a89b11ee51c93 Author: Daniel Tisdall Date: Tue Aug 24 12:51:23 2021 +0100 Renames tla_module_name -> tla_file_name commit 84ab1b63fc6f46d60dd04848d7968e2371f7e59f Author: Daniel Tisdall Date: Tue Aug 24 12:32:44 2021 +0100 Pre TlaFile explicit pathing teardown commit 2438928b32010cbe88b2954b1fd6daa00fb4f011 Author: Daniel Tisdall Date: Tue Aug 24 12:19:56 2021 +0100 Scaffolds Artifact impl for tla_file commit 717de02adbc470d57d29cfcbd63df965d9a791e6 Author: Daniel Tisdall Date: Tue Aug 24 12:16:08 2021 +0100 Reworks Artifact trait to use TryFrom super traits commit 7bf78ec624bf2f0c62b97b714496217f3da54363 Author: Daniel Tisdall Date: Tue Aug 24 11:22:12 2021 +0100 Clarifies path/file var naming in lib.rs traces commit a3ef51fe132f2a8c624e8a7a8c78042a0e102156 Author: Daniel Tisdall Date: Tue Aug 24 11:16:44 2021 +0100 Clarifies naming of internal struct in tla_trace commit bbf6156622be5e0f92be92815b800a58612f0b78 Author: Daniel Tisdall Date: Tue Aug 24 11:16:28 2021 +0100 Adds artifact trait impl scaffold to .tla and .cfg reprs. commit 9fca5e3b615e5fcce3b1c72a97a33b6a213d362c Author: Daniel Tisdall Date: Tue Aug 24 11:00:36 2021 +0100 Clarifies method names in mod.rs commit feeaa8594f7d6c6bee9065edca3f29b0b4400633 Author: Daniel Tisdall Date: Tue Aug 24 10:48:58 2021 +0100 Adds basic artifact declarations commit 45548620bad98911ae35ca4f36ec722f32c28630 Author: Daniel Tisdall Date: Tue Aug 24 10:18:39 2021 +0100 Adds artifacts trait commit 36be5a509b9fd896355517dc267f4363fd5dadc8 Author: Daniel Tisdall Date: Tue Aug 24 10:18:32 2021 +0100 note commit 3f58ab00aea74ca50d4f22e1228f372acc9cf800 Merge: be608de a905c1f Author: Daniel Tisdall Date: Tue Aug 24 09:56:51 2021 +0100 Merge branch 'main' into daniel/working commit be608de038ab03f414459a6630803f450e710887 Author: Daniel Tisdall Date: Mon Aug 23 15:17:49 2021 +0100 settings.json commit 41ffa6e41e50673f1221c54be4f7764589f30bf8 Merge: b6102a7 0db7f5e Author: Daniel Tisdall Date: Mon Aug 23 14:34:50 2021 +0100 Merge branch 'main' into daniel/working commit b6102a789ddae1fe12b3615d3edaf611c10db51b Author: Daniel Tisdall Date: Mon Aug 23 14:13:44 2021 +0100 Adds my own notes commit 660bdb5e31c5c5dcf3ca9d929ebfd36840e4607b Author: Daniel Tisdall Date: Mon Aug 23 14:05:07 2021 +0100 Adds apalache debug launcher commit 3afa62e8d7ac7b8bb6ca59a7ffd494ea93ef5845 Author: Daniel Tisdall Date: Mon Aug 23 14:04:48 2021 +0100 Adds trace.tla and log.mc to .gitignore commit b88b76c63546d72152b468a7e274ad569a09d1ab Author: Daniel Tisdall Date: Mon Aug 23 12:06:20 2021 +0100 Gignores Dans vscode commit e423305bb9f90384e1c9505d8c7b36c00cd025ae Author: Daniel Tisdall Date: Mon Aug 23 12:05:23 2021 +0100 notes commit 0b2a83e0554ea4fee9c9555d85d4cb7beb5cb5bd Author: Daniel Tisdall Date: Mon Aug 23 11:08:07 2021 +0100 Adds some notes-to-self --- .gitignore | 8 +-- .vscode/launch.json | 21 ++++++++ .vscode/settings.json | 42 ++++++++++++++++ .vscode/tasks.json | 4 ++ modelator/src/artifact/artifact.rs | 23 +++++++++ modelator/src/artifact/json_trace.rs | 3 ++ modelator/src/artifact/mod.rs | 2 + modelator/src/artifact/tla_cfg_file.rs | 1 + modelator/src/artifact/tla_file.rs | 65 ++++++++++++++++++------ modelator/src/artifact/tla_trace.rs | 21 ++++---- modelator/src/cache/tla_trace.rs | 2 +- modelator/src/cli/mod.rs | 35 +++++++------ modelator/src/lib.rs | 44 +++++++++-------- modelator/src/module/apalache/mod.rs | 16 ++++-- modelator/src/module/tla/mod.rs | 68 ++++++++++++++------------ modelator/src/module/tlc/mod.rs | 3 ++ z_notes.md | 35 +++++++++++++ 17 files changed, 289 insertions(+), 104 deletions(-) create mode 100644 .vscode/launch.json create mode 100644 .vscode/settings.json create mode 100644 .vscode/tasks.json create mode 100644 modelator/src/artifact/artifact.rs create mode 100644 z_notes.md diff --git a/.gitignore b/.gitignore index 3965fc55..0fb4750c 100644 --- a/.gitignore +++ b/.gitignore @@ -9,9 +9,6 @@ Cargo.lock # These are backup files generated by rustfmt **/*.rs.bk -# VSCode files -.vscode/ - # TLC files states/ @@ -30,3 +27,8 @@ counterexample.tla # cargo tarpaulin files tarpaulin/ tarpaulin-report.html + +# VSCode files +# .vscode/ +trace.tla +mc.log diff --git a/.vscode/launch.json b/.vscode/launch.json new file mode 100644 index 00000000..1afa347a --- /dev/null +++ b/.vscode/launch.json @@ -0,0 +1,21 @@ +{ + "configurations": [ + { + "name": "modelator debug build", + "type": "lldb", + "request": "launch", + "program": "${workspaceRoot}/target/debug/modelator", + "args": [ + "apalache", + "test", + "/Users/danwt/documents/sandbox-tla/mainTests_MyVarTest.tla", + "/Users/danwt/documents/sandbox-tla/mainTests_MyVarTest.cfg", + // "tla", + // "generate-tests", + // "main.tla", + // "main.cfg" + ], + "cwd": "${workspaceRoot}", + } + ], +} \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 00000000..e838a14a --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,42 @@ +{ + "editor.formatOnSave": true, + "files.exclude": { + "LICENSE": true, + "**/.git": true, + "**/.DS_Store": true, + "cargo.lock": true, + "**/.modelator": true, + "mc.log": true, + "log*.smt": true, + "MC.out": true, + "profile-rules.txt": true, + "trace.tla": true, + "detailed.log": true, + "counterexample.json": true, + "counterexample.tla": true, + }, + "git.ignoreLimitWarning": true, + "todohighlight.keywords": [ + { + "text": "NOTE:", + "color": "white", + "backgroundColor": "rgb(111, 189, 133)" + }, + { + "text": "PARAM!", + "color": "white", + "backgroundColor": "rgb(182, 90, 199)" + }, + { + "text": "HACK:", + "color": "white", + "backgroundColor": "rgb(199, 96, 0)" + }, + { + "text": "NEXT:", + "color": "white", + "backgroundColor": "rgb(83,158,230)" + }, + ], + "cSpell.diagnosticLevel": "Hint", +} \ No newline at end of file diff --git a/.vscode/tasks.json b/.vscode/tasks.json new file mode 100644 index 00000000..2f24d448 --- /dev/null +++ b/.vscode/tasks.json @@ -0,0 +1,4 @@ +{ + "version": "2.0.0", + "tasks": [] +} \ No newline at end of file diff --git a/modelator/src/artifact/artifact.rs b/modelator/src/artifact/artifact.rs new file mode 100644 index 00000000..05fae350 --- /dev/null +++ b/modelator/src/artifact/artifact.rs @@ -0,0 +1,23 @@ +use crate::Error; +use std::convert::TryFrom; +use std::path::{Path, PathBuf}; +use std::str; + +/// TODO: +pub trait Artifact +where + Self: std::fmt::Display + + for<'a> TryFrom<&'a str, Error = crate::Error> + + TryFrom + + for<'a> TryFrom<&'a Path, Error = crate::Error> + + TryFrom, +{ + fn as_string(&self) -> &str; + fn try_write_to_file(&self, path: &Path) -> Result<(), Error>; +} + +// impl std::fmt::Debug for dyn Artifact { +// fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { +// todo!() +// } +// } diff --git a/modelator/src/artifact/json_trace.rs b/modelator/src/artifact/json_trace.rs index 04b22e36..a1906a52 100644 --- a/modelator/src/artifact/json_trace.rs +++ b/modelator/src/artifact/json_trace.rs @@ -1,4 +1,7 @@ +use super::Artifact; +use crate::Error; use serde_json::Value as JsonValue; +use std::path::Path; /// `modelator`'s artifact containing a test trace encoded as JSON. #[derive(Debug, Clone, PartialEq, Eq)] diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs index 0aba6b36..3b02c14b 100644 --- a/modelator/src/artifact/mod.rs +++ b/modelator/src/artifact/mod.rs @@ -1,9 +1,11 @@ +pub(crate) mod artifact; pub(crate) mod json_trace; pub(crate) mod tla_cfg_file; pub(crate) mod tla_file; pub(crate) mod tla_trace; // Re-exports. +pub use artifact::Artifact; pub use json_trace::JsonTrace; pub use tla_cfg_file::TlaConfigFile; pub use tla_file::TlaFile; diff --git a/modelator/src/artifact/tla_cfg_file.rs b/modelator/src/artifact/tla_cfg_file.rs index ae28d9a9..8cbf11e1 100644 --- a/modelator/src/artifact/tla_cfg_file.rs +++ b/modelator/src/artifact/tla_cfg_file.rs @@ -1,3 +1,4 @@ +use super::Artifact; use crate::Error; use std::convert::TryFrom; use std::path::{Path, PathBuf}; diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs index 822765fe..8a385e72 100644 --- a/modelator/src/artifact/tla_file.rs +++ b/modelator/src/artifact/tla_file.rs @@ -1,38 +1,62 @@ +use super::Artifact; use crate::Error; use std::convert::TryFrom; +use std::fs; use std::path::{Path, PathBuf}; /// `modelator`'s artifact representing a TLA+ file. #[derive(Debug, Clone, PartialEq, Eq)] pub struct TlaFile { path: PathBuf, + content: String, + file_name: String, +} + +/// TODO: +fn tla_file_name(path: &PathBuf) -> Option { + if path.is_file() { + path.file_name().map(|file_name| { + file_name + .to_string_lossy() + .trim_end_matches(".tla") + .to_owned() + }) + } else { + None + } } impl TlaFile { - pub(crate) fn new>(path: P) -> Result { + // pub(crate) fn new>(path: P) -> Result { + fn new>(path: P) -> Result { let path = path.as_ref().to_path_buf(); crate::util::check_file_existence(&path)?; - Ok(Self { path }) + let content: String = fs::read_to_string(&path)?; + let file_name = tla_file_name(&path); + + match file_name { + Some(val) => Ok(Self { + path, + content, + file_name: val, + }), + None => Err(Error::IO(format!("File doesn't exist {}", path.display()))), + } } /// Returns the path to the TLA+ file. - pub fn path(&self) -> &PathBuf { + pub fn path(&self) -> &Path { &self.path } - /// Infer TLA module name. We assume that the TLA module name matches the - /// name of the file. - pub(crate) fn tla_module_name(&self) -> Option { - if self.path.is_file() { - self.path.file_name().map(|file_name| { - file_name - .to_string_lossy() - .trim_end_matches(".tla") - .to_owned() - }) - } else { - None - } + /// Returns the content of the TLA+ file. + pub fn content(&self) -> &str { + &self.content + } + + /// Returns the name of the TLA+ file. + pub fn file_name(&self) -> &str { + &self.file_name } } @@ -72,3 +96,12 @@ impl std::fmt::Display for TlaFile { write!(f, "{}", crate::util::absolute_path(&self.path)) } } + +impl Artifact for TlaFile { + fn as_string(&self) -> &str { + todo!() + } + fn try_write_to_file(&self, path: &Path) -> Result<(), Error> { + todo!() + } +} diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs index 7d9105f6..ba253678 100644 --- a/modelator/src/artifact/tla_trace.rs +++ b/modelator/src/artifact/tla_trace.rs @@ -1,3 +1,4 @@ +use super::Artifact; use crate::Error; use std::str::FromStr; @@ -67,13 +68,6 @@ fn remove_tla_comments(i: &str) -> String { s } -#[derive(Debug)] -struct TlaFile<'a> { - name: &'a str, - extends: Vec<&'a str>, - operators: Vec<(&'a str, &'a str)>, -} - fn tla_identifiers(i: &str) -> IResult<&str, &str> { recognize(pair( alt((alpha1, tag("_"))), @@ -81,7 +75,14 @@ fn tla_identifiers(i: &str) -> IResult<&str, &str> { ))(i) } -fn parse_tla_file(i: &str) -> IResult<&str, TlaFile<'_>> { +#[derive(Debug)] +struct TlaTraceFileContent<'a> { + name: &'a str, + extends: Vec<&'a str>, + operators: Vec<(&'a str, &'a str)>, +} + +fn parse_tla_trace_file_contents(i: &str) -> IResult<&str, TlaTraceFileContent<'_>> { map( terminated( tuple(( @@ -118,7 +119,7 @@ fn parse_tla_file(i: &str) -> IResult<&str, TlaFile<'_>> { )), delimited(multispace0, many1(char('=')), multispace0), ), - |(name, extends, operators)| TlaFile { + |(name, extends, operators)| TlaTraceFileContent { name, extends, operators, @@ -132,7 +133,7 @@ impl FromStr for TlaTrace { fn from_str(tla_trace: &str) -> Result { let tla_trace = remove_tla_comments(tla_trace); - let tla = parse_tla_file(&tla_trace).unwrap().1; + let tla: TlaTraceFileContent = parse_tla_trace_file_contents(&tla_trace).unwrap().1; let mut states: Vec<(usize, &str)> = tla .operators diff --git a/modelator/src/cache/tla_trace.rs b/modelator/src/cache/tla_trace.rs index 2ca79b44..b62941f6 100644 --- a/modelator/src/cache/tla_trace.rs +++ b/modelator/src/cache/tla_trace.rs @@ -29,7 +29,7 @@ impl TlaTraceCache { tracing::debug!("TlaTraceKey:key {} {}", tla_file, tla_config_file); // get all tla files in the same directory - let mut tla_dir = tla_file.path().clone(); + let mut tla_dir = tla_file.path().to_path_buf(); assert!(tla_dir.pop()); let files_to_hash = crate::util::read_dir(&tla_dir)? diff --git a/modelator/src/cli/mod.rs b/modelator/src/cli/mod.rs index edb3dad5..0aa560cf 100644 --- a/modelator/src/cli/mod.rs +++ b/modelator/src/cli/mod.rs @@ -111,14 +111,17 @@ impl TlaMethods { } } - fn generate_tests(tla_file: String, tla_config_file: String) -> Result { + fn generate_tests( + tla_file_path: String, + tla_config_file_path: String, + ) -> Result { use std::convert::TryFrom; - let tla_file = TlaFile::try_from(tla_file)?; - let tla_config_file = TlaConfigFile::try_from(tla_config_file)?; + let tla_file = TlaFile::try_from(tla_file_path)?; + let tla_config_file = TlaConfigFile::try_from(tla_config_file_path)?; let tests = crate::module::Tla::generate_tests(tla_file, tla_config_file)?; tracing::debug!("Tla::generate_tests output {:#?}", tests); - generated_tests(tests) + json_generated_test_list(tests) } fn tla_trace_to_json_trace(tla_trace_file: String) -> Result { @@ -132,7 +135,7 @@ impl TlaMethods { let json_trace = crate::module::Tla::tla_trace_to_json_trace(tla_trace)?; tracing::debug!("Tla::tla_trace_to_json_trace output {}", json_trace); - save_json_trace(json_trace) + write_json_trace_to_file(json_trace) } } @@ -147,15 +150,15 @@ impl ApalacheMethods { } } - fn test(tla_file: String, tla_config_file: String) -> Result { + fn test(tla_file_path: String, tla_config_file_path: String) -> Result { let options = crate::Options::default(); use std::convert::TryFrom; - let tla_file = TlaFile::try_from(tla_file)?; - let tla_config_file = TlaConfigFile::try_from(tla_config_file)?; + let tla_file = TlaFile::try_from(tla_file_path)?; + let tla_config_file = TlaConfigFile::try_from(tla_config_file_path)?; let tla_trace = crate::module::Apalache::test(tla_file, tla_config_file, &options)?; tracing::debug!("Apalache::test output {}", tla_trace); - save_tla_trace(tla_trace) + write_tla_trace_to_file(tla_trace) } fn parse(tla_file: String) -> Result { @@ -179,20 +182,20 @@ impl TlcMethods { } } - fn test(tla_file: String, tla_config_file: String) -> Result { + fn test(tla_file_path: String, tla_config_file_path: String) -> Result { let options = crate::Options::default(); use std::convert::TryFrom; - let tla_file = TlaFile::try_from(tla_file)?; - let tla_config_file = TlaConfigFile::try_from(tla_config_file)?; + let tla_file = TlaFile::try_from(tla_file_path)?; + let tla_config_file = TlaConfigFile::try_from(tla_config_file_path)?; let tla_trace = crate::module::Tlc::test(tla_file, tla_config_file, &options)?; tracing::debug!("Tlc::test output {}", tla_trace); - save_tla_trace(tla_trace) + write_tla_trace_to_file(tla_trace) } } #[allow(clippy::unnecessary_wraps)] -fn generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result { +fn json_generated_test_list(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result { let json_array_entry = |tla_file: TlaFile, tla_config_file: TlaConfigFile| { json!({ "tla_file": format!("{}", tla_file), @@ -206,7 +209,7 @@ fn generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result Result { +fn write_tla_trace_to_file(tla_trace: TlaTrace) -> Result { let path = Path::new("trace.tla").to_path_buf(); std::fs::write(&path, format!("{}", tla_trace))?; Ok(json!({ @@ -214,7 +217,7 @@ fn save_tla_trace(tla_trace: TlaTrace) -> Result { })) } -fn save_json_trace(json_trace: JsonTrace) -> Result { +fn write_json_trace_to_file(json_trace: JsonTrace) -> Result { let path = Path::new("trace.json").to_path_buf(); std::fs::write(&path, format!("{}", json_trace))?; Ok(json!({ diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs index cc1aa839..b3a4b4e5 100644 --- a/modelator/src/lib.rs +++ b/modelator/src/lib.rs @@ -76,15 +76,15 @@ use tempfile::tempdir; /// # Examples /// /// ``` -/// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; -/// let tla_config_file = "tests/integration/tla/Numbers.cfg"; +/// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla"; +/// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; /// let options = modelator::Options::default(); -/// let traces = modelator::traces(tla_tests_file, tla_config_file, &options).unwrap(); +/// let traces = modelator::traces(tla_tests_file_path, tla_config_file_path, &options).unwrap(); /// println!("{:?}", traces); /// ``` pub fn traces>( - tla_tests_file: P, - tla_config_file: P, + tla_tests_file_path: P, + tla_config_file_path: P, options: &Options, ) -> Result, Error> { // setup modelator @@ -92,8 +92,8 @@ pub fn traces>( // create a temporary directory, and copy TLA+ files there let dir = tempdir()?; - let tla_tests_file = util::copy_files_into("tla", tla_tests_file, dir.path())?; - let tla_config_file = util::copy_files_into("cfg", tla_config_file, dir.path())?; + let tla_tests_file_path = util::copy_files_into("tla", tla_tests_file_path, dir.path())?; + let tla_config_file_path = util::copy_files_into("cfg", tla_config_file_path, dir.path())?; // save the current, and change to the temporary directory let current_dir = env::current_dir()?; @@ -101,8 +101,8 @@ pub fn traces>( // generate tla tests use std::convert::TryFrom; - let tla_tests_file = artifact::TlaFile::try_from(tla_tests_file)?; - let tla_config_file = artifact::TlaConfigFile::try_from(tla_config_file)?; + let tla_tests_file = artifact::TlaFile::try_from(tla_tests_file_path)?; + let tla_config_file = artifact::TlaConfigFile::try_from(tla_config_file_path)?; let tests = module::Tla::generate_tests(tla_tests_file, tla_config_file)?; // run the model checker configured on each tla test @@ -202,16 +202,16 @@ pub fn traces>( /// /// // To run your system against a TLA+ test, just point to the corresponding TLA+ files. /// fn test() { -/// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMinTest.tla"; -/// let tla_config_file = "tests/integration/tla/Numbers.cfg"; +/// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMinTest.tla"; +/// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; /// let options = modelator::Options::default(); /// let mut system = NumberSystem::default(); -/// assert!(run_tla_steps(tla_tests_file, tla_config_file, &options, &mut system).is_ok()); +/// assert!(run_tla_steps(tla_tests_file_path, tla_config_file_path, &options, &mut system).is_ok()); /// } /// ``` pub fn run_tla_steps( - tla_tests_file: P, - tla_config_file: P, + tla_tests_file_path: P, + tla_config_file_path: P, options: &Options, system: &mut System, ) -> Result<(), TestError> @@ -220,7 +220,8 @@ where System: StepRunner + Debug + Clone, Step: DeserializeOwned + Debug + Clone, { - let traces = traces(tla_tests_file, tla_config_file, options).map_err(TestError::Modelator)?; + let traces = + traces(tla_tests_file_path, tla_config_file_path, options).map_err(TestError::Modelator)?; for trace in traces { system.run(trace)?; } @@ -301,8 +302,8 @@ where /// /// // To run your system against a TLA+ test, just point to the corresponding TLA+ files. /// fn main() { -/// let tla_tests_file = "tests/integration/tla/NumbersAMaxBMaxTest.tla"; -/// let tla_config_file = "tests/integration/tla/Numbers.cfg"; +/// let tla_tests_file_path = "tests/integration/tla/NumbersAMaxBMaxTest.tla"; +/// let tla_config_file_path = "tests/integration/tla/Numbers.cfg"; /// let options = modelator::Options::default(); /// /// // We create a system under test @@ -315,7 +316,7 @@ where /// .with_action::(); /// /// // run your system against the events produced from TLA+ tests. -/// let result = run_tla_events(tla_tests_file, tla_config_file, &options, &mut system, &mut runner); +/// let result = run_tla_events(tla_tests_file_path, tla_config_file_path, &options, &mut system, &mut runner); /// // At each step of a test, the state of your system is being checked /// // against the state that the TLA+ model expects /// assert!(result.is_ok()); @@ -329,8 +330,8 @@ where // #[allow(clippy::needless_doctest_main)] #[allow(clippy::needless_doctest_main)] pub fn run_tla_events( - tla_tests_file: P, - tla_config_file: P, + tla_tests_file_path: P, + tla_config_file_path: P, options: &Options, system: &mut System, runner: &mut event::EventRunner, @@ -339,7 +340,8 @@ where P: AsRef, System: Debug + Default, { - let traces = traces(tla_tests_file, tla_config_file, options).map_err(TestError::Modelator)?; + let traces = + traces(tla_tests_file_path, tla_config_file_path, options).map_err(TestError::Modelator)?; for trace in traces { let events: EventStream = trace.clone().into(); runner diff --git a/modelator/src/module/apalache/mod.rs b/modelator/src/module/apalache/mod.rs index b2c2d64a..d1f4c948 100644 --- a/modelator/src/module/apalache/mod.rs +++ b/modelator/src/module/apalache/mod.rs @@ -41,6 +41,8 @@ impl Apalache { tla_config_file: TlaConfigFile, options: &Options, ) -> Result { + // TODO: this method currently just uses the paths of the files so no need for whole artifact objects! + tracing::debug!( "Apalache::test {} {} {:?}", tla_file, @@ -102,15 +104,13 @@ impl Apalache { tracing::debug!("Apalache::parse {} {:?}", tla_file, options); // compute the directory in which the tla file is stored - let mut tla_dir = tla_file.path().clone(); + let mut tla_dir = tla_file.path().to_path_buf(); assert!(tla_dir.pop()); - // compute tla module name: it's okay to unwrap as we have already - // verified that the file exists - let tla_module_name = tla_file.tla_module_name().unwrap(); + let tla_file_name = tla_file.file_name(); // compute the output tla file - let tla_parsed_file = tla_dir.join(format!("{}Parsed.tla", tla_module_name)); + let tla_parsed_file = tla_dir.join(format!("{}Parsed.tla", tla_file_name)); // create apalache parse command let cmd = parse_cmd(tla_file.path(), &tla_parsed_file, options); @@ -141,6 +141,7 @@ fn run_apalache(mut cmd: Command, options: &Options) -> Result { // apalache writes all its output to the stdout // save apalache log + //TODO: probably better to return the log in memory and write it somewhere else std::fs::write(&options.model_checker_options.log, &stdout)?; // check if a failure has occurred @@ -201,6 +202,11 @@ fn apalache_cmd_start>(tla_file: P, options: &Options) -> Command let mut cmd = Command::new("java"); + cmd.env( + "JAVA_HOME", + "/Library/Java/JavaVirtualMachines/zulu-16.jdk/Contents/Home", + ); + // compute the directory where the tla file is, so that it can be added as // a tla library if let Some(tla_file_dir) = tla_file.as_ref().parent() { diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs index c99a62d7..b6d8a291 100644 --- a/modelator/src/module/tla/mod.rs +++ b/modelator/src/module/tla/mod.rs @@ -69,15 +69,19 @@ impl Tla { tracing::debug!("Tla::generate_tests {} {}", tla_tests_file, tla_config_file); // compute the directory in which the tla tests file is stored - let mut tla_tests_dir = tla_tests_file.path().clone(); - assert!(tla_tests_dir.pop()); + let mut tla_tests_file_dir = tla_tests_file.path().to_path_buf(); + assert!(tla_tests_file_dir.pop()); - // compute tla tests module name: it's safe to unwrap because we have - // already checked that the tests file is indeed a file - let tla_tests_module_name = tla_tests_file.tla_module_name().unwrap(); + let tla_tests_file_name = tla_tests_file.file_name(); // retrieve test names from tla tests file - let test_names = extract_test_names(&tla_tests_file)?; + let test_names = extract_test_names(tla_tests_file.content())?; + + tracing::debug!( + "test names extracted from {}:\n{:?}", + tla_tests_file, + test_names + ); // check if no test was found if test_names.is_empty() { @@ -89,8 +93,8 @@ impl Tla { .into_iter() .map(|test_name| { generate_test( - &tla_tests_dir, - &tla_tests_module_name, + &tla_tests_file_dir, + &tla_tests_file_name, &test_name, &tla_config_file, ) @@ -99,9 +103,9 @@ impl Tla { } } -fn extract_test_names(tla_test_file: &TlaFile) -> Result, Error> { - let content = std::fs::read_to_string(tla_test_file.path())?; - let test_names = content +fn extract_test_names(tla_tests_file_content: &str) -> Result, Error> { + //TODO: Error is never returned here so why type it + let test_names = tla_tests_file_content .lines() .filter_map(|line| { // take the first element in the split @@ -121,39 +125,39 @@ fn extract_test_names(tla_test_file: &TlaFile) -> Result, Error> { } }) .collect(); - tracing::debug!( - "test names extracted from {}:\n{:?}", - tla_test_file, - test_names - ); + Ok(test_names) } fn generate_test( - tla_tests_dir: &Path, - tla_tests_module_name: &str, + tla_tests_file_dir: &Path, + tla_tests_file_name: &str, test_name: &str, tla_config_file: &TlaConfigFile, ) -> Result<(TlaFile, TlaConfigFile), Error> { - let test_module_name = format!("{}_{}", tla_tests_module_name, test_name); - let invariant = format!("{}Neg", test_name); + // TODO: it would be better to separate logic from IO steps + // split into 2 funs and also use artifacts: + // instead of writing the files and reading artifacts from them, + // create the artifacts and write the files + let test_module_name = format!("{}_{}", tla_tests_file_name, test_name); + let negated_test_name = format!("{}Neg", test_name); // create tla module where the test is negated - let test_module = genereate_test_module( - tla_tests_module_name, - test_name, + let test_module = generate_test_module( &test_module_name, - &invariant, + tla_tests_file_name, + &negated_test_name, + test_name, ); // create test config with negated test as an invariant - let test_config = generate_test_config(tla_config_file, &invariant)?; + let test_config = generate_test_config(tla_config_file, &negated_test_name)?; // write test module to test module file - let test_module_file = tla_tests_dir.join(format!("{}.tla", test_module_name)); + let test_module_file = tla_tests_file_dir.join(format!("{}.tla", test_module_name)); std::fs::write(&test_module_file, test_module)?; // write test config to test config file - let test_config_file = tla_tests_dir.join(format!("{}.cfg", test_module_name)); + let test_config_file = tla_tests_file_dir.join(format!("{}.cfg", test_module_name)); std::fs::write(&test_config_file, test_config)?; // create tla file and tla config file @@ -163,11 +167,11 @@ fn generate_test( Ok((test_module_file, test_config_file)) } -fn genereate_test_module( - tla_tests_module_name: &str, +fn generate_test_module( + module_name: &str, + file_to_extend: &str, + negated_test_name: &str, test_name: &str, - test_module_name: &str, - invariant: &str, ) -> String { format!( r#" @@ -179,7 +183,7 @@ EXTENDS {} =============================== "#, - test_module_name, tla_tests_module_name, invariant, test_name + module_name, file_to_extend, negated_test_name, test_name ) } diff --git a/modelator/src/module/tlc/mod.rs b/modelator/src/module/tlc/mod.rs index 7182aa60..a275df0c 100644 --- a/modelator/src/module/tlc/mod.rs +++ b/modelator/src/module/tlc/mod.rs @@ -69,6 +69,7 @@ impl Tlc { // occurred // save tlc log + //TODO: probably better to return the log in memory and write it somewhere else std::fs::write(&options.model_checker_options.log, &stdout)?; tracing::debug!( "TLC log written to {}", @@ -76,6 +77,8 @@ impl Tlc { ); // convert tlc output to traces + // TODO: make the logic here mirror the better-implemented Apalache module which returns + // stdout for post-proccesing let mut traces = output::parse(stdout, &options.model_checker_options)?; // check if no trace was found diff --git a/z_notes.md b/z_notes.md new file mode 100644 index 00000000..d81f9812 --- /dev/null +++ b/z_notes.md @@ -0,0 +1,35 @@ +# + +# Commands + +``` +apalache + # Will give an error if not using zulu for m1 + parse + # generated a Parsed.tla file, this is just a wrapper around Apalaches parse functionality + # (used to check spec is syntactically correct) + test + # think this is the same as for _tlc_ cmd but mine panicked for the example I gave it +tla + generate-tests + # takes a .tla and .cfg file for the MBT _tests_, which extend the model. + # The tests are just assertions. + # Converts (each test within) into a form which is directly runnable by TLC/(apalache?) + # named something like + # _.tla + # _.cfg + tla-trace-to-json-trace + # converts .tla traces to json traces +tlc + test + # takes a .tla and .cfg file as generated using 'tla generate-tests <.tla> <.cfg> + # and runs it using tlc to get a .tla trace for the given test +``` + +# TODO: + +Make subprocesses based on `Command` more flexible (env args) + +# Other notes + +I added cmd.env pointing to Java zulu to help me debug From e7a6b7d5ae5603239fb050e7ee0107a2554ae296 Mon Sep 17 00:00:00 2001 From: Daniel Tisdall Date: Tue, 24 Aug 2021 14:03:01 +0100 Subject: [PATCH 2/4] Removes devenv files --- .vscode/launch.json | 21 -------------- .vscode/settings.json | 42 ---------------------------- .vscode/tasks.json | 4 --- modelator/src/module/apalache/mod.rs | 5 ---- z_notes.md | 35 ----------------------- 5 files changed, 107 deletions(-) delete mode 100644 .vscode/launch.json delete mode 100644 .vscode/settings.json delete mode 100644 .vscode/tasks.json delete mode 100644 z_notes.md diff --git a/.vscode/launch.json b/.vscode/launch.json deleted file mode 100644 index 1afa347a..00000000 --- a/.vscode/launch.json +++ /dev/null @@ -1,21 +0,0 @@ -{ - "configurations": [ - { - "name": "modelator debug build", - "type": "lldb", - "request": "launch", - "program": "${workspaceRoot}/target/debug/modelator", - "args": [ - "apalache", - "test", - "/Users/danwt/documents/sandbox-tla/mainTests_MyVarTest.tla", - "/Users/danwt/documents/sandbox-tla/mainTests_MyVarTest.cfg", - // "tla", - // "generate-tests", - // "main.tla", - // "main.cfg" - ], - "cwd": "${workspaceRoot}", - } - ], -} \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index e838a14a..00000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,42 +0,0 @@ -{ - "editor.formatOnSave": true, - "files.exclude": { - "LICENSE": true, - "**/.git": true, - "**/.DS_Store": true, - "cargo.lock": true, - "**/.modelator": true, - "mc.log": true, - "log*.smt": true, - "MC.out": true, - "profile-rules.txt": true, - "trace.tla": true, - "detailed.log": true, - "counterexample.json": true, - "counterexample.tla": true, - }, - "git.ignoreLimitWarning": true, - "todohighlight.keywords": [ - { - "text": "NOTE:", - "color": "white", - "backgroundColor": "rgb(111, 189, 133)" - }, - { - "text": "PARAM!", - "color": "white", - "backgroundColor": "rgb(182, 90, 199)" - }, - { - "text": "HACK:", - "color": "white", - "backgroundColor": "rgb(199, 96, 0)" - }, - { - "text": "NEXT:", - "color": "white", - "backgroundColor": "rgb(83,158,230)" - }, - ], - "cSpell.diagnosticLevel": "Hint", -} \ No newline at end of file diff --git a/.vscode/tasks.json b/.vscode/tasks.json deleted file mode 100644 index 2f24d448..00000000 --- a/.vscode/tasks.json +++ /dev/null @@ -1,4 +0,0 @@ -{ - "version": "2.0.0", - "tasks": [] -} \ No newline at end of file diff --git a/modelator/src/module/apalache/mod.rs b/modelator/src/module/apalache/mod.rs index d1f4c948..4b83f8f1 100644 --- a/modelator/src/module/apalache/mod.rs +++ b/modelator/src/module/apalache/mod.rs @@ -202,11 +202,6 @@ fn apalache_cmd_start>(tla_file: P, options: &Options) -> Command let mut cmd = Command::new("java"); - cmd.env( - "JAVA_HOME", - "/Library/Java/JavaVirtualMachines/zulu-16.jdk/Contents/Home", - ); - // compute the directory where the tla file is, so that it can be added as // a tla library if let Some(tla_file_dir) = tla_file.as_ref().parent() { diff --git a/z_notes.md b/z_notes.md deleted file mode 100644 index d81f9812..00000000 --- a/z_notes.md +++ /dev/null @@ -1,35 +0,0 @@ -# - -# Commands - -``` -apalache - # Will give an error if not using zulu for m1 - parse - # generated a Parsed.tla file, this is just a wrapper around Apalaches parse functionality - # (used to check spec is syntactically correct) - test - # think this is the same as for _tlc_ cmd but mine panicked for the example I gave it -tla - generate-tests - # takes a .tla and .cfg file for the MBT _tests_, which extend the model. - # The tests are just assertions. - # Converts (each test within) into a form which is directly runnable by TLC/(apalache?) - # named something like - # _.tla - # _.cfg - tla-trace-to-json-trace - # converts .tla traces to json traces -tlc - test - # takes a .tla and .cfg file as generated using 'tla generate-tests <.tla> <.cfg> - # and runs it using tlc to get a .tla trace for the given test -``` - -# TODO: - -Make subprocesses based on `Command` more flexible (env args) - -# Other notes - -I added cmd.env pointing to Java zulu to help me debug From 7bf7906fd05e03fbd7e0ec40be8b15875624c0f0 Mon Sep 17 00:00:00 2001 From: Daniel Tisdall Date: Tue, 24 Aug 2021 14:28:42 +0100 Subject: [PATCH 3/4] Clippy fixes --- modelator/src/artifact/artifact.rs | 3 +++ modelator/src/artifact/tla_file.rs | 2 +- modelator/src/artifact/tla_trace.rs | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/modelator/src/artifact/artifact.rs b/modelator/src/artifact/artifact.rs index 05fae350..b24a2c29 100644 --- a/modelator/src/artifact/artifact.rs +++ b/modelator/src/artifact/artifact.rs @@ -12,7 +12,10 @@ where + for<'a> TryFrom<&'a Path, Error = crate::Error> + TryFrom, { + /// Returns a string representation. fn as_string(&self) -> &str; + + /// Tries to write the contents to path. fn try_write_to_file(&self, path: &Path) -> Result<(), Error>; } diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs index 8a385e72..aeb406e8 100644 --- a/modelator/src/artifact/tla_file.rs +++ b/modelator/src/artifact/tla_file.rs @@ -101,7 +101,7 @@ impl Artifact for TlaFile { fn as_string(&self) -> &str { todo!() } - fn try_write_to_file(&self, path: &Path) -> Result<(), Error> { + fn try_write_to_file(&self, _path: &Path) -> Result<(), Error> { todo!() } } diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs index ba253678..016f9c07 100644 --- a/modelator/src/artifact/tla_trace.rs +++ b/modelator/src/artifact/tla_trace.rs @@ -133,7 +133,7 @@ impl FromStr for TlaTrace { fn from_str(tla_trace: &str) -> Result { let tla_trace = remove_tla_comments(tla_trace); - let tla: TlaTraceFileContent = parse_tla_trace_file_contents(&tla_trace).unwrap().1; + let tla: TlaTraceFileContent<'_> = parse_tla_trace_file_contents(&tla_trace).unwrap().1; let mut states: Vec<(usize, &str)> = tla .operators From efad445a562c33fc4623e7e04e6906a3ee4b914f Mon Sep 17 00:00:00 2001 From: Daniel Tisdall Date: Tue, 24 Aug 2021 14:36:38 +0100 Subject: [PATCH 4/4] Clippy * --- modelator/src/artifact/artifact.rs | 26 -------------------------- modelator/src/artifact/mod.rs | 29 +++++++++++++++++++++++++++-- modelator/src/artifact/tla_file.rs | 2 +- modelator/src/module/tla/mod.rs | 2 +- 4 files changed, 29 insertions(+), 30 deletions(-) delete mode 100644 modelator/src/artifact/artifact.rs diff --git a/modelator/src/artifact/artifact.rs b/modelator/src/artifact/artifact.rs deleted file mode 100644 index b24a2c29..00000000 --- a/modelator/src/artifact/artifact.rs +++ /dev/null @@ -1,26 +0,0 @@ -use crate::Error; -use std::convert::TryFrom; -use std::path::{Path, PathBuf}; -use std::str; - -/// TODO: -pub trait Artifact -where - Self: std::fmt::Display - + for<'a> TryFrom<&'a str, Error = crate::Error> - + TryFrom - + for<'a> TryFrom<&'a Path, Error = crate::Error> - + TryFrom, -{ - /// Returns a string representation. - fn as_string(&self) -> &str; - - /// Tries to write the contents to path. - fn try_write_to_file(&self, path: &Path) -> Result<(), Error>; -} - -// impl std::fmt::Debug for dyn Artifact { -// fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { -// todo!() -// } -// } diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs index 3b02c14b..283186b8 100644 --- a/modelator/src/artifact/mod.rs +++ b/modelator/src/artifact/mod.rs @@ -1,11 +1,36 @@ -pub(crate) mod artifact; pub(crate) mod json_trace; pub(crate) mod tla_cfg_file; pub(crate) mod tla_file; pub(crate) mod tla_trace; +use crate::Error; +use std::convert::TryFrom; +use std::path::{Path, PathBuf}; +use std::str; + +/// TODO: +pub trait Artifact +where + Self: std::fmt::Display + + for<'a> TryFrom<&'a str, Error = crate::Error> + + TryFrom + + for<'a> TryFrom<&'a Path, Error = crate::Error> + + TryFrom, +{ + /// Returns a string representation. + fn as_string(&self) -> &str; + + /// Tries to write the contents to path. + fn try_write_to_file(&self, path: &Path) -> Result<(), Error>; +} + +// impl std::fmt::Debug for dyn Artifact { +// fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { +// todo!() +// } +// } + // Re-exports. -pub use artifact::Artifact; pub use json_trace::JsonTrace; pub use tla_cfg_file::TlaConfigFile; pub use tla_file::TlaFile; diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs index aeb406e8..13615597 100644 --- a/modelator/src/artifact/tla_file.rs +++ b/modelator/src/artifact/tla_file.rs @@ -13,7 +13,7 @@ pub struct TlaFile { } /// TODO: -fn tla_file_name(path: &PathBuf) -> Option { +fn tla_file_name(path: &Path) -> Option { if path.is_file() { path.file_name().map(|file_name| { file_name diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs index b6d8a291..020b299d 100644 --- a/modelator/src/module/tla/mod.rs +++ b/modelator/src/module/tla/mod.rs @@ -94,7 +94,7 @@ impl Tla { .map(|test_name| { generate_test( &tla_tests_file_dir, - &tla_tests_file_name, + tla_tests_file_name, &test_name, &tla_config_file, )