diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 51fe6f36f..8c546ec50 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -28,6 +28,7 @@ #include "src/utility/dd.h" #include "src/utility/math.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidStateException.h" namespace storm { namespace builder { @@ -351,111 +352,149 @@ namespace storm { std::set automata; }; - template - struct EdgeDestinationDd { - EdgeDestinationDd(storm::dd::Add const& transitionsDd, std::set const& writtenGlobalVariables = {}) : transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables) { + template + struct ComposerResult { + ComposerResult(storm::dd::Add const& transitions, storm::dd::Add const& stateActionDd, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), stateActionDd(stateActionDd), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { // Intentionally left empty. } - storm::dd::Add transitionsDd; - std::set writtenGlobalVariables; + storm::dd::Add transitions; + storm::dd::Add stateActionDd; + uint64_t numberOfNondeterminismVariables; }; - // This structure represents an edge. - template - struct EdgeDd { - EdgeDd(storm::dd::Add const& guardDd = storm::dd::Add(), storm::dd::Add const& transitionsDd = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guardDd(guardDd), transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { - // Intentionally left empty. - } - - EdgeDd(EdgeDd const& other) : guardDd(other.guardDd), transitionsDd(other.transitionsDd), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { + // A class that is responsible for performing the actual composition. This + template + class SystemComposer : public storm::jani::CompositionVisitor { + public: + SystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : model(model), variables(variables) { // Intentionally left empty. } - EdgeDd& operator=(EdgeDd const& other) { - if (this != &other) { - globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; - writtenGlobalVariables = other.writtenGlobalVariables; - guardDd = other.guardDd; - transitionsDd = other.transitionsDd; - } - return *this; - } + virtual ComposerResult compose() = 0; + + protected: + // The model that is referred to by the composition. + storm::jani::Model const& model; - storm::dd::Add guardDd; - storm::dd::Add transitionsDd; - std::set writtenGlobalVariables; - std::set globalVariablesWrittenMultipleTimes; + // The variable to use when building an automaton. + CompositionVariables const& variables; }; - - // This structure represents a subcomponent of a composition. - template - struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity) : identity(identity) { + + // This structure represents an edge destination. + template + struct EdgeDestinationDd { + EdgeDestinationDd(storm::dd::Add const& transitions, std::set const& writtenGlobalVariables = {}) : transitions(transitions), writtenGlobalVariables(writtenGlobalVariables) { // Intentionally left empty. } - std::map>> actionIndexToEdges; - storm::dd::Add identity; + storm::dd::Add transitions; + std::set writtenGlobalVariables; }; template - EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { - EdgeDd result(edge); - result.transitionsDd *= identity; - return result; - } - - template - EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { - EdgeDd result; + EdgeDestinationDd buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add const& guard, CompositionVariables const& variables) { + storm::dd::Add transitions = variables.manager->template getAddOne(); - // Compose the guards. - result.guardDd = edge1.guardDd * edge2.guardDd; + STORM_LOG_TRACE("Translating edge destination."); - // If the composed guard is already zero, we can immediately return an empty result. - if (result.guardDd.isZero()) { - result.transitionsDd = edge1.transitionsDd.getDdManager().template getAddZero(); - return result; + // Iterate over all assignments (boolean and integer) and build the DD for it. + std::set assignedVariables; + for (auto const& assignment : destination.getAssignments()) { + // Record the variable as being written. + STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName()); + assignedVariables.insert(assignment.getExpressionVariable()); + + // Translate the written variable. + auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap->at(assignment.getExpressionVariable()); + storm::dd::Add writtenVariable = variables.manager->template getIdentity(primedMetaVariable); + + // Translate the expression that is being assigned. + storm::dd::Add updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + + // Combine the update expression with the guard. + storm::dd::Add result = updateExpression * guard; + + // Combine the variable and the assigned expression. + result = result.equals(writtenVariable).template toAdd(); + result *= guard; + + // Restrict the transitions to the range of the written variable. + result = result * variables.manager->getRange(primedMetaVariable).template toAdd(); + + // Combine the assignment DDs. + transitions *= result; } - // Compute the set of variables written multiple times by the composition. - std::set oldVariablesWrittenMultipleTimes; - std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); - - std::set newVariablesWrittenMultipleTimes; - std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); + // Compute the set of assigned global variables. + std::set assignedGlobalVariables; + std::set_intersection(assignedVariables.begin(), assignedVariables.end(), variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); - std::set variablesWrittenMultipleTimes; - std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); - - result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); - - // Compute the set of variables written by the composition. - std::set variablesWritten; - std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); - - result.writtenGlobalVariables = variablesWritten; - - // Compose the guards. - result.guardDd = edge1.guardDd * edge2.guardDd; + // All unassigned boolean variables need to keep their value. + for (storm::jani::BooleanVariable const& variable : automaton.getVariables().getBooleanVariables()) { + if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) { + STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName()); + transitions *= variables.variableToIdentityMap.at(variable.getExpressionVariable()); + } + } - // Compose the transitions. - result.transitionsDd = edge1.transitionsDd * edge2.transitionsDd; + // All unassigned integer variables need to keep their value. + for (storm::jani::BoundedIntegerVariable const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) { + STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName()); + transitions *= variables.variableToIdentityMap.at(variable.getExpressionVariable()); + } + } - return result; + return EdgeDestinationDd(variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd() * transitions * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables); } - // A class that is responsible for performing the actual composition. template - class AutomatonComposer : public storm::jani::CompositionVisitor { + class SeparateEdgesSystemComposer : public SystemComposer { public: - AutomatonComposer(storm::jani::Model const& model, CompositionVariables const& variables) : model(model), variables(variables) { + // This structure represents an edge. + struct EdgeDd { + EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { + // Intentionally left empty. + } + + EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { + // Intentionally left empty. + } + + EdgeDd& operator=(EdgeDd const& other) { + if (this != &other) { + globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes; + writtenGlobalVariables = other.writtenGlobalVariables; + guard = other.guard; + transitions = other.transitions; + } + return *this; + } + + storm::dd::Add guard; + storm::dd::Add transitions; + std::set writtenGlobalVariables; + std::set globalVariablesWrittenMultipleTimes; + }; + + // This structure represents a subcomponent of a composition. + struct AutomatonDd { + AutomatonDd(storm::dd::Add const& identity) : identity(identity) { + // Intentionally left empty. + } + + std::map> actionIndexToEdges; + storm::dd::Add identity; + }; + + SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { // Intentionally left empty. } - AutomatonDd compose() { - return boost::any_cast>(this->model.getSystemComposition().accept(*this, boost::none)); + ComposerResult compose() override { + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); + return buildSystem(this->model, globalAutomaton, this->variables); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { @@ -463,7 +502,7 @@ namespace storm { } boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - AutomatonDd subautomaton = boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); // Build a mapping from indices to indices for the renaming. std::map renamingIndexToIndex; @@ -481,7 +520,7 @@ namespace storm { } // Finally, apply the renaming. - AutomatonDd result(subautomaton.identity); + AutomatonDd result(subautomaton.identity); for (auto const& actionEdges : subautomaton.actionIndexToEdges) { auto it = renamingIndexToIndex.find(actionEdges.first); if (it != renamingIndexToIndex.end()) { @@ -496,8 +535,8 @@ namespace storm { } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - AutomatonDd leftSubautomaton = boost::any_cast>(composition.getLeftSubcomposition().accept(*this, boost::none)); - AutomatonDd rightSubautomaton = boost::any_cast>(composition.getRightSubcomposition().accept(*this, boost::none)); + AutomatonDd leftSubautomaton = boost::any_cast(composition.getLeftSubcomposition().accept(*this, boost::none)); + AutomatonDd rightSubautomaton = boost::any_cast(composition.getRightSubcomposition().accept(*this, boost::none)); // Build the set of synchronizing action indices. std::set synchronizingActionIndices; @@ -512,7 +551,7 @@ namespace storm { // Perform the composition. // First, consider all actions in the left subcomposition. - AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); + AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); uint64_t index = 0; for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { // If we need to synchronize over this action, do so now. @@ -521,8 +560,8 @@ namespace storm { if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { for (auto const& edge1 : actionEdges.second) { for (auto const& edge2 : rightIt->second) { - EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); - if (!edgeDd.guardDd.isZero()) { + EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); + if (!edgeDd.guard.isZero()) { result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); } index++; @@ -552,77 +591,207 @@ namespace storm { } private: - EdgeDestinationDd buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add const& guard) { - storm::dd::Add transitionsDd = variables.manager->template getAddOne(); + storm::dd::Add combineEdgesBySummation(std::vector const& edges, CompositionVariables const& variables) { + storm::dd::Add result = variables.manager->template getAddZero(); + for (auto const& edge : edges) { + // Simply add all actions, but make sure to include the missing global variable identities. + result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables); + } + return result; + } + + std::pair> combineEdgesByNondeterministicChoice(std::vector& edges, CompositionVariables const& variables) { + // Complete all edges by adding the missing global variable identities. + for (auto& edge : edges) { + edge.transitions *= computeMissingGlobalVariableIdentities(edge, variables); + } - STORM_LOG_TRACE("Translating edge destination."); + // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. + storm::dd::Add sumOfGuards = variables.manager->template getAddZero(); + for (auto const& edge : edges) { + sumOfGuards += edge.guard; + } + uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); + STORM_LOG_TRACE("Found " << maxChoices << " local choices."); - // Iterate over all assignments (boolean and integer) and build the DD for it. - std::set assignedVariables; - for (auto const& assignment : destination.getAssignments()) { - // Record the variable as being written. - STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName()); - assignedVariables.insert(assignment.getExpressionVariable()); + // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. + if (maxChoices == 0) { + return std::make_pair(0, variables.manager->template getAddZero()); + } else if (maxChoices == 1) { + return std::make_pair(0, combineEdgesBySummation(edges, variables)); + } else { + // Calculate number of required variables to encode the nondeterminism. + uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - // Translate the written variable. - auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap->at(assignment.getExpressionVariable()); - storm::dd::Add writtenVariable = variables.manager->template getIdentity(primedMetaVariable); + storm::dd::Add allEdges = variables.manager->template getAddZero(); - // Translate the expression that is being assigned. - storm::dd::Add updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + storm::dd::Bdd equalsNumberOfChoicesDd; + std::vector> choiceDds(maxChoices, variables.manager->template getAddZero()); + std::vector> remainingDds(maxChoices, variables.manager->getBddZero()); - // Combine the update expression with the guard. - storm::dd::Add result = updateExpression * guard; + for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { + // Determine the set of states with exactly currentChoices choices. + equalsNumberOfChoicesDd = sumOfGuards.equals(variables.manager->getConstant(static_cast(currentChoices))); + + // If there is no such state, continue with the next possible number of choices. + if (equalsNumberOfChoicesDd.isZero()) { + continue; + } + + // Reset the previously used intermediate storage. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + choiceDds[j] = variables.manager->template getAddZero(); + remainingDds[j] = equalsNumberOfChoicesDd; + } + + for (std::size_t j = 0; j < edges.size(); ++j) { + // 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 = edges[j].guard.toBdd() && equalsNumberOfChoicesDd; + + // If there is no such state, continue with the next command. + if (guardChoicesIntersection.isZero()) { + continue; + } + + // Split the currentChoices nondeterministic choices. + for (uint_fast64_t k = 0; k < currentChoices; ++k) { + // Calculate the overlapping part of command guard and the remaining DD. + storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; + + // Check if we can add some overlapping parts to the current index. + if (!remainingGuardChoicesIntersection.isZero()) { + // Remove overlapping parts from the remaining DD. + remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; + + // Combine the overlapping part of the guard with command updates and add it to the resulting DD. + choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitions; + } + + // Remove overlapping parts from the command guard DD + guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; + + // If the guard DD has become equivalent to false, we can stop here. + if (guardChoicesIntersection.isZero()) { + break; + } + } + } + + // Add the meta variables that encode the nondeterminisim to the different choices. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + allEdges += encodeIndex(j, 0, numberOfBinaryVariables, variables) * choiceDds[j]; + } + + // Delete currentChoices out of overlapping DD + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); + } - // Combine the variable and the assigned expression. - result = result.equals(writtenVariable).template toAdd(); - result *= guard; + return std::make_pair(numberOfBinaryVariables, allEdges); + } + } + + ComposerResult buildSystem(AutomatonDd& automatonDd) { + // If the model is an MDP, we need to encode the nondeterminism using additional variables. + if (this->model.getModelType() == storm::jani::ModelType::MDP) { + std::map>> actionIndexToUsedVariablesAndDd; - // Restrict the transitions to the range of the written variable. - result = result * variables.manager->getRange(primedMetaVariable).template toAdd(); + // Combine the edges of each action individually and keep track of how many local nondeterminism variables + // were used. + uint64_t highestNumberOfUsedNondeterminismVariables = 0; + for (auto& action : automatonDd.actionIndexToEdges) { + std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second, this->variables); + actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); + highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); + } - // Combine the assignment DDs. - transitionsDd *= result; + storm::dd::Add result = this->variables.manager->template getAddZero(); + for (auto const& element : actionIndexToUsedVariablesAndDd) { + result += element.second.second * encodeAction(element.first, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); + } + + return ComposerResult(result, result.sumAbstract(this->variables.columnMetaVariables), highestNumberOfUsedNondeterminismVariables); + } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { + storm::dd::Add result = this->variables.manager->template getAddZero(); + for (auto const& action : automatonDd.actionIndexToEdges) { + result += combineEdgesBySummation(action.second, this->variables); + } + return ComposerResult(result, result.sumAbstract(this->variables.columnMetaVariables)); } - // Compute the set of assigned global variables. - std::set assignedGlobalVariables; - std::set_intersection(assignedVariables.begin(), assignedVariables.end(), variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); - - // All unassigned boolean variables need to keep their value. - for (storm::jani::BooleanVariable const& variable : automaton.getVariables().getBooleanVariables()) { - if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName()); - transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable()); - } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + } + + storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { + std::set missingIdentities; + std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + storm::dd::Add identityEncoding = variables.manager->template getAddOne(); + for (auto const& variable : missingIdentities) { + identityEncoding *= variables.variableToIdentityMap.at(variable); } + return identityEncoding; + } + + EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add const& identity) { + EdgeDd result(edge); + result.transitions *= identity; + return result; + } + + EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { + EdgeDd result; - // All unassigned integer variables need to keep their value. - for (storm::jani::BoundedIntegerVariable const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName()); - transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable()); - } + // Compose the guards. + result.guard = edge1.guard * edge2.guard; + + // If the composed guard is already zero, we can immediately return an empty result. + if (result.guard.isZero()) { + result.transitions = edge1.transitions.getDdManager().template getAddZero(); + return result; } - return EdgeDestinationDd(variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd() * transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables); + // Compute the set of variables written multiple times by the composition. + std::set oldVariablesWrittenMultipleTimes; + std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); + + std::set newVariablesWrittenMultipleTimes; + std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin())); + + std::set variablesWrittenMultipleTimes; + std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin())); + + result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes); + + // Compute the set of variables written by the composition. + std::set variablesWritten; + std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin())); + + result.writtenGlobalVariables = variablesWritten; + + // Compose the guards. + result.guard = edge1.guard * edge2.guard; + + // Compose the transitions. + result.transitions = edge1.transitions * edge2.transitions; + + return result; } /*! * Builds the DD for the given edge. */ - EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { + EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { STORM_LOG_TRACE("Translating guard " << edge.getGuard()); - storm::dd::Add guard = variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * variables.automatonToRangeMap.at(automaton.getName()); + storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * this->variables.automatonToRangeMap.at(automaton.getName()); STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); if (!guard.isZero()) { // Create the DDs representing the individual updates. std::vector> destinationDds; for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { - destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard)); + destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); - STORM_LOG_WARN_COND(!destinationDds.back().transitionsDd.isZero(), "Destination does not have any effect."); + STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); } // Start by gathering all variables that were written in at least one update. @@ -632,9 +801,11 @@ namespace storm { // variables was written by any of the updates and make all update results equal w.r.t. this set. If // the edge is labeled with the silent action, we can already multiply the identities of all global variables. if (edge.getActionId() != this->model.getSilentActionIndex()) { - std::for_each(destinationDds.begin(), destinationDds.end(), [&globalVariablesInSomeUpdate] (EdgeDestinationDd const& edgeDestinationDd) { globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); } ); + for (auto const& edgeDestinationDd : destinationDds) { + globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); + } } else { - globalVariablesInSomeUpdate = variables.allGlobalVariables; + globalVariablesInSomeUpdate = this->variables.allGlobalVariables; } // Then, multiply the missing identities. @@ -644,246 +815,707 @@ namespace storm { for (auto const& variable : missingIdentities) { STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); - destinationDd.transitionsDd *= variables.variableToIdentityMap.at(variable); + destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); } } // Now combine the destination DDs to the edge DD. - storm::dd::Add transitionsDd = variables.manager->template getAddZero(); + storm::dd::Add transitions = this->variables.manager->template getAddZero(); for (auto const& destinationDd : destinationDds) { - transitionsDd += destinationDd.transitionsDd; + transitions += destinationDd.transitions; } // Add the source location and the guard. - transitionsDd *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd() * guard; + transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd() * guard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeUpdate.empty()) { - transitionsDd *= variables.globalVariableRanges; + transitions *= this->variables.globalVariableRanges; } // If the edge has a rate, we multiply it to the DD. if (edge.hasRate()) { - transitionsDd *= variables.rowExpressionAdapter->translateExpression(edge.getRate()); + transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); } - return EdgeDd(guard, transitionsDd, globalVariablesInSomeUpdate); + return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); } else { - return EdgeDd(variables.manager->template getAddZero(), variables.manager->template getAddZero()); + return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); } } /*! * Builds the DD for the automaton with the given name. */ - AutomatonDd buildAutomatonDd(std::string const& automatonName) { - AutomatonDd result(variables.automatonToIdentityMap.at(automatonName)); + AutomatonDd buildAutomatonDd(std::string const& automatonName) { + AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); for (auto const& edge : automaton.getEdges()) { // Build the edge and add it if it adds transitions. - EdgeDd edgeDd = buildEdgeDd(automaton, edge); - if (!edgeDd.guardDd.isZero()) { + EdgeDd edgeDd = buildEdgeDd(automaton, edge); + if (!edgeDd.guard.isZero()) { result.actionIndexToEdges[edge.getActionId()].push_back(edgeDd); } } return result; } - - // The model that is referred to by the composition. - storm::jani::Model const& model; - - // The variable to use when building an automaton. - CompositionVariables const& variables; }; template - storm::dd::Add encodeAction(boost::optional const& actionIndex, CompositionVariables const& variables) { - storm::dd::Add encoding = variables.manager->template getAddOne(); + class CombinedEdgesSystemComposer : public SystemComposer { + public: + // This structure represents an edge. + struct EdgeDd { + EdgeDd(storm::dd::Add const& guard = storm::dd::Add(), storm::dd::Add const& transitions = storm::dd::Add(), std::set const& writtenGlobalVariables = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables) { + // Intentionally left empty. + } + + // A DD that represents all states that have this edge enabled. + storm::dd::Add guard; + + // A DD that represents the transitions of this edge. + storm::dd::Add transitions; + + // The set of global variables written by this edge. + std::set writtenGlobalVariables; + }; + + // 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::pair localNondeterminismVariables = std::pair(0, 0), std::map> const& variableToWritingFragment = {}, storm::dd::Bdd const& illegalFragment = storm::dd::Bdd()) : guard(guard), transitions(transitions), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment) { + // Intentionally left empty. + } + + uint64_t getLowestLocalNondeterminismVariable() { + return localNondeterminismVariables.first; + } + + uint64_t getHighestLocalNondeterminismVariable() { + return localNondeterminismVariables.second; + } + + // A DD that represents all states that have this edge enabled. + storm::dd::Add guard; + + // A DD that represents the transitions of this edge. + storm::dd::Add transitions; + + // The local nondeterminism variables used by this action DD, given as the lowest + std::pair localNondeterminismVariables; + + // A mapping from global variables to a DD that characterizes choices (nondeterminism variables) in + // states that write to this global variable. + std::map> variableToWritingFragment; + + // A DD characterizing the fragment of the states satisfying the guard that are illegal because + // there are synchronizing edges enabled that write to the same global variable. + storm::dd::Bdd illegalFragment; + }; + + // This structure represents a subcomponent of a composition. + struct AutomatonDd { + AutomatonDd(storm::dd::Add const& identity) : identity(identity) { + // Intentionally left empty. + } + + std::map actionIndexToAction; + storm::dd::Add identity; + }; - for (auto it = variables.actionVariablesMap.rbegin(), ite = variables.actionVariablesMap.rend(); it != ite; ++it) { - if (actionIndex && it->first == actionIndex.get()) { - encoding *= variables.manager->getEncoding(it->second, 1).template toAdd(); - } else { - encoding *= variables.manager->getEncoding(it->second, 0).template toAdd(); + CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables) : SystemComposer(model, variables) { + // Intentionally left empty. + } + + ComposerResult compose() override { + std::map actionIndexToLocalNondeterminismVariableOffset; + for (auto const& action : this->model.getActions()) { + actionIndexToLocalNondeterminismVariableOffset[this->model.getActionIndex(action.getName())] = 0; } + + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); + return buildSystem(globalAutomaton); } - return encoding; - } - - template - storm::dd::Add computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables const& variables) { - std::set missingIdentities; - std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); - storm::dd::Add identityEncoding = variables.manager->template getAddOne(); - for (auto const& variable : missingIdentities) { - identityEncoding *= variables.variableToIdentityMap.at(variable); - } - return identityEncoding; - } - - template - storm::dd::Add encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables const& variables) { - storm::dd::Add result = variables.manager->template getAddZero(); + boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset); + } - std::map metaVariableNameToValueMap; - for (uint_fast64_t i = 0; i < numberOfLocalNondeterminismVariables; ++i) { - if (index & (1ull << (numberOfLocalNondeterminismVariables - i - 1))) { - metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 1); - } else { - metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0); + boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { + // Build a mapping from indices to indices for the renaming. + std::map renamingIndexToIndex; + for (auto const& entry : composition.getRenaming()) { + if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) { + // Distinguish the cases where we hide the action or properly rename it. + if (entry.second) { + renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get())); + } else { + renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex()); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action."); + } } + + // Prepare the new offset mapping. + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + for (auto const& indexPair : renamingIndexToIndex) { + auto it = actionIndexToLocalNondeterminismVariableOffset.find(indexPair.second); + STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); + newSynchronizingActionToOffsetMap[indexPair.first] = it->second; + } + + // Then, we translate the subcomposition. + AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + + // Now perform the renaming and return result. + return rename(subautomaton, renamingIndexToIndex); } - result.setValue(metaVariableNameToValueMap, 1); - return result; - } - - template - struct BuilderResult { - BuilderResult(storm::dd::Add const& transitionsDd, storm::dd::Add const& stateActionDd, uint64_t numberOfNondeterminismVariables = 0) : transitionsDd(transitionsDd), stateActionDd(stateActionDd), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { - // Intentionally left empty. + boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { + // Build the set of synchronizing action indices. + std::set synchronizingActionIndices; + for (auto const& entry : composition.getSynchronizationAlphabet()) { + if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) { + synchronizingActionIndices.insert(this->model.getActionIndex(entry)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action."); + } + } + + // Then translate the left subcomposition. + AutomatonDd left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); + + // Prepare the new offset mapping. + std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + std::map newActionIndexToLocalNondeterminismVariableOffset = actionIndexToLocalNondeterminismVariableOffset; + for (auto const& actionIndex : synchronizingActionIndices) { + auto it = left.actionIndexToAction.find(actionIndex); + if (it != left.actionIndexToAction.end()) { + newActionIndexToLocalNondeterminismVariableOffset[actionIndex] = it->second.getHighestLocalNondeterminismVariable(); + } + } + + // Then translate the right subcomposition. + AutomatonDd right = boost::any_cast(composition.getRightSubcomposition().accept(*this, newActionIndexToLocalNondeterminismVariableOffset)); + + return composeInParallel(left, right, synchronizingActionIndices); } - storm::dd::Add transitionsDd; - storm::dd::Add stateActionDd; - uint64_t numberOfNondeterminismVariables; - }; - - template - storm::dd::Add combineEdgesBySummation(std::vector> const& edges, CompositionVariables const& variables) { - storm::dd::Add result = variables.manager->template getAddZero(); - for (auto const& edge : edges) { - // Simply add all actions, but make sure to include the missing global variable identities. - result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables); + private: + AutomatonDd composeInParallel(AutomatonDd const& automaton1, AutomatonDd const& automaton2, std::set const& synchronizingActionIndices) { + AutomatonDd result(automaton1); + + for (auto const& action1 : automaton1.actionIndexToAction) { + // If we need to synchronize over this action index, we try to do so now. + if (synchronizingActionIndices.find(action1.first) != synchronizingActionIndices.end()) { + auto action2It = automaton2.actionIndexToAction.find(action1.first); + if (action2It != automaton2.actionIndexToAction.end()) { + result.actionIndexToAction[action1.first] = combineSynchronizingActions(action1.second, action2It->second); + } + } else { + // If we don't synchronize over this action, we need to construct the interleaving. + + // If both modules contain the action, we need to mutually multiply the other identity. + auto action2It = automaton2.actionIndexToAction.find(action1.first); + if (action2It != automaton2.actionIndexToAction.end()) { + result.actionIndexToAction[action1.first] = combineUnsynchronizedActions(action1.second, action2It->second, automaton1.identity, automaton2.identity); + } else { + // If only the first automaton has this action, we only need to apply the identity of the + // second automaton. + result.actionIndexToAction[action1.first] = ActionDd(action1.second.guard, action1.second.transitions * automaton2.identity, action1.localNondeterminismVariables, action1.variableToWritingFragment, action1.illegalFragment); + } + + } + } + + + + + + + + // Combine the tau action. + uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables; + left.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, left.independentAction, right.independentAction, left.identity, right.identity); + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.independentAction.numberOfUsedNondeterminismVariables); + + // Create an empty action for the case where one of the modules does not have a certain action. + typename DdPrismModelBuilder::ActionDecisionDiagram emptyAction(*generationInfo.manager); + + // Treat all non-tau actions of the left module. + for (auto& action : left.synchronizingActionToDecisionDiagramMap) { + // If we need to synchronize over this action index, we try to do so now. + if (synchronizationActionIndices.find(action.first) != synchronizationActionIndices.end()) { + // If we are to synchronize over an action that does not exist in the second module, the result + // is that the synchronization is the empty action. + if (!right.hasSynchronizingAction(action.first)) { + action.second = emptyAction; + } else { + // Otherwise, the actions of the modules are synchronized. + action.second = DdPrismModelBuilder::combineSynchronizingActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first]); + } + } else { + // If we don't synchronize over this action, we need to construct the interleaving. + + // If both modules contain the action, we need to mutually multiply the other identity. + if (right.hasSynchronizingAction(action.first)) { + action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first], left.identity, right.identity); + } else { + // If only the first module has this action, we need to use a dummy action decision diagram + // for the second module. + action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, emptyAction, left.identity, right.identity); + } + } + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, action.second.numberOfUsedNondeterminismVariables); + } + + // Treat all non-tau actions of the right module. + for (auto const& actionIndex : right.getSynchronizingActionIndices()) { + // Here, we only need to treat actions that the first module does not have, because we have handled + // this case earlier. + if (!left.hasSynchronizingAction(actionIndex)) { + if (synchronizationActionIndices.find(actionIndex) != synchronizationActionIndices.end()) { + // If we are to synchronize over this action that does not exist in the first module, the + // result is that the synchronization is the empty action. + left.synchronizingActionToDecisionDiagramMap[actionIndex] = emptyAction; + } else { + // If only the second module has this action, we need to use a dummy action decision diagram + // for the first module. + left.synchronizingActionToDecisionDiagramMap[actionIndex] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, emptyAction, right.synchronizingActionToDecisionDiagramMap[actionIndex], left.identity, right.identity); + } + } + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); + } + + // Combine identity matrices. + left.identity = left.identity * right.identity; + + // Keep track of the number of nondeterminism variables used. + left.numberOfUsedNondeterminismVariables = std::max(left.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); } - return result; - } - - template - std::pair> combineEdgesByNondeterministicChoice(std::vector>& edges, CompositionVariables const& variables) { - // Complete all edges by adding the missing global variable identities. - for (auto& edge : edges) { - edge.transitionsDd *= computeMissingGlobalVariableIdentities(edge, variables); + + ActionDd combineSynchronizingActions(ActionDd action1, ActionDd action2) { + storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + storm::dd::Bdd guard1 = action1.guard.toBdd(); + storm::dd::Bdd guard2 = action2.guard.toBdd(); + storm::dd::Bdd combinedGuard = guard1 && guard2; + + // Cross-multiply the guards to the other fragments that write global variables and check for overlapping + // parts. This finds illegal parts in which a global variable is written multiple times. + std::map> globalVariableToWritingFragment; + for (auto& entry : action1.variableToWritingFragment) { + entry.second &= guard2; + globalVariableToWritingFragment[entry.first] = entry.second; + } + for (auto& entry : action2.variableToWritingFragment) { + entry.second &= guard1; + auto it = globalVariableToWritingFragment.find(entry.first); + if (it != globalVariableToWritingFragment.end()) { + illegalFragment |= it->second && entry.second; + it->second |= entry.second; + } else { + globalVariableToWritingFragment[entry.first] = entry.second; + } + } + + return ActionDd(action1.guard * action2.guard, action1.transitions * action2.transitions, std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment); } - // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = variables.manager->template getAddZero(); - for (auto const& edge : edges) { - sumOfGuards += edge.guardDd; + ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { + // First extend the action DDs by the other identities. + STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions."); + action1.transitionsDd = action1.transitionsDd * identityDd2; + action2.transitionsDd = action2.transitionsDd * identityDd1; + + // Then combine the extended action DDs. + return combineUnsynchronizedActions(action1, action2); } - uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - STORM_LOG_TRACE("Found " << maxChoices << " local choices."); - // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. - if (maxChoices == 0) { - return std::make_pair(0, variables.manager->template getAddZero()); - } else if (maxChoices == 1) { - return std::make_pair(0, combineEdgesBySummation(edges, variables)); - } else { - // Calculate number of required variables to encode the nondeterminism. - uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); + ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2) { + STORM_LOG_TRACE("Combining unsynchronized actions."); - storm::dd::Add allEdges = variables.manager->template getAddZero(); + if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { + return ActionDd(action1.guard + action2.guard, action1.transitions + action2.transitions, std::make_pair(0, 0), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), this->variables.manager->getBddZero()); + } else if (this->model.getModelType() == storm::jani::ModelType::MDP) { + if (action1.transitions.isZero()) { + return action2; + } else if (action2.transitions.isZero()) { + return action1; + } + + // Bring both choices to the same number of variables that encode the nondeterminism. + assert(action1.getLowestLocalNondeterminismVariable() == action2.getLowestLocalNondeterminismVariable()); + uint_fast64_t highestLocalNondeterminismVariable = std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable()); + if (action1.getHighestLocalNondeterminismVariable() > action2.getHighestLocalNondeterminismVariable()) { + storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); + + for (uint_fast64_t i = action2.getHighestLocalNondeterminismVariable(); i < action1.getHighestLocalNondeterminismVariable(); ++i) { + nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); + } + action2.transitions *= nondeterminismEncoding; + } else if (action2.getHighestLocalNondeterminismVariable() > action1.getHighestLocalNondeterminismVariable()) { + storm::dd::Add nondeterminismEncoding = this->variables.manager->template getAddOne(); + + for (uint_fast64_t i = action1.getHighestLocalNondeterminismVariable(); i < action2.getHighestLocalNondeterminismVariable(); ++i) { + nondeterminismEncoding *= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0).template toAdd(); + } + action1.transitions *= nondeterminismEncoding; + } + + // Add a new variable that resolves the nondeterminism between the two choices. + storm::dd::Add combinedTransitions = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1).ite(action2.transitions, action1.transitions); + + // Add the new variable to the writing fragments of each global variable before joining them. + for (auto& entry : action1.variableToWritingFragment) { + entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 0) && entry.second; + } + for (auto& entry : action2.variableToWritingFragment) { + entry.second = this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[highestLocalNondeterminismVariable], 1) && entry.second; + } + + return ActionDd((action1.guard.toBdd() || action2.guard.toBdd()).template toAdd(), combinedTransitions, std::make_pair(action1.getLowestLocalNondeterminismVariable(), highestLocalNondeterminismVariable + 1), joinVariableWritingFragmentMaps(action1.variableToWritingFragment, action2.variableToWritingFragment), action1.illegalFragment || action2.illegalFragment); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); + } + } + + AutomatonDd rename(AutomatonDd const& automaton, std::map const& indexToIndex) { + AutomatonDd result(automaton.identity); + + for (auto const& action : automaton.actionIndexToAction) { + auto renamingIt = indexToIndex.find(action.first); + if (renamingIt != indexToIndex.end()) { + // If the action is to be renamed and an action with the target index already exists, we need + // to combine the action DDs. + auto itNewActions = result.actionIndexToAction.find(renamingIt->second); + if (itNewActions != result.actionIndexToAction.end()) { + itNewActions->second = combineUnsynchronizedActions(action.second, itNewActions->second); + } else { + // In this case, we can simply copy the action over. + result.actionIndexToAction[renamingIt->second] = action.second; + } + } else { + // If the action is not to be renamed, we need to copy it over. However, if some other action + // was renamed to the very same action name before, we need to combine the transitions. + auto itNewActions = result.actionIndexToAction.find(action.first); + if (itNewActions != result.actionIndexToAction.end()) { + itNewActions->second = combineUnsynchronizedActions(action.second, itNewActions->second); + } else { + // In this case, we can simply copy the action over. + result.actionIndexToAction[action.first] = action.second; + } + } + } - storm::dd::Bdd equalsNumberOfChoicesDd; - std::vector> choiceDds(maxChoices, variables.manager->template getAddZero()); - std::vector> remainingDds(maxChoices, variables.manager->getBddZero()); + return result; + } + + EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { + STORM_LOG_TRACE("Translating guard " << edge.getGuard()); + storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * this->variables.automatonToRangeMap.at(automaton.getName()); + STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); - for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { - // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(variables.manager->getConstant(static_cast(currentChoices))); + if (!guard.isZero()) { + // Create the DDs representing the individual updates. + std::vector> destinationDds; + for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { + destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables)); + + STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); + } + + // Start by gathering all variables that were written in at least one update. + std::set globalVariablesInSomeUpdate; + + // If the edge is not labeled with the silent action, we have to analyze which portion of the global + // variables was written by any of the updates and make all update results equal w.r.t. this set. If + // the edge is labeled with the silent action, we can already multiply the identities of all global variables. + if (edge.getActionId() != this->model.getSilentActionIndex()) { + for (auto const& edgeDestinationDd : destinationDds) { + globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); + } + } else { + globalVariablesInSomeUpdate = this->variables.allGlobalVariables; + } - // If there is no such state, continue with the next possible number of choices. - if (equalsNumberOfChoicesDd.isZero()) { - continue; + // Then, multiply the missing identities. + for (auto& destinationDd : destinationDds) { + std::set missingIdentities; + std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD."); + destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable); + } + } + + // Now combine the destination DDs to the edge DD. + storm::dd::Add transitions = this->variables.manager->template getAddZero(); + for (auto const& destinationDd : destinationDds) { + transitions += destinationDd.transitions; + } + + // Add the source location and the guard. + transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd() * guard; + + // If we multiply the ranges of global variables, make sure everything stays within its bounds. + if (!globalVariablesInSomeUpdate.empty()) { + transitions *= this->variables.globalVariableRanges; + } + + // If the edge has a rate, we multiply it to the DD. + if (edge.hasRate()) { + transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); + } + + return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); + } else { + return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); + } + } + + ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) { + // Translate the individual edges. + std::vector edgeDds; + for (auto const& edge : automaton.getEdges()) { + if (edge.getActionId() == actionIndex) { + edgeDds.push_back(buildEdgeDd(automaton, edge)); } + } + + // Now combine the edges to a single action. + if (!edgeDds.empty()) { + switch (this->model.getModelType()){ + case storm::jani::ModelType::DTMC: + case storm::jani::ModelType::CTMC: + return combineEdgesToActionMarkovChain(edgeDds); + break; + case storm::jani::ModelType::MDP: + return combineEdgesToActionMdp(edgeDds, localNondeterminismVariableOffset); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "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()); + } + } + + ActionDd combineEdgesToActionMarkovChain(std::vector const& edgeDds) { + storm::dd::Bdd allGuards = this->variables.manager->getBddZero(); + storm::dd::Add allTransitions = this->variables.manager->template getAddZero(); + storm::dd::Bdd temporary; + + std::map> globalVariableToWritingFragment; + for (auto const& edgeDd : edgeDds) { + // Check for overlapping guards. + storm::dd::Bdd guardBdd = edgeDd.guard.toBdd(); + temporary = guardBdd && allGuards; + + // Issue a warning if there are overlapping guards in a DTMC. + STORM_LOG_WARN_COND(temporary.isZero() || this->model.getModelType() == storm::jani::ModelType::CTMC, "Guard of a command overlaps with previous guards."); - // Reset the previously used intermediate storage. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = variables.manager->template getAddZero(); - remainingDds[j] = equalsNumberOfChoicesDd; + // Add the elements of the current edge to the global ones. + allGuards |= guardBdd; + allTransitions += edgeDd.transitions; + + // Keep track of the fragment that is writing global variables. + for (auto const& variable : edgeDd.writtenGlobalVariables) { + auto it = globalVariableToWritingFragment.find(variable); + if (it != globalVariableToWritingFragment.end()) { + it->second |= guardBdd; + } else { + globalVariableToWritingFragment[variable] = guardBdd; + } + } + } + + return ActionDd(allGuards.template toAdd(), allTransitions, 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 { + auto it = globalVariableToWritingFragment.find(variable); + if (it != globalVariableToWritingFragment.end()) { + it->second |= partToAdd; + } else { + globalVariableToWritingFragment.emplace(variable, partToAdd); + } + } + + std::map> joinVariableWritingFragmentMaps(std::map> const& globalVariableToWritingFragment1, std::map> const& globalVariableToWritingFragment2) { + std::map> result = globalVariableToWritingFragment1; + + for (auto const& entry : globalVariableToWritingFragment2) { + auto resultIt = result.find(entry.first); + if (resultIt != result.end()) { + resultIt->second |= entry.second; + } else { + result[entry.first] = entry.second; } + } + + return result; + } + + ActionDd combineEdgesBySummation(storm::dd::Add const& guard, std::vector const& edges) { + storm::dd::Add transitions = this->variables.manager->template getAddZero(); + std::map> globalVariableToWritingFragment; + for (auto const& edge : edges) { + transitions += edge.transitions; + for (auto const& variable : edge.writtenGlobalVariables) { + addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, edge.guard.toBdd()); + } + } + return ActionDd(guard, transitions, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); + } + + ActionDd combineEdgesToActionMdp(std::vector const& edges, 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(); + for (auto const& edge : edges) { + sumOfGuards += edge.guard; + allGuards |= edge.guard.toBdd(); + } + uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); + STORM_LOG_TRACE("Found " << maxChoices << " 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(), edges); + } else { + // Calculate number of required variables to encode the nondeterminism. + uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - for (std::size_t j = 0; j < edges.size(); ++j) { - // 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 = edges[j].guardDd.toBdd() && equalsNumberOfChoicesDd; + storm::dd::Add allEdges = this->variables.manager->template getAddZero(); + std::map> globalVariableToWritingFragment; + + storm::dd::Bdd equalsNumberOfChoicesDd; + std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); + std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); + + 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))); - // If there is no such state, continue with the next command. - if (guardChoicesIntersection.isZero()) { + // If there is no such state, continue with the next possible number of choices. + if (equalsNumberOfChoicesDd.isZero()) { continue; } - // Split the currentChoices nondeterministic choices. - for (uint_fast64_t k = 0; k < currentChoices; ++k) { - // Calculate the overlapping part of command guard and the remaining DD. - storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; - - // Check if we can add some overlapping parts to the current index. - if (!remainingGuardChoicesIntersection.isZero()) { - // Remove overlapping parts from the remaining DD. - remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; - - // Combine the overlapping part of the guard with command updates and add it to the resulting DD. - choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * edges[j].transitionsDd; - } + // Reset the previously used intermediate storage. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + choiceDds[j] = this->variables.manager->template getAddZero(); + remainingDds[j] = equalsNumberOfChoicesDd; + } + + for (std::size_t j = 0; j < edges.size(); ++j) { + EdgeDd const& currentEdge = edges[j]; - // Remove overlapping parts from the command guard DD - guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; + // 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; - // If the guard DD has become equivalent to false, we can stop here. + // If there is no such state, continue with the next command. if (guardChoicesIntersection.isZero()) { - break; + continue; + } + + // Split the currentChoices nondeterministic choices. + for (uint_fast64_t k = 0; k < currentChoices; ++k) { + // Calculate the overlapping part of command guard and the remaining DD. + storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; + + // Check if we can add some overlapping parts to the current index. + if (!remainingGuardChoicesIntersection.isZero()) { + // Remove overlapping parts from the remaining DD. + remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; + + // Combine the overlapping part of the guard with command updates and add it to the resulting DD. + choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * currentEdge.transitions; + + // Keep track of the written global variables of the fragment. + for (auto const& variable : currentEdge.writtenGlobalVariables) { + addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, remainingGuardChoicesIntersection && encodeIndex(j, 0, numberOfBinaryVariables, this->variables).toBdd()); + } + } + + // Remove overlapping parts from the command guard DD + guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; + + // If the guard DD has become equivalent to false, we can stop here. + if (guardChoicesIntersection.isZero()) { + break; + } } } + + // Add the meta variables that encode the nondeterminisim to the different choices. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j]; + } + + // Delete currentChoices out of overlapping DD + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } - // Add the meta variables that encode the nondeterminisim to the different choices. - for (uint_fast64_t j = 0; j < currentChoices; ++j) { - allEdges += encodeIndex(j, 0, numberOfBinaryVariables, variables) * choiceDds[j]; - } - - // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); + return ActionDd(allGuards.template toAdd(), allEdges, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } + } + + AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset) { + AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); - return std::make_pair(numberOfBinaryVariables, allEdges); + storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); + for (auto const& action : this->model.getActions()) { + uint64_t actionIndex = this->model.getActionIndex(action.getName()); + + result.actionIndexToAction[actionIndex] = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); + } + return result; } - } + + ComposerResult buildSystem(AutomatonDd& automatonDd) { + // FIXME: do the real thing. + return ComposerResult(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), 0); + } + + }; template - BuilderResult buildSystemFromSingleAutomaton(storm::jani::Model const& model, AutomatonDd& automatonDd, CompositionVariables const& variables) { - // If the model is an MDP, we need to encode the nondeterminism using additional variables. - if (model.getModelType() == storm::jani::ModelType::MDP) { - std::map>> actionIndexToUsedVariablesAndDd; - - // Combine the edges of each action individually and keep track of how many local nondeterminism variables - // were used. - uint64_t highestNumberOfUsedNondeterminismVariables = 0; - for (auto& action : automatonDd.actionIndexToEdges) { - std::pair> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second, variables); - actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); - highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); - } - - storm::dd::Add result = variables.manager->template getAddZero(); - for (auto const& element : actionIndexToUsedVariablesAndDd) { - result += element.second.second * encodeAction(element.first, variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, variables); + storm::dd::Add encodeAction(boost::optional const& actionIndex, CompositionVariables const& variables) { + storm::dd::Add encoding = variables.manager->template getAddOne(); + + for (auto it = variables.actionVariablesMap.rbegin(), ite = variables.actionVariablesMap.rend(); it != ite; ++it) { + if (actionIndex && it->first == actionIndex.get()) { + encoding *= variables.manager->getEncoding(it->second, 1).template toAdd(); + } else { + encoding *= variables.manager->getEncoding(it->second, 0).template toAdd(); } - - return BuilderResult(result, result.sumAbstract(variables.columnMetaVariables), highestNumberOfUsedNondeterminismVariables); - } else if (model.getModelType() == storm::jani::ModelType::DTMC || model.getModelType() == storm::jani::ModelType::CTMC) { - storm::dd::Add result = variables.manager->template getAddZero(); - for (auto const& action : automatonDd.actionIndexToEdges) { - result += combineEdgesBySummation(action.second, variables); + } + + return encoding; + } + + template + storm::dd::Add encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables const& variables) { + storm::dd::Add result = variables.manager->template getAddZero(); + + std::map metaVariableNameToValueMap; + for (uint_fast64_t i = 0; i < numberOfLocalNondeterminismVariables; ++i) { + if (index & (1ull << (numberOfLocalNondeterminismVariables - i - 1))) { + metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 1); + } else { + metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0); } - return BuilderResult(result, result.sumAbstract(variables.columnMetaVariables)); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + result.setValue(metaVariableNameToValueMap, 1); + return result; } template @@ -908,16 +1540,16 @@ namespace storm { } template - void postprocessVariables(storm::jani::ModelType const& modelType, BuilderResult& system, CompositionVariables& variables) { + void postprocessVariables(storm::jani::ModelType const& modelType, ComposerResult& system, CompositionVariables& variables) { // Add all action/row/column variables to the DD. If we omitted multiplying edges in the construction, this will // introduce the variables so they can later be abstracted without raising an error. - system.transitionsDd.addMetaVariables(variables.rowMetaVariables); - system.transitionsDd.addMetaVariables(variables.columnMetaVariables); + system.transitions.addMetaVariables(variables.rowMetaVariables); + system.transitions.addMetaVariables(variables.columnMetaVariables); // If the model is an MDP, we also add all action variables. if (modelType == storm::jani::ModelType::MDP) { for (auto const& actionVariablePair : variables.actionVariablesMap) { - system.transitionsDd.addMetaVariable(actionVariablePair.second); + system.transitions.addMetaVariable(actionVariablePair.second); } } @@ -929,10 +1561,10 @@ namespace storm { } template - void postprocessSystem(storm::jani::Model const& model, BuilderResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + void postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { - system.transitionsDd = system.transitionsDd / system.stateActionDd; + system.transitions = system.transitions / system.stateActionDd; } // If we were asked to treat some states as terminal states, we cut away their transitions now. @@ -951,7 +1583,7 @@ namespace storm { terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); } - system.transitionsDd *= (!terminalStatesBdd).template toAdd(); + system.transitions *= (!terminalStatesBdd).template toAdd(); } } @@ -1013,27 +1645,6 @@ namespace storm { } } - template - class SeparateEdgesSystemBuilder { - public: - SeparateEdgesSystemBuilder(storm::jani::Model const& model, CompositionVariables const& variables) : model(model), variables(variables) { - // Intentional - } - - BuilderResult build() { - // Compose the automata to a single automaton. - AutomatonComposer composer(this->model, variables); - AutomatonDd globalAutomaton = composer.compose(); - - // Combine the edges of the single automaton to the full system DD. - return buildSystemFromSingleAutomaton(this->model, globalAutomaton, variables); - } - - private: - storm::jani::Model const& model; - CompositionVariables const& variables; - }; - template std::shared_ptr> DdJaniModelBuilder::translate() { // Create all necessary variables. @@ -1041,8 +1652,9 @@ namespace storm { CompositionVariables variables = variableCreator.create(); // Create a builder to compose and build the model. - SeparateEdgesSystemBuilder builder(*this->model, variables); - BuilderResult system = builder.build(); +// SeparateEdgesSystemComposer composer(*this->model, variables); + CombinedEdgesSystemComposer composer(*this->model, variables); + ComposerResult system = composer.compose(); // Postprocess the variables in place. postprocessVariables(this->model->getModelType(), system, variables); @@ -1057,7 +1669,7 @@ namespace storm { modelComponents.initialStates = computeInitialStates(*this->model, variables); // Perform reachability analysis to obtain reachable states. - storm::dd::Bdd transitionMatrixBdd = system.transitionsDd.notZero(); + storm::dd::Bdd transitionMatrixBdd = system.transitions.notZero(); if (this->model->getModelType() == storm::jani::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables); } @@ -1065,7 +1677,7 @@ namespace storm { // Cut transitions to reachable states. storm::dd::Add reachableStatesAdd = modelComponents.reachableStates.template toAdd(); - modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd; + modelComponents.transitionMatrix = system.transitions * reachableStatesAdd; system.stateActionDd *= reachableStatesAdd; // Fix deadlocks if existing. diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index f03ca33a4..bd2d89aa7 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -788,7 +788,7 @@ namespace storm { STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards."); allGuards += commandDd.guardDd; - allCommands += commandDd.guardDd * commandDd.transitionsDd; + allCommands += commandDd.transitionsDd; } return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); @@ -873,7 +873,7 @@ namespace storm { continue; } - // Split the currentChoices nondeterministic choices. + // Split the nondeterministic choices. for (uint_fast64_t k = 0; k < currentChoices; ++k) { // Calculate the overlapping part of command guard and the remaining DD. storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k];