Only create TlaFile and TlaConfigFile artifacts if the corresponding …

…file exists

modelator/src/artifact/tla_cfg_file.rs

@@ -1,4 +1,5 @@
 use crate::Error;
+use std::convert::TryFrom;
 use std::path::{Path, PathBuf};
 
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -7,27 +8,38 @@ pub struct TlaConfigFile {
 }
 
 impl TlaConfigFile {
-    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
-        Self {
-            path: path.as_ref().to_path_buf(),
-        }
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+        let path = path.as_ref().to_path_buf();
+        crate::util::check_file_existence(&path)?;
+        Ok(Self { path })
     }
 
     pub fn path(&self) -> &PathBuf {
         &self.path
     }
+}
+
+// TODO: replace the following `TryFrom` implementations with one with generic
+//       bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
+//       is fixed
+impl TryFrom<String> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: String) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
 
-    pub(crate) fn check_existence(&self) -> Result<(), Error> {
-        crate::util::check_file_existence(&self.path)
+impl TryFrom<&Path> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: &Path) -> Result<Self, Self::Error> {
+        Self::new(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 TryFrom<PathBuf> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: PathBuf) -> Result<Self, Self::Error> {
+        Self::new(path)
     }
 }
 

modelator/src/artifact/tla_file.rs

@@ -1,4 +1,5 @@
 use crate::Error;
+use std::convert::TryFrom;
 use std::path::{Path, PathBuf};
 
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -7,20 +8,16 @@ pub struct TlaFile {
 }
 
 impl TlaFile {
-    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
-        Self {
-            path: path.as_ref().to_path_buf(),
-        }
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+        let path = path.as_ref().to_path_buf();
+        crate::util::check_file_existence(&path)?;
+        Ok(Self { path })
     }
 
     pub fn path(&self) -> &PathBuf {
         &self.path
     }
 
-    pub(crate) fn check_existence(&self) -> Result<(), Error> {
-        crate::util::check_file_existence(&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> {
@@ -37,12 +34,27 @@ impl TlaFile {
     }
 }
 
-impl<P> From<P> for TlaFile
-where
-    P: AsRef<Path>,
-{
-    fn from(path: P) -> Self {
-        Self::new(path.as_ref().to_path_buf())
+// TODO: replace the following `TryFrom` implementations with one with generic
+//       bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
+//       is fixed
+impl TryFrom<String> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: String) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
+
+impl TryFrom<&Path> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: &Path) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
+
+impl TryFrom<PathBuf> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: PathBuf) -> Result<Self, Self::Error> {
+        Self::new(path)
     }
 }
 

modelator/src/cli/mod.rs

@@ -55,6 +55,11 @@ pub enum ApalacheMethods {
         /// TLA+ config file generated by the generate-test method in the TLA module.
         tla_config_file: String,
     },
+    /// Parse a TLA+ file.
+    Parse {
+        /// TLA+ file to be parsed.
+        tla_file: String,
+    },
 }
 
 #[derive(Debug, Clap)]
@@ -105,7 +110,10 @@ impl TlaMethods {
     }
 
     fn generate_tests(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
-        let tests = crate::module::Tla::generate_tests(tla_file.into(), tla_config_file.into())?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        let tests = crate::module::Tla::generate_tests(tla_file, tla_config_file)?;
         tracing::debug!("Tla::generate_tests output {:#?}", tests);
 
         generated_tests(tests)
@@ -135,17 +143,30 @@ impl ApalacheMethods {
                 tla_file,
                 tla_config_file,
             } => Self::test(tla_file, tla_config_file),
+            Self::Parse { tla_file } => Self::parse(tla_file),
         }
     }
 
     fn test(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
         let options = crate::Options::default();
-        let tla_trace =
-            crate::module::Apalache::test(tla_file.into(), tla_config_file.into(), &options)?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        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)
     }
+
+    fn parse(tla_file: String) -> Result<JsonValue, Error> {
+        let options = crate::Options::default();
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_file_parsed = crate::module::Apalache::parse(tla_file, &options)?;
+        tracing::debug!("Apalache::parse output {}", tla_file_parsed);
+
+        parsed_tla_file(tla_file_parsed)
+    }
 }
 
 impl TlcMethods {
@@ -160,8 +181,10 @@ impl TlcMethods {
 
     fn test(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
         let options = crate::Options::default();
-        let tla_trace =
-            crate::module::Tlc::test(tla_file.into(), tla_config_file.into(), &options)?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        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)
@@ -198,3 +221,10 @@ fn save_json_trace(json_trace: JsonTrace) -> Result<JsonValue, Error> {
         "json_trace_file": crate::util::absolute_path(&path),
     }))
 }
+
+#[allow(clippy::unnecessary_wraps)]
+fn parsed_tla_file(tla_file_parsed: TlaFile) -> Result<JsonValue, Error> {
+    Ok(json!({
+        "tla_file": format!("{}", tla_file_parsed),
+    }))
+}

modelator/src/lib.rs

@@ -43,7 +43,10 @@ pub fn traces<P: AsRef<Path>>(
     setup(&options)?;
 
     // generate tla tests
-    let tests = module::Tla::generate_tests(tla_tests_file.into(), tla_config_file.into())?;
+    use std::convert::TryFrom;
+    let tla_tests_file = artifact::TlaFile::try_from(tla_tests_file.as_ref())?;
+    let tla_config_file = artifact::TlaConfigFile::try_from(tla_config_file.as_ref())?;
+    let tests = module::Tla::generate_tests(tla_tests_file, tla_config_file)?;
 
     // run the model checker configured on each tla test
     let traces = tests

modelator/src/module/apalache/mod.rs

@@ -24,10 +24,6 @@ impl Apalache {
             options
         );
 
-        // check that the tla file and tla cfg file exist
-        tla_file.check_existence()?;
-        tla_config_file.check_existence()?;
-
         // load cache and check if the result is cached
         let mut cache = TlaTraceCache::new(options)?;
         let cache_key = TlaTraceCache::key(&tla_file, &tla_config_file)?;
@@ -60,20 +56,26 @@ impl Apalache {
     pub fn parse(tla_file: TlaFile, options: &Options) -> Result<TlaFile, Error> {
         tracing::debug!("Apalache::parse {} {:?}", tla_file, options);
 
-        // check that the tla file and tla cfg file exist
-        tla_file.check_existence()?;
+        // compute the directory in which the tla file is stored
+        let mut tla_dir = tla_file.path().clone();
+        assert!(tla_dir.pop());
 
-        // compute the output tla file; it's okay to unwrap as we have already
+        // compute tla module name: it's okay to unwrap as we have already
         // verified that the file exists
         let tla_module_name = tla_file.tla_module_name().unwrap();
-        let tla_parsed_file: TlaFile = format!("{}Parsed.tla", tla_module_name).into();
+
+        // compute the output tla file
+        let tla_parsed_file = tla_dir.join(format!("{}Parsed.tla", tla_module_name));
 
         // create apalache parse command
-        let cmd = parse_cmd(tla_file.path(), tla_parsed_file.path(), options);
+        let cmd = parse_cmd(tla_file.path(), &tla_parsed_file, options);
 
         // run apalache
         run_apalache(cmd, options)?;
 
+        // create tla file
+        use std::convert::TryFrom;
+        let tla_parsed_file = TlaFile::try_from(tla_parsed_file)?;
         Ok(tla_parsed_file)
     }
 }

modelator/src/module/tla/mod.rs

@@ -27,10 +27,6 @@ impl Tla {
     ) -> Result<Vec<(TlaFile, TlaConfigFile)>, Error> {
         tracing::debug!("Tla::generate_tests {} {}", tla_tests_file, tla_config_file);
 
-        // check that the tla tests file and tla cfg file exist
-        tla_tests_file.check_existence()?;
-        tla_config_file.check_existence()?;
-
         // 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());
@@ -119,7 +115,11 @@ fn generate_test(
     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()))
+    // create tla file and tla config file
+    use std::convert::TryFrom;
+    let test_module_file = TlaFile::try_from(test_module_file)?;
+    let test_config_file = TlaConfigFile::try_from(test_config_file)?;
+    Ok((test_module_file, test_config_file))
 }
 
 fn genereate_test_module(

modelator/src/module/tlc/mod.rs

@@ -19,10 +19,6 @@ impl Tlc {
     ) -> Result<TlaTrace, Error> {
         tracing::debug!("Tlc::test {} {} {:?}", tla_file, tla_config_file, options);
 
-        // check that the tla file and tla cfg file exist
-        tla_file.check_existence()?;
-        tla_config_file.check_existence()?;
-
         // load cache and check if the result is cached
         let mut cache = TlaTraceCache::new(options)?;
         let cache_key = TlaTraceCache::key(&tla_file, &tla_config_file)?;

modelator/tests/integration/main.rs

@@ -1,7 +1,7 @@
 // We follow the approach proposed in the following link for integration tests:
 // https://matklad.github.io/2021/02/27/delete-cargo-integration-tests.html
 
-use modelator::artifact::JsonTrace;
+use modelator::artifact::{JsonTrace, TlaFile};
 use modelator::{CliOptions, CliStatus, Error, ModelChecker, ModelCheckerOptions, Options};
 use once_cell::sync::Lazy;
 use serde_json::{json, Value as JsonValue};
@@ -58,8 +58,10 @@ fn all_tests(model_checker: ModelChecker) -> Result<(), Error> {
 
             // parse file if apalache and simply assert it works
             if model_checker == ModelChecker::Apalache {
+                use std::convert::TryFrom;
+                let tla_tests_file = TlaFile::try_from(tla_tests_file.as_ref()).unwrap();
                 let tla_parsed_file =
-                    modelator::module::Apalache::parse(tla_tests_file.into(), &options).unwrap();
+                    modelator::module::Apalache::parse(tla_tests_file, &options).unwrap();
                 std::fs::remove_file(tla_parsed_file.path()).unwrap();
             }
         }