diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index b70c39b97..7c0b49118 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -117,7 +117,7 @@ namespace storm { * @param label The label for which to get the labeled states. * @return The set of states labeled with the requested label in the form of a bit vector. */ - storm::dd::Bdd getStates(std::string const& label) const; + virtual storm::dd::Bdd getStates(std::string const& label) const; /*! * Returns the set of states labeled satisfying the given expression (that must be of boolean type). @@ -125,7 +125,7 @@ namespace storm { * @param expression The expression that needs to hold in the states. * @return The set of states labeled satisfying the given expression. */ - storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; + virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; /*! * Retrieves whether the given label is a valid label in this model. @@ -133,7 +133,7 @@ namespace storm { * @param label The label to be checked for validity. * @return True if the given label is valid in this model. */ - bool hasLabel(std::string const& label) const; + virtual bool hasLabel(std::string const& label) const; /*! * Retrieves the matrix representing the transitions of the model. diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 7e3c6f43f..0f408c9b4 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -95,7 +95,7 @@ namespace storm { return this->getBaseExpression().isFalse(); } - bool Expression::isSame(storm::expressions::Expression const& other) const { + bool Expression::areSame(storm::expressions::Expression const& other) const { return this->expressionPtr == other.expressionPtr; } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 109439948..9455f2acb 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -196,7 +196,7 @@ namespace storm { * * @return True iff the two expressions are the same. */ - bool isSame(storm::expressions::Expression const& other) const; + bool areSame(storm::expressions::Expression const& other) const; /*! * Retrieves whether this expression is a relation expression, i.e., an expression that has a relation @@ -340,14 +340,22 @@ namespace storm { } } -//specialize namespace std { - template<> - struct less < storm::expressions::Expression > { + template <> + struct less { bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const { return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer(); } }; } +namespace std { + template <> + struct hash { + size_t operator()(const storm::expressions::Expression& expr) const { + return reinterpret_cast(expr.getBaseExpressionPointer().get()); + } + }; +} + #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 3d57f0bdd..e0d79e23b 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -105,7 +105,7 @@ namespace storm { } template - storm::models::symbolic::StochasticTwoPlayerGame AbstractProgram::getAbstractGame() { + MenuGame AbstractProgram::getAbstractGame() { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); return *currentGame; } @@ -115,7 +115,7 @@ namespace storm { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); uint_fast64_t index = 0; for (auto const& knownPredicate : expressionInformation.predicates) { - if (knownPredicate.isSame(predicate)) { + if (knownPredicate.areSame(predicate)) { return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; } ++index; @@ -124,7 +124,7 @@ namespace storm { } template - std::unique_ptr> AbstractProgram::buildGame() { + std::unique_ptr> AbstractProgram::buildGame() { // As long as there is only one module, we only build its game representation. std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); @@ -160,7 +160,7 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(ddInformation.commandDdVariable); - return std::unique_ptr>(new storm::models::symbolic::StochasticTwoPlayerGame(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, nullptr, ddInformation.successorVariables, nullptr, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables)); + return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); } template diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 6bb86b2c5..807d5f17e 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -7,11 +7,10 @@ #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" #include "src/storage/prism/menu_games/StateSetAbstractor.h" #include "src/storage/prism/menu_games/AbstractModule.h" +#include "src/storage/prism/menu_games/MenuGame.h" #include "src/storage/expressions/Expression.h" -#include "src/models/symbolic/StochasticTwoPlayerGame.h" - namespace storm { namespace utility { namespace solver { @@ -51,7 +50,7 @@ namespace storm { * * @return The abstract stochastic two player game. */ - storm::models::symbolic::StochasticTwoPlayerGame getAbstractGame(); + MenuGame getAbstractGame(); /*! * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it @@ -85,7 +84,7 @@ namespace storm { * * @return The stochastic game. */ - std::unique_ptr> buildGame(); + std::unique_ptr> buildGame(); // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; @@ -109,7 +108,7 @@ namespace storm { storm::dd::Add commandUpdateProbabilitiesAdd; // The current game-based abstraction. - std::unique_ptr> currentGame; + std::unique_ptr> currentGame; }; } } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index bb98b5a0b..28cfcf886 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -55,6 +55,7 @@ namespace storm { allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); + expressionToBddMap[predicate] = predicateBdds.back().first; } template diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index ef8e08267..80cb914df 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Variable.h" @@ -100,6 +101,9 @@ namespace storm { // The DD variables encoding the nondeterministic choices of player 2. std::vector>> optionDdVariables; + + // A mapping from the predicates to the BDDs. + std::map> expressionToBddMap; }; } diff --git a/src/storage/prism/menu_games/MenuGame.cpp b/src/storage/prism/menu_games/MenuGame.cpp new file mode 100644 index 000000000..d5e0b98f4 --- /dev/null +++ b/src/storage/prism/menu_games/MenuGame.cpp @@ -0,0 +1,53 @@ +#include "src/storage/prism/menu_games/MenuGame.h" + +#include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" + +#include "src/models/symbolic/StandardRewardModel.h" + +namespace storm { + namespace prism { + namespace menu_games { + + template + MenuGame::MenuGame(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& player1Variables, + 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) { + // Intentionally left empty. + } + + template + storm::dd::Bdd MenuGame::getStates(std::string const& label) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels."); + } + + template + storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression) 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(); + } + + template + bool MenuGame::hasLabel(std::string const& label) const { + return false; + } + + template class MenuGame; + + } // namespace menu_games + } // namespace prism +} // namespace storm + diff --git a/src/storage/prism/menu_games/MenuGame.h b/src/storage/prism/menu_games/MenuGame.h new file mode 100644 index 000000000..6c7416068 --- /dev/null +++ b/src/storage/prism/menu_games/MenuGame.h @@ -0,0 +1,78 @@ +#ifndef STORM_PRISM_MENU_GAMES_MENUGAME_H_ +#define STORM_PRISM_MENU_GAMES_MENUGAME_H_ + +#include + +#include "src/models/symbolic/StochasticTwoPlayerGame.h" + +#include "src/utility/OsDetection.h" + +namespace storm { + namespace prism { + namespace menu_games { + + /*! + * This class represents a discrete-time stochastic two-player game. + */ + template + class MenuGame : public storm::models::symbolic::StochasticTwoPlayerGame { + public: + typedef typename storm::models::symbolic::StochasticTwoPlayerGame::RewardModelType RewardModelType; + + MenuGame(MenuGame const& other) = default; + MenuGame& operator=(MenuGame const& other) = default; + +#ifndef WINDOWS + MenuGame(MenuGame&& other) = default; + MenuGame& operator=(MenuGame&& other) = default; +#endif + + /*! + * Constructs a model from the given data. + * + * @param manager The manager responsible for the decision diagrams. + * @param reachableStates A DD representing the reachable states. + * @param initialStates A DD representing the initial states of the model. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param rowVariables The set of row meta variables used in the DDs. + * @param columVariables The set of column meta variables used in the DDs. + * @param rowColumnMetaVariablePairs All pairs of row/column meta variables. + * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1. + * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2. + * @param allNondeterminismVariables The meta variables used to encode the nondeterminism in the model. + * @param updateVariable The variable used to encode the different updates of the probabilistic program. + * @param expressionToBddMap A mapping from expressions (used) in the abstraction to the BDDs encoding + * them. + */ + MenuGame(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& player1Variables, + std::set const& player2Variables, + std::set const& allNondeterminismVariables, + storm::expressions::Variable const& updateVariable, + std::map> const& expressionToBddMap); + + virtual storm::dd::Bdd getStates(std::string const& label) const override; + + virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const override; + + virtual bool hasLabel(std::string const& label) const override; + + private: + // The meta variable used to encode the updates. + storm::expressions::Variable updateVariable; + + // A mapping from expressions that were used in the abstraction process to the the BDDs representing them. + std::map> expressionToBddMap; + }; + + } // namespace menu_games + } // namespace prism +} // namespace storm + +#endif /* STORM_PRISM_MENU_GAMES_MENUGAME_H_ */ diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 8d5792cf1..8eb25f9ed 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -27,7 +27,7 @@ TEST(PrismMenuGame, DieAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(15, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); @@ -45,7 +45,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)})); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(15, game.getNumberOfTransitions()); EXPECT_EQ(3, game.getNumberOfStates()); @@ -76,7 +76,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(20, game.getNumberOfTransitions()); EXPECT_EQ(13, game.getNumberOfStates()); @@ -93,7 +93,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(16, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); @@ -112,7 +112,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")})); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(38, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -183,7 +183,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); @@ -202,7 +202,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(58, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -223,7 +223,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)})); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(212, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -273,7 +273,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(436, game.getNumberOfTransitions()); EXPECT_EQ(169, game.getNumberOfStates()); @@ -293,7 +293,7 @@ TEST(PrismMenuGame, WlanAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(307, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -315,7 +315,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)})); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(612, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -433,7 +433,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(59, game.getNumberOfTransitions()); EXPECT_EQ(37, game.getNumberOfStates());