From 972795912a5e48c00bd658a5aa2558f4ea2e7f52 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Sep 2015 21:43:04 +0200 Subject: [PATCH] added some convenience accessor methods in symbolic model/games. added return type for prob01 for games that can also store strategies. added tests for prob0 for games Former-commit-id: f0a8b156caf9014c94841a3cc11102c898f31a12 --- src/models/symbolic/Model.cpp | 5 +++ src/models/symbolic/Model.h | 10 ++++- .../symbolic/StochasticTwoPlayerGame.cpp | 1 + .../prism/menu_games/AbstractProgram.cpp | 2 +- src/storage/prism/menu_games/MenuGame.cpp | 13 +++++- src/storage/prism/menu_games/MenuGame.h | 17 +++++++ src/utility/graph.cpp | 44 ++++++++++--------- src/utility/graph.h | 13 +++++- test/functional/utility/GraphTest.cpp | 35 +++++++++++++++ 9 files changed, 114 insertions(+), 26 deletions(-) diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index d61d51115..c30c75b67 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -90,6 +90,11 @@ namespace storm { return transitionMatrix; } + template + storm::dd::Bdd Model::getQualitativeTransitionMatrix() const { + return this->getTransitionMatrix().notZero(); + } + template std::size_t Model::getSizeInBytes() const { return sizeof(*this) + sizeof(DdNode) * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount()); diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 7c0b49118..9ced28001 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -123,7 +123,7 @@ namespace storm { * Returns the set of states labeled satisfying the given expression (that must be of boolean type). * * @param expression The expression that needs to hold in the states. - * @return The set of states labeled satisfying the given expression. + * @return The set of states satisfying the given expression. */ virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; @@ -148,6 +148,14 @@ namespace storm { * @return A matrix representing the transitions of the model. */ storm::dd::Add& getTransitionMatrix(); + + /*! + * Retrieves the matrix qualitatively (i.e. without probabilities) representing the transitions of the + * model. + * + * @return A matrix representing the qualitative transitions of the model. + */ + storm::dd::Bdd getQualitativeTransitionMatrix() const; /*! * Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices. diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index d8f1df1f6..6b9f72a14 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -28,6 +28,7 @@ namespace storm { : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { // Compute legal player 1 mask. + transitionMatrix.exportToDot("trans.dot"); illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index e0d79e23b..53cafc69e 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -153,7 +153,7 @@ namespace storm { storm::dd::Add transitionMatrix = (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; std::set usedPlayer2Variables; - for (uint_fast64_t index = 0; index < ddInformation.optionDdVariables.size(); ++index) { + for (uint_fast64_t index = 0; index < gameBdd.second; ++index) { usedPlayer2Variables.insert(usedPlayer2Variables.end(), ddInformation.optionDdVariables[index].first); } diff --git a/src/storage/prism/menu_games/MenuGame.cpp b/src/storage/prism/menu_games/MenuGame.cpp index d5e0b98f4..22f25e251 100644 --- a/src/storage/prism/menu_games/MenuGame.cpp +++ b/src/storage/prism/menu_games/MenuGame.cpp @@ -24,7 +24,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, storm::expressions::Variable const& updateVariable, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, transitionMatrix, rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap) { // Intentionally left empty. } @@ -35,9 +35,18 @@ namespace storm { template storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression) const { + return this->getStates(expression, false); + } + + template + storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression, bool negated) const { auto it = expressionToBddMap.find(expression); STORM_LOG_THROW(it != expressionToBddMap.end(), storm::exceptions::InvalidArgumentException, "The given expression was not used in the abstraction process and can therefore not be retrieved."); - return it->second && this->getReachableStates(); + if (negated) { + return !it->second && this->getReachableStates(); + } else { + return it->second && this->getReachableStates(); + } } template diff --git a/src/storage/prism/menu_games/MenuGame.h b/src/storage/prism/menu_games/MenuGame.h index 6c7416068..854dbe5f6 100644 --- a/src/storage/prism/menu_games/MenuGame.h +++ b/src/storage/prism/menu_games/MenuGame.h @@ -59,7 +59,24 @@ namespace storm { virtual storm::dd::Bdd getStates(std::string const& label) const override; + /*! + * Returns the set of states satisfying the given expression (that must be of boolean type). Note that + * for menu games, the given expression must be a predicate that was used to build the abstract game. + * + * @param expression The expression that needs to hold in the states. + * @return The set of states satisfying the given expression. + */ virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const override; + + /*! + * Returns the set of states satisfying the given expression (that must be of boolean type). Note that + * for menu games, the given expression must be a predicate that was used to build the abstract game. + * + * @param expression The expression that needs to hold in the states. + * @param negated If set to true, the result is the set of states not satisfying the expression. + * @return The set of states labeled satisfying the given expression. + */ + storm::dd::Bdd getStates(storm::expressions::Expression const& expression, bool negated) const; virtual bool hasLabel(std::string const& label) const override; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index e377c4f09..e78408a1b 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -690,7 +690,7 @@ namespace storm { } template - void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy) { + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy) { // The solution set. storm::dd::Bdd solution = psiStates; @@ -725,26 +725,28 @@ namespace storm { // Since we have determined the inverse of the desired set, we need to complement it now. solution = !solution && model.getReachableStates(); - // Determine all transitions between prob0 states. - storm::dd::Bdd transitionsBetweenProb0States = solution && (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs())); + return GameProb01Result(solution); - // Determine the distributions that have only successors that are prob0 states. - storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); - - boost::optional> player2StrategyBdd; - if (player2Strategy == OptimizationDirection::Minimize) { - // Pick a distribution that has only prob0 successors. - player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); - } - - boost::optional> player1StrategyBdd; - if (player1Strategy == OptimizationDirection::Minimize) { - // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. - onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables()); - - // Pick a prob0 player 2 state. - onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables()); - } +// // Determine all transitions between prob0 states. +// storm::dd::Bdd transitionsBetweenProb0States = solution && (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs())); +// +// // Determine the distributions that have only successors that are prob0 states. +// storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); +// +// boost::optional> player2StrategyBdd; +// if (player2Strategy == OptimizationDirection::Minimize) { +// // Pick a distribution that has only prob0 successors. +// player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); +// } +// +// boost::optional> player1StrategyBdd; +// if (player1Strategy == OptimizationDirection::Minimize) { +// // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. +// onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables()); +// +// // Pick a prob0 player 2 state. +// onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables()); +// } } template @@ -1079,7 +1081,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - template void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); } // namespace graph } // namespace utility diff --git a/src/utility/graph.h b/src/utility/graph.h index 5118ef726..ccc7cc784 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -433,6 +433,17 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template + struct GameProb01Result { + GameProb01Result(storm::dd::Bdd const& states, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : states(states), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + // Intentionally left empty. + } + + storm::dd::Bdd states; + boost::optional> player1Strategy; + boost::optional> player2Strategy; + }; + /*! * Computes the set of states that have probability 0 given the strategies of the two players. * @@ -442,7 +453,7 @@ namespace storm { * @param psiStates The BDD containing all psi states of the model. */ template - void performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); /*! * Performs a topological sort of the states of the system according to the given transitions. diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index d58de5ca9..6dba4e688 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -88,6 +88,41 @@ TEST(GraphTest, SymbolicProb01MinMax) { EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); } +#ifdef STORM_HAVE_MSAT + +#include "src/storage/prism/menu_games/AbstractProgram.h" + +#include "src/storage/expressions/Expression.h" + +#include "src/utility/solver.h" + +TEST(GraphTest, SymbolicProb0StochasticGame) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); + + storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + + storm::utility::graph::GameProb01Result result1 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(1, result1.states.getNonZeroCount()); + + storm::utility::graph::GameProb01Result result2 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(1, result2.states.getNonZeroCount()); + + storm::utility::graph::GameProb01Result result3 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); + EXPECT_EQ(0, result3.states.getNonZeroCount()); + + storm::utility::graph::GameProb01Result result4 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); + EXPECT_EQ(0, result4.states.getNonZeroCount()); +} + +#endif + TEST(GraphTest, ExplicitProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program);