Improving TLC error message for temporal existential quantifier in sp…

…ec - tlaplus#304 . Adding the temporal for-all case as well; message displayed now reads: "TLC does not support temporal existential, nor universal, quantification over state variables." [Enhancement][Tools]
BusyJay · Feb 13, 2020 · 3932995 · 3932995
1 parent 6569e88
commit 3932995
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
@@ -725,7 +725,7 @@ else if (parameters.length == 2) {
         	break;
 
         case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS:
-        	b.append("TLC does not support temporal existential quantification over state variables.");
+        	b.append("TLC does not support temporal existential, nor universal, quantification over state variables.");
         	break;
         /* ************************************************************************ */
         case EC.TLC_MODULE_TLCGET_UNDEFINED:

diff --git a/tlatools/src/tlc2/tool/impl/SpecProcessor.java b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
@@ -1051,7 +1051,7 @@ private final void processConfigSpec(ExprNode pred, Context c, List subs)
             }
 
             int opcode = BuiltInOPs.getOpCode(pred1.getOperator().getName());
-            if (opcode == OPCODE_te)
+            if ((opcode == OPCODE_te) || (opcode == OPCODE_tf))
             {
             	Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS);
             }