diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 98ff3128a..467821ee0 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -221,11 +221,34 @@ namespace storm { } virtual boost::any visit(storm::prism::RenamingComposition const& composition) override { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Renaming is currently not supported in symbolic model building."); + // First, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this)); + + // Create the mapping from action indices to action indices. + std::map renaming; + for (auto const& namePair : composition.getActionRenaming()) { + STORM_LOG_THROW(generationInfo.program.hasAction(namePair.first), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.first << "'."); + STORM_LOG_THROW(generationInfo.program.hasAction(namePair.second), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.second << "'."); + renaming.emplace(generationInfo.program.getActionIndex(namePair.first), generationInfo.program.getActionIndex(namePair.second)); + } + + // Perform the renaming and return result. + return rename(sub, renaming); } virtual boost::any visit(storm::prism::HidingComposition const& composition) override { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hiding is currently not supported in symbolic model building."); + // First, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this)); + + // Create the mapping from action indices to action indices. + std::set actionIndicesToHide; + for (auto const& action : composition.getActionsToHide()) { + STORM_LOG_THROW(generationInfo.program.hasAction(action), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << action << "'."); + actionIndicesToHide.insert(generationInfo.program.getActionIndex(action)); + } + + // Perform the hiding and return result. + return hide(sub, actionIndicesToHide); } virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition) override { @@ -280,16 +303,62 @@ namespace storm { private: /*! - * Composes the given modules while synchronizing over the provided action indices. As a result, the first - * module is modified in place and will contain the composition after a call to this method. + * Hides the actions of the given module according to the given set. As a result, the module is modified in + * place. */ - void composeInParallel(typename DdPrismModelBuilder::ModuleDecisionDiagram& left, typename DdPrismModelBuilder::ModuleDecisionDiagram& right, std::set const& synchronizationActionIndices) { + void hide(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::set const& actionIndicesToHide) const { + STORM_LOG_TRACE("Hiding the actions " << boost::join(actionIndicesToHide, ", ") << "."); + + for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { + if (actionIndicesToHide.find(action) != actionIndicesToHide.end()) { + + } + } + } + + /*! + * Renames the actions of the given module according to the given renaming. + */ + typename DdPrismModelBuilder::ModuleDecisionDiagram rename(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::map const& renaming) const { + STORM_LOG_TRACE("Renaming actions."); + uint_fast64_t numberOfUsedNondeterminismVariables = sub.numberOfUsedNondeterminismVariables; + std::map::ActionDecisionDiagram> actionIndexToDdMap; - std::vector actionNames; - for (auto const& actionIndex : synchronizationActionIndices) { - actionNames.push_back(generationInfo.program.getActionName(actionIndex)); + // Go through all action DDs with a synchronizing label and rename them if they appear in the renaming. + for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { + auto renamingIt = renaming.find(action.first); + if (renamingIt != renaming.end()) { + // If the action is to be renamed and an action with the target index already exists, we need + // to combine the action DDs. + auto itNewActions = actionIndexToDdMap.find(renamingIt.second); + if (itNewActions != actionIndexToDdMap.end()) { + actionIndexToDdMap[renamingIt.second] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); + } else { + // In this case, we can simply copy the action over. + actionIndexToDdMap[renamingIt.second] = action.second; + } + } else { + // If the action is not to be renamed, we need to copy it over. However, if some other action + // was renamed to the very same action name before, we need to combine the transitions. + auto itNewActions = actionIndexToDdMap.find(action.first); + if (itNewActions != actionIndexToDdMap.end()) { + actionIndexToDdMap[action.first] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); + } else { + // In this case, we can simply copy the action over. + actionIndexToDdMap[action.first] = action.second; + } + } } - STORM_LOG_TRACE("Composing two modules over the actions '" << boost::join(actionNames, ", ") << "'."); + + return ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, numberOfUsedNondeterminismVariables); + } + + /*! + * Composes the given modules while synchronizing over the provided action indices. As a result, the first + * module is modified in place and will contain the composition after a call to this method. + */ + void composeInParallel(typename DdPrismModelBuilder::ModuleDecisionDiagram& left, typename DdPrismModelBuilder::ModuleDecisionDiagram& right, std::set const& synchronizationActionIndices) const { + STORM_LOG_TRACE("Composing two modules over the actions " << boost::join(synchronizationActionIndices, ", ") << "."); // Combine the tau action. uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables; @@ -802,21 +871,30 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { - storm::dd::Add action1Extended = action1.transitionsDd * identityDd2; - storm::dd::Add action2Extended = action2.transitionsDd * identityDd1; + // First extend the action DDs by the other identities. + STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions."); + action1.transitionsDd = action1.transitionsDd * identityDd2; + action2.transitionsDd = action2.transitionsDd * identityDd1; + + // Then combine the extended action DDs. + return combineUnsynchronizedActions(generationInfo, action1, action2); + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) { STORM_LOG_TRACE("Combining unsynchronized actions."); // Make both action DDs write to the same global variables. std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, action1, action2); if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, assignedGlobalVariables, 0); + return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { if (action1.transitionsDd.isZero()) { - return ActionDecisionDiagram(action2.guardDd, action2Extended, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); + return ActionDecisionDiagram(action2.guardDd, action2.transitionsDd, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); } else if (action2.transitionsDd.isZero()) { - return ActionDecisionDiagram(action1.guardDd, action1Extended, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables); + return ActionDecisionDiagram(action1.guardDd, action1.transitionsDd, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables); } // Bring both choices to the same number of variables that encode the nondeterminism. @@ -827,18 +905,18 @@ namespace storm { for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); } - action2Extended *= nondeterminismEncoding; + action2.transitionsDd *= nondeterminismEncoding; } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); } - action1Extended *= nondeterminismEncoding; + action1.transitionsDd *= nondeterminismEncoding; } // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended); + storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2.transitionsDd, action1.transitionsDd); return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); } else { diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 44e9fdb9a..9de5cf2df 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -242,6 +242,8 @@ namespace storm { static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2); + + static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2); static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); diff --git a/src/storage/prism/HidingComposition.cpp b/src/storage/prism/HidingComposition.cpp index baaa2572f..50afe0338 100644 --- a/src/storage/prism/HidingComposition.cpp +++ b/src/storage/prism/HidingComposition.cpp @@ -17,6 +17,10 @@ namespace storm { return *sub; } + std::set const& HidingComposition::getActionsToHide() const { + return actionsToHide; + } + void HidingComposition::writeToStream(std::ostream& stream) const { stream << "(" << *sub << ")" << " " << "{" << boost::join(actionsToHide, ", ") << "}"; } diff --git a/src/storage/prism/HidingComposition.h b/src/storage/prism/HidingComposition.h index 048847fa5..094f00b0e 100644 --- a/src/storage/prism/HidingComposition.h +++ b/src/storage/prism/HidingComposition.h @@ -16,6 +16,8 @@ namespace storm { Composition const& getSubcomposition() const; + std::set const& getActionsToHide() const; + protected: virtual void writeToStream(std::ostream& stream) const override; diff --git a/src/storage/prism/RenamingComposition.cpp b/src/storage/prism/RenamingComposition.cpp index ac92dc416..c1d928abb 100644 --- a/src/storage/prism/RenamingComposition.cpp +++ b/src/storage/prism/RenamingComposition.cpp @@ -19,6 +19,10 @@ namespace storm { return *sub; } + std::map const& RenamingComposition::getActionRenaming() const { + return actionRenaming; + } + void RenamingComposition::writeToStream(std::ostream& stream) const { std::vector renamings; for (auto const& renaming : actionRenaming) { diff --git a/src/storage/prism/RenamingComposition.h b/src/storage/prism/RenamingComposition.h index c20c1ec5a..117af5727 100644 --- a/src/storage/prism/RenamingComposition.h +++ b/src/storage/prism/RenamingComposition.h @@ -17,6 +17,8 @@ namespace storm { Composition const& getSubcomposition() const; + std::map const& getActionRenaming() const; + protected: virtual void writeToStream(std::ostream& stream) const override;