Refactor implementation introducing the concept of modules and artifacts

modelator/src/artifact/json_trace.rs

@@ -0,0 +1,19 @@
+use serde_json::Value as JsonValue;
+pub struct JsonTrace {
+    states: Vec<JsonValue>,
+}
+
+impl IntoIterator for JsonTrace {
+    type Item = JsonValue;
+    type IntoIter = std::vec::IntoIter<Self::Item>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.states.into_iter()
+    }
+}
+
+impl From<Vec<JsonValue>> for JsonTrace {
+    fn from(states: Vec<JsonValue>) -> Self {
+        Self { states }
+    }
+}

modelator/src/artifact/mod.rs

@@ -0,0 +1,19 @@
+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 json_trace::JsonTrace;
+pub use tla_cfg_file::TlaConfigFile;
+pub use tla_file::TlaFile;
+pub use tla_trace::TlaTrace;
+
+use serde::de::DeserializeOwned;
+use serde::Serialize;
+
+/// Artifacts should be able to serialized (into a string/file) and deserialized
+/// (from string/file).
+pub trait Artifact: Serialize + DeserializeOwned {}
+
+// TODO: assert that all artifacts implement the above trait.

modelator/src/artifact/tla_cfg_file.rs

@@ -0,0 +1,32 @@
+use std::path::{Path, PathBuf};
+
+pub struct TlaConfigFile {
+    path: PathBuf,
+}
+
+impl TlaConfigFile {
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
+        Self {
+            path: path.as_ref().to_path_buf(),
+        }
+    }
+
+    pub(crate) fn path(&self) -> &PathBuf {
+        &self.path
+    }
+}
+
+impl<P> From<P> for TlaConfigFile
+where
+    P: AsRef<Path>,
+{
+    fn from(path: P) -> Self {
+        Self::new(path.as_ref().to_path_buf())
+    }
+}
+
+impl std::fmt::Display for TlaConfigFile {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self.path)
+    }
+}

modelator/src/artifact/tla_file.rs

@@ -0,0 +1,47 @@
+use std::path::{Path, PathBuf};
+
+pub struct TlaFile {
+    path: PathBuf,
+}
+
+impl TlaFile {
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
+        Self {
+            path: path.as_ref().to_path_buf(),
+        }
+    }
+
+    pub(crate) fn path(&self) -> &PathBuf {
+        &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
+        }
+    }
+}
+
+impl<P> From<P> for TlaFile
+where
+    P: AsRef<Path>,
+{
+    fn from(path: P) -> Self {
+        Self::new(path.as_ref().to_path_buf())
+    }
+}
+
+impl std::fmt::Display for TlaFile {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self.path)
+    }
+}

modelator/src/artifact/tla_trace.rs

@@ -0,0 +1,38 @@
+pub(crate) type TlaState = String;
+
+#[derive(Debug)]
+pub struct TlaTrace {
+    states: Vec<TlaState>,
+}
+
+impl TlaTrace {
+    pub(crate) fn new() -> Self {
+        Self { states: Vec::new() }
+    }
+
+    pub(crate) fn add(&mut self, state: TlaState) {
+        self.states.push(state);
+    }
+
+    pub(crate) fn is_empty(&self) -> bool {
+        self.states.is_empty()
+    }
+}
+
+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 + 1, state)?;
+        }
+        Ok(())
+    }
+}

modelator/src/error.rs

@@ -1,4 +1,3 @@
-use crate::Artifact;
 use std::fmt::Debug;
 use thiserror::Error;
 
@@ -33,13 +32,6 @@ pub enum Error {
 
     #[error("Nom error: {0}")]
     Nom(String),
-
-    #[error("Error while running method {module}.{method}")]
-    ModuleRun {
-        module: String,
-        method: String,
-        errors: Vec<Box<dyn Artifact>>,
-    },
 }
 
 #[derive(Error, Debug)]