Artifact interfaces for tla config file json trace tla trace (#71)

* Adds some notes-to-self

* notes

* Gignores Dans vscode

* Adds trace.tla and log.mc to .gitignore

* Adds apalache debug launcher

* Adds my own notes

* settings.json

* note

* Adds artifacts trait

* Adds basic artifact declarations

* Clarifies method names in mod.rs

* Adds artifact trait impl scaffold to .tla and .cfg reprs.

* Clarifies naming of internal struct in tla_trace

* Clarifies path/file var naming in lib.rs traces

* Reworks Artifact trait to use TryFrom super traits

* Scaffolds Artifact impl for tla_file

* Pre TlaFile explicit pathing teardown

* Renames tla_module_name -> tla_file_name

* TlaFile now saves content and filename internally

* Partially refactors the use of TlaFile in tla module

* Clarifies file path var names in cli

* Removes todo in tla module generate_test

* Adds todos to Apalache and Tlc mod.rs's

* Merge main

* Clean up related to TlaConfigFile

* Declares Artifact impl for TlaTrace

* Encapsulates a file write for TlaTrace

* Impl Artifact for JsonTrace, encapsulating 1 file write

* Devnv

* Removes .vscode

Co-authored-by: Daniel Tisdall <daniel@informal.systems>

modelator/src/artifact/json_trace.rs

@@ -1,7 +1,9 @@
 use super::Artifact;
 use crate::Error;
 use serde_json::Value as JsonValue;
-use std::path::Path;
+use std::convert::TryFrom;
+use std::path::{Path, PathBuf};
+use std::str::FromStr;
 
 /// `modelator`'s artifact containing a test trace encoded as JSON.
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -37,3 +39,44 @@ impl std::fmt::Display for JsonTrace {
         write!(f, "{:#}", self.states)
     }
 }
+
+impl TryFrom<&str> for JsonTrace {
+    type Error = crate::Error;
+    fn try_from(_path: &str) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<String> for JsonTrace {
+    type Error = crate::Error;
+    fn try_from(_path: String) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<&Path> for JsonTrace {
+    type Error = crate::Error;
+    fn try_from(_path: &Path) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<PathBuf> for JsonTrace {
+    type Error = crate::Error;
+    fn try_from(_path: PathBuf) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl Artifact for JsonTrace {
+    fn as_string(&self) -> &str {
+        todo!()
+    }
+    fn try_write_to_file(&self, path: &Path) -> Result<(), Error> {
+        Ok(std::fs::write(&path, format!("{}", self))?)
+    }
+}

modelator/src/artifact/tla_cfg_file.rs

@@ -1,26 +1,34 @@
 use super::Artifact;
 use crate::Error;
 use std::convert::TryFrom;
+use std::fs;
 use std::path::{Path, PathBuf};
 
 /// `modelator`'s artifact representing a TLA+ config file containing the TLA+
 /// model `CONSTANT`s and `INIT` and `NEXT` predicates.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct TlaConfigFile {
     path: PathBuf,
+    content: String,
 }
 
 impl TlaConfigFile {
     pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
         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)?;
+        Ok(Self { path, content })
     }
 
     /// Returns the path to the TLA+ config file.
     pub fn path(&self) -> &PathBuf {
         &self.path
     }
+
+    /// Returns the content of the TLA+ config file.
+    pub fn content(&self) -> &str {
+        &self.content
+    }
 }
 
 // TODO: replace the following `TryFrom` implementations with one with generic
@@ -59,3 +67,12 @@ impl std::fmt::Display for TlaConfigFile {
         write!(f, "{}", crate::util::absolute_path(&self.path))
     }
 }
+
+impl Artifact for TlaConfigFile {
+    fn as_string(&self) -> &str {
+        todo!()
+    }
+    fn try_write_to_file(&self, _path: &Path) -> Result<(), Error> {
+        todo!()
+    }
+}

modelator/src/artifact/tla_trace.rs

@@ -1,5 +1,8 @@
 use super::Artifact;
 use crate::Error;
+use std::convert::TryFrom;
+use std::fs;
+use std::path::{Path, PathBuf};
 use std::str::FromStr;
 
 use nom::{
@@ -34,6 +37,65 @@ impl TlaTrace {
     }
 }
 
+impl IntoIterator for TlaTrace {
+    type Item = TlaState;
+    type IntoIter = std::vec::IntoIter<Self::Item>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.states.into_iter()
+    }
+}
+
+impl std::fmt::Display for TlaTrace {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        for (index, state) in self.states.iter().enumerate() {
+            write!(f, "State{} ==\n{}", index, state)?;
+        }
+        Ok(())
+    }
+}
+
+impl TryFrom<&str> for TlaTrace {
+    type Error = crate::Error;
+    fn try_from(_path: &str) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<String> for TlaTrace {
+    type Error = crate::Error;
+    fn try_from(_path: String) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<&Path> for TlaTrace {
+    type Error = crate::Error;
+    fn try_from(_path: &Path) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl TryFrom<PathBuf> for TlaTrace {
+    type Error = crate::Error;
+    fn try_from(_path: PathBuf) -> Result<Self, Self::Error> {
+        // Self::new(path)
+        todo!();
+    }
+}
+
+impl Artifact for TlaTrace {
+    fn as_string(&self) -> &str {
+        todo!()
+    }
+    fn try_write_to_file(&self, path: &Path) -> Result<(), Error> {
+        Ok(std::fs::write(&path, format!("{}", self))?)
+    }
+}
+
 fn tla_single_line_comment(i: &str) -> IResult<&str, &str> {
     recognize(pair(tag("\\*"), is_not("\n\r")))(i)
 }
@@ -158,21 +220,3 @@ impl FromStr for TlaTrace {
         Ok(trace)
     }
 }
-
-impl IntoIterator for TlaTrace {
-    type Item = TlaState;
-    type IntoIter = std::vec::IntoIter<Self::Item>;
-
-    fn into_iter(self) -> Self::IntoIter {
-        self.states.into_iter()
-    }
-}
-
-impl std::fmt::Display for TlaTrace {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        for (index, state) in self.states.iter().enumerate() {
-            write!(f, "State{} ==\n{}", index, state)?;
-        }
-        Ok(())
-    }
-}

modelator/src/cache/tla_trace.rs

@@ -18,6 +18,7 @@ impl TlaTraceCache {
     }
 
     pub(crate) fn insert(&mut self, key: String, tla_trace: &TlaTrace) -> Result<(), Error> {
+        // TODO: this to_string is Display trait's, but maybe we want our own repr.
         let value = tla_trace.to_string();
         self.cache.insert(key, value)
     }
@@ -38,7 +39,7 @@ impl TlaTraceCache {
             // compute full path
             .map(|filename| tla_dir.join(filename))
             // also hash the tla config file
-            .chain(std::iter::once(tla_config_file.path().clone()))
+            .chain(std::iter::once(tla_config_file.path().to_path_buf()))
             .map(|path| crate::util::absolute_path(&path))
             // sort files so that the hash is deterministic
             .collect();

modelator/src/cli/mod.rs

@@ -1,7 +1,7 @@
 // CLI output.
 pub(crate) mod output;
 
-use crate::artifact::{JsonTrace, TlaConfigFile, TlaFile, TlaTrace};
+use crate::artifact::{Artifact, JsonTrace, TlaConfigFile, TlaFile, TlaTrace};
 use crate::Error;
 use clap::{AppSettings, Clap, Subcommand};
 use serde_json::{json, Value as JsonValue};
@@ -121,7 +121,7 @@ impl TlaMethods {
         let tests = crate::module::Tla::generate_tests(tla_file, tla_config_file)?;
         tracing::debug!("Tla::generate_tests output {:#?}", tests);
 
-        json_generated_test_list(tests)
+        json_list_generated_tests(tests)
     }
 
     fn tla_trace_to_json_trace(tla_trace_file: String) -> Result<JsonValue, Error> {
@@ -195,7 +195,7 @@ impl TlcMethods {
 }
 
 #[allow(clippy::unnecessary_wraps)]
-fn json_generated_test_list(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<JsonValue, Error> {
+fn json_list_generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<JsonValue, Error> {
     let json_array_entry = |tla_file: TlaFile, tla_config_file: TlaConfigFile| {
         json!({
             "tla_file": format!("{}", tla_file),
@@ -210,16 +210,18 @@ fn json_generated_test_list(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<Json
 }
 
 fn write_tla_trace_to_file(tla_trace: TlaTrace) -> Result<JsonValue, Error> {
-    let path = Path::new("trace.tla").to_path_buf();
-    std::fs::write(&path, format!("{}", tla_trace))?;
+    // TODO: hardcoded!
+    let path = Path::new("trace.tla");
+    tla_trace.try_write_to_file(path)?;
     Ok(json!({
         "tla_trace_file": crate::util::absolute_path(&path),
     }))
 }
 
 fn write_json_trace_to_file(json_trace: JsonTrace) -> Result<JsonValue, Error> {
-    let path = Path::new("trace.json").to_path_buf();
-    std::fs::write(&path, format!("{}", json_trace))?;
+    // TODO: hardcoded!
+    let path = Path::new("trace.json");
+    json_trace.try_write_to_file(path)?;
     Ok(json!({
         "json_trace_file": crate::util::absolute_path(&path),
     }))

modelator/src/module/apalache/mod.rs

@@ -160,13 +160,13 @@ fn run_apalache(mut cmd: Command, options: &Options) -> Result<String, Error> {
     }
 }
 
-fn test_cmd<P: AsRef<Path>>(tla_file: P, tla_config_file: P, options: &Options) -> Command {
+fn test_cmd<P: AsRef<Path>>(tla_file: P, tla_config_file_path: P, options: &Options) -> Command {
     let mut cmd = apalache_cmd_start(&tla_file, options);
     cmd.arg("check")
         // set tla config file
         .arg(format!(
             "--config={}",
-            tla_config_file.as_ref().to_string_lossy()
+            tla_config_file_path.as_ref().to_string_lossy()
         ))
         // set tla file
         .arg(tla_file.as_ref());

modelator/src/module/tla/mod.rs

@@ -150,7 +150,7 @@ fn generate_test(
         test_name,
     );
     // create test config with negated test as an invariant
-    let test_config = generate_test_config(tla_config_file, &negated_test_name)?;
+    let test_config = generate_test_config(tla_config_file.content(), &negated_test_name)?;
 
     // write test module to test module file
     let test_module_file = tla_tests_file_dir.join(format!("{}.tla", test_module_name));
@@ -187,13 +187,12 @@ EXTENDS {}
     )
 }
 
-fn generate_test_config(tla_config_file: &TlaConfigFile, invariant: &str) -> Result<String, Error> {
-    let tla_config = std::fs::read_to_string(tla_config_file.path())?;
+fn generate_test_config(tla_config_file_content: &str, invariant: &str) -> Result<String, Error> {
     Ok(format!(
         r#"
 {}
 INVARIANT {}
 "#,
-        tla_config, invariant
+        tla_config_file_content, invariant
     ))
 }

modelator/src/module/tlc/mod.rs

@@ -112,7 +112,7 @@ impl Tlc {
     }
 }
 
-fn test_cmd<P: AsRef<Path>>(tla_file: P, tla_config_file: P, options: &Options) -> Command {
+fn test_cmd<P: AsRef<Path>>(tla_file: P, tla_config_file_path: P, options: &Options) -> Command {
     let tla2tools = jar::Jar::Tla.path(&options.dir);
     let community_modules = jar::Jar::CommunityModules.path(&options.dir);
 
@@ -130,7 +130,7 @@ fn test_cmd<P: AsRef<Path>>(tla_file: P, tla_config_file: P, options: &Options)
         .arg(tla_file.as_ref())
         // set tla config file
         .arg("-config")
-        .arg(tla_config_file.as_ref())
+        .arg(tla_config_file_path.as_ref())
         // set "-tool" flag, which allows easier parsing of TLC's output
         .arg("-tool")
         // set the number of TLC's workers

modelator/src/module/tlc/output.rs

@@ -3,6 +3,7 @@ use crate::{Error, ModelCheckerOptions};
 
 use std::collections::HashMap;
 
+// TODO: don't need entire options object
 pub(crate) fn parse(output: String, options: &ModelCheckerOptions) -> Result<Vec<TlaTrace>, Error> {
     let mut parsed_output: HashMap<u8, HashMap<usize, Vec<String>>> = HashMap::new();