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<Type, ValueType>::GenerationInformation& generationInfo) : generationInfo(generationInfo) {
- for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
- synchronizingActionToOffsetMap[actionIndex] = 0;
- }
+ // Intentionally left empty.
}
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) {
std::cout << "composing the system " << composition << std::endl;
- return boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.accept(*this));
+
+ return boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.accept(*this, newSynchronizingActionToOffsetMap()));
}
- virtual boost::any visit(storm::prism::ModuleComposition const& composition) override {
- STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'.");
- typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram result = DdPrismModelBuilder<Type, ValueType>::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap);
-
- // Update the offset indices.
+ std::map<uint_fast64_t, uint_fast64_t> newSynchronizingActionToOffsetMap() const {
+ std::map<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t, uint_fast64_t> updateSynchronizingActionToOffsetMap(typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram const& sub, std::map<uint_fast64_t, uint_fast64_t> const& oldMapping) const {
+ std::map<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram result = DdPrismModelBuilder<Type, ValueType>::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<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::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<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+ std::map<uint_fast64_t, uint_fast64_t> 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<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::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<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::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<uint_fast64_t> 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<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+ std::map<uint_fast64_t, uint_fast64_t> newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap;
+ for (auto const& index : actionIndicesToHide) {
+ newSynchronizingActionToOffsetMap[index] = 0;
+ }
+
+ // Then, we translate the subcomposition.
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::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<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
- typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data));
+
+ // Prepare the new offset mapping.
+ std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+ std::map<uint_fast64_t, uint_fast64_t> newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap;
+ for (auto const& action : left.synchronizingActionToDecisionDiagramMap) {
+ newSynchronizingActionToOffsetMap[action.first] = action.second.numberOfUsedNondeterminismVariables;
+ }
+
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap));
// Then, determine the action indices on which we need to synchronize.
std::set<uint_fast64_t> 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<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
- typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data));
+
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, data));
// Finally, we compose the subcompositions to create the result.
composeInParallel(left, right, std::set<uint_fast64_t>());
return left;
}
- virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition) override {
- // First, we translate the subcompositions.
- typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
- typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::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<uint_fast64_t> synchronizingActionIndices;
for (auto const& action : composition.getSynchronizingActions()) {
synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action));
}
+ // Then, we translate the subcompositions.
+ typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data));
+
+ // Prepare the new offset mapping.
+ std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+ std::map<uint_fast64_t, uint_fast64_t> 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<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap));
+
std::set<uint_fast64_t> 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<Type, ValueType>::ModuleDecisionDiagram& sub, std::set<uint_fast64_t> 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<Type, ValueType>::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<Type, ValueType>::ModuleDecisionDiagram rename(typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& sub, std::map<uint_fast64_t, uint_fast64_t> const& renaming) const {
STORM_LOG_TRACE("Renaming actions.");
- uint_fast64_t numberOfUsedNondeterminismVariables = sub.numberOfUsedNondeterminismVariables;
std::map<uint_fast64_t, typename DdPrismModelBuilder<Type, ValueType>::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<Type, ValueType>::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second);
+ actionIndexToDdMap[renamingIt->second] = DdPrismModelBuilder<Type, ValueType>::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<Type, ValueType>::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<Type, ValueType>::ModuleDecisionDiagram& left, typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& right, std::set<uint_fast64_t> 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<Type, ValueType>::GenerationInformation& generationInfo;
- std::map<uint_fast64_t, uint_fast64_t> synchronizingActionToOffsetMap;
};
template <storm::dd::DdType Type, typename ValueType>
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<std::pair<std::string, std::string>>(qi::_2, qi::_1))];
+ actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct<std::pair<std::string, std::string>>(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<Composition> const& sub, std::set<std::string> 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<Composition> const& left, std::shared_ptr<Composition> 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<bool>(composition.accept(*this));
+ bool isValid = boost::any_cast<bool>(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<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+ virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override {
+ return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this, data));
}
- virtual boost::any visit(InterleavingParallelComposition const& composition) override {
- return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+ virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override {
+ return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this, data));
}
- virtual boost::any visit(RestrictedParallelComposition const& composition) override {
- bool isValid = boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+ virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override {
+ bool isValid = boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this, data)) && boost::any_cast<bool>(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<Composition> const& sub, std::map<std::string, std::string> 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<std::string> 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<Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<Composition> const& right);
- virtual boost::any accept(CompositionVisitor& visitor) const override;
+ virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
std::set<std::string> 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<Composition> const& left, std::shared_ptr<Composition> 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