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

.  .. and naming the EC constant better to reflect both TE and TF

[Enhancement][Tools]

tlatools/src/tlc2/output/EC.java

@@ -166,7 +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_SPECIFICATION_FEATURES_TEMPORAL_QUANTIFIER = 2301;
     
     public static final int TLC_STARTING = 2185;
     public static final int TLC_FINISHED = 2186;

tlatools/src/tlc2/output/MP.java

@@ -724,7 +724,7 @@ public class MP
         	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:
+        case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_QUANTIFIER:
         	b.append("TLC does not support temporal existential, nor universal, quantification over state variables.");
         	break;
         /* ************************************************************************ */

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

@@ -1053,7 +1053,7 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
             int opcode = BuiltInOPs.getOpCode(pred1.getOperator().getName());
             if ((opcode == OPCODE_te) || (opcode == OPCODE_tf))
             {
-            	Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS);
+            	Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_QUANTIFIER);
             }
             if (opcode == OPCODE_cl || opcode == OPCODE_land)
             {