diff --git a/src/storage/expressions/UnaryExpression.cpp b/src/storage/expressions/UnaryExpression.cpp index 1223368fd..451e0521e 100644 --- a/src/storage/expressions/UnaryExpression.cpp +++ b/src/storage/expressions/UnaryExpression.cpp @@ -18,7 +18,7 @@ namespace storm { } void UnaryExpression::gatherVariables(std::set& variables) const { - return; + this->getOperand()->gatherVariables(variables); } std::shared_ptr const& UnaryExpression::getOperand() const { diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index bd019a4a9..de66bf091 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -57,7 +57,6 @@ namespace storm { if (!recomputeDd) { // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities. cachedDd.first &= computeMissingGlobalIdentities(); - cachedDd.first.toAdd().exportToDot("cmd" + std::to_string(command.get().getGlobalIndex()) + ".dot"); } else { // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver. addMissingPredicates(newRelevantPredicates); @@ -70,7 +69,7 @@ namespace storm { template void AbstractCommand::recomputeCachedBdd() { STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); - + // Create a mapping from source state DDs to their distributions. std::unordered_map, std::vector>> sourceToDistributionsMap; uint_fast64_t modelCounter = 0; @@ -110,7 +109,6 @@ namespace storm { STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); // Cache the result. - resultBdd.toAdd().exportToDot("cmd" + std::to_string(command.get().getGlobalIndex()) + ".dot"); cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); } @@ -118,9 +116,6 @@ namespace storm { std::pair, std::set> AbstractCommand::computeRelevantPredicates(std::vector const& assignments) const { std::pair, std::set> result; - // To start with, all predicates related to the guard are relevant source predicates. - result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); - std::set assignedVariables; for (auto const& assignment : assignments) { // Also, variables appearing on the right-hand side of an assignment are relevant for source state. @@ -147,6 +142,10 @@ namespace storm { std::pair, std::vector>> AbstractCommand::computeRelevantPredicates() const { std::pair, std::vector>> result; + // To start with, all predicates related to the guard are relevant source predicates. + result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); + + // Then, we add the predicates that become relevant, because of some update. for (auto const& update : command.get().getUpdates()) { std::pair, std::set> relevantUpdatePredicates = computeRelevantPredicates(update.getAssignments()); result.first.insert(relevantUpdatePredicates.first.begin(), relevantUpdatePredicates.first.end()); diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 476b18aac..c515a9074 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -69,8 +69,6 @@ namespace storm { template void AbstractProgram::refine(std::vector const& predicates) { - std::cout << " >>>> refine <<<<<<" << std::endl; - // Add the predicates to the global list of predicates. uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size(); expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end()); diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 26b41e87a..0fcf721dc 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -28,7 +28,8 @@ TEST(PrismMenuGame, DieAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(19, abstraction.getNodeCount()); + EXPECT_EQ(15, abstraction.getNonZeroCount()); + EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { @@ -47,7 +48,8 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)})); ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(26, abstraction.getNodeCount()); + EXPECT_EQ(15, abstraction.getNonZeroCount()); + EXPECT_EQ(3, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, DieFullAbstractionTest) { @@ -78,12 +80,8 @@ TEST(PrismMenuGame, DieFullAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(313, abstraction.getNodeCount()); - - storm::dd::Bdd reachableStatesInAbstraction; - ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); - - EXPECT_EQ(13, reachableStatesInAbstraction.getNonZeroCount()); + EXPECT_EQ(20, abstraction.getNonZeroCount()); + EXPECT_EQ(13, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionTest) { @@ -100,7 +98,8 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(46, abstraction.getNodeCount()); + EXPECT_EQ(16, abstraction.getNonZeroCount()); + EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { @@ -117,12 +116,11 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(46, abstraction.getNodeCount()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")})); ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(75, abstraction.getNodeCount()); + EXPECT_EQ(38, abstraction.getNonZeroCount()); + EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest) { @@ -193,10 +191,8 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - storm::dd::Bdd reachableStatesInAbstraction; - ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); - - EXPECT_EQ(8607, reachableStatesInAbstraction.getNonZeroCount()); + EXPECT_EQ(15113, abstraction.getNonZeroCount()); + EXPECT_EQ(8607, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest) { @@ -215,7 +211,8 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(38, abstraction.getNodeCount()); + EXPECT_EQ(58, abstraction.getNonZeroCount()); + EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { @@ -234,15 +231,11 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(38, abstraction.getNodeCount()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)})); ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(95, abstraction.getNodeCount()); - - storm::dd::Bdd reachableStatesInAbstraction; - ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); + EXPECT_EQ(212, abstraction.getNonZeroCount()); + EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { @@ -292,12 +285,8 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(1635, abstraction.getNodeCount()); - - storm::dd::Bdd reachableStatesInAbstraction; - ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); - - EXPECT_EQ(169, reachableStatesInAbstraction.getNonZeroCount()); + EXPECT_EQ(436, abstraction.getNonZeroCount()); + EXPECT_EQ(169, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionTest) { @@ -317,7 +306,8 @@ TEST(PrismMenuGame, WlanAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(221, abstraction.getNodeCount()); + EXPECT_EQ(307, abstraction.getNonZeroCount()); + EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { @@ -337,12 +327,11 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(221, abstraction.getNodeCount()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)})); ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(287, abstraction.getNodeCount()); + EXPECT_EQ(612, abstraction.getNonZeroCount()); + EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanFullAbstractionTest) { @@ -460,12 +449,8 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { storm::dd::Add abstraction; ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(2861, abstraction.getNodeCount()); - - storm::dd::Bdd reachableStatesInAbstraction; - ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); - - EXPECT_EQ(37, reachableStatesInAbstraction.getNonZeroCount()); + EXPECT_EQ(59, abstraction.getNonZeroCount()); + EXPECT_EQ(37, abstractProgram.getReachableStates().getNonZeroCount()); } #endif \ No newline at end of file