Reintroduces a simple Artifact trait which TlaFile implements. Begins cleanup of path assumptions.

.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

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)]

modelator/src/artifact/mod.rs

@@ -3,6 +3,33 @@ 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<String, Error = crate::Error>
+        + for<'a> TryFrom<&'a Path, Error = crate::Error>
+        + TryFrom<PathBuf, Error = crate::Error>,
+{
+    /// 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 json_trace::JsonTrace;
 pub use tla_cfg_file::TlaConfigFile;

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};

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: &Path) -> Option<String> {
+    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<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+    // pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+    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)?;
+        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<String> {
-        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!()
+    }
+}

modelator/src/artifact/tla_trace.rs

@@ -1,3 +1,4 @@
+use super::Artifact;
 use crate::Error;
 use std::str::FromStr;
 
@@ -67,21 +68,21 @@ 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("_"))),
         many0(alt((alphanumeric1, tag("_")))),
     ))(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<Self, Self::Err> {
         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

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)?

modelator/src/cli/mod.rs

@@ -111,14 +111,17 @@ impl TlaMethods {
         }
     }
 
-    fn generate_tests(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
+    fn generate_tests(
+        tla_file_path: String,
+        tla_config_file_path: String,
+    ) -> Result<JsonValue, Error> {
         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<JsonValue, Error> {
@@ -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<JsonValue, Error> {
+    fn test(tla_file_path: String, tla_config_file_path: String) -> Result<JsonValue, Error> {
         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<JsonValue, Error> {
@@ -179,20 +182,20 @@ impl TlcMethods {
         }
     }
 
-    fn test(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
+    fn test(tla_file_path: String, tla_config_file_path: String) -> Result<JsonValue, Error> {
         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<JsonValue, Error> {
+fn json_generated_test_list(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<JsonValue, Error> {
     let json_array_entry = |tla_file: TlaFile, tla_config_file: TlaConfigFile| {
         json!({
             "tla_file": format!("{}", tla_file),
@@ -206,15 +209,15 @@ fn generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<JsonValue, Er
     Ok(JsonValue::Array(json_array))
 }
 
-fn save_tla_trace(tla_trace: TlaTrace) -> Result<JsonValue, Error> {
+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))?;
     Ok(json!({
         "tla_trace_file": crate::util::absolute_path(&path),
     }))
 }
 
-fn save_json_trace(json_trace: JsonTrace) -> Result<JsonValue, Error> {
+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))?;
     Ok(json!({