diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 2c308559c..d9cb430ec 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -518,7 +518,7 @@ namespace storm { result.setValue(metaVariableNameToValueMap, 1); return result; } - + template class CombinedEdgesSystemComposer : public SystemComposer { public: @@ -606,9 +606,53 @@ namespace storm { bool inputEnabled; }; + struct ActionIdentification { + ActionIdentification(uint64_t actionIndex) : actionIndex(actionIndex), synchronizationVectorIndex(boost::none) { + // Intentionally left empty. + } + + ActionIdentification(uint64_t actionIndex, uint64_t synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) { + // Intentionally left empty. + } + + ActionIdentification(uint64_t actionIndex, boost::optional synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) { + // Intentionally left empty. + } + + bool operator==(ActionIdentification const& other) const { + bool result = actionIndex == other.actionIndex; + if (synchronizationVectorIndex) { + if (other.synchronizationVectorIndex) { + result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get(); + } else { + result = false; + } + } else { + if (other.synchronizationVectorIndex) { + result = false; + } + } + return result; + } + + uint64_t actionIndex; + boost::optional synchronizationVectorIndex; + }; + + struct ActionIdentificationHash { + std::size_t operator()(ActionIdentification const& identification) const { + std::size_t seed = 0; + boost::hash_combine(seed, identification.actionIndex); + if (identification.synchronizationVectorIndex) { + boost::hash_combine(seed, identification.synchronizationVectorIndex.get()); + } + return seed; + } + }; + // This structure represents a subcomponent of a composition. struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity, std::map> const& transientLocationAssignments = {}) : actionIndexToAction(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { + AutomatonDd(storm::dd::Add const& identity, std::map> const& transientLocationAssignments = {}) : actions(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { // Intentionally left empty. } @@ -633,8 +677,8 @@ namespace storm { setHighestLocalNondeterminismVariable(std::max(localNondeterminismVariables.second, getHighestLocalNondeterminismVariable())); } - // A mapping from action indices to the action DDs. - std::map actionIndexToAction; + // A mapping from action identifications to the action DDs. + std::unordered_map actions; // A mapping from transient variables to their location-based transient assignment values. std::map> transientLocationAssignments; @@ -644,7 +688,6 @@ namespace storm { // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index. std::pair localNondeterminismVariables; - }; CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { @@ -654,208 +697,192 @@ namespace storm { storm::jani::CompositionInformation const& actionInformation; ComposerResult compose() override { - std::map actionIndexToLocalNondeterminismVariableOffset; - for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { - actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; - } - actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::SILENT_ACTION_INDEX] = 0; - - AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); + STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions."); + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::any())); return buildSystemFromAutomaton(globalAutomaton); } + struct ActionInstantiation { + ActionInstantiation(uint64_t actionIndex, uint64_t synchronizationVectorIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) { + // Intentionally left empty. + } + + ActionInstantiation(uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) { + // Intentionally left empty. + } + + bool operator==(ActionInstantiation const& other) const { + bool result = actionIndex == other.actionIndex; + result &= localNondeterminismVariableOffset == other.localNondeterminismVariableOffset; + if (synchronizationVectorIndex) { + if (!other.synchronizationVectorIndex) { + result = false; + } else { + result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get(); + } + } else { + if (other.synchronizationVectorIndex) { + result = false; + } + } + return result; + } + + uint64_t actionIndex; + boost::optional synchronizationVectorIndex; + uint64_t localNondeterminismVariableOffset; + }; + + struct ActionInstantiationHash { + std::size_t operator()(ActionInstantiation const& instantiation) const { + std::size_t seed = 0; + boost::hash_combine(seed, instantiation.actionIndex); + boost::hash_combine(seed, instantiation.localNondeterminismVariableOffset); + if (instantiation.synchronizationVectorIndex) { + boost::hash_combine(seed, instantiation.synchronizationVectorIndex.get()); + } + return seed; + } + }; + + typedef std::map> ActionInstantiations; + boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + ActionInstantiations actionInstantiations; + if (data.empty()) { + // If no data was provided, this is the top level element in which case we build the full automaton. + for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { + actionInstantiations[actionIndex].emplace_back(actionIndex, 0); + } + actionInstantiations[storm::jani::Model::SILENT_ACTION_INDEX].emplace_back(storm::jani::Model::SILENT_ACTION_INDEX, 0); + } std::set inputEnabledActionIndices; for (auto const& actionName : composition.getInputEnabledActions()) { inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName)); } - return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices); + return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices); } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - + STORM_LOG_ASSERT(data.empty(), "Expected parallel composition to be on topmost level to be JANI compliant."); + + // Prepare storage for the subautomata of the composition. std::vector subautomata; + + // The outer loop iterates over the indices of the subcomposition, because the first subcomposition needs + // to be built before the second and so on. + uint64_t silentActionIndex = actionInformation.getActionIndex(storm::jani::Model::SILENT_ACTION_NAME); for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) { - // Prepare the new offset mapping. - std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + // Now build a new set of action instantiations for the current subcomposition index. + ActionInstantiations actionInstantiations; + actionInstantiations[silentActionIndex].emplace_back(silentActionIndex, 0); - if (subcompositionIndex == 0) { - for (auto const& synchVector : composition.getSynchronizationVectors()) { - auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput())); - STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << "."); - if (synchVector.getInput(0) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { - newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second; - } - } - } else { - // Based on the previous results, we need to update the offsets. - for (auto const& synchVector : composition.getSynchronizationVectors()) { - if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { - boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); - if (previousActionPosition) { - AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; + for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchronizationVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchronizationVectorIndex); + + // Determine the first participating subcomposition, because we need to build the corresponding action + // from all local nondeterminism variable offsets that the output action of the synchronization vector + // is required to have. + if (subcompositionIndex == synchVector.getPositionOfFirstParticipatingAction()) { + uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex)); + actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, 0); + } else if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { + uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex)); - std::string const& previousAction = synchVector.getInput(previousActionPosition.get()); - auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(previousAction)); - if (it != previousAutomatonDd.actionIndexToAction.end()) { - newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable(); - } else { - STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition."); - } - } - } + // If this subcomposition is participating in the synchronization vector, but it's not the first + // such subcomposition, then we have to retrieve the offset we need for the participating action + // by looking at the maximal offset used by the preceding participating action. + boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); + STORM_LOG_ASSERT(previousActionPosition, "Inconsistent information about synchronization vector."); + AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; + auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())), synchronizationVectorIndex)); + STORM_LOG_THROW(precedingActionIt != previousAutomatonDd.actions.end(), storm::exceptions::WrongFormatException, "Subcomposition does not have action that is mentioned in parallel composition."); + actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, precedingActionIt->second.getHighestLocalNondeterminismVariable()); } } - // Build the DD for the next element of the composition wrt. to the current offset mapping. - subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap))); + subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, actionInstantiations))); } - + return composeInParallel(subautomata, composition.getSynchronizationVectors()); } 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; - SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none); - for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { - AutomatonDd const& subautomaton = subautomata[automatonIndex]; - - // Add the transient assignments from the new subautomaton. - addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); - - // Initilize the used local nondeterminism variables appropriately. - if (automatonIndex == 0) { - result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable()); - result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable()); - } - - // Compose the actions according to the synchronization vectors. - std::set actionsInSynch; - for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { - auto const& synchVector = synchronizationVectors[synchVectorIndex]; - - if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) { - if (automatonIndex == 0) { - // Create a new action that is the identity over the first automaton. - 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().second *= subautomaton.identity; - } - } - } else { - // Determine the indices of input (at the current automaton position) and the output. - uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); - actionsInSynch.insert(inputActionIndex); - - // Either set the action (if it's the first of the ones to compose) or compose the actions directly. - if (automatonIndex == 0) { - // 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] = 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 - // not provide the action necessary for the synchronization vector to resolve. - if (synchronizationVectorActions[synchVectorIndex]) { - auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); - if (inputActionIt != subautomaton.actionIndexToAction.end()) { - 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. - synchronizationVectorActions[synchVectorIndex] = boost::none; - } - } - } - } - } - // Now treat all unsynchronizing actions. - if (automatonIndex == 0) { - // Since it's the first automaton, there is nothing to combine. - for (auto const& action : subautomaton.actionIndexToAction) { - if (actionsInSynch.find(action.first) == actionsInSynch.end()) { - nonSynchronizingActions[action.first].push_back(action.second); - } - } - } else { - // Extend all other non-synchronizing actions with the identity of the current subautomaton. - for (auto& actions : nonSynchronizingActions) { - for (auto& action : actions.second) { - STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition."); - action.transitions *= subautomaton.identity; - } - } - - // Extend the actions of the current subautomaton with the identity of the previous system and - // add it to the overall non-synchronizing action result. - for (auto const& action : subautomaton.actionIndexToAction) { - if (actionsInSynch.find(action.first) == actionsInSynch.end()) { - STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity."); - nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity)); - } - } - } + // Build the results of the synchronization vectors. + std::map> actions; + for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) { + auto const& synchVector = synchronizationVectors[synchronizationVectorIndex]; - // Finally, construct combined identity. - result.identity *= subautomaton.identity; + boost::optional synchronizingAction = combineSynchronizingActions(subautomata, synchVector, synchronizationVectorIndex); + if (synchronizingAction) { + actions[actionInformation.getActionIndex(synchVector.getOutput())].emplace_back(synchronizingAction.get()); + } } - // Add the results of the synchronization vectors to that of the non-synchronizing actions. - for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { - auto const& synchVector = synchronizationVectors[synchVectorIndex]; + // Construct the silent action DDs. + std::vector silentActionDds; + for (auto const& automaton : subautomata) { + for (auto& actionDd : silentActionDds) { + STORM_LOG_TRACE("Extending previous silent action by identity of current automaton."); + actionDd = actionDd.multiplyTransitions(automaton.identity); + } - // 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(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second)); + ActionIdentification silentActionIdentification(storm::jani::Model::SILENT_ACTION_INDEX); + auto silentActionIt = automaton.actions.find(silentActionIdentification); + if (silentActionIt != automaton.actions.end()) { + STORM_LOG_TRACE("Extending silent action by running identity."); + silentActionDds.emplace_back(silentActionIt->second.multiplyTransitions(result.identity)); } + + result.identity *= automaton.identity; } - // Now that we have built the individual action DDs for all resulting actions, we need to combine them - // in an unsynchronizing way. - for (auto const& nonSynchronizingActionDds : nonSynchronizingActions) { - std::vector const& actionDds = nonSynchronizingActionDds.second; - if (actionDds.size() > 1) { - ActionDd combinedAction = combineUnsynchronizedActions(actionDds); - result.actionIndexToAction[nonSynchronizingActionDds.first] = combinedAction; - result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables()); - } else { - result.actionIndexToAction[nonSynchronizingActionDds.first] = actionDds.front(); - result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables()); - } + if (!silentActionDds.empty()) { + auto& allSilentActionDds = actions[storm::jani::Model::SILENT_ACTION_INDEX]; + allSilentActionDds.insert(actions[storm::jani::Model::SILENT_ACTION_INDEX].end(), silentActionDds.begin(), silentActionDds.end()); } + // Finally, combine (potential) multiple action DDs. + for (auto const& actionDds : actions) { + ActionDd combinedAction = actionDds.second.size() > 1 ? combineUnsynchronizedActions(actionDds.second) : actionDds.second.front(); + result.actions[ActionIdentification(actionDds.first)] = combinedAction; + result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables()); + } + + // Construct combined identity. + for (auto const& subautomaton : subautomata) { + result.identity *= subautomaton.identity; + } + return result; } - 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; + boost::optional combineSynchronizingActions(std::vector const& subautomata, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) { + std::vector>> actions; + storm::dd::Add nonSynchronizingIdentity = this->variables.manager->template getAddOne(); + for (uint64_t subautomatonIndex = 0; subautomatonIndex < subautomata.size(); ++subautomatonIndex) { + auto const& subautomaton = subautomata[subautomatonIndex]; + if (synchronizationVector.getInput(subautomatonIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { + auto it = subautomaton.actions.find(ActionIdentification(actionInformation.getActionIndex(synchronizationVector.getInput(subautomatonIndex)), synchronizationVectorIndex)); + if (it != subautomaton.actions.end()) { + actions.emplace_back(subautomatonIndex, it->second); + } else { + return boost::none; + } + } else { + nonSynchronizingIdentity *= subautomaton.identity; + } } // 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()) { + for (auto const& action : actions) { + if (!action.second.get().isInputEnabled()) { allActionsInputEnabled = false; } } @@ -875,12 +902,13 @@ namespace storm { 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(); + uint64_t lowestNondeterminismVariable = actions.front().second.get().getLowestLocalNondeterminismVariable(); + uint64_t highestNondeterminismVariable = actions.front().second.get().getHighestLocalNondeterminismVariable(); storm::dd::Bdd newIllegalFragment = this->variables.manager->getBddZero(); - for (auto const& actionIdentityPair : actionsAndIdentities) { - auto const& action = actionIdentityPair.first; + for (auto const& actionIndexPair : actions) { + auto componentIndex = actionIndexPair.first; + auto const& action = actionIndexPair.second.get(); storm::dd::Bdd actionGuard = action.guard.toBdd(); if (guardDisjunction) { guardDisjunction.get() |= actionGuard; @@ -892,7 +920,7 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. - transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); + transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity); } else { transitions *= action.transitions; } @@ -948,7 +976,7 @@ namespace storm { // such a combined transition. illegalFragment &= inputEnabledGuard; - return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); + return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -1141,7 +1169,7 @@ namespace storm { bool overlappingGuards = false; for (auto const& edge : edgeDds) { - STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::InvalidArgumentException, "Can only combine Markovian edges."); + STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::WrongFormatException, "Can only combine Markovian edges."); if (!overlappingGuards) { overlappingGuards |= !(guard && edge.guard.toBdd()).isZero(); @@ -1197,7 +1225,7 @@ namespace storm { } return combineEdgesToActionNondeterministic(nonMarkovianEdges, markovianEdge, localNondeterminismVariableOffset); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of this type."); } } else { return ActionDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); @@ -1479,23 +1507,30 @@ namespace storm { } } - AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset, std::set const& inputEnabledActionIndices) { + AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices) { + STORM_LOG_TRACE("Building DD for automaton '" << automatonName << "'."); AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); - for (auto const& action : this->model.getActions()) { - uint64_t actionIndex = this->model.getActionIndex(action.getName()); + for (auto const& actionInstantiation : actionInstantiations) { + uint64_t actionIndex = actionInstantiation.first; if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue; } - ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); + bool inputEnabled = false; if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) { - actionDd.setIsInputEnabled(); + inputEnabled = true; + } + for (auto const& instantiationOffset : actionInstantiation.second) { + STORM_LOG_TRACE("Building " << (actionInformation.getActionName(actionIndex).empty() ? "silent " : "") << "action " << (actionInformation.getActionName(actionIndex).empty() ? "" : actionInformation.getActionName(actionIndex) + " ") << "from offset " << instantiationOffset.localNondeterminismVariableOffset << "."); + ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, instantiationOffset.localNondeterminismVariableOffset); + if (inputEnabled) { + actionDd.setIsInputEnabled(); + } + STORM_LOG_TRACE("Used local nondeterminism variables are " << actionDd.getLowestLocalNondeterminismVariable() << " to " << actionDd.getHighestLocalNondeterminismVariable() << "."); + result.actions[ActionIdentification(actionIndex, instantiationOffset.synchronizationVectorIndex)] = actionDd; + result.extendLocalNondeterminismVariables(actionDd.getLocalNondeterminismVariables()); } - - result.actionIndexToAction[actionIndex] = actionDd; - result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); - result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); } for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { @@ -1513,7 +1548,7 @@ namespace storm { return result; } - + void addMissingGlobalVariableIdentities(ActionDd& action) { // Build a DD that we can multiply to the transitions and adds all missing global variable identities that way. storm::dd::Add missingIdentities = this->variables.manager->template getAddOne(); @@ -1539,13 +1574,18 @@ namespace storm { // First, determine the highest number of nondeterminism variables that is used in any action and make // all actions use the same amout of nondeterminism variables. uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable(); + STORM_LOG_TRACE("Building system from composed automaton; number of used nondeterminism variables is " << numberOfUsedNondeterminismVariables << "."); // Add missing global variable identities, action and nondeterminism encodings. std::map> transientEdgeAssignments; - for (auto& action : automaton.actionIndexToAction) { + std::unordered_set actionIndices; + for (auto& action : automaton.actions) { + uint64_t actionIndex = action.first.actionIndex; + STORM_LOG_THROW(actionIndices.find(actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(actionIndex)); + actionIndices.insert(action.first.actionIndex); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); - storm::dd::Add actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional(action.first) : boost::none, this->variables); + storm::dd::Add actionEncoding = encodeAction(actionIndex != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional(actionIndex) : boost::none, this->variables); storm::dd::Add missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables); storm::dd::Add extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions; for (auto const& transientAssignment : action.second.transientEdgeAssignments) { @@ -1562,7 +1602,10 @@ namespace storm { storm::dd::Add result = this->variables.manager->template getAddZero(); storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); std::map> transientEdgeAssignments; - for (auto& action : automaton.actionIndexToAction) { + std::unordered_set actionIndices; + for (auto& action : automaton.actions) { + STORM_LOG_THROW(actionIndices.find(action.first.actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(action.first.actionIndex)); + actionIndices.insert(action.first.actionIndex); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); addToTransientAssignmentMap(transientEdgeAssignments, action.second.transientEdgeAssignments); @@ -1571,7 +1614,7 @@ namespace storm { return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, 0); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal model type."); } } }; @@ -1596,7 +1639,7 @@ namespace storm { } else if (modelType == storm::jani::ModelType::MDP) { return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); } } @@ -1718,7 +1761,7 @@ namespace storm { transitionMatrix += deadlockStatesAdd * globalIdentity * action; } } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); } } return deadlockStates; @@ -1813,8 +1856,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } - STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels."); - STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support reusing actions in parallel composition"); + STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support assignment levels."); storm::jani::Model preparedModel = model; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 8f6791441..6943c6178 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -758,10 +758,7 @@ namespace storm { ++i; } - // Only add the synchronization vector if there is more than one participating automaton. - if (numberOfParticipatingAutomata > 1) { - synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName)); - } + synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName)); } return std::make_shared(subcompositions, synchVectors); diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp index 2622662dc..911d49551 100644 --- a/src/test/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/builder/DdJaniModelBuilderTest.cpp @@ -328,9 +328,42 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { automataCompositions.push_back(std::make_shared("one")); automataCompositions.push_back(std::make_shared("two")); automataCompositions.push_back(std::make_shared("three")); - + // First, make all actions non-synchronizing. std::vector synchronizationVectors; + + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("b"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -338,22 +371,50 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { EXPECT_EQ(48ul, model->getNumberOfTransitions()); // Then, make only a, b and c synchronize. - std::vector inputVector; + synchronizationVectors.clear(); + inputVector.clear(); inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); EXPECT_EQ(7ul, model->getNumberOfStates()); EXPECT_EQ(10ul, model->getNumberOfTransitions()); + synchronizationVectors.clear(); + inputVector.clear(); + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -367,7 +428,7 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); - EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { @@ -389,6 +450,39 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { // First, make all actions non-synchronizing. std::vector synchronizationVectors; + + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("b"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -396,22 +490,50 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { EXPECT_EQ(48ul, model->getNumberOfTransitions()); // Then, make only a, b and c synchronize. - std::vector inputVector; + synchronizationVectors.clear(); + inputVector.clear(); inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); EXPECT_EQ(7ul, model->getNumberOfStates()); EXPECT_EQ(10ul, model->getNumberOfTransitions()); + synchronizationVectors.clear(); + inputVector.clear(); + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -425,7 +547,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); - EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Sylvan, Composition) { @@ -433,24 +555,11 @@ TEST(DdJaniModelBuilderTest_Sylvan, Composition) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; - std::shared_ptr> model = builder.build(janiModel); - - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(21ul, mdp->getNumberOfStates()); - EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm"); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - model = builder.build(janiModel); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - mdp = model->as>(); - - EXPECT_EQ(8ul, mdp->getNumberOfStates()); - EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(21ul, mdp->getNumberOfChoices()); + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Cudd, Composition) { @@ -458,24 +567,11 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; - std::shared_ptr> model = builder.build(janiModel); - - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(21ul, mdp->getNumberOfStates()); - EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm"); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - model = builder.build(janiModel); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - mdp = model->as>(); - - EXPECT_EQ(8ul, mdp->getNumberOfStates()); - EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(21ul, mdp->getNumberOfChoices()); + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) { @@ -496,12 +592,17 @@ TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) { inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); @@ -528,12 +629,17 @@ TEST(DdJaniModelBuilderTest_Sylvan, InputEnabling) { inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition);