diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 94df8a2f9..bf4725841 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -172,14 +172,15 @@ namespace storm { template class CompositionVariableCreator : public storm::jani::CompositionVisitor { public: - CompositionVariableCreator(storm::jani::Model const& model) : model(model) { + CompositionVariableCreator(storm::jani::Model const& model) : model(model), automata() { // Intentionally left empty. } CompositionVariables create() { - // First, check whether every automaton appears exactly once in the system composition. + // First, check whether every automaton appears exactly once in the system composition. Simultaneously, + // we determine the set of non-silent actions used by the composition. automata.clear(); - this->model.getSystemComposition().accept(*this, boost::none); + nonSilentActions = boost::any_cast>(this->model.getSystemComposition().accept(*this, boost::none)); STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata."); // Then, check that the model does not contain unbounded integer or non-transient real variables. @@ -193,25 +194,64 @@ namespace storm { } // Based on this assumption, we create the variables. - return createVariables(); + return createVariables(nonSilentActions); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { auto it = automata.find(composition.getAutomatonName()); STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times."); automata.insert(it, composition.getAutomatonName()); - return boost::none; + + // Compute the set of actions used by this automaton. + std::set actionIndices = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices(); + std::set result; + for (auto const& index : actionIndices) { + result.insert(this->model.getAction(index).getName()); + } + return result; } boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - composition.getSubcomposition().accept(*this, boost::none); - return boost::none; + std::set usedActions = boost::any_cast>(composition.getSubcomposition().accept(*this, boost::none)); + + std::set newUsedActions; + for (auto const& action : usedActions) { + auto it = composition.getRenaming().find(action); + if (it != composition.getRenaming().end()) { + if (it->second) { + newUsedActions.insert(it->second.get()); + } + } else { + newUsedActions.insert(action); + } + } + + return newUsedActions; } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - composition.getLeftSubcomposition().accept(*this, boost::none); - composition.getRightSubcomposition().accept(*this, boost::none); - return boost::none; + std::vector> subresults; + for (auto const& subcomposition : composition.getSubcompositions()) { + subresults.push_back(boost::any_cast>(subcomposition->accept(*this, boost::none))); + } + + // Determine all actions that do not take part in synchronization vectors. + std::set result; + for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) { + std::set actionsInSynch; + for (auto const& synchVector : composition.getSynchronizationVectors()) { + actionsInSynch.insert(synchVector.getInput()[subresultIndex]); + } + + std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin())); + } + + // Now add all outputs of synchronization vectors. + for (auto const& synchVector : composition.getSynchronizationVectors()) { + result.insert(synchVector.getOutput()); + } + + return result; } private: @@ -350,6 +390,7 @@ namespace storm { storm::jani::Model const& model; std::set automata; + std::set nonSilentActions; }; template @@ -488,434 +529,434 @@ namespace storm { return result; } - template - class SeparateEdgesSystemComposer : 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 = {}, 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. - } - - ComposerResult compose() override { - AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); - return buildSystemFromAutomaton(globalAutomaton); - } - - boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - return buildAutomatonDd(composition.getAutomatonName()); - } - - boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { - AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); - - // 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."); - } - } - - // Finally, apply the renaming. - AutomatonDd result(subautomaton.identity); - for (auto const& actionEdges : subautomaton.actionIndexToEdges) { - auto it = renamingIndexToIndex.find(actionEdges.first); - if (it != renamingIndexToIndex.end()) { - // If we are to rename the action, do so. - result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); - } else { - // Otherwise copy over the edges. - result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); - } - } - return result; - } - - 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)); - - // 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."); - } - } - - // Perform the composition. - - // First, consider all actions in the left subcomposition. - 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. - if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { - auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); - if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { - for (auto const& edge1 : actionEdges.second) { - for (auto const& edge2 : rightIt->second) { - EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); - if (!edgeDd.guard.isZero()) { - result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); - } - index++; - } - } - } - } else { - // Extend all edges by the missing identity (unsynchronizing) and copy them over. - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); - } - } - } - - // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because - // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, - // such transitions can not be taken and we can drop them. - for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { - if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { - for (auto const& edge : actionEdges.second) { - result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); - } - } - } - - return result; - } - - private: - 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) { - // Complete all edges by adding the missing global variable identities. - for (auto& edge : edges) { - edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); - } - - // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Add sumOfGuards = this->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."); - - // 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, this->variables.manager->template getAddZero()); - } else if (maxChoices == 1) { - return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); - } else { - // Calculate number of required variables to encode the nondeterminism. - uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - - storm::dd::Add allEdges = this->variables.manager->template getAddZero(); - - 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 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] = this->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, this->variables) * choiceDds[j]; - } - - // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); - } - - return std::make_pair(numberOfBinaryVariables, allEdges); - } - } - - storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { - // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. - storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); - for (auto const& action : actionIndexToEdges) { - for (auto const& edge : action.second) { - if (!edge.globalVariablesWrittenMultipleTimes.empty()) { - for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { - STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); - illegalFragment |= edge.guard.toBdd(); - } - } - } - } - return illegalFragment; - } - - ComposerResult buildSystemFromAutomaton(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; - - // 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); - actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); - highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); - } - - storm::dd::Add result = this->variables.manager->template getAddZero(); - for (auto const& element : actionIndexToUsedVariablesAndDd) { - result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); - } - - return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 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, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); - } - - 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; - - // 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; - } - - // 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) { - 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."); - - 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.getActionIndex() != this->model.getSilentActionIndex()) { - for (auto const& edgeDestinationDd : destinationDds) { - globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); - } - } else { - globalVariablesInSomeUpdate = this->variables.allGlobalVariables; - } - - // 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.getSourceLocationIndex()).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()); - } - } - - /*! - * Builds the DD for the automaton with the given name. - */ - 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.guard.isZero()) { - result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); - } - } - - return result; - } - }; +// template +// class SeparateEdgesSystemComposer : 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 = {}, 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. +// } +// +// ComposerResult compose() override { +// AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); +// return buildSystemFromAutomaton(globalAutomaton); +// } +// +// boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { +// return buildAutomatonDd(composition.getAutomatonName()); +// } +// +// boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override { +// AutomatonDd subautomaton = boost::any_cast(composition.getSubcomposition().accept(*this, boost::none)); +// +// // 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."); +// } +// } +// +// // Finally, apply the renaming. +// AutomatonDd result(subautomaton.identity); +// for (auto const& actionEdges : subautomaton.actionIndexToEdges) { +// auto it = renamingIndexToIndex.find(actionEdges.first); +// if (it != renamingIndexToIndex.end()) { +// // If we are to rename the action, do so. +// result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end()); +// } else { +// // Otherwise copy over the edges. +// result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end()); +// } +// } +// return result; +// } +// +// 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)); +// +// // 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."); +// } +// } +// +// // Perform the composition. +// +// // First, consider all actions in the left subcomposition. +// 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. +// if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { +// auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first); +// if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { +// for (auto const& edge1 : actionEdges.second) { +// for (auto const& edge2 : rightIt->second) { +// EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); +// if (!edgeDd.guard.isZero()) { +// result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); +// } +// index++; +// } +// } +// } +// } else { +// // Extend all edges by the missing identity (unsynchronizing) and copy them over. +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity)); +// } +// } +// } +// +// // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because +// // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none, +// // such transitions can not be taken and we can drop them. +// for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) { +// if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) { +// for (auto const& edge : actionEdges.second) { +// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity)); +// } +// } +// } +// +// return result; +// } +// +// private: +// 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) { +// // Complete all edges by adding the missing global variable identities. +// for (auto& edge : edges) { +// edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables); +// } +// +// // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. +// storm::dd::Add sumOfGuards = this->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."); +// +// // 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, this->variables.manager->template getAddZero()); +// } else if (maxChoices == 1) { +// return std::make_pair(0, combineEdgesBySummation(edges, this->variables)); +// } else { +// // Calculate number of required variables to encode the nondeterminism. +// uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); +// +// storm::dd::Add allEdges = this->variables.manager->template getAddZero(); +// +// 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 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] = this->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, this->variables) * choiceDds[j]; +// } +// +// // Delete currentChoices out of overlapping DD +// sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); +// } +// +// return std::make_pair(numberOfBinaryVariables, allEdges); +// } +// } +// +// storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { +// // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. +// storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); +// for (auto const& action : actionIndexToEdges) { +// for (auto const& edge : action.second) { +// if (!edge.globalVariablesWrittenMultipleTimes.empty()) { +// for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { +// STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); +// illegalFragment |= edge.guard.toBdd(); +// } +// } +// } +// } +// return illegalFragment; +// } +// +// ComposerResult buildSystemFromAutomaton(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; +// +// // 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); +// actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd); +// highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first); +// } +// +// storm::dd::Add result = this->variables.manager->template getAddZero(); +// for (auto const& element : actionIndexToUsedVariablesAndDd) { +// result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); +// } +// +// return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 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, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); +// } +// +// 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; +// +// // 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; +// } +// +// // 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) { +// 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."); +// +// 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.getActionIndex() != this->model.getSilentActionIndex()) { +// for (auto const& edgeDestinationDd : destinationDds) { +// globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); +// } +// } else { +// globalVariablesInSomeUpdate = this->variables.allGlobalVariables; +// } +// +// // 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.getSourceLocationIndex()).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()); +// } +// } +// +// /*! +// * Builds the DD for the automaton with the given name. +// */ +// 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.guard.isZero()) { +// result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd); +// } +// } +// +// return result; +// } +// }; template class CombinedEdgesSystemComposer : public SystemComposer { @@ -1019,9 +1060,11 @@ namespace storm { }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionToIndex(model.getActionToIndexMap()) { // Intentionally left empty. } + + std::unordered_map actionToIndex; ComposerResult compose() override { std::map actionIndexToLocalNondeterminismVariableOffset; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 9c618a838..d3c68cd39 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -391,6 +391,14 @@ namespace storm { edge.finalize(containingModel); } } + + std::set Automaton::getUsedActionIndices() const { + std::set result; + for (auto const& edge : edges) { + result.insert(edge.getActionIndex()); + } + return result; + } } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index c6219aa1e..f2c784084 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -294,6 +294,11 @@ namespace storm { */ void finalize(Model const& containingModel); + /*! + * Retrieves the action indices appearing at some edge of the automaton. + */ + std::set getUsedActionIndices() const; + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index d6b661b53..b07911ca6 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -6,11 +6,11 @@ namespace storm { namespace jani { - CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) { + CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), nonStandardParallelComposition(false) { // Intentionally left empty. } - CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) { + CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenameComposition, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), nonStandardParallelComposition(nonStandardParallelComposition) { // Intentionally left empty. } @@ -49,12 +49,12 @@ namespace storm { return renameComposition; } - void CompositionInformation::setContainsRestrictedParallelComposition() { - restrictedParallelComposition = true; + void CompositionInformation::setContainsNonStandardParallelComposition() { + nonStandardParallelComposition = true; } - bool CompositionInformation::containsRestrictedParallelComposition() const { - return restrictedParallelComposition; + bool CompositionInformation::containsNonStandardParallelComposition() const { + return nonStandardParallelComposition; } std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { @@ -90,30 +90,61 @@ namespace storm { boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) { CompositionInformation subresult = boost::any_cast(composition.getSubcomposition().accept(*this, data)); std::set nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming()); - return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition()); + return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsNonStandardParallelComposition()); } boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { - CompositionInformation left = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)); - CompositionInformation right = boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); - - // Join the information from both sides. - bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition(); - bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition(); - std::map joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap()); + std::vector subinformation; - std::set nonsilentActions; - std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin())); + for (auto const& subcomposition : composition.getSubcompositions()) { + subinformation.push_back(boost::any_cast(subcomposition->accept(*this, data))); + } + + std::map joinedAutomatonToMultiplicityMap; + bool containsRenameComposition = false; + bool containsNonStandardParallelComposition = false; + + for (auto const& subinfo : subinformation) { + containsRenameComposition |= subinfo.containsRenameComposition(); + containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition(); + joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap()); + + } - // If there was no restricted parallel composition yet, maybe the current composition is one, so check it. - if (!containsRestrictedParallelComposition) { - std::set commonNonsilentActions; - std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin())); - bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end()); - containsRestrictedParallelComposition = !allCommonActionsIncluded; + // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have + // the non-silent actions that are referred to. + std::set effectiveSynchVectors; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + effectiveSynchVectors.insert(synchVectorIndex); } - return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition); + // Now compute non-silent actions. + std::set nonsilentActions; + for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) { + auto const& subinfo = subinformation[infoIndex]; + + std::set enabledSynchVectors; + for (auto const& nonsilentAction : subinfo.getNonsilentActions()) { + bool appearsInSomeSynchVector = false; + for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); + if (synchVector.getInput(infoIndex) == nonsilentAction) { + appearsInSomeSynchVector = true; + enabledSynchVectors.insert(synchVectorIndex); + } + } + + if (!appearsInSomeSynchVector) { + nonsilentActions.insert(nonsilentAction); + } + } + + std::set newEffectiveSynchVectors; + std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); + effectiveSynchVectors = std::move(newEffectiveSynchVectors); + } + + return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsRenameComposition, containsNonStandardParallelComposition); } } diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 59a422a41..786078e2e 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -16,7 +16,7 @@ namespace storm { class CompositionInformation { public: CompositionInformation(); - CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition); + CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool containsRenaming, bool nonStandardParallelComposition); void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); @@ -27,8 +27,8 @@ namespace storm { void setContainsRenameComposition(); bool containsRenameComposition() const; - void setContainsRestrictedParallelComposition(); - bool containsRestrictedParallelComposition() const; + void setContainsNonStandardParallelComposition(); + bool containsNonStandardParallelComposition() const; static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); std::map const& getAutomatonToMultiplicityMap() const; @@ -43,8 +43,8 @@ namespace storm { /// A flag indicating whether the composition contains a renaming composition. bool renameComposition; - /// A flag indicating whether the composition contains - bool restrictedParallelComposition; + /// A flag indicating whether the composition contains any non-standard parallel composition. + bool nonStandardParallelComposition; }; class CompositionInformationVisitor : public CompositionVisitor { diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index fc170ac58..5f6d3e6eb 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -75,6 +75,10 @@ namespace storm { return it->second; } + std::unordered_map const& Model::getActionToIndexMap() const { + return actionToIndex; + } + std::vector const& Model::getActions() const { return actions; } @@ -448,7 +452,7 @@ namespace storm { bool Model::hasDefaultComposition() const { CompositionInformationVisitor visitor; CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this); - if (info.containsRestrictedParallelComposition() || info.containsRenameComposition()) { + if (info.containsNonStandardParallelComposition() || info.containsRenameComposition()) { return false; } for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 2fc06b18f..d955bb0e7 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -65,6 +65,11 @@ namespace storm { */ uint64_t getActionIndex(std::string const& name) const; + /*! + * Retrieves the mapping from action names to their indices. + */ + std::unordered_map const& getActionToIndexMap() const; + /** * Adds an action to the model. * diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index f767e32cc..0f8a41d63 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -1,32 +1,132 @@ #include "src/storage/jani/ParallelComposition.h" +#include + #include +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace jani { - ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) { + SynchronizationVector::SynchronizationVector(std::vector const& input, std::string const& output) : input(input), output(output) { // Intentionally left empty. } - Composition const& ParallelComposition::getLeftSubcomposition() const { - return *leftSubcomposition; + std::size_t SynchronizationVector::size() const { + return input.size(); + } + + std::vector const& SynchronizationVector::getInput() const { + return input; + } + + std::string const& SynchronizationVector::getInput(uint64_t index) const { + return input[index]; + } + + std::string const& SynchronizationVector::getOutput() const { + return output; } - Composition const& ParallelComposition::getRightSubcomposition() const { - return *rightSubcomposition; + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) { + bool first = true; + stream << "("; + for (auto const& element : synchronizationVector.getInput()) { + if (!first) { + stream << ", "; + } + stream << element; + } + stream << ") -> " << synchronizationVector.getOutput(); + return stream; } - std::set const& ParallelComposition::getSynchronizationAlphabet() const { - return alphabet; + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + + for (auto const& vector : this->synchronizationVectors) { + STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); + } } + + ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() { + STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition."); + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + ParallelComposition::ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet) { + subcompositions.push_back(leftSubcomposition); + subcompositions.push_back(rightSubcomposition); + + // Manually construct the synchronization vectors for all elements of the synchronization alphabet. + for (auto const& action : synchronizationAlphabet) { + synchronizationVectors.emplace_back(std::vector(this->subcompositions.size(), action), action); + } + } + + Composition const& ParallelComposition::getSubcomposition(uint64_t index) const { + return *subcompositions[index]; + } + + std::vector> const& ParallelComposition::getSubcompositions() const { + return subcompositions; + } + + uint64_t ParallelComposition::getNumberOfSubcompositions() const { + return subcompositions.size(); + } + + SynchronizationVector const& ParallelComposition::getSynchronizationVector(uint64_t index) const { + return synchronizationVectors[index]; + } + + std::vector const& ParallelComposition::getSynchronizationVectors() const { + return synchronizationVectors; + } + + std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const { + return synchronizationVectors.size(); + } + + bool ParallelComposition::checkSynchronizationVectors() const { + for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { + std::set actions; + for (auto const& vector : synchronizationVectors) { + std::string const& action = vector.getInput(inputIndex); + STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vector."); + actions.insert(action); + } + } + } + boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } void ParallelComposition::write(std::ostream& stream) const { - stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition(); + std::vector synchronizationVectorsAsStrings; + for (auto const& synchronizationVector : synchronizationVectors) { + std::stringstream tmpStream; + tmpStream << synchronizationVector; + synchronizationVectorsAsStrings.push_back(tmpStream.str()); + } + + bool first = true; + stream << "("; + for (auto const& subcomposition : subcompositions) { + if (!first) { + stream << " || "; + first = false; + } + stream << *subcomposition; + } + stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]"; } } diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h index 4b7ff69be..0ae525714 100644 --- a/src/storage/jani/ParallelComposition.h +++ b/src/storage/jani/ParallelComposition.h @@ -2,47 +2,95 @@ #include #include +#include +#include #include "src/storage/jani/Composition.h" namespace storm { namespace jani { + class SynchronizationVector { + public: + SynchronizationVector(std::vector const& input, std::string const& output); + + std::size_t size() const; + std::vector const& getInput() const; + std::string const& getInput(uint64_t index) const; + std::string const& getOutput() const; + + private: + /// The input to the synchronization. + std::vector input; + + /// The output of the synchronization. + std::string output; + }; + + std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector); + class ParallelComposition : public Composition { public: /*! - * Creates a parallel composition of the two subcompositions. + * Creates a parallel composition of the subcompositions and the provided synchronization vectors. */ - ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& alphabet = {}); - + ParallelComposition(std::vector> const& subcompositions, std::vector const& synchronizationVectors); + /*! - * Retrieves the left subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getLeftSubcomposition() const; + ParallelComposition(std::vector> const& subcompositions, std::set const& synchronizationAlphabet); /*! - * Retrieves the right subcomposition. + * Creates a parallel composition of the subcompositions over the provided synchronization alphabet. */ - Composition const& getRightSubcomposition() const; + ParallelComposition(std::shared_ptr const& leftSubcomposition, std::shared_ptr const& rightSubcomposition, std::set const& synchronizationAlphabet); /*! - * Retrieves the alphabet of actions over which to synchronize the automata. + * Retrieves the subcomposition with the given index. */ - std::set const& getSynchronizationAlphabet() const; + Composition const& getSubcomposition(uint64_t index) const; + + /*! + * Retrieves the subcompositions of the parallel composition. + */ + std::vector> const& getSubcompositions() const; + + /*! + * Retrieves the number of subcompositions of this parallel composition. + */ + uint64_t getNumberOfSubcompositions() const; + + /*! + * Retrieves the synchronization vector with the given index. + */ + SynchronizationVector const& getSynchronizationVector(uint64_t index) const; + + /*! + * Retrieves the synchronization vectors of the parallel composition. + */ + std::vector const& getSynchronizationVectors() const; + + /*! + * Retrieves the number of synchronization vectors. + */ + std::size_t getNumberOfSynchronizationVectors() const; virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; virtual void write(std::ostream& stream) const override; private: - // The left subcomposition. - std::shared_ptr leftSubcomposition; + /*! + * Checks the synchronization vectors for validity. + */ + bool checkSynchronizationVectors() const; - // The right subcomposition. - std::shared_ptr rightSubcomposition; + /// The subcompositions. + std::vector> subcompositions; - // The alphabet of actions over which to synchronize. - std::set alphabet; + /// The synchronization vectors of the parallel composition. + std::vector synchronizationVectors; }; } diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 33ad88fef..08819964a 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -137,7 +137,7 @@ namespace storm { } STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented."); } - STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); + STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // previously built mapping to make variables global that are read by more than one module.