From traits for crate Error (#68)

* impl From for Error

* catch error message from TLC (#52)

modelator/src/cache/mod.rs

@@ -17,7 +17,7 @@ impl Cache {
     pub(crate) fn new(options: &Options) -> Result<Self, Error> {
         // create cache dir (if it doesn't exist)
         let cache_dir = options.dir.join("cache");
-        std::fs::create_dir_all(&cache_dir).map_err(Error::io)?;
+        std::fs::create_dir_all(&cache_dir)?;
 
         // read files the cache directory
         let cached_keys = crate::util::read_dir(&cache_dir)?;
@@ -33,7 +33,7 @@ impl Cache {
         let value = if self.cached_keys.contains(key) {
             // if this key is cached, read it from disk
             let path = self.key_path(key);
-            let value = std::fs::read_to_string(path).map_err(Error::io)?;
+            let value = std::fs::read_to_string(path)?;
             Some(value)
         } else {
             None
@@ -51,7 +51,7 @@ impl Cache {
 
         // write the value associated with this key to disk
         let path = self.key_path(&key);
-        std::fs::write(path, value).map_err(Error::io)?;
+        std::fs::write(path, value)?;
 
         // mark the key as cached
         self.cached_keys.insert(key);

modelator/src/cli/mod.rs

@@ -127,9 +127,7 @@ impl TlaMethods {
         if !tla_trace_file.is_file() {
             return Err(Error::FileNotFound(tla_trace_file.to_path_buf()));
         }
-        let tla_trace = std::fs::read_to_string(&tla_trace_file)
-            .map_err(Error::io)?
-            .parse()?;
+        let tla_trace = std::fs::read_to_string(&tla_trace_file)?.parse()?;
 
         let json_trace = crate::module::Tla::tla_trace_to_json_trace(tla_trace)?;
         tracing::debug!("Tla::tla_trace_to_json_trace output {}", json_trace);
@@ -210,15 +208,15 @@ fn generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result<JsonValue, Er
 
 fn save_tla_trace(tla_trace: TlaTrace) -> Result<JsonValue, Error> {
     let path = Path::new("trace.tla").to_path_buf();
-    std::fs::write(&path, format!("{}", tla_trace)).map_err(Error::io)?;
+    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> {
     let path = Path::new("trace.json").to_path_buf();
-    std::fs::write(&path, format!("{}", json_trace)).map_err(Error::io)?;
+    std::fs::write(&path, format!("{}", json_trace))?;
     Ok(json!({
         "json_trace_file": crate::util::absolute_path(&path),
     }))

modelator/src/error.rs

@@ -63,16 +63,20 @@ pub enum Error {
     JsonParseError(String),
 }
 
-impl Error {
-    pub(crate) fn io(err: std::io::Error) -> Error {
+impl From<std::io::Error> for Error {
+    fn from(err: std::io::Error) -> Self {
         Error::IO(err.to_string())
     }
+}
 
-    pub(crate) fn ureq(err: ureq::Error) -> Error {
+impl From<ureq::Error> for Error {
+    fn from(err: ureq::Error) -> Self {
         Error::Ureq(err.to_string())
     }
+}
 
-    pub(crate) fn nom(err: nom::Err<nom::error::Error<&str>>) -> Error {
+impl From<nom::Err<nom::error::Error<&str>>> for Error {
+    fn from(err: nom::Err<nom::error::Error<&str>>) -> Self {
         Error::Nom(err.to_string())
     }
 }

modelator/src/jar.rs

@@ -57,13 +57,13 @@ impl Jar {
         let path = self.path(&modelator_dir);
 
         // download the jar
-        let response = ureq::get(&self.link()).call().map_err(Error::ureq)?;
+        let response = ureq::get(&self.link()).call()?;
         let mut reader = response.into_reader();
 
         // write jar bytes to the file
-        let file = std::fs::File::create(path).map_err(Error::io)?;
+        let file = std::fs::File::create(path)?;
         let mut file_writer = std::io::BufWriter::new(file);
-        std::io::copy(&mut reader, &mut file_writer).map_err(Error::io)?;
+        std::io::copy(&mut reader, &mut file_writer)?;
         Ok(())
     }
 
@@ -99,8 +99,8 @@ pub(crate) fn download_jars<P: AsRef<Path>>(modelator_dir: P) -> Result<(), Erro
             eprintln!("[modelator] Checksum of downloaded jars does not match the expected. Will try again!");
 
             // delete modelator dir and create it again
-            std::fs::remove_dir_all(&modelator_dir).map_err(Error::io)?;
-            std::fs::create_dir(&modelator_dir).map_err(Error::io)?;
+            std::fs::remove_dir_all(&modelator_dir)?;
+            std::fs::create_dir(&modelator_dir)?;
 
             // try to download jars again
             return download_jars(modelator_dir);

modelator/src/lib.rs

@@ -91,13 +91,13 @@ pub fn traces<P: AsRef<Path>>(
     setup(options)?;
 
     // create a temporary directory, and copy TLA+ files there
-    let dir = tempdir().map_err(Error::io)?;
+    let dir = tempdir()?;
     let tla_tests_file = util::copy_files_into("tla", tla_tests_file, dir.path())?;
     let tla_config_file = util::copy_files_into("cfg", tla_config_file, dir.path())?;
 
     // save the current, and change to the temporary directory
-    let current_dir = env::current_dir().map_err(Error::io)?;
-    env::set_current_dir(dir.path()).map_err(Error::io)?;
+    let current_dir = env::current_dir()?;
+    env::set_current_dir(dir.path())?;
 
     // generate tla tests
     use std::convert::TryFrom;
@@ -119,9 +119,9 @@ pub fn traces<P: AsRef<Path>>(
         .collect::<Result<Vec<_>, _>>()?;
 
     // cleanup everything by removing the temporary directory
-    dir.close().map_err(Error::io)?;
+    dir.close()?;
     // restore the current directory
-    env::set_current_dir(current_dir).map_err(Error::io)?;
+    env::set_current_dir(current_dir)?;
 
     // convert each tla trace to json
     traces
@@ -380,7 +380,7 @@ pub(crate) fn setup(options: &Options) -> Result<(), 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)?;
+        std::fs::create_dir_all(&options.dir)?;
     }
 
     // download missing jars

modelator/src/module/apalache/mod.rs

@@ -65,7 +65,7 @@ impl Apalache {
         // convert apalache counterexample to a trace
         let counterexample_path = Path::new("counterexample.tla");
         if counterexample_path.is_file() {
-            let counterexample = std::fs::read_to_string(counterexample_path).map_err(Error::io)?;
+            let counterexample = std::fs::read_to_string(counterexample_path)?;
             tracing::debug!("Apalache counterexample:\n{}", counterexample);
             let trace = counterexample::parse(counterexample)?;
 
@@ -128,7 +128,7 @@ impl Apalache {
 fn run_apalache(mut cmd: Command, options: &Options) -> Result<String, Error> {
     // start apalache
     // TODO: add timeout
-    let output = cmd.output().map_err(Error::io)?;
+    let output = cmd.output()?;
 
     // get apalache stdout and stderr
     let stdout = crate::util::cmd_output_to_string(&output.stdout);
@@ -141,7 +141,7 @@ fn run_apalache(mut cmd: Command, options: &Options) -> Result<String, Error> {
             // apalache writes all its output to the stdout
 
             // save apalache log
-            std::fs::write(&options.model_checker_options.log, &stdout).map_err(Error::io)?;
+            std::fs::write(&options.model_checker_options.log, &stdout)?;
 
             // check if a failure has occurred
             if stdout.contains("EXITCODE: ERROR") {

modelator/src/module/tla/json/mod.rs

@@ -13,5 +13,5 @@ pub(crate) fn state_to_json(state: &str) -> Result<JsonValue, Error> {
             );
             value
         })
-        .map_err(Error::nom)
+        .map_err(Into::into)
 }

modelator/src/module/tla/mod.rs

@@ -100,7 +100,7 @@ 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 content = std::fs::read_to_string(tla_test_file.path())?;
     let test_names = content
         .lines()
         .filter_map(|line| {
@@ -150,11 +150,11 @@ fn generate_test(
 
     // 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)?;
+    std::fs::write(&test_module_file, test_module)?;
 
     // write test config to test config file
     let test_config_file = tla_tests_dir.join(format!("{}.cfg", test_module_name));
-    std::fs::write(&test_config_file, test_config).map_err(Error::io)?;
+    std::fs::write(&test_config_file, test_config)?;
 
     // create tla file and tla config file
     use std::convert::TryFrom;
@@ -184,7 +184,7 @@ 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()).map_err(Error::io)?;
+    let tla_config = std::fs::read_to_string(tla_config_file.path())?;
     Ok(format!(
         r#"
 {}

modelator/src/module/tlc/mod.rs

@@ -55,7 +55,7 @@ impl Tlc {
 
         // start tlc
         // TODO: add timeout
-        let output = cmd.output().map_err(Error::io)?;
+        let output = cmd.output()?;
 
         // get tlc stdout and stderr
         let stdout = crate::util::cmd_output_to_string(&output.stdout);
@@ -69,7 +69,7 @@ impl Tlc {
                 // occurred
 
                 // save tlc log
-                std::fs::write(&options.model_checker_options.log, &stdout).map_err(Error::io)?;
+                std::fs::write(&options.model_checker_options.log, &stdout)?;
                 tracing::debug!(
                     "TLC log written to {}",
                     crate::util::absolute_path(&options.model_checker_options.log)

modelator/src/module/tlc/output.rs

@@ -1,23 +1,95 @@
 use crate::artifact::tla_trace::{TlaState, TlaTrace};
 use crate::{Error, ModelCheckerOptions};
 
+use std::collections::HashMap;
+
 pub(crate) fn parse(output: String, options: &ModelCheckerOptions) -> Result<Vec<TlaTrace>, Error> {
-    let mut traces = Vec::new();
-    let mut lines = output.lines();
+    let mut parsed_output: HashMap<u8, HashMap<usize, Vec<String>>> = HashMap::new();
+
+    let mut curr_message_id = None;
+    let mut curr_message = String::new();
+
+    output.lines().for_each(|line| {
+        if line.starts_with("@!@!@STARTMSG ") {
+            // without annotattion
+            let (code, class) = curr_message_id.take().unwrap_or((0, 0));
+            parsed_output
+                .entry(class)
+                .or_default()
+                .entry(code)
+                .or_default()
+                .push(curr_message.drain(..).collect());
 
-    while let Some(line) = lines.next() {
-        // check if found the beginning of the next trace
-        if line.starts_with("@!@!@ENDMSG 2121 @!@!@") {
-            if let Some(trace) = parse_trace(&mut lines, options)? {
-                traces.push(trace);
+            let (code, class) = line.splitn(3, ' ').nth(1).unwrap().split_once(':').unwrap();
+            curr_message_id.insert((code.parse().unwrap(), class.parse().unwrap()));
+        } else if line.starts_with("@!@!@ENDMSG ") {
+            let (code, class) = curr_message_id.take().unwrap_or((0, 0));
+            parsed_output
+                .entry(class)
+                .or_default()
+                .entry(code)
+                .or_default()
+                .push(curr_message.drain(..).collect());
+
+            let c_code = line.splitn(3, ' ').nth(1).unwrap();
+            assert_eq!(code, c_code.parse::<usize>().unwrap());
+        } else {
+            curr_message.push_str(line);
+            curr_message.push('\n');
+        }
+    });
+
+    if let Some(lines) = parsed_output.get(&4).and_then(|x| x.get(&2217)) {
+        let mut traces = Vec::new();
+        let mut trace = None;
+        for line in lines {
+            if line.starts_with("1: <Initial predicate>") {
+                // start of new trace
+                if let Some(t) = trace.take() {
+                    traces.push(t)
+                }
+                trace = Some(TlaTrace::new());
+            }
+            if let Some(t) = trace.as_mut() {
+                t.add(line.split_once('\n').unwrap().1.into());
             }
         }
+        // last trace
+        if let Some(t) = trace.take() {
+            traces.push(t)
+        }
+        Ok(traces)
+    } else if let Some(errors) = parsed_output.get(&1) {
+        // Message Codes ref
+        // https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/output/EC.java
+        // Message Classes ref
+        // https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/output/MP.java
+        // NONE = 0; ERROR = 1; TLCBUG = 2; WARNING = 3; STATE = 4;
+
+        let message = errors
+            .iter()
+            .map(|(code, message)| {
+                format!(
+                    "[{}:{}]: {}",
+                    options.log.to_string_lossy(),
+                    code,
+                    &message
+                        .iter()
+                        .map(|x| x.trim().replace("\n", " "))
+                        .collect::<Vec<_>>()
+                        .join(" ")
+                )
+            })
+            .collect::<Vec<_>>()
+            .join("\n");
+        Err(Error::TLCFailure(message))
+    } else {
+        Ok(vec![])
     }
-    Ok(traces)
 }
 
 fn parse_trace<'a>(
-    lines: &mut std::str::Lines<'a>,
+    lines: &mut impl Iterator<Item = &'a str>,
     options: &ModelCheckerOptions,
 ) -> Result<Option<TlaTrace>, Error> {
     let mut state_index = 0;

modelator/src/util.rs

@@ -33,11 +33,10 @@ pub(crate) fn absolute_path<P: AsRef<Path>>(path: P) -> String {
 
 pub(crate) fn read_dir<P: AsRef<Path>>(path: P) -> Result<HashSet<String>, Error> {
     let mut file_names = HashSet::new();
-    let files = std::fs::read_dir(path).map_err(Error::io)?;
+    let files = std::fs::read_dir(path)?;
     for file in files {
         // for each file in the modelator directory, check if it is a jar
-        let file_name = file
-            .map_err(Error::io)?
+        let file_name = file?
             .file_name()
             .into_string()
             .map_err(Error::InvalidUnicode)?;
@@ -64,13 +63,13 @@ pub(crate) mod digest {
     }
 
     fn digest_file(path: String, digest: &mut sha2::Sha256) -> Result<(), Error> {
-        let file = std::fs::File::open(path).map_err(Error::io)?;
+        let file = std::fs::File::open(path)?;
         let mut reader = std::io::BufReader::new(file);
 
         let mut buffer = [0; 1024];
         loop {
             use std::io::Read;
-            let count = reader.read(&mut buffer).map_err(Error::io)?;
+            let count = reader.read(&mut buffer)?;
             if count == 0 {
                 break;
             }
@@ -98,7 +97,7 @@ pub(crate) fn copy_files_into<P: AsRef<Path>, Q: AsRef<Path>>(
     for file in files {
         if let Some(file_name) = file.file_name() {
             let dest = dir.join(file_name);
-            copy(file, dest).map_err(Error::io)?;
+            copy(file, dest)?;
         }
     }
     // it is OK to unwrap, as the file has been checked before
@@ -127,8 +126,7 @@ fn list_files<P: AsRef<Path>>(ext: &str, file: P) -> Result<Vec<PathBuf>, Error>
         }
     });
     // Collect all files with the same extension in this directory
-    let files = std::fs::read_dir(dir)
-        .map_err(Error::io)?
+    let files = std::fs::read_dir(dir)?
         .flatten()
         .filter(|dir_entry| {
             dir_entry