Implement DOMAIN operator

will62794 · Jun 29, 2022 · 30f4151 · 30f4151
1 parent 806197a
commit 30f4151
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 3 deletions.
diff --git a/js/eval.js b/js/eval.js
@@ -1207,6 +1207,18 @@ function evalBoundPrefix(node, ctx){
     let symbol = node.children[0];
     let rhs = node.children[1];
     evalLog("evalBoundPrefix: ", node.type, ", ", node.text, `, prefix symbol: '${symbol.type}' `, "ctx:", ctx);
+
+    // DOMAIN.
+    if(symbol.type === "domain"){
+        evalLog("DOMAIN op");
+        evalLog(rhs);
+        let rhsVal = evalExpr(rhs, ctx)[0]["val"];
+        evalLog("rhsVal: ", rhsVal);
+        let domainVal = new SetValue(rhsVal.getDomain());
+        evalLog("domain val: ", domainVal);
+        return [ctx.withVal(domainVal)];
+    }
+
     if(symbol.type === "powerset"){
         evalLog("POWERSET op");
         evalLog(rhs);

diff --git a/specs/with_state_graphs/tla_expr_eval.tla b/specs/with_state_graphs/tla_expr_eval.tla
@@ -24,6 +24,7 @@ Init == exprs = [
     head2 |-> Head(<<3,2,1>>),
     tail1 |-> Tail(<<1,2,3>>),
     tail2 |-> Tail(<<1>>),
+    domain1 |-> DOMAIN [a |-> 1, b |-> 2, c |-> 3],
     case1 |-> CASE TRUE -> 3 [] FALSE -> 5,
     case2 |-> CASE FALSE -> 3 [] TRUE -> 5,
     case3 |-> CASE FALSE -> 3 [] FALSE -> 5 [] TRUE -> 7,

diff --git a/specs/with_state_graphs/tla_expr_eval.tla.json b/specs/with_state_graphs/tla_expr_eval.tla.json
@@ -1,7 +1,7 @@
 {
   "states": [
     {
-      "fp": 787083421091669876,
+      "fp": 9222512163447704883,
       "val": {
         "exprs": {
           "#type": "record",
@@ -67,6 +67,23 @@
               "#type": "tup",
               "#value": []
             },
+            "domain1": {
+              "#type": "set",
+              "#value": [
+                {
+                  "#type": "string",
+                  "#value": "a"
+                },
+                {
+                  "#type": "string",
+                  "#value": "b"
+                },
+                {
+                  "#type": "string",
+                  "#value": "c"
+                }
+              ]
+            },
             "case1": {
               "#type": "int",
               "#value": 3
@@ -335,8 +352,8 @@
   ],
   "edges": [
     [
-      787083421091669876,
-      787083421091669876
+      9222512163447704883,
+      9222512163447704883
     ]
   ]
 }