From bf65ef726c598e76e6616b38917b707ea65bcdc3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 May 2016 13:50:58 +0200 Subject: [PATCH] system composition in PRISM appears to be working Former-commit-id: e7f0dd84e88541123952607c80f27b427f66684a --- src/builder/DdPrismModelBuilder.cpp | 137 ++++++++++++------ src/parser/PrismParser.cpp | 2 +- src/storage/prism/Composition.h | 2 +- src/storage/prism/CompositionVisitor.h | 12 +- src/storage/prism/HidingComposition.cpp | 4 +- src/storage/prism/HidingComposition.h | 2 +- .../prism/InterleavingParallelComposition.cpp | 4 +- .../prism/InterleavingParallelComposition.h | 2 +- src/storage/prism/ModuleComposition.cpp | 4 +- src/storage/prism/ModuleComposition.h | 2 +- src/storage/prism/Program.cpp | 24 +-- src/storage/prism/RenamingComposition.cpp | 4 +- src/storage/prism/RenamingComposition.h | 2 +- .../prism/RestrictedParallelComposition.cpp | 4 +- .../prism/RestrictedParallelComposition.h | 2 +- .../SynchronizingParallelComposition.cpp | 4 +- .../prism/SynchronizingParallelComposition.h | 2 +- test/functional/builder/system_composition.nm | 15 +- 18 files changed, 140 insertions(+), 88 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 467821ee0..4602b5caf 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -196,34 +196,41 @@ namespace storm { class ModuleComposer : public storm::prism::CompositionVisitor { public: ModuleComposer(typename DdPrismModelBuilder::GenerationInformation& generationInfo) : generationInfo(generationInfo) { - for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { - synchronizingActionToOffsetMap[actionIndex] = 0; - } + // Intentionally left empty. } typename DdPrismModelBuilder::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) { std::cout << "composing the system " << composition << std::endl; - return boost::any_cast::ModuleDecisionDiagram>(composition.accept(*this)); + + return boost::any_cast::ModuleDecisionDiagram>(composition.accept(*this, newSynchronizingActionToOffsetMap())); } - virtual boost::any visit(storm::prism::ModuleComposition const& composition) override { - STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'."); - typename DdPrismModelBuilder::ModuleDecisionDiagram result = DdPrismModelBuilder::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap); - - // Update the offset indices. + std::map newSynchronizingActionToOffsetMap() const { + std::map result; for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { - if (result.hasSynchronizingAction(actionIndex)) { - synchronizingActionToOffsetMap[actionIndex] = result.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; - } + result[actionIndex] = 0; } + return result; + } + + std::map updateSynchronizingActionToOffsetMap(typename DdPrismModelBuilder::ModuleDecisionDiagram const& sub, std::map const& oldMapping) const { + std::map result = oldMapping; + for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { + result[action.first] = action.second.numberOfUsedNondeterminismVariables; + } + return result; + } + + virtual boost::any visit(storm::prism::ModuleComposition const& composition, boost::any const& data) override { + STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'."); + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + + typename DdPrismModelBuilder::ModuleDecisionDiagram result = DdPrismModelBuilder::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap); return result; } - virtual boost::any visit(storm::prism::RenamingComposition const& composition) override { - // First, we translate the subcomposition. - typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this)); - + virtual boost::any visit(storm::prism::RenamingComposition const& composition, boost::any const& data) override { // Create the mapping from action indices to action indices. std::map renaming; for (auto const& namePair : composition.getActionRenaming()) { @@ -231,30 +238,58 @@ namespace storm { 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)); } + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& indexPair : renaming) { + auto it = synchronizingActionToOffsetMap.find(indexPair.second); + STORM_LOG_THROW(it != synchronizingActionToOffsetMap.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); + newSynchronizingActionToOffsetMap[indexPair.first] = it->second; + } + + // Then, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); // Perform the renaming and return result. return rename(sub, renaming); } - virtual boost::any visit(storm::prism::HidingComposition const& composition) override { - // First, we translate the subcomposition. - typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this)); - + virtual boost::any visit(storm::prism::HidingComposition const& composition, boost::any const& data) override { // 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)); } + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& index : actionIndicesToHide) { + newSynchronizingActionToOffsetMap[index] = 0; + } + + // Then, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); // Perform the hiding and return result. - return hide(sub, actionIndicesToHide); + hide(sub, actionIndicesToHide); + return sub; } - virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition) override { + virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition, boost::any const& data) override { // First, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& action : left.synchronizingActionToDecisionDiagramMap) { + newSynchronizingActionToOffsetMap[action.first] = action.second.numberOfUsedNondeterminismVariables; + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); // Then, determine the action indices on which we need to synchronize. std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); @@ -267,27 +302,39 @@ namespace storm { return left; } - virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition) override { + virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition, boost::any const& data) override { // First, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, data)); // Finally, we compose the subcompositions to create the result. composeInParallel(left, right, std::set()); return left; } - virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition) override { - // First, we translate the subcompositions. - typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); - typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); - + virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition, boost::any const& data) override { // Construct the synchronizing action indices from the synchronizing action names. std::set synchronizingActionIndices; for (auto const& action : composition.getSynchronizingActions()) { synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action)); } + // Then, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& actionIndex : synchronizingActionIndices) { + auto it = left.synchronizingActionToDecisionDiagramMap.find(actionIndex); + if (it != left.synchronizingActionToDecisionDiagramMap.end()) { + newSynchronizingActionToOffsetMap[actionIndex] = it->second.numberOfUsedNondeterminismVariables; + } + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); bool isContainedInLeft = std::includes(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); STORM_LOG_WARN_COND(isContainedInLeft, "Left subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); @@ -307,11 +354,14 @@ namespace storm { * place. */ void hide(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::set const& actionIndicesToHide) const { - STORM_LOG_TRACE("Hiding the actions " << boost::join(actionIndicesToHide, ", ") << "."); + STORM_LOG_TRACE("Hiding actions."); - for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { - if (actionIndicesToHide.find(action) != actionIndicesToHide.end()) { - + for (auto const& actionIndex : actionIndicesToHide) { + auto it = sub.synchronizingActionToDecisionDiagramMap.find(actionIndex); + if (it != sub.synchronizingActionToDecisionDiagramMap.end()) { + sub.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, sub.independentAction, it->second); + sub.numberOfUsedNondeterminismVariables = std::max(sub.numberOfUsedNondeterminismVariables, sub.independentAction.numberOfUsedNondeterminismVariables); + sub.synchronizingActionToDecisionDiagramMap.erase(it); } } } @@ -321,21 +371,21 @@ namespace storm { */ 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; // Go through all action DDs with a synchronizing label and rename them if they appear in the renaming. - for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { + for (auto& 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); + auto itNewActions = actionIndexToDdMap.find(renamingIt->second); if (itNewActions != actionIndexToDdMap.end()) { - actionIndexToDdMap[renamingIt.second] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); + 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; + 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 @@ -350,7 +400,7 @@ namespace storm { } } - return ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, numberOfUsedNondeterminismVariables); + return typename DdPrismModelBuilder::ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, sub.numberOfUsedNondeterminismVariables); } /*! @@ -358,7 +408,7 @@ namespace storm { * 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, ", ") << "."); + STORM_LOG_TRACE("Composing two modules."); // Combine the tau action. uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables; @@ -421,7 +471,6 @@ namespace storm { } typename DdPrismModelBuilder::GenerationInformation& generationInfo; - std::map synchronizingActionToOffsetMap; }; template diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 50a9b0627..7d54f18c6 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -162,7 +162,7 @@ namespace storm { hidingComposition = (atomicComposition >> (qi::lit("/") > (qi::lit("{") > actionNameList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)]; hidingComposition.name("hiding composition"); - actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct>(qi::_2, qi::_1))]; + actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct>(qi::_1, qi::_2))]; actionRenamingList.name("action renaming list"); renamingComposition = (atomicComposition >> (qi::lit("{") > (actionRenamingList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)]; diff --git a/src/storage/prism/Composition.h b/src/storage/prism/Composition.h index 97352162d..b5817aaf2 100644 --- a/src/storage/prism/Composition.h +++ b/src/storage/prism/Composition.h @@ -13,7 +13,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, Composition const& composition); - virtual boost::any accept(CompositionVisitor& visitor) const = 0; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0; protected: virtual void writeToStream(std::ostream& stream) const = 0; diff --git a/src/storage/prism/CompositionVisitor.h b/src/storage/prism/CompositionVisitor.h index 2cb705654..b266e8f28 100644 --- a/src/storage/prism/CompositionVisitor.h +++ b/src/storage/prism/CompositionVisitor.h @@ -15,12 +15,12 @@ namespace storm { class CompositionVisitor { public: - virtual boost::any visit(ModuleComposition const& composition) = 0; - virtual boost::any visit(RenamingComposition const& composition) = 0; - virtual boost::any visit(HidingComposition const& composition) = 0; - virtual boost::any visit(SynchronizingParallelComposition const& composition) = 0; - virtual boost::any visit(InterleavingParallelComposition const& composition) = 0; - virtual boost::any visit(RestrictedParallelComposition const& composition) = 0; + virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) = 0; + virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) = 0; + virtual boost::any visit(HidingComposition const& composition, boost::any const& data) = 0; + virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) = 0; + virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) = 0; + virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) = 0; }; } } diff --git a/src/storage/prism/HidingComposition.cpp b/src/storage/prism/HidingComposition.cpp index 50afe0338..78af490d0 100644 --- a/src/storage/prism/HidingComposition.cpp +++ b/src/storage/prism/HidingComposition.cpp @@ -9,8 +9,8 @@ namespace storm { // Intentionally left empty. } - boost::any HidingComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any HidingComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } Composition const& HidingComposition::getSubcomposition() const { diff --git a/src/storage/prism/HidingComposition.h b/src/storage/prism/HidingComposition.h index 094f00b0e..4de9e8eba 100644 --- a/src/storage/prism/HidingComposition.h +++ b/src/storage/prism/HidingComposition.h @@ -12,7 +12,7 @@ namespace storm { public: HidingComposition(std::shared_ptr const& sub, std::set const& actionsToHide); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; Composition const& getSubcomposition() const; diff --git a/src/storage/prism/InterleavingParallelComposition.cpp b/src/storage/prism/InterleavingParallelComposition.cpp index 3c5de8f8e..54fd113e4 100644 --- a/src/storage/prism/InterleavingParallelComposition.cpp +++ b/src/storage/prism/InterleavingParallelComposition.cpp @@ -7,8 +7,8 @@ namespace storm { // Intentionally left empty. } - boost::any InterleavingParallelComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any InterleavingParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void InterleavingParallelComposition::writeToStream(std::ostream& stream) const { diff --git a/src/storage/prism/InterleavingParallelComposition.h b/src/storage/prism/InterleavingParallelComposition.h index 42c8ca771..7a77fe90c 100644 --- a/src/storage/prism/InterleavingParallelComposition.h +++ b/src/storage/prism/InterleavingParallelComposition.h @@ -9,7 +9,7 @@ namespace storm { public: InterleavingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; protected: virtual void writeToStream(std::ostream& stream) const override; diff --git a/src/storage/prism/ModuleComposition.cpp b/src/storage/prism/ModuleComposition.cpp index 3dd32d37d..a3f422e89 100644 --- a/src/storage/prism/ModuleComposition.cpp +++ b/src/storage/prism/ModuleComposition.cpp @@ -7,8 +7,8 @@ namespace storm { // Intentionally left empty. } - boost::any ModuleComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any ModuleComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::string const& ModuleComposition::getModuleName() const { diff --git a/src/storage/prism/ModuleComposition.h b/src/storage/prism/ModuleComposition.h index 6208fa27a..20349d13b 100644 --- a/src/storage/prism/ModuleComposition.h +++ b/src/storage/prism/ModuleComposition.h @@ -11,7 +11,7 @@ namespace storm { public: ModuleComposition(std::string const& moduleName); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; std::string const& getModuleName() const; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index a76be8dc6..7d7a5ad4e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -27,7 +27,7 @@ namespace storm { } bool isValid(Composition const& composition) { - bool isValid = boost::any_cast(composition.accept(*this)); + bool isValid = boost::any_cast(composition.accept(*this, boost::any())); if (appearingModules.size() != program.getNumberOfModules()) { isValid = false; STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Not every module is used in the system composition."); @@ -35,7 +35,7 @@ namespace storm { return isValid; } - virtual boost::any visit(ModuleComposition const& composition) override { + virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) override { bool isValid = program.hasModule(composition.getModuleName()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist."); isValid = appearingModules.find(composition.getModuleName()) == appearingModules.end(); @@ -44,24 +44,24 @@ namespace storm { return isValid; } - virtual boost::any visit(RenamingComposition const& composition) override { - return composition.getSubcomposition().accept(*this); + virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override { + return composition.getSubcomposition().accept(*this, data); } - virtual boost::any visit(HidingComposition const& composition) override { - return composition.getSubcomposition().accept(*this); + virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override { + return composition.getSubcomposition().accept(*this, data); } - virtual boost::any visit(SynchronizingParallelComposition const& composition) override { - return boost::any_cast(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast(composition.getRightSubcomposition().accept(*this)); + virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override { + return boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); } - virtual boost::any visit(InterleavingParallelComposition const& composition) override { - return boost::any_cast(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast(composition.getRightSubcomposition().accept(*this)); + virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override { + return boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); } - virtual boost::any visit(RestrictedParallelComposition const& composition) override { - bool isValid = boost::any_cast(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast(composition.getRightSubcomposition().accept(*this)); + virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override { + bool isValid = boost::any_cast(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast(composition.getRightSubcomposition().accept(*this, data)); for (auto const& action : composition.getSynchronizingActions()) { if (!program.hasAction(action)) { diff --git a/src/storage/prism/RenamingComposition.cpp b/src/storage/prism/RenamingComposition.cpp index c1d928abb..9fe7d72e6 100644 --- a/src/storage/prism/RenamingComposition.cpp +++ b/src/storage/prism/RenamingComposition.cpp @@ -11,8 +11,8 @@ namespace storm { // Intentionally left empty. } - boost::any RenamingComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any RenamingComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } Composition const& RenamingComposition::getSubcomposition() const { diff --git a/src/storage/prism/RenamingComposition.h b/src/storage/prism/RenamingComposition.h index 117af5727..124889d3c 100644 --- a/src/storage/prism/RenamingComposition.h +++ b/src/storage/prism/RenamingComposition.h @@ -13,7 +13,7 @@ namespace storm { public: RenamingComposition(std::shared_ptr const& sub, std::map const& actionRenaming); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; Composition const& getSubcomposition() const; diff --git a/src/storage/prism/RestrictedParallelComposition.cpp b/src/storage/prism/RestrictedParallelComposition.cpp index 681fcc4b0..409b7aad3 100644 --- a/src/storage/prism/RestrictedParallelComposition.cpp +++ b/src/storage/prism/RestrictedParallelComposition.cpp @@ -9,8 +9,8 @@ namespace storm { // Intentionally left empty. } - boost::any RestrictedParallelComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any RestrictedParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } std::set const& RestrictedParallelComposition::getSynchronizingActions() const { diff --git a/src/storage/prism/RestrictedParallelComposition.h b/src/storage/prism/RestrictedParallelComposition.h index 9f0f14591..af7404056 100644 --- a/src/storage/prism/RestrictedParallelComposition.h +++ b/src/storage/prism/RestrictedParallelComposition.h @@ -12,7 +12,7 @@ namespace storm { public: RestrictedParallelComposition(std::shared_ptr const& left, std::set const& synchronizingActions, std::shared_ptr const& right); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; std::set const& getSynchronizingActions() const; diff --git a/src/storage/prism/SynchronizingParallelComposition.cpp b/src/storage/prism/SynchronizingParallelComposition.cpp index 56652c3a7..b25334508 100644 --- a/src/storage/prism/SynchronizingParallelComposition.cpp +++ b/src/storage/prism/SynchronizingParallelComposition.cpp @@ -7,8 +7,8 @@ namespace storm { // Intentionally left empty. } - boost::any SynchronizingParallelComposition::accept(CompositionVisitor& visitor) const { - return visitor.visit(*this); + boost::any SynchronizingParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const { + return visitor.visit(*this, data); } void SynchronizingParallelComposition::writeToStream(std::ostream& stream) const { diff --git a/src/storage/prism/SynchronizingParallelComposition.h b/src/storage/prism/SynchronizingParallelComposition.h index 3bb668bb0..a0aca654a 100644 --- a/src/storage/prism/SynchronizingParallelComposition.h +++ b/src/storage/prism/SynchronizingParallelComposition.h @@ -9,7 +9,7 @@ namespace storm { public: SynchronizingParallelComposition(std::shared_ptr const& left, std::shared_ptr const& right); - virtual boost::any accept(CompositionVisitor& visitor) const override; + virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; protected: virtual void writeToStream(std::ostream& stream) const override; diff --git a/test/functional/builder/system_composition.nm b/test/functional/builder/system_composition.nm index 3b8ec854e..30f4368b2 100644 --- a/test/functional/builder/system_composition.nm +++ b/test/functional/builder/system_composition.nm @@ -3,25 +3,28 @@ mdp module one x : [0 .. 2] init 0; - [a] x = 0 -> (x'=1); - [] x = 1 -> true; + [a] x=0 -> (x'=1); + [] x>=0 -> (x'=2); + [done] x>=1 -> true; endmodule module two y : [0 .. 2] init 0; [b] y=0 -> (y'=1); - [] y=1 -> true; + [] y>=0 -> (y'=2); + [done] y>=1 -> true; endmodule module three z : [0 .. 2] init 0; - [c] z=0 -> (z'=1); - [] z=1 -> true; + [a] z=0 -> (z'=1); + [] x=0&y=0&z=1 -> (z'=2); + [loop] z>=1 -> true; endmodule system - ((one || two) {a <- b} |[a]| (three {a <- c})) / {a, b, c} + ((one || two {b <- a}) / {a}) {done <- loop} || three endsystem