diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index b5731a3f3..d975c8e9e 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -204,6 +204,7 @@ namespace storm { // Explicitly instantiate the symbolic expression adapter template class AddExpressionAdapter; template class AddExpressionAdapter; + #ifdef STORM_HAVE_CARL template class AddExpressionAdapter; #endif diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 94fda1882..c3d91b533 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -35,6 +35,8 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace builder { @@ -135,9 +137,9 @@ namespace storm { struct CompositionVariables { CompositionVariables() : manager(std::make_shared>()), variableToRowMetaVariableMap(std::make_shared>()), - rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), + rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), variableToColumnMetaVariableMap(std::make_shared>()), - columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)) { + columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)) { // Intentionally left empty. } @@ -146,12 +148,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; std::shared_ptr> variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -429,7 +431,7 @@ namespace storm { }; template - EdgeDestinationDd buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add const& guard, CompositionVariables const& variables) { + EdgeDestinationDd buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Bdd const& guard, CompositionVariables const& variables) { storm::dd::Add transitions = variables.rowExpressionAdapter->translateExpression(destination.getProbability()); STORM_LOG_TRACE("Translating edge destination."); @@ -449,11 +451,11 @@ namespace storm { storm::dd::Add assignedExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); // Combine the assigned expression with the guard. - storm::dd::Add result = assignedExpression * guard; + storm::dd::Add result = assignedExpression * guard.template toAdd(); // Combine the variable and the assigned expression. result = result.equals(writtenVariable).template toAdd(); - result *= guard; + result *= guard.template toAdd(); // Restrict the transitions to the range of the written variable. result = result * variables.variableToRangeMap.at(primedMetaVariable).template toAdd(); @@ -515,7 +517,7 @@ namespace storm { } } - result.setValue(metaVariableNameToValueMap, 1); + result.setValue(metaVariableNameToValueMap, storm::utility::one()); return result; } @@ -524,15 +526,15 @@ namespace storm { public: // This structure represents an edge. struct EdgeDd { - EdgeDd(bool isMarkovian, storm::dd::Add const& guard, storm::dd::Add const& transitions, std::map> const& transientEdgeAssignments, std::set const& writtenGlobalVariables) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment() { + EdgeDd(bool isMarkovian, storm::dd::Bdd const& guard, storm::dd::Add const& transitions, std::map> const& transientEdgeAssignments, std::set const& writtenGlobalVariables) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment() { // Convert the set of written variables to a mapping from variable to the writing fragments. for (auto const& variable : writtenGlobalVariables) { - variableToWritingFragment[variable] = guard.toBdd(); + variableToWritingFragment[variable] = guard; } } - EdgeDd(bool isMarkovian, storm::dd::Add const& guard, storm::dd::Add const& transitions, std::map> const& transientEdgeAssignments, std::map> const& variableToWritingFragment) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment(variableToWritingFragment) { + EdgeDd(bool isMarkovian, storm::dd::Bdd const& guard, storm::dd::Add const& transitions, std::map> const& transientEdgeAssignments, std::map> const& variableToWritingFragment) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment(variableToWritingFragment) { // Intentionally left empty. } @@ -540,7 +542,7 @@ namespace storm { bool isMarkovian; // A DD that represents all states that have this edge enabled. - storm::dd::Add guard; + storm::dd::Bdd guard; // A DD that represents the transitions of this edge. storm::dd::Add transitions; @@ -554,7 +556,7 @@ namespace storm { // This structure represents an edge. struct ActionDd { - ActionDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientEdgeAssignments = {}, std::pair localNondeterminismVariables = std::pair(0, 0), std::map> const& variableToWritingFragment = {}, storm::dd::Bdd const& illegalFragment = storm::dd::Bdd()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) { + ActionDd(storm::dd::Bdd const& guard = storm::dd::Bdd(), storm::dd::Add const& transitions = storm::dd::Add(), std::map> const& transientEdgeAssignments = {}, std::pair localNondeterminismVariables = std::pair(0, 0), std::map> const& variableToWritingFragment = {}, storm::dd::Bdd const& illegalFragment = storm::dd::Bdd()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) { // Intentionally left empty. } @@ -583,7 +585,7 @@ namespace storm { } // A DD that represents all states that have this edge enabled. - storm::dd::Add guard; + storm::dd::Bdd guard; // A DD that represents the transitions of this edge. storm::dd::Add transitions; @@ -909,9 +911,8 @@ namespace storm { for (auto const& actionIndexPair : actions) { auto componentIndex = actionIndexPair.first; auto const& action = actionIndexPair.second.get(); - storm::dd::Bdd actionGuard = action.guard.toBdd(); if (guardDisjunction) { - guardDisjunction.get() |= actionGuard; + guardDisjunction.get() |= action.guard; } lowestNondeterminismVariable = std::min(lowestNondeterminismVariable, action.getLowestLocalNondeterminismVariable()); @@ -920,7 +921,7 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. - transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity); + transitions *= action.guard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity); } else { transitions *= action.transitions; } @@ -956,12 +957,12 @@ namespace storm { // guard of the current action if the current action is not input enabled. for (auto& entry : globalVariableToWritingFragment) { if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end() && !action.isInputEnabled()) { - entry.second &= actionGuard; + entry.second &= action.guard; } } if (!action.isInputEnabled()) { - inputEnabledGuard &= actionGuard; + inputEnabledGuard &= action.guard; } } @@ -976,7 +977,7 @@ namespace storm { // such a combined transition. illegalFragment &= inputEnabledGuard; - return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); + return ActionDd(inputEnabledGuard, transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -1001,7 +1002,7 @@ namespace storm { ActionDd result(*actionIt); for (++actionIt; actionIt != actions.end(); ++actionIt) { - result = ActionDd(result.guard + actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment); + result = ActionDd(result.guard || actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment); } return result; } else if (this->model.getModelType() == storm::jani::ModelType::MDP) { @@ -1041,7 +1042,7 @@ namespace storm { for (uint64_t actionIndex = 0; actionIndex < actions.size(); ++actionIndex) { ActionDd& action = actions[actionIndex]; - guard |= action.guard.toBdd(); + guard |= action.guard; storm::dd::Add nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables); transitions += nondeterminismEncoding * action.transitions; @@ -1056,7 +1057,7 @@ namespace storm { illegalFragment |= action.illegalFragment; } - return ActionDd(guard.template toAdd(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment); + return ActionDd(guard, transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } @@ -1084,8 +1085,8 @@ namespace storm { // We keep the guard and a "ranged" version seperate, because building the destinations tends to be // slower when the full range is applied. - storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()); - storm::dd::Add rangedGuard = guard * this->variables.automatonToRangeMap.at(automaton.getName()); + storm::dd::Bdd guard = this->variables.rowExpressionAdapter->translateBooleanExpression(edge.getGuard()); + storm::dd::Bdd rangedGuard = guard && this->variables.automatonToRangeMap.at(automaton.getName()).toBdd(); STORM_LOG_WARN_COND(!rangedGuard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); if (!rangedGuard.isZero()) { @@ -1132,7 +1133,7 @@ namespace storm { } // Add the source location and the guard. - storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard.template toAdd(); transitions *= sourceLocationAndGuard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. @@ -1155,9 +1156,9 @@ namespace storm { } ); } - return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); + return EdgeDd(isMarkovian, guard, guard.template toAdd() * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); } else { - return EdgeDd(false, rangedGuard, rangedGuard, std::map>(), std::set()); + return EdgeDd(false, rangedGuard, rangedGuard.template toAdd(), std::map>(), std::set()); } } @@ -1172,10 +1173,10 @@ namespace storm { STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::WrongFormatException, "Can only combine Markovian edges."); if (!overlappingGuards) { - overlappingGuards |= !(guard && edge.guard.toBdd()).isZero(); + overlappingGuards |= !(guard && edge.guard).isZero(); } - guard |= edge.guard.toBdd(); + guard |= edge.guard; transitions += edge.transitions; variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment); joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments); @@ -1184,7 +1185,7 @@ namespace storm { // Currently, we can only combine the transient edge assignments if there is no overlap of the guards of the edges. STORM_LOG_THROW(!overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards."); - return EdgeDd(true, guard.template toAdd(), transitions, transientEdgeAssignments, variableToWritingFragment); + return EdgeDd(true, guard, transitions, transientEdgeAssignments, variableToWritingFragment); } ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) { @@ -1228,7 +1229,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of this type."); } } else { - return ActionDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); + return ActionDd(this->variables.manager->template getBddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); } } @@ -1279,14 +1280,13 @@ namespace storm { STORM_LOG_THROW((this->model.getModelType() == storm::jani::ModelType::CTMC) == edgeDd.isMarkovian, storm::exceptions::WrongFormatException, "Unexpected non-Markovian edge in CTMC."); // Check for overlapping guards. - storm::dd::Bdd guardBdd = edgeDd.guard.toBdd(); - overlappingGuards = !(guardBdd && allGuards).isZero(); + overlappingGuards = !(edgeDd.guard && allGuards).isZero(); // Issue a warning if there are overlapping guards in a DTMC. STORM_LOG_WARN_COND(!overlappingGuards || this->model.getModelType() == storm::jani::ModelType::CTMC, "Guard of an edge in a DTMC overlaps with previous guards."); // Add the elements of the current edge to the global ones. - allGuards |= guardBdd; + allGuards |= edgeDd.guard; allTransitions += edgeDd.transitions; // Add the transient variable assignments to the resulting one. This transformation is illegal for @@ -1300,7 +1300,7 @@ namespace storm { STORM_LOG_THROW(this->model.getModelType() == storm::jani::ModelType::DTMC || !overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards."); - return ActionDd(allGuards.template toAdd(), allTransitions, transientEdgeAssignments, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); + return ActionDd(allGuards, allTransitions, transientEdgeAssignments, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } void addToVariableWritingFragmentMap(std::map>& globalVariableToWritingFragment, storm::expressions::Variable const& variable, storm::dd::Bdd const& partToAdd) const { @@ -1333,7 +1333,7 @@ namespace storm { return result; } - ActionDd combineEdgesBySummation(storm::dd::Add const& guard, std::vector const& edges, boost::optional const& markovianEdge) { + ActionDd combineEdgesBySummation(storm::dd::Bdd const& guard, std::vector const& edges, boost::optional const& markovianEdge) { bool addMarkovianFlag = this->model.getModelType() == storm::jani::ModelType::MA; STORM_LOG_ASSERT(addMarkovianFlag || !markovianEdge, "Illegally adding Markovian edge without marker."); @@ -1374,18 +1374,18 @@ namespace storm { ActionDd combineEdgesToActionNondeterministic(std::vector const& nonMarkovianEdges, boost::optional const& markovianEdge, uint64_t localNondeterminismVariableOffset) { // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. storm::dd::Bdd allGuards = this->variables.manager->getBddZero(); - storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); + storm::dd::Add sumOfGuards = this->variables.manager->template getAddZero(); for (auto const& edge : nonMarkovianEdges) { STORM_LOG_ASSERT(!edge.isMarkovian, "Unexpected Markovian edge."); - sumOfGuards += edge.guard; - allGuards |= edge.guard.toBdd(); + sumOfGuards += edge.guard.template toAdd(); + allGuards |= edge.guard; } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); + uint_fast64_t maxChoices = sumOfGuards.getMax(); STORM_LOG_TRACE("Found " << maxChoices << " non-Markovian local choices."); // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. if (maxChoices <= 1) { - return combineEdgesBySummation(allGuards.template toAdd(), nonMarkovianEdges, markovianEdge); + return combineEdgesBySummation(allGuards, nonMarkovianEdges, markovianEdge); } else { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); @@ -1405,7 +1405,7 @@ namespace storm { for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast(currentChoices))); + equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(currentChoices)); // If there is no such state, continue with the next possible number of choices. if (equalsNumberOfChoicesDd.isZero()) { @@ -1423,7 +1423,7 @@ namespace storm { // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices // choices such that one outgoing choice is given by the j-th edge. - storm::dd::Bdd guardChoicesIntersection = currentEdge.guard.toBdd() && equalsNumberOfChoicesDd; + storm::dd::Bdd guardChoicesIntersection = currentEdge.guard && equalsNumberOfChoicesDd; // If there is no such state, continue with the next command. if (guardChoicesIntersection.isZero()) { @@ -1470,7 +1470,7 @@ namespace storm { } // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } // Extend the transitions with the appropriate flag if needed. @@ -1503,7 +1503,7 @@ namespace storm { } } - return ActionDd(allGuards.template toAdd(), allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero()); + return ActionDd(allGuards, allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } } @@ -1633,11 +1633,11 @@ namespace storm { std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { if (modelType == storm::jani::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); + return std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else if (modelType == storm::jani::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); + return std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else if (modelType == storm::jani::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); + return std::make_shared>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); } @@ -1927,5 +1927,7 @@ namespace storm { template class DdJaniModelBuilder; template class DdJaniModelBuilder; + + template class DdJaniModelBuilder; } } diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index e2afeeae6..a8481e21b 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -26,6 +26,8 @@ #include "storm/settings/modules/CoreSettings.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace builder { @@ -786,7 +788,7 @@ namespace storm { } } - result.setValue(metaVariableNameToValueMap, ValueType(1)); + result.setValue(metaVariableNameToValueMap, storm::utility::one()); return result; } @@ -799,12 +801,12 @@ namespace storm { std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = generationInfo.manager->template getAddZero(); + storm::dd::Add sumOfGuards = generationInfo.manager->template getAddZero(); for (auto const& commandDd : commandDds) { - sumOfGuards += commandDd.guardDd.template toAdd(); + sumOfGuards += commandDd.guardDd.template toAdd(); allGuards |= commandDd.guardDd; } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); + uint_fast64_t maxChoices = sumOfGuards.getMax(); STORM_LOG_TRACE("Found " << maxChoices << " local choices."); @@ -827,7 +829,7 @@ namespace storm { for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices))); + equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(currentChoices)); // If there is no such state, continue with the next possible number of choices. if (equalsNumberOfChoicesDd.isZero()) { @@ -880,7 +882,7 @@ namespace storm { } // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); @@ -1111,6 +1113,17 @@ namespace storm { return rewardModels; } + template + void checkRewards(storm::dd::Add const& rewards) { + STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + } + + template + void checkRewards(storm::dd::Add const& rewards) { + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + } + template storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& transitionMatrix, boost::optional>& stateActionDd) { @@ -1127,8 +1140,7 @@ namespace storm { rewards = reachableStatesAdd * states * rewards; // Perform some sanity checks. - STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + checkRewards(rewards); // Add the rewards to the global state reward vector. stateRewards.get() += rewards; @@ -1165,8 +1177,7 @@ namespace storm { } // Perform some sanity checks. - STORM_LOG_WARN_COND(stateActionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!stateActionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); + checkRewards(stateActionRewardDd); // Add the rewards to the global transition reward matrix. stateActionRewards.get() += stateActionRewardDd; @@ -1217,8 +1228,7 @@ namespace storm { } // Perform some sanity checks. - STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); - STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); + checkRewards(transitionRewardDd); // Add the rewards to the global transition reward matrix. transitionRewards.get() += transitionRewardDd; @@ -1427,7 +1437,9 @@ namespace storm { // Explicitly instantiate the symbolic model builder. template class DdPrismModelBuilder; template class DdPrismModelBuilder; - + + template class DdPrismModelBuilder; + } // namespace adapters } // namespace storm diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 8b968e756..2dd312a51 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -196,8 +196,8 @@ namespace storm { } #endif - template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + template + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& property : formulas) { STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); std::cout.flush(); @@ -217,8 +217,8 @@ namespace storm { } } - template - void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + template + void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& property : formulas) { STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); std::cout.flush(); @@ -277,11 +277,11 @@ namespace storm { STORM_LOG_ASSERT(false, "Unknown model type."); \ } - template + template void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. storm::utility::Stopwatch modelBuildingWatch(true); - auto markovModel = buildSymbolicModel(model, extractFormulasFromProperties(properties)); + auto markovModel = buildSymbolicModel(model, extractFormulasFromProperties(properties)); modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -290,9 +290,9 @@ namespace storm { // Then select the correct engine. if (hybrid) { - verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant); + verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant); } else { - verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant); + verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant); } } @@ -376,8 +376,17 @@ namespace storm { template<> void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { - STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); - buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); + auto engine = storm::settings::getModule().getEngine(); + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + auto ddlib = storm::settings::getModule().getDdLibraryType(); + STORM_LOG_THROW(ddlib == storm::dd::DdType::Sylvan, storm::exceptions::InvalidSettingsException, "This data-type is only available when selecting sylvan."); + buildAndCheckSymbolicModelWithSymbolicEngine(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant); + } else { + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine."); + buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); + } + + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine."); } #endif diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp index 410e247b5..9b8ceea68 100644 --- a/src/storm/models/symbolic/Ctmc.cpp +++ b/src/storm/models/symbolic/Ctmc.cpp @@ -6,6 +6,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -57,6 +59,8 @@ namespace storm { template class Ctmc; template class Ctmc; + template class Ctmc; + } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp index c4e1d56a8..23dd73d90 100644 --- a/src/storm/models/symbolic/DeterministicModel.cpp +++ b/src/storm/models/symbolic/DeterministicModel.cpp @@ -6,6 +6,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -31,7 +33,9 @@ namespace storm { // Explicitly instantiate the template class. template class DeterministicModel; template class DeterministicModel; - + + template class DeterministicModel; + } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/storm/models/symbolic/Dtmc.cpp b/src/storm/models/symbolic/Dtmc.cpp index 87aa5c323..584074481 100644 --- a/src/storm/models/symbolic/Dtmc.cpp +++ b/src/storm/models/symbolic/Dtmc.cpp @@ -6,6 +6,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -30,7 +32,9 @@ namespace storm { // Explicitly instantiate the template class. template class Dtmc; template class Dtmc; - + + template class Dtmc; + } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/storm/models/symbolic/Mdp.cpp b/src/storm/models/symbolic/Mdp.cpp index 49c7b5935..a8260eb1b 100644 --- a/src/storm/models/symbolic/Mdp.cpp +++ b/src/storm/models/symbolic/Mdp.cpp @@ -6,6 +6,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -31,6 +33,8 @@ namespace storm { // Explicitly instantiate the template class. template class Mdp; template class Mdp; + + template class Mdp; } // namespace symbolic } // namespace models diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 703686ea6..fb61b4575 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -271,9 +271,8 @@ namespace storm { // Explicitly instantiate the template class. template class Model; template class Model; -#ifdef STORM_HAVE_CARL + template class Model; -#endif } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index 0a3e37e79..88d9fc3e0 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -4,6 +4,8 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -157,6 +159,9 @@ namespace storm { template class StandardRewardModel; template class StandardRewardModel; + + template class StandardRewardModel; + } } } diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 5505b185e..65938e3c5 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -5,6 +5,8 @@ #include "storm/utility/dd.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace solver { @@ -20,45 +22,100 @@ namespace storm { template storm::dd::Add SymbolicEliminationLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::DdManager& ddManager = x.getDdManager(); + + // We start by creating triple-layered meta variables for all original meta variables. We will use them later in the elimination process. + std::vector> oldToNewMapping; + std::set newRowVariables; + std::set newColumnVariables; + std::set helperVariables; + std::vector> newRowColumnMetaVariablePairs; + std::vector> columnHelperMetaVariablePairs; + std::vector> rowRowMetaVariablePairs; + std::vector> columnColumnMetaVariablePairs; + for (auto const& metaVariablePair : this->rowColumnMetaVariablePairs) { + auto rowVariable = metaVariablePair.first; + + storm::dd::DdMetaVariable const& metaVariable = ddManager.getMetaVariable(rowVariable); + + std::vector newMetaVariables; + if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) { + newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), 3); + } else { + newMetaVariables = ddManager.addMetaVariable("tmp_" + metaVariable.getName(), metaVariable.getLow(), metaVariable.getHigh(), 3); + } + + newRowVariables.insert(newMetaVariables[0]); + newColumnVariables.insert(newMetaVariables[1]); + helperVariables.insert(newMetaVariables[2]); + + newRowColumnMetaVariablePairs.emplace_back(newMetaVariables[0], newMetaVariables[1]); + columnHelperMetaVariablePairs.emplace_back(newMetaVariables[1], newMetaVariables[2]); + + rowRowMetaVariablePairs.emplace_back(metaVariablePair.first, newMetaVariables[0]); + columnColumnMetaVariablePairs.emplace_back(metaVariablePair.second, newMetaVariables[1]); + + oldToNewMapping.emplace_back(std::move(newMetaVariables)); + } + + std::vector> oldNewMetaVariablePairs = rowRowMetaVariablePairs; + for (auto const& entry : columnColumnMetaVariablePairs) { + oldNewMetaVariablePairs.emplace_back(entry.first, entry.second); + } + + std::vector> shiftMetaVariablePairs = newRowColumnMetaVariablePairs; + for (auto const& entry : columnHelperMetaVariablePairs) { + shiftMetaVariablePairs.emplace_back(entry.first, entry.second); + } + + // Build diagonal BDD over new meta variables. storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); diagonal &= this->allRows; + diagonal = diagonal.swapVariables(oldNewMetaVariablePairs); - storm::dd::Add rowsAdd = this->allRows.template toAdd(); + + storm::dd::Add rowsAdd = this->allRows.swapVariables(rowRowMetaVariablePairs).template toAdd(); storm::dd::Add diagonalAdd = diagonal.template toAdd(); - // Revert the conversion to an equation system. - storm::dd::Add matrix = diagonalAdd - this->A; + // Revert the conversion to an equation system and move it to the new meta variables. + storm::dd::Add matrix = diagonalAdd - this->A.swapVariables(oldNewMetaVariablePairs); - storm::dd::Add solution = b; + // Initialize solution over the new meta variables. + storm::dd::Add solution = b.swapVariables(oldNewMetaVariablePairs); // As long as there are transitions, we eliminate them. + uint64_t iterations = 0; while (!matrix.isZero()) { // Determine inverse loop probabilies - storm::dd::Add inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(this->columnMetaVariables)); - - inverseLoopProbabilities.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add inverseLoopProbabilities = rowsAdd / (rowsAdd - (diagonalAdd * matrix).sumAbstract(newColumnVariables)); // Scale all transitions with the inverse loop probabilities. matrix *= inverseLoopProbabilities; + solution *= inverseLoopProbabilities; // Delete diagonal elements, i.e. remove self-loops. - matrix = diagonal.ite(x.getDdManager().template getAddZero(), matrix); + matrix = diagonal.ite(ddManager.template getAddZero(), matrix); // Update the one-step probabilities. - solution += (matrix * solution.swapVariables(this->rowColumnMetaVariablePairs)).sumAbstract(this->columnMetaVariables); + solution += (matrix * solution.swapVariables(newRowColumnMetaVariablePairs)).sumAbstract(newColumnVariables); + + // Shortcut all transitions by eliminating one intermediate step. + matrix = matrix.multiplyMatrix(matrix.permuteVariables(shiftMetaVariablePairs), newColumnVariables); + matrix = matrix.swapVariables(columnHelperMetaVariablePairs); - // Now eliminate all direct transitions of all states. - storm::dd::Add matrixWithRemoved; + ++iterations; + std::cout << "iteration: " << iterations << std::endl; } - std::cout << "here" << std::endl; - solution.exportToDot("solution.dot"); + STORM_LOG_DEBUG("Elimination completed in " << iterations << " iterations."); - exit(-1); + return solution.swapVariables(rowRowMetaVariablePairs); } template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; - + + template class SymbolicEliminationLinearEquationSolver; + } } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 85efc4cd9..2d0895838 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -8,6 +8,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace solver { @@ -26,47 +28,7 @@ namespace storm { precision = settings.getPrecision(); relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; } - - template - storm::dd::Add SymbolicLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { - // Start by computing the Jacobi decomposition of the matrix A. - storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), rowColumnMetaVariablePairs); - diagonal &= allRows; - - storm::dd::Add lu = diagonal.ite(this->A.getDdManager().template getAddZero(), this->A); - storm::dd::Add diagonalAdd = diagonal.template toAdd(); - storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); - - storm::dd::Add scaledLu = lu / diag; - storm::dd::Add scaledB = b / diag; - - // Set up additional environment variables. - storm::dd::Add xCopy = x; - uint_fast64_t iterationCount = 0; - bool converged = false; - - while (!converged && iterationCount < maximalNumberOfIterations) { - storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); - storm::dd::Add tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); - - // Now check if the process already converged within our precision. - converged = tmp.equalModuloPrecision(xCopy, precision, relative); - - xCopy = tmp; - // Increase iteration count so we can abort if convergence is too slow. - ++iterationCount; - } - - if (converged) { - STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations."); - } else { - STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations."); - } - - return xCopy; - } - template storm::dd::Add SymbolicLinearEquationSolver::multiply(storm::dd::Add const& x, storm::dd::Add const* b, uint_fast64_t n) const { storm::dd::Add xCopy = x; @@ -86,5 +48,7 @@ namespace storm { template class SymbolicLinearEquationSolver; template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolver; + } } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index 0026a3318..25195c446 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -63,7 +63,7 @@ namespace storm { * @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A. * @return The solution of the equation system. */ - virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const; + virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp new file mode 100644 index 000000000..c3613e3ea --- /dev/null +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -0,0 +1,68 @@ +#include "storm/solver/SymbolicNativeLinearEquationSolver.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" + +#include "storm/utility/dd.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" + +namespace storm { + namespace solver { + + template + SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, precision, maximalNumberOfIterations, relative) { + // Intentionally left empty. + } + + template + SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { + // Intentionally left empty. + } + + template + storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { + // Start by computing the Jacobi decomposition of the matrix A. + storm::dd::Bdd diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs); + diagonal &= this->allRows; + + storm::dd::Add lu = diagonal.ite(this->A.getDdManager().template getAddZero(), this->A); + storm::dd::Add diagonalAdd = diagonal.template toAdd(); + storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); + + storm::dd::Add scaledLu = lu / diag; + storm::dd::Add scaledB = b / diag; + + // Set up additional environment variables. + storm::dd::Add xCopy = x; + uint_fast64_t iterationCount = 0; + bool converged = false; + + while (!converged && iterationCount < this->maximalNumberOfIterations) { + storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); + + // Now check if the process already converged within our precision. + converged = tmp.equalModuloPrecision(xCopy, this->precision, this->relative); + + xCopy = tmp; + + // Increase iteration count so we can abort if convergence is too slow. + ++iterationCount; + } + + if (converged) { + STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations."); + } else { + STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations."); + } + + return xCopy; + } + + template class SymbolicNativeLinearEquationSolver; + template class SymbolicNativeLinearEquationSolver; + + } +} diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.h b/src/storm/solver/SymbolicNativeLinearEquationSolver.h new file mode 100644 index 000000000..f83806a89 --- /dev/null +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.h @@ -0,0 +1,58 @@ +#pragma once + +#include "storm/solver/SymbolicLinearEquationSolver.h" + +namespace storm { + namespace solver { + + /*! + * An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of + * linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided. + */ + template + class SymbolicNativeLinearEquationSolver : public SymbolicLinearEquationSolver { + public: + /*! + * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. + * + * @param A The matrix defining the coefficients of the linear equation system. + * @param diagonal An ADD characterizing the elements on the diagonal of the matrix. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + */ + SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); + + /*! + * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. + * + * @param A The matrix defining the coefficients of the linear equation system. + * @param allRows A BDD characterizing all rows of the equation system. + * @param rowMetaVariables The meta variables used to encode the rows of the matrix. + * @param columnMetaVariables The meta variables used to encode the columns of the matrix. + * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta + * variables. + * @param precision The precision to achieve. + * @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear + * equation system iteratively. + * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. + */ + SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + /*! + * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. + * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has + * to be given upon construction time of the solver object. + * + * @param x The initial guess for the solution vector. Its length must be equal to the number of rows of A. + * @param b The right-hand side of the equation system. Its length must be equal to the number of rows of A. + * @return The solution of the equation system. + */ + virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const; + + }; + + } // namespace solver +} // namespace storm diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 1f09fa687..521bc9f46 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -219,6 +219,31 @@ namespace storm { return Add(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); } + template + Add Add::permuteVariables(std::vector> const& metaVariablePairs) const { + std::set newContainedMetaVariables; + 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); + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable); + } + } + STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables."); + return Add(this->getDdManager(), internalAdd.permuteVariables(from, to), newContainedMetaVariables); + } + template Add Add::multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const { // Create the CUDD summation variables. diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index a0db0be76..b3803bfc2 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -329,6 +329,15 @@ namespace storm { */ Add swapVariables(std::vector> const& metaVariablePairs) const; + /*! + * Permutes the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have + * the same number of underlying ADD variables. The first component of the i-th entry is substituted by the second component. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be permuted. + * @return The resulting ADD. + */ + Add permuteVariables(std::vector> const& metaVariablePairs) const; + /*! * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta * variables. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 872ef4856..723694fe1 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -188,6 +188,24 @@ namespace storm { return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } + template + InternalAdd InternalAdd::permuteVariables(std::vector> const& from, std::vector> const& to) const { + // Build the full permutation. + uint64_t numberOfVariables = ddManager->getCuddManager().ReadSize(); + int* permutation = new int[numberOfVariables]; + for (uint64_t variable = 0; variable < numberOfVariables; ++variable) { + permutation[variable] = variable; + } + + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { + permutation[it1->getIndex()] = it2->getIndex(); + } + InternalAdd result(ddManager, this->getCuddAdd().Permute(permutation)); + + delete[] permutation; + return result; + } + template InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { // Create the CUDD summation variables. diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 78f840b96..096bbbcf3 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -309,6 +309,16 @@ namespace storm { */ InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; + /*! + * Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by + * ADDs must have equal length. + * + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. + * @return The resulting ADD. + */ + InternalAdd permuteVariables(std::vector> const& from, std::vector> const& to) const; + /*! * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta * variables. diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 08eb74bb1..12d7d31f0 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -405,6 +405,17 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); } + template + InternalAdd InternalAdd::permuteVariables(std::vector> const& from, std::vector> const& to) const { + std::vector fromIndices; + std::vector toIndices; + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { + fromIndices.push_back(it1->getIndex()); + toIndices.push_back(it2->getIndex()); + } + return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); + } + template InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { InternalBdd summationVariables = ddManager->getBddOne(); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index d91374903..93f732acc 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -327,7 +327,17 @@ namespace storm { * @return The resulting ADD. */ InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; - + + /*! + * Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by + * ADDs must have equal length. + * + * @param from The vector that specifies the 'from' part of the variable renaming. + * @param to The vector that specifies the 'to' part of the variable renaming. + * @return The resulting ADD. + */ + InternalAdd permuteVariables(std::vector> const& from, std::vector> const& to) const; + /*! * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta * variables. diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index 26259d98b..afdee551d 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -70,7 +70,6 @@ namespace storm { template ValueType maximum(std::map const& values); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 7b0cc1f94..88280f306 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -2,7 +2,7 @@ #include -#include "storm/solver/SymbolicLinearEquationSolver.h" +#include "storm/solver/SymbolicNativeLinearEquationSolver.h" #include "storm/solver/SymbolicEliminationLinearEquationSolver.h" #include "storm/solver/SymbolicMinMaxLinearEquationSolver.h" #include "storm/solver/SymbolicGameSolver.h" @@ -25,7 +25,6 @@ namespace storm { namespace utility { namespace solver { - template std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { @@ -33,8 +32,10 @@ namespace storm { switch (equationSolver) { case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; + case storm::solver::EquationSolverType::Native: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); default: - return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to native solver."); + return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 3aca0dbe2..c03076915 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -550,25 +550,25 @@ namespace storm { #endif - template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { + template + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Ctmc) { - std::shared_ptr> ctmc = model->template as>(); - storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); + std::shared_ptr> ctmc = model->template as>(); + storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } @@ -577,20 +577,49 @@ namespace storm { } return result; } - + template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { +// std::unique_ptr result; +// storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); +// if (model->getType() == storm::models::ModelType::Dtmc) { +// std::shared_ptr> dtmc = model->template as>(); +// storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); +// if (modelchecker.canHandle(task)) { +// result = modelchecker.check(task); +// } +// } else if (model->getType() == storm::models::ModelType::Ctmc) { +// std::shared_ptr> ctmc = model->template as>(); +// storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); +// if (modelchecker.canHandle(task)) { +// result = modelchecker.check(task); +// } +// } else if (model->getType() == storm::models::ModelType::Mdp) { +// std::shared_ptr> mdp = model->template as>(); +// storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); +// if (modelchecker.canHandle(task)) { +// result = modelchecker.check(task); +// } +// } else { +// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); +// } +// return result; + return nullptr; + } + + template + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } @@ -600,6 +629,29 @@ namespace storm { return result; } + template + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { +// std::unique_ptr result; +// storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); +// if (model->getType() == storm::models::ModelType::Dtmc) { +// std::shared_ptr> dtmc = model->template as>(); +// storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); +// if (modelchecker.canHandle(task)) { +// result = modelchecker.check(task); +// } +// } else if (model->getType() == storm::models::ModelType::Mdp) { +// std::shared_ptr> mdp = model->template as>(); +// storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); +// if (modelchecker.canHandle(task)) { +// result = modelchecker.check(task); +// } +// } else { +// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); +// } +// return result; + return nullptr; + } + template std::unique_ptr verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) {