storm::logic::FormulaVisitor Class Reference

#include <FormulaVisitor.h>

Inheritance diagram for storm::logic::FormulaVisitor:

Public Member Functions
virtual	~FormulaVisitor ()=default
virtual boost::any	visit (AtomicExpressionFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (AtomicLabelFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (BinaryBooleanStateFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (BinaryBooleanPathFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (BooleanLiteralFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (BoundedUntilFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (ConditionalFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (CumulativeRewardFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (EventuallyFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (TimeOperatorFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (GloballyFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (GameFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (InstantaneousRewardFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (LongRunAverageOperatorFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (LongRunAverageRewardFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (MultiObjectiveFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (QuantileFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (NextFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (ProbabilityOperatorFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (RewardOperatorFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (TotalRewardFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (UnaryBooleanStateFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (UnaryBooleanPathFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (UntilFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (WeakUntilFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (ReleaseFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (HOAPathFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (DiscountedCumulativeRewardFormula const &f, boost::any const &data) const =0
virtual boost::any	visit (DiscountedTotalRewardFormula const &f, boost::any const &data) const =0

Detailed Description

Definition at line 11 of file FormulaVisitor.h.

Constructor & Destructor Documentation

~FormulaVisitor()

virtual storm::logic::FormulaVisitor::~FormulaVisitor ( )

virtualdefault

Member Function Documentation

visit() [1/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [2/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LabelSubstitutionVisitor, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [3/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [4/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [5/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [6/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::RewardModelNameSubstitutionVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [7/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [8/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::RewardModelNameSubstitutionVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [9/29]

virtual boost::any storm::logic::FormulaVisitor::visit ( DiscountedCumulativeRewardFormula const & f, boost::any const & data ) const

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::RewardModelNameSubstitutionVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [10/29]

virtual boost::any storm::logic::FormulaVisitor::visit ( DiscountedTotalRewardFormula const & f, boost::any const & data ) const

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [11/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [12/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [13/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [14/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [15/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [16/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [17/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [18/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [19/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [20/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [21/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [22/29]

virtual boost::any storm::logic::FormulaVisitor::visit ( ReleaseFormula const & f, boost::any const & data ) const

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [23/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::RewardModelNameSubstitutionVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [24/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExpectedTimeToExpectedRewardVisitor, storm::logic::ExpressionSubstitutionVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [25/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::RewardAccumulationEliminationVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [26/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [27/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [28/29]

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

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

visit() [29/29]

virtual boost::any storm::logic::FormulaVisitor::visit ( WeakUntilFormula const & f, boost::any const & data ) const

pure virtual

Implemented in storm::jani::FormulaToJaniJson, storm::logic::CloneVisitor, storm::logic::ExtractMaximalStateFormulasVisitor, storm::logic::FormulaInformationVisitor, storm::logic::FragmentChecker, storm::logic::LiftableTransitionRewardsVisitor, storm::logic::ToExpressionVisitor, storm::logic::ToPrefixStringVisitor, and storm::logic::TraverseFormulaVisitor.

---

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

• src/storm/logic/FormulaVisitor.h