Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ToExpressionVisitor.h
Go to the documentation of this file.
1#ifndef STORM_LOGIC_TOEXPRESSIONVISITOR_H_
2#define STORM_LOGIC_TOEXPRESSIONVISITOR_H_
3
4#include "storm/logic/FormulaVisitor.h"
5
6#include "storm/storage/expressions/Expression.h"
7
8namespace storm {
9namespace logic {
10
11class ToExpressionVisitor : public FormulaVisitor {
12 public:
13 storm::expressions::Expression toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const;
14
15 virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
16 virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
17 virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
18 virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
19 virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
20 virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
21 virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
22 virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
23 virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
24 virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
25 virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
26 virtual boost::any visit(GameFormula const& f, boost::any const& data) const override;
27 virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
28 virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
29 virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
30 virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
31 virtual boost::any visit(QuantileFormula const& f, boost::any const& data) const override;
32 virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
33 virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
34 virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
35 virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
36 virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
37 virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
38 virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
39 virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
40};
41
42} // namespace logic
43} // namespace storm
44
45#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:72
storm::logic::ToExpressionVisitor::visit
virtual boost::any visit(AtomicExpressionFormula const &f, boost::any const &data) const override
Definition ToExpressionVisitor.cpp:19
storm::logic::ToExpressionVisitor::toExpression
storm::expressions::Expression toExpression(Formula const &f, storm::expressions::ExpressionManager const &manager) const
Definition ToExpressionVisitor.cpp:14
storm
LabParser.cpp.
Definition cli.cpp:18