From 0bd0b963d72005aa6af34bd7626c34ad5a2b614b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 19 Sep 2015 19:38:36 +0200
Subject: [PATCH] introduced new menu game class
Former-commit-id: f27691f9d69eed78a52f05e2f12692a7d0964758
---
src/models/symbolic/Model.h | 6 +-
src/storage/expressions/Expression.cpp | 2 +-
src/storage/expressions/Expression.h | 16 +++-
.../prism/menu_games/AbstractProgram.cpp | 8 +-
.../prism/menu_games/AbstractProgram.h | 9 +--
.../menu_games/AbstractionDdInformation.cpp | 1 +
.../menu_games/AbstractionDdInformation.h | 4 +
src/storage/prism/menu_games/MenuGame.cpp | 53 +++++++++++++
src/storage/prism/menu_games/MenuGame.h | 78 +++++++++++++++++++
.../abstraction/PrismMenuGameTest.cpp | 24 +++---
10 files changed, 172 insertions(+), 29 deletions(-)
create mode 100644 src/storage/prism/menu_games/MenuGame.cpp
create mode 100644 src/storage/prism/menu_games/MenuGame.h
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<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.
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 <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_ */
\ 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::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>
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<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;
};
}
}
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 <storm::dd::DdType DdType, typename ValueType>
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 <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;
};
}
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<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
+
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 <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_ */
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<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());