sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

system composition in PRISM appears to be working 

Former-commit-id: e7f0dd84e8
tempestpy_adaptions
dehnert 9 years ago
parent
a4687ad230
commit
bf65ef726c
18 changed files with 140 additions and 88 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 137
      src/builder/DdPrismModelBuilder.cpp
  2. 2
      src/parser/PrismParser.cpp
  3. 2
      src/storage/prism/Composition.h
  4. 12
      src/storage/prism/CompositionVisitor.h
  5. 4
      src/storage/prism/HidingComposition.cpp
  6. 2
      src/storage/prism/HidingComposition.h
  7. 4
      src/storage/prism/InterleavingParallelComposition.cpp
  8. 2
      src/storage/prism/InterleavingParallelComposition.h
  9. 4
      src/storage/prism/ModuleComposition.cpp
  10. 2
      src/storage/prism/ModuleComposition.h
  11. 24
      src/storage/prism/Program.cpp
  12. 4
      src/storage/prism/RenamingComposition.cpp
  13. 2
      src/storage/prism/RenamingComposition.h
  14. 4
      src/storage/prism/RestrictedParallelComposition.cpp
  15. 2
      src/storage/prism/RestrictedParallelComposition.h
  16. 4
      src/storage/prism/SynchronizingParallelComposition.cpp
  17. 2
      src/storage/prism/SynchronizingParallelComposition.h
  18. 15
      test/functional/builder/system_composition.nm

137
src/builder/DdPrismModelBuilder.cpp
View File

@ -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));
}
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);
return boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.accept(*this, newSynchronizingActionToOffsetMap()));
}
// 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::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::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, 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()) {
@ -232,14 +239,23 @@ namespace storm {
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()) {
@ -247,14 +263,33 @@ namespace storm {
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, ", ") << ".");
for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) {
if (actionIndicesToHide.find(action) != actionIndicesToHide.end()) {
STORM_LOG_TRACE("Hiding actions.");
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>

2
src/parser/PrismParser.cpp
View File

@ -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)];

2
src/storage/prism/Composition.h
View File

@ -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;

12
src/storage/prism/CompositionVisitor.h
View File

@ -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;
};
}
}

4
src/storage/prism/HidingComposition.cpp
View File

@ -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 {

2
src/storage/prism/HidingComposition.h
View File

@ -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;

4
src/storage/prism/InterleavingParallelComposition.cpp
View File

@ -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 {

2
src/storage/prism/InterleavingParallelComposition.h
View File

@ -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;

4
src/storage/prism/ModuleComposition.cpp
View File

@ -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 {

2
src/storage/prism/ModuleComposition.h
View File

@ -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;

24
src/storage/prism/Program.cpp
View File

@ -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)) {

4
src/storage/prism/RenamingComposition.cpp
View File

@ -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 {

2
src/storage/prism/RenamingComposition.h
View File

@ -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;

4
src/storage/prism/RestrictedParallelComposition.cpp
View File

@ -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 {

2
src/storage/prism/RestrictedParallelComposition.h
View File

@ -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;

4
src/storage/prism/SynchronizingParallelComposition.cpp
View File

@ -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 {

2
src/storage/prism/SynchronizingParallelComposition.h
View File

@ -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;

15
test/functional/builder/system_composition.nm
View File

@ -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
Write Preview
Loading…
Cancel
Save