diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 2fc5446ea..ff28089b2 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -14,13 +14,13 @@ namespace storm { namespace abstraction { template - AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& allVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), variables(allVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), expressionToBddMap() { + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : expressionManager(expressionManager), equivalenceChecker(std::move(smtSolver)), abstractedVariables(abstractedVariables), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()), expressionToBddMap() { // Intentionally left empty. } template void AbstractionInformation::addExpressionVariable(storm::expressions::Variable const& variable) { - variables.insert(variable); + abstractedVariables.insert(variable); } template @@ -29,11 +29,6 @@ namespace storm { addConstraint(constraint); } - template - std::set AbstractionInformation::getExpressionVariables() const { - return variables; - } - template void AbstractionInformation::addConstraint(storm::expressions::Expression const& constraint) { constraints.push_back(constraint); @@ -68,8 +63,8 @@ namespace storm { allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); - orderedSourceVariables.push_back(newMetaVariable.first); - orderedSuccessorVariables.push_back(newMetaVariable.second); + orderedSourcePredicateVariables.push_back(newMetaVariable.first); + orderedSuccessorPredicateVariables.push_back(newMetaVariable.second); ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; expressionToBddMap[predicate] = predicateBdds[predicateIndex].first && !bottomStateBdds.first; @@ -164,8 +159,8 @@ namespace storm { } template - std::set const& AbstractionInformation::getVariables() const { - return variables; + std::set const& AbstractionInformation::getAbstractedVariables() const { + return abstractedVariables; } template @@ -284,15 +279,15 @@ namespace storm { } template - std::vector const& AbstractionInformation::getOrderedSuccessorVariables() const { - return orderedSuccessorVariables; + std::vector const& AbstractionInformation::getOrderedSourcePredicateVariables() const { + return orderedSourcePredicateVariables; } template - std::vector const& AbstractionInformation::getOrderedSourceVariables() const { - return orderedSourceVariables; + std::vector const& AbstractionInformation::getOrderedSuccessorPredicateVariables() const { + return orderedSuccessorPredicateVariables; } - + template storm::dd::Bdd const& AbstractionInformation::getAllPredicateIdentities() const { return allPredicateIdentities; @@ -432,8 +427,8 @@ namespace storm { storm::dd::Add add = state.template toAdd(); auto it = add.begin(); auto stateValuePair = *it; - for (uint_fast64_t index = 0; index < this->getOrderedSourceVariables().size(); ++index) { - auto const& successorVariable = this->getOrderedSourceVariables()[index]; + for (uint_fast64_t index = 0; index < this->getOrderedSourcePredicateVariables().size(); ++index) { + auto const& successorVariable = this->getOrderedSourcePredicateVariables()[index]; if (stateValuePair.first.getBooleanValue(successorVariable)) { statePredicates.set(index); } @@ -452,8 +447,8 @@ namespace storm { uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount()); storm::storage::BitVector successor(this->getNumberOfPredicates()); - for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) { - auto const& successorVariable = this->getOrderedSuccessorVariables()[index]; + for (uint_fast64_t index = 0; index < this->getOrderedSuccessorPredicateVariables().size(); ++index) { + auto const& successorVariable = this->getOrderedSuccessorPredicateVariables()[index]; if (successorValuePair.first.getBooleanValue(successorVariable)) { successor.set(index); } @@ -475,8 +470,8 @@ namespace storm { auto stateValuePair = *it; uint64_t choiceIndex = this->decodePlayer1Choice(stateValuePair.first, this->getPlayer1VariableCount()); uint64_t updateIndex = this->decodeAux(stateValuePair.first, 0, this->getAuxVariableCount()); - for (uint_fast64_t index = 0; index < this->getOrderedSourceVariables().size(); ++index) { - auto const& successorVariable = this->getOrderedSourceVariables()[index]; + for (uint_fast64_t index = 0; index < this->getOrderedSourcePredicateVariables().size(); ++index) { + auto const& successorVariable = this->getOrderedSourcePredicateVariables()[index]; if (stateValuePair.first.getBooleanValue(successorVariable)) { statePredicates.set(index); @@ -486,6 +481,41 @@ namespace storm { return std::make_tuple(statePredicates, choiceIndex, updateIndex); } + template + std::pair, uint64_t> AbstractionInformation::addLocationVariables(uint64_t highestLocationIndex) { + locationVariablePairs.emplace_back(ddManager->addMetaVariable("loc_" + std::to_string(locationVariablePairs.size()), 0, highestLocationIndex)); + allSourceLocationVariables.insert(locationVariablePairs.back().first); + sourceVariables.insert(locationVariablePairs.back().first); + allSuccessorLocationVariables.insert(locationVariablePairs.back().second); + successorVariables.insert(locationVariablePairs.back().second); + extendedPredicateDdVariables.emplace_back(locationVariablePairs.back()); + return std::make_pair(locationVariablePairs.back(), locationVariablePairs.size() - 1); + } + + template + storm::expressions::Variable AbstractionInformation::getLocationVariable(uint64_t locationVariableIndex, bool source) const { + if (source) { + return locationVariablePairs[locationVariableIndex].first; + } else { + return locationVariablePairs[locationVariableIndex].second; + } + } + + template + std::set const& AbstractionInformation::getSourceLocationVariables() const { + return allSourceLocationVariables; + } + + template + std::set const& AbstractionInformation::getSuccessorLocationVariables() const { + return allSuccessorLocationVariables; + } + + template + storm::dd::Bdd AbstractionInformation::encodeLocation(storm::expressions::Variable const& locationVariable, uint64_t locationIndex) const { + return this->getDdManager().getEncoding(locationVariable, locationIndex); + } + template class AbstractionInformation; template class AbstractionInformation; diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index b0336afe5..4a2276e6b 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -34,11 +34,11 @@ namespace storm { * Creates a new abstraction information object. * * @param expressionManager The manager responsible for all variables and expressions during the abstraction process. - * @param allVariables All expression variables that can appear in predicates known to this object. + * @param abstractedVariables All expression variables that can appear in predicates known to this object. * @param smtSolver An SMT solver that is used to detect equivalent predicates. * @param ddManager The manager responsible for the DDs. */ - AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& allVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager = std::make_shared>()); + AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& abstractedVariables, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager = std::make_shared>()); /*! * Adds the given variable. @@ -46,13 +46,6 @@ namespace storm { * @param variable The variable to add. */ void addExpressionVariable(storm::expressions::Variable const& variable); - - /*! - * Retrieves all known variables that may be used in predicates. - * - * @return All known variables. - */ - std::set getExpressionVariables() const; /*! * Adds the given variable whose range is restricted. @@ -181,7 +174,7 @@ namespace storm { * * @return The set of known variables. */ - std::set const& getVariables() const; + std::set const& getAbstractedVariables() const; /*! * Creates the given number of variables used to encode the choices of player 1/2 and auxiliary information. @@ -347,20 +340,6 @@ namespace storm { * @return All successor meta variables. */ std::set const& getSuccessorVariables() const; - - /*! - * Retrieves the ordered collection of source meta variables. - * - * @return All source meta variables. - */ - std::vector const& getOrderedSourceVariables() const; - - /*! - * Retrieves the ordered collection of successor meta variables. - * - * @return All successor meta variables. - */ - std::vector const& getOrderedSuccessorVariables() const; /*! * Retrieves a BDD representing the identities of all predicates. @@ -466,7 +445,46 @@ namespace storm { */ std::tuple decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd const& stateChoiceAndUpdate) const; - private: + /*! + * Adds a location variable of appropriate range and returns the pair of meta variables. + */ + std::pair, uint64_t> addLocationVariables(uint64_t highestLocationIndex); + + /*! + * Retrieves the location variable with the given index as either source or successor. + */ + storm::expressions::Variable getLocationVariable(uint64_t locationVariableIndex, bool source) const; + + /*! + * Retrieves the source location variables. + */ + std::set const& getSourceLocationVariables() const; + + /*! + * Retrieves the source location variables. + */ + std::set const& getSuccessorLocationVariables() const; + + /*! + * Encodes the given location index as either source or successor. + */ + storm::dd::Bdd encodeLocation(storm::expressions::Variable const& locationVariable, uint64_t locationIndex) const; + + protected: + /*! + * Retrieves the ordered collection of source predicate meta variables. + * + * @return All source meta variables. + */ + std::vector const& getOrderedSourcePredicateVariables() const; + + /*! + * Retrieves the ordered collection of successor predicate meta variables. + * + * @return All successor meta variables. + */ + std::vector const& getOrderedSuccessorPredicateVariables() const; + /*! * Encodes the given index with the given number of variables from the given variables. * @@ -503,8 +521,8 @@ namespace storm { /// The current set of predicates used in the abstraction. std::vector predicates; - /// The set of all variables. - std::set variables; + /// The set of all abstracted variables. + std::set abstractedVariables; /// The expressions characterizing legal variable values. std::vector constraints; @@ -527,10 +545,10 @@ namespace storm { std::set successorVariables; /// An ordered collection of the source variables. - std::vector orderedSourceVariables; + std::vector orderedSourcePredicateVariables; /// An ordered collection of the successor variables. - std::vector orderedSuccessorVariables; + std::vector orderedSuccessorPredicateVariables; /// The BDDs corresponding to the predicates. std::vector, storm::dd::Bdd>> predicateBdds; @@ -570,6 +588,16 @@ namespace storm { /// A mapping from expressions to the corresponding BDDs. std::map> expressionToBddMap; + + /// The location variable pairs (source/successor). + std::vector> locationVariablePairs; + + // All source location variables. + std::set allSourceLocationVariables; + + // All successor location variables. + std::set allSuccessorLocationVariables; + }; } diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp new file mode 100644 index 000000000..adc6525c1 --- /dev/null +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -0,0 +1,195 @@ +#include "storm/abstraction/ExpressionTranslator.h" + +#include "storm/abstraction/AbstractionInformation.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Bdd.h" + +#include "storm/storage/expressions/Expression.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace abstraction { + + using namespace storm::expressions; + + template + ExpressionTranslator::ExpressionTranslator(AbstractionInformation& abstractionInformation, std::unique_ptr&& smtSolver) : abstractionInformation(abstractionInformation), equivalenceChecker(std::move(smtSolver)), locationVariables(abstractionInformation.getSourceLocationVariables()), abstractedVariables(abstractionInformation.getAbstractedVariables()) { + // Intentionally left empty. + } + + template + storm::dd::Bdd ExpressionTranslator::translate(storm::expressions::Expression const& expression) { + return boost::any_cast>(expression.accept(*this, boost::none)); + } + + template + boost::any ExpressionTranslator::visit(IfThenElseExpression const& expression, boost::any const& data) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } + + template + boost::any ExpressionTranslator::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + // Check whether the expression is either fully contained in the location variables fragment or the abstracted + // variables fragment. + std::set variablesInExpression; + expression.gatherVariables(variablesInExpression); + + std::set tmp; + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), locationVariables.begin(), locationVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasLocationVariables = !tmp.empty(); + + tmp.clear(); + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), abstractedVariables.begin(), abstractedVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasAbstractedVariables = !tmp.empty(); + + STORM_LOG_THROW(hasLocationVariables || hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions without variables are currently not supported by the abstraction expression translator."); + + if (hasAbstractedVariables && !hasLocationVariables) { + for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) { + if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) { + return abstractionInformation.get().encodePredicateAsSource(predicateIndex); + } + } + + // At this point, none of the predicates was found to be equivalent, so we split the expression. + } + + storm::dd::Bdd left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + storm::dd::Bdd right = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + switch (expression.getOperatorType()) { + case BinaryBooleanFunctionExpression::OperatorType::And: return left && right; + case BinaryBooleanFunctionExpression::OperatorType::Or: return left || right; + case BinaryBooleanFunctionExpression::OperatorType::Xor: return left.exclusiveOr(right); + case BinaryBooleanFunctionExpression::OperatorType::Implies: return !left || right; + case BinaryBooleanFunctionExpression::OperatorType::Iff: return (left && right) || (!left && !right); + } + } + + template + boost::any ExpressionTranslator::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } + + template + boost::any ExpressionTranslator::visit(BinaryRelationExpression const& expression, boost::any const& data) { + // Check whether the expression is either fully contained in the location variables fragment or the abstracted + // variables fragment. + std::set variablesInExpression; + expression.gatherVariables(variablesInExpression); + + std::set tmp; + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), locationVariables.begin(), locationVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasLocationVariables = !tmp.empty(); + + tmp.clear(); + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), abstractedVariables.begin(), abstractedVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasAbstractedVariables = !tmp.empty(); + + STORM_LOG_THROW(hasLocationVariables || hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions without variables are currently not supported by the abstraction expression translator."); + STORM_LOG_THROW(!hasLocationVariables || !hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions with two types (location variables and abstracted variables) of variables are currently not supported by the abstraction expression translator."); + + if (hasLocationVariables) { + storm::dd::Add left = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + storm::dd::Add right = boost::any_cast>(expression.getFirstOperand()->accept(*this, boost::none)); + + switch (expression.getRelationType()) { + case BinaryRelationExpression::RelationType::Equal: return left.equals(right); + case BinaryRelationExpression::RelationType::NotEqual: return left.notEquals(right); + case BinaryRelationExpression::RelationType::Less: return left.less(right); + case BinaryRelationExpression::RelationType::LessOrEqual: return left.lessOrEqual(right); + case BinaryRelationExpression::RelationType::Greater: return left.greater(right); + case BinaryRelationExpression::RelationType::GreaterOrEqual: return left.greaterOrEqual(right); + } + } else { + for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) { + if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) { + return abstractionInformation.get().encodePredicateAsSource(predicateIndex); + } + } + + // At this point, none of the predicates was found to be equivalent, but there is no need to split as the subexpressions are not valid predicates. + + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } + } + + template + boost::any ExpressionTranslator::visit(VariableExpression const& expression, boost::any const& data) { + if (abstractedVariables.find(expression.getVariable()) != abstractedVariables.end()) { + for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) { + if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) { + return abstractionInformation.get().encodePredicateAsSource(predicateIndex); + } + } + + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } else { + return abstractionInformation.get().getDdManager().template getIdentity(expression.getVariable()); + } + } + + template + boost::any ExpressionTranslator::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + // Check whether the expression is either fully contained in the location variables fragment or the abstracted + // variables fragment. + std::set variablesInExpression; + expression.gatherVariables(variablesInExpression); + + std::set tmp; + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), locationVariables.begin(), locationVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasLocationVariables = !tmp.empty(); + + tmp.clear(); + std::set_intersection(variablesInExpression.begin(), variablesInExpression.end(), abstractedVariables.begin(), abstractedVariables.end(), std::inserter(tmp, tmp.begin())); + bool hasAbstractedVariables = !tmp.empty(); + + STORM_LOG_THROW(hasLocationVariables || hasAbstractedVariables, storm::exceptions::NotSupportedException, "Expressions without variables are currently not supported by the abstraction expression translator."); + + if (hasAbstractedVariables && !hasLocationVariables) { + for (uint64_t predicateIndex = 0; predicateIndex < abstractionInformation.get().getNumberOfPredicates(); ++predicateIndex) { + if (equivalenceChecker.areEquivalent(abstractionInformation.get().getPredicateByIndex(predicateIndex), expression.toExpression())) { + return abstractionInformation.get().encodePredicateAsSource(predicateIndex); + } + } + + // At this point, none of the predicates was found to be equivalent, so we split the expression. + } + + storm::dd::Bdd sub = boost::any_cast>(expression.getOperand()->accept(*this, boost::none)); + switch (expression.getOperatorType()) { + case UnaryBooleanFunctionExpression::OperatorType::Not: return !sub; + } + } + + template + boost::any ExpressionTranslator::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } + + template + boost::any ExpressionTranslator::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + if (expression.isTrue()) { + return abstractionInformation.get().getDdManager().getBddOne(); + } else { + return abstractionInformation.get().getDdManager().getBddZero(); + } + } + + template + boost::any ExpressionTranslator::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + return abstractionInformation.get().getDdManager().template getConstant(expression.getValue()); + } + + template + boost::any ExpressionTranslator::visit(RationalLiteralExpression const& expression, boost::any const& data) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); + } + + template class ExpressionTranslator; + template class ExpressionTranslator; + + } +} diff --git a/src/storm/abstraction/ExpressionTranslator.h b/src/storm/abstraction/ExpressionTranslator.h new file mode 100644 index 000000000..3516e5a34 --- /dev/null +++ b/src/storm/abstraction/ExpressionTranslator.h @@ -0,0 +1,53 @@ +#pragma once + +#include + +#include "storm/storage/dd/DdType.h" +#include "storm/storage/expressions/ExpressionVisitor.h" +#include "storm/storage/expressions/EquivalenceChecker.h" + +#include "storm/solver/SmtSolver.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace expressions { + class Expression; + } + + namespace abstraction { + + template + class AbstractionInformation; + + template + class ExpressionTranslator : public storm::expressions::ExpressionVisitor { + public: + ExpressionTranslator(AbstractionInformation& abstractionInformation, std::unique_ptr&& smtSolver); + + storm::dd::Bdd translate(storm::expressions::Expression const& expression); + + virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data); + + private: + std::reference_wrapper> abstractionInformation; + storm::expressions::EquivalenceChecker equivalenceChecker; + + std::set locationVariables; + std::set abstractedVariables; + }; + + } +} diff --git a/src/storm/abstraction/LocalExpressionInformation.cpp b/src/storm/abstraction/LocalExpressionInformation.cpp index d7002169c..6d6231a1e 100644 --- a/src/storm/abstraction/LocalExpressionInformation.cpp +++ b/src/storm/abstraction/LocalExpressionInformation.cpp @@ -10,7 +10,7 @@ namespace storm { namespace abstraction { template - LocalExpressionInformation::LocalExpressionInformation(AbstractionInformation const& abstractionInformation) : relevantVariables(abstractionInformation.getVariables()), expressionBlocks(relevantVariables.size()), abstractionInformation(abstractionInformation) { + LocalExpressionInformation::LocalExpressionInformation(AbstractionInformation const& abstractionInformation) : relevantVariables(abstractionInformation.getAbstractedVariables()), expressionBlocks(relevantVariables.size()), abstractionInformation(abstractionInformation) { // Assign each variable to a new block. uint_fast64_t currentBlock = 0; variableBlocks.resize(relevantVariables.size()); diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index ee5e383a4..cec5818b0 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -11,6 +11,11 @@ #include "storm/storage/expressions/Expression.h" namespace storm { + namespace dd { + template + class Bdd; + } + namespace abstraction { template @@ -29,6 +34,12 @@ namespace storm { virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0; virtual storm::expressions::Expression getInitialExpression() const = 0; + /*! + * Retrieves a BDD that characterizes the states corresponding to the given expression. For this to work, + * appropriate predicates must have been used to refine the abstraction, otherwise this will fail. + */ + virtual storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const = 0; + /// Methods to refine the abstraction. virtual void refine(RefinementCommand const& command) = 0; diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index 10c392cc5..986589294 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -14,7 +14,7 @@ namespace storm { namespace abstraction { template - StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::vector const& statePredicates, std::shared_ptr const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) { + StateSetAbstractor::StateSetAbstractor(AbstractionInformation& abstractionInformation, std::vector const& statePredicates, std::shared_ptr const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), relevantPredicatesAndVariables(), concretePredicateVariables(), forceRecomputation(true), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) { // Assert all state predicates. for (auto const& predicate : statePredicates) { @@ -46,7 +46,22 @@ namespace storm { for (auto const& predicateIndex : newPredicates) { localExpressionInformation.addExpression(predicateIndex); } - needsRecomputation = true; + + std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); + // Since the number of relevant predicates is monotonic, we can simply check for the size here. + STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); + if (newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size()) { + // 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(); + forceRecomputation = true; + } } template @@ -78,27 +93,6 @@ namespace storm { template void StateSetAbstractor::recomputeCachedBdd() { - // Now check whether we need to recompute the cached BDD. - std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); - - // Since the number of relevant predicates is monotonic, we can simply check for the size here. - STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); - bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); - - 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 = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -141,7 +135,7 @@ namespace storm { template storm::dd::Bdd StateSetAbstractor::getAbstractStates() { - if (needsRecomputation) { + if (forceRecomputation) { this->recomputeCachedBdd(); } return cachedBdd; diff --git a/src/storm/abstraction/StateSetAbstractor.h b/src/storm/abstraction/StateSetAbstractor.h index 9352f2d58..96861e8b1 100644 --- a/src/storm/abstraction/StateSetAbstractor.h +++ b/src/storm/abstraction/StateSetAbstractor.h @@ -146,7 +146,7 @@ namespace storm { std::vector decisionVariables; // A flag indicating whether the cached BDD needs recomputation. - bool needsRecomputation; + bool forceRecomputation; // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work // needed to be done). diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 4f4098d92..33731ddcc 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -2,7 +2,7 @@ #include "storm/abstraction/BottomStateResult.h" #include "storm/abstraction/GameBddResult.h" -#include "storm/abstraction/jani/JaniAbstractionInformation.h" +#include "storm/abstraction/AbstractionInformation.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -23,7 +23,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { + AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { // For each concrete command, we create an abstract counterpart. uint64_t edgeId = 0; @@ -31,6 +31,10 @@ namespace storm { edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition); ++edgeId; } + + if (automaton.getNumberOfLocations() > 1) { + locationVariables = abstractionInformation.addLocationVariables(automaton.getNumberOfLocations() - 1).first; + } } template @@ -87,7 +91,21 @@ namespace storm { storm::dd::Add AutomatonAbstractor::getEdgeDecoratorAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (auto const& edge : edges) { - result += edge.getEdgeDecoratorAdd(); + result += edge.getEdgeDecoratorAdd(locationVariables); + } + return result; + } + + template + storm::dd::Bdd AutomatonAbstractor::getInitialLocationsBdd() const { + if (automaton.get().getNumberOfLocations()) { + return this->getAbstractionInformation().getDdManager().getBddOne(); + } + + std::set const& initialLocationIndices = automaton.get().getInitialLocationIndices(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + for (auto const& initialLocationIndex : initialLocationIndices) { + result |= this->getAbstractionInformation().encodeLocation(locationVariables.get().first, initialLocationIndex); } return result; } @@ -108,7 +126,7 @@ namespace storm { } template - JaniAbstractionInformation const& AutomatonAbstractor::getAbstractionInformation() const { + AbstractionInformation const& AutomatonAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index e564d2dde..ac010a0d9 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -17,13 +17,13 @@ namespace storm { } namespace abstraction { + template + class AbstractionInformation; + template struct BottomStateResult; namespace jani { - template - class JaniAbstractionInformation; - template class AutomatonAbstractor { public: @@ -35,7 +35,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - AutomatonAbstractor(storm::jani::Automaton const& automaton, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); AutomatonAbstractor(AutomatonAbstractor const&) = default; AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; @@ -86,6 +86,11 @@ namespace storm { */ storm::dd::Add getEdgeDecoratorAdd() const; + /*! + * Retrieves a BDD that encodes all initial locations of this abstract automaton. + */ + storm::dd::Bdd getInitialLocationsBdd() const; + /*! * Retrieves the abstract edges of this abstract automton. * @@ -113,19 +118,22 @@ namespace storm { * * @return The abstraction information. */ - JaniAbstractionInformation const& getAbstractionInformation() const; + AbstractionInformation const& getAbstractionInformation() const; // A factory that can be used to create new SMT solvers. std::shared_ptr smtSolverFactory; // The DD-related information. - std::reference_wrapper const> abstractionInformation; + std::reference_wrapper const> abstractionInformation; // The abstract edge of the abstract automaton. std::vector> edges; // The concrete module this abstract automaton refers to. std::reference_wrapper automaton; + + // If the automaton has more than one location, we need variables to encode that. + boost::optional> locationVariables; }; } } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index ebaf89d58..51fef5753 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -5,7 +5,7 @@ #include #include "storm/abstraction/BottomStateResult.h" -#include "storm/abstraction/jani/JaniAbstractionInformation.h" +#include "storm/abstraction/AbstractionInformation.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace jani { template - EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { + EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations()); @@ -653,12 +653,22 @@ namespace storm { } template - storm::dd::Add EdgeAbstractor::getEdgeDecoratorAdd() const { + storm::dd::Add EdgeAbstractor::getEdgeDecoratorAdd(boost::optional> const& locationVariables) const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) { - result += this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())) * this->getAbstractionInformation().encodeLocation(edge.get().getDestination(destinationIndex).getLocationIndex(), false).template toAdd(); + result += this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability())); + if (locationVariables) { + result *= this->getAbstractionInformation().encodeLocation(locationVariables.get().second, edge.get().getDestination(destinationIndex).getLocationIndex()).template toAdd(); + } + } + + storm::dd::Add tmp = this->getAbstractionInformation().getDdManager().template getAddOne(); + if (locationVariables) { + tmp *= this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex()).template toAdd(); } - result *= this->getAbstractionInformation().encodeLocation(edge.get().getSourceLocationIndex(), true).template toAdd() * this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); + tmp *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); + + result *= tmp; return result; } @@ -668,12 +678,12 @@ namespace storm { } template - JaniAbstractionInformation const& EdgeAbstractor::getAbstractionInformation() const { + AbstractionInformation const& EdgeAbstractor::getAbstractionInformation() const { return abstractionInformation.get(); } template - JaniAbstractionInformation& EdgeAbstractor::getAbstractionInformation() { + AbstractionInformation& EdgeAbstractor::getAbstractionInformation() { return abstractionInformation.get(); } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 30c9b07a3..b0deaf1e9 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -39,13 +39,13 @@ namespace storm { } namespace abstraction { + template + class AbstractionInformation; + template class BottomStateResult; namespace jani { - template - class JaniAbstractionInformation; - template class EdgeAbstractor { public: @@ -58,7 +58,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction. */ - EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, JaniAbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); /*! * Refines the abstract edge with the given predicates. @@ -98,9 +98,11 @@ namespace storm { /*! * Retrieves an ADD that maps the encoding of the edge, source/target locations and its updates to their probabilities. * + * @param locationVariables If provided, the location variables are used to encode the source/destination locations of the edge + * and its destinations. * @return The decorator ADD. */ - storm::dd::Add getEdgeDecoratorAdd() const; + storm::dd::Add getEdgeDecoratorAdd(boost::optional> const& locationVariables) const; /*! * Retrieves the concrete edge that is abstracted by this abstract edge. @@ -194,14 +196,14 @@ namespace storm { * * @return The abstraction information object. */ - JaniAbstractionInformation const& getAbstractionInformation() const; + AbstractionInformation const& getAbstractionInformation() const; /*! * Retrieves the abstraction information object. * * @return The abstraction information object. */ - JaniAbstractionInformation& getAbstractionInformation(); + AbstractionInformation& getAbstractionInformation(); /*! * Computes the globally missing state identities. @@ -215,7 +217,7 @@ namespace storm { std::unique_ptr smtSolver; // The abstraction-related information. - std::reference_wrapper> abstractionInformation; + std::reference_wrapper> abstractionInformation; // The ID of the edge. uint64_t edgeId; diff --git a/src/storm/abstraction/jani/JaniAbstractionInformation.cpp b/src/storm/abstraction/jani/JaniAbstractionInformation.cpp deleted file mode 100644 index 53dcdf934..000000000 --- a/src/storm/abstraction/jani/JaniAbstractionInformation.cpp +++ /dev/null @@ -1,48 +0,0 @@ -#include "storm/abstraction/jani/JaniAbstractionInformation.h" - -#include "storm/storage/dd/DdManager.h" - -namespace storm { - namespace abstraction { - namespace jani { - - template - JaniAbstractionInformation::JaniAbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::set const& allVariables, uint64_t numberOfLocations, std::unique_ptr&& smtSolver, std::shared_ptr> ddManager) : AbstractionInformation(expressionManager, allVariables, std::move(smtSolver), ddManager) { - - // Create the location variable to have the appropriate dimension. - if (numberOfLocations > 1) { - locationVariables = ddManager->addMetaVariable("loc", 0, numberOfLocations - 1); - sourceLocationVariables.insert(locationVariables.get().first); - successorLocationVariables.insert(locationVariables.get().second); - } - } - - template - storm::dd::Bdd JaniAbstractionInformation::encodeLocation(uint64_t locationIndex, bool source) const { - if (locationVariables) { - if (source) { - return this->getDdManager().getEncoding(locationVariables.get().first, locationIndex); - } else { - return this->getDdManager().getEncoding(locationVariables.get().second, locationIndex); - } - } else { - return this->getDdManager().getBddOne(); - } - } - - template - std::set const& JaniAbstractionInformation::getSourceLocationVariables() const { - return sourceLocationVariables; - } - - template - std::set const& JaniAbstractionInformation::getSuccessorLocationVariables() const { - return successorLocationVariables; - } - - template class JaniAbstractionInformation; - template class JaniAbstractionInformation; - - } - } -} diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 8dc61ec87..e4a39ff8d 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -31,7 +31,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), model.getAutomaton(0).getNumberOfLocations(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) { // 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,7 +65,8 @@ namespace storm { automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition); } - // Retrieve the decorator ADD, so we can multiply it with the abstraction BDD later. + // Retrieve global BDDs/ADDs so we can multiply them in the abstraction process. + initialLocationsBdd = automata.front().getInitialLocationsBdd(); edgeDecoratorAdd = automata.front().getEdgeDecoratorAdd(); } @@ -127,7 +128,7 @@ namespace storm { } template - storm::dd::Bdd JaniMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) { + storm::dd::Bdd JaniMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) const { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); return abstractionInformation.getPredicateSourceVariable(predicate); } @@ -137,6 +138,9 @@ namespace storm { // As long as there is only one module, we only build its game representation. GameBddResult game = automata.front().abstract(); + // Add the locations to the transitions. + game.bdd &= edgeDecoratorAdd.notZero(); + // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); @@ -146,7 +150,7 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); - storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); + storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, @@ -162,7 +166,7 @@ namespace storm { // Compute bottom states and the appropriate transitions if necessary. BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); - bottomStateResult = automata.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + bottomStateResult = automata.front().getBottomStateTransitions(reachableStates.existsAbstract(abstractionInformation.getSourceLocationVariables()), game.numberOfPlayer2Variables); bool hasBottomStates = !bottomStateResult.states.isZero(); // Construct the transition matrix by cutting away the transitions of unreachable states. @@ -181,19 +185,15 @@ namespace storm { reachableStates |= bottomStateResult.states; } - std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); - - std::set allNondeterminismVariables = usedPlayer2Variables; + std::set allNondeterminismVariables = player2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); std::set allSourceVariables(abstractionInformation.getSourceVariables()); allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); - allSourceVariables.insert(abstractionInformation.getSourceLocationVariables().begin(), abstractionInformation.getSourceLocationVariables().end()); std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); - allSuccessorVariables.insert(abstractionInformation.getSuccessorLocationVariables().begin(), abstractionInformation.getSuccessorLocationVariables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), player2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 329da0fcd..335e61f60 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -6,7 +6,7 @@ #include "storm/abstraction/MenuGame.h" #include "storm/abstraction/RefinementCommand.h" #include "storm/abstraction/ValidBlockAbstractor.h" -#include "storm/abstraction/jani/JaniAbstractionInformation.h" +#include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/jani/AutomatonAbstractor.h" #include "storm/storage/dd/Add.h" @@ -98,7 +98,7 @@ namespace storm { * @param predicate The predicate for which to retrieve the states. * @return The BDD representing the set of states. */ - storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); + storm::dd::Bdd getStates(storm::expressions::Expression const& predicate) const override; /*! * Performs the given refinement command. @@ -139,7 +139,7 @@ namespace storm { std::shared_ptr smtSolverFactory; // An object containing all information about the abstraction like predicates and the corresponding DDs. - JaniAbstractionInformation abstractionInformation; + AbstractionInformation abstractionInformation; // The abstract modules of the abstract program. std::vector> automata; @@ -149,7 +149,10 @@ namespace storm { // An object that is used to compute the valid blocks. ValidBlockAbstractor validBlockAbstractor; - + + // A BDD characterizing the initial locations of the abstracted automata. + storm::dd::Bdd initialLocationsBdd; + // An ADD characterizing the probabilities and source/target locations of edges and their updates. storm::dd::Add edgeDecoratorAdd; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 89e3b6026..992f6fec8 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -129,9 +129,9 @@ namespace storm { } template - storm::dd::Bdd PrismMenuGameAbstractor::getStates(storm::expressions::Expression const& predicate) { + storm::dd::Bdd PrismMenuGameAbstractor::getStates(storm::expressions::Expression const& expression) const { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); - return abstractionInformation.getPredicateSourceVariable(predicate); + return abstractionInformation.getPredicateSourceVariable(expression); } template diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index e8f19eccc..cc4ad4e69 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -98,7 +98,7 @@ namespace storm { * @param predicate The predicate for which to retrieve the states. * @return The BDD representing the set of states. */ - storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); + storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; /*! * Performs the given refinement command. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 139438392..ee18dc9e0 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -407,7 +407,7 @@ namespace storm { auto quantitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStateValue << ", " << quantitativeResult.max.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); - + // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. result = checkForResultAfterQuantitativeCheck(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue, comparator); if (result) { diff --git a/src/storm/storage/expressions/BaseExpression.cpp b/src/storm/storage/expressions/BaseExpression.cpp index 8c84a7e29..761264074 100644 --- a/src/storm/storage/expressions/BaseExpression.cpp +++ b/src/storm/storage/expressions/BaseExpression.cpp @@ -12,6 +12,10 @@ namespace storm { // Intentionally left empty. } + Expression BaseExpression::toExpression() const { + return Expression(shared_from_this()); + } + Type const& BaseExpression::getType() const { return this->type; } diff --git a/src/storm/storage/expressions/BaseExpression.h b/src/storm/storage/expressions/BaseExpression.h index 8c38ca544..325aa33d4 100644 --- a/src/storm/storage/expressions/BaseExpression.h +++ b/src/storm/storage/expressions/BaseExpression.h @@ -16,6 +16,7 @@ namespace storm { // Forward-declare expression classes. class ExpressionManager; class Variable; + class Expression; class Valuation; class ExpressionVisitor; enum struct OperatorType; @@ -53,6 +54,11 @@ namespace storm { // Make the destructor virtual (to allow destruction via base class pointer) and default it. virtual ~BaseExpression() = default; + + /*! + * Converts the base expression to a proper expression. + */ + Expression toExpression() const; /*! * Evaluates the expression under the valuation of unknowns (variables and constants) given by the