Parse ranged set from TLA state (#157)

* parse range * tests for ranged set * added changelog
informalsystems · Dec 17, 2021 · 32cccaf · 32cccaf
1 parent 7536350
commit 32cccaf
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 1 deletion.
diff --git a/.changelog/unreleased/rust/157-support-ranged-set.md 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
@@ -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,14 +295,15 @@ 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
         "#
     }
 
     const fn booleans_and_numbers_state() -> &'static str {
         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