Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FragmentChecker.h
Go to the documentation of this file.
1#ifndef STORM_LOGIC_FRAGMENTCHECKER_H_
2#define STORM_LOGIC_FRAGMENTCHECKER_H_
3
4#include "storm/logic/FormulaVisitor.h"
5
6#include "storm/logic/FragmentSpecification.h"
7
8namespace storm {
9namespace logic {
10
11class FragmentChecker : public FormulaVisitor {
12 public:
13 bool conformsToSpecification(Formula const& f, FragmentSpecification const& specification) 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_FRAGMENTCHECKER_H_ */
storm::logic::FragmentChecker::conformsToSpecification
bool conformsToSpecification(Formula const &f, FragmentSpecification const &specification) const
Definition FragmentChecker.cpp:22
storm::logic::FragmentChecker::visit
virtual boost::any visit(AtomicExpressionFormula const &f, boost::any const &data) const override
Definition FragmentChecker.cpp:38
storm
LabParser.cpp.
Definition cli.cpp:18