diff --git a/tlatools/src/tla2sany/semantic/LevelNode.java b/tlatools/src/tla2sany/semantic/LevelNode.java
index 5e6caf692d861dbe2f5cbf3232ab3b833283eb30..986dfbbdef5a679017917ec7228ef7132853d5b5 100644
--- a/tlatools/src/tla2sany/semantic/LevelNode.java
+++ b/tlatools/src/tla2sany/semantic/LevelNode.java
@@ -607,6 +607,28 @@ public int levelChecked = 0 ;
// (* any reasonable case where this will disallow a level-correct expression *)
// (* that a user is likely to write. *)
// (* *)
+// (* The decision to simplify the bookkeeping results in the following, *)
+// (* somewhat less unlikely problem. With the definitions *)
+// (* *)
+// (* ApplyToPrime(Op(_)) == Op(x') *)
+// (* EqualsNoPrime(a) == x *)
+// (* *)
+// (* the expression ApplyToPrime(EqualsNoPrime)' , which equals x', is *)
+// (* considered to be illegal. This is because the algorithm to compute the *)
+// (* level makes the assumption that ApplyToPrime will always be applied to *)
+// (* operators Op for which the level of Op(exp) depends on the level of *)
+// (* exp. Hence, SANY's algorithm gives ApplyToPrime(Op) a level of at *)
+// (* least 2 (primed expression) for any operator Op. A slightly more *)
+// (* realistic example can be constructed by modifying ApplyToPrime a bit *)
+// (* and applying it to ENABLED. *)
+// (* TLC warns users about this bug if it reports an invariant to be *)
+// (* level-incorrect in tlc2.tool.Spec.processConfigInvariants() with error *)
+// (* code tlc2.output.EC.TLC_INVARIANT_VIOLATED_LEVEL. *)
+// (* A corresponding test can be found in test52. Its invariant "Invariant" *)
+// (* covers the ENABLED scenario. However, the invariant remains disabled *)
+// (* for as long as this bug is open. The invariant Invariant can be *)
+// (* re-enabled in test52.cfg once this bug is closed. *)
+// (* *)
// (* To compute the values of op.level, op.weights, and op.minMaxLevel for *)
// (* an OpDefNode op corresponding to a definition, a level-checking *)
// (* algorithm needs to keep track of the constraints on its formal *)
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index c3b9c369c2b376561639ed2501c0eec1714c0afd..f4af880376328ecdc126527cf403d167254cad3c 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -363,7 +363,12 @@ public class MP
b.append("Invariant %1% is violated.");
break;
case EC.TLC_INVARIANT_VIOLATED_LEVEL:
- b.append("The invariant %1% is not a state predicate (one with no primes or temporal operators).");
+ b.append("The invariant %1% is not a state predicate (one with no primes or temporal operators).");
+ if (parameters.length > 1) {
+ b.append("\nNote that a bug can cause TLC to incorrectly report this error.\n"
+ + "If you believe your TLA+ or PlusCal specification to be correct,\n"
+ + "please check if this bug described in LevelNode.java starting at line 590ff affects you.");
+ }
break;
case EC.TLC_INVARIANT_EVALUATION_FAILED:
@@ -1124,6 +1129,7 @@ public class MP
*/
public static String getError(int errorCode, String[] parameters)
{
+ recorder.record(errorCode, parameters);
return getMessage(ERROR, errorCode, parameters);
}
@@ -1154,6 +1160,7 @@ public class MP
*/
public static String getMessage(int errorCode, String[] parameters)
{
+ recorder.record(errorCode, parameters);
return getMessage(NONE, errorCode, parameters);
}
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 3c402b8a8115a9f7954dfcccecb53ab92eb90174..81bed024e392ba7acf726b38e29d5c56c2520e61 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -952,9 +952,19 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
{
Assert.fail(EC.TLC_CONFIG_ID_REQUIRES_NO_ARG, new String[] { "invariant", name });
}
+ // MK 07/25/2017: Check if the invariant is a valid state predicate and produce
+ // a meaningful warning otherwise. With this enhancement, a rare bug in TLC's
+ // level-checking surfaced for which we don't have a fix right now. Fortunately,
+ // the bug is rather unlikely which is why TLC simply produces a warning for now
+ // if it "thinks" a user might be affected by the bug.
+ // see LevelNode.java line 590ff, Test52, TestInvalidInvariant, and related files
+ // for more context.
if (def.getLevel() >= 2)
{
- Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, new String[] { def.getName().toString() });
+ if (!def.getBody().levelParams.isEmpty()) {
+ Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, new String[] { def.getName().toString(), "includeWarning" });
+ }
+ Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, def.getName().toString());
}
this.invNameVec.addElement(name);
this.invVec.addElement(new Action(def.getBody(), Context.Empty));
diff --git a/tlatools/test-model/suite/test52.cfg b/tlatools/test-model/suite/test52.cfg
index f0e860231ad0256721aa61b69aec5db318681a6c..8990f16d455df1338b40f248faa8eb41101160d1 100644
--- a/tlatools/test-model/suite/test52.cfg
+++ b/tlatools/test-model/suite/test52.cfg
@@ -1,3 +1,6 @@
SPECIFICATION Spec
PROPERTY Property
-INVARIANT Invariant
+\* The Invariant is commented because of a known bug in TLC.
+\* If this bug is ever addressed, Invariant can be re-enabled
+\* and the test test52enabled be deleted.
+\*INVARIANT Invariant
diff --git a/tlatools/test-model/test52.cfg b/tlatools/test-model/test52.cfg
index f0e860231ad0256721aa61b69aec5db318681a6c..8990f16d455df1338b40f248faa8eb41101160d1 100644
--- a/tlatools/test-model/test52.cfg
+++ b/tlatools/test-model/test52.cfg
@@ -1,3 +1,6 @@
SPECIFICATION Spec
PROPERTY Property
-INVARIANT Invariant
+\* The Invariant is commented because of a known bug in TLC.
+\* If this bug is ever addressed, Invariant can be re-enabled
+\* and the test test52enabled be deleted.
+\*INVARIANT Invariant
diff --git a/tlatools/test-model/testinvalidinvariant.cfg b/tlatools/test-model/testinvalidinvariant.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..f0e860231ad0256721aa61b69aec5db318681a6c
--- /dev/null
+++ b/tlatools/test-model/testinvalidinvariant.cfg
@@ -0,0 +1,3 @@
+SPECIFICATION Spec
+PROPERTY Property
+INVARIANT Invariant
diff --git a/tlatools/test-model/testinvalidinvariant.tla b/tlatools/test-model/testinvalidinvariant.tla
new file mode 100644
index 0000000000000000000000000000000000000000..e00c9bd9158a664ad6639c0094f6e0d3f014fff7
--- /dev/null
+++ b/tlatools/test-model/testinvalidinvariant.tla
@@ -0,0 +1,12 @@
+------------------ MODULE testinvalidinvariant --------------------
+EXTENDS Integers
+
+VARIABLES x
+Init == /\ x = 1
+Next == /\ x'= x + 1
+Spec == Init /\ [][Next]_<<x>>
+
+\* Primed variable is invalid.
+Invariant == x' \in Nat
+
+==================================================================
diff --git a/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java b/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java
new file mode 100644
index 0000000000000000000000000000000000000000..1e7f5b1d3ff37fe87eee2fc38fff698e7bbeea7b
--- /dev/null
+++ b/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java
@@ -0,0 +1,52 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ * Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool.suite;
+
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class TestInvalidInvariant extends ModelCheckerTestCase {
+
+ public TestInvalidInvariant() {
+ super("testinvalidinvariant");
+ }
+
+ @Test
+ public void testSpec() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertTrue(recorder.recordedWithStringValue(EC.TLC_INVARIANT_VIOLATED_LEVEL, "Invariant"));
+ assertTrue(recorder.recordedWithSubStringValue(EC.GENERAL,
+ "The invariant Invariant is not a state predicate (one with no primes or temporal operators)."));
+ // See LevelNode.java line 590ff and tlc2.tool.Spec.processConfigInvariants().
+ assertFalse(recorder.recordedWithSubStringValue(EC.GENERAL,
+ "Note that a bug can cause TLC to incorrectly report this error."));
+ }
+}