Disable unlikely level-checking bug in test suite. Warn users if it's

likely they are affected by the bug (in which case they need to simplify
the incorrectly flagged expression.

[Bug][TLC]

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          *)

tlatools/src/tlc2/output/MP.java

@@ -364,6 +364,11 @@ public class MP
             break;
         case EC.TLC_INVARIANT_VIOLATED_LEVEL:
         	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);
     }
 

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));

tlatools/test-model/suite/test52.cfg

 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

tlatools/test-model/test52.cfg

 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

tlatools/test-model/testinvalidinvariant.cfg

+SPECIFICATION Spec
+PROPERTY Property
+INVARIANT Invariant

tlatools/test-model/testinvalidinvariant.tla

+------------------ 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
+
+==================================================================

tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java

+/*******************************************************************************
+ * 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."));
+	}
+}