diff --git a/.gitignore b/.gitignore index 8d18b13b4..aa15c7b9a 100644 --- a/.gitignore +++ b/.gitignore @@ -33,6 +33,7 @@ resources/3rdparty/cudd-2.5.0/ ipch/ obj/ CMakeFiles/ +CPackConfig.cmake # The build Dir build/ build//CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 9d88dc762..e8b342aed 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -223,6 +223,13 @@ configure_file ( "${PROJECT_SOURCE_DIR}/storm-config.h.in" "${PROJECT_BINARY_DIR}/include/storm-config.h" ) + +# Configure a header file to pass the storm version to the source code +configure_file ( + "${PROJECT_SOURCE_DIR}/storm-version.h.in" + "${PROJECT_BINARY_DIR}/include/storm-version.h" +) + # Add the binary dir include directory for storm-config.h include_directories("${PROJECT_BINARY_DIR}/include") @@ -249,7 +256,8 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB_RECURSE STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) +file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp) @@ -282,6 +290,7 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) source_group(solver FILES ${STORM_SOLVER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) +source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) @@ -539,4 +548,4 @@ INSTALL(TARGETS storm storm-functional-tests storm-performance-tests LIBRARY DESTINATION lib ARCHIVE DESTINATION lib ) -include(CPackConfig.cmake) +include(StormCPackConfig.cmake) diff --git a/CPackConfig.cmake b/StormCPackConfig.cmake similarity index 100% rename from CPackConfig.cmake rename to StormCPackConfig.cmake diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a2932b9c9..f1ef50396 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -233,6 +233,13 @@ namespace storm { } std::set const& commandIndices = module.getCommandsByAction(action); + + // If the module contains the action, but there is no command in the module that is labeled with + // this action, we don't have any feasible command combinations. + if (commandIndices.empty()) { + return boost::optional>>(); + } + std::list commands; // Look up commands by their indices and add them if the guard evaluates to true in the given state. diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index be0729729..29ab6c613 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -157,7 +157,6 @@ private: for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); - bool initialValue = booleanVariable.getInitialValue()->getValueAsBool(nullptr); *initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]); } for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { @@ -187,7 +186,6 @@ private: } bool changed; - int iter = 0; do { changed = false; *newReachableStates = *reachableStates * *systemAdd01; diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 3ec8256ed..de9c6b057 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -169,7 +169,6 @@ namespace storm { * @return A mapping from labels to variable indices. */ static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { - int error = 0; std::stringstream variableNameBuffer; std::unordered_map resultingMap; for (auto const& label : relevantLabels) { @@ -190,7 +189,6 @@ namespace storm { * @return A mapping from states to a list of choice variable indices. */ static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map> resultingMap; @@ -219,7 +217,6 @@ namespace storm { * @return A mapping from initial states to choice variable indices. */ static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -245,7 +242,6 @@ namespace storm { * @return A mapping from states to the index of the corresponding probability variables. */ static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -269,7 +265,6 @@ namespace storm { * @return The index of the variable for the probability of the virtual initial state. */ static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver, bool maximizeProbability = false) { - int error = 0; std::stringstream variableNameBuffer; variableNameBuffer << "pinit"; @@ -285,7 +280,6 @@ namespace storm { * @return A mapping from problematic states to the index of the corresponding variables. */ static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -329,7 +323,6 @@ namespace storm { * @return A mapping from problematic choices to the index of the corresponding variables. */ static std::pair, uint_fast64_t, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, uint_fast64_t, PairHash> resultingMap; @@ -539,7 +532,6 @@ namespace storm { */ static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - int error = 0; for (auto state : stateInformation.relevantStates) { std::vector coefficients; std::vector variables; @@ -1021,7 +1013,7 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; } - bool strictBound = !probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS; + bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::property::ComparisonType::LESS); // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. double bound = probBoundFormula->getBound(); diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 6b67ee579..5724db8df 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -169,11 +169,16 @@ namespace storm { if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { return actionsCommandSetPair->second; } + LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module."); throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module."; } void Module::collectActions() { + // Clear the current mapping. + this->actionsToCommandIndexMap.clear(); + + // Add the mapping for all commands. for (unsigned int id = 0; id < this->commands.size(); id++) { std::string const& action = this->commands[id].getActionName(); if (action != "") { @@ -184,9 +189,18 @@ namespace storm { this->actions.insert(action); } } + + // For all actions that are "in the module", but for which no command exists, we add the mapping to an empty + // set of commands. + for (auto const& action : this->actions) { + if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { + this->actionsToCommandIndexMap[action] = std::set(); + } + } } void Module::restrictCommands(boost::container::flat_set const& indexSet) { + // First construct the new vector of commands. std::vector newCommands; for (auto const& command : commands) { if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { @@ -194,6 +208,9 @@ namespace storm { } } commands = std::move(newCommands); + + // Then refresh the internal mappings. + this->collectActions(); } } // namespace ir diff --git a/src/ir/Module.h b/src/ir/Module.h index e6762bb8d..d9570c652 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -188,8 +188,8 @@ namespace storm { * @param indexSet The set of indices for which to keep the commands. */ void restrictCommands(boost::container::flat_set const& indexSet); - private: + private: /*! * Computes the locally maintained mappings for fast data retrieval. */ @@ -217,11 +217,7 @@ namespace storm { std::set actions; // A map of actions to the set of commands labeled with this action. -#ifdef LINUX - boost::container::map> actionsToCommandIndexMap; -#else std::map> actionsToCommandIndexMap; -#endif }; } // namespace ir diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 1f9250c10..22b6ab13f 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -123,7 +123,7 @@ namespace storm { } // Then compute how many rows the new matrix is going to have. - uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; + //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates() + 1); diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index e343526f2..e122fcb16 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -110,8 +110,6 @@ namespace storm { glp_set_row_name(this->lp, nextConstraintIndex, name.c_str()); // Determine the type of the constraint and add it properly. - bool isUpperBound = boundType == LESS || boundType == LESS_EQUAL; - bool isStrict = boundType == LESS || boundType == GREATER; switch (boundType) { case LESS: glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index f81f4267a..c7ef52247 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -152,7 +152,6 @@ namespace storm { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index 29829f535..1b408d740 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp @@ -59,7 +59,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index d55b4e2e5..d26ad0344 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -106,7 +106,6 @@ namespace storm { void NativeLinearEquationSolver::performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp index 5dc25f2c1..7f88258f1 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/src/solver/NativeNondeterministicLinearEquationSolver.cpp @@ -54,7 +54,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index b4b282e0b..6907c45be 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -200,7 +200,6 @@ namespace storm { } BitVector& BitVector::operator&=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { @@ -224,7 +223,6 @@ namespace storm { } BitVector& BitVector::operator|=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 28fa2dc5b..95bc8e129 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -753,7 +753,6 @@ namespace storm { const_iterator it = this->begin(); const_iterator ite; typename std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::const_iterator rowIteratorEnd = rowIndications.end(); typename std::vector::iterator resultIterator = result.begin(); typename std::vector::iterator resultIteratorEnd = result.end(); diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp new file mode 100644 index 000000000..eba51a557 --- /dev/null +++ b/src/storage/dd/CuddDd.cpp @@ -0,0 +1,354 @@ +#include + +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddDdManager.h" + +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace dd { + Dd::Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) { + // Intentionally left empty. + } + + bool Dd::operator==(Dd const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); + } + + Dd Dd::operator+(Dd const& other) const { + Dd result(*this); + result += other; + return result; + } + + Dd& Dd::operator+=(Dd const& other) { + this->getCuddAdd() += other.getCuddAdd(); + + // Join the variable sets of the two participating DDs. + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return *this; + } + + Dd Dd::operator*(Dd const& other) const { + Dd result(*this); + result *= other; + return result; + } + + Dd& Dd::operator*=(Dd const& other) { + this->getCuddAdd() *= other.getCuddAdd(); + + // Join the variable sets of the two participating DDs. + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return *this; + } + + Dd Dd::operator-(Dd const& other) const { + Dd result(*this); + result -= other; + return result; + } + + Dd& Dd::operator-=(Dd const& other) { + this->getCuddAdd() -= other.getCuddAdd(); + + // Join the variable sets of the two participating DDs. + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return *this; + } + + Dd Dd::operator/(Dd const& other) const { + Dd result(*this); + result /= other; + return result; + } + + Dd& Dd::operator/=(Dd const& other) { + this->getCuddAdd().Divide(other.getCuddAdd()); + + // Join the variable sets of the two participating DDs. + this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return *this; + } + + Dd Dd::operator~() const { + Dd result(*this); + result.complement(); + return result; + } + + Dd& Dd::complement() { + this->getCuddAdd() = ~this->getCuddAdd(); + return *this; + } + + Dd Dd::equals(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().Equals(other.getCuddAdd()); + return result; + } + + Dd Dd::notEquals(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().NotEquals(other.getCuddAdd()); + return result; + } + + Dd Dd::less(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().LessThan(other.getCuddAdd()); + return result; + } + + Dd Dd::lessOrEqual(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().LessThanOrEqual(other.getCuddAdd()); + return result; + } + + Dd Dd::greater(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().GreaterThan(other.getCuddAdd()); + return result; + } + + Dd Dd::greaterOrEqual(Dd const& other) const { + Dd result(*this); + result.getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()); + return result; + } + + void Dd::existsAbstract(std::set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd()); + } + + void Dd::sumAbstract(std::set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd()); + } + + void Dd::minAbstract(std::set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().Minimum(cubeDd.getCuddAdd()); + } + + void Dd::maxAbstract(std::set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->getCuddAdd().Maximum(cubeDd.getCuddAdd()); + } + + void Dd::swapVariables(std::vector> const& metaVariablePairs) { + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { + throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; + } + + // Keep track of the contained meta variables in the DD. + bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); + bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); + if (containsVariable1 && !containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.first); + this->addContainedMetaVariable(metaVariablePair.second); + } else if (!containsVariable1 && containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.second); + this->addContainedMetaVariable(metaVariablePair.first); + } + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.getCuddAdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.getCuddAdd()); + } + } + + // Finally, call CUDD to swap the variables. + this->getCuddAdd().SwapVariables(from, to); + } + + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + std::vector summationDdVariables; + + // Create the CUDD summation variables. + for (auto const& metaVariableName : summationMetaVariableNames) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariableName).getDdVariables()) { + summationDdVariables.push_back(ddVariable.getCuddAdd()); + } + } + + std::set unionOfMetaVariableNames; + std::set_union(this->getContainedMetaVariableNames().begin(), this->getContainedMetaVariableNames().end(), otherMatrix.getContainedMetaVariableNames().begin(), otherMatrix.getContainedMetaVariableNames().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); + std::set containedMetaVariableNames; + std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); + + return Dd(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); + } + + + uint_fast64_t Dd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariableName : this->containedMetaVariableNames) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables(); + } + return static_cast(this->cuddAdd.CountMinterm(static_cast(numberOfDdVariables))); + } + + uint_fast64_t Dd::getLeafCount() const { + return static_cast(this->cuddAdd.CountLeaves()); + } + + uint_fast64_t Dd::getNodeCount() const { + return static_cast(this->cuddAdd.nodeCount()); + } + + double Dd::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); + return static_cast(Cudd_V(constantMinAdd.getNode())); + } + + double Dd::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); + return static_cast(Cudd_V(constantMaxAdd.getNode())); + } + + void Dd::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) { + std::unordered_map metaVariableNameToValueMap; + metaVariableNameToValueMap.emplace(metaVariableName, variableValue); + this->setValue(metaVariableNameToValueMap, targetValue); + } + + void Dd::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) { + std::unordered_map metaVariableNameToValueMap; + metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1); + metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2); + this->setValue(metaVariableNameToValueMap, targetValue); + } + + void Dd::setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue) { + Dd valueEncoding(this->getDdManager()->getOne()); + for (auto const& nameValuePair : metaVariableNameToValueMap) { + valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + } + + this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); + } + + bool Dd::isOne() const { + return *this == this->getDdManager()->getOne(); + } + + bool Dd::isZero() const { + return *this == this->getDdManager()->getZero(); + } + + bool Dd::containsMetaVariable(std::string const& metaVariableName) const { + auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); + return metaVariable != containedMetaVariableNames.end(); + } + + bool Dd::containsMetaVariables(std::set metaVariableNames) const { + for (auto const& metaVariableName : metaVariableNames) { + auto const& metaVariable = containedMetaVariableNames.find(metaVariableName); + + if (metaVariable == containedMetaVariableNames.end()) { + return false; + } + } + return true; + } + + std::set const& Dd::getContainedMetaVariableNames() const { + return this->containedMetaVariableNames; + } + + std::set& Dd::getContainedMetaVariableNames() { + return this->containedMetaVariableNames; + } + + void Dd::exportToDot(std::string const& filename) const { + FILE* filePointer = fopen(filename.c_str() , "w"); + this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer); + fclose(filePointer); + } + + ADD Dd::getCuddAdd() { + return this->cuddAdd; + } + + ADD const& Dd::getCuddAdd() const { + return this->cuddAdd; + } + + void Dd::addContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().insert(metaVariableName); + } + + void Dd::removeContainedMetaVariable(std::string const& metaVariableName) { + this->getContainedMetaVariableNames().erase(metaVariableName); + } + + std::shared_ptr> Dd::getDdManager() const { + return this->ddManager; + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h new file mode 100644 index 000000000..1f8339fe6 --- /dev/null +++ b/src/storage/dd/CuddDd.h @@ -0,0 +1,407 @@ +#ifndef STORM_STORAGE_DD_CUDDDD_H_ +#define STORM_STORAGE_DD_CUDDDD_H_ + +#include +#include +#include + +#include "src/storage/dd/Dd.h" +#include "src/utility/OsDetection.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + // Forward-declare the DdManager class. + template class DdManager; + + template<> + class Dd { + public: + // Declare the DdManager class as friend so it can access the internals of a DD. + friend class DdManager; + + // Instantiate all copy/move constructors/assignments with the default implementation. + Dd() = default; + Dd(Dd const& other) = default; + Dd& operator=(Dd const& other) = default; +#ifndef WINDOWS + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; +#endif + + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + */ + bool operator==(Dd const& other) const; + + /*! + * Adds the two DDs. + * + * @param other The DD to add to the current one. + * @return The result of the addition. + */ + Dd operator+(Dd const& other) const; + + /*! + * Adds the given DD to the current one. + * + * @param other The DD to add to the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator+=(Dd const& other); + + /*! + * Multiplies the two DDs. + * + * @param other The DD to multiply with the current one. + * @return The result of the multiplication. + */ + Dd operator*(Dd const& other) const; + + /*! + * Multiplies the given DD with the current one and assigns the result to the current DD. + * + * @param other The DD to multiply with the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator*=(Dd const& other); + + /*! + * Subtracts the given DD from the current one. + * + * @param other The DD to subtract from the current one. + * @return The result of the subtraction. + */ + Dd operator-(Dd const& other) const; + + /*! + * Subtracts the given DD from the current one and assigns the result to the current DD. + * + * @param other The DD to subtract from the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator-=(Dd const& other); + + /*! + * Divides the current DD by the given one. + * + * @param other The DD by which to divide the current one. + * @return The result of the division. + */ + Dd operator/(Dd const& other) const; + + /*! + * Divides the current DD by the given one and assigns the result to the current DD. + * + * @param other The DD by which to divide the current one. + * @return A reference to the current DD after the operation. + */ + Dd& operator/=(Dd const& other); + + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd minus() const; + + /*! + * Retrieves the logical complement of the current DD. The result will map all encodings with a value + * unequal to zero to false and all others to true. + * + * @return The logical complement of the current DD. + */ + Dd operator~() const; + + /*! + * Logically complements the current DD. The result will map all encodings with a value + * unequal to zero to false and all others to true. + * + * @return A reference to the current DD after the operation. + */ + Dd& complement(); + + /*! + * Retrieves the function that maps all evaluations to one that have an identical function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd equals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd notEquals(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd less(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or + * equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd lessOrEqual(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd greater(Dd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater + * or equal than the one in the given DD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd greaterOrEqual(Dd const& other) const; + + /*! + * Existentially abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void existsAbstract(std::set const& metaVariableNames); + + /*! + * Sum-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void sumAbstract(std::set const& metaVariableNames); + + /*! + * Min-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void minAbstract(std::set const& metaVariableNames); + + /*! + * Max-abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void maxAbstract(std::set const& metaVariableNames); + + /*! + * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have + * the same number of underlying DD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + */ + void swapVariables(std::vector> const& metaVariablePairs); + + /*! + * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariableNames The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return A DD representing the result of the matrix-matrix multiplication. + */ + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + uint_fast64_t getNonZeroCount() const; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + uint_fast64_t getNodeCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + double getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + double getMax() const; + + /*! + * Sets the function values of all encodings that have the given value of the meta variable to the given + * target value. + * + * @param metaVariableName The name of the meta variable that has to be equal to the given value. + * @param variableValue The value that the meta variable is supposed to have. This must be within the range + * of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the two meta variables to the + * given target value. + * + * @param metaVariableName1 The name of the first meta variable that has to be equal to the first given + * value. + * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the + * range of the meta variable. + * @param metaVariableName2 The name of the first meta variable that has to be equal to the second given + * value. + * @param variableValue2 The value that the second meta variable is supposed to have. This must be within + * the range of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the given meta variables to the + * given target value. + * + * @param metaVariableNameToValueMap A mapping of meta variable names to the values they are supposed to + * have. All values must be within the range of the respective meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::unordered_map const& metaVariableNameToValueMap, double targetValue); + + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Retrieves whether the given meta variable is contained in the DD. + * + * @param metaVariableName The name of the meta variable for which to query membership. + * @return True iff the meta variable is contained in the DD. + */ + bool containsMetaVariable(std::string const& metaVariableName) const; + + /*! + * Retrieves whether the given meta variables are all contained in the DD. + * + * @param metaVariableNames The names of the meta variable for which to query membership. + * @return True iff all meta variables are contained in the DD. + */ + bool containsMetaVariables(std::set metaVariableNames) const; + + /*! + * Retrieves the set of all names of meta variables contained in the DD. + * + * @return The set of names of all meta variables contained in the DD. + */ + std::set const& getContainedMetaVariableNames() const; + + /*! + * Retrieves the set of all names of meta variables contained in the DD. + * + * @return The set of names of all meta variables contained in the DD. + */ + std::set& getContainedMetaVariableNames(); + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToDot(std::string const& filename) const; + + /*! + * Retrieves the manager that is responsible for this DD. + * + * A pointer to the manager that is responsible for this DD. + */ + std::shared_ptr> getDdManager() const; + + private: + /*! + * Retrieves the CUDD ADD object associated with this DD. + * + * @return The CUDD ADD object assoicated with this DD. + */ + ADD getCuddAdd(); + + /*! + * Retrieves the CUDD ADD object associated with this DD. + * + * @return The CUDD ADD object assoicated with this DD. + */ + ADD const& getCuddAdd() const; + + /*! + * Adds the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to add. + */ + void addContainedMetaVariable(std::string const& metaVariableName); + + /*! + * Removes the given meta variable name to the set of meta variables that are contained in this DD. + * + * @param metaVariableName The name of the meta variable to remove. + */ + void removeContainedMetaVariable(std::string const& metaVariableName); + + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddAdd The CUDD ADD to store. + * @param + */ + Dd(std::shared_ptr> ddManager, ADD cuddAdd, std::set const& containedMetaVariableNames = std::set()); + + // A pointer to the manager responsible for this DD. + std::shared_ptr> ddManager; + + // The ADD created by CUDD. + ADD cuddAdd; + + // The names of all meta variables that appear in this DD. + std::set containedMetaVariableNames; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp new file mode 100644 index 000000000..dd6ce4f4f --- /dev/null +++ b/src/storage/dd/CuddDdManager.cpp @@ -0,0 +1,149 @@ +#include +#include + +#include "src/storage/dd/CuddDdManager.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include + +namespace storm { + namespace dd { + DdManager::DdManager() : metaVariableMap(), cuddManager() { + // Intentionally left empty. + } + + Dd DdManager::getOne() { + return Dd(this->shared_from_this(), cuddManager.addOne()); + } + + Dd DdManager::getZero() { + return Dd(this->shared_from_this(), cuddManager.addZero()); + } + + Dd DdManager::getConstant(double value) { + return Dd(this->shared_from_this(), cuddManager.constant(value)); + } + + Dd DdManager::getEncoding(std::string const& metaVariableName, int_fast64_t value) { + std::vector> ddVariables = this->getMetaVariable(metaVariableName).getDdVariables(); + + Dd result; + if (value & (1ull << (ddVariables.size() - 1))) { + result = ddVariables[0]; + } else { + result = ddVariables[0]; + } + + for (std::size_t i = 1; i < ddVariables.size(); ++i) { + if (value & (1ull << (ddVariables.size() - i - 1))) { + result *= ddVariables[i]; + } else { + result *= ~ddVariables[i]; + } + } + + return result; + } + + Dd DdManager::getRange(std::string const metaVariableName) { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(metaVariableName); + + Dd result = this->getZero(); + for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { + result.setValue(metaVariableName, value - metaVariable.getLow(), static_cast(value)); + } + return result; + } + + void DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { + // Check whether a meta variable already exists. + if (this->hasMetaVariable(name)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists."; + } + + // Check that the range is legal. + if (high == low) { + throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; + } + + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); + + std::vector> variables; + for (std::size_t i = 0; i < numberOfBits; ++i) { + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {name})); + } + + metaVariableMap.emplace(name, DdMetaVariable(name, low, high, variables, this->shared_from_this())); + } + + void DdManager::addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high) { + // Make sure that at least one meta variable is added. + if (names.size() == 0) { + throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables."; + } + + // Check that there are no duplicate names in the given name vector. + std::vector nameCopy(names); + std::sort(nameCopy.begin(), nameCopy.end()); + if (std::adjacent_find(nameCopy.begin(), nameCopy.end()) != nameCopy.end()) { + throw storm::exceptions::InvalidArgumentException() << "Cannot add duplicate meta variables."; + } + + // Check that the range is legal. + if (high == low) { + throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements."; + } + + // Check whether a meta variable already exists. + for (auto const& metaVariableName : names) { + if (this->hasMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists."; + } + } + + // Add the variables in interleaved order. + std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); + std::vector>> variables(names.size()); + for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) { + for (uint_fast64_t i = 0; i < names.size(); ++i) { + variables[i].emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {names[i]})); + } + } + + // Now add the meta variables. + for (uint_fast64_t i = 0; i < names.size(); ++i) { + metaVariableMap.emplace(names[i], DdMetaVariable(names[i], low, high, variables[i], this->shared_from_this())); + } + } + + DdMetaVariable const& DdManager::getMetaVariable(std::string const& metaVariableName) const { + auto const& nameVariablePair = metaVariableMap.find(metaVariableName); + + if (!this->hasMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name."; + } + + return nameVariablePair->second; + } + + std::set DdManager::getAllMetaVariableNames() const { + std::set result; + for (auto const& nameValuePair : metaVariableMap) { + result.insert(nameValuePair.first); + } + return result; + } + + std::size_t DdManager::getNumberOfMetaVariables() const { + return this->metaVariableMap.size(); + } + + bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { + return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end(); + } + + Cudd& DdManager::getCuddManager() { + return this->cuddManager; + } + } +} \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h new file mode 100644 index 000000000..1d0d32a99 --- /dev/null +++ b/src/storage/dd/CuddDdManager.h @@ -0,0 +1,141 @@ +#ifndef STORM_STORAGE_DD_CUDDDDMANAGER_H_ +#define STORM_STORAGE_DD_CUDDDDMANAGER_H_ + +#include + +#include "src/storage/dd/DdManager.h" +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/CuddDd.h" +#include "src/utility/OsDetection.h" + +// Include the C++-interface of CUDD. +#include "cuddObj.hh" + +namespace storm { + namespace dd { + template<> + class DdManager : public std::enable_shared_from_this> { + public: + // To break the cylic dependencies, we need to forward-declare the other DD-related classes. + friend class Dd; + + /*! + * Creates an empty manager without any meta variables. + */ + DdManager(); + + // Explictly forbid copying a DdManager, but allow moving it. + DdManager(DdManager const& other) = delete; + DdManager& operator=(DdManager const& other) = delete; +#ifndef WINDOWS + DdManager(DdManager&& other) = default; + DdManager& operator=(DdManager&& other) = default; +#endif + + /*! + * Retrieves a DD representing the constant one function. + * + * @return A DD representing the constant one function. + */ + Dd getOne(); + + /*! + * Retrieves a DD representing the constant zero function. + * + * @return A DD representing the constant zero function. + */ + Dd getZero(); + + /*! + * Retrieves a DD representing the constant function with the given value. + * + * @return A DD representing the constant function with the given value. + */ + Dd getConstant(double value); + + /*! + * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + * + * @param metaVariableName The meta variable that is supposed to have the given value. + * @param value The value the meta variable is supposed to have. + * @return The DD representing the function that maps all inputs which have the given meta variable equal + * to the given value one. + */ + Dd getEncoding(std::string const& metaVariableName, int_fast64_t value); + + /*! + * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values + * of the range of the meta variable to one. + * + * @param metaVariableName The name of the meta variable whose range to retrieve. + * @return The range of the meta variable + */ + Dd getRange(std::string const metaVariableName); + + /*! + * Adds a meta variable with the given name and range. + * + * @param name The name of the meta variable. + * @param low The lowest value of the range of the variable. + * @param high The highest value of the range of the variable. + */ + void addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high); + + /*! + * Adds meta variables with the given names and (equal) range and arranges the DD variables in an interleaved order. + * + * @param names The names of the variables. + * @param low The lowest value of the ranges of the variables. + * @param high The highest value of the ranges of the variables. + */ + void addMetaVariablesInterleaved(std::vector const& names, int_fast64_t low, int_fast64_t high); + + /*! + * Retrieves the meta variable with the given name if it exists. + * + * @param metaVariableName The name of the meta variable to retrieve. + * @return The meta variable with the given name. + */ + DdMetaVariable const& getMetaVariable(std::string const& metaVariableName) const; + + /*! + * Retrieves the names of all meta variables that have been added to the manager. + * + * @return The set of all meta variable names of the manager. + */ + std::set getAllMetaVariableNames() const; + + /*! + * Retrieves the number of meta variables that are contained in this manager. + * + * @return The number of meta variables contained in this manager. + */ + std::size_t getNumberOfMetaVariables() const; + + /*! + * Retrieves whether the given meta variable name is already in use. + * + * @param metaVariableName The meta variable name whose membership to query. + * @return True if the given meta variable name is managed by this manager. + */ + bool hasMetaVariable(std::string const& metaVariableName) const; + + private: + /*! + * Retrieves the underlying CUDD manager. + * + * @return The underlying CUDD manager. + */ + Cudd& getCuddManager(); + + // A mapping from variable names to the meta variable information. + std::unordered_map> metaVariableMap; + + // The manager responsible for the DDs created/modified with this DdManager. + Cudd cuddManager; + }; + } +} + +#endif /* STORM_STORAGE_DD_CUDDDDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h new file mode 100644 index 000000000..bc7075f46 --- /dev/null +++ b/src/storage/dd/Dd.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DD_H_ +#define STORM_STORAGE_DD_DD_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare Dd class so we can then specialize it for the different DD types. + template class Dd; + } +} + +#endif /* STORM_STORAGE_DD_DD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h new file mode 100644 index 000000000..53fde64bb --- /dev/null +++ b/src/storage/dd/DdManager.h @@ -0,0 +1,13 @@ +#ifndef STORM_STORAGE_DD_DDMANAGER_H_ +#define STORM_STORAGE_DD_DDMANAGER_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + // Declare DdManager class so we can then specialize it for the different DD types. + template class DdManager; + } +} + +#endif /* STORM_STORAGE_DD_DDMANAGER_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp new file mode 100644 index 000000000..7671289fc --- /dev/null +++ b/src/storage/dd/DdMetaVariable.cpp @@ -0,0 +1,52 @@ +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/CuddDdManager.h" + +namespace storm { + namespace dd { + template + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + // Create the cube of all variables of this meta variable. + for (auto const& ddVariable : this->ddVariables) { + this->cube *= ddVariable; + } + } + + template + std::string const& DdMetaVariable::getName() const { + return this->name; + } + + template + int_fast64_t DdMetaVariable::getLow() const { + return this->low; + } + + template + int_fast64_t DdMetaVariable::getHigh() const { + return this->high; + } + + template + std::size_t DdMetaVariable::getNumberOfDdVariables() const { + return this->ddVariables.size(); + } + + template + std::shared_ptr> DdMetaVariable::getDdManager() const { + return this->manager; + } + + template + std::vector> const& DdMetaVariable::getDdVariables() const { + return this->ddVariables; + } + + template + Dd const& DdMetaVariable::getCube() const { + return this->cube; + } + + // Explicitly instantiate DdMetaVariable. + template class DdMetaVariable; + } +} \ No newline at end of file diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h new file mode 100644 index 000000000..f6c90cc21 --- /dev/null +++ b/src/storage/dd/DdMetaVariable.h @@ -0,0 +1,114 @@ +#ifndef STORM_STORAGE_DD_DDMETAVARIABLE_H_ +#define STORM_STORAGE_DD_DDMETAVARIABLE_H_ + +#include +#include +#include +#include + +#include "utility/OsDetection.h" +#include "src/storage/dd/CuddDd.h" + +namespace storm { + namespace dd { + // Forward-declare the DdManager class. + template class DdManager; + + template + class DdMetaVariable { + public: + // Declare the DdManager class as friend so it can access the internals of a meta variable. + friend class DdManager; + friend class Dd; + + /*! + * Creates a meta variable with the given name, range bounds. + * + * @param name The name of the meta variable. + * @param low The lowest value of the range of the variable. + * @param high The highest value of the range of the variable. + * @param ddVariables The vector of variables used to encode this variable. + * @param manager A pointer to the manager that is responsible for this meta variable. + */ + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); + + // Explictly generate all default versions of copy/move constructors/assignments. + DdMetaVariable(DdMetaVariable const& other) = default; + DdMetaVariable& operator=(DdMetaVariable const& other) = default; +#ifndef WINDOWS + DdMetaVariable(DdMetaVariable&& other) = default; + DdMetaVariable& operator=(DdMetaVariable&& other) = default; +#endif + + /*! + * Retrieves the name of the meta variable. + * + * @return The name of the variable. + */ + std::string const& getName() const; + + /*! + * Retrieves the lowest value of the range of the variable. + * + * @return The lowest value of the range of the variable. + */ + int_fast64_t getLow() const; + + /*! + * Retrieves the highest value of the range of the variable. + * + * @return The highest value of the range of the variable. + */ + int_fast64_t getHigh() const; + + /*! + * Retrieves the manager that is responsible for this meta variable. + * + * A pointer to the manager that is responsible for this meta variable. + */ + std::shared_ptr> getDdManager() const; + + /*! + * Retrieves the number of DD variables for this meta variable. + * + * @return The number of DD variables for this meta variable. + */ + std::size_t getNumberOfDdVariables() const; + + private: + /*! + * Retrieves the variables used to encode the meta variable. + * + * @return A vector of variables used to encode the meta variable. + */ + std::vector> const& getDdVariables() const; + + /*! + * Retrieves the cube of all variables that encode this meta variable. + * + * @return The cube of all variables that encode this meta variable. + */ + Dd const& getCube() const; + + // The name of the meta variable. + std::string name; + + // The lowest value of the range of the variable. + int_fast64_t low; + + // The highest value of the range of the variable. + int_fast64_t high; + + // The vector of variables that are used to encode the meta variable. + std::vector> ddVariables; + + // The cube consisting of all variables that encode the meta variable. + Dd cube; + + // A pointer to the manager responsible for this meta variable. + std::shared_ptr> manager; + }; + } +} + +#endif /* STORM_STORAGE_DD_DDMETAVARIABLE_H_ */ \ No newline at end of file diff --git a/src/storage/dd/DdType.h b/src/storage/dd/DdType.h new file mode 100644 index 000000000..327832ec5 --- /dev/null +++ b/src/storage/dd/DdType.h @@ -0,0 +1,12 @@ +#ifndef STORM_STORAGE_DD_DDTYPE_H_ +#define STORM_STORAGE_DD_DDTYPE_H_ + +namespace storm { + namespace dd { + enum DdType { + CUDD + }; + } +} + +#endif /* STORM_STORAGE_DD_DDTYPE_H_ */ diff --git a/src/storm.cpp b/src/storm.cpp index ef23b9f2f..a13bf8e23 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -21,6 +21,7 @@ #include #include "storm-config.h" +#include "storm-version.h" #include "src/models/Dtmc.h" #include "src/models/MarkovAutomaton.h" #include "src/storage/SparseMatrix.h" @@ -240,7 +241,7 @@ void setUp() { * Performs some necessary clean-up. */ void cleanUp() { - delete storm::utility::cuddUtilityInstance(); + // Intentionally left empty. } /*! diff --git a/src/utility/vector.h b/src/utility/vector.h index dd3bb2a1f..82913a902 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -94,7 +94,6 @@ namespace storm { */ template void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; for (uint_fast64_t i = 0; i < vector.size(); ++i) { vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; } diff --git a/storm-config.h.in b/storm-config.h.in index cc6e63c41..5b577888d 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -8,13 +8,6 @@ #ifndef STORM_GENERATED_STORMCONFIG_H_ #define STORM_GENERATED_STORMCONFIG_H_ -// Version Information -#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ // The major version of StoRM -#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ // The minor version of StoRM -#define STORM_CPP_VERSION_PATCH @STORM_CPP_VERSION_PATCH@ // The patch version of StoRM -#define STORM_CPP_VERSION_COMMITS_AHEAD @STORM_CPP_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set -#define STORM_CPP_VERSION_HASH "@STORM_CPP_VERSION_HASH@" // The short hash of the git commit this build is bases on -#define STORM_CPP_VERSION_DIRTY @STORM_CPP_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else // The path of the sources from which StoRM will be/was build #define STORM_CPP_BASE_PATH "@PROJECT_SOURCE_DIR@" diff --git a/storm-version.h.in b/storm-version.h.in new file mode 100644 index 000000000..5ccac6125 --- /dev/null +++ b/storm-version.h.in @@ -0,0 +1,12 @@ +#ifndef STORM_GENERATED_VERSION_H_ +#define STORM_GENERATED_VERSION_H_ + +// Version Information +#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ // The major version of StoRM +#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ // The minor version of StoRM +#define STORM_CPP_VERSION_PATCH @STORM_CPP_VERSION_PATCH@ // The patch version of StoRM +#define STORM_CPP_VERSION_COMMITS_AHEAD @STORM_CPP_VERSION_COMMITS_AHEAD@ // How many commits passed since the tag was last set +#define STORM_CPP_VERSION_HASH "@STORM_CPP_VERSION_HASH@" // The short hash of the git commit this build is bases on +#define STORM_CPP_VERSION_DIRTY @STORM_CPP_VERSION_DIRTY@ // 0 iff there no files were modified in the checkout, 1 else + +#endif \ No newline at end of file diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp new file mode 100644 index 000000000..a92dbc929 --- /dev/null +++ b/test/functional/storage/CuddDdTest.cpp @@ -0,0 +1,71 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/DdMetaVariable.h" + +TEST(CuddDdManager, Constants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Dd zero; + ASSERT_NO_THROW(zero = manager->getZero()); + + EXPECT_EQ(0, zero.getNonZeroCount()); + EXPECT_EQ(1, zero.getLeafCount()); + EXPECT_EQ(1, zero.getNodeCount()); + EXPECT_EQ(0, zero.getMin()); + EXPECT_EQ(0, zero.getMax()); + + storm::dd::Dd one; + ASSERT_NO_THROW(one = manager->getOne()); + + EXPECT_EQ(1, one.getNonZeroCount()); + EXPECT_EQ(1, one.getLeafCount()); + EXPECT_EQ(1, one.getNodeCount()); + EXPECT_EQ(1, one.getMin()); + EXPECT_EQ(1, one.getMax()); + + storm::dd::Dd two; + ASSERT_NO_THROW(two = manager->getConstant(2)); + + EXPECT_EQ(1, two.getNonZeroCount()); + EXPECT_EQ(1, two.getLeafCount()); + EXPECT_EQ(1, two.getNodeCount()); + EXPECT_EQ(2, two.getMin()); + EXPECT_EQ(2, two.getMax()); +} + +TEST(CuddDdManager, MetaVariableTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + EXPECT_EQ(1, manager->getNumberOfMetaVariables()); + + std::vector names = {"x", "x'"}; + ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + + names = {"y", "y"}; + ASSERT_THROW(manager->addMetaVariablesInterleaved(names, 0, 3), storm::exceptions::InvalidArgumentException); + + names = {"y", "y'"}; + ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3)); + EXPECT_EQ(3, manager->getNumberOfMetaVariables()); + + EXPECT_FALSE(manager->hasMetaVariable("x'")); + EXPECT_TRUE(manager->hasMetaVariable("y'")); + + std::set metaVariableSet = {"x", "y", "y'"}; + EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); + + ASSERT_THROW(storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x")); + storm::dd::DdMetaVariable const& metaVariableX = manager->getMetaVariable("x"); + + EXPECT_EQ(1, metaVariableX.getLow()); + EXPECT_EQ(9, metaVariableX.getHigh()); + EXPECT_EQ("x", metaVariableX.getName()); + EXPECT_EQ(manager, metaVariableX.getDdManager()); + EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables()); +} +