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

const and non-const jani traverser

main
TimQu 7 years ago
parent
6564abd434
commit
dadf571934
4 changed files with 218 additions and 24 deletions
Unified View
  1. 8
      src/storm/storage/jani/traverser/AssignmentsFinder.cpp
  2. 2
      src/storm/storage/jani/traverser/AssignmentsFinder.h
  3. 204
      src/storm/storage/jani/traverser/JaniTraverser.cpp
  4. 28
      src/storm/storage/jani/traverser/JaniTraverser.h

8
src/storm/storage/jani/traverser/AssignmentsFinder.cpp
View File

@ -9,7 +9,7 @@ namespace storm {
res.hasLocationAssignment = false; res.hasLocationAssignment = false;
res.hasEdgeAssignment = false; res.hasEdgeAssignment = false;
res.hasEdgeDestinationAssignment = false; res.hasEdgeDestinationAssignment = false;
JaniTraverser::traverse(model, std::make_pair(&variable, &res)); ConstJaniTraverser::traverse(model, std::make_pair(&variable, &res));
return res; return res;
} }
@ -20,7 +20,7 @@ namespace storm {
resVar.second->hasLocationAssignment = true; resVar.second->hasLocationAssignment = true;
} }
} }
JaniTraverser::traverse(location, data); ConstJaniTraverser::traverse(location, data);
} }
void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
@ -30,7 +30,7 @@ namespace storm {
resVar.second->hasEdgeAssignment = true; resVar.second->hasEdgeAssignment = true;
} }
} }
JaniTraverser::traverse(templateEdge, data); ConstJaniTraverser::traverse(templateEdge, data);
} }
void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
@ -40,7 +40,7 @@ namespace storm {
resVar.second->hasEdgeDestinationAssignment = true; resVar.second->hasEdgeDestinationAssignment = true;
} }
} }
JaniTraverser::traverse(templateEdgeDestination, data); ConstJaniTraverser::traverse(templateEdgeDestination, data);
} }
} }
} }

2
src/storm/storage/jani/traverser/AssignmentsFinder.h
View File

@ -7,7 +7,7 @@
namespace storm { namespace storm {
namespace jani { namespace jani {
class AssignmentsFinder : public JaniTraverser { class AssignmentsFinder : public ConstJaniTraverser {
public: public:
struct ResultType { struct ResultType {

204
src/storm/storage/jani/traverser/JaniTraverser.cpp
View File

@ -3,7 +3,159 @@
namespace storm { namespace storm {
namespace jani { namespace jani {
void JaniTraverser::traverse(Model const& model, boost::any const& data) const { void JaniTraverser::traverse(Model& model, boost::any const& data) const {
for (auto& act : model.getActions()) {
traverse(act, data);
}
for (auto& c : model.getConstants()) {
traverse(c, data);
}
traverse(model.getGlobalVariables(), data);
for (auto& aut : model.getAutomata()) {
traverse(aut, data);
}
if (model.hasInitialStatesRestriction()) {
traverse(model.getInitialStatesRestriction(), data);
}
}
void JaniTraverser::traverse(Action const& action, boost::any const& data) const {
// Intentionally left empty.
}
void JaniTraverser::traverse(Automaton& automaton, boost::any const& data) const {
traverse(automaton.getVariables(), data);
for (auto& loc : automaton.getLocations()) {
traverse(loc, data);
}
traverse(automaton.getEdgeContainer(), data);
if (automaton.hasInitialStatesRestriction()) {
traverse(automaton.getInitialStatesRestriction(), data);
}
}
void JaniTraverser::traverse(Constant& constant, boost::any const& data) const {
if (constant.isDefined()) {
traverse(constant.getExpression(), data);
}
}
void JaniTraverser::traverse(VariableSet& variableSet, boost::any const& data) const {
for (auto& v : variableSet.getBooleanVariables()) {
traverse(v, data);
}
for (auto& v : variableSet.getBoundedIntegerVariables()) {
traverse(v, data);
}
for (auto& v : variableSet.getUnboundedIntegerVariables()) {
traverse(v, data);
}
for (auto& v : variableSet.getRealVariables()) {
traverse(v, data);
}
for (auto& v : variableSet.getArrayVariables()) {
traverse(v, data);
}
}
void JaniTraverser::traverse(Location& location, boost::any const& data) const {
traverse(location.getAssignments(), data);
}
void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
}
void JaniTraverser::traverse(BoundedIntegerVariable& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
traverse(variable.getLowerBound(), data);
traverse(variable.getUpperBound(), data);
}
void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
}
void JaniTraverser::traverse(RealVariable& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
}
void JaniTraverser::traverse(ArrayVariable& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
if (variable.hasElementTypeBounds()) {
traverse(variable.getElementTypeBounds().first, data);
traverse(variable.getElementTypeBounds().second, data);
}
}
void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) const {
for (auto& templateEdge : edgeContainer.getTemplateEdges()) {
traverse(*templateEdge, data);
}
for (auto& concreteEdge : edgeContainer.getConcreteEdges()) {
traverse(concreteEdge, data);
}
}
void JaniTraverser::traverse(TemplateEdge& templateEdge, boost::any const& data) const {
traverse(templateEdge.getGuard(), data);
for (auto& dest : templateEdge.getDestinations()) {
traverse(dest, data);
}
traverse(templateEdge.getAssignments(), data);
}
void JaniTraverser::traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const {
traverse(templateEdgeDestination.getOrderedAssignments(), data);
}
void JaniTraverser::traverse(Edge& edge, boost::any const& data) const {
if (edge.hasRate()) {
traverse(edge.getRate(), data);
}
for (auto& dest : edge.getDestinations()) {
traverse(dest, data);
}
}
void JaniTraverser::traverse(EdgeDestination& edgeDestination, boost::any const& data) const {
traverse(edgeDestination.getProbability(), data);
}
void JaniTraverser::traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const {
for (auto& assignment : orderedAssignments) {
traverse(assignment, data);
}
STORM_LOG_ASSERT(orderedAssignments.checkOrder(), "Order of ordered assignment has been violated.");
}
void JaniTraverser::traverse(Assignment& assignment, boost::any const& data) const {
traverse(assignment.getAssignedExpression(), data);
traverse(assignment.getLValue(), data);
}
void JaniTraverser::traverse(LValue& lValue, boost::any const& data) const {
if (lValue.isArrayAccess()) {
traverse(lValue.getArrayIndex(), data);
}
}
void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
// intentionally left empty.
}
void ConstJaniTraverser::traverse(Model const& model, boost::any const& data) const {
for (auto const& act : model.getActions()) { for (auto const& act : model.getActions()) {
traverse(act, data); traverse(act, data);
} }
@ -19,11 +171,11 @@ namespace storm {
} }
} }
void JaniTraverser::traverse(Action const& action, boost::any const& data) const { void ConstJaniTraverser::traverse(Action const& action, boost::any const& data) const {
// Intentionally left empty. // Intentionally left empty.
} }
void JaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const { void ConstJaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const {
traverse(automaton.getVariables(), data); traverse(automaton.getVariables(), data);
for (auto const& loc : automaton.getLocations()) { for (auto const& loc : automaton.getLocations()) {
traverse(loc, data); traverse(loc, data);
@ -34,13 +186,13 @@ namespace storm {
} }
} }
void JaniTraverser::traverse(Constant const& constant, boost::any const& data) const { void ConstJaniTraverser::traverse(Constant const& constant, boost::any const& data) const {
if (constant.isDefined()) { if (constant.isDefined()) {
traverse(constant.getExpression(), data); traverse(constant.getExpression(), data);
} }
} }
void JaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const { void ConstJaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const {
for (auto const& v : variableSet.getBooleanVariables()) { for (auto const& v : variableSet.getBooleanVariables()) {
traverse(v, data); traverse(v, data);
} }
@ -53,19 +205,22 @@ namespace storm {
for (auto const& v : variableSet.getRealVariables()) { for (auto const& v : variableSet.getRealVariables()) {
traverse(v, data); traverse(v, data);
} }
for (auto const& v : variableSet.getArrayVariables()) {
traverse(v, data);
}
} }
void JaniTraverser::traverse(Location const& location, boost::any const& data) const { void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) const {
traverse(location.getAssignments(), data); traverse(location.getAssignments(), data);
} }
void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const { void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const {
if (variable.hasInitExpression()) { if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data); traverse(variable.getInitExpression(), data);
} }
} }
void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const { void ConstJaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const {
if (variable.hasInitExpression()) { if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data); traverse(variable.getInitExpression(), data);
} }
@ -73,19 +228,29 @@ namespace storm {
traverse(variable.getUpperBound(), data); traverse(variable.getUpperBound(), data);
} }
void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const { void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const {
if (variable.hasInitExpression()) { if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data); traverse(variable.getInitExpression(), data);
} }
} }
void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const { void ConstJaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const {
if (variable.hasInitExpression()) { if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data); traverse(variable.getInitExpression(), data);
} }
} }
void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const { void ConstJaniTraverser::traverse(ArrayVariable const& variable, boost::any const& data) const {
if (variable.hasInitExpression()) {
traverse(variable.getInitExpression(), data);
}
if (variable.hasElementTypeBounds()) {
traverse(variable.getElementTypeBounds().first, data);
traverse(variable.getElementTypeBounds().second, data);
}
}
void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const {
for (auto const& templateEdge : edgeContainer.getTemplateEdges()) { for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
traverse(*templateEdge, data); traverse(*templateEdge, data);
} }
@ -94,7 +259,7 @@ namespace storm {
} }
} }
void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { void ConstJaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
traverse(templateEdge.getGuard(), data); traverse(templateEdge.getGuard(), data);
for (auto const& dest : templateEdge.getDestinations()) { for (auto const& dest : templateEdge.getDestinations()) {
traverse(dest, data); traverse(dest, data);
@ -102,11 +267,11 @@ namespace storm {
traverse(templateEdge.getAssignments(), data); traverse(templateEdge.getAssignments(), data);
} }
void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { void ConstJaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
traverse(templateEdgeDestination.getOrderedAssignments(), data); traverse(templateEdgeDestination.getOrderedAssignments(), data);
} }
void JaniTraverser::traverse(Edge const& edge, boost::any const& data) const { void ConstJaniTraverser::traverse(Edge const& edge, boost::any const& data) const {
if (edge.hasRate()) { if (edge.hasRate()) {
traverse(edge.getRate(), data); traverse(edge.getRate(), data);
} }
@ -115,27 +280,28 @@ namespace storm {
} }
} }
void JaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const { void ConstJaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const {
traverse(edgeDestination.getProbability(), data); traverse(edgeDestination.getProbability(), data);
} }
void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const { void ConstJaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const {
for (auto const& assignment : orderedAssignments) { for (auto const& assignment : orderedAssignments) {
traverse(assignment, data); traverse(assignment, data);
} }
} }
void JaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const { void ConstJaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const {
traverse(assignment.getAssignedExpression(), data); traverse(assignment.getAssignedExpression(), data);
traverse(assignment.getLValue(), data);
} }
void JaniTraverser::traverse(LValue const& lValue, boost::any const& data) const { void ConstJaniTraverser::traverse(LValue const& lValue, boost::any const& data) const {
if (lValue.isArrayAccess()) { if (lValue.isArrayAccess()) {
traverse(lValue.getArrayIndex(), data); traverse(lValue.getArrayIndex(), data);
} }
} }
void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const { void ConstJaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
// intentionally left empty. // intentionally left empty.
} }

28
src/storm/storage/jani/traverser/JaniTraverser.h
View File

@ -11,6 +11,33 @@ namespace storm {
public: public:
virtual ~JaniTraverser() = default; virtual ~JaniTraverser() = default;
virtual void traverse(Model& model, boost::any const& data) const;
virtual void traverse(Action const& action, boost::any const& data) const;
virtual void traverse(Automaton& automaton, boost::any const& data) const;
virtual void traverse(Constant& constant, boost::any const& data) const;
virtual void traverse(VariableSet& variableSet, boost::any const& data) const;
virtual void traverse(Location& location, boost::any const& data) const;
virtual void traverse(BooleanVariable& variable, boost::any const& data) const;
virtual void traverse(BoundedIntegerVariable& variable, boost::any const& data) const;
virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data) const;
virtual void traverse(RealVariable& variable, boost::any const& data) const;
virtual void traverse(ArrayVariable& variable, boost::any const& data) const;
virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data) const;
virtual void traverse(TemplateEdge& templateEdge, boost::any const& data) const;
virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const;
virtual void traverse(Edge& edge, boost::any const& data) const;
virtual void traverse(EdgeDestination& edgeDestination, boost::any const& data) const;
virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const;
virtual void traverse(Assignment& assignment, boost::any const& data) const;
virtual void traverse(LValue& lValue, boost::any const& data) const;
virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
};
class ConstJaniTraverser {
public:
virtual ~ConstJaniTraverser() = default;
virtual void traverse(Model const& model, boost::any const& data) const; virtual void traverse(Model const& model, boost::any const& data) const;
virtual void traverse(Action const& action, boost::any const& data) const; virtual void traverse(Action const& action, boost::any const& data) const;
@ -22,6 +49,7 @@ namespace storm {
virtual void traverse(BoundedIntegerVariable 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(UnboundedIntegerVariable const& variable, boost::any const& data) const;
virtual void traverse(RealVariable const& variable, boost::any const& data) const; virtual void traverse(RealVariable const& variable, boost::any const& data) const;
virtual void traverse(ArrayVariable const& variable, boost::any const& data) const;
virtual void traverse(EdgeContainer const& edgeContainer, 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(TemplateEdge const& templateEdge, boost::any const& data) const;
virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const; virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const;

Write Preview
|||||||
100:0
Loading…
Cancel
Save