diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index a908ca8ad..d7aa33cb3 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -611,11 +611,12 @@ cuddBddExistAbstractRepresentativeRecur( if (res1 == NULL) { return(NULL); } + // FIXME if (res1 == one) { if (F->ref != 1) { cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); } - return(one); + return(cube); } cuddRef(res1); diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 7efb46245..97f3d46f4 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -51,6 +51,7 @@ namespace storm { std::pair newMetaVariable = ddManager->addMetaVariable(stream.str()); predicateDdVariables.push_back(newMetaVariable); + extendedPredicateDdVariables.push_back(newMetaVariable); predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1)); predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1))); allPredicateIdentities &= predicateIdentities.back(); diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 61dadc76f..ccc15e1ce 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -205,6 +205,96 @@ namespace storm { return reachableStates; } + template + void AbstractProgram::exportToDot(std::string const& filename) const { + std::ofstream out(filename); + out << "digraph game {" << std::endl; + + // Create the player 1 nodes. + storm::dd::Add statesAsAdd = currentGame->getReachableStates().template toAdd(); + for (auto stateValue : statesAsAdd) { + out << "\tpl1_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + out << stateName.str(); + out << " [ label=\""; + if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { + out << "*\", margin=0, width=0, height=0, shape=\"none"; + } else { + out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval"; + } + out << "\" ];" << std::endl; + } + + // Create the nodes of the second player. + storm::dd::Add player2States = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); + for (auto stateValue : player2States) { + out << "\tpl2_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = 0; + for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { + index |= 1; + } + } + out << stateName.str() << "_" << index; + out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; + out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + + // Create the nodes of the probabilistic player. + storm::dd::Add playerPStates = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); + for (auto stateValue : playerPStates) { + out << "\tplp_"; + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + uint_fast64_t index = 0; + for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { + index |= 1; + } + } + stateName << "_" << index; + index = 0; + for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) { + index <<= 1; + if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) { + index |= 1; + } } + out << stateName.str() << "_" << index; + out << " [ shape=\"point\", label=\"\" ];" << std::endl; + out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; + } + +// for (auto stateValue : currentGame->getTransitionMatrix()) { +// std::stringstream stateName; +// +// } + + out << "}" << std::endl; + } + // Explicitly instantiate the class. template class AbstractProgram; template class AbstractProgram; diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 77eb91c07..ec33b3135 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -74,6 +74,13 @@ namespace storm { */ void refine(std::vector const& predicates); + /*! + * Exports the current state of the abstraction in the dot format to the given file. + * + * @param filename The name of the file to which to write the dot output. + */ + void exportToDot(std::string const& filename) const; + private: /*! * Computes the reachable states of the transition relation. diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp index 535357f25..16421829a 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -23,6 +23,11 @@ namespace storm { void PrismMenuGameAbstractor::refine(std::vector const& predicates) { abstractProgram.refine(predicates); } + + template + void PrismMenuGameAbstractor::exportToDot(std::string const& filename) const { + abstractProgram.exportToDot(filename); + } template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h index 655e1a422..b46a4f497 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/abstraction/prism/PrismMenuGameAbstractor.h @@ -16,6 +16,8 @@ namespace storm { virtual storm::abstraction::MenuGame abstract() override; virtual void refine(std::vector const& predicates) override; + void exportToDot(std::string const& filename) const; + private: /// The abstract program that performs the actual abstraction. AbstractProgram abstractProgram; diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9b079d111..f48c6fe9e 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -70,9 +70,9 @@ namespace storm { storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); - // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. storm::abstraction::MenuGame game = abstractor.abstract(); + abstractor.exportToDot("game.dot"); STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds. @@ -95,22 +95,34 @@ namespace storm { void GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); - game.getTransitionMatrix().exportToDot("trans.dot"); - bottomStatesBdd.template toAdd().exportToDot("bottom.dot"); storm::dd::Bdd targetStates = game.getStates(targetStateExpression); if (player1Direction == storm::OptimizationDirection::Minimize) { targetStates |= game.getBottomStates(); } + + transitionMatrixBdd.template toAdd().exportToDot("transbdd.dot"); // Start by computing the states with probability 0/1 when player 2 minimizes. storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); - storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false); // Now compute the states with probability 0/1 when player 2 maximizes. - storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false); storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); +// STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy."); + + STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy."); + +// prob0Min.getPlayer1Strategy().template toAdd().exportToDot("prob0_min_pl1_strat.dot"); + prob0Min.getPlayer2Strategy().template toAdd().exportToDot("prob0_min_pl2_strat.dot"); + + prob1Max.getPlayer1Strategy().template toAdd().exportToDot("prob1_max_pl1_strat.dot"); + prob1Max.getPlayer2Strategy().template toAdd().exportToDot("prob1_max_pl2_strat.dot"); + STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index 379a0ff22..a1432f901 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -117,7 +117,7 @@ namespace storm { // valuations later. for (auto const& metaVariable : *this->metaVariables) { bool metaVariableAppearsInCube = false; - std::vector> localRelenvantDontCareDdVariables; + std::vector> localRelevantDontCareDdVariables; auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); if (ddMetaVariable.getType() == MetaVariableType::Bool) { if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) { @@ -127,7 +127,8 @@ namespace storm { metaVariableAppearsInCube = true; currentValuation.setBooleanValue(metaVariable, true); } else { - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); + currentValuation.setBooleanValue(metaVariable, false); + localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); } } else { int_fast64_t intValue = 0; @@ -141,7 +142,7 @@ namespace storm { } else { // Temporarily leave bit unset so we can iterate trough the other option later. // Add the bit to the relevant don't care bits. - localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); + localRelevantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); } } if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { @@ -152,7 +153,7 @@ namespace storm { // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the // missing bits to later enumerate all possible valuations. if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { - relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end()); + relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelevantDontCareDdVariables.begin(), localRelevantDontCareDdVariables.end()); } } diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 04139d129..55cb72cda 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -955,7 +955,7 @@ namespace storm { solution = tmp; ++iterations; } - + // Since we have determined the inverse of the desired set, we need to complement it now. solution = !solution && model.getReachableStates(); diff --git a/src/utility/graph.h b/src/utility/graph.h index ce5f1cd2f..d57c8a731 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -528,6 +528,26 @@ namespace storm { // Intentionally left empty. } + bool hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + storm::dd::Bdd const& getPlayer1Strategy() { + return player1Strategy.get(); + } + + bool hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + storm::dd::Bdd const& getPlayer2Strategy() { + return player2Strategy.get(); + } + + storm::dd::Bdd const& getStates() const { + return states; + } + storm::dd::Bdd states; boost::optional> player1Strategy; boost::optional> player2Strategy; diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 62c52b0f9..534f33df5 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -215,30 +215,30 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(1, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(2, result.states.getNonZeroCount()); + EXPECT_EQ(3, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -249,7 +249,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { targetStates = game.getStates(initialPredicates[0], true); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -258,33 +258,33 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { EXPECT_TRUE(nonProb0StatesWithStrategy.isZero()); // Proceed by checking whether they select exactly one action in each state. - storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables());; - EXPECT_EQ(0, stateDistributionsUnderStrategies.getNonZeroCount()); + storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); + EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(0, stateDistributionCount.getMax()); + EXPECT_EQ(1, stateDistributionCount.getMax()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(3, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(3, result.states.getNonZeroCount()); + EXPECT_EQ(4, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(2, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); EXPECT_EQ(3, result.states.getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(0, result.states.getNonZeroCount()); + EXPECT_EQ(1, result.states.getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); - EXPECT_EQ(3, result.states.getNonZeroCount()); + EXPECT_EQ(4, result.states.getNonZeroCount()); EXPECT_TRUE(static_cast(result.player1Strategy)); EXPECT_TRUE(static_cast(result.player2Strategy)); @@ -294,7 +294,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(3, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(4, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());