diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index ee4a46c03..42d4d6ef9 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -147,8 +147,12 @@ namespace storm { storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); auto pl1It = player1ChoiceAsAdd.begin(); uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); + std::cout << "command index " << commandIndex << std::endl; + std::cout << program.get() << std::endl; storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); + player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); + std::cout << concreteCommand << std::endl; // Check whether there are bottom states in the game and whether one of the choices actually picks the // bottom state as the successor. @@ -195,6 +199,7 @@ namespace storm { for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); uint_fast64_t updateIndex = lowerIt->first; + std::cout << "update idx " << updateIndex << std::endl; bool deviates = lowerIt->second != upperIt->second; if (deviates) { for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 9397ed925..892f470b3 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -112,7 +112,7 @@ namespace storm { stream << constant.get().getName() << " (" << constant.get().getType() << ")"; strings.push_back(stream.str()); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " << boost::join(strings, ", ") << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } this->model = this->model->substituteConstants(); diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index a397b0de0..5ed00475e 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1231,22 +1231,7 @@ namespace storm { std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { preparedProgram = program; - if (preparedProgram->hasUndefinedConstants()) { - std::vector> undefinedConstants = preparedProgram->getUndefinedConstants(); - std::stringstream stream; - bool printComma = false; - for (auto const& constant : undefinedConstants) { - if (printComma) { - stream << ", "; - } else { - printComma = true; - } - stream << constant.get().getName() << " (" << constant.get().getType() << ")"; - } - stream << "."; - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); - } - + storm::utility::prism::requireNoUndefinedConstants(preparedProgram.get()); preparedProgram = preparedProgram->substituteConstants(); STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index d4a7d21bf..98715706f 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -17,6 +17,7 @@ #include "src/utility/solver.h" #include "src/utility/dd.h" +#include "src/utility/prism.h" #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" @@ -37,7 +38,8 @@ namespace storm { template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : originalProgram(program), smtSolverFactory(smtSolverFactory) { STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); - + storm::utility::prism::requireNoUndefinedConstants(originalProgram); + // Start by preparing the program. That is, we flatten the modules if there is more than one. if (originalProgram.getNumberOfModules() > 1) { preprocessedProgram = originalProgram.flattenModules(this->smtSolverFactory); @@ -178,19 +180,22 @@ namespace storm { storm::dd::Bdd frontier = initialStates; storm::dd::Bdd frontierPivotStates = frontier && pivotStates; + uint64_t level = 0; bool foundPivotState = !frontierPivotStates.isZero(); if (foundPivotState) { pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); } else { while (!foundPivotState) { frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables); frontierPivotStates = frontier && pivotStates; if (!frontierPivotStates.isZero()) { - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level, " << pivotStates.getNonZeroCount() << " candidates in total."); + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); foundPivotState = true; } + ++level; } } @@ -200,25 +205,41 @@ namespace storm { template bool refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { STORM_LOG_TRACE("Trying refinement after qualitative check."); + // Get all relevant strategies. + storm::dd::Bdd minPlayer1Strategy = prob01.min.first.getPlayer1Strategy(); + storm::dd::Bdd minPlayer2Strategy = prob01.min.first.getPlayer2Strategy(); + storm::dd::Bdd maxPlayer1Strategy = prob01.max.second.getPlayer1Strategy(); + storm::dd::Bdd maxPlayer2Strategy = prob01.max.second.getPlayer2Strategy(); + + // Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2 + // state that is also a prob 0 state.. + minPlayer1Strategy = (maxPlayer1Strategy && prob01.min.first.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy); + // Build the fragment of transitions that is reachable by both the min and the max strategies. - storm::dd::Bdd reachableTransitions = transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy(); + storm::dd::Bdd reachableTransitions = transitionMatrixBdd && minPlayer1Strategy && minPlayer2Strategy && maxPlayer1Strategy && maxPlayer2Strategy; reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); + (minPlayer1Strategy && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); + (maxPlayer1Strategy && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); + (minPlayer2Strategy && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); + (maxPlayer2Strategy && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); + // Require the pivot state to be a [0, 1] state. - pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States(); + // TODO: is this restriction necessary or is it already implied? +// pivotStates &= prob01.min.first.getPlayer1States() && prob01.max.second.getPlayer1States(); // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and // that the difference is not because of a missing strategy in either case. // Start with constructing the player 2 states that have a prob 0 (min) and prob 1 (max) strategy. - storm::dd::Bdd constraint = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.max.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()); + storm::dd::Bdd constraint = minPlayer2Strategy.existsAbstract(game.getPlayer2Variables()) && maxPlayer2Strategy.existsAbstract(game.getPlayer2Variables()); // Now construct all player 2 choices that actually exist and differ in the min and max case. - constraint &= prob01.min.first.getPlayer2Strategy().exclusiveOr(prob01.max.second.getPlayer2Strategy()); + constraint &= minPlayer2Strategy.exclusiveOr(maxPlayer2Strategy); // Then restrict the pivot states by requiring existing and different player 2 choices. - pivotStates &= ((prob01.min.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy()) && constraint).existsAbstract(game.getNondeterminismVariables()); + pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); // We can only refine in case we have a reachable player 1 state with a player 2 successor (under either // player 1's min or max strategy) such that from this player 2 state, both prob0 min and prob0 max define @@ -236,24 +257,24 @@ namespace storm { // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); - storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.min.first.getPlayer1Strategy(); - storm::dd::Bdd lowerChoice1 = (lowerChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); - storm::dd::Bdd lowerChoice2 = (lowerChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; + storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Refining based on lower choice."); - abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); return true; } else { - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy(); - storm::dd::Bdd upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; + storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); - abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + abstractor.refine(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); return true; } else { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); @@ -265,15 +286,37 @@ namespace storm { template void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, storm::dd::Add const& minResult, storm::dd::Add const& maxResult, detail::GameProb01Result const& prob01, std::pair, storm::dd::Bdd> const& minStrategyPair, std::pair, storm::dd::Bdd> const& maxStrategyPair, storm::dd::Bdd const& transitionMatrixBdd) { STORM_LOG_TRACE("Refining after quantitative check."); - // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. - storm::dd::Bdd reachableTransitions = minStrategyPair.second || maxStrategyPair.second; - reachableTransitions = (minStrategyPair.first && reachableTransitions) || (maxStrategyPair.first && reachableTransitions); - reachableTransitions &= transitionMatrixBdd; + // Build the fragment of transitions that is reachable by both the min and the max strategies. + storm::dd::Bdd reachableTransitions = transitionMatrixBdd && minStrategyPair.first && minStrategyPair.second && maxStrategyPair.first && maxStrategyPair.second; reachableTransitions = reachableTransitions.existsAbstract(game.getNondeterminismVariables()); storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables()); - // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different. - pivotStates &= ((minStrategyPair.first || maxStrategyPair.first) && (minStrategyPair.second.exclusiveOr(maxStrategyPair.second))).existsAbstract(game.getNondeterminismVariables()); + // Require the pivot state to be a state with a lower bound strictly smaller than the upper bound. + pivotStates &= minResult.less(maxResult); + + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); + + // Then constrain these states by the requirement that for either the lower or upper player 1 choice the player 2 choices must be different and + // that the difference is not because of a missing strategy in either case. + + // Start with constructing the player 2 states that have a prob 0 (min) and prob 1 (max) strategy. + storm::dd::Bdd constraint = minStrategyPair.second.existsAbstract(game.getPlayer2Variables()) && maxStrategyPair.second.existsAbstract(game.getPlayer2Variables()); + + STORM_LOG_ASSERT(!(constraint && pivotStates).isZero(), "Unable to refine without pivot state candidates."); + + (minStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_min_pl1.dot"); + (maxStrategyPair.first && pivotStates).template toAdd().exportToDot("piv_max_pl1.dot"); + (minStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_min_pl2.dot"); + (maxStrategyPair.second && pivotStates).template toAdd().exportToDot("piv_max_pl2.dot"); + + // Now construct all player 2 choices that actually exist and differ in the min and max case. + constraint &= minStrategyPair.second.exclusiveOr(maxStrategyPair.second); + + STORM_LOG_ASSERT(!(constraint && pivotStates).isZero(), "Unable to refine without pivot state candidates."); + + // Then restrict the pivot states by requiring existing and different player 2 choices. + pivotStates &= ((minStrategyPair.first || maxStrategyPair.first) && constraint).existsAbstract(game.getNondeterminismVariables()); + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. @@ -486,6 +529,8 @@ namespace storm { minMaybeStateResult = solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.getPlayer1States()); minResult += minMaybeStateResult.values; storm::dd::Add initialStateMin = initialStatesAdd * minResult; + initialStatesAdd.exportToDot("init.dot"); + initialStateMin.exportToDot("initmin.dot"); // Here we can only require a non-zero count of *at most* one, because the result may actually be 0. STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() <= 1, "Wrong number of results for initial states. Expected <= 1, but got " << initialStateMin.getNonZeroCount() << "."); minValue = initialStateMin.getMax(); diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp index a34f5e531..e7a4ab354 100644 --- a/src/utility/prism.cpp +++ b/src/utility/prism.cpp @@ -81,6 +81,24 @@ namespace storm { return constantDefinitions; } + + void requireNoUndefinedConstants(storm::prism::Program const& program) { + if (program.hasUndefinedConstants()) { + std::vector> undefinedConstants = program.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + } + } } } diff --git a/src/utility/prism.h b/src/utility/prism.h index 1c94a3395..8abd2f8ec 100644 --- a/src/utility/prism.h +++ b/src/utility/prism.h @@ -26,6 +26,8 @@ namespace storm { storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); + void requireNoUndefinedConstants(storm::prism::Program const& program); + } // namespace prism } // namespace utility } // namespace storm diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 0d628fb75..92c581ecf 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -224,7 +224,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(84, game.getNumberOfTransitions()); + EXPECT_EQ(68, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } @@ -244,7 +244,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(84, game.getNumberOfTransitions()); + EXPECT_EQ(68, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } @@ -450,7 +450,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(324, game.getNumberOfTransitions()); + EXPECT_EQ(276, game.getNumberOfTransitions()); EXPECT_EQ(16, game.getNumberOfStates()); EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } @@ -472,7 +472,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(324, game.getNumberOfTransitions()); + EXPECT_EQ(276, game.getNumberOfTransitions()); EXPECT_EQ(16, game.getNumberOfStates()); EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } @@ -595,7 +595,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(2323, game.getNumberOfTransitions()); + EXPECT_EQ(1335, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } @@ -616,7 +616,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(2323, game.getNumberOfTransitions()); + EXPECT_EQ(1335, game.getNumberOfTransitions()); EXPECT_EQ(12, game.getNumberOfStates()); EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } @@ -639,7 +639,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(4600, game.getNumberOfTransitions()); + EXPECT_EQ(2656, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); } @@ -662,7 +662,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(4600, game.getNumberOfTransitions()); + EXPECT_EQ(2656, game.getNumberOfTransitions()); EXPECT_EQ(24, game.getNumberOfStates()); EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); }