Skip to content
Permalink
Browse files

CostModel lookup failed for LAMBDA expression.

Fixes GitHub issue #415
#415

[Bug][TLC]
  • Loading branch information
lemmy committed Jan 14, 2020
1 parent 7d274ad commit b62ee8de143c6c4282273be24a2aa4f49c23e733
@@ -150,7 +150,7 @@

private final Deque<CostModelNode> stack = new ArrayDeque<>();
private final Map<ExprOrOpArgNode, Subst> substs = new HashMap<>();
private final Map<OpApplNode, OpApplNodeWrapper> node2Wrapper = new HashMap<>();
private final Map<OpApplNode, Set<OpApplNodeWrapper>> node2Wrapper = new HashMap<>();
private final Set<OpDefNode> opDefNodes = new HashSet<>();
// Set of OpDefNodes occurring in LetIns and their OpApplNodes.
private final Map<ExprNode, ExprNode> letIns = new HashMap<>();
@@ -288,9 +288,8 @@ public void preVisit(final ExploreNode exploreNode) {
//
// To summarize, this is a clutch that has been hacked to work good enough!
//
// Three if branches 1., 2., and 3. below re not evaluated right after each
// other but in three different invocation of outer preVisit for different
// ExploreNodes.
// if-branches 1., 2., and 3. below are evaluated in three distinct
// invocation of outer preVisit for different ExploreNodes.
if (tool != null && operator instanceof OpDefNode && opApplNode.hasOpcode(0)
&& opApplNode.argsContainOpArgNodes()) {
// 1) Maintain Context for all OpApplNode iff one or more of its args are of
@@ -311,14 +310,13 @@ public void preVisit(final ExploreNode exploreNode) {
// body#setToolObject(tla2sany.semantic.FrontEnd.getToolId(), oan) instead of in
// node2Wrapper. However, node2Wrapper can be gc'ed after the CostModel has been
// created and before state space exploration.
this.node2Wrapper.put((OpApplNode) body, oan);
this.node2Wrapper.computeIfAbsent((OpApplNode) body, key -> new HashSet<>()).add(oan);
}
}
if (this.node2Wrapper.containsKey(opApplNode)) {
// 3) Now it's later. Connect w and oan where
// w is 'Op(s)' and oan is 'LAMBDA e: e...'
final OpApplNodeWrapper w = this.node2Wrapper.get(opApplNode);
w.addChild(oan);
this.node2Wrapper.get(opApplNode).forEach(w -> w.addChild(oan));
}
// End of Higher-order operators/Operators as arguments (LAMBDA, ...)

@@ -0,0 +1,2 @@
SPECIFICATION
Spec
@@ -0,0 +1,10 @@
------------------------------ MODULE L ------------------------------
EXTENDS Naturals

VARIABLE v

ChooseOne(S, P(_)) == CHOOSE x \in S : P(x) /\ \A y \in S : P(y)

Spec == v = ChooseOne({1}, LAMBDA x : TRUE) /\ [][UNCHANGED v]_v

============
@@ -0,0 +1,53 @@
/*******************************************************************************
* Copyright (c) 2020 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 LCoverageTest extends AbstractCoverageTest {

public LCoverageTest () {
super("L");
}

@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, "1"));
assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "2", "1", "0"));

// No 'general' errors recorded
assertFalse(recorder.recorded(EC.GENERAL));

assertFalse(recorder.recorded(EC.TLC_COVERAGE_MISMATCH));
}
}

0 comments on commit b62ee8d

Please sign in to comment.
You can’t perform that action at this time.