#include <FragmentChecker.h>

Inheritance diagram for storm::logic::FragmentChecker:

Collaboration diagram for storm::logic::FragmentChecker:

Public Member Functions
bool	conformsToSpecification (Formula const &f, FragmentSpecification const &specification) const

virtual boost::any	visit (AtomicExpressionFormula const &f, boost::any const &data) const override

virtual boost::any	visit (AtomicLabelFormula const &f, boost::any const &data) const override

virtual boost::any	visit (BinaryBooleanStateFormula const &f, boost::any const &data) const override

virtual boost::any	visit (BinaryBooleanPathFormula const &f, boost::any const &data) const override

virtual boost::any	visit (BooleanLiteralFormula const &f, boost::any const &data) const override

virtual boost::any	visit (BoundedUntilFormula const &f, boost::any const &data) const override

virtual boost::any	visit (ConditionalFormula 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 (TimeOperatorFormula const &f, boost::any const &data) const override

virtual boost::any	visit (GloballyFormula const &f, boost::any const &data) const override

virtual boost::any	visit (GameFormula const &f, boost::any const &data) const override

virtual boost::any	visit (InstantaneousRewardFormula const &f, boost::any const &data) const override

virtual boost::any	visit (LongRunAverageOperatorFormula const &f, boost::any const &data) const override

virtual boost::any	visit (LongRunAverageRewardFormula const &f, boost::any const &data) const override

virtual boost::any	visit (MultiObjectiveFormula const &f, boost::any const &data) const override

virtual boost::any	visit (QuantileFormula const &f, boost::any const &data) const override

virtual boost::any	visit (NextFormula const &f, boost::any const &data) const override

virtual boost::any	visit (ProbabilityOperatorFormula 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

virtual boost::any	visit (UnaryBooleanStateFormula const &f, boost::any const &data) const override

virtual boost::any	visit (UnaryBooleanPathFormula const &f, boost::any const &data) const override

virtual boost::any	visit (UntilFormula const &f, boost::any const &data) const override

virtual boost::any	visit (HOAPathFormula const &f, boost::any const &data) const override

Public Member Functions inherited from storm::logic::FormulaVisitor
virtual	~FormulaVisitor ()=default

Detailed Description

Definition at line 11 of file FragmentChecker.h.

Member Function Documentation

◆ conformsToSpecification()

bool storm::logic::FragmentChecker::conformsToSpecification	(	Formula const &	f,
		FragmentSpecification const &	specification
	)		const

Definition at line 22 of file FragmentChecker.cpp.

◆ visit() [1/25]

boost::any storm::logic::FragmentChecker::visit	(	AtomicExpressionFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 38 of file FragmentChecker.cpp.

◆ visit() [2/25]

boost::any storm::logic::FragmentChecker::visit	(	AtomicLabelFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 43 of file FragmentChecker.cpp.

◆ visit() [3/25]

boost::any storm::logic::FragmentChecker::visit	(	BinaryBooleanPathFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 56 of file FragmentChecker.cpp.

◆ visit() [4/25]

boost::any storm::logic::FragmentChecker::visit	(	BinaryBooleanStateFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 48 of file FragmentChecker.cpp.

◆ visit() [5/25]

boost::any storm::logic::FragmentChecker::visit	(	BooleanLiteralFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 64 of file FragmentChecker.cpp.

◆ visit() [6/25]

boost::any storm::logic::FragmentChecker::visit	(	BoundedUntilFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 69 of file FragmentChecker.cpp.

◆ visit() [7/25]

boost::any storm::logic::FragmentChecker::visit	(	ConditionalFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 111 of file FragmentChecker.cpp.

◆ visit() [8/25]

boost::any storm::logic::FragmentChecker::visit	(	CumulativeRewardFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 131 of file FragmentChecker.cpp.

◆ visit() [9/25]

boost::any storm::logic::FragmentChecker::visit	(	EventuallyFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 154 of file FragmentChecker.cpp.

◆ visit() [10/25]

boost::any storm::logic::FragmentChecker::visit	(	GameFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 201 of file FragmentChecker.cpp.

◆ visit() [11/25]

boost::any storm::logic::FragmentChecker::visit	(	GloballyFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 191 of file FragmentChecker.cpp.

◆ visit() [12/25]

boost::any storm::logic::FragmentChecker::visit	(	HOAPathFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 335 of file FragmentChecker.cpp.

◆ visit() [13/25]

boost::any storm::logic::FragmentChecker::visit	(	InstantaneousRewardFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 207 of file FragmentChecker.cpp.

◆ visit() [14/25]

boost::any storm::logic::FragmentChecker::visit	(	LongRunAverageOperatorFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 212 of file FragmentChecker.cpp.

◆ visit() [15/25]

boost::any storm::logic::FragmentChecker::visit	(	LongRunAverageRewardFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 225 of file FragmentChecker.cpp.

◆ visit() [16/25]

boost::any storm::logic::FragmentChecker::visit	(	MultiObjectiveFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 231 of file FragmentChecker.cpp.

◆ visit() [17/25]

boost::any storm::logic::FragmentChecker::visit	(	NextFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 260 of file FragmentChecker.cpp.

◆ visit() [18/25]

boost::any storm::logic::FragmentChecker::visit	(	ProbabilityOperatorFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 270 of file FragmentChecker.cpp.

◆ visit() [19/25]

boost::any storm::logic::FragmentChecker::visit	(	QuantileFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 252 of file FragmentChecker.cpp.

◆ visit() [20/25]

boost::any storm::logic::FragmentChecker::visit	(	RewardOperatorFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 286 of file FragmentChecker.cpp.

◆ visit() [21/25]

boost::any storm::logic::FragmentChecker::visit	(	TimeOperatorFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 176 of file FragmentChecker.cpp.

◆ visit() [22/25]

boost::any storm::logic::FragmentChecker::visit	(	TotalRewardFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 302 of file FragmentChecker.cpp.

◆ visit() [23/25]

boost::any storm::logic::FragmentChecker::visit	(	UnaryBooleanPathFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 316 of file FragmentChecker.cpp.

◆ visit() [24/25]

boost::any storm::logic::FragmentChecker::visit	(	UnaryBooleanStateFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 309 of file FragmentChecker.cpp.

◆ visit() [25/25]

boost::any storm::logic::FragmentChecker::visit	(	UntilFormula const &	f,
		boost::any const &	data
	)		const

overridevirtual

Implements storm::logic::FormulaVisitor.

Definition at line 323 of file FragmentChecker.cpp.

The documentation for this class was generated from the following files:

src/storm/logic/FragmentChecker.h
src/storm/logic/FragmentChecker.cpp

Public Member Functions

Detailed Description

Member Function Documentation

◆ conformsToSpecification()

◆ visit() [1/25]

◆ visit() [2/25]

◆ visit() [3/25]

◆ visit() [4/25]

◆ visit() [5/25]

◆ visit() [6/25]

◆ visit() [7/25]

◆ visit() [8/25]

◆ visit() [9/25]

◆ visit() [10/25]

◆ visit() [11/25]

◆ visit() [12/25]

◆ visit() [13/25]

◆ visit() [14/25]

◆ visit() [15/25]

◆ visit() [16/25]

◆ visit() [17/25]

◆ visit() [18/25]

◆ visit() [19/25]

◆ visit() [20/25]

◆ visit() [21/25]

◆ visit() [22/25]

◆ visit() [23/25]

◆ visit() [24/25]

◆ visit() [25/25]