ClassCastException in profiler's CostModel when top-level expression of

action, init-predicate, invariant, constraints ... is declared RECURSIVE

Fixes Github issue #649
#649

[Bug][TLC]

tlatools/org.lamport.tlatools/src/tlc2/tool/coverage/CostModelCreator.java

@@ -254,13 +254,10 @@ public void preVisit(final ExploreNode exploreNode) {
 			if (operator instanceof OpDefNode) {
 				final OpDefNode odn = (OpDefNode) operator;
 				if (odn.getInRecursive()) {
-					final OpApplNodeWrapper recursive = (OpApplNodeWrapper) stack.stream()
+					stack.stream()
 							.filter(w -> w.getNode() != null && w.getNode() instanceof OpApplNode
 									&& ((OpApplNode) w.getNode()).getOperator() == odn)
-							.findFirst().orElse(null);
-					if (recursive != null) {
-						oan.setRecursive(recursive);
-					}
+							.findFirst().ifPresent(cmn -> oan.setRecursive(cmn));
 				}
 			}
 
@@ -287,7 +284,7 @@ public void preVisit(final ExploreNode exploreNode) {
 			// specification took approximately 60 seconds. With the safeguard, it is down
 			// to a second or two.
 			//
-			// To summarize, this is a clutch that has been hacked to work good enough!
+			// To summarize, this is a clutch that has been hacked to be good enough!
 			// 
 			// if-branches 1., 2., and 3. below are evaluated in three distinct
 			// invocation of outer preVisit for different ExploreNodes.

tlatools/org.lamport.tlatools/src/tlc2/tool/coverage/OpApplNodeWrapper.java

@@ -54,7 +54,7 @@ public class OpApplNodeWrapper extends CostModelNode implements Comparable<OpApp
 	private long snapshotEvalCount = 0;
 	private boolean primed = false;
 	private int level;
-	private OpApplNodeWrapper recursive;
+	private CostModelNode recursive;
 	protected final Map<SemanticNode, CostModelNode> lets = new LinkedHashMap<>();
 
 	OpApplNodeWrapper(OpApplNode node, CostModelNode root) {
@@ -142,7 +142,7 @@ public OpApplNodeWrapper addLets(OpApplNodeWrapper lets) {
 		return this;
 	}
 
-	public OpApplNodeWrapper setRecursive(OpApplNodeWrapper recursive) {
+	public OpApplNodeWrapper setRecursive(CostModelNode recursive) {
 		assert this.recursive == null;
 		this.recursive = recursive;
 		return this;

tlatools/org.lamport.tlatools/test-model/coverage/Github649.cfg

@@ -0,0 +1,4 @@
+INIT Init
+NEXT Next
+INVARIANT TypeOK
+CONSTRAINT Constraint

tlatools/org.lamport.tlatools/test-model/coverage/Github649.tla

@@ -0,0 +1,20 @@
+---- MODULE Github649 ----
+EXTENDS Naturals
+
+VARIABLE clock
+
+RECURSIVE Check(_,_)
+Check(c,n) == IF n = 0 THEN c \in BOOLEAN ELSE Check(c, n - 1)
+
+TypeOK == Check(clock,1)
+
+RECURSIVE Flip(_,_,_)
+Flip(v, b, n) == IF n = 0 THEN v = ~b ELSE Flip(v, b, n - 1)
+
+Init == Flip(clock, FALSE, 1)  \* The expression Flip(..) does *not* appear in the coverage result. Some of its parameters are covered (invoked),
+                               \* but the Flip(..) itself gets skipped over by TLC.  It correctly does not get marked as uncovered.
+Next == clock' = ~clock
+
+Constraint ==
+	Flip(clock, ~clock, 2)
+====

tlatools/org.lamport.tlatools/test/tlc2/tool/coverage/Github649CoverageTest.java

@@ -0,0 +1,75 @@
+/*******************************************************************************
+ * Copyright (c) 2021 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.coverage;
+
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+
+public class Github649CoverageTest extends AbstractCoverageTest {
+
+    public Github649CoverageTest () {
+        super("Github649");
+    }
+
+    @Test
+    public void testSpec () {
+		// ModelChecker has finished and generated the expected amount of states
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertTrue(recorder.recordedWithStringValue(EC.TLC_SEARCH_DEPTH, "2"));
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "3", "2", "0"));
+
+		// No 'general' errors recorded
+		assertFalse(recorder.recorded(EC.GENERAL));
+
+		assertCoverage("<Init line 14, col 1 to line 14, col 4 of module Github649>: 1:1\n"
+				+ "  line 12, col 21 to line 12, col 25 of module Github649: 2\n"
+				+ "  line 12, col 32 to line 12, col 37 of module Github649: 1\n"
+				+ "  line 12, col 44 to line 12, col 60 of module Github649: 1\n"
+				+ "  line 14, col 21 to line 14, col 25 of module Github649: 1\n"
+				+ "<Next line 16, col 1 to line 16, col 4 of module Github649>: 1:2\n"
+				+ "  line 16, col 9 to line 16, col 23 of module Github649: 2\n"
+				+ "<TypeOK line 9, col 1 to line 9, col 6 of module Github649>\n"
+				+ "  line 9, col 11 to line 9, col 24 of module Github649: 2\n"
+				+ "  |line 7, col 15 to line 7, col 62 of module Github649: 4\n"
+				+ "  ||line 7, col 18 to line 7, col 22 of module Github649: 4\n"
+				+ "  ||line 7, col 29 to line 7, col 41 of module Github649: 2\n"
+				+ "  ||line 7, col 48 to line 7, col 62 of module Github649: 2\n"
+				+ "  |line 9, col 17 to line 9, col 21 of module Github649: 2\n"
+				+ "<Constraint line 18, col 1 to line 18, col 10 of module Github649>: 3:3\n"
+				+ "  line 19, col 9 to line 19, col 30 of module Github649: 3\n"
+				+ "  |line 12, col 18 to line 12, col 60 of module Github649: 9\n"
+				+ "  ||line 12, col 21 to line 12, col 25 of module Github649: 9\n"
+				+ "  ||line 12, col 32 to line 12, col 37 of module Github649: 3\n"
+				+ "  ||line 12, col 44 to line 12, col 60 of module Github649: 6\n"
+				+ "  |line 19, col 14 to line 19, col 18 of module Github649: 3\n"
+				+ "  |line 19, col 21 to line 19, col 26 of module Github649: 3");
+		assertFalse(recorder.recorded(EC.TLC_COVERAGE_MISMATCH));
+    }
+}