diff --git a/tlatools/src/tlc2/output/EC.java b/tlatools/src/tlc2/output/EC.java index e15213becf998ed191f1922880feec3181da660b..322470816bb57226d4d9c9371498fbbf0d1d8079 100644 --- a/tlatools/src/tlc2/output/EC.java +++ b/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; diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java index 51672a15f04aeef9bf17c2250c35ce520158469d..504e98312b44006576fd435b1633f60b6fee771a 100644 --- a/tlatools/src/tlc2/output/MP.java +++ b/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; /* ************************************************************************ */ diff --git a/tlatools/src/tlc2/tool/impl/SpecProcessor.java b/tlatools/src/tlc2/tool/impl/SpecProcessor.java index fed019f39e11ba08f7f164ac0d4c6235bdb38c22..58a3b2cd046743777b747f72e5d6ed2d1a452ac5 100644 --- a/tlatools/src/tlc2/tool/impl/SpecProcessor.java +++ b/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) {