diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 06e6fead7..b78242fb7 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -360,11 +360,11 @@ namespace storm { return this->labels; } - std::vector Program::getAllGuards() const { + std::vector Program::getAllGuards(bool negated) const { std::vector allGuards; for (auto const& module : modules) { for (auto const& command : module.getCommands()) { - allGuards.push_back(command.getGuardExpression()); + allGuards.push_back(negated ? !command.getGuardExpression() : command.getGuardExpression()); } } return allGuards; diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 188fbb58f..556273901 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -363,9 +363,10 @@ namespace storm { /*! * Retrieves all guards appearing in the program. * + * @param negated A flag indicating whether the guards should be negated. * @return All guards appearing in the program. */ - std::vector getAllGuards() const; + std::vector getAllGuards(bool negated = false) const; /*! * Retrieves the expression associated with the given label, if it exists. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 3193d4fd6..acf5878e2 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -17,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>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(), *this->smtSolverFactory), currentGame(nullptr) { + 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>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, 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. @@ -71,7 +71,7 @@ namespace storm { // 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()); + expressionInformation.addPredicates(predicates); // Create DD variables and some auxiliary data structures for the new predicates. for (auto const& predicate : predicates) { @@ -140,10 +140,11 @@ namespace storm { if (addedAllGuards) { bottomStates = ddInformation.manager->getBddZero(); } else { - // bottomStates = bottomStateAbstractor.getAbstractStates(); + bottomStateAbstractor.constrain(reachableStates); + bottomStates = bottomStateAbstractor.getAbstractStates(); } - // std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl; + std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl; // Find the deadlock states in the model. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 92905a499..6b7dcc8e0 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -16,7 +16,7 @@ namespace storm { namespace menu_games { template - AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager, std::vector const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()) { + AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager, std::vector const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()), bddVariableIndexToPredicateMap() { for (auto const& predicate : initialPredicates) { this->addPredicate(predicate); } @@ -58,6 +58,7 @@ namespace storm { sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); expressionToBddMap[predicate] = predicateBdds.back().first; + bddVariableIndexToPredicateMap[predicateIdentities.back().getIndex()] = predicate; } template diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index 6368139c0..d3b86d12c 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -5,6 +5,7 @@ #include #include #include +#include #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Variable.h" @@ -105,6 +106,9 @@ namespace storm { // A mapping from the predicates to the BDDs. std::map> expressionToBddMap; + + // A mapping from the indices of the BDD variables to the predicates. + std::unordered_map bddVariableIndexToPredicateMap; }; } diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp index d82401545..b3fd5a64a 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp @@ -11,6 +11,16 @@ namespace storm { // Intentionally left empty. } + void AbstractionExpressionInformation::addPredicate(storm::expressions::Expression const& predicate) { + predicates.push_back(predicate); + } + + void AbstractionExpressionInformation::addPredicates(std::vector const& predicates) { + for (auto const& predicate : predicates) { + this->addPredicate(predicate); + } + } + } } } \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h index b2961b7a1..2037fa364 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h @@ -26,6 +26,20 @@ namespace storm { */ AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector const& predicates = std::vector(), std::set const& variables = std::set(), std::vector const& rangeExpressions = std::vector()); + /*! + * Adds the given predicate. + * + * @param predicate The predicate to add. + */ + void addPredicate(storm::expressions::Expression const& predicate); + + /*! + * Adds the given predicates. + * + * @param predicates The predicates to add. + */ + void addPredicates(std::vector const& predicates); + // The manager responsible for the expressions of the program and the SMT solvers. storm::expressions::ExpressionManager& manager; diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp index fa1e91127..9208273a8 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.cpp +++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp @@ -13,7 +13,7 @@ namespace storm { namespace menu_games { template - StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraintBdd(ddInformation.manager->getBddOne()) { + StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) { // Assert all range expressions to enforce legal variable values. for (auto const& rangeExpression : expressionInformation.rangeExpressions) { @@ -52,12 +52,21 @@ namespace storm { } template - void StateSetAbstractor::refine(std::vector const& newPredicates, boost::optional> const& constraintBdd) { + void StateSetAbstractor::refine(std::vector const& newPredicates) { // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction. for (auto const& predicateIndex : newPredicates) { variablePartition.addExpression(expressionInformation.predicates[predicateIndex]); } - this->recomputeCachedBdd(); + needsRecomputation = true; + } + + template + void StateSetAbstractor::constrain(storm::dd::Bdd const& newConstraint) { + // If the constraint is different from the last one, we add it to the solver. + if (newConstraint != this->constraint) { + constraint = newConstraint; + this->pushConstraintBdd(); + } } template @@ -90,11 +99,17 @@ namespace storm { if (!recomputeBdd) { return; } - + + // Before adding the missing predicates, we need to remove the constraint BDD. + this->popConstraintBdd(); + // If we need to recompute the BDD, we start by introducing decision variables and the corresponding // constraints in the SMT problem. addMissingPredicates(newRelevantPredicateIndices); + // Then re-add the constraint BDD. + this->pushConstraintBdd(); + STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); storm::dd::Bdd result = ddInformation.manager->getBddZero(); @@ -104,8 +119,34 @@ namespace storm { cachedBdd = result; } + template + void StateSetAbstractor::popConstraintBdd() { + // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver. + if (!this->constraint.isOne()) { + smtSolver->pop(); + } + } + + template + void StateSetAbstractor::pushConstraintBdd() { + // Create a new backtracking point before adding the constraint. + smtSolver->push(); + + // Then add the constraint. + std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap); + + std::cout << "adding expressions... " << std::endl; + for (auto const& expression : result.first) { + std::cout << expression << std::endl; + smtSolver->add(expression); + } + } + template storm::dd::Bdd StateSetAbstractor::getAbstractStates() { + if (needsRecomputation) { + this->recomputeCachedBdd(); + } return cachedBdd; } diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h index bbdc8f3b6..7fff45bff 100644 --- a/src/storage/prism/menu_games/StateSetAbstractor.h +++ b/src/storage/prism/menu_games/StateSetAbstractor.h @@ -65,7 +65,14 @@ namespace storm { * * @param newPredicateIndices The indices of the new predicates. */ - void refine(std::vector const& newPredicateIndices, boost::optional> const& constraintBdd = boost::none); + void refine(std::vector const& newPredicateIndices); + + /*! + * Constraints the abstract states with the given BDD. + * + * @param newConstraint The BDD used as the constraint. + */ + void constrain(storm::dd::Bdd const& newConstraint); /*! * Retrieves the set of abstract states matching all predicates added to this abstractor. @@ -82,6 +89,16 @@ namespace storm { */ void addMissingPredicates(std::set const& newRelevantPredicateIndices); + /*! + * Adds the current constraint BDD to the solver. + */ + void pushConstraintBdd(); + + /*! + * Removes the current constraint BDD (if any) from the solver. + */ + void popConstraintBdd(); + /*! * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. */ @@ -124,7 +141,7 @@ namespace storm { storm::dd::Bdd cachedBdd; // This BDD currently constrains the search for solutions. - storm::dd::Bdd constraintBdd; + storm::dd::Bdd constraint; }; } }