TimQu
7 years ago
55 changed files with 1179 additions and 225 deletions
-
9CHANGELOG.md
-
5src/storm-cli-utilities/model-handling.h
-
4src/storm-conv-cli/storm-conv.cpp
-
8src/storm-conv/api/storm-conv.cpp
-
4src/storm-conv/api/storm-conv.h
-
10src/storm-conv/settings/modules/JaniExportSettings.cpp
-
15src/storm-conv/settings/modules/JaniExportSettings.h
-
38src/storm-gspn-cli/storm-gspn.cpp
-
36src/storm-gspn/api/storm-gspn.cpp
-
6src/storm-gspn/api/storm-gspn.h
-
34src/storm-gspn/builder/JaniGSPNBuilder.cpp
-
106src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
-
11src/storm-gspn/parser/GreatSpnEditorProjectParser.h
-
5src/storm-gspn/parser/GspnParser.cpp
-
2src/storm-gspn/parser/GspnParser.h
-
12src/storm-gspn/settings/modules/GSPNSettings.cpp
-
13src/storm-gspn/settings/modules/GSPNSettings.h
-
20src/storm-gspn/storage/gspn/GSPN.cpp
-
11src/storm-gspn/storage/gspn/GSPN.h
-
24src/storm-gspn/storage/gspn/GspnBuilder.cpp
-
15src/storm-gspn/storage/gspn/GspnBuilder.h
-
11src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
-
47src/storm-gspn/storage/gspn/TimedTransition.h
-
83src/storm-parsers/parser/JaniParser.cpp
-
4src/storm-parsers/parser/JaniParser.h
-
2src/storm-pgcl-cli/storm-pgcl.cpp
-
1src/storm/builder/DdPrismModelBuilder.h
-
6src/storm/logic/BoundedUntilFormula.cpp
-
10src/storm/logic/CloneVisitor.cpp
-
22src/storm/logic/CumulativeRewardFormula.cpp
-
9src/storm/logic/CumulativeRewardFormula.h
-
14src/storm/logic/EventuallyFormula.cpp
-
8src/storm/logic/EventuallyFormula.h
-
17src/storm/logic/FragmentChecker.cpp
-
13src/storm/logic/FragmentSpecification.cpp
-
12src/storm/logic/FragmentSpecification.h
-
51src/storm/logic/RewardAccumulation.cpp
-
27src/storm/logic/RewardAccumulation.h
-
153src/storm/logic/RewardAccumulationEliminationVisitor.cpp
-
39src/storm/logic/RewardAccumulationEliminationVisitor.h
-
19src/storm/logic/TimeBoundType.h
-
10src/storm/logic/TotalRewardFormula.cpp
-
13src/storm/logic/TotalRewardFormula.h
-
4src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
-
4src/storm/storage/jani/Automaton.cpp
-
2src/storm/storage/jani/Automaton.h
-
6src/storm/storage/jani/EdgeContainer.cpp
-
2src/storm/storage/jani/EdgeContainer.h
-
145src/storm/storage/jani/JSONExporter.cpp
-
18src/storm/storage/jani/JSONExporter.h
-
14src/storm/storage/jani/OrderedAssignments.cpp
-
47src/storm/storage/jani/traverser/AssignmentsFinder.cpp
-
29src/storm/storage/jani/traverser/AssignmentsFinder.h
-
138src/storm/storage/jani/traverser/JaniTraverser.cpp
-
36src/storm/storage/jani/traverser/JaniTraverser.h
@ -0,0 +1,51 @@ |
|||
#include "storm/logic/RewardAccumulation.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : steps(steps), time(time), exit(exit){ |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
bool RewardAccumulation::isStepsSet() const { |
|||
return steps; |
|||
} |
|||
|
|||
bool RewardAccumulation::isTimeSet() const { |
|||
return time; |
|||
} |
|||
|
|||
bool RewardAccumulation::isExitSet() const { |
|||
return exit; |
|||
} |
|||
|
|||
bool RewardAccumulation::isEmpty() const { |
|||
return !isStepsSet() && !isTimeSet() && !isExitSet(); |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) { |
|||
bool hasEntry = false; |
|||
if (acc.isStepsSet()) { |
|||
out << "steps"; |
|||
hasEntry = true; |
|||
} |
|||
if (acc.isTimeSet()) { |
|||
if (hasEntry) { |
|||
out << ", "; |
|||
} |
|||
out << "time"; |
|||
hasEntry = true; |
|||
} |
|||
if (acc.isExitSet()) { |
|||
if (hasEntry) { |
|||
out << ", "; |
|||
} |
|||
out << "exit"; |
|||
hasEntry = true; |
|||
} |
|||
|
|||
return out; |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,27 @@ |
|||
#pragma once |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class RewardAccumulation { |
|||
public: |
|||
RewardAccumulation(bool steps, bool time, bool exit); |
|||
RewardAccumulation(RewardAccumulation const& other) = default; |
|||
|
|||
bool isStepsSet() const; // If set, choice rewards and transition rewards are accumulated upon taking the transition |
|||
bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states) |
|||
bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state |
|||
|
|||
// Returns true iff accumulation for all types of reward is disabled. |
|||
bool isEmpty() const; |
|||
|
|||
private: |
|||
bool time, steps, exit; |
|||
}; |
|||
|
|||
std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc); |
|||
|
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,153 @@ |
|||
#include "storm/logic/RewardAccumulationEliminationVisitor.h"
|
|||
#include "storm/logic/Formulas.h"
|
|||
|
|||
#include "storm/storage/jani/Model.h"
|
|||
#include "storm/storage/jani/traverser/AssignmentsFinder.h"
|
|||
#include "storm/utility/macros.h"
|
|||
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
#include "storm/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
std::shared_ptr<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { |
|||
boost::any result = f.accept(*this, boost::any()); |
|||
return boost::any_cast<std::shared_ptr<Formula>>(result); |
|||
} |
|||
|
|||
void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const { |
|||
for (auto& p : properties) { |
|||
auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula()); |
|||
auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula()); |
|||
storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states); |
|||
p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment()); |
|||
} |
|||
} |
|||
|
|||
boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { |
|||
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds; |
|||
std::vector<TimeBoundReference> timeBoundReferences; |
|||
for (uint64_t i = 0; i < f.getDimension(); ++i) { |
|||
if (f.hasLowerBound(i)) { |
|||
lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i))); |
|||
} else { |
|||
lowerBounds.emplace_back(); |
|||
} |
|||
if (f.hasUpperBound(i)) { |
|||
upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i))); |
|||
} else { |
|||
upperBounds.emplace_back(); |
|||
} |
|||
storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i); |
|||
if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) { |
|||
// Eliminate accumulation
|
|||
tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none); |
|||
} |
|||
timeBoundReferences.push_back(std::move(tbr)); |
|||
} |
|||
if (f.hasMultiDimensionalSubformulas()) { |
|||
std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas; |
|||
for (uint64_t i = 0; i < f.getDimension(); ++i) { |
|||
leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data))); |
|||
rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data))); |
|||
} |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); |
|||
} else { |
|||
std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data)); |
|||
std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data)); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences)); |
|||
} |
|||
} |
|||
|
|||
boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { |
|||
boost::optional<storm::logic::RewardAccumulation> rewAcc; |
|||
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); |
|||
auto rewName = boost::any_cast<boost::optional<std::string>>(data); |
|||
if (f.hasRewardAccumulation() && !canEliminate(f.getRewardAccumulation(), rewName)) { |
|||
rewAcc = f.getRewardAccumulation(); |
|||
} |
|||
|
|||
std::vector<TimeBound> bounds; |
|||
std::vector<TimeBoundReference> timeBoundReferences; |
|||
for (uint64_t i = 0; i < f.getDimension(); ++i) { |
|||
bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i))); |
|||
storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i); |
|||
if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) { |
|||
// Eliminate accumulation
|
|||
tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none); |
|||
} |
|||
timeBoundReferences.push_back(std::move(tbr)); |
|||
} |
|||
return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc)); |
|||
} |
|||
|
|||
boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); |
|||
if (f.hasRewardAccumulation()) { |
|||
if (f.isTimePathFormula()) { |
|||
if (model.isDiscreteTimeModel() && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation())); |
|||
} else if (!model.isDiscreteTimeModel() && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation())); |
|||
} |
|||
} else if (f.isRewardPathFormula()) { |
|||
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); |
|||
auto rewName = boost::any_cast<boost::optional<std::string>>(data); |
|||
if (!canEliminate(f.getRewardAccumulation(), rewName)) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation())); |
|||
} |
|||
} |
|||
} |
|||
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext())); |
|||
} |
|||
|
|||
boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { |
|||
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName())); |
|||
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); |
|||
} |
|||
|
|||
boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { |
|||
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); |
|||
auto rewName = boost::any_cast<boost::optional<std::string>>(data); |
|||
if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>()); |
|||
} else { |
|||
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation())); |
|||
} |
|||
} |
|||
|
|||
bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const { |
|||
STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model."); |
|||
storm::jani::AssignmentsFinder::ResultType assignmentKinds; |
|||
STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << "."); |
|||
storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get()); |
|||
if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) { |
|||
assignmentKinds.hasLocationAssignment = true; |
|||
assignmentKinds.hasEdgeAssignment = true; |
|||
assignmentKinds.hasEdgeDestinationAssignment = true; |
|||
} |
|||
assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); |
|||
if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) { |
|||
return false; |
|||
} |
|||
if (assignmentKinds.hasLocationAssignment) { |
|||
if (model.isDiscreteTimeModel()) { |
|||
if (!accumulation.isExitSet()) { |
|||
return false; |
|||
} |
|||
// accumulating over time in discrete time models has no effect, i.e., the value of accumulation.isTimeSet() does not matter here.
|
|||
} else { |
|||
if (accumulation.isExitSet() || !accumulation.isTimeSet()) { |
|||
return false; |
|||
} |
|||
} |
|||
} |
|||
return true; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,39 @@ |
|||
#pragma once |
|||
|
|||
#include <unordered_map> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/logic/CloneVisitor.h" |
|||
#include "storm/logic/RewardAccumulation.h" |
|||
#include "storm/storage/jani/Model.h" |
|||
#include "storm/storage/jani/Property.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
|
|||
class RewardAccumulationEliminationVisitor : public CloneVisitor { |
|||
public: |
|||
RewardAccumulationEliminationVisitor(storm::jani::Model const& model); |
|||
|
|||
/*! |
|||
* Eliminates any reward accumulations of the formula, where the presence of the reward accumulation does not change the result of the formula |
|||
*/ |
|||
std::shared_ptr<Formula> eliminateRewardAccumulations(Formula const& f) const; |
|||
|
|||
void eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const; |
|||
|
|||
virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; |
|||
virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; |
|||
|
|||
|
|||
private: |
|||
bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const; |
|||
|
|||
storm::jani::Model const& model; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -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<std::pair<Variable const*, ResultType*>>(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<std::pair<Variable const*, ResultType*>>(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<std::pair<Variable const*, ResultType*>>(data); |
|||
for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) { |
|||
if (assignment.getVariable() == *resVar.first) { |
|||
resVar.second->hasEdgeDestinationAssignment = true; |
|||
} |
|||
} |
|||
JaniTraverser::traverse(templateEdgeDestination, data); |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,29 @@ |
|||
#pragma once |
|||
|
|||
|
|||
#include <boost/any.hpp> |
|||
|
|||
#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; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,138 @@ |
|||
#include "storm/storage/jani/traverser/JaniTraverser.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace jani { |
|||
void JaniTraverser::traverse(Model const& model, boost::any const& 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); |
|||
} |
|||
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 const& automaton, boost::any const& data) const { |
|||
traverse(automaton.getVariables(), data); |
|||
for (auto const& loc : automaton.getLocations()) { |
|||
traverse(loc, data); |
|||
} |
|||
traverse(automaton.getEdgeContainer(), data); |
|||
if (automaton.hasInitialStatesRestriction()) { |
|||
traverse(automaton.getInitialStatesRestriction(), 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 const& 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 const& data) const { |
|||
traverse(location.getAssignments(), data); |
|||
} |
|||
|
|||
void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const { |
|||
if (variable.hasInitExpression()) { |
|||
traverse(variable.getInitExpression(), data); |
|||
} |
|||
} |
|||
|
|||
void JaniTraverser::traverse(BoundedIntegerVariable const& 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 const& variable, boost::any const& data) const { |
|||
if (variable.hasInitExpression()) { |
|||
traverse(variable.getInitExpression(), data); |
|||
} |
|||
} |
|||
|
|||
void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const { |
|||
if (variable.hasInitExpression()) { |
|||
traverse(variable.getInitExpression(), data); |
|||
} |
|||
} |
|||
|
|||
void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& 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 const& 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 const& data) const { |
|||
traverse(templateEdgeDestination.getOrderedAssignments(), 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 const& data) const { |
|||
traverse(edgeDestination.getProbability(), data); |
|||
} |
|||
|
|||
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 const& data) const { |
|||
traverse(assignment.getAssignedExpression(), data); |
|||
} |
|||
|
|||
void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const { |
|||
// intentionally left empty.
|
|||
} |
|||
|
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,36 @@ |
|||
#pragma once |
|||
|
|||
|
|||
#include <boost/any.hpp> |
|||
|
|||
#include "storm/storage/jani/Model.h" |
|||
|
|||
namespace storm { |
|||
namespace jani { |
|||
class JaniTraverser { |
|||
public: |
|||
virtual ~JaniTraverser() = default; |
|||
|
|||
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(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; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
Reference in new issue
xxxxxxxxxx