NullPointerException when last state of the trace is *not* in

the model.

If the final state of a counterexample is excluded from the model
because state- or action-constraints evaluate to false, it is not
written to the trace file.  This omission causes a NullPointerException
when attempting to read the final state from the trace file during
counterexample reconstruction.  To address this issue, the final state
is now explicitly appended to the counterexample to ensure completeness
and avoid runtime errors.

[Bug][TLC]

Signed-off-by: Markus Alexander Kuppe <[email protected]>

tlatools/org.lamport.tlatools/src/tlc2/tool/ModelChecker.java

@@ -1072,6 +1072,10 @@ public void resume() {
 		}
 	}
 
+	/**
+	 * PostCondition:
+	 *      IF IsInitial(s) THEN s \in Range(Trace) ELSE s \notin Range(Trace)
+	 */
 	@Override
 	public TLCStateInfo[] getTraceInfo(TLCState s) throws IOException {
 		return trace.getTrace(s);

tlatools/org.lamport.tlatools/src/tlc2/tool/Worker.java

@@ -639,6 +639,19 @@ private final void doPostCondition(TLCState curState, TLCState succState) throws
 		} else if (succState == null) {
 			trace.addAll(Arrays.asList(tlc.getTraceInfo(curState)));
 			trace.add(tool.getState(curState, trace.getLast().state));
+		} else if (succState.allAssigned() && succState.workerId == Short.MAX_VALUE) {
+			if (curState.isInitial()) {
+		        // Handle case where successor is fully assigned but not in the model because
+		    	// of an action- or state-constraint.
+				trace.add(tool.getState(curState.fingerPrint()));
+				trace.add(tool.getState(succState, curState));
+			} else {
+				// succState is not in the model because of an action- or state-constraint.
+				// Therefore, calling tlc.getTraceInfo(succState) would throw a NPE.
+				trace.addAll(Arrays.asList(tlc.getTraceInfo(curState)));
+				trace.add(tool.getState(curState, trace.getLast().state));
+				trace.add(tool.getState(succState, curState));
+			}
 		} else {
 			trace.addAll(Arrays.asList(tlc.getTraceInfo(succState)));
 			trace.add(tool.getState(succState, curState));

tlatools/org.lamport.tlatools/test-model/DotConstrained.cfg

@@ -1,4 +1,5 @@
 INIT Init
 NEXT Next
 ACTION_CONSTRAINT ActionConstraint
-INVARIANT Inv
+INVARIANT Inv
+POSTCONDITION PostCondition

tlatools/org.lamport.tlatools/test-model/Github1087.cfg

@@ -0,0 +1,5 @@
+INIT Init2
+NEXT Next
+ACTION_CONSTRAINT ActionConstraint
+INVARIANT Inv
+POSTCONDITION PostCondition2

tlatools/org.lamport.tlatools/test-model/Github602.tla

@@ -1,5 +1,5 @@
 ------ MODULE Github602 ------
-EXTENDS Integers
+EXTENDS Integers, TLC, TLCExt
 
 VARIABLE x
 
@@ -17,6 +17,16 @@ Constraint ==  x \in Nat
 Inv == x >= 0
 
 ActionConstraint == x' \in Nat
+
+PostCondition ==
+	/\ TLCSet(42, TLCGet("generated"))
+	/\ ToTrace(CounterExample) = << [x |-> 0],[x |-> 1],[x |-> -1] >> 
+
+Init2 == x = 1
+
+PostCondition2 ==
+	/\ TLCSet(42, TLCGet("generated"))
+	/\ ToTrace(CounterExample) = << [x |-> 1],[x |-> -1] >> 
 ====
 
 ---- CONFIG Github602 ----

tlatools/org.lamport.tlatools/test-model/TLCGetAll.tla

@@ -36,7 +36,8 @@ Sum(seq) ==
     IN S[Len(seq)]
 
 PostCondition ==
-    LET vals == TLCGet("all")
+ /\ TLCSet(42, TLCGet("generated"))
+ /\ LET vals == TLCGet("all")
     IN /\ DOMAIN vals = {R, 42} 
        \* vars[R] is a tuple with length N where N is the number of workers.
        \* In other words, vars[R] has the value of TLCGet(R) for each worker.

tlatools/org.lamport.tlatools/test-model/ViewMap.tla

@@ -103,7 +103,8 @@ view == <<buffer, waitset>>
 CONSTANTS c1, c2, p1
 
 PostCondition ==
-	CounterExample =
+	/\ TLCSet(42, TLCGet("generated"))
+	/\ CounterExample =
 		[ state |->
 		      { << 1,
 		           [ buffer |-> <<>>,

tlatools/org.lamport.tlatools/test-model/cdot/ChainedCdots.tla

@@ -21,6 +21,7 @@ Spec ==
     Init /\ [][Next]_x
 
 PostCondition ==
-	TLCGet(0) = 63
+	/\ TLCSet(42, TLCGet("generated"))
+	/\ TLCGet(0) = 63
 
 =======

tlatools/org.lamport.tlatools/test/tlc2/tool/ChainedCdotsTest.java

@@ -25,16 +25,21 @@
  ******************************************************************************/
 package tlc2.tool;
 
+import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertFalse;
 import static org.junit.Assert.assertTrue;
 
 import java.io.IOException;
+import java.util.List;
 
 import org.junit.Test;
 
+import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.tool.impl.Tool;
 import tlc2.tool.liveness.ModelCheckerTestCase;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
 
 public class ChainedCdotsTest extends ModelCheckerTestCase {
 
@@ -58,5 +63,15 @@ public void testSpec() throws IOException {
 
 		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "9", "4", "0"));
 		assertTrue(recorder.recordedWithStringValue(EC.TLC_SEARCH_DEPTH, "2"));
+
+		// Assert POSTCONDITION.
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_EVALUATION_ERROR));
+
+		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
+		// register.
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(9), allValue.get(0));
 	}
 }

tlatools/org.lamport.tlatools/test/tlc2/tool/DotConstrainedTest.java

@@ -26,6 +26,7 @@
 
 package tlc2.tool;
 
+import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertFalse;
 import static org.junit.Assert.assertTrue;
 import static org.junit.Assert.fail;
@@ -38,11 +39,14 @@
 import org.junit.Test;
 
 import tla2sany.semantic.SemanticNode;
+import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.output.EC.ExitStatus;
 import tlc2.tool.liveness.ModelCheckerTestCase;
 import tlc2.util.DotStateWriter;
 import tlc2.util.IStateWriter;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
 import util.FileUtil;
 
 public class DotConstrainedTest extends ModelCheckerTestCase {
@@ -101,6 +105,16 @@ public void testSpec() {
 
 		assertTrue(constrained.get());
 
+		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
+		// register.
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(4), allValue.get(0));
+
+		// Assert POSTCONDITION.
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_EVALUATION_ERROR));
+
 		assertZeroUncovered();
 	}
 }

tlatools/org.lamport.tlatools/test/tlc2/tool/Github1087Test.java

@@ -0,0 +1,77 @@
+/*******************************************************************************
+ * Copyright (c) 2024 Microsoft Corp. 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;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import org.junit.Test;
+
+import tlc2.TLCGlobals;
+import tlc2.output.EC;
+import tlc2.output.EC.ExitStatus;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
+
+public class Github1087Test extends ModelCheckerTestCase {
+
+	public Github1087Test() {
+		super("Github602", new String[] { "-config", "Github1087.cfg" }, ExitStatus.VIOLATION_SAFETY);
+	}
+
+	@Test
+	public void testSpec() {
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertFalse(recorder.recorded(EC.GENERAL));
+
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "2", "1", "0"));
+
+		// Assert it has found the temporal violation and also a counter example
+		assertTrue(recorder.recorded(EC.TLC_INVARIANT_VIOLATED_BEHAVIOR));
+
+		// Assert the error trace
+		assertTrue(recorder.recorded(EC.TLC_STATE_PRINT2));
+		final List<String> expectedTrace = new ArrayList<String>(2);
+		expectedTrace.add("x = 1");
+		expectedTrace.add("x = -1");
+		assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace);
+
+		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
+		// register.
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(2), allValue.get(0));
+
+		// Assert POSTCONDITION.
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_EVALUATION_ERROR));
+	}
+}

tlatools/org.lamport.tlatools/test/tlc2/tool/TLCGetAllTest.java

@@ -25,12 +25,19 @@
  ******************************************************************************/
 package tlc2.tool;
 
+import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import java.util.List;
 
 import org.junit.Test;
 
+import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.tool.liveness.ModelCheckerTestCase;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
 
 public class TLCGetAllTest extends ModelCheckerTestCase {
 
@@ -47,5 +54,15 @@ protected int getNumberOfThreads() {
 	public void testSpec() {
 		assertFalse(recorder.recorded(EC.GENERAL));
 		assertZeroUncovered();
+
+		// Assert POSTCONDITION.
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_EVALUATION_ERROR));
+
+		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
+		// register.
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(10101), allValue.get(0));
 	}
 }

tlatools/org.lamport.tlatools/test/tlc2/tool/ViewMapTest.java

@@ -25,6 +25,7 @@
  ******************************************************************************/
 package tlc2.tool;
 
+import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertFalse;
 import static org.junit.Assert.assertTrue;
 
@@ -33,9 +34,12 @@
 
 import org.junit.Test;
 
+import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.output.EC.ExitStatus;
 import tlc2.tool.liveness.ModelCheckerTestCase;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
 
 public class ViewMapTest extends ModelCheckerTestCase {
 
@@ -76,5 +80,15 @@ public void testSpec() {
 		assertTraceWith(recorder.getRecords(EC.TLC_STATE_PRINT2), expectedTrace, expectedActions);
 
 		assertUncovered("line 91, col 60 to line 91, col 73 of module ViewMap: 0");
+
+		// Assert POSTCONDITION.
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_FALSE));
+		assertFalse(recorder.recorded(EC.TLC_ASSUMPTION_EVALUATION_ERROR));
+
+		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
+		// register.
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(43), allValue.get(0));
 	}
 }

tlatools/org.lamport.tlatools/test/tlc2/tool/liveness/OneBitMutexNoSymmetryTest.java

@@ -26,15 +26,20 @@
 
 package tlc2.tool.liveness;
 
+import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertFalse;
 import static org.junit.Assert.assertTrue;
 
 import java.io.File;
+import java.util.List;
 
 import org.junit.Test;
 
+import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.output.EC.ExitStatus;
+import tlc2.value.IValue;
+import tlc2.value.impl.IntValue;
 
 public class OneBitMutexNoSymmetryTest extends ModelCheckerTestCase {
 
@@ -67,8 +72,8 @@ public void testSpec() {
 
 		// Check that POSTCONDITION wrote the number of generated states to a TLCSet
 		// register.
-//		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
-//		assertTrue(!allValue.isEmpty());
-//		assertEquals(IntValue.gen(244), allValue.get(0));
+		final List<IValue> allValue = TLCGlobals.mainChecker.getAllValue(42);
+		assertTrue(!allValue.isEmpty());
+		assertEquals(IntValue.gen(244), allValue.get(0));
 	}
 }

tlatools/org.lamport.tlatools/test/tlc2/tool/simulation/Github602Test.java

@@ -31,7 +31,6 @@
 
 import org.junit.Test;
 
-import tlc2.TLC;
 import tlc2.output.EC;
 import tlc2.tool.liveness.ModelCheckerTestCase;