diff --git a/src/abstraction/AbstractionDdInformation.cpp b/src/abstraction/AbstractionDdInformation.cpp deleted file mode 100644 index 1014117a0..000000000 --- a/src/abstraction/AbstractionDdInformation.cpp +++ /dev/null @@ -1,90 +0,0 @@ -#include "src/abstraction/AbstractionDdInformation.h" - -#include - -#include "src/storage/expressions/ExpressionManager.h" - -#include "src/storage/dd/DdManager.h" -#include "src/storage/dd/Bdd.h" -#include "src/storage/dd/Add.h" - -#include "src/utility/macros.h" - -namespace storm { - namespace abstraction { - - template - 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); - } - } - - template - storm::dd::Bdd AbstractionDdInformation::encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const { - storm::dd::Bdd result = manager->getBddOne(); - for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { - STORM_LOG_ASSERT(!(optionDdVariables[bitIndex].second.isZero() || optionDdVariables[bitIndex].second.isOne()), "Option variable is corrupted."); - if ((distributionIndex & 1) != 0) { - result &= optionDdVariables[bitIndex].second; - } else { - result &= !optionDdVariables[bitIndex].second; - } - distributionIndex >>= 1; - } - STORM_LOG_ASSERT(!result.isZero(), "Update BDD encoding must not be zero."); - return result; - } - - template - void AbstractionDdInformation::addPredicate(storm::expressions::Expression const& predicate) { - std::stringstream stream; - stream << predicate; - std::pair newMetaVariable = manager->addMetaVariable(stream.str()); - - predicateDdVariables.push_back(newMetaVariable); - predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1)); - predicateIdentities.push_back(manager->getEncoding(newMetaVariable.first, 1).iff(manager->getEncoding(newMetaVariable.second, 1))); - allPredicateIdentities &= predicateIdentities.back(); - sourceVariables.insert(newMetaVariable.first); - successorVariables.insert(newMetaVariable.second); - expressionToBddMap[predicate] = predicateBdds.back().first; - bddVariableIndexToPredicateMap[predicateIdentities.back().getIndex()] = predicate; - } - - template - storm::dd::Bdd AbstractionDdInformation::getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const { - storm::dd::Bdd result = manager->getBddOne(); - - for (uint_fast64_t index = begin; index < end; ++index) { - result &= optionDdVariables[index].second; - } - - STORM_LOG_ASSERT(!result.isZero(), "Update variable cube must not be zero."); - - return result; - } - - template - std::vector> AbstractionDdInformation::declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates) { - std::vector> result; - - auto oldIt = oldRelevantPredicates.begin(); - auto oldIte = oldRelevantPredicates.end(); - for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) { - // If the new variable does not yet exist as a source variable, we create it now. - if (oldIt == oldIte || oldIt->second != *newIt) { - result.push_back(std::make_pair(manager.declareFreshBooleanVariable(), *newIt)); - } else { - ++oldIt; - } - } - - return result; - } - - template struct AbstractionDdInformation; - template struct AbstractionDdInformation; - - } -} \ No newline at end of file diff --git a/src/abstraction/AbstractionDdInformation.h b/src/abstraction/AbstractionDdInformation.h deleted file mode 100644 index 0f9961bbd..000000000 --- a/src/abstraction/AbstractionDdInformation.h +++ /dev/null @@ -1,111 +0,0 @@ -#pragma once - -#include -#include -#include -#include -#include -#include - -#include "src/storage/dd/DdType.h" -#include "src/storage/expressions/Expression.h" -#include "src/storage/expressions/Variable.h" - -namespace storm { - namespace dd { - template - class DdManager; - - template - class Bdd; - } - - namespace abstraction { - - template - struct AbstractionDdInformation { - public: - /*! - * Creates a new DdInformation that uses the given manager. - * - * @param manager The manager to use. - * @param initialPredicates The initially considered predicates. - */ - AbstractionDdInformation(std::shared_ptr> const& manager, std::vector const& initialPredicates = std::vector()); - - /*! - * Encodes the given distribution index by using the given number of variables from the optionDdVariables - * vector. - * - * @param numberOfVariables The number of variables to use. - * @param distributionIndex The distribution index to encode. - * @return The encoded distribution index. - */ - storm::dd::Bdd encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const; - - /*! - * Adds the given predicate and creates all associated ressources. - * - * @param predicate The predicate to add. - */ - void addPredicate(storm::expressions::Expression const& predicate); - - /*! - * Retrieves the cube of option variables in the range [begin, end) the given indices. - * - * @param begin The first variable of the range to return. - * @param end One past the last variable of the range to return. - * @return The cube of variables in the given range. - */ - storm::dd::Bdd getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const; - - /*! - * Examines the old and new relevant predicates and declares decision variables for the missing relevant - * predicates. - * - * @param manager The manager in which to declare the decision variable. - * @param oldRelevantPredicates The previously relevant predicates. - * @param newRelevantPredicates The new relevant predicates. - * @return Pairs of decision variables and their index for the missing predicates. - */ - static std::vector> declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates); - - // The manager responsible for the DDs. - std::shared_ptr> manager; - - // The DD variables corresponding to the predicates. - std::vector> predicateDdVariables; - - // The set of all source variables. - std::set sourceVariables; - - // The set of all source variables. - std::set successorVariables; - - // The BDDs corresponding to the predicates. - std::vector, storm::dd::Bdd>> predicateBdds; - - // The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value). - std::vector> predicateIdentities; - - // A BDD that represents the identity of all predicate variables. - storm::dd::Bdd allPredicateIdentities; - - // The DD variable encoding the command (i.e., the nondeterministic choices of player 1). - storm::expressions::Variable commandDdVariable; - - // The DD variable encoding the update IDs for all actions. - storm::expressions::Variable updateDdVariable; - - // The DD variables encoding the nondeterministic choices of player 2. - std::vector>> optionDdVariables; - - // 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/abstraction/AbstractionExpressionInformation.cpp b/src/abstraction/AbstractionExpressionInformation.cpp deleted file mode 100644 index 8a0ddd6f9..000000000 --- a/src/abstraction/AbstractionExpressionInformation.cpp +++ /dev/null @@ -1,64 +0,0 @@ -#include "src/abstraction/AbstractionExpressionInformation.h" - -#include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/expressions/Expression.h" - -namespace storm { - namespace abstraction { - - AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector const& predicates, std::set const& variables, std::vector const& rangeExpressions) : manager(manager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) { - // 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); - } - } - - storm::expressions::ExpressionManager& AbstractionExpressionInformation::getManager() { - return manager; - } - - storm::expressions::ExpressionManager const& AbstractionExpressionInformation::getManager() const { - return manager; - } - - std::vector& AbstractionExpressionInformation::getPredicates() { - return predicates; - } - - std::vector const& AbstractionExpressionInformation::getPredicates() const { - return predicates; - } - - storm::expressions::Expression const& AbstractionExpressionInformation::getPredicateByIndex(uint_fast64_t index) const { - return predicates[index]; - } - - std::size_t AbstractionExpressionInformation::getNumberOfPredicates() const { - return predicates.size(); - } - - std::set& AbstractionExpressionInformation::getVariables() { - return variables; - } - - std::set const& AbstractionExpressionInformation::getVariables() const { - return variables; - } - - std::vector& AbstractionExpressionInformation::getRangeExpressions() { - return rangeExpressions; - } - - std::vector const& AbstractionExpressionInformation::getRangeExpressions() const { - return rangeExpressions; - } - - } -} diff --git a/src/abstraction/AbstractionExpressionInformation.h b/src/abstraction/AbstractionExpressionInformation.h deleted file mode 100644 index f26958b2f..000000000 --- a/src/abstraction/AbstractionExpressionInformation.h +++ /dev/null @@ -1,127 +0,0 @@ -#pragma once - -#include -#include -#include - -namespace storm { - namespace expressions { - class ExpressionManager; - class Expression; - class Variable; - } - - namespace abstraction { - - struct AbstractionExpressionInformation { - public: - /*! - * Creates an expression information object with the given expression manager. - * - * @param manager The expression manager to use. - * @param predicates The initial set of predicates. - * @param variables The variables. - * @param rangeExpressions A set of expressions that enforce the variable bounds. - */ - 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); - - /*! - * Retrieves the expression manager. - * - * @return The manager. - */ - storm::expressions::ExpressionManager& getManager(); - - /*! - * Retrieves the expression manager. - * - * @return The manager. - */ - storm::expressions::ExpressionManager const& getManager() const; - - /*! - * Retrieves all currently known predicates. - * - * @return The list of known predicates. - */ - std::vector& getPredicates(); - - /*! - * Retrieves all currently known predicates. - * - * @return The list of known predicates. - */ - std::vector const& getPredicates() const; - - /*! - * Retrieves the predicate with the given index. - * - * @param index The index of the predicate. - */ - storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const; - - /*! - * Retrieves the number of predicates. - * - * @return The number of predicates. - */ - std::size_t getNumberOfPredicates() const; - - /*! - * Retrieves all currently known variables. - * - * @return The set of known variables. - */ - std::set& getVariables(); - - /*! - * Retrieves all currently known variables. - * - * @return The set of known variables. - */ - std::set const& getVariables() const; - - /*! - * Retrieves a list of expressions that ensure the ranges of the variables. - * - * @return The range expressions. - */ - std::vector& getRangeExpressions(); - - /*! - * Retrieves a list of expressions that ensure the ranges of the variables. - * - * @return The range expressions. - */ - std::vector const& getRangeExpressions() const; - - private: - // The manager responsible for the expressions of the program and the SMT solvers. - storm::expressions::ExpressionManager& manager; - - // The current set of predicates used in the abstraction. - std::vector predicates; - - // The set of all variables. - std::set variables; - - // The expression characterizing the legal ranges of all variables. - std::vector rangeExpressions; - }; - - } -} diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 2a3aafe3a..6af114592 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -1,80 +1,321 @@ #include "src/abstraction/AbstractionInformation.h" +#include "src/storage/dd/DdManager.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace abstraction { - template - AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager) : expressionManager(expressionManager) { + template + AbstractionInformation::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr> ddManager) : expressionManager(expressionManager), ddManager(ddManager), allPredicateIdentities(ddManager->getBddOne()) { // Intentionally left empty. } - template - void AbstractionInformation::addVariable(storm::expressions::Variable const& variable) { + template + void AbstractionInformation::addExpressionVariable(storm::expressions::Variable const& variable) { variables.insert(variable); } - template - void AbstractionInformation::addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) { - addVariable(variable); + template + void AbstractionInformation::addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) { + addExpressionVariable(variable); addConstraint(constraint); } - template - void AbstractionInformation::addConstraint(storm::expressions::Expression const& constraint) { + template + std::set AbstractionInformation::getExpressionVariables() const { + return variables; + } + + template + void AbstractionInformation::addConstraint(storm::expressions::Expression const& constraint) { constraints.push_back(constraint); } - template - void AbstractionInformation::addPredicate(storm::expressions::Expression const& predicate) { + template + uint_fast64_t AbstractionInformation::addPredicate(storm::expressions::Expression const& predicate) { + std::size_t predicateIndex = predicates.size(); + predicateToIndexMap[predicate] = predicateIndex; + + // Add the new predicate to the list of known predicates. predicates.push_back(predicate); + + // Add DD variables for the new predicate. + std::stringstream stream; + stream << predicate; + std::pair newMetaVariable = ddManager->addMetaVariable(stream.str()); + + predicateDdVariables.push_back(newMetaVariable); + predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1)); + predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1))); + allPredicateIdentities &= predicateIdentities.back(); + sourceVariables.insert(newMetaVariable.first); + successorVariables.insert(newMetaVariable.second); + ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; + return predicateIndex; } - template - void AbstractionInformation::addPredicates(std::vector const& predicates) { + template + std::vector AbstractionInformation::addPredicates(std::vector const& predicates) { + std::vector predicateIndices; for (auto const& predicate : predicates) { - this->addPredicate(predicate); + predicateIndices.push_back(this->addPredicate(predicate)); } + return predicateIndices; + } + + template + std::vector const& AbstractionInformation::getConstraints() const { + return constraints; + } + + template + storm::expressions::ExpressionManager& AbstractionInformation::getExpressionManager() { + return expressionManager.get(); } - template - storm::expressions::ExpressionManager& AbstractionInformation::getExpressionManager() { - return expressionManager; + template + storm::expressions::ExpressionManager const& AbstractionInformation::getExpressionManager() const { + return expressionManager.get(); } - template - storm::expressions::ExpressionManager const& AbstractionInformation::getExpressionManager() const { - return expressionManager; + template + storm::dd::DdManager& AbstractionInformation::getDdManager() { + return *ddManager; } - template - std::vector const& AbstractionInformation::getPredicates() const { + template + storm::dd::DdManager const& AbstractionInformation::getDdManager() const { + return *ddManager; + } + + template + std::shared_ptr> AbstractionInformation::getDdManagerAsSharedPointer() { + return ddManager; + } + + template + std::shared_ptr const> AbstractionInformation::getDdManagerAsSharedPointer() const { + return ddManager; + } + + template + std::vector const& AbstractionInformation::getPredicates() const { return predicates; } - template - storm::expressions::Expression const& AbstractionInformation::getPredicateByIndex(uint_fast64_t index) const { + template + storm::expressions::Expression const& AbstractionInformation::getPredicateByIndex(uint_fast64_t index) const { return predicates[index]; } - template - std::size_t AbstractionInformation::getNumberOfPredicates() const { + template + storm::dd::Bdd AbstractionInformation::getPredicateSourceVariable(storm::expressions::Expression const& predicate) const { + auto indexIt = predicateToIndexMap.find(predicate); + STORM_LOG_THROW(indexIt != predicateToIndexMap.end(), storm::exceptions::InvalidOperationException, "Cannot retrieve BDD for unknown predicate."); + return predicateBdds[indexIt->second].first; + } + + template + std::size_t AbstractionInformation::getNumberOfPredicates() const { return predicates.size(); } - template - std::set const& AbstractionInformation::getVariables() const { + template + std::set const& AbstractionInformation::getVariables() const { return variables; } - template - std::vector const& AbstractionInformation::getConstraints() const { - return constraints; + template + void AbstractionInformation::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount) { + STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created."); + + for (uint64_t index = 0; index < player1VariableCount; ++index) { + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1_" + std::to_string(index)).first; + player1Variables.push_back(newVariable); + player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); + } + STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables."); + + for (uint64_t index = 0; index < player2VariableCount; ++index) { + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2_" + std::to_string(index)).first; + player2Variables.push_back(newVariable); + player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); + } + STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables."); + + for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) { + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb_" + std::to_string(index)).first; + probabilisticBranchingVariables.push_back(newVariable); + probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); + } + STORM_LOG_DEBUG("Created " << probabilisticBranchingVariableCount << " probabilistic branching variables."); + } + + template + storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { + return encodeChoice(index, numberOfVariables, player1VariableBdds); + } + + template + storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { + return encodeChoice(index, numberOfVariables, player2VariableBdds); + } + + template + storm::dd::Bdd AbstractionInformation::encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { + return encodeChoice(index, numberOfVariables, probabilisticBranchingVariableBdds); + } + + template + storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const { + storm::dd::Bdd result = ddManager->getBddOne(); + for (uint_fast64_t index = offset; index < numberOfVariables; ++index) { + result &= player2VariableBdds[index]; + } + STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); + return result; + } + + template + std::vector const& AbstractionInformation::getPlayer1Variables() const { + return player1Variables; + } + + template + std::set AbstractionInformation::getPlayer1VariableSet(uint_fast64_t count) const { + return std::set(player1Variables.begin(), player1Variables.begin() + count); + } + + template + std::vector const& AbstractionInformation::getPlayer2Variables() const { + return player2Variables; + } + + template + std::set AbstractionInformation::getPlayer2VariableSet(uint_fast64_t count) const { + return std::set(player2Variables.begin(), player2Variables.begin() + count); + } + + template + std::vector const& AbstractionInformation::getProbabilisticBranchingVariables() const { + return probabilisticBranchingVariables; + } + + template + std::set AbstractionInformation::getProbabilisticBranchingVariableSet(uint_fast64_t count) const { + return std::set(probabilisticBranchingVariables.begin(), probabilisticBranchingVariables.begin() + count); + } + + template + std::set const& AbstractionInformation::getSourceVariables() const { + return sourceVariables; + } + + template + std::set const& AbstractionInformation::getSuccessorVariables() const { + return successorVariables; + } + + template + storm::dd::Bdd const& AbstractionInformation::getAllPredicateIdentities() const { + return allPredicateIdentities; + } + + template + std::size_t AbstractionInformation::getPlayer1VariableCount() const { + return player1Variables.size(); + } + + template + std::size_t AbstractionInformation::getPlayer2VariableCount() const { + return player2Variables.size(); + } + + template + std::size_t AbstractionInformation::getProbabilisticBranchingVariableCount() const { + return probabilisticBranchingVariables.size(); + } + + template + std::map> AbstractionInformation::getPredicateToBddMap() const { + std::map> result; + + for (uint_fast64_t index = 0; index < predicates.size(); ++index) { + result[predicates[index]] = predicateBdds[index].first; + } + + return result; + } + + template + std::vector> const& AbstractionInformation::getSourceSuccessorVariablePairs() const { + return predicateDdVariables; + } + + template + storm::dd::Bdd const& AbstractionInformation::encodePredicateAsSource(uint_fast64_t predicateIndex) const { + return predicateBdds[predicateIndex].first; + } + + template + storm::dd::Bdd const& AbstractionInformation::encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const { + return predicateBdds[predicateIndex].second; + } + + template + storm::dd::Bdd const& AbstractionInformation::getPredicateIdentity(uint_fast64_t predicateIndex) const { + return predicateIdentities[predicateIndex]; + } + + template + storm::expressions::Expression const& AbstractionInformation::getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const { + auto indexIt = ddVariableIndexToPredicateIndexMap.find(ddVariableIndex); + STORM_LOG_THROW(indexIt != ddVariableIndexToPredicateIndexMap.end(), storm::exceptions::InvalidOperationException, "Unknown DD variable index."); + return predicates[indexIt->second]; + } + + template + std::vector> AbstractionInformation::declareNewVariables(std::vector> const& oldPredicates, std::set const& newPredicates) const { + std::vector> result; + + auto oldIt = oldPredicates.begin(); + auto oldIte = oldPredicates.end(); + auto newIt = newPredicates.begin(); + auto newIte = newPredicates.end(); + + for (; newIt != newIte; ++newIt) { + if (oldIt == oldIte || oldIt->second != *newIt) { + result.push_back(std::make_pair(expressionManager.get().declareFreshBooleanVariable(), *newIt)); + } else { + ++oldIt; + } + } + + return result; + } + + template + storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector> const& variables) const { + storm::dd::Bdd result = ddManager->getBddOne(); + for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { + if ((index & 1) != 0) { + result &= variables[bitIndex]; + } else { + result &= !variables[bitIndex]; + } + index >>= 1; + } + STORM_LOG_ASSERT(!result.isZero(), "BDD encoding must not be zero."); + return result; } - template class AbstractionInformation; - template class AbstractionInformation; + template class AbstractionInformation; + template class AbstractionInformation; } } diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index 3035853f1..ebad0817a 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -6,6 +6,8 @@ #include "src/storage/dd/DdType.h" +#include "src/storage/dd/Bdd.h" + namespace storm { namespace expressions { class ExpressionManager; @@ -13,9 +15,14 @@ namespace storm { class Variable; } + namespace dd { + template + class DdManager; + } + namespace abstraction { - template + template class AbstractionInformation { public: /*! @@ -23,22 +30,29 @@ namespace storm { * * @param expressionManager The manager responsible for all variables and expressions during the abstraction process. */ - AbstractionInformation(storm::expressions::ExpressionManager& expressionManager); + AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr> ddManager = std::make_shared>()); /*! * Adds the given variable. * * @param variable The variable to add. */ - void addVariable(storm::expressions::Variable const& variable); + 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. * * @param variable The variable to add. * @param constraint An expression characterizing the legal values of the variable. */ - void addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint); + void addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint); /*! * Adds an expression that constrains the legal variable values. @@ -47,19 +61,28 @@ namespace storm { */ void addConstraint(storm::expressions::Expression const& constraint); + /*! + * Retrieves a list of expressions that constrain the valid variable values. + * + * @return The constraint expressions. + */ + std::vector const& getConstraints() const; + /*! * Adds the given predicate. * * @param predicate The predicate to add. + * @return The index of the newly added predicate in the global list of predicates. */ - void addPredicate(storm::expressions::Expression const& predicate); + uint_fast64_t addPredicate(storm::expressions::Expression const& predicate); /*! * Adds the given predicates. * * @param predicates The predicates to add. + * @return A list of indices corresponding to the new predicates. */ - void addPredicates(std::vector const& predicates); + std::vector addPredicates(std::vector const& predicates); /*! * Retrieves the expression manager. @@ -75,6 +98,34 @@ namespace storm { */ storm::expressions::ExpressionManager const& getExpressionManager() const; + /*! + * Retrieves the DD manager. + * + * @return The manager. + */ + storm::dd::DdManager& getDdManager(); + + /*! + * Retrieves the DD manager. + * + * @return The manager. + */ + storm::dd::DdManager const& getDdManager() const; + + /*! + * Retrieves the shared pointer to the DD manager. + * + * @return The shared pointer to the DD manager. + */ + std::shared_ptr> getDdManagerAsSharedPointer(); + + /*! + * Retrieves the shared pointer to the DD manager. + * + * @return The shared pointer to the DD manager. + */ + std::shared_ptr const> getDdManagerAsSharedPointer() const; + /*! * Retrieves all currently known predicates. * @@ -89,6 +140,14 @@ namespace storm { */ storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const; + /*! + * Retrieves the source variable associated with the given predicate. Note that the given predicate must be + * known to this abstraction information. + * + * @param predicate The predicate for which to retrieve the source variable. + */ + storm::dd::Bdd getPredicateSourceVariable(storm::expressions::Expression const& predicate) const; + /*! * Retrieves the number of predicates. * @@ -104,17 +163,211 @@ namespace storm { std::set const& getVariables() const; /*! - * Retrieves a list of expressions that constrain the valid variable values. + * Creates the given number of variables used to encode the choices of player 1/2 and probabilistic branching. * - * @return The constraint expressions. + * @param player1VariableCount The number of variables to use for encoding player 1 choices. + * @param player2VariableCount The number of variables to use for encoding player 2 choices. + * @param probabilisticBranchingVariableCount The number of variables to use for encoding probabilistic branching. */ - std::vector const& getConstraints() const; + void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount); + + /*! + * Encodes the given index using the indicated player 1 variables. + * + * @param index The index to encode. + * @param numberOfVariables The number of variables to use for encoding the index. + * @return The index encoded as a BDD. + */ + storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + + /*! + * Encodes the given index using the indicated player 2 variables. + * + * @param index The index to encode. + * @param numberOfVariables The number of variables to use for encoding the index. + * @return The index encoded as a BDD. + */ + storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + + /*! + * Encodes the given index using the indicated probabilistic branching variables. + * + * @param index The index to encode. + * @param numberOfVariables The number of variables to use for encoding the index. + * @return The index encoded as a BDD. + */ + storm::dd::Bdd encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + + /*! + * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). + * + * @param numberOfVariables The number of variables to use in total. The number of variables in the returned + * cube is the number of variables minus the offset. + * @param offset The first variable of the range to return. + * @return The cube of variables starting from the offset until the given number of variables is reached. + */ + storm::dd::Bdd getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const; + + /*! + * Retrieves the meta variables associated with the player 1 choices. + * + * @return The meta variables associated with the player 1 choices. + */ + std::vector const& getPlayer1Variables() const; + + /*! + * Retrieves the set of player 1 variables. + * + * @param count The number of player 1 variables to include. + * @return The set of player 1 variables. + */ + std::set getPlayer1VariableSet(uint_fast64_t count) const; + + /*! + * Retrieves the number of player 1 variables. + * + * @return The number of player 1 variables. + */ + std::size_t getPlayer1VariableCount() const; + + /*! + * Retrieves the meta variables associated with the player 2 choices. + * + * @return The meta variables associated with the player 2 choices. + */ + std::vector const& getPlayer2Variables() const; + + /*! + * Retrieves the number of player 2 variables. + * + * @return The number of player 2 variables. + */ + std::size_t getPlayer2VariableCount() const; + + /*! + * Retrieves the set of player 2 variables. + * + * @param count The number of player 2 variables to include. + * @return The set of player 2 variables. + */ + std::set getPlayer2VariableSet(uint_fast64_t count) const; + + /*! + * Retrieves the meta variables associated with the probabilistic branching. + * + * @return The meta variables associated with the probabilistic branching. + */ + std::vector const& getProbabilisticBranchingVariables() const; + + /*! + * Retrieves the set of probabilistic branching variables. + * + * @param count The number of probabilistic branching variables to include. + * @return The set of probabilistic branching variables. + */ + std::set getProbabilisticBranchingVariableSet(uint_fast64_t count) const; + + /*! + * Retrieves the number of probabilistic branching variables. + * + * @return The number of probabilistic branching variables. + */ + std::size_t getProbabilisticBranchingVariableCount() const; + + /*! + * Retrieves the set of source meta variables. + * + * @return All source meta variables. + */ + std::set const& getSourceVariables() const; + + /*! + * Retrieves the set of successor meta variables. + * + * @return All successor meta variables. + */ + std::set const& getSuccessorVariables() const; + + /*! + * Retrieves a BDD representing the identities of all predicates. + * + * @return All predicate identities. + */ + storm::dd::Bdd const& getAllPredicateIdentities() const; + + /*! + * Retrieves a mapping of the known predicates to the BDDs that represent the corresponding states. + * + * @return A mapping from predicates to their representing BDDs. + */ + std::map> getPredicateToBddMap() const; + + /*! + * Retrieves the meta variables pairs for all predicates. + * + * @return The meta variable pairs for all predicates. + */ + std::vector> const& getSourceSuccessorVariablePairs() const; + + /*! + * Retrieves the BDD for the predicate with the given index over the source variables. + * + * @param predicateIndex The index of the predicate. + * @return The encoding the predicate over the source variables. + */ + storm::dd::Bdd const& encodePredicateAsSource(uint_fast64_t predicateIndex) const; + + /*! + * Retrieves the BDD for the predicate with the given index over the successor variables. + * + * @param predicateIndex The index of the predicate. + * @return The encoding the predicate over the successor variables. + */ + storm::dd::Bdd const& encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const; + + /*! + * Retrieves a BDD representing the identity for the predicate with the given index. + * + * @param predicateIndex The index of the predicate. + * @return The identity for the predicate. + */ + storm::dd::Bdd const& getPredicateIdentity(uint_fast64_t predicateIndex) const; + + /*! + * Retrieves the predicate associated with the given DD variable index. + * + * @param ddVariableIndex The DD variable index for which to retrieve the predicate. + * @return The predicate associated with the given DD variable index. + */ + storm::expressions::Expression const& getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const; + + /*! + * Declares new variables for the missing predicates. + * + * @param oldPredicates The old predicates. + * @param newPredicates The new predicates. + * @return A list of the missing variables together with the predicate index they represent. + */ + std::vector> declareNewVariables(std::vector> const& oldPredicates, std::set const& newPredicates) const; private: + /*! + * Encodes the given index with the given number of variables from the given variables. + * + * @param index The index to encode. + * @param numberOfVariables The total number of variables to use. + * @param variables The BDDs of the variables to use to encode the index. + */ + storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector> const& variables) const; + // The expression related data. /// The manager responsible for the expressions of the program and the SMT solvers. - storm::expressions::ExpressionManager& expressionManager; + std::reference_wrapper expressionManager; + + /// A mapping from predicates to their indices in the predicate list. + // FIXME: Does this properly store the expressions? What about equality checking? + std::unordered_map predicateToIndexMap; /// The current set of predicates used in the abstraction. std::vector predicates; @@ -124,6 +377,50 @@ namespace storm { /// The expressions characterizing legal variable values. std::vector constraints; + + // The DD-related data. + + /// The manager responsible for the DDs. + std::shared_ptr> ddManager; + + /// The DD variables corresponding to the predicates. + std::vector> predicateDdVariables; + + /// The set of all source variables. + std::set sourceVariables; + + /// The set of all source variables. + std::set successorVariables; + + /// The BDDs corresponding to the predicates. + std::vector, storm::dd::Bdd>> predicateBdds; + + /// The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value). + std::vector> predicateIdentities; + + /// A BDD that represents the identity of all predicate variables. + storm::dd::Bdd allPredicateIdentities; + + /// A mapping from DD variable indices to the predicate index they represent. + std::unordered_map ddVariableIndexToPredicateIndexMap; + + /// Variables that encode the choices of player 1. + std::vector player1Variables; + + /// The BDDs associated with the meta variables of player 1. + std::vector> player1VariableBdds; + + /// Variables that encode the choices of player 2. + std::vector player2Variables; + + /// The BDDs associated with the meta variables of player 2. + std::vector> player2VariableBdds; + + /// Variables that can be used to encode the probabilistic branching. + std::vector probabilisticBranchingVariables; + + /// The BDDs associated with the meta variables encoding the probabilistic branching. + std::vector> probabilisticBranchingVariableBdds; }; } diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index d9ad05124..6e4420aa9 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -24,8 +24,8 @@ namespace storm { std::set const& player1Variables, std::set const& player2Variables, std::set const& allNondeterminismVariables, - storm::expressions::Variable const& updateVariable, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { + std::set const& probabilisticBranchingVariables, + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } diff --git a/src/abstraction/MenuGame.h b/src/abstraction/MenuGame.h index 2d1be6b44..3b192881b 100644 --- a/src/abstraction/MenuGame.h +++ b/src/abstraction/MenuGame.h @@ -37,7 +37,7 @@ namespace storm { * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1. * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2. * @param allNondeterminismVariables The meta variables used to encode the nondeterminism in the model. - * @param updateVariable The variable used to encode the different updates of the probabilistic program. + * @param probabilisticBranchingVariables The variables used to encode probabilistic branching. * @param expressionToBddMap A mapping from expressions (used) in the abstraction to the BDDs encoding * them. */ @@ -53,7 +53,7 @@ namespace storm { std::set const& player1Variables, std::set const& player2Variables, std::set const& allNondeterminismVariables, - storm::expressions::Variable const& updateVariable, + std::set const& probabilisticBranchingVariables, std::map> const& expressionToBddMap); virtual storm::dd::Bdd getStates(std::string const& label) const override; @@ -87,8 +87,8 @@ namespace storm { virtual bool hasLabel(std::string const& label) const override; private: - // The meta variable used to encode the updates. - storm::expressions::Variable updateVariable; + // The meta variables used to probabilistic branching. + std::set probabilisticBranchingVariables; // A mapping from expressions that were used in the abstraction process to the the BDDs representing them. std::map> expressionToBddMap; diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 1aad4651d..e3d6b6949 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -1,7 +1,6 @@ #include "src/abstraction/StateSetAbstractor.h" -#include "src/abstraction/AbstractionExpressionInformation.h" -#include "src/abstraction/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionInformation.h" #include "src/storage/dd/DdManager.h" @@ -12,12 +11,7 @@ namespace storm { namespace abstraction { template - StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), localExpressionInformation(globalExpressionInformation.getVariables()), 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 : globalExpressionInformation.getRangeExpressions()) { - smtSolver->add(rangeExpression); - } + 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()) { // Assert all state predicates. for (auto const& predicate : statePredicates) { @@ -28,21 +22,14 @@ namespace storm { concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end()); localExpressionInformation.relate(usedVariables); } - - // Refine the command based on all initial predicates. - std::vector allPredicateIndices(globalExpressionInformation.getPredicates().size()); - for (auto index = 0; index < globalExpressionInformation.getPredicates().size(); ++index) { - allPredicateIndices[index] = index; - } - this->refine(allPredicateIndices); } template void StateSetAbstractor::addMissingPredicates(std::set const& newRelevantPredicateIndices) { - std::vector> newPredicateVariables = AbstractionDdInformation::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices); + std::vector> newPredicateVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables, newRelevantPredicateIndices); for (auto const& element : newPredicateVariables) { - smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicates()[element.second])); + smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second))); decisionVariables.push_back(element.first); } @@ -54,11 +41,16 @@ namespace storm { 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) { - localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex); + localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex); } needsRecomputation = true; } + template + void StateSetAbstractor::constrain(storm::expressions::Expression const& constraint) { + smtSolver->add(constraint); + } + template void StateSetAbstractor::constrain(storm::dd::Bdd const& newConstraint) { // If the constraint is different from the last one, we add it to the solver. @@ -71,12 +63,12 @@ namespace storm { template storm::dd::Bdd StateSetAbstractor::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { STORM_LOG_TRACE("Building source state BDD."); - storm::dd::Bdd result = ddInformation.manager->getBddOne(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables) { if (model.getBooleanValue(variableIndexPair.first)) { - result &= ddInformation.predicateBdds[variableIndexPair.second].first; + result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { - result &= !ddInformation.predicateBdds[variableIndexPair.second].first; + result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } } return result; @@ -108,9 +100,9 @@ namespace storm { STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); - storm::dd::Bdd result = ddInformation.manager->getBddZero(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); uint_fast64_t modelCounter = 0; - smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); + smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; return true; } ); cachedBdd = result; } @@ -134,7 +126,7 @@ namespace storm { smtSolver->push(); // Create the constraint. - std::pair, std::unordered_map> result = constraint.toExpression(globalExpressionInformation.getManager()); + std::pair, std::unordered_map> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager()); // Then add the constraint. for (auto const& expression : result.first) { @@ -143,9 +135,7 @@ namespace storm { // Finally associate the level variables with the predicates. for (auto const& indexVariablePair : result.second) { - auto predicateIt = ddInformation.bddVariableIndexToPredicateMap.find(indexVariablePair.first); - STORM_LOG_ASSERT(predicateIt != ddInformation.bddVariableIndexToPredicateMap.end(), "Missing predicate for DD variable."); - smtSolver->add(storm::expressions::iff(indexVariablePair.second, predicateIt->second)); + smtSolver->add(storm::expressions::iff(indexVariablePair.second, this->getAbstractionInformation().getPredicateForDdVariableIndex(indexVariablePair.first))); } } @@ -157,6 +147,16 @@ namespace storm { return cachedBdd; } + template + AbstractionInformation& StateSetAbstractor::getAbstractionInformation() { + return abstractionInformation.get(); + } + + template + AbstractionInformation const& StateSetAbstractor::getAbstractionInformation() const { + return abstractionInformation.get(); + } + template class StateSetAbstractor; template class StateSetAbstractor; } diff --git a/src/abstraction/StateSetAbstractor.h b/src/abstraction/StateSetAbstractor.h index bcacc70fa..dad33e664 100644 --- a/src/abstraction/StateSetAbstractor.h +++ b/src/abstraction/StateSetAbstractor.h @@ -28,17 +28,12 @@ namespace storm { } namespace abstraction { - template - class AbstractionDdInformation; - - class AbstractionExpressionInformation; + template + class AbstractionInformation; template class StateSetAbstractor { public: - // Provide a no-op default constructor. - StateSetAbstractor() = default; - StateSetAbstractor(StateSetAbstractor const& other) = default; StateSetAbstractor& operator=(StateSetAbstractor const& other) = default; @@ -50,13 +45,13 @@ namespace storm { /*! * Creates a state set abstractor. * - * @param expressionInformation The expression-related information including the manager and the predicates. - * @param ddInformation The DD-related information including the manager. + * @param abstractionInformation An object storing information about the abstraction such as predicates and BDDs. + * @param allVariables All variables that appear in the predicates. * @param statePredicates A set of predicates that have to hold in the concrete states this abstractor is * supposed to abstract. * @param smtSolverFactory A factory that can create new SMT solvers. */ - StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + StateSetAbstractor(AbstractionInformation& abstractionInformation, std::set const& allVariables, std::vector const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstractor by making the given predicates new abstract predicates. @@ -65,6 +60,14 @@ namespace storm { */ void refine(std::vector const& newPredicateIndices); + /*! + * Constrains the abstract states with the given expression. + * Note that all constaints must be added before the abstractor is used to retrieve the abstract states. + * + * @param constraint The constraint to add. + */ + void constrain(storm::expressions::Expression const& constraint); + /*! * Constraints the abstract states with the given BDD. * @@ -110,14 +113,25 @@ namespace storm { */ storm::dd::Bdd getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; + /*! + * Retrieves the abstraction information. + * + * @return The abstraction information. + */ + AbstractionInformation& getAbstractionInformation(); + + /*! + * Retrieves the abstraction information. + * + * @return The abstraction information. + */ + AbstractionInformation const& getAbstractionInformation() const; + // The SMT solver used for abstracting the set of states. std::unique_ptr smtSolver; - // The global expression-related information. - AbstractionExpressionInformation& globalExpressionInformation; - - // The DD-related information. - AbstractionDdInformation const& ddInformation; + // The abstraction-related information. + std::reference_wrapper> abstractionInformation; // The local expression-related information. LocalExpressionInformation localExpressionInformation; diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index e39bfd911..ca6a3a141 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -2,8 +2,7 @@ #include -#include "src/abstraction/AbstractionExpressionInformation.h" -#include "src/abstraction/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionInformation.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -11,8 +10,6 @@ #include "src/storage/prism/Command.h" #include "src/storage/prism/Update.h" -#include "src/storage/expressions/ExpressionEvaluator.h" - #include "src/utility/solver.h" #include "src/utility/macros.h" @@ -20,32 +17,32 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), command(command), localExpressionInformation(globalExpressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(abstractionInformation.getDdManager().getBddZero(), 0)), decisionVariables() { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); - // Assert all range expressions to enforce legal variable values. - for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) { - smtSolver->add(rangeExpression); + // Assert all constraints to enforce legal variable values. + for (auto const& constraint : abstractionInformation.getConstraints()) { + smtSolver->add(constraint); } // Assert the guard of the command. smtSolver->add(command.getGuardExpression()); // Refine the command based on all initial predicates. - std::vector allPredicateIndices(globalExpressionInformation.getNumberOfPredicates()); - for (auto index = 0; index < globalExpressionInformation.getNumberOfPredicates(); ++index) { + std::vector allPredicateIndices(abstractionInformation.getNumberOfPredicates()); + for (auto index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); } - + template void AbstractCommand::refine(std::vector const& predicates) { // Add all predicates to the variable partition. for (auto predicateIndex : predicates) { - localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex); + localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex); } STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation); @@ -89,15 +86,15 @@ namespace storm { uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices))); // Finally, build overall result. - storm::dd::Bdd resultBdd = ddInformation.manager->getBddZero(); + storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); - storm::dd::Bdd allDistributions = ddInformation.manager->getBddZero(); + storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); uint_fast64_t distributionIndex = 0; for (auto const& distribution : sourceDistributionsPair.second) { - allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex); + allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded); ++distributionIndex; STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); } @@ -107,7 +104,7 @@ namespace storm { } resultBdd &= computeMissingIdentities(); - resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()); + resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); // Cache the result. @@ -175,9 +172,9 @@ namespace storm { template void AbstractCommand::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { // Determine and add new relevant source predicates. - std::vector> newSourceVariables = AbstractionDdInformation::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first); + std::vector> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { - smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second))); + smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second))); decisionVariables.push_back(element.first); } @@ -187,9 +184,9 @@ namespace storm { // Do the same for every update. for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { - std::vector> newSuccessorVariables = AbstractionDdInformation::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + std::vector> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); for (auto const& element : newSuccessorVariables) { - smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); + smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); decisionVariables.push_back(element.first); } @@ -201,12 +198,12 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { STORM_LOG_TRACE("Building source state BDD."); - storm::dd::Bdd result = ddInformation.manager->getBddOne(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { if (model.getBooleanValue(variableIndexPair.first)) { - result &= ddInformation.predicateBdds[variableIndexPair.second].first; + result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { - result &= !ddInformation.predicateBdds[variableIndexPair.second].first; + result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } } @@ -217,19 +214,19 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { STORM_LOG_TRACE("Building distribution BDD."); - storm::dd::Bdd result = ddInformation.manager->getBddZero(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - storm::dd::Bdd updateBdd = ddInformation.manager->getBddOne(); + storm::dd::Bdd updateBdd = this->getAbstractionInformation().getDdManager().getBddOne(); // Translate block variables for this update into a successor block. for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) { if (model.getBooleanValue(variableIndexPair.first)) { - updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second; + updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } else { - updateBdd &= !ddInformation.predicateBdds[variableIndexPair.second].second; + updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex); + updateBdd &= this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()); } result |= updateBdd; @@ -248,7 +245,7 @@ namespace storm { template storm::dd::Bdd AbstractCommand::computeMissingUpdateIdentities() const { - storm::dd::Bdd result = ddInformation.manager->getBddZero(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { // Compute the identities that are missing for this update. auto firstIt = relevantPredicatesAndVariables.first.begin(); @@ -258,17 +255,17 @@ namespace storm { // Go through all relevant source predicates. This is guaranteed to be a superset of the set of // relevant successor predicates for any update. - storm::dd::Bdd updateIdentity = ddInformation.manager->getBddOne(); + storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); for (; firstIt != firstIte; ++firstIt) { // If the predicates do not match, there is a predicate missing, so we need to add its identity. if (secondIt == secondIte || firstIt->second != secondIt->second) { - updateIdentity &= ddInformation.predicateIdentities[firstIt->second]; + updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(firstIt->second); } else if (secondIt != secondIte) { ++secondIt; } } - result |= updateIdentity && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex); + result |= updateIdentity && this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()); } return result; } @@ -278,10 +275,10 @@ namespace storm { auto relevantIt = relevantPredicatesAndVariables.first.begin(); auto relevantIte = relevantPredicatesAndVariables.first.end(); - storm::dd::Bdd result = ddInformation.manager->getBddOne(); - for (uint_fast64_t predicateIndex = 0; predicateIndex < globalExpressionInformation.getNumberOfPredicates(); ++predicateIndex) { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); + for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { - result &= ddInformation.predicateIdentities[predicateIndex]; + result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); } else { ++relevantIt; } @@ -296,15 +293,24 @@ namespace storm { template storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { - storm::expressions::ExpressionEvaluator evaluator(globalExpressionInformation.getManager()); - storm::dd::Add result = ddInformation.manager->template getAddZero(); + storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex).template toAdd() * ddInformation.manager->getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } - result *= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()).template toAdd(); + result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; } + template + AbstractionInformation const& AbstractCommand::getAbstractionInformation() const { + return abstractionInformation.get(); + } + + template + AbstractionInformation& AbstractCommand::getAbstractionInformation() { + return abstractionInformation.get(); + } + template class AbstractCommand; template class AbstractCommand; } diff --git a/src/abstraction/prism/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index 9e5d44c24..97f4d464c 100644 --- a/src/abstraction/prism/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -7,6 +7,8 @@ #include "src/abstraction/LocalExpressionInformation.h" +#include "src/storage/expressions/ExpressionEvaluator.h" + #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Expression.h" @@ -34,11 +36,9 @@ namespace storm { } namespace abstraction { - template - struct AbstractionDdInformation; + template + class AbstractionInformation; - struct AbstractionExpressionInformation; - namespace prism { template class AbstractCommand { @@ -47,11 +47,10 @@ namespace storm { * Constructs an abstract command from the given command and the initial predicates. * * @param command The concrete command for which to build the abstraction. - * @param expressionInformation The expression-related information including the manager and the predicates. - * @param ddInformation The DD-related information including the manager. + * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); /*! * Refines the abstract command with the given predicates. @@ -145,6 +144,20 @@ namespace storm { */ storm::dd::Bdd computeMissingUpdateIdentities() const; + /*! + * Retrieves the abstraction information object. + * + * @return The abstraction information object. + */ + AbstractionInformation const& getAbstractionInformation() const; + + /*! + * Retrieves the abstraction information object. + * + * @return The abstraction information object. + */ + AbstractionInformation& getAbstractionInformation(); + /*! * Computes the globally missing state identities. * @@ -156,11 +169,8 @@ namespace storm { // An SMT responsible for this abstract command. std::unique_ptr smtSolver; - // The global expression-related information. - AbstractionExpressionInformation& globalExpressionInformation; - - // The DD-related information. - AbstractionDdInformation const& ddInformation; + // The abstraction-related information. + std::reference_wrapper> abstractionInformation; // The concrete command this abstract command refers to. std::reference_wrapper command; @@ -168,6 +178,9 @@ namespace storm { // The local expression-related information. LocalExpressionInformation localExpressionInformation; + // The evaluator used to translate the probability expressions. + storm::expressions::ExpressionEvaluator evaluator; + // The currently relevant source/successor predicates and the corresponding variables. std::pair>, std::vector>>> relevantPredicatesAndVariables; diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 069bbf0ef..3adcc9860 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -1,7 +1,6 @@ #include "src/abstraction/prism/AbstractModule.h" -#include "src/abstraction/AbstractionExpressionInformation.h" -#include "src/abstraction/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionInformation.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -13,11 +12,11 @@ namespace storm { namespace prism { template - AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) { + AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(command, expressionInformation, ddInformation, smtSolverFactory); + commands.emplace_back(command, abstractionInformation, smtSolverFactory); } } @@ -40,22 +39,27 @@ namespace storm { // Then, we build the module BDD by adding the single command DDs. We need to make sure that all command // DDs use the same amount DD variable encoding the choices of player 2. - storm::dd::Bdd result = ddInformation.manager->getBddZero(); + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { - result |= commandDd.first && ddInformation.getMissingOptionVariableCube(commandDd.second, maximalNumberOfUsedOptionVariables); + result |= commandDd.first && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.second); } return std::make_pair(result, maximalNumberOfUsedOptionVariables); } template storm::dd::Add AbstractModule::getCommandUpdateProbabilitiesAdd() const { - storm::dd::Add result = ddInformation.manager->template getAddZero(); + storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (auto const& command : commands) { result += command.getCommandUpdateProbabilitiesAdd(); } return result; } + template + AbstractionInformation const& AbstractModule::getAbstractionInformation() const { + return abstractionInformation.get(); + } + template class AbstractModule; template class AbstractModule; } diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 721b2c3f3..28428e2f1 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -15,11 +15,9 @@ namespace storm { } namespace abstraction { - template - struct AbstractionDdInformation; + template + class AbstractionInformation; - struct AbstractionExpressionInformation; - namespace prism { template class AbstractModule { @@ -28,11 +26,15 @@ namespace storm { * Constructs an abstract module from the given module and the initial predicates. * * @param module The concrete module for which to build the abstraction. - * @param expressionInformation The expression-related information including the manager and the predicates. - * @param ddInformation The DD-related information including the manager. + * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. */ - AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + + AbstractModule(AbstractModule const&) = default; + AbstractModule& operator=(AbstractModule const&) = default; + AbstractModule(AbstractModule&&) = default; + AbstractModule& operator=(AbstractModule&&) = default; /*! * Refines the abstract module with the given predicates. @@ -56,11 +58,18 @@ namespace storm { storm::dd::Add getCommandUpdateProbabilitiesAdd() const; private: + /*! + * Retrieves the abstraction information. + * + * @return The abstraction information. + */ + AbstractionInformation const& getAbstractionInformation() const; + // A factory that can be used to create new SMT solvers. storm::utility::solver::SmtSolverFactory const& smtSolverFactory; // The DD-related information. - AbstractionDdInformation const& ddInformation; + std::reference_wrapper const> abstractionInformation; // The abstract commands of the abstract module. std::vector> commands; diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 1e7d63b73..1eeeef9ad 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -17,12 +17,26 @@ namespace storm { namespace prism { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *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) + : 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) { // 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. STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules."); + // Add all variables and range expressions to the information object. + for (auto const& variable : this->program.get().getAllExpressionVariables()) { + abstractionInformation.addExpressionVariable(variable); + } + for (auto const& range : this->program.get().getAllRangeExpressions()) { + abstractionInformation.addConstraint(range); + initialStateAbstractor.constrain(range); + bottomStateAbstractor.constrain(range); + } + uint_fast64_t totalNumberOfCommands = 0; uint_fast64_t maximalUpdateCount = 0; std::vector allGuards; @@ -30,7 +44,6 @@ namespace storm { // If we were requested to add all guards to the set of predicates, we do so now. for (auto const& command : module.getCommands()) { if (addAllGuards) { - expressionInformation.getPredicates().push_back(command.getGuardExpression()); allGuards.push_back(command.getGuardExpression()); } maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); @@ -39,36 +52,31 @@ namespace storm { totalNumberOfCommands += module.getNumberOfCommands(); } - // Create DD variable for the command encoding. - ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; - - // Create DD variable for update encoding. - ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first; - - // Create DD variables encoding the nondeterministic choices of player 2. - // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices. - // If for some reason this should not be enough, we could grow this vector dynamically, but odds are - // that it's impossible to treat such models in any event. - for (uint_fast64_t index = 0; index < 100; ++index) { - storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first; - ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getEncoding(newOptionVar, 1))); - } + // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible + // choices. If for some reason this should not be enough, we could grow this vector dynamically, but + // odds are that it's impossible to treat such models in any event. + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // Now that we have created all other DD variables, we create the DD variables for the predicates. + std::vector allPredicateIndices; if (addAllGuards) { for (auto const& guard : allGuards) { - ddInformation.addPredicate(guard); + allPredicateIndices.push_back(abstractionInformation.addPredicate(guard)); } } for (auto const& predicate : initialPredicates) { - ddInformation.addPredicate(predicate); + allPredicateIndices.push_back(abstractionInformation.addPredicate(predicate)); } // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory); + this->modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory); } + // Refine the state abstractors using the initial predicates. + initialStateAbstractor.refine(allPredicateIndices); + bottomStateAbstractor.refine(allPredicateIndices); + // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); @@ -81,19 +89,11 @@ namespace storm { STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates."); // Add the predicates to the global list of predicates. - uint_fast64_t firstNewPredicateIndex = expressionInformation.getPredicates().size(); - expressionInformation.addPredicates(predicates); - - // Create DD variables and some auxiliary data structures for the new predicates. + std::vector newPredicateIndices; for (auto const& predicate : predicates) { STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); - ddInformation.addPredicate(predicate); - } - - // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors. - std::vector newPredicateIndices; - for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.getPredicates().size(); ++index) { - newPredicateIndices.push_back(index); + uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate); + newPredicateIndices.push_back(newPredicateIndex); } // Refine all abstract modules. @@ -107,7 +107,7 @@ namespace storm { // Refine bottom state abstractor. bottomStateAbstractor.refine(newPredicateIndices); - // Finally, we rebuild the game.. + // Finally, we rebuild the game. currentGame = buildGame(); } @@ -120,14 +120,7 @@ namespace storm { template storm::dd::Bdd AbstractProgram::getStates(storm::expressions::Expression const& predicate) { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); - uint_fast64_t index = 0; - for (auto const& knownPredicate : expressionInformation.getPredicates()) { - if (knownPredicate.areSame(predicate)) { - return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first; - } - ++index; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given predicate is illegal, since it was neither used as an initial predicate nor used to refine the abstraction."); + return abstractionInformation.getPredicateSourceVariable(predicate); } template @@ -136,47 +129,45 @@ namespace storm { std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); // Construct a set of all unnecessary variables, so we can abstract from it. - std::set variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable}; - for (uint_fast64_t index = 0; index < gameBdd.second; ++index) { - variablesToAbstract.insert(ddInformation.optionDdVariables[index].first); - } + std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + auto player2Variables = abstractionInformation.getPlayer2VariableSet(gameBdd.second); + variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); + auto probBranchingVariables = abstractionInformation.getProbabilisticBranchingVariableSet(abstractionInformation.getProbabilisticBranchingVariableCount()); + variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); storm::dd::Bdd reachableStates = this->getReachableStates(initialStates, transitionRelation); - + // Determine the bottom states. storm::dd::Bdd bottomStates; if (addedAllGuards) { - bottomStates = ddInformation.manager->getBddZero(); + bottomStates = abstractionInformation.getDdManager().getBddZero(); } else { bottomStateAbstractor.constrain(reachableStates); bottomStates = bottomStateAbstractor.getAbstractStates(); } // Find the deadlock states in the model. - storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); + storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); deadlockStates = reachableStates && !deadlockStates; // If there are deadlock states, we fix them now. - storm::dd::Add deadlockTransitions = ddInformation.manager->template getAddZero(); + storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); if (!deadlockStates.isZero()) { - deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0) && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd(); } - + // Construct the transition matrix by cutting away the transitions of unreachable states. storm::dd::Add transitionMatrix = (gameBdd.first && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; - std::set usedPlayer2Variables; - for (uint_fast64_t index = 0; index < gameBdd.second; ++index) { - usedPlayer2Variables.insert(usedPlayer2Variables.end(), ddInformation.optionDdVariables[index].first); - } + std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + gameBdd.second); std::set allNondeterminismVariables = usedPlayer2Variables; - allNondeterminismVariables.insert(ddInformation.commandDdVariable); - - return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, ddInformation.manager->getBddZero(), transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); + allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); + + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().end()), abstractionInformation.getPredicateToBddMap()); } template @@ -187,8 +178,8 @@ namespace storm { uint_fast64_t reachabilityIteration = 0; while (!frontier.isZero()) { ++reachabilityIteration; - frontier = frontier.andExists(transitionRelation, ddInformation.sourceVariables); - frontier = frontier.swapVariables(ddInformation.predicateDdVariables); + frontier = frontier.andExists(transitionRelation, abstractionInformation.getSourceVariables()); + frontier = frontier.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()); frontier &= !reachableStates; reachableStates |= frontier; STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis."); diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 412a556a5..8b4eb9a82 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -2,8 +2,7 @@ #include "src/storage/dd/DdType.h" -#include "src/abstraction/AbstractionDdInformation.h" -#include "src/abstraction/AbstractionExpressionInformation.h" +#include "src/abstraction/AbstractionInformation.h" #include "src/abstraction/StateSetAbstractor.h" #include "src/abstraction/MenuGame.h" #include "src/abstraction/prism/AbstractModule.h" @@ -46,6 +45,11 @@ namespace storm { */ 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(AbstractProgram const&) = default; + AbstractProgram& operator=(AbstractProgram const&) = default; + AbstractProgram(AbstractProgram&&) = default; + AbstractProgram& operator=(AbstractProgram&&) = default; + /*! * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. * @@ -87,21 +91,18 @@ namespace storm { */ std::unique_ptr> buildGame(); + // The concrete program this abstract program refers to. + std::reference_wrapper program; + // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; - // A struct containing all DD-related information like variables and managers. - AbstractionDdInformation ddInformation; - - // A struct containing all expression-related information like variables, managers and the predicates. - AbstractionExpressionInformation expressionInformation; + // An object containing all information about the abstraction like predicates and the corresponding DDs. + AbstractionInformation abstractionInformation; // The abstract modules of the abstract program. std::vector> modules; - // The concrete program this abstract program refers to. - std::reference_wrapper program; - // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index de4f22cdb..d5dd28262 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -367,18 +367,23 @@ namespace storm { namespace std { template <> - struct less { - bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const { + struct less { + bool operator()(storm::expressions::Expression const& lhs, storm::expressions::Expression const& rhs) const { return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer(); } }; -} -namespace std { template <> - struct hash { - size_t operator()(const storm::expressions::Expression& expr) const { - return reinterpret_cast(expr.getBaseExpressionPointer().get()); + struct hash { + size_t operator()(storm::expressions::Expression const& e) const { + return reinterpret_cast(e.getBaseExpressionPointer().get()); + } + }; + + template <> + struct equal_to { + bool operator()(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2) const { + return e1.areSame(e2); } }; } diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index d24bc742c..8581ea394 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -7,18 +7,18 @@ namespace storm { namespace expressions { template - ExprtkExpressionEvaluatorBase::ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase(manager), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) { + ExprtkExpressionEvaluatorBase::ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase(manager), parser(std::make_unique>()), symbolTable(std::make_unique>()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) { for (auto const& variableTypePair : manager) { if (variableTypePair.second.isBooleanType()) { - symbolTable.add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]); } else if (variableTypePair.second.isIntegerType()) { - symbolTable.add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]); } else if (variableTypePair.second.isRationalType()) { - symbolTable.add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]); } } - symbolTable.add_constants(); + symbolTable->add_constants(); } template @@ -47,8 +47,8 @@ namespace storm { typename ExprtkExpressionEvaluatorBase::CompiledExpressionType& ExprtkExpressionEvaluatorBase::getCompiledExpression(storm::expressions::Expression const& expression) const { std::pair result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType()); CompiledExpressionType& compiledExpression = result.first->second; - compiledExpression.register_symbol_table(symbolTable); - bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression); + compiledExpression.register_symbol_table(*symbolTable); + bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression); STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk: " << expression); return compiledExpression; } diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h index 2ae6800ba..3b7ec3732 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storage/expressions/ExprtkExpressionEvaluator.h @@ -37,10 +37,10 @@ namespace storm { CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const; // The parser used. - mutable exprtk::parser parser; + mutable std::unique_ptr> parser; // The symbol table used. - mutable exprtk::symbol_table symbolTable; + mutable std::unique_ptr> symbolTable; // The actual data that is fed into the expression. std::vector booleanValues;