diff --git a/.changelog/unreleased/rust/157-support-ranged-set.md b/.changelog/unreleased/rust/157-support-ranged-set.md new file mode 100644 index 00000000..e0b489c8 --- /dev/null +++ b/.changelog/unreleased/rust/157-support-ranged-set.md @@ -0,0 +1 @@ +- Parse ranged sets from TLA states. (#157) diff --git a/rs/modelator/src/model/language/tla/json/parser.rs b/rs/modelator/src/model/language/tla/json/parser.rs index 4025904c..ae0918ec 100644 --- a/rs/modelator/src/model/language/tla/json/parser.rs +++ b/rs/modelator/src/model/language/tla/json/parser.rs @@ -53,6 +53,7 @@ fn parse_any_value(i: &str) -> IResult<&str, JsonValue> { alt(( parse_bool, parse_function, + parse_range, parse_number, parse_string, parse_identifiers_as_values, @@ -103,6 +104,19 @@ fn parse_string(i: &str) -> IResult<&str, JsonValue> { )(i) } +fn parse_range(i: &str) -> IResult<&str, JsonValue> { + map( + separated_pair(parse_number, tag(".."), parse_number), + |(low, high)| { + JsonValue::Array( + (low.as_i64().unwrap()..=high.as_i64().unwrap()) + .map(|x| JsonValue::Number(x.into())) + .collect(), + ) + }, + )(i) +} + fn parse_set(i: &str) -> IResult<&str, JsonValue> { map( delimited( @@ -281,7 +295,7 @@ mod tests { const fn booleans_and_numbers_state_without_first_logical_and() -> &'static str { r#" - empty_set = {} /\ set = {1, 2, 3} /\ pos_number = 1 /\ neg_number = -1 /\ bool = TRUE + empty_set = {} /\ set = {1, 2, 3} /\ ranged_set = 1..5 /\ pos_number = 1 /\ neg_number = -1 /\ bool = TRUE "# } @@ -289,6 +303,7 @@ mod tests { r#" /\ empty_set = {} /\ set = {1, 2, 3} + /\ ranged_set = 1..5 /\ pos_number = 1 /\ neg_number = -1 /\ bool = TRUE @@ -299,6 +314,7 @@ mod tests { json!({ "empty_set": [], "set": [1, 2, 3], + "ranged_set": [1, 2, 3, 4, 5], "pos_number": 1, "neg_number": -1, "bool": true @@ -309,6 +325,7 @@ mod tests { r#" /\ empty_set = {} /\ set = {1, 2, 3} + /\ ranged_set = 1..5 /\ pos_number = 1 /\ neg_number = -1 /\ bool = TRUE @@ -319,6 +336,7 @@ mod tests { json!({ "empty_set": [], "set": [1, 2, 3], + "ranged_set": [1, 2, 3, 4, 5], "pos_number": 1, "neg_number": -1, "bool": true