diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 408f8af7c..d61d51115 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -66,11 +66,12 @@ namespace storm { template storm::dd::Bdd Model::getStates(std::string const& label) const { STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); - return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates; + return this->getStates(labelToExpressionMap.at(label)); } template storm::dd::Bdd Model::getStates(storm::expressions::Expression const& expression) const { + STORM_LOG_THROW(rowExpressionAdapter != nullptr, storm::exceptions::InvalidOperationException, "Cannot create BDD for expression without expression adapter."); return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates; } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index ec723eedf..7e3c6f43f 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -94,6 +94,10 @@ namespace storm { bool Expression::isFalse() const { return this->getBaseExpression().isFalse(); } + + bool Expression::isSame(storm::expressions::Expression const& other) const { + return this->expressionPtr == other.expressionPtr; + } std::set Expression::getVariables() const { std::set result; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 285a508b2..109439948 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -190,6 +190,14 @@ namespace storm { */ bool isFalse() const; + /*! + * Checks whether the two expressions are the same. Note that this does not check for syntactical or even + * semantical equivalence, but only returns true if both are the very same expressions. + * + * @return True iff the two expressions are the same. + */ + bool isSame(storm::expressions::Expression const& other) const; + /*! * Retrieves whether this expression is a relation expression, i.e., an expression that has a relation * (equal, not equal, less, less or equal, etc.) as its top-level operator. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index c515a9074..3d57f0bdd 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -5,6 +5,8 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" +#include "src/models/symbolic/StandardRewardModel.h" + #include "src/utility/macros.h" #include "src/utility/solver.h" #include "src/exceptions/WrongFormatException.h" @@ -15,7 +17,7 @@ namespace storm { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()), lastReachableStates(ddInformation.manager->getBddZero()) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), currentGame(nullptr) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. @@ -65,10 +67,15 @@ namespace storm { // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); + + // Finally, we build the game the first time. + currentGame = buildGame(); } template void AbstractProgram::refine(std::vector const& predicates) { + STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); + // Add the predicates to the global list of predicates. uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size(); expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end()); @@ -92,20 +99,34 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(newPredicateIndices); + + // Finally, we rebuild the game. + currentGame = buildGame(); + } + + template + storm::models::symbolic::StochasticTwoPlayerGame AbstractProgram::getAbstractGame() { + STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); + return *currentGame; + } + + template + storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { + 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)) { + return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; + } + ++index; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given predicate is illegal, since it was neither used as an initial predicate nor used to refine the abstraction."); } template - storm::dd::Add AbstractProgram::getAbstractAdd() { + 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(); - - // If the abstraction did not change, we can return the most recenty obtained ADD. - if (gameBdd.first == lastAbstractBdd) { - return lastAbstractAdd; - } - - // Otherwise, we remember that the abstract BDD changed and perform a reachability analysis. - lastAbstractBdd = gameBdd.first; // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable}; @@ -114,12 +135,13 @@ namespace storm { } // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract); - lastReachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation); - + storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); + storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + storm::dd::Bdd reachableStates = this->getReachableStates(initialStates, transitionRelation); + // Find the deadlock states in the model. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); - deadlockStates = lastReachableStates && !deadlockStates; + deadlockStates = reachableStates && !deadlockStates; // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = ddInformation.manager->getAddZero(); @@ -127,15 +149,18 @@ namespace storm { deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0) && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).toAdd(); } - // Construct the final game by cutting away the transitions of unreachable states. - lastAbstractAdd = (lastAbstractBdd && lastReachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; - return lastAbstractAdd; - } + // Construct the transition matrix by cutting away the transitions of unreachable states. + storm::dd::Add transitionMatrix = (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; - - template - storm::dd::Bdd AbstractProgram::getReachableStates() { - return lastReachableStates; + std::set usedPlayer2Variables; + for (uint_fast64_t index = 0; index < ddInformation.optionDdVariables.size(); ++index) { + usedPlayer2Variables.insert(usedPlayer2Variables.end(), ddInformation.optionDdVariables[index].first); + } + + 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)); } template diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index c1f54b585..6bb86b2c5 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -10,6 +10,8 @@ #include "src/storage/expressions/Expression.h" +#include "src/models/symbolic/StochasticTwoPlayerGame.h" + namespace storm { namespace utility { namespace solver { @@ -17,6 +19,13 @@ namespace storm { } } + namespace models { + namespace symbolic { + template + class StochasticTwoPlayerGame; + } + } + namespace prism { // Forward-declare concrete Program class. class Program; @@ -40,17 +49,18 @@ namespace storm { /*! * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. * - * @return The ADD representing the game. + * @return The abstract stochastic two player game. */ - storm::dd::Add getAbstractAdd(); + storm::models::symbolic::StochasticTwoPlayerGame getAbstractGame(); /*! - * Retrieves the reachable state space of the abstract game (that was previously retrieved via the - * appropriate method. + * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it + * was either given as an initial predicate or used as a refining predicate later. * - * @return The reachable state space in the form of a BDD. + * @param predicate The predicate for which to retrieve the states. + * @return The BDD representing the set of states. */ - storm::dd::Bdd getReachableStates(); + storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); /*! * Refines the abstract module with the given predicates. @@ -70,6 +80,13 @@ namespace storm { */ storm::dd::Bdd getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation); + /*! + * Builds the stochastic game representing the abstraction of the program. + * + * @return The stochastic game. + */ + std::unique_ptr> buildGame(); + // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; @@ -91,14 +108,8 @@ namespace storm { // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; - // A BDD that is the result of the last abstraction of the system. - storm::dd::Bdd lastAbstractBdd; - - // An ADD that is the result of the last abstraction of the system. - storm::dd::Add lastAbstractAdd; - - // A BDD that is the result of the reachability analysis on the abstraction of the system. - storm::dd::Bdd lastReachableStates; + // The current game-based abstraction. + std::unique_ptr> currentGame; }; } } diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 0fcf721dc..8d5792cf1 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -13,6 +13,8 @@ #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddBdd.h" +#include "src/models/symbolic/StandardRewardModel.h" + #include "src/utility/solver.h" TEST(PrismMenuGame, DieAbstractionTest) { @@ -25,11 +27,10 @@ TEST(PrismMenuGame, DieAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(15, abstraction.getNonZeroCount()); - EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(15, game.getNumberOfTransitions()); + EXPECT_EQ(2, game.getNumberOfStates()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { @@ -42,14 +43,12 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)})); - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(15, abstraction.getNonZeroCount()); - EXPECT_EQ(3, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(15, game.getNumberOfTransitions()); + EXPECT_EQ(3, game.getNumberOfStates()); } TEST(PrismMenuGame, DieFullAbstractionTest) { @@ -77,11 +76,10 @@ TEST(PrismMenuGame, DieFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(20, abstraction.getNonZeroCount()); - EXPECT_EQ(13, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(20, game.getNumberOfTransitions()); + EXPECT_EQ(13, game.getNumberOfStates()); } TEST(PrismMenuGame, CrowdsAbstractionTest) { @@ -95,11 +93,10 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(16, abstraction.getNonZeroCount()); - EXPECT_EQ(2, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(16, game.getNumberOfTransitions()); + EXPECT_EQ(2, game.getNumberOfStates()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { @@ -113,14 +110,12 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")})); - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - EXPECT_EQ(38, abstraction.getNonZeroCount()); - EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + + EXPECT_EQ(38, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest) { @@ -188,11 +183,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(15113, abstraction.getNonZeroCount()); - EXPECT_EQ(8607, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(15113, game.getNumberOfTransitions()); + EXPECT_EQ(8607, game.getNumberOfStates()); } TEST(PrismMenuGame, TwoDiceAbstractionTest) { @@ -208,11 +202,10 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(58, abstraction.getNonZeroCount()); - EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(58, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { @@ -228,14 +221,12 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)})); - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - - EXPECT_EQ(212, abstraction.getNonZeroCount()); - EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount()); + + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + + EXPECT_EQ(212, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { @@ -282,11 +273,10 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(436, abstraction.getNonZeroCount()); - EXPECT_EQ(169, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(436, game.getNumberOfTransitions()); + EXPECT_EQ(169, game.getNumberOfStates()); } TEST(PrismMenuGame, WlanAbstractionTest) { @@ -303,11 +293,10 @@ TEST(PrismMenuGame, WlanAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(307, abstraction.getNonZeroCount()); - EXPECT_EQ(4, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(307, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { @@ -324,14 +313,12 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)})); - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); - - EXPECT_EQ(612, abstraction.getNonZeroCount()); - EXPECT_EQ(8, abstractProgram.getReachableStates().getNonZeroCount()); + + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); + + EXPECT_EQ(612, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); } TEST(PrismMenuGame, WlanFullAbstractionTest) { @@ -446,11 +433,10 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::dd::Add abstraction; - ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + storm::models::symbolic::StochasticTwoPlayerGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(59, abstraction.getNonZeroCount()); - EXPECT_EQ(37, abstractProgram.getReachableStates().getNonZeroCount()); + EXPECT_EQ(59, game.getNumberOfTransitions()); + EXPECT_EQ(37, game.getNumberOfStates()); } #endif \ No newline at end of file