From 3932995edee46a61ccddac24104b796cbdfc7bfb Mon Sep 17 00:00:00 2001
From: loki der quaeler <quaeler@gmail.com>
Date: Thu, 13 Feb 2020 11:16:30 -0800
Subject: [PATCH] Improving TLC error message for temporal existential
 quantifier in spec - #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]
---
 tlatools/src/tlc2/output/MP.java               | 2 +-
 tlatools/src/tlc2/tool/impl/SpecProcessor.java | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index 83a6fb199..51672a15f 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -725,7 +725,7 @@ public class MP
         	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
index 5249ba9f5..fed019f39 100644
--- a/tlatools/src/tlc2/tool/impl/SpecProcessor.java
+++ b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
@@ -1051,7 +1051,7 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
             }
 
             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);
             }
-- 
GitLab