Initial implementation of ENABLED

js/eval.js

@@ -1608,11 +1608,24 @@ function evalBoundInfix(node, ctx){
 
 }
 
-function evalBoundPrefix(node, ctx){
+function evalEnabled(node, ctx) {
+    let rhs = node.childForFieldName("rhs");
+    let rhsVal = evalExpr(rhs, ctx)[0]["val"];
+    evalLog("rhs ENABLED: ", rhsVal);
+    assert(rhsVal instanceof BoolValue);
+    return [ctx.withVal(rhsVal)];
+}
+
+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);
 
+    // ENABLED.
+    if (symbol.type === "enabled") {
+        return evalEnabled(node, ctx);
+    }
+
     // DOMAIN.
     if(symbol.type === "domain"){
         evalLog("DOMAIN op");

js/test.js

@@ -197,6 +197,7 @@ function testStateGraphEquiv(testId, stateGraph, specText, constvals) {
         { "spec": "simple_domain", "constvals": undefined },
         { "spec": "simple6", "constvals": undefined },
         { "spec": "simple7", "constvals": undefined },
+        { "spec": "simple_enabled", "constvals": undefined },
         { "spec": "simple_fcn", "constvals": undefined },
         { "spec": "simple_subset", "constvals": undefined },
         { "spec": "simple_quant", "constvals": undefined },

specs/with_state_graphs/simple_enabled.cfg

@@ -0,0 +1,2 @@
+INIT Init
+NEXT Next

specs/with_state_graphs/simple_enabled.tla

@@ -0,0 +1,16 @@
+---- MODULE simple_enabled ----
+EXTENDS Naturals
+
+VARIABLE x
+
+Action == x > 0 /\ x' = 2
+
+Action2 == x' = 3
+
+Init == x = 1
+
+Next == 
+    /\ ENABLED Action
+    /\ Action2
+
+====

specs/with_state_graphs/simple_enabled.tla.dot

@@ -0,0 +1,12 @@
+strict digraph DiskGraph {
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+-6230161439325923452 [label="x = 1",style = filled]
+-6230161439325923452 -> 7158667421841284535 [label="",color="black",fontcolor="black"];
+7158667421841284535 [label="x = 3"];
+7158667421841284535 -> 7158667421841284535 [label="",color="black",fontcolor="black"];
+{rank = same; -6230161439325923452;}
+{rank = same; 7158667421841284535;}
+}
+}

specs/with_state_graphs/simple_enabled.tla.dot.json

@@ -0,0 +1,74 @@
+{
+  "name": "DiskGraph",
+  "directed": true,
+  "strict": true,
+  "nodesep": "0.35",
+  "_subgraph_cnt": 3,
+  "objects": [
+    {
+      "name": "cluster_graph",
+      "color": "white",
+      "nodesep": "0.35",
+      "_gvid": 0,
+      "subgraphs": [
+        1,
+2
+      ],
+      "nodes": [
+        3,4
+      ],
+      "edges": [
+        0,1
+      ]
+    },
+    {
+      "name": "%7",
+      "color": "white",
+      "nodesep": "0.35",
+      "rank": "same",
+      "_gvid": 1,
+      "nodes": [
+        3
+      ]
+    },
+    {
+      "name": "%9",
+      "color": "white",
+      "nodesep": "0.35",
+      "rank": "same",
+      "_gvid": 2,
+      "nodes": [
+        4
+      ]
+    },
+    {
+      "_gvid": 3,
+      "name": "-6230161439325923452",
+      "label": "x = 1",
+      "style": "filled"
+    },
+    {
+      "_gvid": 4,
+      "name": "7158667421841284535",
+      "label": "x = 3"
+    }
+  ],
+  "edges": [
+    {
+      "_gvid": 0,
+      "tail": 3,
+      "head": 4,
+      "color": "black",
+      "fontcolor": "black",
+      "label": ""
+    },
+    {
+      "_gvid": 1,
+      "tail": 4,
+      "head": 4,
+      "color": "black",
+      "fontcolor": "black",
+      "label": ""
+    }
+  ]
+}