TLA parser refactoring

modelator/Cargo.toml

@@ -16,7 +16,7 @@ authors = [
 [dependencies]
 clap = "=3.0.0-beta.4"
 hex = "0.4.3"
-nom = "6.2.1"
+nom = "7.0.0"
 serde = { version = "1.0.127", features = ["derive"] }
 serde_json = "1.0.66"
 sha2 = "0.9.5"

modelator/src/artifact/tla_trace.rs

@@ -1,6 +1,16 @@
 use crate::Error;
 use std::str::FromStr;
 
+use nom::{
+    branch::alt,
+    bytes::complete::{is_not, tag, tag_no_case, take_until},
+    character::complete::{alpha1, alphanumeric1, char, multispace0, multispace1},
+    combinator::{map, opt, recognize, rest},
+    multi::{many0, many1, separated_list0, separated_list1},
+    sequence::{delimited, pair, preceded, separated_pair, terminated, tuple},
+    IResult,
+};
+
 pub(crate) type TlaState = String;
 
 /// `modelator`'s artifact containing a test trace encoded as TLA+.
@@ -23,52 +33,127 @@ impl TlaTrace {
     }
 }
 
+fn tla_single_line_comment(i: &str) -> IResult<&str, &str> {
+    recognize(pair(tag("\\*"), is_not("\n\r")))(i)
+}
+
+fn tla_multi_line_comment(i: &'_ str) -> IResult<&str, &str> {
+    recognize(delimited(tag("(*"), take_until("*)"), tag("*)")))(i)
+}
+
+fn remove_tla_single_line_comments(i: &str) -> IResult<&str, String> {
+    map(
+        preceded(
+            opt(tla_single_line_comment),
+            separated_list0(tla_single_line_comment, alt((take_until("\\*"), rest))),
+        ),
+        |value| value.concat(),
+    )(i)
+}
+
+fn remove_tla_multi_line_comments(i: &str) -> IResult<&str, String> {
+    map(
+        preceded(
+            opt(tla_multi_line_comment),
+            separated_list0(tla_multi_line_comment, alt((take_until("(*"), rest))),
+        ),
+        |value| value.concat(),
+    )(i)
+}
+
+fn remove_tla_comments(i: &str) -> String {
+    let (_, s) = remove_tla_single_line_comments(i).unwrap();
+    let (_, s) = remove_tla_multi_line_comments(&s).unwrap();
+    s
+}
+
+#[derive(Debug)]
+struct TlaFile<'a> {
+    name: &'a str,
+    extends: Vec<&'a str>,
+    operators: Vec<(&'a str, &'a str)>,
+}
+
+fn tla_identifiers(i: &str) -> IResult<&str, &str> {
+    recognize(pair(
+        alt((alpha1, tag("_"))),
+        many0(alt((alphanumeric1, tag("_")))),
+    ))(i)
+}
+
+fn parse_tla_file(i: &str) -> IResult<&str, TlaFile<'_>> {
+    map(
+        terminated(
+            tuple((
+                terminated(
+                    delimited(
+                        many1(char('-')),
+                        delimited(
+                            multispace1,
+                            preceded(tag_no_case("MODULE "), tla_identifiers),
+                            multispace1,
+                        ),
+                        many1(char('-')),
+                    ),
+                    multispace1,
+                ),
+                terminated(
+                    preceded(
+                        tag_no_case("EXTENDS "),
+                        separated_list1(
+                            delimited(multispace0, char(','), multispace0),
+                            tla_identifiers,
+                        ),
+                    ),
+                    multispace1,
+                ),
+                separated_list1(
+                    multispace1,
+                    separated_pair(
+                        tla_identifiers,
+                        delimited(multispace0, tag("=="), multispace0),
+                        take_until("\n\n"),
+                    ),
+                ),
+            )),
+            delimited(multispace0, many1(char('=')), multispace0),
+        ),
+        |(name, extends, operators)| TlaFile {
+            name,
+            extends,
+            operators,
+        },
+    )(i)
+}
+
 impl FromStr for TlaTrace {
     type Err = Error;
 
     fn from_str(tla_trace: &str) -> Result<Self, Self::Err> {
-        let lines = tla_trace.lines();
-        let mut state_index = 0;
-        let mut state = None;
-        let mut trace = TlaTrace::new();
+        let tla_trace = remove_tla_comments(tla_trace);
 
-        for line in lines {
-            // check if found the start of the next state
-            let next_state = format!("State{} ==", state_index);
-            if line.starts_with(&next_state) {
-                if state_index > 0 {
-                    // the previous state has ended, so we save it
-                    let state = state
-                        .take()
-                        .expect("[modelator] a TLA trace state should have been started");
-                    trace.add(state);
-                }
-
-                // start a new state with the remaining of this line
-                let mut tla_state = TlaState::new();
-                // trim the prefix
-                let line = line.trim_start_matches(&next_state);
-                // save remaining of the line
-                tla_state.push_str(line);
-                tla_state.push('\n');
-                state = Some(tla_state);
-
-                state_index += 1;
-                continue;
-            }
-
-            // save any line if we have a state started
-            if let Some(state) = state.as_mut() {
-                state.push_str(line);
-                state.push('\n');
-            }
-        }
+        let tla = parse_tla_file(&tla_trace).unwrap().1;
+
+        let mut states: Vec<(usize, &str)> = tla
+            .operators
+            .into_iter()
+            .filter(|(identifier, _)| identifier.starts_with("State"))
+            .map(|(k, state)| (k[5..k.len()].parse().unwrap(), state))
+            .collect();
+
+        states.sort_unstable();
+        states.dedup_by_key(|(k, _)| *k);
 
-        // save the last state
-        let state = state
-            .take()
-            .expect("[modelator] a TLA trace should have at least one TLA state");
-        trace.add(state);
+        assert_eq!(
+            (states.first().unwrap().0, states.last().unwrap().0 + 1),
+            (0, states.len()),
+            "some consecutive states are missing in .tla trace"
+        );
+
+        let mut trace = TlaTrace::new();
+        states
+            .into_iter()
+            .for_each(|(_, state)| trace.add(state.into()));
         Ok(trace)
     }
 }