Improving TLC error message for temporal existential quantifier in spec - #304

.  Upon encountering the usage of a temporal existential quantifier in the specification, a better fail message is displayed:
"TLC does not support temporal existential quantification over state variables."

[Enhancement][Tools]

tlatools/src/tlc2/output/EC.java

@@ -166,6 +166,7 @@ public interface EC
     public static final int TLC_MODULE_APPLY_EMPTY_SEQ = 2184;
     
     public static final int TLC_SYMMETRY_SET_TOO_SMALL = 2300;
+    public static final int TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS = 2301;
     
     public static final int TLC_STARTING = 2185;
     public static final int TLC_FINISHED = 2186;

tlatools/src/tlc2/output/MP.java

@@ -723,6 +723,10 @@ public class MP
         case EC.TLC_SYMMETRY_SET_TOO_SMALL:
         	b.append("The set%1% %2% %3% been defined to be a symmetry set but only contain%4% a single element.");
         	break;
+            
+        case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS:
+        	b.append("TLC does not support temporal existential quantification over state variables.");
+        	break;
         /* ************************************************************************ */
         case EC.TLC_MODULE_TLCGET_UNDEFINED:
             b.append("TLCGet(%1%) was undefined.");
@@ -1171,7 +1175,13 @@ public class MP
             break;
         case EC.TLC_CONFIG_MISSING_INIT:
             b.append("The configuration file did not specify the initial state predicate." +
-                     // Following part of error message added by LL on 15 Nov 2012
+                     // The below part of the error message was added by LL on 15 Nov 2012
+            		 //
+            		 //	ldq, 13 Feb 2020: I don't think this is semantically correct; I receive
+                     //			no errors when defining a specification that references
+            		 //			a formula which is a parameterized INSTANCE. I *do* receive
+                     //			such an error when that formula is being constrained via
+            		 //			the temporal existential qualifier.
                      "\nCan also be caused by trying to run TLC on a specification from" +
                      "\na module imported with a parameterized INSTANCE statement.");
             break;

tlatools/src/tlc2/tool/impl/SpecProcessor.java

@@ -1051,6 +1051,10 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
             }
 
             int opcode = BuiltInOPs.getOpCode(pred1.getOperator().getName());
+            if (opcode == OPCODE_te)
+            {
+            	Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS);
+            }
             if (opcode == OPCODE_cl || opcode == OPCODE_land)
             {
                 for (int i = 0; i < args.length; i++)