From 4f7eaa0a4387a98c1025dd2e0e4f401160eb74ec Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 9 Aug 2016 16:57:37 +0200 Subject: [PATCH] some more work towards abstraction refinement Former-commit-id: 360cb016c32cb9397ee3b762cabe1144274e6601 --- src/abstraction/MenuGame.cpp | 6 +++ src/abstraction/StateSetAbstractor.cpp | 2 +- src/abstraction/StateSetAbstractor.h | 3 +- src/abstraction/prism/AbstractCommand.cpp | 2 +- src/abstraction/prism/AbstractProgram.cpp | 6 +-- src/abstraction/prism/AbstractProgram.h | 4 +- .../prism/PrismMenuGameAbstractor.cpp | 8 +++- .../prism/PrismMenuGameAbstractor.h | 2 +- .../abstraction/GameBasedMdpModelChecker.cpp | 38 ++++++++++++++++++- .../abstraction/GameBasedMdpModelChecker.h | 14 ++++--- src/models/symbolic/Model.cpp | 5 +++ src/storage/prism/Program.cpp | 8 +--- src/storage/prism/Program.h | 11 +----- 13 files changed, 76 insertions(+), 33 deletions(-) diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index 6e4420aa9..4ada7add8 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -5,6 +5,7 @@ #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" +#include "src/storage/dd/DdManager.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -41,6 +42,11 @@ namespace storm { template storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression, bool negated) const { + if (expression.isTrue()) { + return this->getReachableStates(); + } else if (expression.isFalse()) { + return this->getManager().getBddZero(); + } 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."); if (negated) { diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index e3d6b6949..97874d080 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -11,7 +11,7 @@ namespace storm { namespace abstraction { template - StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) { + StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, std::shared_ptr const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) { // Assert all state predicates. for (auto const& predicate : statePredicates) { diff --git a/src/abstraction/StateSetAbstractor.h b/src/abstraction/StateSetAbstractor.h index dad33e664..20950939c 100644 --- a/src/abstraction/StateSetAbstractor.h +++ b/src/abstraction/StateSetAbstractor.h @@ -8,6 +8,7 @@ #include "src/storage/dd/DdType.h" +#include "src/utility/solver.h" #include "src/solver/SmtSolver.h" #include "src/abstraction/LocalExpressionInformation.h" @@ -51,7 +52,7 @@ namespace storm { * supposed to abstract. * @param smtSolverFactory A factory that can create new SMT solvers. */ - StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, std::shared_ptr const& smtSolverFactory = std::make_shared()); /*! * Refines the abstractor by making the given predicates new abstract predicates. diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index ca6a3a141..ea39a5922 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -32,7 +32,7 @@ namespace storm { // Refine the command based on all initial predicates. std::vector allPredicateIndices(abstractionInformation.getNumberOfPredicates()); - for (auto index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) { + for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 1eeeef9ad..441dd07b6 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -17,11 +17,11 @@ namespace storm { namespace prism { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, + AbstractProgram::AbstractProgram(storm::prism::Program const& program, std::vector const& initialPredicates, - std::unique_ptr&& smtSolverFactory, + std::shared_ptr const& smtSolverFactory, bool addAllGuards) - : program(program), smtSolverFactory(std::move(smtSolverFactory)), abstractionInformation(expressionManager), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) { + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), 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. diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 435d905d8..39c5e0e78 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -45,7 +45,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates. */ - AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory = std::make_unique(), bool addAllGuards = false); + AbstractProgram(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool addAllGuards = false); AbstractProgram(AbstractProgram const&) = default; AbstractProgram& operator=(AbstractProgram const&) = default; @@ -97,7 +97,7 @@ namespace storm { std::reference_wrapper program; // A factory that can be used to create new SMT solvers. - std::unique_ptr smtSolverFactory; + std::shared_ptr smtSolverFactory; // An object containing all information about the abstraction like predicates and the corresponding DDs. AbstractionInformation abstractionInformation; diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp index 1d965f344..535357f25 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -1,5 +1,7 @@ #include "src/abstraction/prism/PrismMenuGameAbstractor.h" +#include "src/models/symbolic/StandardRewardModel.h" + #include "src/settings/SettingsManager.h" #include "src/settings/modules/AbstractionSettings.h" @@ -8,7 +10,7 @@ namespace storm { namespace prism { template - PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule().isAddAllGuardsSet()) { + PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule().isAddAllGuardsSet()) { // Intentionally left empty. } @@ -21,7 +23,9 @@ namespace storm { void PrismMenuGameAbstractor::refine(std::vector const& predicates) { abstractProgram.refine(predicates); } - + + template class PrismMenuGameAbstractor; + template class PrismMenuGameAbstractor; } } } \ No newline at end of file diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h index 44301bc7f..655e1a422 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/abstraction/prism/PrismMenuGameAbstractor.h @@ -11,7 +11,7 @@ namespace storm { template class PrismMenuGameAbstractor : public MenuGameAbstractor { public: - PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory = std::make_shared()); virtual storm::abstraction::MenuGame abstract() override; virtual void refine(std::vector const& predicates) override; diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a24189152..388ffcfa5 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -8,6 +8,7 @@ #include "src/logic/FragmentSpecification.h" +#include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" @@ -18,7 +19,7 @@ namespace storm { namespace modelchecker { template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory) : originalProgram(program), expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory) : originalProgram(program), smtSolverFactory(smtSolverFactory) { STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); // Start by preparing the program. That is, we flatten the modules if there is more than one. @@ -57,18 +58,31 @@ namespace storm { std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); + // Set up initial predicates. std::vector initialPredicates; initialPredicates.push_back(targetStateExpression); if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) { initialPredicates.push_back(constraintExpression); } - storm::abstraction::prism::PrismMenuGameAbstractor abstractor(expressionManager, preprocessedProgram, initialPredicates, *smtSolverFactory); + + // Derive the optimization direction for player 1 (assuming menu-game abstraction). + storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; + + storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); + // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + storm::abstraction::MenuGame game = abstractor.abstract(); + STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds. // Note that we have to deal with bottom states if not all guards were added in the beginning. // Also note that it might be the case that not both bounds need to be computed if there is a bound given in checkTask. + computeProb01States(player1Direction, game, constraintExpression, targetStateExpression); + +// std::unique_ptr> gameSolverFactory = std::make_unique>(); +// gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates()); +// storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables // 3. if the bounds suffice to complete checkTask, return result now. @@ -77,6 +91,26 @@ namespace storm { return nullptr; } + template + void GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { + storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); + game.getTransitionMatrix().exportToDot("trans.dot"); + bottomStatesBdd.template toAdd().exportToDot("bottom.dot"); + + // Start by computing the states with probability 0/1 for the case in which player 2 minimizes. + storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true); + + // Now compute the states with probability 0/1 for the case in which player 2 maximizes. + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true); + + STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); + STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); + + } + template storm::expressions::Expression GameBasedMdpModelChecker::getExpression(storm::logic::Formula const& formula) { STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index 0c6658fee..a23f68021 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -10,6 +10,11 @@ #include "src/storage/dd/DdType.h" namespace storm { + namespace abstraction { + template + class MenuGame; + } + namespace modelchecker { template class GameBasedMdpModelChecker : public AbstractModelChecker { @@ -21,7 +26,7 @@ namespace storm { * @param program The program that implicitly specifies the model to check. * @param smtSolverFactory A factory used to create SMT solver when necessary. */ - explicit GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory = std::make_unique()); + explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::shared_ptr const& smtSolverFactory = std::make_shared()); virtual ~GameBasedMdpModelChecker() override; @@ -33,6 +38,8 @@ namespace storm { private: std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + void computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + storm::expressions::Expression getExpression(storm::logic::Formula const& formula); // The original program that was used to create this model checker. @@ -42,11 +49,8 @@ namespace storm { // original program. storm::prism::Program preprocessedProgram; - /// The expression manager over which to build expressions during the abstraction. - storm::expressions::ExpressionManager& expressionManager; - // A factory that is used for creating SMT solvers when needed. - std::unique_ptr smtSolverFactory; + std::shared_ptr smtSolverFactory; }; } } diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 97c1537c4..945faba47 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -72,6 +72,11 @@ namespace storm { template storm::dd::Bdd Model::getStates(storm::expressions::Expression const& expression) const { + if (expression.isTrue()) { + return this->getReachableStates(); + } else if (expression.isFalse()) { + return manager->getBddZero(); + } 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/prism/Program.cpp b/src/storage/prism/Program.cpp index d1551eef9..21f999a40 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1231,7 +1231,7 @@ namespace storm { return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct()); } - Program Program::flattenModules(std::unique_ptr const& smtSolverFactory) const { + Program Program::flattenModules(std::shared_ptr const& smtSolverFactory) const { // If the current program has only one module, we can simply return a copy. if (this->getNumberOfModules() == 1) { return Program(*this); @@ -1512,11 +1512,7 @@ namespace storm { return this->indexToActionMap.rbegin()->first; } - storm::expressions::ExpressionManager const& Program::getManager() const { - return *this->manager; - } - - storm::expressions::ExpressionManager& Program::getManager() { + storm::expressions::ExpressionManager& Program::getManager() const { return *this->manager; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 1297f9b35..baa90938d 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -546,7 +546,7 @@ namespace storm { * @param smtSolverFactory an SMT solver factory to use. If none is given, the default one is used. * @return The resulting program. */ - Program flattenModules(std::unique_ptr const& smtSolverFactory = std::unique_ptr(new storm::utility::solver::SmtSolverFactory())) const; + Program flattenModules(std::shared_ptr const& smtSolverFactory = std::shared_ptr(new storm::utility::solver::SmtSolverFactory())) const; friend std::ostream& operator<<(std::ostream& stream, Program const& program); @@ -555,14 +555,7 @@ namespace storm { * * @return The manager responsible for the expressions of this program. */ - storm::expressions::ExpressionManager const& getManager() const; - - /*! - * Retrieves the manager responsible for the expressions of this program. - * - * @return The manager responsible for the expressions of this program. - */ - storm::expressions::ExpressionManager& getManager(); + storm::expressions::ExpressionManager& getManager() const; /*! *