Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | List of all members
storm::logic::FormulaVisitor Class Referenceabstract

#include <FormulaVisitor.h>

Inheritance diagram for storm::logic::FormulaVisitor:
Inheritance graph
[legend]

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 (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 12 of file FormulaVisitor.h.

Constructor & Destructor Documentation

◆ ~FormulaVisitor()

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

Member Function Documentation

◆ visit() [1/27]

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

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

◆ visit() [2/27]

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

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

◆ visit() [3/27]

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

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

◆ visit() [4/27]

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

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

◆ visit() [5/27]

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

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

◆ visit() [6/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [7/27]

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

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

◆ visit() [8/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [9/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [10/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [11/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [12/27]

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

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

◆ visit() [13/27]

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

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

◆ visit() [14/27]

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

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

◆ visit() [15/27]

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

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

◆ visit() [16/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [17/27]

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

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

◆ visit() [18/27]

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

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

◆ visit() [19/27]

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

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

◆ visit() [20/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [21/27]

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

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

◆ visit() [22/27]

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

Implemented in 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::jani::FormulaToJaniJson.

◆ visit() [23/27]

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, and storm::logic::ToPrefixStringVisitor.

◆ visit() [24/27]

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, and storm::logic::ToPrefixStringVisitor.

◆ visit() [25/27]

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, and storm::logic::ToPrefixStringVisitor.

◆ visit() [26/27]

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, and storm::logic::ToPrefixStringVisitor.

◆ visit() [27/27]

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, and storm::logic::ToPrefixStringVisitor.

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