diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 889c5439b..966113a02 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -530,7 +530,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) { + 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) { // Intentionally left empty. } @@ -550,6 +550,14 @@ namespace storm { return ActionDd(guard, transitions * factor, transientEdgeAssignments, localNondeterminismVariables, variableToWritingFragment, illegalFragment); } + bool isInputEnabled() const { + return inputEnabled; + } + + void setIsInputEnabled() { + inputEnabled = true; + } + // A DD that represents all states that have this edge enabled. storm::dd::Add guard; @@ -569,6 +577,9 @@ namespace storm { // 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; + + // A flag storing whether this action is input-enabled. + bool inputEnabled; }; // This structure represents a subcomponent of a composition. @@ -631,7 +642,13 @@ namespace storm { 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::set inputEnabledActionIndices; + for (auto const& actionName : composition.getInputEnabledActions()) { + inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName)); + } + + return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices); } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { @@ -679,10 +696,15 @@ namespace storm { private: AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { + typedef storm::dd::Add IdentityAdd; + typedef std::pair ActionAndAutomatonIdentity; + typedef std::vector ActionAndAutomatonIdentities; + typedef std::vector>> SynchronizationVectorActionsAndIdentities; + AutomatonDd result(this->variables.manager->template getAddOne()); std::map> nonSynchronizingActions; - std::vector> synchronizationVectorActions(synchronizationVectors.size(), boost::none); + SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none); for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { AutomatonDd const& subautomaton = subautomata[automatonIndex]; @@ -703,12 +725,12 @@ namespace storm { if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) { if (automatonIndex == 0) { // Create a new action that is the identity over the first automaton. - synchronizationVectorActions[synchVectorIndex] = ActionDd(this->variables.manager->template getAddOne(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()); + synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(ActionDd(this->variables.manager->template getAddOne(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()), subautomaton.identity)}, this->variables.manager->template getAddOne()); } else { // If there is no action in the output spot, this means that some other subcomposition did // not provide the action necessary for the synchronization vector to resolve. if (synchronizationVectorActions[synchVectorIndex]) { - synchronizationVectorActions[synchVectorIndex].get().transitions *= subautomaton.identity; + synchronizationVectorActions[synchVectorIndex].get().second *= subautomaton.identity; } } } else { @@ -721,7 +743,7 @@ namespace storm { // If the action cannot be found, the particular spot in the output will be left empty. auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex] = inputActionIt->second; + synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(inputActionIt->second, subautomaton.identity)}, this->variables.manager->template getAddOne()); } } else { // If there is no action in the output spot, this means that some other subcomposition did @@ -729,7 +751,7 @@ namespace storm { if (synchronizationVectorActions[synchVectorIndex]) { auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex] = combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get(), inputActionIt->second); + synchronizationVectorActions[synchVectorIndex].get().first.push_back(std::make_pair(inputActionIt->second, subautomaton.identity)); } else { // If the current subcomposition does not provide the required action for the synchronization // vector, we clear the action. @@ -778,7 +800,7 @@ namespace storm { // If there is an action resulting from this combination of actions, add it to the output action. if (synchronizationVectorActions[synchVectorIndex]) { uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput()); - nonSynchronizingActions[outputActionIndex].push_back(synchronizationVectorActions[synchVectorIndex].get()); + nonSynchronizingActions[outputActionIndex].push_back(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second)); } } @@ -799,33 +821,101 @@ namespace storm { return result; } - ActionDd combineSynchronizingActions(ActionDd action1, ActionDd action2) { + ActionDd combineSynchronizingActions(std::vector>> const& actionsAndIdentities, storm::dd::Add const& nonSynchronizingAutomataIdentities) { + // If there is just one action, no need to combine anything. + if (actionsAndIdentities.size() == 1) { + return actionsAndIdentities.front().first; + } + + // If there are only input-enabled actions, we also need to build the disjunction of the guards. + bool allActionsInputEnabled = true; + for (auto const& actionIdentityPair : actionsAndIdentities) { + auto const& action = actionIdentityPair.first; + if (!action.isInputEnabled()) { + allActionsInputEnabled = false; + break; + } + } + boost::optional> guardDisjunction; + if (allActionsInputEnabled) { + guardDisjunction = this->variables.manager->getBddZero(); + } + + // Otherwise, construct the synchronization. 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()) { - auto action1LocalNondeterminismVariableSet = std::set(this->variables.localNondeterminismVariables.begin() + action1.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action1.getHighestLocalNondeterminismVariable()); - auto action2LocalNondeterminismVariableSet = std::set(this->variables.localNondeterminismVariables.begin() + action2.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action2.getHighestLocalNondeterminismVariable()); - illegalFragment |= it->second.existsAbstract(action1LocalNondeterminismVariableSet) && entry.second.existsAbstract(action2LocalNondeterminismVariableSet); - it->second &= entry.second; + std::map> globalVariableToWritingFragmentWithoutNondeterminism; + + storm::dd::Bdd guardConjunction = this->variables.manager->getBddOne(); + storm::dd::Add transitions = this->variables.manager->template getAddOne(); + std::map> transientEdgeAssignments; + + uint64_t lowestNondeterminismVariable = actionsAndIdentities.front().first.getLowestLocalNondeterminismVariable(); + uint64_t highestNondeterminismVariable = actionsAndIdentities.front().first.getHighestLocalNondeterminismVariable(); + + storm::dd::Bdd newIllegalFragment = this->variables.manager->getBddZero(); + for (auto const& actionIdentityPair : actionsAndIdentities) { + auto const& action = actionIdentityPair.first; + storm::dd::Bdd actionGuard = action.guard.toBdd(); + if (guardDisjunction) { + guardDisjunction.get() |= actionGuard; + } + + lowestNondeterminismVariable = std::min(lowestNondeterminismVariable, action.getLowestLocalNondeterminismVariable()); + highestNondeterminismVariable = std::max(highestNondeterminismVariable, action.getHighestLocalNondeterminismVariable()); + transientEdgeAssignments = joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments); + + 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) * actionIdentityPair.second); } else { - globalVariableToWritingFragment[entry.first] = entry.second; + transitions *= action.transitions; + } + + // Create a set of variables that is used as nondeterminism variables in this action. + auto nondetVariables = std::set(this->variables.localNondeterminismVariables.begin() + action.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action.getHighestLocalNondeterminismVariable()); + + for (auto const& entry : action.variableToWritingFragment) { + storm::dd::Bdd guardedWritingFragment = guardConjunction && entry.second; + + // Check whether there already is an entry for this variable in the mapping of global variables + // to their writing fragments. + auto globalFragmentIt = globalVariableToWritingFragment.find(entry.first); + if (globalFragmentIt != globalVariableToWritingFragment.end()) { + // If it does, take the conjunction of the entries and also of their versions without nondeterminism + // variables. + globalFragmentIt->second &= guardedWritingFragment; + illegalFragment |= globalVariableToWritingFragmentWithoutNondeterminism[entry.first] && guardedWritingFragment.existsAbstract(nondetVariables); + globalVariableToWritingFragmentWithoutNondeterminism[entry.first] |= guardedWritingFragment.existsAbstract(nondetVariables); + } else { + // If not, create the entry and also create a version of the entry that abstracts from the + // used nondeterminism variables. + globalVariableToWritingFragment[entry.first] = guardedWritingFragment; + globalVariableToWritingFragmentWithoutNondeterminism[entry.first] = guardedWritingFragment.existsAbstract(nondetVariables); + } + + // Join all individual illegal fragments so we can see whether any of these elements lie in the + // conjunction of all guards. + illegalFragment |= action.illegalFragment; } + + // Now go through all fragments that are not written by the current action and join them with the + // guard of the current action. + for (auto& entry : globalVariableToWritingFragment) { + if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end()) { + entry.second &= actionGuard; + } + } + + guardConjunction &= actionGuard; } - return ActionDd(combinedGuard.template toAdd(), action1.transitions * action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment); + // Cut the union of the illegal fragments to the conjunction of the guards since only these states have + // such a combined transition. + illegalFragment &= guardConjunction; + + return ActionDd(guardConjunction.template toAdd(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -1353,7 +1443,7 @@ namespace storm { } } - AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset) { + AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset, std::set const& inputEnabledActionIndices) { AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); @@ -1363,6 +1453,9 @@ namespace storm { continue; } ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); + if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) { + actionDd.setIsInputEnabled(); + } result.actionIndexToAction[actionIndex] = actionDd; result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable()));