#414: full model-based test TLA+ -> Apalache -> Jsonatr -> lite::veri…

…fy_single

tendermint/tests/lite-model-based.rs

@@ -5,7 +5,7 @@ use tendermint::block::{Header};
 use tendermint::lite::{TrustThresholdFraction, TrustedState};
 
 mod utils;
-use utils::{*, apalache::*, command::*, lite::*};
+use utils::{*, apalache::*, jsonatr::*, command::*, lite::*};
 
 type Trusted = lite::TrustedState<SignedHeader, Header>;
 
@@ -103,21 +103,24 @@ fn single_step_test() {
 
 #[test]
 fn apalache_test() {
-
-    println!("Apalache: {}", Command::exists_program("apalache-mc"));
-    println!("Jsonatr: {}", Command::exists_program("jsonatr"));
+    assert!(Command::exists_program("apalache-mc"));
+    assert!(Command::exists_program("jsonatr"));
 
     let test = ApalacheTestCase {
         model: "MC4_4_faulty.tla".to_string(),
         test: "TestFailureInv".to_string(),
         length: None,
         timeout: None
     };
-    match run_apalache_test("tests/support/lite-model-based", test) {
-        Ok(run) => {
-            eprintln!("Stdout: {}", run.stdout);
-            eprintln!("Stderr: {}", run.stderr)
-        },
-        Err(e) => eprintln!("ERR: {}", e.to_string())
-    }
+    assert!(run_apalache_test(TEST_DIR, test).is_ok());
+
+    let transform = JsonatrTransform {
+        input: "counterexample.json".to_string(),
+        include: vec!["../../utils/jsonatr-lib/apalache_to_lite_test.json".to_string()],
+        output: "lite_test.json".to_string()
+    };
+    assert!(run_jsonatr_transform(TEST_DIR, transform).is_ok());
+
+    let tc = read_single_step_test(TEST_DIR, "lite_test.json");
+    run_single_step_test(&tc);
 }

tendermint/tests/utils/jsonatr.rs

@@ -20,6 +20,9 @@ pub fn run_jsonatr_transform(dir: &str, transform: JsonatrTransform) -> io::Resu
         cmd.arg("--use");
         cmd.arg(&include);
     }
+    if !dir.is_empty() {
+        cmd.current_dir(dir);
+    }
     match cmd.spawn() {
         Ok(run) => {
             if run.status.success() {