From 759a87831e2d41cff77d3d2b35349f78cfbf9be7 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 12:24:37 +0100
Subject: [PATCH 1/9] Only keep the Artifact trait

---
 modelator/src/artifact.rs               | 39 ---------------
 modelator/src/artifact/json_trace.rs    |  0
 modelator/src/artifact/mod.rs           | 20 ++++++++
 modelator/src/artifact/model.rs         | 47 ------------------
 modelator/src/artifact/tla_file.rs      | 35 +++++++++++++
 modelator/src/artifact/tla_trace.rs     | 28 +++++++++++
 modelator/src/artifact/trace.rs         | 66 -------------------------
 modelator/src/error.rs                  |  8 ---
 modelator/src/{util => keep}/convert.rs |  0
 modelator/src/{ => keep}/module.rs      | 18 ++++++-
 modelator/src/lib.rs                    | 10 ++--
 modelator/src/util/mod.rs               |  1 -
 12 files changed, 103 insertions(+), 169 deletions(-)
 delete mode 100644 modelator/src/artifact.rs
 create mode 100644 modelator/src/artifact/json_trace.rs
 create mode 100644 modelator/src/artifact/mod.rs
 delete mode 100644 modelator/src/artifact/model.rs
 create mode 100644 modelator/src/artifact/tla_file.rs
 create mode 100644 modelator/src/artifact/tla_trace.rs
 delete mode 100644 modelator/src/artifact/trace.rs
 rename modelator/src/{util => keep}/convert.rs (100%)
 rename modelator/src/{ => keep}/module.rs (94%)
 delete mode 100644 modelator/src/util/mod.rs

diff --git a/modelator/src/artifact.rs b/modelator/src/artifact.rs
deleted file mode 100644
index 2a18c029..00000000
--- a/modelator/src/artifact.rs
+++ /dev/null
@@ -1,39 +0,0 @@
-use crate::error::Error;
-use serde::{Deserialize, Serialize};
-use std::{fmt, path::Path, str};
-
-pub mod model;
-pub mod trace;
-
-pub enum ArtifactFormat {
-    TLA,
-    JSON,
-    TLC,
-}
-
-#[derive(Debug, Deserialize, Serialize, PartialEq)]
-pub struct ArtifactManifest {
-    pub name: &'static str,
-    #[serde(rename = "type")]
-    pub typ: &'static str,
-}
-
-pub trait Artifact: fmt::Display {
-    fn name(&self) -> &'static str;
-    fn typ(&self) -> &'static str;
-    fn formats(&self) -> Vec<ArtifactFormat>;
-
-    fn from_string(s: &str) -> Result<Self, Error>
-    where
-        Self: Sized;
-    fn from_file(f: &Path) -> Result<Self, Error>
-    where
-        Self: Sized;
-    fn to_file(&self, f: &Path, format: ArtifactFormat) -> Result<(), Error>;
-}
-
-impl fmt::Debug for dyn Artifact {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        todo!()
-    }
-}
diff --git a/modelator/src/artifact/json_trace.rs b/modelator/src/artifact/json_trace.rs
new file mode 100644
index 00000000..e69de29b
diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs
new file mode 100644
index 00000000..00674f80
--- /dev/null
+++ b/modelator/src/artifact/mod.rs
@@ -0,0 +1,20 @@
+mod tla_file;
+mod tla_trace;
+mod json_trace;
+
+use crate::error::Error;
+use std::{path::Path, str};
+
+pub trait Artifact {
+    fn name(&self) -> &'static str;
+
+    fn to_file(&self, f: &Path) -> Result<(), Error>;
+
+    fn from_file(f: &Path) -> Result<Self, Error>
+    where
+        Self: Sized;
+
+    fn from_string(s: &str) -> Result<Self, Error>
+    where
+        Self: Sized;
+}
diff --git a/modelator/src/artifact/model.rs b/modelator/src/artifact/model.rs
deleted file mode 100644
index ff99db63..00000000
--- a/modelator/src/artifact/model.rs
+++ /dev/null
@@ -1,47 +0,0 @@
-use crate::Artifact;
-use std::{fmt::Display, path::Path};
-
-use super::ArtifactFormat;
-
-pub(crate) type TLAState = String;
-
-#[derive(Debug)]
-pub(crate) struct Model {}
-
-impl Display for Model {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        Ok(())
-    }
-}
-
-impl Artifact for Model {
-    fn name(&self) -> &'static str {
-        "TLA+ model"
-    }
-
-    fn typ(&self) -> &'static str {
-        "model"
-    }
-
-    fn from_string(s: &str) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn from_file(f: &Path) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn formats(&self) -> Vec<ArtifactFormat> {
-        vec![ArtifactFormat::TLA, ArtifactFormat::JSON]
-    }
-
-    fn to_file(&self, f: &Path, format: super::ArtifactFormat) -> Result<(), crate::Error> {
-        todo!()
-    }
-}
diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs
new file mode 100644
index 00000000..3591d302
--- /dev/null
+++ b/modelator/src/artifact/tla_file.rs
@@ -0,0 +1,35 @@
+use crate::Artifact;
+use std::{fmt::Display, path::Path};
+
+#[derive(Debug)]
+pub(crate) struct TLAFile {}
+
+impl Display for TLAFile {
+    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        Ok(())
+    }
+}
+
+impl Artifact for TLAFile {
+    fn name(&self) -> &'static str {
+        "TLA+ file"
+    }
+
+    fn from_string(_s: &str) -> Result<Self, crate::Error>
+    where
+        Self: Sized,
+    {
+        todo!()
+    }
+
+    fn from_file(_f: &Path) -> Result<Self, crate::Error>
+    where
+        Self: Sized,
+    {
+        todo!()
+    }
+
+    fn to_file(&self, _f: &Path) -> Result<(), crate::Error> {
+        todo!()
+    }
+}
diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs
new file mode 100644
index 00000000..d0fb1cb0
--- /dev/null
+++ b/modelator/src/artifact/tla_trace.rs
@@ -0,0 +1,28 @@
+use crate::Artifact;
+use std::path::Path;
+
+pub(crate) struct Trace {}
+
+impl Artifact for Trace {
+    fn name(&self) -> &'static str {
+        "State trace from model checking"
+    }
+
+    fn from_string(_s: &str) -> Result<Self, crate::Error>
+    where
+        Self: Sized,
+    {
+        todo!()
+    }
+
+    fn from_file(_f: &Path) -> Result<Self, crate::Error>
+    where
+        Self: Sized,
+    {
+        todo!()
+    }
+
+    fn to_file(&self, _f: &Path) -> Result<(), crate::Error> {
+        todo!()
+    }
+}
diff --git a/modelator/src/artifact/trace.rs b/modelator/src/artifact/trace.rs
deleted file mode 100644
index 62a4d6ab..00000000
--- a/modelator/src/artifact/trace.rs
+++ /dev/null
@@ -1,66 +0,0 @@
-use crate::Artifact;
-use std::{fmt::Display, path::Path};
-
-use super::ArtifactFormat;
-
-pub(crate) type TLAState = String;
-
-#[derive(Debug)]
-pub(crate) struct Trace {
-    pub states: Vec<TLAState>,
-}
-
-impl Trace {
-    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 Display for Trace {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        for state in &self.states {
-            write!(f, "{}\n\n", state)?;
-        }
-        Ok(())
-    }
-}
-
-impl Artifact for Trace {
-    fn name(&self) -> &'static str {
-        "State trace from model checking"
-    }
-
-    fn typ(&self) -> &'static str {
-        "trace"
-    }
-
-    fn from_string(s: &str) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn from_file(f: &Path) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn formats(&self) -> Vec<ArtifactFormat> {
-        vec![ArtifactFormat::TLC, ArtifactFormat::JSON]
-    }
-
-    fn to_file(&self, f: &Path, format: super::ArtifactFormat) -> Result<(), crate::Error> {
-        todo!()
-    }
-}
diff --git a/modelator/src/error.rs b/modelator/src/error.rs
index 41a8462d..a2ae546a 100644
--- a/modelator/src/error.rs
+++ b/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)]
diff --git a/modelator/src/util/convert.rs b/modelator/src/keep/convert.rs
similarity index 100%
rename from modelator/src/util/convert.rs
rename to modelator/src/keep/convert.rs
diff --git a/modelator/src/module.rs b/modelator/src/keep/module.rs
similarity index 94%
rename from modelator/src/module.rs
rename to modelator/src/keep/module.rs
index 5be42f72..de3b4759 100644
--- a/modelator/src/module.rs
+++ b/modelator/src/keep/module.rs
@@ -1,8 +1,15 @@
-use crate::{Artifact, ArtifactManifest};
+use crate::Artifact;
 use paste::paste;
 use serde::{Deserialize, Serialize};
 use serde_json;
 
+#[derive(Debug, Deserialize, Serialize, PartialEq)]
+pub struct ArtifactManifest {
+    pub name: &'static str,
+    #[serde(rename = "type")]
+    pub typ: &'static str,
+}
+
 #[derive(Debug, Deserialize, Serialize, PartialEq)]
 pub struct ModuleManifest {
     pub name: &'static str,
@@ -36,6 +43,15 @@ pub trait Module {
     //fn run(&self, method: &str, inputs: Vec<Box<dyn Artifact>>) -> Result<Vec<Box<dyn Artifact>>, Vec<Box<dyn Artifact>>>;
 }
 
+// #[modulator::module]
+// struct TLC {
+// }
+
+// impl TLC {
+//     #[modulator::method]
+//     fn check(&self, tla: TLA, )
+// }
+
 pub trait Method {
     fn manifest() -> MethodManifest;
     fn run(
diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs
index ef77b50b..bc62b9a2 100644
--- a/modelator/src/lib.rs
+++ b/modelator/src/lib.rs
@@ -4,13 +4,8 @@ mod options;
 /// Modelator's error type.
 mod error;
 
-mod util;
-
-mod module;
-pub use module::{MethodManifest, Module, ModuleManifest};
-
-pub mod artifact;
-pub use artifact::{Artifact, ArtifactManifest};
+/// List of artifacts.
+mod artifact;
 
 /// Download jar utilities.
 mod jar;
@@ -22,6 +17,7 @@ mod mc;
 pub mod runner;
 
 /// Re-exports.
+pub use artifact::Artifact;
 pub use error::{Error, TestError};
 pub use mc::JsonTrace;
 pub use options::{ModelChecker, Options, RunMode, Workers};
diff --git a/modelator/src/util/mod.rs b/modelator/src/util/mod.rs
deleted file mode 100644
index b5b67213..00000000
--- a/modelator/src/util/mod.rs
+++ /dev/null
@@ -1 +0,0 @@
-pub mod convert;

From 30452d2e63c871926a60bdb1b6f9ddef66928df1 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 14:29:42 +0100
Subject: [PATCH 2/9] Add TlaTrace and JsonTrace artifacts; Add TLA module

---
 modelator/src/artifact/json_trace.rs          | 13 ++++++
 modelator/src/artifact/mod.rs                 | 10 +++--
 modelator/src/artifact/tla_file.rs            |  3 +-
 modelator/src/artifact/tla_trace.rs           | 33 ++++++++++++--
 modelator/src/lib.rs                          | 17 ++++---
 modelator/src/{keep => macros}/convert.rs     |  0
 modelator/src/{keep => macros}/module.rs      |  0
 modelator/src/mc/mod.rs                       | 15 ++-----
 modelator/src/mc/tlc/mod.rs                   |  4 +-
 modelator/src/mc/tlc/output.rs                | 10 ++---
 modelator/src/mc/trace.rs                     | 45 -------------------
 modelator/src/module/mod.rs                   |  5 +++
 modelator/src/{mc => module/tla}/json/mod.rs  |  1 -
 .../src/{mc => module/tla}/json/parser.rs     |  0
 modelator/src/module/tla/mod.rs               | 19 ++++++++
 modelator/src/runner.rs                       |  3 +-
 16 files changed, 99 insertions(+), 79 deletions(-)
 rename modelator/src/{keep => macros}/convert.rs (100%)
 rename modelator/src/{keep => macros}/module.rs (100%)
 delete mode 100644 modelator/src/mc/trace.rs
 create mode 100644 modelator/src/module/mod.rs
 rename modelator/src/{mc => module/tla}/json/mod.rs (85%)
 rename modelator/src/{mc => module/tla}/json/parser.rs (100%)
 create mode 100644 modelator/src/module/tla/mod.rs

diff --git a/modelator/src/artifact/json_trace.rs b/modelator/src/artifact/json_trace.rs
index e69de29b..cac4dd98 100644
--- a/modelator/src/artifact/json_trace.rs
+++ b/modelator/src/artifact/json_trace.rs
@@ -0,0 +1,13 @@
+use serde_json::Value as JsonValue;
+pub struct JsonTrace {
+    pub 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()
+    }
+}
diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs
index 00674f80..b77af6bf 100644
--- a/modelator/src/artifact/mod.rs
+++ b/modelator/src/artifact/mod.rs
@@ -1,10 +1,14 @@
-mod tla_file;
-mod tla_trace;
-mod json_trace;
+pub(crate) mod tla_file;
+pub(crate) mod tla_trace;
+pub(crate) mod json_trace;
 
 use crate::error::Error;
 use std::{path::Path, str};
 
+// Re-exports.
+pub use tla_trace::TlaTrace;
+pub use json_trace::JsonTrace;
+
 pub trait Artifact {
     fn name(&self) -> &'static str;
 
diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs
index 3591d302..a6459972 100644
--- a/modelator/src/artifact/tla_file.rs
+++ b/modelator/src/artifact/tla_file.rs
@@ -1,4 +1,3 @@
-use crate::Artifact;
 use std::{fmt::Display, path::Path};
 
 #[derive(Debug)]
@@ -10,7 +9,7 @@ impl Display for TLAFile {
     }
 }
 
-impl Artifact for TLAFile {
+impl crate::artifact::Artifact for TLAFile {
     fn name(&self) -> &'static str {
         "TLA+ file"
     }
diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs
index d0fb1cb0..36090d8c 100644
--- a/modelator/src/artifact/tla_trace.rs
+++ b/modelator/src/artifact/tla_trace.rs
@@ -1,9 +1,36 @@
-use crate::Artifact;
 use std::path::Path;
 
-pub(crate) struct Trace {}
+pub(crate) type TlaState = String;
 
-impl Artifact for Trace {
+#[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 crate::artifact::Artifact for TlaTrace {
     fn name(&self) -> &'static str {
         "State trace from model checking"
     }
diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs
index bc62b9a2..c64ab116 100644
--- a/modelator/src/lib.rs
+++ b/modelator/src/lib.rs
@@ -5,7 +5,10 @@ mod options;
 mod error;
 
 /// List of artifacts.
-mod artifact;
+pub mod artifact;
+
+/// List of modules.
+pub mod module;
 
 /// Download jar utilities.
 mod jar;
@@ -17,15 +20,13 @@ mod mc;
 pub mod runner;
 
 /// Re-exports.
-pub use artifact::Artifact;
 pub use error::{Error, TestError};
-pub use mc::JsonTrace;
 pub use options::{ModelChecker, Options, RunMode, Workers};
 
 use serde::de::DeserializeOwned;
 use std::fmt::Debug;
 
-pub fn traces(options: Options) -> Result<Vec<JsonTrace>, Error> {
+pub fn traces(options: Options) -> Result<Vec<artifact::JsonTrace>, Error> {
     // create modelator dir (if it doens't already exist)
     if !options.dir.as_path().is_dir() {
         std::fs::create_dir_all(&options.dir).map_err(Error::IO)?;
@@ -38,7 +39,13 @@ pub fn traces(options: Options) -> Result<Vec<JsonTrace>, Error> {
     tracing::trace!("modelator setup completed");
 
     // run model checker
-    mc::run(options)
+    let traces = mc::run(options)?;
+
+    // convert each tla trace to json
+    traces
+        .into_iter()
+        .map(|tla_trace| module::Tla::tla_trace_to_json_trace(tla_trace))
+        .collect()
 }
 
 pub fn run<Runner, Step>(options: Options, runner: Runner) -> Result<(), TestError<Runner, Step>>
diff --git a/modelator/src/keep/convert.rs b/modelator/src/macros/convert.rs
similarity index 100%
rename from modelator/src/keep/convert.rs
rename to modelator/src/macros/convert.rs
diff --git a/modelator/src/keep/module.rs b/modelator/src/macros/module.rs
similarity index 100%
rename from modelator/src/keep/module.rs
rename to modelator/src/macros/module.rs
diff --git a/modelator/src/mc/mod.rs b/modelator/src/mc/mod.rs
index 03e72610..e35af047 100644
--- a/modelator/src/mc/mod.rs
+++ b/modelator/src/mc/mod.rs
@@ -1,22 +1,14 @@
-/// Definition of a Trace.
-mod trace;
-
 /// TLC model-checker.
 mod tlc;
 
-/// Conversion from TLA counterexamples to JSON.
-mod json;
-
 /// Utilitary functions.
 mod util;
 
-/// Re-exports.
-pub use trace::JsonTrace;
-
+use crate::artifact::TlaTrace;
 use crate::{Error, ModelChecker, Options, RunMode};
 use std::path::{Path, PathBuf};
 
-pub(crate) fn run(mut options: Options) -> Result<Vec<JsonTrace>, Error> {
+pub(crate) fn run(mut options: Options) -> Result<Vec<TlaTrace>, Error> {
     // check that the model tla file exists
     if !options.model_file.is_file() {
         return Err(Error::FileNotFound(options.model_file));
@@ -58,8 +50,7 @@ pub(crate) fn run(mut options: Options) -> Result<Vec<JsonTrace>, Error> {
         return Err(Error::NoTraceFound(options.log));
     }
 
-    // convert each trace to json
-    traces.into_iter().map(|trace| trace.parse()).collect()
+    Ok(traces)
 }
 
 fn create_test<P: AsRef<Path>>(
diff --git a/modelator/src/mc/tlc/mod.rs b/modelator/src/mc/tlc/mod.rs
index fa9d09b6..9f99684b 100644
--- a/modelator/src/mc/tlc/mod.rs
+++ b/modelator/src/mc/tlc/mod.rs
@@ -1,12 +1,12 @@
 /// Parsing of TLC's output.
 mod output;
 
-use super::trace::Trace;
+use crate::artifact::TlaTrace;
 use super::util;
 use crate::{jar, Error, Options, Workers};
 use std::process::Command;
 
-pub(crate) fn run(options: &Options) -> Result<Vec<Trace>, Error> {
+pub(crate) fn run(options: &Options) -> Result<Vec<TlaTrace>, Error> {
     // create tlc command
     let mut cmd = cmd(options);
 
diff --git a/modelator/src/mc/tlc/output.rs b/modelator/src/mc/tlc/output.rs
index 7525c327..e6aacc0f 100644
--- a/modelator/src/mc/tlc/output.rs
+++ b/modelator/src/mc/tlc/output.rs
@@ -1,7 +1,7 @@
-use crate::mc::trace::{TLAState, Trace};
+use crate::artifact::tla_trace::{TlaState, TlaTrace};
 use crate::{Error, Options};
 
-pub(crate) fn parse(output: String, options: &Options) -> Result<Vec<Trace>, Error> {
+pub(crate) fn parse(output: String, options: &Options) -> Result<Vec<TlaTrace>, Error> {
     let mut traces = Vec::new();
     let mut lines = output.lines();
 
@@ -19,10 +19,10 @@ pub(crate) fn parse(output: String, options: &Options) -> Result<Vec<Trace>, Err
 fn parse_trace<'a>(
     lines: &mut std::str::Lines<'a>,
     options: &Options,
-) -> Result<Option<Trace>, Error> {
+) -> Result<Option<TlaTrace>, Error> {
     let mut state_index = 0;
     let mut state = None;
-    let mut trace = Trace::new();
+    let mut trace = TlaTrace::new();
     loop {
         let line = lines
             .next()
@@ -55,7 +55,7 @@ fn parse_trace<'a>(
                 state.is_none(),
                 "[modelator] previous trace state has not ended yet"
             );
-            state = Some(TLAState::new());
+            state = Some(TlaState::new());
             continue;
         }
 
diff --git a/modelator/src/mc/trace.rs b/modelator/src/mc/trace.rs
deleted file mode 100644
index cca23a32..00000000
--- a/modelator/src/mc/trace.rs
+++ /dev/null
@@ -1,45 +0,0 @@
-use crate::Error;
-use serde_json::Value as JsonValue;
-
-pub(crate) type TLAState = String;
-
-#[derive(Debug)]
-pub(crate) struct Trace {
-    states: Vec<TLAState>,
-}
-
-impl Trace {
-    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()
-    }
-
-    pub(crate) fn parse(self) -> Result<JsonTrace, Error> {
-        let states = self
-            .states
-            .into_iter()
-            .map(|state| crate::mc::json::state_to_json(&state))
-            .collect::<Result<_, _>>()?;
-        Ok(JsonTrace { states })
-    }
-}
-
-pub struct JsonTrace {
-    pub 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()
-    }
-}
diff --git a/modelator/src/module/mod.rs b/modelator/src/module/mod.rs
new file mode 100644
index 00000000..be6578d2
--- /dev/null
+++ b/modelator/src/module/mod.rs
@@ -0,0 +1,5 @@
+// TLA+ module.
+mod tla;
+
+// Re-exports.
+pub use tla::Tla;
\ No newline at end of file
diff --git a/modelator/src/mc/json/mod.rs b/modelator/src/module/tla/json/mod.rs
similarity index 85%
rename from modelator/src/mc/json/mod.rs
rename to modelator/src/module/tla/json/mod.rs
index 7ae14663..a6afa57e 100644
--- a/modelator/src/mc/json/mod.rs
+++ b/modelator/src/module/tla/json/mod.rs
@@ -5,7 +5,6 @@ use crate::Error;
 use serde_json::Value as JsonValue;
 
 pub fn state_to_json(state: &str) -> Result<JsonValue, Error> {
-    tracing::debug!("converting the following state to json:\n{}", state);
     parser::parse_state(state)
         .map(|(input, value)| {
             assert!(
diff --git a/modelator/src/mc/json/parser.rs b/modelator/src/module/tla/json/parser.rs
similarity index 100%
rename from modelator/src/mc/json/parser.rs
rename to modelator/src/module/tla/json/parser.rs
diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs
new file mode 100644
index 00000000..c02fc7de
--- /dev/null
+++ b/modelator/src/module/tla/mod.rs
@@ -0,0 +1,19 @@
+/// Conversion from TLA traces to JSON.
+mod json;
+
+use crate::artifact::{JsonTrace, TlaTrace};
+
+// #[modelator::module]
+pub struct Tla;
+
+impl Tla {
+    // #[modelator::method]
+    pub fn tla_trace_to_json_trace(tla_trace: TlaTrace) -> Result<JsonTrace, crate::Error> {
+        tracing::debug!("Tla::tla_trace_to_json_trace:\n{:#?}", tla_trace);
+        let states = tla_trace
+            .into_iter()
+            .map(|state| json::state_to_json(&state))
+            .collect::<Result<_, _>>()?;
+        Ok(JsonTrace { states })
+    }
+}
diff --git a/modelator/src/runner.rs b/modelator/src/runner.rs
index b9f30b33..50014313 100644
--- a/modelator/src/runner.rs
+++ b/modelator/src/runner.rs
@@ -1,4 +1,5 @@
-use crate::{JsonTrace, TestError};
+use crate::artifact::JsonTrace;
+use crate::TestError;
 use serde::de::DeserializeOwned;
 use std::fmt::Debug;
 

From f94c92891fb5626afb4bf5e1bf01fe50944d5788 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 17:25:15 +0100
Subject: [PATCH 3/9] Add TlaConfigFile artifact; Add Tlc module

---
 modelator/src/artifact/json_trace.rs       |   8 +-
 modelator/src/artifact/mod.rs              |  26 ++--
 modelator/src/artifact/tla_cfg_file.rs     |  26 ++++
 modelator/src/artifact/tla_file.rs         |  53 ++++----
 modelator/src/artifact/tla_trace.rs        |  26 ----
 modelator/src/lib.rs                       |  32 +++--
 modelator/src/main.rs                      |  12 +-
 modelator/src/mc/mod.rs                    | 103 ---------------
 modelator/src/mc/tlc/mod.rs                |  87 -------------
 modelator/src/mc/util.rs                   |   3 -
 modelator/src/module/mod.rs                |   9 +-
 modelator/src/module/tla/mod.rs            | 111 +++++++++++++++-
 modelator/src/module/tlc/mod.rs            | 114 +++++++++++++++++
 modelator/src/{mc => module}/tlc/output.rs |   6 +-
 modelator/src/module/util.rs               |   3 +
 modelator/src/options.rs                   | 139 ++++++---------------
 16 files changed, 371 insertions(+), 387 deletions(-)
 create mode 100644 modelator/src/artifact/tla_cfg_file.rs
 delete mode 100644 modelator/src/mc/mod.rs
 delete mode 100644 modelator/src/mc/tlc/mod.rs
 delete mode 100644 modelator/src/mc/util.rs
 create mode 100644 modelator/src/module/tlc/mod.rs
 rename modelator/src/{mc => module}/tlc/output.rs (91%)
 create mode 100644 modelator/src/module/util.rs

diff --git a/modelator/src/artifact/json_trace.rs b/modelator/src/artifact/json_trace.rs
index cac4dd98..59d42f23 100644
--- a/modelator/src/artifact/json_trace.rs
+++ b/modelator/src/artifact/json_trace.rs
@@ -1,6 +1,6 @@
 use serde_json::Value as JsonValue;
 pub struct JsonTrace {
-    pub states: Vec<JsonValue>,
+    states: Vec<JsonValue>,
 }
 
 impl IntoIterator for JsonTrace {
@@ -11,3 +11,9 @@ impl IntoIterator for JsonTrace {
         self.states.into_iter()
     }
 }
+
+impl From<Vec<JsonValue>> for JsonTrace {
+    fn from(states: Vec<JsonValue>) -> Self {
+        Self { states }
+    }
+}
diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs
index b77af6bf..8e4f4df0 100644
--- a/modelator/src/artifact/mod.rs
+++ b/modelator/src/artifact/mod.rs
@@ -1,24 +1,20 @@
+pub(crate) mod json_trace;
+pub(crate) mod tla_cfg_file;
 pub(crate) mod tla_file;
 pub(crate) mod tla_trace;
-pub(crate) mod json_trace;
-
-use crate::error::Error;
-use std::{path::Path, str};
 
 // Re-exports.
-pub use tla_trace::TlaTrace;
 pub use json_trace::JsonTrace;
+pub use tla_cfg_file::TlaConfigFile;
+pub use tla_file::TlaFile;
+pub use tla_trace::TlaTrace;
 
-pub trait Artifact {
-    fn name(&self) -> &'static str;
+use serde::de::DeserializeOwned;
+use serde::Serialize;
 
-    fn to_file(&self, f: &Path) -> Result<(), Error>;
+/// Artifacts should be able to serialized (into a string/file) and deserialized
+/// (from string/file).
+pub trait Artifact: Serialize + DeserializeOwned {}
 
-    fn from_file(f: &Path) -> Result<Self, Error>
-    where
-        Self: Sized;
 
-    fn from_string(s: &str) -> Result<Self, Error>
-    where
-        Self: Sized;
-}
+// TODO: assert that all artifacts implement the above trait.
\ No newline at end of file
diff --git a/modelator/src/artifact/tla_cfg_file.rs b/modelator/src/artifact/tla_cfg_file.rs
new file mode 100644
index 00000000..ce166bd5
--- /dev/null
+++ b/modelator/src/artifact/tla_cfg_file.rs
@@ -0,0 +1,26 @@
+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())
+    }
+}
diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs
index a6459972..9ff69c50 100644
--- a/modelator/src/artifact/tla_file.rs
+++ b/modelator/src/artifact/tla_file.rs
@@ -1,34 +1,41 @@
-use std::{fmt::Display, path::Path};
+use std::path::{Path, PathBuf};
 
-#[derive(Debug)]
-pub(crate) struct TLAFile {}
-
-impl Display for TLAFile {
-    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        Ok(())
-    }
+pub struct TlaFile {
+    path: PathBuf,
 }
 
-impl crate::artifact::Artifact for TLAFile {
-    fn name(&self) -> &'static str {
-        "TLA+ file"
+impl TlaFile {
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
+        Self {
+            path: path.as_ref().to_path_buf(),
+        }
     }
 
-    fn from_string(_s: &str) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
+    pub(crate) fn path(&self) -> &PathBuf {
+        &self.path
     }
 
-    fn from_file(_f: &Path) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
+    /// 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
+        }
     }
+}
 
-    fn to_file(&self, _f: &Path) -> Result<(), crate::Error> {
-        todo!()
+impl<P> From<P> for TlaFile
+where
+    P: AsRef<Path>,
+{
+    fn from(path: P) -> Self {
+        Self::new(path.as_ref().to_path_buf())
     }
 }
diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs
index 36090d8c..6d7850bc 100644
--- a/modelator/src/artifact/tla_trace.rs
+++ b/modelator/src/artifact/tla_trace.rs
@@ -1,5 +1,3 @@
-use std::path::Path;
-
 pub(crate) type TlaState = String;
 
 #[derive(Debug)]
@@ -29,27 +27,3 @@ impl IntoIterator for TlaTrace {
         self.states.into_iter()
     }
 }
-
-impl crate::artifact::Artifact for TlaTrace {
-    fn name(&self) -> &'static str {
-        "State trace from model checking"
-    }
-
-    fn from_string(_s: &str) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn from_file(_f: &Path) -> Result<Self, crate::Error>
-    where
-        Self: Sized,
-    {
-        todo!()
-    }
-
-    fn to_file(&self, _f: &Path) -> Result<(), crate::Error> {
-        todo!()
-    }
-}
diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs
index c64ab116..41450c74 100644
--- a/modelator/src/lib.rs
+++ b/modelator/src/lib.rs
@@ -13,20 +13,22 @@ pub mod module;
 /// Download jar utilities.
 mod jar;
 
-/// Model checkers.
-mod mc;
-
 /// Test runner.
 pub mod runner;
 
 /// Re-exports.
 pub use error::{Error, TestError};
-pub use options::{ModelChecker, Options, RunMode, Workers};
+pub use options::{ModelCheckerOptions, ModelCheckerWorkers, Options};
 
 use serde::de::DeserializeOwned;
 use std::fmt::Debug;
+use std::path::Path;
 
-pub fn traces(options: Options) -> Result<Vec<artifact::JsonTrace>, Error> {
+pub fn traces<P: AsRef<Path>>(
+    tla_tests_file: P,
+    tla_config_file: P,
+    options: Options,
+) -> Result<Vec<artifact::JsonTrace>, Error> {
     // create modelator dir (if it doens't already exist)
     if !options.dir.as_path().is_dir() {
         std::fs::create_dir_all(&options.dir).map_err(Error::IO)?;
@@ -38,8 +40,14 @@ pub fn traces(options: Options) -> Result<Vec<artifact::JsonTrace>, Error> {
     jar::download_jars(&options.dir)?;
     tracing::trace!("modelator setup completed");
 
-    // run model checker
-    let traces = mc::run(options)?;
+    // generate tla tests
+    let tests = module::Tla::generate_tests(tla_tests_file.into(), tla_config_file.into())?;
+
+    // run tlc on each tla test
+    let traces = tests
+        .into_iter()
+        .map(|(tla_file, tla_config_file)| module::Tlc::test(tla_file, tla_config_file, &options))
+        .collect::<Result<Vec<_>, _>>()?;
 
     // convert each tla trace to json
     traces
@@ -48,12 +56,18 @@ pub fn traces(options: Options) -> Result<Vec<artifact::JsonTrace>, Error> {
         .collect()
 }
 
-pub fn run<Runner, Step>(options: Options, runner: Runner) -> Result<(), TestError<Runner, Step>>
+pub fn run<P, Runner, Step>(
+    tla_tests_file: P,
+    tla_config_file: P,
+    runner: Runner,
+) -> Result<(), TestError<Runner, Step>>
 where
+    P: AsRef<Path>,
     Runner: runner::TestRunner<Step> + Debug + Clone,
     Step: DeserializeOwned + Debug + Clone,
 {
-    let traces = traces(options).map_err(TestError::Modelator)?;
+    let options = Options::default();
+    let traces = traces(tla_tests_file, tla_config_file, options).map_err(TestError::Modelator)?;
     for trace in traces {
         let runner = runner.clone();
         runner::run(trace, runner)?;
diff --git a/modelator/src/main.rs b/modelator/src/main.rs
index bf168ced..aee6f5ff 100644
--- a/modelator/src/main.rs
+++ b/modelator/src/main.rs
@@ -1,16 +1,8 @@
-use clap::Clap;
 use modelator::{Error, Options};
 
 fn main() -> Result<(), Error> {
-    let _options = Options::new("IBCTests.tla")
-        .tlc()
-        .workers(modelator::Workers::Auto)
-        .test("ICS03ConnectionOpenConfirmOKTest")
-        .log("tlc.log");
-
-    // cargo run -- IBCTests.tla -r test,ICS03ConnectionOpenConfirmOKTest
-    let options = Options::parse();
-    let traces = modelator::traces(options)?;
+    let options = Options::default();
+    let traces = modelator::traces("IBCTests.tla", "IBCTests.cfg", options)?;
 
     // aggregate all traces into a json array (and each trace into a json array
     // as well)
diff --git a/modelator/src/mc/mod.rs b/modelator/src/mc/mod.rs
deleted file mode 100644
index e35af047..00000000
--- a/modelator/src/mc/mod.rs
+++ /dev/null
@@ -1,103 +0,0 @@
-/// TLC model-checker.
-mod tlc;
-
-/// Utilitary functions.
-mod util;
-
-use crate::artifact::TlaTrace;
-use crate::{Error, ModelChecker, Options, RunMode};
-use std::path::{Path, PathBuf};
-
-pub(crate) fn run(mut options: Options) -> Result<Vec<TlaTrace>, Error> {
-    // check that the model tla file exists
-    if !options.model_file.is_file() {
-        return Err(Error::FileNotFound(options.model_file));
-    }
-
-    // compute model directory
-    let mut model_dir = options.model_file.clone();
-    assert!(model_dir.pop());
-
-    // extract tla model name
-    let model_name = options
-        .model_file
-        .file_name()
-        .unwrap()
-        .to_string_lossy()
-        .trim_end_matches(".tla")
-        .to_owned();
-
-    // check that the model cfg file exists
-    let cfg_file = model_dir.join(format!("{}.cfg", model_name));
-    if !cfg_file.is_file() {
-        return Err(Error::FileNotFound(cfg_file));
-    }
-
-    // create new model file with the tests negated if `RunMode::Test`
-    if let RunMode::Test(test_name) = &options.run_mode {
-        let model_file = create_test(model_dir, &model_name, test_name, cfg_file)?;
-        // update model file in options
-        options.model_file = model_file;
-    };
-
-    // run the model checker
-    let traces = match options.model_checker {
-        ModelChecker::TLC => tlc::run(&options),
-    }?;
-
-    // check if no trace was found
-    if traces.is_empty() {
-        return Err(Error::NoTraceFound(options.log));
-    }
-
-    Ok(traces)
-}
-
-fn create_test<P: AsRef<Path>>(
-    model_dir: P,
-    model_name: &str,
-    test_name: &str,
-    cfg_file: P,
-) -> Result<PathBuf, Error> {
-    let test_model_name = format!("{}_{}", model_name, test_name);
-    let invariant = format!("{}Neg", test_name);
-    // create test model where the test is negated
-    let test_model = test_model(model_name, test_name, &test_model_name, &invariant);
-    // create test config with negated test as an invariant
-    let test_cfg = test_cfg(&invariant, cfg_file)?;
-
-    // write test model to test model file
-    let test_model_file = model_dir.as_ref().join(format!("{}.tla", test_model_name));
-    std::fs::write(&test_model_file, test_model).map_err(Error::IO)?;
-
-    // write test cfg to test cfg file
-    let test_cfg_file = model_dir.as_ref().join(format!("{}.cfg", test_model_name));
-    std::fs::write(&test_cfg_file, test_cfg).map_err(Error::IO)?;
-    Ok(test_model_file)
-}
-
-fn test_model(model_name: &str, test_name: &str, test_model_name: &str, invariant: &str) -> String {
-    format!(
-        r#"
----------- MODULE {} ----------
-
-EXTENDS {}
-
-{} == ~{}
-
-===============================
-"#,
-        test_model_name, model_name, invariant, test_name
-    )
-}
-
-fn test_cfg<P: AsRef<Path>>(invariant: &str, cfg_file: P) -> Result<String, Error> {
-    let cfg = std::fs::read_to_string(cfg_file).map_err(Error::IO)?;
-    Ok(format!(
-        r#"
-{}
-INVARIANT {}
-"#,
-        cfg, invariant
-    ))
-}
diff --git a/modelator/src/mc/tlc/mod.rs b/modelator/src/mc/tlc/mod.rs
deleted file mode 100644
index 9f99684b..00000000
--- a/modelator/src/mc/tlc/mod.rs
+++ /dev/null
@@ -1,87 +0,0 @@
-/// Parsing of TLC's output.
-mod output;
-
-use crate::artifact::TlaTrace;
-use super::util;
-use crate::{jar, Error, Options, Workers};
-use std::process::Command;
-
-pub(crate) fn run(options: &Options) -> Result<Vec<TlaTrace>, Error> {
-    // create tlc command
-    let mut cmd = cmd(options);
-
-    // start tlc
-    // TODO: add timeout
-    let output = cmd.output().map_err(Error::IO)?;
-
-    // get tlc stdout and stderr
-    let stdout = util::output_to_string(&output.stdout);
-    let stderr = util::output_to_string(&output.stderr);
-    tracing::debug!("TLC stdout:\n{}", stdout);
-    tracing::debug!("TLC stderr:\n{}", stderr);
-
-    match (stdout.is_empty(), stderr.is_empty()) {
-        (false, true) => {
-            // if stderr is empty, but the stdout is not, then no error has
-            // occurred
-
-            // save tlc log
-            std::fs::write(&options.log, &stdout).map_err(Error::IO)?;
-
-            // remove tlc 'states' folder. on each run, tlc creates a new folder
-            // inside the 'states' folder named using the current date with a
-            // second precision (e.g. 'states/21-03-04-16-42-04'). if we happen
-            // to run tlc twice in the same second, tlc fails when trying to
-            // create this folder for the second time. we avoid this problem by
-            // simply removing the parent folder 'states' after every tlc run
-            std::fs::remove_dir_all("states").map_err(Error::IO)?;
-
-            // convert tlc output to counterexamples
-            output::parse(stdout, &options)
-        }
-        (true, false) => {
-            // if stdout is empty, but the stderr is not, return an error
-            Err(Error::TLCFailure(stderr))
-        }
-        _ => {
-            panic!("[modelator] unexpected TLC's stdout/stderr combination")
-        }
-    }
-}
-
-fn cmd(options: &Options) -> Command {
-    let tla2tools = jar::Jar::Tla.file(&options.dir);
-    let community_modules = jar::Jar::CommunityModules.file(&options.dir);
-    let mut cmd = Command::new("java");
-    cmd
-        // set classpath
-        .arg("-cp")
-        .arg(format!(
-            "{}:{}",
-            tla2tools.as_path().to_string_lossy(),
-            community_modules.as_path().to_string_lossy(),
-        ))
-        // set tla file
-        .arg("tlc2.TLC")
-        .arg(&options.model_file)
-        // set "-tool" flag, which allows easier parsing of TLC's output
-        .arg("-tool")
-        // set the number of TLC's workers
-        .arg("-workers")
-        .arg(workers(options.workers));
-
-    // show command being run
-    let pretty = format!("{:?}", cmd).replace("\"", "");
-    let pretty = pretty.trim_start_matches("Command { std:");
-    let pretty = pretty.trim_end_matches(", kill_on_drop: false }");
-    tracing::debug!("{}", pretty);
-
-    cmd
-}
-
-fn workers(workers: Workers) -> String {
-    match workers {
-        Workers::Auto => "auto".to_string(),
-        Workers::Count(count) => count.to_string(),
-    }
-}
diff --git a/modelator/src/mc/util.rs b/modelator/src/mc/util.rs
deleted file mode 100644
index f91285d8..00000000
--- a/modelator/src/mc/util.rs
+++ /dev/null
@@ -1,3 +0,0 @@
-pub(crate) fn output_to_string(output: &[u8]) -> String {
-    String::from_utf8_lossy(output).to_string()
-}
diff --git a/modelator/src/module/mod.rs b/modelator/src/module/mod.rs
index be6578d2..3499de6c 100644
--- a/modelator/src/module/mod.rs
+++ b/modelator/src/module/mod.rs
@@ -1,5 +1,12 @@
 // TLA+ module.
 mod tla;
 
+// TLC module.
+mod tlc;
+
+/// Utilitary functions.
+mod util;
+
 // Re-exports.
-pub use tla::Tla;
\ No newline at end of file
+pub use tla::Tla;
+pub use tlc::Tlc;
diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs
index c02fc7de..a2735ec7 100644
--- a/modelator/src/module/tla/mod.rs
+++ b/modelator/src/module/tla/mod.rs
@@ -1,19 +1,120 @@
 /// Conversion from TLA traces to JSON.
 mod json;
 
-use crate::artifact::{JsonTrace, TlaTrace};
-
+use crate::artifact::{JsonTrace, TlaConfigFile, TlaFile, TlaTrace};
+use crate::Error;
+use serde_json::Value as JsonValue;
+use std::path::PathBuf;
 // #[modelator::module]
 pub struct Tla;
 
 impl Tla {
     // #[modelator::method]
-    pub fn tla_trace_to_json_trace(tla_trace: TlaTrace) -> Result<JsonTrace, crate::Error> {
+    pub fn tla_trace_to_json_trace(tla_trace: TlaTrace) -> Result<JsonTrace, Error> {
         tracing::debug!("Tla::tla_trace_to_json_trace:\n{:#?}", tla_trace);
-        let states = tla_trace
+        let states: Vec<JsonValue> = tla_trace
             .into_iter()
             .map(|state| json::state_to_json(&state))
             .collect::<Result<_, _>>()?;
-        Ok(JsonTrace { states })
+        Ok(states.into())
     }
+
+    // #[modelator::method]
+    pub fn generate_tests(
+        tla_tests_file: TlaFile,
+        tla_config_file: TlaConfigFile,
+    ) -> Result<Vec<(TlaFile, TlaConfigFile)>, Error> {
+        // check that the tla tests file exists
+        if !tla_tests_file.path().is_file() {
+            return Err(Error::FileNotFound(tla_tests_file.path().clone()));
+        }
+
+        // check that the tla cfg file exists
+        if !tla_config_file.path().is_file() {
+            return Err(Error::FileNotFound(tla_config_file.path().clone()));
+        }
+
+        // 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());
+
+        // 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();
+
+        // TODO: retrieve test names from tla tests file
+        let test_names = Vec::new();
+        test_names
+            .into_iter()
+            .map(|test_name| {
+                generate_test(
+                    &tla_tests_dir,
+                    &tla_tests_module_name,
+                    test_name,
+                    &tla_config_file,
+                )
+            })
+            .collect()
+    }
+}
+
+fn generate_test(
+    tla_tests_dir: &PathBuf,
+    tla_tests_module_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);
+
+    // create tla module where the test is negated
+    let test_module = genereate_test_module(
+        tla_tests_module_name,
+        test_name,
+        &test_module_name,
+        &invariant,
+    );
+    // create test config with negated test as an invariant
+    let test_config = generate_test_config(tla_config_file, &invariant)?;
+
+    // write test module to test module file
+    let test_module_file = tla_tests_dir.join(format!("{}.tla", test_module_name));
+    std::fs::write(&test_module_file, test_module).map_err(Error::IO)?;
+
+    // write test config to test config file
+    let test_config_file = tla_tests_dir.join(format!("{}.cfg", test_module_name));
+    std::fs::write(&test_config_file, test_config).map_err(Error::IO)?;
+
+    Ok((test_module_file.into(), test_config_file.into()))
+}
+
+fn genereate_test_module(
+    tla_tests_module_name: &str,
+    test_name: &str,
+    test_module_name: &str,
+    invariant: &str,
+) -> String {
+    format!(
+        r#"
+---------- MODULE {} ----------
+
+EXTENDS {}
+
+{} == ~{}
+
+===============================
+"#,
+        test_module_name, tla_tests_module_name, invariant, test_name
+    )
+}
+
+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()).map_err(Error::IO)?;
+    Ok(format!(
+        r#"
+{}
+INVARIANT {}
+"#,
+        tla_config, invariant
+    ))
 }
diff --git a/modelator/src/module/tlc/mod.rs b/modelator/src/module/tlc/mod.rs
new file mode 100644
index 00000000..76478bda
--- /dev/null
+++ b/modelator/src/module/tlc/mod.rs
@@ -0,0 +1,114 @@
+/// Parsing of TLC's output.
+mod output;
+
+use super::util;
+use crate::artifact::{TlaConfigFile, TlaFile, TlaTrace};
+use crate::{jar, Error, ModelCheckerWorkers, Options};
+use std::path::Path;
+use std::process::Command;
+
+// #[modelator::module]
+pub struct Tlc;
+
+impl Tlc {
+    // #[modelator::method]
+    pub fn test(
+        tla_file: TlaFile,
+        tla_config_file: TlaConfigFile,
+        options: &Options,
+    ) -> Result<TlaTrace, Error> {
+        // create tlc command
+        let mut cmd = cmd(tla_file.path(), tla_config_file.path(), options);
+
+        // start tlc
+        // TODO: add timeout
+        let output = cmd.output().map_err(Error::IO)?;
+
+        // get tlc stdout and stderr
+        let stdout = util::cmd_output_to_string(&output.stdout);
+        let stderr = util::cmd_output_to_string(&output.stderr);
+        tracing::debug!("TLC stdout:\n{}", stdout);
+        tracing::debug!("TLC stderr:\n{}", stderr);
+
+        match (stdout.is_empty(), stderr.is_empty()) {
+            (false, true) => {
+                // if stderr is empty, but the stdout is not, then no error has
+                // occurred
+
+                // save tlc log
+                std::fs::write(&options.model_checker_options.log, &stdout).map_err(Error::IO)?;
+
+                // remove tlc 'states' folder. on each run, tlc creates a new folder
+                // inside the 'states' folder named using the current date with a
+                // second precision (e.g. 'states/21-03-04-16-42-04'). if we happen
+                // to run tlc twice in the same second, tlc fails when trying to
+                // create this folder for the second time. we avoid this problem by
+                // simply removing the parent folder 'states' after every tlc run
+                std::fs::remove_dir_all("states").map_err(Error::IO)?;
+
+                // convert tlc output to traces
+                let mut traces = output::parse(stdout, &options.model_checker_options)?;
+
+                // check if no trace was found
+                if traces.is_empty() {
+                    return Err(Error::NoTraceFound(
+                        options.model_checker_options.log.clone(),
+                    ));
+                }
+
+                // at most one trace should have been found
+                assert_eq!(
+                    traces.len(),
+                    1,
+                    "[modelator] unexpected number of traces in TLC's log"
+                );
+                Ok(traces.pop().unwrap())
+            }
+            (true, false) => {
+                // if stdout is empty, but the stderr is not, return an error
+                Err(Error::TLCFailure(stderr))
+            }
+            _ => {
+                panic!("[modelator] unexpected TLC's stdout/stderr combination")
+            }
+        }
+    }
+}
+
+fn cmd<P: AsRef<Path>>(tla_file: P, tla_config_file: P, options: &Options) -> Command {
+    let tla2tools = jar::Jar::Tla.file(&options.dir);
+    let community_modules = jar::Jar::CommunityModules.file(&options.dir);
+
+    let mut cmd = Command::new("java");
+    cmd
+        // set classpath
+        .arg("-cp")
+        .arg(format!(
+            "{}:{}",
+            tla2tools.as_path().to_string_lossy(),
+            community_modules.as_path().to_string_lossy(),
+        ))
+        // set tla file
+        .arg("tlc2.TLC")
+        .arg(tla_file.as_ref())
+        // set "-tool" flag, which allows easier parsing of TLC's output
+        .arg("-tool")
+        // set the number of TLC's workers
+        .arg("-workers")
+        .arg(workers(options));
+
+    // show command being run
+    let pretty = format!("{:?}", cmd).replace("\"", "");
+    let pretty = pretty.trim_start_matches("Command { std:");
+    let pretty = pretty.trim_end_matches(", kill_on_drop: false }");
+    tracing::debug!("{}", pretty);
+
+    cmd
+}
+
+fn workers(options: &Options) -> String {
+    match options.model_checker_options.workers {
+        ModelCheckerWorkers::Auto => "auto".to_string(),
+        ModelCheckerWorkers::Count(count) => count.to_string(),
+    }
+}
diff --git a/modelator/src/mc/tlc/output.rs b/modelator/src/module/tlc/output.rs
similarity index 91%
rename from modelator/src/mc/tlc/output.rs
rename to modelator/src/module/tlc/output.rs
index e6aacc0f..e7d37aec 100644
--- a/modelator/src/mc/tlc/output.rs
+++ b/modelator/src/module/tlc/output.rs
@@ -1,7 +1,7 @@
 use crate::artifact::tla_trace::{TlaState, TlaTrace};
-use crate::{Error, Options};
+use crate::{Error, ModelCheckerOptions};
 
-pub(crate) fn parse(output: String, options: &Options) -> Result<Vec<TlaTrace>, Error> {
+pub(crate) fn parse(output: String, options: &ModelCheckerOptions) -> Result<Vec<TlaTrace>, Error> {
     let mut traces = Vec::new();
     let mut lines = output.lines();
 
@@ -18,7 +18,7 @@ pub(crate) fn parse(output: String, options: &Options) -> Result<Vec<TlaTrace>,
 
 fn parse_trace<'a>(
     lines: &mut std::str::Lines<'a>,
-    options: &Options,
+    options: &ModelCheckerOptions,
 ) -> Result<Option<TlaTrace>, Error> {
     let mut state_index = 0;
     let mut state = None;
diff --git a/modelator/src/module/util.rs b/modelator/src/module/util.rs
new file mode 100644
index 00000000..b19b3fd7
--- /dev/null
+++ b/modelator/src/module/util.rs
@@ -0,0 +1,3 @@
+pub(crate) fn cmd_output_to_string(output: &[u8]) -> String {
+    String::from_utf8_lossy(output).to_string()
+}
diff --git a/modelator/src/options.rs b/modelator/src/options.rs
index 79ca734c..3647ca4c 100644
--- a/modelator/src/options.rs
+++ b/modelator/src/options.rs
@@ -1,69 +1,51 @@
-use clap::Clap;
 use std::path::{Path, PathBuf};
 
-#[derive(Clone, Debug, Clap)]
+#[derive(Clone, Debug)]
 pub struct Options {
-    /// TLA model file.
-    pub model_file: PathBuf,
-
-    /// Which model checker to use. Possible values: 'TLC'.
-    #[clap(short, long, default_value = "TLC")]
-    pub model_checker: ModelChecker,
-
-    /// Model checher run mode. Possible values: 'explore,10' to explore the
-    /// model randomly and generate 10 random traces; and 'test,X' to generate
-    /// a test for X (if possible).
-    #[clap(short, long, default_value = "explore,10")]
-    pub run_mode: RunMode,
-
-    /// Number of model checker workers. Possible values: 'auto' to select the
-    /// number of model checker worker threads based on on the number of
-    /// available cores; and any number (e.g. '4') precising the number of
-    /// workers threads.
-    #[clap(short, long, default_value = "auto")]
-    pub workers: Workers,
-
-    /// Model checker log file for debugging purposes.
-    #[clap(long, default_value = "mc.log")]
-    pub log: PathBuf,
+    /// Model checker options.
+    pub model_checker_options: ModelCheckerOptions,
 
     /// Modelator directory.
-    #[clap(long, default_value = ".modelator")]
     pub dir: PathBuf,
 }
 
 impl Options {
-    pub fn new<P: AsRef<Path>>(model_file: P) -> Self {
-        Self {
-            model_file: model_file.as_ref().to_path_buf(),
-            model_checker: ModelChecker::TLC,
-            workers: Workers::Auto,
-            run_mode: RunMode::Explore(10),
-            log: Path::new("mc.log").to_path_buf(),
-            dir: Path::new(".modelator").to_path_buf(),
-        }
-    }
-
-    /// Set the TLC model checker.
-    pub fn tlc(mut self) -> Self {
-        self.model_checker = ModelChecker::TLC;
+    /// Set TLC options.
+    pub fn model_checker_options(mut self, model_checker_options: ModelCheckerOptions) -> Self {
+        self.model_checker_options = model_checker_options;
         self
     }
 
-    /// Set the test run mode given the test name.
-    pub fn test<S: Into<String>>(mut self, test_name: S) -> Self {
-        self.run_mode = RunMode::Test(test_name.into());
+    /// Set modelator directory.
+    pub fn dir(mut self, dir: impl AsRef<Path>) -> Self {
+        self.dir = dir.as_ref().to_path_buf();
         self
     }
+}
 
-    /// Set the explore run mode given the number of traces to be generated.
-    pub fn explore(mut self, trace_count: usize) -> Self {
-        self.run_mode = RunMode::Explore(trace_count);
-        self
+impl Default for Options {
+    fn default() -> Self {
+        Self {
+            model_checker_options: ModelCheckerOptions::default(),
+            dir: Path::new(".modelator").to_path_buf(),
+        }
     }
+}
 
+#[derive(Clone, Debug)]
+pub struct ModelCheckerOptions {
+    /// Number of model checker worker threads. Possible values: 'auto' to
+    /// select the number of worker threads based on the number of available
+    /// cores; and any number (e.g. '4') precising the number of workers threads.
+    pub workers: ModelCheckerWorkers,
+
+    /// Model checker log file for debugging purposes.
+    pub log: PathBuf,
+}
+
+impl ModelCheckerOptions {
     /// Set number of model checker workers.
-    pub fn workers(mut self, workers: Workers) -> Self {
+    pub fn workers(mut self, workers: ModelCheckerWorkers) -> Self {
         self.workers = workers;
         self
     }
@@ -73,72 +55,27 @@ impl Options {
         self.log = log.as_ref().to_path_buf();
         self
     }
-
-    /// Set modelator directory.
-    pub fn dir(mut self, dir: impl AsRef<Path>) -> Self {
-        self.dir = dir.as_ref().to_path_buf();
-        self
-    }
-}
-
-#[derive(Clone, Copy, Debug)]
-pub enum ModelChecker {
-    TLC,
-}
-
-impl std::str::FromStr for ModelChecker {
-    type Err = String;
-
-    fn from_str(s: &str) -> Result<Self, Self::Err> {
-        match s {
-            "TLC" => Ok(Self::TLC),
-            _ => Err(unsupported(s)),
-        }
-    }
 }
 
-#[derive(Clone, Debug)]
-pub enum RunMode {
-    /// Test mode. The argument is the name of the test.
-    Test(String),
-    /// Exploration mode. The argument is the number of traces to be generated.
-    /// This mode corresponds to TLC's simulation mode.
-    Explore(usize),
-}
-
-impl std::str::FromStr for RunMode {
-    type Err = String;
-
-    fn from_str(s: &str) -> Result<Self, Self::Err> {
-        let parts: Vec<_> = s.split(',').collect();
-        if parts.len() != 2 {
-            return Err(unsupported(s));
-        }
-
-        match parts[0] {
-            "test" => Ok(Self::Test(parts[1].to_string())),
-            "explore" => {
-                if let Ok(count) = parts[1].parse() {
-                    Ok(Self::Explore(count))
-                } else {
-                    Err(unsupported(s))
-                }
-            }
-            _ => Err(unsupported(s)),
+impl Default for ModelCheckerOptions {
+    fn default() -> Self {
+        Self {
+            workers: ModelCheckerWorkers::Auto,
+            log: Path::new("mc.log").to_path_buf(),
         }
     }
 }
 
 #[derive(Clone, Copy, Debug)]
-pub enum Workers {
+pub enum ModelCheckerWorkers {
     /// Automatically select the number of model checker worker threads based
-    // on the number of available cores.
+    /// on the number of available cores.
     Auto,
     /// Number of model checker worker threads.
     Count(usize),
 }
 
-impl std::str::FromStr for Workers {
+impl std::str::FromStr for ModelCheckerWorkers {
     type Err = String;
 
     fn from_str(s: &str) -> Result<Self, Self::Err> {

From f6e9ee4cfcbcc626fdfffd0d29924499f0b40862 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 18:03:32 +0100
Subject: [PATCH 4/9] clippy; fmt

---
 modelator/src/artifact/mod.rs | 3 +--
 modelator/src/lib.rs          | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/modelator/src/artifact/mod.rs b/modelator/src/artifact/mod.rs
index 8e4f4df0..c3a133e1 100644
--- a/modelator/src/artifact/mod.rs
+++ b/modelator/src/artifact/mod.rs
@@ -16,5 +16,4 @@ use serde::Serialize;
 /// (from string/file).
 pub trait Artifact: Serialize + DeserializeOwned {}
 
-
-// TODO: assert that all artifacts implement the above trait.
\ No newline at end of file
+// TODO: assert that all artifacts implement the above trait.
diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs
index 41450c74..36acc6da 100644
--- a/modelator/src/lib.rs
+++ b/modelator/src/lib.rs
@@ -52,7 +52,7 @@ pub fn traces<P: AsRef<Path>>(
     // convert each tla trace to json
     traces
         .into_iter()
-        .map(|tla_trace| module::Tla::tla_trace_to_json_trace(tla_trace))
+        .map(module::Tla::tla_trace_to_json_trace)
         .collect()
 }
 

From e38de779120757ec38c714d3c4c9d0e62f3c0824 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 18:05:55 +0100
Subject: [PATCH 5/9] tlc: set tla config file in tlc command

---
 modelator/src/module/tlc/mod.rs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/modelator/src/module/tlc/mod.rs b/modelator/src/module/tlc/mod.rs
index 76478bda..3cdae3b7 100644
--- a/modelator/src/module/tlc/mod.rs
+++ b/modelator/src/module/tlc/mod.rs
@@ -91,6 +91,9 @@ fn cmd<P: AsRef<Path>>(tla_file: P, tla_config_file: P, options: &Options) -> Co
         // set tla file
         .arg("tlc2.TLC")
         .arg(tla_file.as_ref())
+        // set tla config file
+        .arg("-config")
+        .arg(tla_config_file.as_ref())
         // set "-tool" flag, which allows easier parsing of TLC's output
         .arg("-tool")
         // set the number of TLC's workers

From f41a640d455861189f5f06e152880bff8a6a96ff Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 18:27:57 +0100
Subject: [PATCH 6/9] tla: extract test names from tla test file

---
 modelator/src/artifact/tla_cfg_file.rs |  6 +++++
 modelator/src/artifact/tla_file.rs     |  6 +++++
 modelator/src/module/tla/mod.rs        | 32 +++++++++++++++++++++++---
 modelator/src/module/tlc/mod.rs        |  1 +
 4 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/modelator/src/artifact/tla_cfg_file.rs b/modelator/src/artifact/tla_cfg_file.rs
index ce166bd5..dfe1e8ef 100644
--- a/modelator/src/artifact/tla_cfg_file.rs
+++ b/modelator/src/artifact/tla_cfg_file.rs
@@ -24,3 +24,9 @@ where
         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)
+    }
+}
diff --git a/modelator/src/artifact/tla_file.rs b/modelator/src/artifact/tla_file.rs
index 9ff69c50..5b6720af 100644
--- a/modelator/src/artifact/tla_file.rs
+++ b/modelator/src/artifact/tla_file.rs
@@ -39,3 +39,9 @@ where
         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)
+    }
+}
diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs
index a2735ec7..44c2f486 100644
--- a/modelator/src/module/tla/mod.rs
+++ b/modelator/src/module/tla/mod.rs
@@ -24,6 +24,7 @@ impl Tla {
         tla_tests_file: TlaFile,
         tla_config_file: TlaConfigFile,
     ) -> Result<Vec<(TlaFile, TlaConfigFile)>, Error> {
+        tracing::debug!("Tla::generate_tests {} {}", tla_tests_file, tla_config_file);
         // check that the tla tests file exists
         if !tla_tests_file.path().is_file() {
             return Err(Error::FileNotFound(tla_tests_file.path().clone()));
@@ -43,14 +44,13 @@ impl Tla {
         let tla_tests_module_name = tla_tests_file.tla_module_name().unwrap();
 
         // TODO: retrieve test names from tla tests file
-        let test_names = Vec::new();
-        test_names
+        extract_test_names(&tla_tests_file)?
             .into_iter()
             .map(|test_name| {
                 generate_test(
                     &tla_tests_dir,
                     &tla_tests_module_name,
-                    test_name,
+                    &test_name,
                     &tla_config_file,
                 )
             })
@@ -58,6 +58,32 @@ impl Tla {
     }
 }
 
+fn extract_test_names(tla_test_file: &TlaFile) -> Result<Vec<String>, Error> {
+    let content = std::fs::read_to_string(tla_test_file.path()).map_err(Error::IO)?;
+    let test_names = content
+        .lines()
+        .filter_map(|line| {
+            // take the first element in the split
+            line.trim().split("==").next()
+        })
+        .filter_map(|name| {
+            let name = name.trim();
+            // consider this as a test name if it starts/ends Test
+            if name.starts_with("Test") || name.ends_with("Test") {
+                Some(name.to_string())
+            } else {
+                None
+            }
+        })
+        .collect();
+    tracing::debug!(
+        "test names extracted from {}:\n{:?}",
+        tla_test_file,
+        test_names
+    );
+    Ok(test_names)
+}
+
 fn generate_test(
     tla_tests_dir: &PathBuf,
     tla_tests_module_name: &str,
diff --git a/modelator/src/module/tlc/mod.rs b/modelator/src/module/tlc/mod.rs
index 3cdae3b7..5631ac81 100644
--- a/modelator/src/module/tlc/mod.rs
+++ b/modelator/src/module/tlc/mod.rs
@@ -17,6 +17,7 @@ impl Tlc {
         tla_config_file: TlaConfigFile,
         options: &Options,
     ) -> Result<TlaTrace, Error> {
+        tracing::debug!("Tlc::test {} {} {:?}", tla_file, tla_config_file, options);
         // create tlc command
         let mut cmd = cmd(tla_file.path(), tla_config_file.path(), options);
 

From 23cd2c6773a97ca864fc50d72deabd26467956e7 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 18:35:00 +0100
Subject: [PATCH 7/9] tla: ignore commented out tests

---
 modelator/src/module/tla/mod.rs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs
index 44c2f486..e8166f98 100644
--- a/modelator/src/module/tla/mod.rs
+++ b/modelator/src/module/tla/mod.rs
@@ -68,8 +68,12 @@ fn extract_test_names(tla_test_file: &TlaFile) -> Result<Vec<String>, Error> {
         })
         .filter_map(|name| {
             let name = name.trim();
-            // consider this as a test name if it starts/ends Test
-            if name.starts_with("Test") || name.ends_with("Test") {
+            // consider this as a test name if:
+            // - it starts/ends Test
+            // - it's not commented out
+            let is_test = name.starts_with("Test") || name.ends_with("Test");
+            let is_commented_out = name.starts_with("\\*") || name.starts_with("(*");
+            if is_test && !is_commented_out {
                 Some(name.to_string())
             } else {
                 None

From 08af3868e220d33354d1583f52ebc2986cf34444 Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 18:55:24 +0100
Subject: [PATCH 8/9] tla_trace: implement Display

---
 modelator/src/artifact/tla_trace.rs | 9 +++++++++
 modelator/src/main.rs               | 6 +++++-
 modelator/src/module/tla/mod.rs     | 2 +-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs
index 6d7850bc..09e325f1 100644
--- a/modelator/src/artifact/tla_trace.rs
+++ b/modelator/src/artifact/tla_trace.rs
@@ -27,3 +27,12 @@ impl IntoIterator for TlaTrace {
         self.states.into_iter()
     }
 }
+
+impl std::fmt::Display for TlaTrace {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        for state in self.states.iter() {
+            write!(f, "{}", state)?;
+        }
+        Ok(())
+    }
+}
diff --git a/modelator/src/main.rs b/modelator/src/main.rs
index aee6f5ff..4209df0a 100644
--- a/modelator/src/main.rs
+++ b/modelator/src/main.rs
@@ -2,7 +2,11 @@ use modelator::{Error, Options};
 
 fn main() -> Result<(), Error> {
     let options = Options::default();
-    let traces = modelator::traces("IBCTests.tla", "IBCTests.cfg", options)?;
+    let traces = modelator::traces(
+        "../ibc-rs/modules/tests/support/model_based/IBCTests.tla",
+        "../ibc-rs/modules/tests/support/model_based/IBCTests.cfg",
+        options,
+    )?;
 
     // aggregate all traces into a json array (and each trace into a json array
     // as well)
diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs
index e8166f98..6e4d22f5 100644
--- a/modelator/src/module/tla/mod.rs
+++ b/modelator/src/module/tla/mod.rs
@@ -11,7 +11,7 @@ pub struct Tla;
 impl Tla {
     // #[modelator::method]
     pub fn tla_trace_to_json_trace(tla_trace: TlaTrace) -> Result<JsonTrace, Error> {
-        tracing::debug!("Tla::tla_trace_to_json_trace:\n{:#?}", tla_trace);
+        tracing::debug!("Tla::tla_trace_to_json_trace:\n{}", tla_trace);
         let states: Vec<JsonValue> = tla_trace
             .into_iter()
             .map(|state| json::state_to_json(&state))

From 1136669af485f89f252b4c53c0ae919401fd5edc Mon Sep 17 00:00:00 2001
From: Vitor Enes <vitorenesduarte@gmail.com>
Date: Thu, 11 Mar 2021 19:00:15 +0100
Subject: [PATCH 9/9] tla_trace: improve Display

---
 modelator/src/artifact/tla_trace.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs
index 09e325f1..6273cea2 100644
--- a/modelator/src/artifact/tla_trace.rs
+++ b/modelator/src/artifact/tla_trace.rs
@@ -30,8 +30,8 @@ impl IntoIterator for TlaTrace {
 
 impl std::fmt::Display for TlaTrace {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        for state in self.states.iter() {
-            write!(f, "{}", state)?;
+        for (index, state) in self.states.iter().enumerate() {
+            write!(f, "State{} ==\n{}", index + 1, state)?;
         }
         Ok(())
     }