introduced new menu game class

Former-commit-id: f27691f9d6

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<Type> getStates(std::string const& label) const;
+                virtual storm::dd::Bdd<Type> 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<Type> getStates(storm::expressions::Expression const& expression) const;
+                virtual storm::dd::Bdd<Type> 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.

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;
         }
 

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 <storm::expressions::Expression> {
 		bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const {
 			return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer();
 		}
 	};
 }
 
+namespace std {
+    template <>
+    struct hash <storm::expressions::Expression> {
+        size_t operator()(const storm::expressions::Expression& expr) const {
+            return reinterpret_cast<size_t>(expr.getBaseExpressionPointer().get());
+        }
+    };
+}
+
 #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -105,7 +105,7 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::models::symbolic::StochasticTwoPlayerGame<DdType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
+            MenuGame<DdType> AbstractProgram<DdType, ValueType>::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 <storm::dd::DdType DdType, typename ValueType>
-            std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> AbstractProgram<DdType, ValueType>::buildGame() {
+            std::unique_ptr<MenuGame<DdType>> AbstractProgram<DdType, ValueType>::buildGame() {
                 // As long as there is only one module, we only build its game representation.
                 std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> gameBdd = modules.front().getAbstractBdd();
 
@@ -160,7 +160,7 @@ namespace storm {
                 std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
                 allNondeterminismVariables.insert(ddInformation.commandDdVariable);
                 
-                return std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>>(new storm::models::symbolic::StochasticTwoPlayerGame<DdType>(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, nullptr, ddInformation.successorVariables, nullptr, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables));
+                return std::unique_ptr<MenuGame<DdType>>(new MenuGame<DdType>(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap));
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

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<DdType> getAbstractGame();
+                MenuGame<DdType> 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<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> buildGame();
+                std::unique_ptr<MenuGame<DdType>> buildGame();
                 
                 // A factory that can be used to create new SMT solvers.
                 std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
@@ -109,7 +108,7 @@ namespace storm {
                 storm::dd::Add<DdType> commandUpdateProbabilitiesAdd;
                 
                 // The current game-based abstraction.
-                std::unique_ptr<storm::models::symbolic::StochasticTwoPlayerGame<DdType>> currentGame;
+                std::unique_ptr<MenuGame<DdType>> currentGame;
             };
         }
     }

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 <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -4,6 +4,7 @@
 #include <memory>
 #include <vector>
 #include <set>
+#include <map>
 
 #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<std::pair<storm::expressions::Variable, storm::dd::Bdd<DdType>>> optionDdVariables;
+                
+                // A mapping from the predicates to the BDDs.
+                std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap;
             };
             
         }

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<storm::dd::DdType Type>
+            MenuGame<Type>::MenuGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
+                                     storm::dd::Bdd<Type> reachableStates,
+                                     storm::dd::Bdd<Type> initialStates,
+                                     storm::dd::Add<Type> transitionMatrix,
+                                     std::set<storm::expressions::Variable> const& rowVariables,
+                                     std::set<storm::expressions::Variable> const& columnVariables,
+                                     std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                                     std::set<storm::expressions::Variable> const& player1Variables,
+                                     std::set<storm::expressions::Variable> const& player2Variables,
+                                     std::set<storm::expressions::Variable> const& allNondeterminismVariables,
+                                     storm::expressions::Variable const& updateVariable,
+                                     std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, transitionMatrix, rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType Type>
+            storm::dd::Bdd<Type> MenuGame<Type>::getStates(std::string const& label) const {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels.");
+            }
+            
+            template<storm::dd::DdType Type>
+            storm::dd::Bdd<Type> MenuGame<Type>::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<storm::dd::DdType Type>
+            bool MenuGame<Type>::hasLabel(std::string const& label) const {
+                return false;
+            }
+            
+            template class MenuGame<storm::dd::DdType::CUDD>;
+            
+        } // namespace menu_games
+    } // namespace prism
+} // namespace storm
+

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 <map>
+
+#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<storm::dd::DdType Type>
+            class MenuGame : public storm::models::symbolic::StochasticTwoPlayerGame<Type> {
+            public:
+                typedef typename storm::models::symbolic::StochasticTwoPlayerGame<Type>::RewardModelType RewardModelType;
+                
+                MenuGame(MenuGame<Type> const& other) = default;
+                MenuGame& operator=(MenuGame<Type> const& other) = default;
+                
+#ifndef WINDOWS
+                MenuGame(MenuGame<Type>&& other) = default;
+                MenuGame& operator=(MenuGame<Type>&& 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<storm::dd::DdManager<Type>> manager,
+                         storm::dd::Bdd<Type> reachableStates,
+                         storm::dd::Bdd<Type> initialStates,
+                         storm::dd::Add<Type> transitionMatrix,
+                         std::set<storm::expressions::Variable> const& rowVariables,
+                         std::set<storm::expressions::Variable> const& columnVariables,
+                         std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                         std::set<storm::expressions::Variable> const& player1Variables,
+                         std::set<storm::expressions::Variable> const& player2Variables,
+                         std::set<storm::expressions::Variable> const& allNondeterminismVariables,
+                         storm::expressions::Variable const& updateVariable,
+                         std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap);
+                
+                virtual storm::dd::Bdd<Type> getStates(std::string const& label) const override;
+                
+                virtual storm::dd::Bdd<Type> 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<storm::expressions::Expression, storm::dd::Bdd<Type>> expressionToBddMap;
+            };
+            
+        } // namespace menu_games
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_PRISM_MENU_GAMES_MENUGAME_H_ */

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -27,7 +27,7 @@ TEST(PrismMenuGame, DieAbstractionTest) {
     
     storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
     EXPECT_EQ(59, game.getNumberOfTransitions());
     EXPECT_EQ(37, game.getNumberOfStates());