diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index d63e855d3..1b26c6987 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -8,7 +8,7 @@ ExternalProject_Add( DOWNLOAD_COMMAND "" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0 PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 - UPDATE_COMMAND ${AUTORECONF} + PATCH_COMMAND ${AUTORECONF} CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} BUILD_COMMAND make "CFLAGS=-O2 -w" INSTALL_COMMAND make install diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6e4271092..7d241ec00 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -10,6 +10,8 @@ file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.cpp) +file(GLOB STORM_ABSTRACTION_FILES ${PROJECT_SOURCE_DIR}/src/abstraction/*.h ${PROJECT_SOURCE_DIR}/src/abstraction/*.cpp) +file(GLOB_RECURSE STORM_ABSTRACTION_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/abstraction/prism/*.h ${PROJECT_SOURCE_DIR}/src/abstraction/prism/*.cpp) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) file(GLOB_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp) @@ -47,7 +49,6 @@ file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/ file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) -file(GLOB STORM_STORAGE_PRISM_MENU_GAME_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) @@ -66,6 +67,8 @@ set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) source_group(dft FILES ${STORM_DYFTTEE_FILE}) +source_group(abstraction FILES ${STORM_ABSTRACTION_FILES}) +source_group(abstraction\\prism FILES ${STORM_ABSTRACTION_PRISM_FILES}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) source_group(generator FILES ${STORM_GENERATOR_FILES}) diff --git a/src/abstraction/AbstractionDdInformation.cpp b/src/abstraction/AbstractionDdInformation.cpp new file mode 100644 index 000000000..f3b8dbf15 --- /dev/null +++ b/src/abstraction/AbstractionDdInformation.cpp @@ -0,0 +1,97 @@ +#include "src/abstraction/AbstractionDdInformation.h" + +#include + +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Expression.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; + + // Create the new predicate variable below all other predicate variables. + if (predicateDdVariables.empty()) { + newMetaVariable = manager->addMetaVariable(stream.str()); + } else { + newMetaVariable = manager->addMetaVariable(stream.str(), std::make_pair(storm::dd::MetaVariablePosition::Below, predicateDdVariables.back().second)); + } + + 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; + + } +} \ No newline at end of file diff --git a/src/abstraction/AbstractionDdInformation.h b/src/abstraction/AbstractionDdInformation.h new file mode 100644 index 000000000..0c6301936 --- /dev/null +++ b/src/abstraction/AbstractionDdInformation.h @@ -0,0 +1,113 @@ +#pragma once + +#include +#include +#include +#include +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace dd { + template + class DdManager; + + template + class Bdd; + } + + namespace expressions { + class Expression; + } + + 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 new file mode 100644 index 000000000..f3ef47074 --- /dev/null +++ b/src/abstraction/AbstractionExpressionInformation.cpp @@ -0,0 +1,64 @@ +#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; + } + + } +} \ No newline at end of file diff --git a/src/abstraction/AbstractionExpressionInformation.h b/src/abstraction/AbstractionExpressionInformation.h new file mode 100644 index 000000000..97c3ec54e --- /dev/null +++ b/src/abstraction/AbstractionExpressionInformation.h @@ -0,0 +1,126 @@ +#pragma once + +#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/LocalExpressionInformation.cpp b/src/abstraction/LocalExpressionInformation.cpp new file mode 100644 index 000000000..91a1af80d --- /dev/null +++ b/src/abstraction/LocalExpressionInformation.cpp @@ -0,0 +1,196 @@ +#include "src/abstraction/LocalExpressionInformation.h" + +#include + +#include "src/utility/macros.h" + +namespace storm { + namespace abstraction { + + LocalExpressionInformation::LocalExpressionInformation(std::set const& relevantVariables, std::vector> const& expressionIndexPairs) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) { + // Assign each variable to a new block. + uint_fast64_t currentBlock = 0; + variableBlocks.resize(relevantVariables.size()); + for (auto const& variable : relevantVariables) { + this->variableToBlockMapping[variable] = currentBlock; + this->variableToExpressionsMapping[variable] = std::set(); + variableBlocks[currentBlock].insert(variable); + ++currentBlock; + } + + // Add all expressions, which might relate some variables. + for (auto const& expressionIndexPair : expressionIndexPairs) { + this->addExpression(expressionIndexPair.first, expressionIndexPair.second); + } + } + + bool LocalExpressionInformation::addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex) { + // Register the expression for all variables that appear in it. + std::set expressionVariables = expression.getVariables(); + for (auto const& variable : expressionVariables) { + variableToExpressionsMapping[variable].insert(this->expressions.size()); + } + + // Add the expression to the block of the first variable. When relating the variables, the blocks will + // get merged (if necessary). + STORM_LOG_ASSERT(!expressionVariables.empty(), "Found no variables in expression."); + expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size()); + + // Add expression and relate all the appearing variables. + this->globalToLocalIndexMapping[globalExpressionIndex] = this->expressions.size(); + this->expressions.push_back(expression); + return this->relate(expressionVariables); + } + + bool LocalExpressionInformation::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { + return getBlockIndexOfVariable(firstVariable) == getBlockIndexOfVariable(secondVariable); + } + + bool LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { + return this->relate({firstVariable, secondVariable}); + } + + bool LocalExpressionInformation::relate(std::set const& variables) { + // Determine all blocks that need to be merged. + std::set blocksToMerge; + for (auto const& variable : variables) { + blocksToMerge.insert(getBlockIndexOfVariable(variable)); + } + + STORM_LOG_ASSERT(!blocksToMerge.empty(), "Found no blocks to merge."); + + // If we found a single block only, there is nothing to do. + if (blocksToMerge.size() == 1) { + return false; + } + + this->mergeBlocks(blocksToMerge); + return true; + } + + void LocalExpressionInformation::mergeBlocks(std::set const& blocksToMerge) { + // Merge all blocks into the block to keep. + std::vector> newVariableBlocks; + std::vector> newExpressionBlocks; + + std::set::const_iterator blocksToMergeIt = blocksToMerge.begin(); + std::set::const_iterator blocksToMergeIte = blocksToMerge.end(); + + // Determine which block to keep (to merge the other blocks into). + uint_fast64_t blockToKeep = *blocksToMergeIt; + ++blocksToMergeIt; + + for (uint_fast64_t blockIndex = 0; blockIndex < variableBlocks.size(); ++blockIndex) { + // If the block is the next one to merge into the block to keep, do so now. + if (blocksToMergeIt != blocksToMergeIte && *blocksToMergeIt == blockIndex && blockIndex != blockToKeep) { + // Adjust the mapping for all variables of the old block. + for (auto const& variable : variableBlocks[blockIndex]) { + variableToBlockMapping[variable] = blockToKeep; + } + + newVariableBlocks[blockToKeep].insert(variableBlocks[blockIndex].begin(), variableBlocks[blockIndex].end()); + newExpressionBlocks[blockToKeep].insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end()); + ++blocksToMergeIt; + } else { + // Otherwise just move the current block to the new partition. + + // Adjust the mapping for all variables of the old block. + for (auto const& variable : variableBlocks[blockIndex]) { + variableToBlockMapping[variable] = newVariableBlocks.size(); + } + + newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex])); + newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex])); + } + } + + variableBlocks = std::move(newVariableBlocks); + expressionBlocks = std::move(newExpressionBlocks); + } + + std::set const& LocalExpressionInformation::getBlockOfVariable(storm::expressions::Variable const& variable) const { + return variableBlocks[getBlockIndexOfVariable(variable)]; + } + + uint_fast64_t LocalExpressionInformation::getNumberOfBlocks() const { + return this->variableBlocks.size(); + } + + std::set const& LocalExpressionInformation::getVariableBlockWithIndex(uint_fast64_t blockIndex) const { + return this->variableBlocks[blockIndex]; + } + + uint_fast64_t LocalExpressionInformation::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const { + STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); + return this->variableToBlockMapping.find(variable)->second; + } + + std::set const& LocalExpressionInformation::getRelatedExpressions(storm::expressions::Variable const& variable) const { + return this->expressionBlocks[getBlockIndexOfVariable(variable)]; + } + + std::set LocalExpressionInformation::getRelatedExpressions(std::set const& variables) const { + // Start by determining the indices of all expression blocks that are related to any of the variables. + std::set relatedExpressionBlockIndices; + for (auto const& variable : variables) { + relatedExpressionBlockIndices.insert(getBlockIndexOfVariable(variable)); + } + + // Then join the expressions of these blocks and return the result. + std::set result; + for (auto const& blockIndex : relatedExpressionBlockIndices) { + result.insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end()); + } + return result; + } + + std::set const& LocalExpressionInformation::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const { + STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); + return this->variableToExpressionsMapping.find(variable)->second; + } + + std::set LocalExpressionInformation::getExpressionsUsingVariables(std::set const& variables) const { + std::set result; + + for (auto const& variable : variables) { + STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); + auto it = this->variableToExpressionsMapping.find(variable); + result.insert(it->second.begin(), it->second.end()); + } + + return result; + } + + storm::expressions::Expression const& LocalExpressionInformation::getExpression(uint_fast64_t expressionIndex) const { + return this->expressions[expressionIndex]; + } + + std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) { + std::vector blocks; + for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) { + auto const& variableBlock = partition.variableBlocks[index]; + auto const& expressionBlock = partition.expressionBlocks[index]; + + std::vector variablesInBlock; + for (auto const& variable : variableBlock) { + variablesInBlock.push_back(variable.getName()); + } + + std::vector expressionsInBlock; + for (auto const& expression : expressionBlock) { + std::stringstream stream; + stream << partition.expressions[expression]; + expressionsInBlock.push_back(stream.str()); + } + + blocks.push_back("<[" + boost::algorithm::join(variablesInBlock, ", ") + "], [" + boost::algorithm::join(expressionsInBlock, ", ") + "]>"); + } + + out << "{"; + out << boost::join(blocks, ", "); + out << "}"; + return out; + } + + } +} \ No newline at end of file diff --git a/src/abstraction/LocalExpressionInformation.h b/src/abstraction/LocalExpressionInformation.h new file mode 100644 index 000000000..b9fc39b91 --- /dev/null +++ b/src/abstraction/LocalExpressionInformation.h @@ -0,0 +1,165 @@ +#pragma once + +#include +#include +#include +#include + +#include "src/storage/expressions/Variable.h" +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace abstraction { + + class LocalExpressionInformation { + public: + /*! + * Constructs a new variable partition. + * + * @param relevantVariables The variables of this partition. + * @param expressionIndexPairs The (initial) pairs of expressions and their global indices. + */ + LocalExpressionInformation(std::set const& relevantVariables, std::vector> const& expressionIndexPairs = {}); + + /*! + * Adds the expression and therefore indirectly may cause blocks of variables to be merged. + * + * @param expression The expression to add. + * @param globalExpressionIndex The global index of the expression. + * @return True iff the partition changed. + */ + bool addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex); + + /*! + * Retrieves whether the two given variables are in the same block of the partition. + * + * @param firstVariable The first variable. + * @param secondVariable The second variable. + * @return True iff the two variables are in the same block. + */ + bool areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); + + /*! + * Places the given variables in the same block of the partition and performs the implied merges. + * + * @param firstVariable The first variable. + * @param secondVariable The second variable. + * @return True iff the partition changed. + */ + bool relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); + + /*! + * Places the given variables in the same block of the partition and performs the implied merges. + * + * @param variables The variables to relate. + * @return True iff the partition changed. + */ + bool relate(std::set const& variables); + + /*! + * Retrieves the block of related variables of the given variable. + * + * @param variable The variable whose block to retrieve. + * @return The block of the variable. + */ + std::set const& getBlockOfVariable(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the block index of the given variable. + * + * @param variable The variable for which to retrieve the block. + * @return The block index of the given variable. + */ + uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the number of blocks of the variable partition. + * + * @return The number of blocks in this partition. + */ + uint_fast64_t getNumberOfBlocks() const; + + /*! + * Retrieves the block with the given index. + * + * @param blockIndex The index of the block to retrieve. + * @return The block with the given index. + */ + std::set const& getVariableBlockWithIndex(uint_fast64_t blockIndex) const; + + /*! + * Retrieves the indices of the expressions related to the given variable. + * + * @param variable The variable for which to retrieve the related expressions. + * @return The related expressions. + */ + std::set const& getRelatedExpressions(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the indices of the expressions related to any of the given variables. + * + * @param variables The variables for which to retrieve the related expressions. + * @return The related expressions. + */ + std::set getRelatedExpressions(std::set const& variables) const; + + /*! + * Retrieves the indices of the expressions in which the given variable appears. + * + * @param variable The variable for which to retrieve the expressions. + * @return The indices of all expressions using the given variable. + */ + std::set const& getExpressionsUsingVariable(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the indices of the expressions in which the given variables appear. + * + * @param variables The variables for which to retrieve the expressions. + * @return The indices of all expressions using the given variables. + */ + std::set getExpressionsUsingVariables(std::set const& variables) const; + + /*! + * Retrieves the expression with the given index. + * + * @param expressionIndex The index of the expression to retrieve. + * @return The corresponding expression. + */ + storm::expressions::Expression const& getExpression(uint_fast64_t expressionIndex) const; + + friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition); + + private: + /*! + * Merges the blocks with the given indices. + * + * @param blocksToMerge The indices of the blocks to merge. + */ + void mergeBlocks(std::set const& blocksToMerge); + + // The set of variables relevant for this partition. + std::set relevantVariables; + + // A mapping from variables to their blocks. + std::unordered_map variableToBlockMapping; + + // The variable blocks of the partition. + std::vector> variableBlocks; + + // The expression blocks of the partition. + std::vector> expressionBlocks; + + // A mapping from variables to the indices of all expressions they appear in. + std::unordered_map> variableToExpressionsMapping; + + // A mapping from global expression indices to local ones. + std::unordered_map globalToLocalIndexMapping; + + // The vector of all expressions. + std::vector expressions; + }; + + std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition); + + } +} diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp new file mode 100644 index 000000000..b84a735ae --- /dev/null +++ b/src/abstraction/MenuGame.cpp @@ -0,0 +1,67 @@ +#include "src/abstraction/MenuGame.h" + +#include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/Add.h" + +#include "src/models/symbolic/StandardRewardModel.h" + +namespace storm { + namespace abstraction { + + template + MenuGame::MenuGame(std::shared_ptr> manager, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + storm::dd::Bdd bottomStates, + std::set const& rowVariables, + std::set const& columnVariables, + std::vector> const& rowColumnMetaVariablePairs, + 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) { + // Intentionally left empty. + } + + template + storm::dd::Bdd MenuGame::getStates(std::string const& label) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels."); + } + + template + storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression) const { + return this->getStates(expression, false); + } + + template + storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression, bool negated) const { + auto it = expressionToBddMap.find(expression); + STORM_LOG_THROW(it != expressionToBddMap.end(), storm::exceptions::InvalidArgumentException, "The given expression was not used in the abstraction process and can therefore not be retrieved."); + if (negated) { + return !it->second && this->getReachableStates(); + } else { + return it->second && this->getReachableStates(); + } + } + + template + storm::dd::Bdd MenuGame::getBottomStates() const { + return bottomStates; + } + + template + bool MenuGame::hasLabel(std::string const& label) const { + return false; + } + + template class MenuGame; + + } +} + diff --git a/src/storage/prism/menu_games/MenuGame.h b/src/abstraction/MenuGame.h similarity index 94% rename from src/storage/prism/menu_games/MenuGame.h rename to src/abstraction/MenuGame.h index fbec4e062..2d1be6b44 100644 --- a/src/storage/prism/menu_games/MenuGame.h +++ b/src/abstraction/MenuGame.h @@ -1,5 +1,4 @@ -#ifndef STORM_PRISM_MENU_GAMES_MENUGAME_H_ -#define STORM_PRISM_MENU_GAMES_MENUGAME_H_ +#pragma once #include @@ -8,9 +7,8 @@ #include "src/utility/OsDetection.h" namespace storm { - namespace prism { - namespace menu_games { - + namespace abstraction { + /*! * This class represents a discrete-time stochastic two-player game. */ @@ -21,11 +19,8 @@ namespace storm { MenuGame(MenuGame const& other) = default; MenuGame& operator=(MenuGame const& other) = default; - -#ifndef WINDOWS MenuGame(MenuGame&& other) = default; MenuGame& operator=(MenuGame&& other) = default; -#endif /*! * Constructs a model from the given data. @@ -102,8 +97,5 @@ namespace storm { storm::dd::Bdd bottomStates; }; - } // namespace menu_games - } // namespace prism -} // namespace storm - -#endif /* STORM_PRISM_MENU_GAMES_MENUGAME_H_ */ + } +} diff --git a/src/abstraction/MenuGameAbstractor.cpp b/src/abstraction/MenuGameAbstractor.cpp new file mode 100644 index 000000000..dc9f1ceac --- /dev/null +++ b/src/abstraction/MenuGameAbstractor.cpp @@ -0,0 +1 @@ +#include "src/abstraction/MenuGameAbstractor.h" \ No newline at end of file diff --git a/src/abstraction/MenuGameAbstractor.h b/src/abstraction/MenuGameAbstractor.h new file mode 100644 index 000000000..a99cd8fdd --- /dev/null +++ b/src/abstraction/MenuGameAbstractor.h @@ -0,0 +1,16 @@ +#pragma once + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace abstraction { + + template + class MenuGameAbstractor { + + + + }; + + } +} \ No newline at end of file diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp new file mode 100644 index 000000000..f104956ed --- /dev/null +++ b/src/abstraction/StateSetAbstractor.cpp @@ -0,0 +1,154 @@ +#include "src/abstraction/StateSetAbstractor.h" + +#include "src/abstraction/AbstractionExpressionInformation.h" +#include "src/abstraction/AbstractionDdInformation.h" + +#include "src/storage/dd/DdManager.h" + +#include "src/utility/macros.h" +#include "src/utility/solver.h" + +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); + } + + // Assert all state predicates. + for (auto const& predicate : statePredicates) { + smtSolver->add(predicate); + + // Extract the variables of the predicate, so we know which variables were used when abstracting. + std::set usedVariables = predicate.getVariables(); + 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); + + for (auto const& element : newPredicateVariables) { + smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicates()[element.second])); + decisionVariables.push_back(element.first); + } + + relevantPredicatesAndVariables.insert(relevantPredicatesAndVariables.end(), newPredicateVariables.begin(), newPredicateVariables.end()); + std::sort(relevantPredicatesAndVariables.begin(), relevantPredicatesAndVariables.end(), [] (std::pair const& firstPair, std::pair const& secondPair) { return firstPair.second < secondPair.second; } ); + } + + template + 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); + } + needsRecomputation = true; + } + + template + void StateSetAbstractor::constrain(storm::dd::Bdd const& newConstraint) { + // If the constraint is different from the last one, we add it to the solver. + if (newConstraint != this->constraint) { + constraint = newConstraint; + this->pushConstraintBdd(); + } + } + + template + 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(); + for (auto const& variableIndexPair : relevantPredicatesAndVariables) { + if (model.getBooleanValue(variableIndexPair.first)) { + result &= ddInformation.predicateBdds[variableIndexPair.second].first; + } else { + result &= !ddInformation.predicateBdds[variableIndexPair.second].first; + } + } + return result; + } + + template + void StateSetAbstractor::recomputeCachedBdd() { + // Now check whether we need to recompute the cached BDD. + std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); + STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); + + // Since the number of relevant predicates is monotonic, we can simply check for the size here. + STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); + bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); + + if (!recomputeBdd) { + return; + } + + // Before adding the missing predicates, we need to remove the constraint BDD. + this->popConstraintBdd(); + + // If we need to recompute the BDD, we start by introducing decision variables and the corresponding + // constraints in the SMT problem. + addMissingPredicates(newRelevantPredicateIndices); + + // Then re-add the constraint BDD. + this->pushConstraintBdd(); + + STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); + + storm::dd::Bdd result = ddInformation.manager->getBddZero(); + uint_fast64_t modelCounter = 0; + smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); + + cachedBdd = result; + } + + template + void StateSetAbstractor::popConstraintBdd() { + // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver. + if (this->constraint.isOne()) { + return; + } + smtSolver->pop(); + } + + template + void StateSetAbstractor::pushConstraintBdd() { + if (this->constraint.isOne()) { + return; + } + + // Create a new backtracking point before adding the constraint. + smtSolver->push(); + + // Then add the constraint. + std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap); + + for (auto const& expression : result.first) { + smtSolver->add(expression); + } + } + + template + storm::dd::Bdd StateSetAbstractor::getAbstractStates() { + if (needsRecomputation) { + this->recomputeCachedBdd(); + } + return cachedBdd; + } + + template class StateSetAbstractor; + } +} diff --git a/src/abstraction/StateSetAbstractor.h b/src/abstraction/StateSetAbstractor.h new file mode 100644 index 000000000..bcacc70fa --- /dev/null +++ b/src/abstraction/StateSetAbstractor.h @@ -0,0 +1,145 @@ +#pragma once + +#include +#include +#include + +#include "src/utility/OsDetection.h" + +#include "src/storage/dd/DdType.h" + +#include "src/solver/SmtSolver.h" + +#include "src/abstraction/LocalExpressionInformation.h" + +namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace dd { + template + class Bdd; + + template + class Add; + } + + namespace abstraction { + template + class AbstractionDdInformation; + + class AbstractionExpressionInformation; + + template + class StateSetAbstractor { + public: + // Provide a no-op default constructor. + StateSetAbstractor() = default; + + StateSetAbstractor(StateSetAbstractor const& other) = default; + StateSetAbstractor& operator=(StateSetAbstractor const& other) = default; + +#ifndef WINDOWS + StateSetAbstractor(StateSetAbstractor&& other) = default; + StateSetAbstractor& operator=(StateSetAbstractor&& other) = default; +#endif + + /*! + * 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 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); + + /*! + * Refines the abstractor by making the given predicates new abstract predicates. + * + * @param newPredicateIndices The indices of the new predicates. + */ + void refine(std::vector const& newPredicateIndices); + + /*! + * Constraints the abstract states with the given BDD. + * + * @param newConstraint The BDD used as the constraint. + */ + void constrain(storm::dd::Bdd const& newConstraint); + + /*! + * Retrieves the set of abstract states matching all predicates added to this abstractor. + * + * @return The set of matching abstract states in the form of a BDD + */ + storm::dd::Bdd getAbstractStates(); + + private: + /*! + * Creates decision variables and the corresponding constraints for the missing predicates. + * + * @param newRelevantPredicateIndices The set of all relevant predicate indices. + */ + void addMissingPredicates(std::set const& newRelevantPredicateIndices); + + /*! + * Adds the current constraint BDD to the solver. + */ + void pushConstraintBdd(); + + /*! + * Removes the current constraint BDD (if any) from the solver. + */ + void popConstraintBdd(); + + /*! + * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. + */ + void recomputeCachedBdd(); + + /*! + * Translates the given model to a state DD. + * + * @param model The model to translate. + * @return The state encoded as a DD. + */ + storm::dd::Bdd getStateBdd(storm::solver::SmtSolver::ModelReference const& model) 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 local expression-related information. + LocalExpressionInformation localExpressionInformation; + + // The set of relevant predicates and the corresponding decision variables. + std::vector> relevantPredicatesAndVariables; + + // The set of all variables appearing in the concrete predicates. + std::set concretePredicateVariables; + + // The set of all decision variables over which to perform the all-sat enumeration. + std::vector decisionVariables; + + // A flag indicating whether the cached BDD needs recomputation. + bool needsRecomputation; + + // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work + // needed to be done). + storm::dd::Bdd cachedBdd; + + // This BDD currently constrains the search for solutions. + storm::dd::Bdd constraint; + }; + } +} diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp similarity index 98% rename from src/storage/prism/menu_games/AbstractCommand.cpp rename to src/abstraction/prism/AbstractCommand.cpp index 821512f95..22c476eec 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -1,9 +1,9 @@ -#include "src/storage/prism/menu_games/AbstractCommand.h" +#include "src/abstraction/prism/AbstractCommand.h" #include -#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" -#include "src/storage/prism/menu_games/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionExpressionInformation.h" +#include "src/abstraction/AbstractionDdInformation.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -15,8 +15,8 @@ #include "src/utility/macros.h" namespace storm { - namespace prism { - namespace menu_games { + 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() { diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h similarity index 93% rename from src/storage/prism/menu_games/AbstractCommand.h rename to src/abstraction/prism/AbstractCommand.h index 57f7db9ed..9e5d44c24 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -1,12 +1,11 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ +#pragma once #include #include #include #include -#include "src/storage/prism/menu_games/LocalExpressionInformation.h" +#include "src/abstraction/LocalExpressionInformation.h" #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Expression.h" @@ -32,13 +31,15 @@ namespace storm { // Forward-declare concrete command and assignment classes. class Command; class Assignment; + } + + namespace abstraction { + template + struct AbstractionDdInformation; - namespace menu_games { - template - struct AbstractionDdInformation; - - struct AbstractionExpressionInformation; - + struct AbstractionExpressionInformation; + + namespace prism { template class AbstractCommand { public: @@ -162,7 +163,7 @@ namespace storm { AbstractionDdInformation const& ddInformation; // The concrete command this abstract command refers to. - std::reference_wrapper command; + std::reference_wrapper command; // The local expression-related information. LocalExpressionInformation localExpressionInformation; @@ -180,5 +181,3 @@ namespace storm { } } } - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp similarity index 92% rename from src/storage/prism/menu_games/AbstractModule.cpp rename to src/abstraction/prism/AbstractModule.cpp index c9d597d02..feb7c7df3 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -1,7 +1,7 @@ -#include "src/storage/prism/menu_games/AbstractModule.h" +#include "src/abstraction/prism/AbstractModule.h" -#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" -#include "src/storage/prism/menu_games/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionExpressionInformation.h" +#include "src/abstraction/AbstractionDdInformation.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -9,8 +9,8 @@ #include "src/storage/prism/Module.h" namespace storm { - namespace prism { - namespace menu_games { + namespace abstraction { + 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) { diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/abstraction/prism/AbstractModule.h similarity index 84% rename from src/storage/prism/menu_games/AbstractModule.h rename to src/abstraction/prism/AbstractModule.h index 473eb4913..721b2c3f3 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -1,9 +1,8 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ +#pragma once #include "src/storage/dd/DdType.h" -#include "src/storage/prism/menu_games/AbstractCommand.h" +#include "src/abstraction/prism/AbstractCommand.h" #include "src/storage/expressions/Expression.h" @@ -13,13 +12,15 @@ namespace storm { namespace prism { // Forward-declare concrete module class. class Module; + } + + namespace abstraction { + template + struct AbstractionDdInformation; - namespace menu_games { - template - struct AbstractionDdInformation; - - struct AbstractionExpressionInformation; - + struct AbstractionExpressionInformation; + + namespace prism { template class AbstractModule { public: @@ -65,10 +66,8 @@ namespace storm { std::vector> commands; // The concrete module this abstract module refers to. - std::reference_wrapper module; + std::reference_wrapper module; }; } } } - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp similarity index 97% rename from src/storage/prism/menu_games/AbstractProgram.cpp rename to src/abstraction/prism/AbstractProgram.cpp index e8ec36ea7..933f0ebc3 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -1,4 +1,4 @@ -#include "src/storage/prism/menu_games/AbstractProgram.h" +#include "src/abstraction/prism/AbstractProgram.h" #include "src/storage/prism/Program.h" @@ -13,8 +13,8 @@ #include "src/exceptions/InvalidArgumentException.h" namespace storm { - namespace prism { - namespace menu_games { + namespace abstraction { + 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) { @@ -69,7 +69,7 @@ namespace storm { modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory); } - // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. + // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); // Finally, we build the game the first time. @@ -176,7 +176,6 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(ddInformation.commandDdVariable); - // FIXME: no deadlock states guaranteed? 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)); } diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h similarity index 87% rename from src/storage/prism/menu_games/AbstractProgram.h rename to src/abstraction/prism/AbstractProgram.h index ceccb33fc..412a556a5 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -1,13 +1,12 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ +#pragma once #include "src/storage/dd/DdType.h" -#include "src/storage/prism/menu_games/AbstractionDdInformation.h" -#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" -#include "src/storage/prism/menu_games/StateSetAbstractor.h" -#include "src/storage/prism/menu_games/AbstractModule.h" -#include "src/storage/prism/menu_games/MenuGame.h" +#include "src/abstraction/AbstractionDdInformation.h" +#include "src/abstraction/AbstractionExpressionInformation.h" +#include "src/abstraction/StateSetAbstractor.h" +#include "src/abstraction/MenuGame.h" +#include "src/abstraction/prism/AbstractModule.h" #include "src/storage/expressions/Expression.h" @@ -28,8 +27,10 @@ namespace storm { namespace prism { // Forward-declare concrete Program class. class Program; - - namespace menu_games { + } + + namespace abstraction { + namespace prism { template class AbstractProgram { @@ -43,7 +44,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates. */ - AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory = std::unique_ptr(new storm::utility::solver::SmtSolverFactory()), bool addAllGuards = false); + AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory = std::make_unique(), bool addAllGuards = false); /*! * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. @@ -99,7 +100,7 @@ namespace storm { std::vector> modules; // The concrete program this abstract program refers to. - std::reference_wrapper program; + std::reference_wrapper program; // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; @@ -119,5 +120,3 @@ namespace storm { } } } - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index ec4de2b96..11174c167 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -6,7 +6,7 @@ namespace storm { namespace dd { - InternalDdManager::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE) { + InternalDdManager::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), numberOfDdVariables(0) { this->cuddManager.SetMaxMemory(static_cast(storm::settings::getModule().getMaximalMemory() * 1024ul * 1024ul)); this->cuddManager.SetEpsilon(storm::settings::getModule().getConstantPrecision()); diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp deleted file mode 100644 index a60bdb80f..000000000 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ /dev/null @@ -1,99 +0,0 @@ -#include "src/storage/prism/menu_games/AbstractionDdInformation.h" - -#include - -#include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/expressions/Expression.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 prism { - namespace menu_games { - - 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; - - // Create the new predicate variable below all other predicate variables. - if (predicateDdVariables.empty()) { - newMetaVariable = manager->addMetaVariable(stream.str()); - } else { - newMetaVariable = manager->addMetaVariable(stream.str(), std::make_pair(storm::dd::MetaVariablePosition::Below, predicateDdVariables.back().second)); - } - - 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; - - } - } -} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h deleted file mode 100644 index d3b86d12c..000000000 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ /dev/null @@ -1,118 +0,0 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ - -#include -#include -#include -#include -#include - -#include "src/storage/dd/DdType.h" -#include "src/storage/expressions/Variable.h" - -namespace storm { - namespace dd { - template - class DdManager; - - template - class Bdd; - } - - namespace expressions { - class Expression; - } - - namespace prism { - namespace menu_games { - - 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; - }; - - } - } -} - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ */ diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp deleted file mode 100644 index 54ce74223..000000000 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp +++ /dev/null @@ -1,66 +0,0 @@ -#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" - -#include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/expressions/Expression.h" - -namespace storm { - namespace prism { - namespace menu_games { - - 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; - } - - } - } -} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h deleted file mode 100644 index ece6e2075..000000000 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h +++ /dev/null @@ -1,130 +0,0 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ - -#include -#include - -namespace storm { - namespace expressions { - class ExpressionManager; - class Expression; - class Variable; - } - - namespace prism { - namespace menu_games { - - 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; - }; - } - } -} - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/LocalExpressionInformation.cpp b/src/storage/prism/menu_games/LocalExpressionInformation.cpp deleted file mode 100644 index 2be853712..000000000 --- a/src/storage/prism/menu_games/LocalExpressionInformation.cpp +++ /dev/null @@ -1,197 +0,0 @@ -#include "src/storage/prism/menu_games/LocalExpressionInformation.h" - -#include - -#include "src/utility/macros.h" - -namespace storm { - namespace prism { - namespace menu_games { - LocalExpressionInformation::LocalExpressionInformation(std::set const& relevantVariables, std::vector> const& expressionIndexPairs) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) { - // Assign each variable to a new block. - uint_fast64_t currentBlock = 0; - variableBlocks.resize(relevantVariables.size()); - for (auto const& variable : relevantVariables) { - this->variableToBlockMapping[variable] = currentBlock; - this->variableToExpressionsMapping[variable] = std::set(); - variableBlocks[currentBlock].insert(variable); - ++currentBlock; - } - - // Add all expressions, which might relate some variables. - for (auto const& expressionIndexPair : expressionIndexPairs) { - this->addExpression(expressionIndexPair.first, expressionIndexPair.second); - } - } - - bool LocalExpressionInformation::addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex) { - // Register the expression for all variables that appear in it. - std::set expressionVariables = expression.getVariables(); - for (auto const& variable : expressionVariables) { - variableToExpressionsMapping[variable].insert(this->expressions.size()); - } - - // Add the expression to the block of the first variable. When relating the variables, the blocks will - // get merged (if necessary). - STORM_LOG_ASSERT(!expressionVariables.empty(), "Found no variables in expression."); - expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size()); - - // Add expression and relate all the appearing variables. - this->globalToLocalIndexMapping[globalExpressionIndex] = this->expressions.size(); - this->expressions.push_back(expression); - return this->relate(expressionVariables); - } - - bool LocalExpressionInformation::areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { - return getBlockIndexOfVariable(firstVariable) == getBlockIndexOfVariable(secondVariable); - } - - bool LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { - return this->relate({firstVariable, secondVariable}); - } - - bool LocalExpressionInformation::relate(std::set const& variables) { - // Determine all blocks that need to be merged. - std::set blocksToMerge; - for (auto const& variable : variables) { - blocksToMerge.insert(getBlockIndexOfVariable(variable)); - } - - STORM_LOG_ASSERT(!blocksToMerge.empty(), "Found no blocks to merge."); - - // If we found a single block only, there is nothing to do. - if (blocksToMerge.size() == 1) { - return false; - } - - this->mergeBlocks(blocksToMerge); - return true; - } - - void LocalExpressionInformation::mergeBlocks(std::set const& blocksToMerge) { - // Merge all blocks into the block to keep. - std::vector> newVariableBlocks; - std::vector> newExpressionBlocks; - - std::set::const_iterator blocksToMergeIt = blocksToMerge.begin(); - std::set::const_iterator blocksToMergeIte = blocksToMerge.end(); - - // Determine which block to keep (to merge the other blocks into). - uint_fast64_t blockToKeep = *blocksToMergeIt; - ++blocksToMergeIt; - - for (uint_fast64_t blockIndex = 0; blockIndex < variableBlocks.size(); ++blockIndex) { - // If the block is the next one to merge into the block to keep, do so now. - if (blocksToMergeIt != blocksToMergeIte && *blocksToMergeIt == blockIndex && blockIndex != blockToKeep) { - // Adjust the mapping for all variables of the old block. - for (auto const& variable : variableBlocks[blockIndex]) { - variableToBlockMapping[variable] = blockToKeep; - } - - newVariableBlocks[blockToKeep].insert(variableBlocks[blockIndex].begin(), variableBlocks[blockIndex].end()); - newExpressionBlocks[blockToKeep].insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end()); - ++blocksToMergeIt; - } else { - // Otherwise just move the current block to the new partition. - - // Adjust the mapping for all variables of the old block. - for (auto const& variable : variableBlocks[blockIndex]) { - variableToBlockMapping[variable] = newVariableBlocks.size(); - } - - newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex])); - newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex])); - } - } - - variableBlocks = std::move(newVariableBlocks); - expressionBlocks = std::move(newExpressionBlocks); - } - - std::set const& LocalExpressionInformation::getBlockOfVariable(storm::expressions::Variable const& variable) const { - return variableBlocks[getBlockIndexOfVariable(variable)]; - } - - uint_fast64_t LocalExpressionInformation::getNumberOfBlocks() const { - return this->variableBlocks.size(); - } - - std::set const& LocalExpressionInformation::getVariableBlockWithIndex(uint_fast64_t blockIndex) const { - return this->variableBlocks[blockIndex]; - } - - uint_fast64_t LocalExpressionInformation::getBlockIndexOfVariable(storm::expressions::Variable const& variable) const { - STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); - return this->variableToBlockMapping.find(variable)->second; - } - - std::set const& LocalExpressionInformation::getRelatedExpressions(storm::expressions::Variable const& variable) const { - return this->expressionBlocks[getBlockIndexOfVariable(variable)]; - } - - std::set LocalExpressionInformation::getRelatedExpressions(std::set const& variables) const { - // Start by determining the indices of all expression blocks that are related to any of the variables. - std::set relatedExpressionBlockIndices; - for (auto const& variable : variables) { - relatedExpressionBlockIndices.insert(getBlockIndexOfVariable(variable)); - } - - // Then join the expressions of these blocks and return the result. - std::set result; - for (auto const& blockIndex : relatedExpressionBlockIndices) { - result.insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end()); - } - return result; - } - - std::set const& LocalExpressionInformation::getExpressionsUsingVariable(storm::expressions::Variable const& variable) const { - STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); - return this->variableToExpressionsMapping.find(variable)->second; - } - - std::set LocalExpressionInformation::getExpressionsUsingVariables(std::set const& variables) const { - std::set result; - - for (auto const& variable : variables) { - STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); - auto it = this->variableToExpressionsMapping.find(variable); - result.insert(it->second.begin(), it->second.end()); - } - - return result; - } - - storm::expressions::Expression const& LocalExpressionInformation::getExpression(uint_fast64_t expressionIndex) const { - return this->expressions[expressionIndex]; - } - - std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) { - std::vector blocks; - for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) { - auto const& variableBlock = partition.variableBlocks[index]; - auto const& expressionBlock = partition.expressionBlocks[index]; - - std::vector variablesInBlock; - for (auto const& variable : variableBlock) { - variablesInBlock.push_back(variable.getName()); - } - - std::vector expressionsInBlock; - for (auto const& expression : expressionBlock) { - std::stringstream stream; - stream << partition.expressions[expression]; - expressionsInBlock.push_back(stream.str()); - } - - blocks.push_back("<[" + boost::algorithm::join(variablesInBlock, ", ") + "], [" + boost::algorithm::join(expressionsInBlock, ", ") + "]>"); - } - - out << "{"; - out << boost::join(blocks, ", "); - out << "}"; - return out; - } - - } - } -} \ No newline at end of file diff --git a/src/storage/prism/menu_games/LocalExpressionInformation.h b/src/storage/prism/menu_games/LocalExpressionInformation.h deleted file mode 100644 index 908d2f181..000000000 --- a/src/storage/prism/menu_games/LocalExpressionInformation.h +++ /dev/null @@ -1,170 +0,0 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_ - -#include -#include -#include -#include - -#include "src/storage/expressions/Variable.h" -#include "src/storage/expressions/Expression.h" - -namespace storm { - namespace prism { - namespace menu_games { - - class LocalExpressionInformation { - public: - /*! - * Constructs a new variable partition. - * - * @param relevantVariables The variables of this partition. - * @param expressionIndexPairs The (initial) pairs of expressions and their global indices. - */ - LocalExpressionInformation(std::set const& relevantVariables, std::vector> const& expressionIndexPairs = {}); - - /*! - * Adds the expression and therefore indirectly may cause blocks of variables to be merged. - * - * @param expression The expression to add. - * @param globalExpressionIndex The global index of the expression. - * @return True iff the partition changed. - */ - bool addExpression(storm::expressions::Expression const& expression, uint_fast64_t globalExpressionIndex); - - /*! - * Retrieves whether the two given variables are in the same block of the partition. - * - * @param firstVariable The first variable. - * @param secondVariable The second variable. - * @return True iff the two variables are in the same block. - */ - bool areRelated(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); - - /*! - * Places the given variables in the same block of the partition and performs the implied merges. - * - * @param firstVariable The first variable. - * @param secondVariable The second variable. - * @return True iff the partition changed. - */ - bool relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); - - /*! - * Places the given variables in the same block of the partition and performs the implied merges. - * - * @param variables The variables to relate. - * @return True iff the partition changed. - */ - bool relate(std::set const& variables); - - /*! - * Retrieves the block of related variables of the given variable. - * - * @param variable The variable whose block to retrieve. - * @return The block of the variable. - */ - std::set const& getBlockOfVariable(storm::expressions::Variable const& variable) const; - - /*! - * Retrieves the block index of the given variable. - * - * @param variable The variable for which to retrieve the block. - * @return The block index of the given variable. - */ - uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const; - - /*! - * Retrieves the number of blocks of the variable partition. - * - * @return The number of blocks in this partition. - */ - uint_fast64_t getNumberOfBlocks() const; - - /*! - * Retrieves the block with the given index. - * - * @param blockIndex The index of the block to retrieve. - * @return The block with the given index. - */ - std::set const& getVariableBlockWithIndex(uint_fast64_t blockIndex) const; - - /*! - * Retrieves the indices of the expressions related to the given variable. - * - * @param variable The variable for which to retrieve the related expressions. - * @return The related expressions. - */ - std::set const& getRelatedExpressions(storm::expressions::Variable const& variable) const; - - /*! - * Retrieves the indices of the expressions related to any of the given variables. - * - * @param variables The variables for which to retrieve the related expressions. - * @return The related expressions. - */ - std::set getRelatedExpressions(std::set const& variables) const; - - /*! - * Retrieves the indices of the expressions in which the given variable appears. - * - * @param variable The variable for which to retrieve the expressions. - * @return The indices of all expressions using the given variable. - */ - std::set const& getExpressionsUsingVariable(storm::expressions::Variable const& variable) const; - - /*! - * Retrieves the indices of the expressions in which the given variables appear. - * - * @param variables The variables for which to retrieve the expressions. - * @return The indices of all expressions using the given variables. - */ - std::set getExpressionsUsingVariables(std::set const& variables) const; - - /*! - * Retrieves the expression with the given index. - * - * @param expressionIndex The index of the expression to retrieve. - * @return The corresponding expression. - */ - storm::expressions::Expression const& getExpression(uint_fast64_t expressionIndex) const; - - friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition); - - private: - /*! - * Merges the blocks with the given indices. - * - * @param blocksToMerge The indices of the blocks to merge. - */ - void mergeBlocks(std::set const& blocksToMerge); - - // The set of variables relevant for this partition. - std::set relevantVariables; - - // A mapping from variables to their blocks. - std::unordered_map variableToBlockMapping; - - // The variable blocks of the partition. - std::vector> variableBlocks; - - // The expression blocks of the partition. - std::vector> expressionBlocks; - - // A mapping from variables to the indices of all expressions they appear in. - std::unordered_map> variableToExpressionsMapping; - - // A mapping from global expression indices to local ones. - std::unordered_map globalToLocalIndexMapping; - - // The vector of all expressions. - std::vector expressions; - }; - - std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition); - - } - } -} - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_LOCALEXPRESSIONINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/MenuGame.cpp b/src/storage/prism/menu_games/MenuGame.cpp deleted file mode 100644 index 38967f7ee..000000000 --- a/src/storage/prism/menu_games/MenuGame.cpp +++ /dev/null @@ -1,69 +0,0 @@ -#include "src/storage/prism/menu_games/MenuGame.h" - -#include "src/exceptions/InvalidOperationException.h" -#include "src/exceptions/InvalidArgumentException.h" - -#include "src/storage/dd/Bdd.h" -#include "src/storage/dd/Add.h" - -#include "src/models/symbolic/StandardRewardModel.h" - -namespace storm { - namespace prism { - namespace menu_games { - - template - MenuGame::MenuGame(std::shared_ptr> manager, - storm::dd::Bdd reachableStates, - storm::dd::Bdd initialStates, - storm::dd::Bdd deadlockStates, - storm::dd::Add transitionMatrix, - storm::dd::Bdd bottomStates, - std::set const& rowVariables, - std::set const& columnVariables, - std::vector> const& rowColumnMetaVariablePairs, - 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) { - // Intentionally left empty. - } - - template - storm::dd::Bdd MenuGame::getStates(std::string const& label) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Menu games do not provide labels."); - } - - template - storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression) const { - return this->getStates(expression, false); - } - - template - storm::dd::Bdd MenuGame::getStates(storm::expressions::Expression const& expression, bool negated) const { - auto it = expressionToBddMap.find(expression); - STORM_LOG_THROW(it != expressionToBddMap.end(), storm::exceptions::InvalidArgumentException, "The given expression was not used in the abstraction process and can therefore not be retrieved."); - if (negated) { - return !it->second && this->getReachableStates(); - } else { - return it->second && this->getReachableStates(); - } - } - - template - storm::dd::Bdd MenuGame::getBottomStates() const { - return bottomStates; - } - - template - bool MenuGame::hasLabel(std::string const& label) const { - return false; - } - - template class MenuGame; - - } // namespace menu_games - } // namespace prism -} // namespace storm - diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp deleted file mode 100644 index 5b228afbb..000000000 --- a/src/storage/prism/menu_games/StateSetAbstractor.cpp +++ /dev/null @@ -1,156 +0,0 @@ -#include "src/storage/prism/menu_games/StateSetAbstractor.h" - -#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" -#include "src/storage/prism/menu_games/AbstractionDdInformation.h" - -#include "src/storage/dd/DdManager.h" - -#include "src/utility/macros.h" -#include "src/utility/solver.h" - -namespace storm { - namespace prism { - namespace menu_games { - - 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); - } - - // Assert all state predicates. - for (auto const& predicate : statePredicates) { - smtSolver->add(predicate); - - // Extract the variables of the predicate, so we know which variables were used when abstracting. - std::set usedVariables = predicate.getVariables(); - 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); - - for (auto const& element : newPredicateVariables) { - smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicates()[element.second])); - decisionVariables.push_back(element.first); - } - - relevantPredicatesAndVariables.insert(relevantPredicatesAndVariables.end(), newPredicateVariables.begin(), newPredicateVariables.end()); - std::sort(relevantPredicatesAndVariables.begin(), relevantPredicatesAndVariables.end(), [] (std::pair const& firstPair, std::pair const& secondPair) { return firstPair.second < secondPair.second; } ); - } - - template - 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); - } - needsRecomputation = true; - } - - template - void StateSetAbstractor::constrain(storm::dd::Bdd const& newConstraint) { - // If the constraint is different from the last one, we add it to the solver. - if (newConstraint != this->constraint) { - constraint = newConstraint; - this->pushConstraintBdd(); - } - } - - template - 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(); - for (auto const& variableIndexPair : relevantPredicatesAndVariables) { - if (model.getBooleanValue(variableIndexPair.first)) { - result &= ddInformation.predicateBdds[variableIndexPair.second].first; - } else { - result &= !ddInformation.predicateBdds[variableIndexPair.second].first; - } - } - return result; - } - - template - void StateSetAbstractor::recomputeCachedBdd() { - // Now check whether we need to recompute the cached BDD. - std::set newRelevantPredicateIndices = localExpressionInformation.getRelatedExpressions(concretePredicateVariables); - STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); - - // Since the number of relevant predicates is monotonic, we can simply check for the size here. - STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); - bool recomputeBdd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); - - if (!recomputeBdd) { - return; - } - - // Before adding the missing predicates, we need to remove the constraint BDD. - this->popConstraintBdd(); - - // If we need to recompute the BDD, we start by introducing decision variables and the corresponding - // constraints in the SMT problem. - addMissingPredicates(newRelevantPredicateIndices); - - // Then re-add the constraint BDD. - this->pushConstraintBdd(); - - STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); - - storm::dd::Bdd result = ddInformation.manager->getBddZero(); - uint_fast64_t modelCounter = 0; - smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); - - cachedBdd = result; - } - - template - void StateSetAbstractor::popConstraintBdd() { - // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver. - if (this->constraint.isOne()) { - return; - } - smtSolver->pop(); - } - - template - void StateSetAbstractor::pushConstraintBdd() { - if (this->constraint.isOne()) { - return; - } - - // Create a new backtracking point before adding the constraint. - smtSolver->push(); - - // Then add the constraint. - std::pair, std::unordered_map, storm::expressions::Variable>> result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap); - - for (auto const& expression : result.first) { - smtSolver->add(expression); - } - } - - template - storm::dd::Bdd StateSetAbstractor::getAbstractStates() { - if (needsRecomputation) { - this->recomputeCachedBdd(); - } - return cachedBdd; - } - - template class StateSetAbstractor; - } - } -} diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h deleted file mode 100644 index 157aa27b7..000000000 --- a/src/storage/prism/menu_games/StateSetAbstractor.h +++ /dev/null @@ -1,150 +0,0 @@ -#ifndef STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ -#define STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ - -#include -#include -#include - -#include "src/utility/OsDetection.h" - -#include "src/storage/dd/DdType.h" - -#include "src/solver/SmtSolver.h" - -#include "src/storage/prism/menu_games/LocalExpressionInformation.h" - -namespace storm { - namespace utility { - namespace solver { - class SmtSolverFactory; - } - } - - namespace dd { - template - class Bdd; - - template - class Add; - } - - namespace prism { - namespace menu_games { - template - class AbstractionDdInformation; - - class AbstractionExpressionInformation; - - template - class StateSetAbstractor { - public: - // Provide a no-op default constructor. - StateSetAbstractor() = default; - - StateSetAbstractor(StateSetAbstractor const& other) = default; - StateSetAbstractor& operator=(StateSetAbstractor const& other) = default; - -#ifndef WINDOWS - StateSetAbstractor(StateSetAbstractor&& other) = default; - StateSetAbstractor& operator=(StateSetAbstractor&& other) = default; -#endif - - /*! - * 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 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); - - /*! - * Refines the abstractor by making the given predicates new abstract predicates. - * - * @param newPredicateIndices The indices of the new predicates. - */ - void refine(std::vector const& newPredicateIndices); - - /*! - * Constraints the abstract states with the given BDD. - * - * @param newConstraint The BDD used as the constraint. - */ - void constrain(storm::dd::Bdd const& newConstraint); - - /*! - * Retrieves the set of abstract states matching all predicates added to this abstractor. - * - * @return The set of matching abstract states in the form of a BDD - */ - storm::dd::Bdd getAbstractStates(); - - private: - /*! - * Creates decision variables and the corresponding constraints for the missing predicates. - * - * @param newRelevantPredicateIndices The set of all relevant predicate indices. - */ - void addMissingPredicates(std::set const& newRelevantPredicateIndices); - - /*! - * Adds the current constraint BDD to the solver. - */ - void pushConstraintBdd(); - - /*! - * Removes the current constraint BDD (if any) from the solver. - */ - void popConstraintBdd(); - - /*! - * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. - */ - void recomputeCachedBdd(); - - /*! - * Translates the given model to a state DD. - * - * @param model The model to translate. - * @return The state encoded as a DD. - */ - storm::dd::Bdd getStateBdd(storm::solver::SmtSolver::ModelReference const& model) 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 local expression-related information. - LocalExpressionInformation localExpressionInformation; - - // The set of relevant predicates and the corresponding decision variables. - std::vector> relevantPredicatesAndVariables; - - // The set of all variables appearing in the concrete predicates. - std::set concretePredicateVariables; - - // The set of all decision variables over which to perform the all-sat enumeration. - std::vector decisionVariables; - - // A flag indicating whether the cached BDD needs recomputation. - bool needsRecomputation; - - // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work - // needed to be done). - storm::dd::Bdd cachedBdd; - - // This BDD currently constrains the search for solutions. - storm::dd::Bdd constraint; - }; - } - } -} - -#endif /* STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ */ diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index ad6489c86..f23949a8c 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -5,7 +5,7 @@ #include "src/parser/PrismParser.h" -#include "src/storage/prism/menu_games/AbstractProgram.h" +#include "src/abstraction/prism/AbstractProgram.h" #include "src/storage/expressions/Expression.h" @@ -24,9 +24,9 @@ TEST(PrismMenuGame, DieAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(10, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); @@ -41,11 +41,11 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)})); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(10, game.getNumberOfTransitions()); EXPECT_EQ(3, game.getNumberOfStates()); @@ -75,9 +75,9 @@ TEST(PrismMenuGame, DieFullAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(20, game.getNumberOfTransitions()); EXPECT_EQ(13, game.getNumberOfStates()); @@ -93,9 +93,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(11, game.getNumberOfTransitions()); EXPECT_EQ(2, game.getNumberOfStates()); @@ -111,11 +111,11 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")})); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(28, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -185,9 +185,9 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); @@ -205,9 +205,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(34, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -225,11 +225,11 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3)); initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)})); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(164, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -278,9 +278,9 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(436, game.getNumberOfTransitions()); EXPECT_EQ(169, game.getNumberOfStates()); @@ -299,9 +299,9 @@ TEST(PrismMenuGame, WlanAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(283, game.getNumberOfTransitions()); EXPECT_EQ(4, game.getNumberOfStates()); @@ -320,11 +320,11 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2")); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)})); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(568, game.getNumberOfTransitions()); EXPECT_EQ(8, game.getNumberOfStates()); @@ -441,9 +441,9 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); EXPECT_EQ(9503, game.getNumberOfTransitions()); EXPECT_EQ(5523, game.getNumberOfStates()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index cc60c5576..8f88c696a 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -193,7 +193,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { #ifdef STORM_HAVE_MSAT -#include "src/storage/prism/menu_games/AbstractProgram.h" +#include "src/abstraction/prism/AbstractProgram.h" #include "src/storage/expressions/Expression.h" @@ -207,9 +207,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); @@ -343,9 +343,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5)); initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. storm::dd::Bdd targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false); @@ -512,9 +512,9 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0)); initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1)); - storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); - storm::prism::menu_games::MenuGame game = abstractProgram.getAbstractGame(); + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); // The target states are those states where col == 2. storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false);