Support Apalache v0.17.5

.changelog/unreleased/improvements/rust/135-bump-apalache.md

@@ -0,0 +1 @@
+Update Apalache to `v0.17.5`.

rs/modelator/src/jar.rs

@@ -10,9 +10,18 @@ const MIN_JAVA_VERSION: usize = 8;
 
 pub(crate) const TLA_JAR: &str = "tla2tools-v1.8.0.jar";
 pub(crate) const COMMUNITY_MODULES_JAR: &str = "CommunityModules-202103092123.jar";
-pub(crate) const APALACHE_JAR: &str = "apalache-pkg-0.15.13-full.jar";
+pub(crate) const APALACHE_JAR: &str = "apalache-pkg-0.17.5-full.jar";
+
+/* To update to new checksum, execute
+cd jars/
+LC_COLLATE=C sort <<EOF | xargs cat | sha256sum
+tla2tools-v1.8.0.jar
+CommunityModules-202103092123.jar
+apalache-pkg-0.17.5-full.jar
+EOF
+*/
 pub(crate) const JARS_CHECKSUM: &str =
-    "d99b5645fbf6986bfbe50895f2b02d9268f3595a171f2bfffc989979d8f2c8bf";
+    "fa5c17bfe6adf631e2d0250de5a8f905e9e41a0ead837608f8c35d131077a9c2";
 
 #[derive(Debug, Hash, PartialEq, Eq, Clone, Copy)]
 pub(crate) enum Jar {
@@ -45,8 +54,9 @@ impl Jar {
     }
 
     fn link(&self) -> String {
+        // TODO: change to `main` branch after merge
         format!(
-            "https://github.com/informalsystems/modelator/raw/main/jars/{}",
+            "https://github.com/informalsystems/modelator/raw/rnbguy/rust/support-latest-apalache/jars/{}",
             self.file_name()
         )
     }

rs/modelator/src/model/checker/apalache/cmd_output.rs

@@ -23,19 +23,15 @@ fn is_counterexample_line(line: &str) -> bool {
 fn parse_filename(line: &str) -> String {
     // The line looks like '...d. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@11:13:37.003'
     assert!(is_counterexample_line(line));
-    match line.find("in:") {
-        None => {
-            panic!("Expected to find substring 'in:' in line when parsing for counterexample file name")
-        }
-        Some(ix) => {
-            let slice = &line[ix..];
-            let mut split = slice.split(' ');
-            // Now have [:, counterexample.tla,, ...]
-            split.next();
-            let with_trailing_comma = split.next().unwrap();
-            with_trailing_comma[..with_trailing_comma.len() - 1].to_owned()
-        }
-    }
+    let (_, files) = line.split_once("in:").expect(
+        "Expected to find substring 'in:' in line when parsing for counterexample file name",
+    );
+    let tla_file = files
+        .trim()
+        .split_whitespace()
+        .next()
+        .expect("Must have counterexample1.tla, MC1.OUT, counterexample1.json");
+    tla_file.trim().into()
 }
 
 fn is_deadlock_line(line: &str) -> bool {
@@ -59,8 +55,22 @@ impl CmdOutput {
     pub(crate) fn apalache_stdout_error_lines(&self) -> Vec<String> {
         self.stdout
             .iter()
+            .scan(Vec::new(), |state, line| {
+                state.push(line.clone());
+                // Looking for E@XX:XX:XX.XXX lines
+                if line.len() >= 14 && &line[(line.len() - 14)..(line.len() - 12)] == "E@" {
+                    let next_state = state.join("\n");
+                    *state = Vec::new();
+                    Some(Some(next_state))
+                } else if line.len() >= 14 && &line[(line.len() - 13)..(line.len() - 12)] == "@" {
+                    *state = Vec::new();
+                    Some(None)
+                } else {
+                    Some(None)
+                }
+            })
+            .flatten()
             .filter(|line| is_error_line(line))
-            .map(ToString::to_string)
             .collect()
     }
 
@@ -136,14 +146,14 @@ mod tests {
 
     #[test]
     fn test_is_error_line() {
-        let line = "State 2: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@11:13:37.003";
+        let line = "State 2: state invariant 0 violated. Check the counterexample in:\n  counterexample1.tla\n  MC1.out\n  counterexample1.json E@11:13:37.003";
         let res = is_error_line(line);
         assert!(res);
     }
 
     #[test]
     fn test_parse_filename() {
-        let line = "State 2: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@11:13:37.003";
+        let line = "State 2: state invariant 0 violated. Check the counterexample in:\n  counterexample1.tla\n  MC1.out\n  counterexample1.json E@11:13:37.003";
         let res = parse_filename(line);
         assert_eq!("counterexample1.tla".to_owned(), res);
     }
@@ -152,8 +162,14 @@ mod tests {
     fn test_parse_all_counterexample_filenames() {
         let to_parse = r#"PASS #13: BoundedChecker                                          I@11:13:35.033
 State 2: Checking 1 state invariants                              I@11:13:36.959
-State 2: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@11:13:37.003
-State 2: state invariant 0 violated. Check the counterexample in: counterexample2.tla, MC2.out, counterexample2.json E@11:13:37.015
+State 2: state invariant 0 violated. Check the counterexample in:
+  counterexample1.tla
+  MC1.out
+  counterexample1.json E@11:13:37.003
+State 2: state invariant 0 violated. Check the counterexample in:
+  counterexample2.tla
+  MC2.out
+  counterexample2.json E@11:13:37.015
 Found 2 error(s)                                                  I@11:13:37.017
 Total time: 4.857 sec                                             I@11:13:37.020
 EXITCODE: ERROR (12)