diff --git a/modelator/Cargo.toml b/modelator/Cargo.toml index 0caecc33..8b6379ed 100644 --- a/modelator/Cargo.toml +++ b/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" diff --git a/modelator/src/artifact/tla_trace.rs b/modelator/src/artifact/tla_trace.rs index ad467ab9..7d9105f6 100644 --- a/modelator/src/artifact/tla_trace.rs +++ b/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 { - 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) } } diff --git a/modelator/src/module/tla/json/parser.rs b/modelator/src/module/tla/json/parser.rs index bcc52987..8682035e 100644 --- a/modelator/src/module/tla/json/parser.rs +++ b/modelator/src/module/tla/json/parser.rs @@ -1,190 +1,208 @@ -use nom::branch::alt; -use nom::bytes::complete::{tag, take_while}; -use nom::character::complete::{char, digit1, multispace0, satisfy}; -use nom::combinator::{cut, opt, value}; -use nom::multi::{many1, separated_list0, separated_list1}; -use nom::sequence::{preceded, separated_pair, terminated}; -use nom::IResult; +use nom::{ + branch::alt, + bytes::complete::{is_not, tag, take_while}, + character::complete::{char, digit1, multispace0, satisfy}, + combinator::{complete, cut, map, opt, recognize, value}, + multi::{many1, separated_list0, separated_list1}, + sequence::{delimited, pair, preceded, separated_pair}, + IResult, +}; + use serde_json::Value as JsonValue; -pub(crate) fn parse_state(input: &str) -> IResult<&str, JsonValue> { - preceded( - space, - preceded(opt(tag("/\\")), separated_list0(tag("/\\"), parse_var)), - )(input) - .map(|(next_input, value)| { - let value = value.into_iter().collect(); - (next_input, JsonValue::Object(value)) - }) +pub(crate) fn parse_state(i: &str) -> IResult<&str, JsonValue> { + map( + preceded( + opt(delimited(multispace0, complete(tag("/\\")), multispace0)), + separated_list0( + delimited(multispace0, complete(tag("/\\")), multispace0), + parse_var, + ), + ), + |value| JsonValue::Object(value.into_iter().collect()), + )(i) } -fn parse_var(input: &str) -> IResult<&str, (String, JsonValue)> { - preceded( - space, - terminated( - separated_pair( - preceded(space, parse_identifier), - preceded(space, char('=')), - preceded(space, parse_any_value), - ), - space, +fn parse_var(i: &str) -> IResult<&str, (String, JsonValue)> { + delimited( + multispace0, + separated_pair( + parse_identifier, + delimited(multispace0, char('='), multispace0), + parse_any_value, ), - )(input) + multispace0, + )(i) } -fn space(input: &str) -> IResult<&str, &str> { - multispace0(input) +// TODO: what else can TLA var idenfitiers have? +fn parse_identifier(i: &str) -> IResult<&str, String> { + map( + many1(satisfy(|c| c.is_alphanumeric() || "_-".contains(c))), + |value| value.into_iter().collect(), + )(i) } -fn parse_identifier(input: &str) -> IResult<&str, String> { - // TODO: what else can TLA var idenfitiers have? - many1(satisfy(|c| c.is_alphanumeric() || "_-".contains(c)))(input).map(|(next_input, value)| { - let value = value.into_iter().collect(); - (next_input, value) - }) +fn parse_identifiers_as_values(i: &str) -> IResult<&str, JsonValue> { + map(parse_identifier, JsonValue::String)(i) } -fn parse_any_value(input: &str) -> IResult<&str, JsonValue> { - // identifiers of model variables can also be used as TLA values - let parse_identifiers_as_values = |input| { - parse_identifier(input).map(|(next_input, value)| { - let value = JsonValue::String(value); - (next_input, value) - }) - }; +fn parse_any_value(i: &str) -> IResult<&str, JsonValue> { preceded( - space, + multispace0, alt(( parse_bool, + parse_function, parse_number, parse_string, parse_identifiers_as_values, parse_set, parse_sequence, parse_record, - parse_function, )), - )(input) + )(i) } -fn parse_bool(input: &str) -> IResult<&str, JsonValue> { - let parse_true = value(JsonValue::Bool(true), tag("TRUE")); - let parse_false = value(JsonValue::Bool(false), tag("FALSE")); - alt((parse_true, parse_false))(input) +fn parse_bool(i: &str) -> IResult<&str, JsonValue> { + map( + alt((value(true, tag("TRUE")), value(false, tag("FALSE")))), + JsonValue::Bool, + )(i) } -fn parse_number(input: &str) -> IResult<&str, JsonValue> { - alt((parse_pos_number, parse_neg_number))(input) +fn parse_number(i: &str) -> IResult<&str, JsonValue> { + alt((parse_pos_number, parse_neg_number))(i) } -fn parse_pos_number(input: &str) -> IResult<&str, JsonValue> { - digit1(input).map(|(next_input, value)| { - let value: u64 = value - .parse() - .expect("u64 parsed by nom should be a valid u64"); - (next_input, JsonValue::Number(value.into())) - }) +fn parse_pos_number(i: &str) -> IResult<&str, JsonValue> { + map(digit1, |value: &str| { + JsonValue::Number( + value + .parse::() + .expect("u64 parsed by nom should be a valid u64") + .into(), + ) + })(i) } -fn parse_neg_number(input: &str) -> IResult<&str, JsonValue> { - preceded(tag("-"), digit1)(input).map(|(next_input, value)| { - let value: i64 = format!("-{}", value) - .parse() - .expect("i64 parsed by nom should be a valid i64"); - (next_input, JsonValue::Number(value.into())) - }) +fn parse_neg_number(i: &str) -> IResult<&str, JsonValue> { + map(preceded(char('-'), digit1), |value| { + JsonValue::Number( + format!("-{}", value) + .parse::() + .expect("i64 parsed by nom should be a valid i64") + .into(), + ) + })(i) } -fn parse_string(input: &str) -> IResult<&str, JsonValue> { - // we support any string that doesn't escape with '\"' - preceded( - char('\"'), - cut(terminated(take_while(|c| c != '\"'), char('\"'))), - )(input) - .map(|(next_input, value)| { - let value = JsonValue::String(value.to_owned()); - (next_input, value) - }) +fn parse_string(i: &str) -> IResult<&str, JsonValue> { + map( + delimited(char('"'), cut(take_while(|c| c != '"')), char('"')), + |value: &str| JsonValue::String(value.into()), + )(i) } -fn parse_set(input: &str) -> IResult<&str, JsonValue> { - preceded( - char('{'), - cut(terminated( - separated_list0(preceded(space, char(',')), parse_any_value), - preceded(space, char('}')), - )), - )(input) - .map(|(next_input, value)| { - let value = JsonValue::Array(value); - (next_input, value) - }) +fn parse_set(i: &str) -> IResult<&str, JsonValue> { + map( + delimited( + pair(char('{'), multispace0), + cut(separated_list0( + delimited(multispace0, char(','), multispace0), + parse_any_value, + )), + pair(multispace0, char('}')), + ), + JsonValue::Array, + )(i) } -fn parse_sequence(input: &str) -> IResult<&str, JsonValue> { - preceded( - tag("<<"), - cut(terminated( - separated_list0(preceded(space, char(',')), parse_any_value), - preceded(space, tag(">>")), - )), - )(input) - .map(|(next_input, value)| { - let value = JsonValue::Array(value); - (next_input, value) - }) +fn parse_sequence(i: &str) -> IResult<&str, JsonValue> { + map( + delimited( + pair(tag("<<"), multispace0), + cut(separated_list0( + delimited(multispace0, char(','), multispace0), + parse_any_value, + )), + pair(multispace0, tag(">>")), + ), + JsonValue::Array, + )(i) } -fn parse_record(input: &str) -> IResult<&str, JsonValue> { - preceded( - char('('), - cut(terminated( - separated_list1(preceded(space, tag("@@")), parse_record_entry), - preceded(space, char(')')), - )), - )(input) - .map(|(next_input, value)| { - let value = value.into_iter().collect(); - let value = JsonValue::Object(value); - (next_input, value) - }) +fn parse_function(i: &str) -> IResult<&str, JsonValue> { + map( + delimited( + multispace0, + separated_list1( + delimited(multispace0, complete(tag("@@")), multispace0), + alt(( + map(parse_function_entry, |x| { + JsonValue::Object(vec![x].into_iter().collect()) + }), + delimited( + pair(char('('), multispace0), + parse_function, + pair(multispace0, char(')')), + ), + )), + ), + multispace0, + ), + |values| { + JsonValue::Object( + values + .into_iter() + .map(|value| { + value + .as_object() + .unwrap() + .into_iter() + .map(|(k, v)| (k.clone(), v.clone())) + .collect::>() + }) + .flatten() + .collect(), + ) + }, + )(i) } -fn parse_record_entry(input: &str) -> IResult<&str, (String, JsonValue)> { +fn parse_function_entry(i: &str) -> IResult<&str, (String, JsonValue)> { preceded( - space, + multispace0, separated_pair( - preceded(space, parse_identifier), - preceded(space, tag(":>")), - preceded(space, parse_any_value), + parse_identifier, + delimited(multispace0, complete(tag(":>")), multispace0), + parse_any_value, ), - )(input) + )(i) } -fn parse_function(input: &str) -> IResult<&str, JsonValue> { - preceded( - char('['), - cut(terminated( - separated_list1(preceded(space, char(',')), parse_function_entry), - preceded(space, char(']')), - )), - )(input) - .map(|(next_input, value)| { - let value = value.into_iter().collect(); - let value = JsonValue::Object(value); - (next_input, value) - }) +fn parse_record(i: &str) -> IResult<&str, JsonValue> { + map( + delimited( + pair(char('['), multispace0), + cut(separated_list1( + delimited(multispace0, char(','), multispace0), + parse_record_entry, + )), + pair(multispace0, char(']')), + ), + |value| JsonValue::Object(value.into_iter().collect()), + )(i) } -fn parse_function_entry(input: &str) -> IResult<&str, (String, JsonValue)> { +fn parse_record_entry(i: &str) -> IResult<&str, (String, JsonValue)> { preceded( - space, + multispace0, separated_pair( - preceded(space, parse_identifier), - preceded(space, tag("|->")), - preceded(space, parse_any_value), + parse_identifier, + delimited(multispace0, tag("|->"), multispace0), + parse_any_value, ), - )(input) + )(i) } #[cfg(test)]