diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp new file mode 100644 index 000000000..f1450d004 --- /dev/null +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp @@ -0,0 +1,47 @@ +#include "storm/storage/jani/traverser/AssignmentsFinder.h" + + +namespace storm { + namespace jani { + + AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, Variable const& variable) { + ResultType res; + res.hasLocationAssignment = false; + res.hasEdgeAssignment = false; + res.hasEdgeDestinationAssignment = false; + JaniTraverser::traverse(model, std::make_pair(&variable, &res)); + return res; + } + + void AssignmentsFinder::traverse(Location const& location, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : location.getAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasLocationAssignment = true; + } + } + JaniTraverser::traverse(location, data); + } + + void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : templateEdge.getAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasEdgeAssignment = true; + } + } + JaniTraverser::traverse(templateEdge, data); + } + + void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasEdgeDestinationAssignment = true; + } + } + JaniTraverser::traverse(templateEdgeDestination, data); + } + } +} + diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h new file mode 100644 index 000000000..2a2d2cdd0 --- /dev/null +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h @@ -0,0 +1,29 @@ +#pragma once + + +#include + +#include "storm/storage/jani/traverser/JaniTraverser.h" + +namespace storm { + namespace jani { + class AssignmentsFinder : public JaniTraverser { + public: + + struct ResultType { + bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment; + }; + + AssignmentsFinder() = default; + + ResultType find(Model const& model, Variable const& variable); + + virtual ~AssignmentsFinder() = default; + + virtual void traverse(Location const& location, boost::any const& data) const override; + virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override; + }; + } +} + diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp index 3c695d0c1..2461792b5 100644 --- a/src/storm/storage/jani/traverser/JaniTraverser.cpp +++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - void JaniTraverser::traverse(Model const& model, boost::any& data) const { + void JaniTraverser::traverse(Model const& model, boost::any const& data) const { for (auto const& act : model.getActions()) { traverse(act, data); } @@ -14,27 +14,33 @@ namespace storm { for (auto const& aut : model.getAutomata()) { traverse(aut, data); } - traverse(model.getInitialStatesRestriction(), data); + if (model.hasInitialStatesRestriction()) { + traverse(model.getInitialStatesRestriction(), data); + } } - void JaniTraverser::traverse(Action const& action, boost::any& data) const { + void JaniTraverser::traverse(Action const& action, boost::any const& data) const { // Intentionally left empty. } - void JaniTraverser::traverse(Automaton const& automaton, boost::any& data) const { + void JaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const { traverse(automaton.getVariables(), data); for (auto const& loc : automaton.getLocations()) { traverse(loc, data); } traverse(automaton.getEdgeContainer(), data); - traverse(automaton.getInitialStatesRestriction(), data); + if (automaton.hasInitialStatesRestriction()) { + traverse(automaton.getInitialStatesRestriction(), data); + } } - void JaniTraverser::traverse(Constant const& constant, boost::any& data) const { - traverse(constant.getExpression(), data); + void JaniTraverser::traverse(Constant const& constant, boost::any const& data) const { + if (constant.isDefined()) { + traverse(constant.getExpression(), data); + } } - void JaniTraverser::traverse(VariableSet const& variableSet, boost::any& data) const { + void JaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const { for (auto const& v : variableSet.getBooleanVariables()) { traverse(v, data); } @@ -49,46 +55,46 @@ namespace storm { } } - void JaniTraverser::traverse(Location const& location, boost::any& data) const { - traverse(location.getAssignments(), data) + void JaniTraverser::traverse(Location const& location, boost::any const& data) const { + traverse(location.getAssignments(), data); } - void JaniTraverser::traverse(BooleanVariable const& variable, boost::any& data) const { + void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const { if (variable.hasInitExpression()) { - traverse(variable.getInitExpression()); + traverse(variable.getInitExpression(), data); } } - void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any& data) const { + void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const { if (variable.hasInitExpression()) { - traverse(variable.getInitExpression()); + traverse(variable.getInitExpression(), data); } - traverse(variable.getLowerBound()); - traverse(variable.getUpperBound()); + traverse(variable.getLowerBound(), data); + traverse(variable.getUpperBound(), data); } - void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any& data) const { + void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const { if (variable.hasInitExpression()) { - traverse(variable.getInitExpression()); + traverse(variable.getInitExpression(), data); } } - void JaniTraverser::traverse(RealVariable const& variable, boost::any& data) const { + void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const { if (variable.hasInitExpression()) { - traverse(variable.getInitExpression()); + traverse(variable.getInitExpression(), data); } } - void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any& data) const { + void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const { for (auto const& templateEdge : edgeContainer.getTemplateEdges()) { - traverse(templateEdge, data); + traverse(*templateEdge, data); } for (auto const& concreteEdge : edgeContainer.getConcreteEdges()) { traverse(concreteEdge, data); } } - void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any& data) const { + void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { traverse(templateEdge.getGuard(), data); for (auto const& dest : templateEdge.getDestinations()) { traverse(dest, data); @@ -96,32 +102,34 @@ namespace storm { traverse(templateEdge.getAssignments(), data); } - void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any& data) const { + void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { traverse(templateEdgeDestination.getOrderedAssignments(), data); } - void JaniTraverser::traverse(Edge const& edge, boost::any& data) const { - traverse(edge.getRate(), data); + void JaniTraverser::traverse(Edge const& edge, boost::any const& data) const { + if (edge.hasRate()) { + 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(EdgeDestination const& edgeDestination, boost::any const& data) const { + traverse(edgeDestination.getProbability(), data); } - void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any& data) const { + void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const { for (auto const& assignment : orderedAssignments) { traverse(assignment, data); } } - void JaniTraverser::traverse(Assignment const& assignment, boost::any& data) const { + void JaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const { traverse(assignment.getAssignedExpression(), data); } - void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any& data) const { + void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const { // intentionally left empty. } diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h index 24b619c1f..905ad0208 100644 --- a/src/storm/storage/jani/traverser/JaniTraverser.h +++ b/src/storm/storage/jani/traverser/JaniTraverser.h @@ -11,25 +11,25 @@ namespace storm { public: virtual ~JaniTraverser() = default; - virtual void traverse(Model const& model, boost::any& data) const; + virtual void traverse(Model const& model, boost::any const& 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; + virtual void traverse(Action const& action, boost::any const& data) const; + virtual void traverse(Automaton const& automaton, boost::any const& data) const; + virtual void traverse(Constant const& constant, boost::any const& data) const; + virtual void traverse(VariableSet const& variableSet, boost::any const& data) const; + virtual void traverse(Location const& location, boost::any const& data) const; + virtual void traverse(BooleanVariable const& variable, boost::any const& data) const; + virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) const; + virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const; + virtual void traverse(RealVariable const& variable, boost::any const& data) const; + virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data) const; + virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const; + virtual void traverse(Edge const& edge, boost::any const& data) const; + virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const; + virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const; + virtual void traverse(Assignment const& assignment, boost::any const& data) const; + virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const; }; } }