From 1714126a6fe3ed668ae92d83ab6cca45614fab8a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 28 Aug 2018 16:43:16 +0200 Subject: [PATCH] traverser for jani models --- src/storm/storage/jani/Automaton.cpp | 4 + src/storm/storage/jani/Automaton.h | 2 + src/storm/storage/jani/EdgeContainer.cpp | 6 +- src/storm/storage/jani/EdgeContainer.h | 2 + .../storage/jani/traverser/JaniTraverser.cpp | 130 ++++++++++++++++++ .../storage/jani/traverser/JaniTraverser.h | 36 +++++ 6 files changed, 178 insertions(+), 2 deletions(-) create mode 100644 src/storm/storage/jani/traverser/JaniTraverser.cpp create mode 100644 src/storm/storage/jani/traverser/JaniTraverser.h diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index cc75d080e..62d2576cf 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -270,6 +270,10 @@ namespace storm { return ConstEdges(it1, it2); } + EdgeContainer const& Automaton::getEdgeContainer() const { + return edges; + } + void Automaton::addEdge(Edge const& edge) { STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'."); assert(validate()); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index eb1362741..869f5cd09 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -192,6 +192,8 @@ namespace storm { */ ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const; + EdgeContainer const& getEdgeContainer() const; + /*! * Adds the template edge to the list of edges */ diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp index b7a9ca1ec..d735bc80d 100644 --- a/src/storm/storage/jani/EdgeContainer.cpp +++ b/src/storm/storage/jani/EdgeContainer.cpp @@ -121,8 +121,6 @@ namespace storm { } - - std::vector & EdgeContainer::getConcreteEdges() { return edges; } @@ -130,6 +128,10 @@ namespace storm { std::vector const& EdgeContainer::getConcreteEdges() const { return edges; } + + TemplateEdgeContainer const& EdgeContainer::getTemplateEdges() const { + return templates; + } std::set EdgeContainer::getActionIndices() const { std::set result; diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h index f4738e1e0..faa33a418 100644 --- a/src/storm/storage/jani/EdgeContainer.h +++ b/src/storm/storage/jani/EdgeContainer.h @@ -95,6 +95,8 @@ namespace storm { void clearConcreteEdges(); std::vector const& getConcreteEdges() const; std::vector & getConcreteEdges(); + TemplateEdgeContainer const& getTemplateEdges const; + size_t size() const; iterator begin(); diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp new file mode 100644 index 000000000..3c695d0c1 --- /dev/null +++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp @@ -0,0 +1,130 @@ +#include "storm/storage/jani/traverser/JaniTraverser.h" + + +namespace storm { + namespace jani { + void JaniTraverser::traverse(Model const& model, boost::any& data) const { + for (auto const& act : model.getActions()) { + traverse(act, data); + } + for (auto const& c : model.getConstants()) { + traverse(c, data); + } + traverse(model.getGlobalVariables(), data); + for (auto const& aut : model.getAutomata()) { + traverse(aut, data); + } + traverse(model.getInitialStatesRestriction(), data); + } + + void JaniTraverser::traverse(Action const& action, boost::any& data) const { + // Intentionally left empty. + } + + void JaniTraverser::traverse(Automaton const& automaton, boost::any& data) const { + traverse(automaton.getVariables(), data); + for (auto const& loc : automaton.getLocations()) { + traverse(loc, data); + } + traverse(automaton.getEdgeContainer(), data); + traverse(automaton.getInitialStatesRestriction(), data); + } + + void JaniTraverser::traverse(Constant const& constant, boost::any& data) const { + traverse(constant.getExpression(), data); + } + + void JaniTraverser::traverse(VariableSet const& variableSet, boost::any& data) const { + for (auto const& v : variableSet.getBooleanVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getBoundedIntegerVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getUnboundedIntegerVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getRealVariables()) { + traverse(v, data); + } + } + + void JaniTraverser::traverse(Location const& location, boost::any& data) const { + traverse(location.getAssignments(), data) + } + + void JaniTraverser::traverse(BooleanVariable const& variable, boost::any& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression()); + } + } + + void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression()); + } + traverse(variable.getLowerBound()); + traverse(variable.getUpperBound()); + } + + void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression()); + } + } + + void JaniTraverser::traverse(RealVariable const& variable, boost::any& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression()); + } + } + + void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any& data) const { + for (auto const& templateEdge : edgeContainer.getTemplateEdges()) { + traverse(templateEdge, data); + } + for (auto const& concreteEdge : edgeContainer.getConcreteEdges()) { + traverse(concreteEdge, data); + } + } + + void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any& data) const { + traverse(templateEdge.getGuard(), data); + for (auto const& dest : templateEdge.getDestinations()) { + traverse(dest, data); + } + traverse(templateEdge.getAssignments(), data); + } + + void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any& data) const { + traverse(templateEdgeDestination.getOrderedAssignments(), data); + } + + void JaniTraverser::traverse(Edge const& edge, boost::any& data) const { + traverse(edge.getRate(), data); + for (auto const& dest : edge.getDestinations()) { + traverse(dest, data); + } + } + + void JaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any& data) const { + traverse(edgeDestination.getProbability()); + } + + void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any& data) const { + for (auto const& assignment : orderedAssignments) { + traverse(assignment, data); + } + } + + void JaniTraverser::traverse(Assignment const& assignment, boost::any& data) const { + traverse(assignment.getAssignedExpression(), data); + } + + void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any& data) const { + // intentionally left empty. + } + + } +} + diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h new file mode 100644 index 000000000..24b619c1f --- /dev/null +++ b/src/storm/storage/jani/traverser/JaniTraverser.h @@ -0,0 +1,36 @@ +#pragma once + + +#include + +#include "storm/storage/jani/Model.h" + +namespace storm { + namespace jani { + class JaniTraverser { + public: + virtual ~JaniTraverser() = default; + + virtual void traverse(Model const& model, boost::any& data) const; + + virtual void traverse(Action const& action, boost::any& data) const; + virtual void traverse(Automaton const& automaton, boost::any& data) const; + virtual void traverse(Constant const& constant, boost::any& data) const; + virtual void traverse(VariableSet const& variableSet, boost::any& data) const; + virtual void traverse(Location const& location, boost::any& data) const; + virtual void traverse(BooleanVariable const& variable, boost::any& data) const; + virtual void traverse(BoundedIntegerVariable const& variable, boost::any& data) const; + virtual void traverse(UnboundedIntegerVariable const& variable, boost::any& data) const; + virtual void traverse(RealVariable const& variable, boost::any& data) const; + virtual void traverse(EdgeContainer const& edgeContainer, boost::any& data) const; + virtual void traverse(TemplateEdge const& templateEdge, boost::any& data) const; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any& data) const; + virtual void traverse(Edge const& edge, boost::any& data) const; + virtual void traverse(EdgeDestination const& edgeDestination, boost::any& data) const; + virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any& data) const; + virtual void traverse(Assignment const& assignment, boost::any& data) const; + virtual void traverse(storm::expressions::Expression const& expression, boost::any& data) const; + }; + } +} +