Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | List of all members
storm::logic::QuantileFormula Class Reference

#include <QuantileFormula.h>

Inheritance diagram for storm::logic::QuantileFormula:
Inheritance graph
[legend]
Collaboration diagram for storm::logic::QuantileFormula:
Collaboration graph
[legend]

Public Member Functions

 QuantileFormula (std::vector< storm::expressions::Variable > const &boundVariables, std::shared_ptr< Formula const > subformula)
 
virtual ~QuantileFormula ()
 
virtual bool isQuantileFormula () const override
 
virtual bool hasQuantitativeResult () const override
 
virtual bool hasNumericalResult () const
 
virtual bool hasParetoCurveResult () const
 
Formula const & getSubformula () const
 
uint64_t getDimension () const
 
bool isMultiDimensional () const
 
storm::expressions::Variable const & getBoundVariable () const
 
storm::expressions::Variable const & getBoundVariable (uint64_t index) const
 
std::vector< storm::expressions::Variable > const & getBoundVariables () const
 
virtual boost::any accept (FormulaVisitor const &visitor, boost::any const &data) const override
 
virtual void gatherAtomicExpressionFormulas (std::vector< std::shared_ptr< AtomicExpressionFormula const > > &atomicExpressionFormulas) const override
 
virtual void gatherAtomicLabelFormulas (std::vector< std::shared_ptr< AtomicLabelFormula const > > &atomicLabelFormulas) const override
 
virtual void gatherReferencedRewardModels (std::set< std::string > &referencedRewardModels) const override
 
virtual std::ostream & writeToStream (std::ostream &out, bool allowParentheses=false) const override
 Writes the forumla to the given output stream.
 
- Public Member Functions inherited from storm::logic::StateFormula
virtual ~StateFormula ()
 
virtual bool isStateFormula () const override
 
virtual bool isProbabilityPathFormula () const override
 
- Public Member Functions inherited from storm::logic::Formula
virtual ~Formula ()
 
virtual bool isPathFormula () const
 
virtual bool isConditionalProbabilityFormula () const
 
virtual bool isConditionalRewardFormula () const
 
virtual bool isRewardPathFormula () const
 
virtual bool isTimePathFormula () const
 
virtual bool isBinaryBooleanStateFormula () const
 
virtual bool isUnaryBooleanStateFormula () const
 
virtual bool isBinaryBooleanPathFormula () const
 
virtual bool isUnaryBooleanPathFormula () const
 
virtual bool isMultiObjectiveFormula () const
 
virtual bool isOperatorFormula () const
 
virtual bool isLongRunAverageOperatorFormula () const
 
virtual bool isTimeOperatorFormula () const
 
virtual bool isProbabilityOperatorFormula () const
 
virtual bool isRewardOperatorFormula () const
 
virtual bool isBooleanLiteralFormula () const
 
virtual bool isTrueFormula () const
 
virtual bool isFalseFormula () const
 
virtual bool isAtomicExpressionFormula () const
 
virtual bool isAtomicLabelFormula () const
 
virtual bool isNextFormula () const
 
virtual bool isUntilFormula () const
 
virtual bool isBoundedUntilFormula () const
 
virtual bool isGloballyFormula () const
 
virtual bool isEventuallyFormula () const
 
virtual bool isReachabilityProbabilityFormula () const
 
virtual bool isHOAPathFormula () const
 
virtual bool isCumulativeRewardFormula () const
 
virtual bool isDiscountedCumulativeRewardFormula () const
 
virtual bool isInstantaneousRewardFormula () const
 
virtual bool isReachabilityRewardFormula () const
 
virtual bool isLongRunAverageRewardFormula () const
 
virtual bool isTotalRewardFormula () const
 
virtual bool isDiscountedTotalRewardFormula () const
 
virtual bool isReachabilityTimeFormula () const
 
virtual bool isGameFormula () const
 
virtual bool isBinaryPathFormula () const
 
virtual bool isBinaryStateFormula () const
 
virtual bool isUnaryPathFormula () const
 
virtual bool isUnaryStateFormula () const
 
bool isUnaryFormula () const
 
virtual bool hasQualitativeResult () const
 
bool isInFragment (FragmentSpecification const &fragment) const
 
FormulaInformation info (bool recurseIntoOperators=true) const
 
boost::any accept (FormulaVisitor const &visitor) const
 
bool isInitialFormula () const
 
PathFormula & asPathFormula ()
 
PathFormula const & asPathFormula () const
 
StateFormula & asStateFormula ()
 
StateFormula const & asStateFormula () const
 
MultiObjectiveFormula & asMultiObjectiveFormula ()
 
MultiObjectiveFormula const & asMultiObjectiveFormula () const
 
QuantileFormula & asQuantileFormula ()
 
QuantileFormula const & asQuantileFormula () const
 
BinaryStateFormula & asBinaryStateFormula ()
 
BinaryStateFormula const & asBinaryStateFormula () const
 
UnaryStateFormula & asUnaryStateFormula ()
 
UnaryStateFormula const & asUnaryStateFormula () const
 
BinaryBooleanStateFormula & asBinaryBooleanStateFormula ()
 
BinaryBooleanStateFormula const & asBinaryBooleanStateFormula () const
 
UnaryBooleanStateFormula & asUnaryBooleanStateFormula ()
 
UnaryBooleanStateFormula const & asUnaryBooleanStateFormula () const
 
BooleanLiteralFormula & asBooleanLiteralFormula ()
 
BooleanLiteralFormula const & asBooleanLiteralFormula () const
 
AtomicExpressionFormula & asAtomicExpressionFormula ()
 
AtomicExpressionFormula const & asAtomicExpressionFormula () const
 
AtomicLabelFormula & asAtomicLabelFormula ()
 
AtomicLabelFormula const & asAtomicLabelFormula () const
 
UntilFormula & asUntilFormula ()
 
UntilFormula const & asUntilFormula () const
 
HOAPathFormula & asHOAPathFormula ()
 
HOAPathFormula const & asHOAPathFormula () const
 
BoundedUntilFormula & asBoundedUntilFormula ()
 
BoundedUntilFormula const & asBoundedUntilFormula () const
 
EventuallyFormula & asEventuallyFormula ()
 
EventuallyFormula const & asEventuallyFormula () const
 
EventuallyFormula & asReachabilityProbabilityFormula ()
 
EventuallyFormula const & asReachabilityProbabilityFormula () const
 
EventuallyFormula & asReachabilityRewardFormula ()
 
EventuallyFormula const & asReachabilityRewardFormula () const
 
EventuallyFormula & asReachabilityTimeFormula ()
 
EventuallyFormula const & asReachabilityTimeFormula () const
 
GameFormula & asGameFormula ()
 
GameFormula const & asGameFormula () const
 
GloballyFormula & asGloballyFormula ()
 
GloballyFormula const & asGloballyFormula () const
 
BinaryPathFormula & asBinaryPathFormula ()
 
BinaryPathFormula const & asBinaryPathFormula () const
 
UnaryPathFormula & asUnaryPathFormula ()
 
UnaryPathFormula const & asUnaryPathFormula () const
 
ConditionalFormula & asConditionalFormula ()
 
ConditionalFormula const & asConditionalFormula () const
 
NextFormula & asNextFormula ()
 
NextFormula const & asNextFormula () const
 
LongRunAverageOperatorFormula & asLongRunAverageOperatorFormula ()
 
LongRunAverageOperatorFormula const & asLongRunAverageOperatorFormula () const
 
TimeOperatorFormula & asTimeOperatorFormula ()
 
TimeOperatorFormula const & asTimeOperatorFormula () const
 
CumulativeRewardFormula & asCumulativeRewardFormula ()
 
CumulativeRewardFormula const & asCumulativeRewardFormula () const
 
TotalRewardFormula & asTotalRewardFormula ()
 
TotalRewardFormula const & asTotalRewardFormula () const
 
DiscountedCumulativeRewardFormula & asDiscountedCumulativeRewardFormula ()
 
DiscountedCumulativeRewardFormula const & asDiscountedCumulativeRewardFormula () const
 
DiscountedTotalRewardFormula & asDiscountedTotalRewardFormula ()
 
DiscountedTotalRewardFormula const & asDiscountedTotalRewardFormula () const
 
InstantaneousRewardFormula & asInstantaneousRewardFormula ()
 
InstantaneousRewardFormula const & asInstantaneousRewardFormula () const
 
LongRunAverageRewardFormula & asLongRunAverageRewardFormula ()
 
LongRunAverageRewardFormula const & asLongRunAverageRewardFormula () const
 
ProbabilityOperatorFormula & asProbabilityOperatorFormula ()
 
ProbabilityOperatorFormula const & asProbabilityOperatorFormula () const
 
RewardOperatorFormula & asRewardOperatorFormula ()
 
RewardOperatorFormula const & asRewardOperatorFormula () const
 
OperatorFormula & asOperatorFormula ()
 
OperatorFormula const & asOperatorFormula () const
 
std::vector< std::shared_ptr< AtomicExpressionFormula const > > getAtomicExpressionFormulas () const
 
std::vector< std::shared_ptr< AtomicLabelFormula const > > getAtomicLabelFormulas () const
 
std::set< storm::expressions::Variable > getUsedVariables () const
 
std::set< std::string > getReferencedRewardModels () const
 
std::shared_ptr< Formula const > asSharedPointer ()
 
std::shared_ptr< Formula const > asSharedPointer () const
 
std::shared_ptr< Formula > clone () const
 
std::shared_ptr< Formula > substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 
std::shared_ptr< Formula > substitute (std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &expressionSubstitution) const
 
std::shared_ptr< Formula > substitute (std::map< std::string, storm::expressions::Expression > const &labelSubstitution) const
 
std::shared_ptr< Formula > substitute (std::map< std::string, std::string > const &labelSubstitution) const
 
std::shared_ptr< Formula > substituteRewardModelNames (std::map< std::string, std::string > const &rewardModelNameSubstitution) const
 
std::shared_ptr< Formula > substituteTranscendentalNumbers () const
 
storm::expressions::Expression toExpression (storm::expressions::ExpressionManager const &manager, std::map< std::string, storm::expressions::Expression > const &labelToExpressionMapping={}) const
 Takes the formula and converts it to an equivalent expression.
 
std::string toString () const
 
std::string toPrefixString () const
 
virtual void gatherUsedVariables (std::set< storm::expressions::Variable > &usedVariables) const
 

Additional Inherited Members

- Static Public Member Functions inherited from storm::logic::Formula
static std::shared_ptr< Formula const > getTrueFormula ()
 

Detailed Description

Definition at line 7 of file QuantileFormula.h.

Constructor & Destructor Documentation

◆ QuantileFormula()

storm::logic::QuantileFormula::QuantileFormula ( std::vector< storm::expressions::Variable > const &  boundVariables,
std::shared_ptr< Formula const >  subformula 
)

Definition at line 13 of file QuantileFormula.cpp.

◆ ~QuantileFormula()

storm::logic::QuantileFormula::~QuantileFormula ( )
virtual

Definition at line 18 of file QuantileFormula.cpp.

Member Function Documentation

◆ accept()

boost::any storm::logic::QuantileFormula::accept ( FormulaVisitor const &  visitor,
boost::any const &  data 
) const
overridevirtual

Implements storm::logic::Formula.

Definition at line 66 of file QuantileFormula.cpp.

◆ gatherAtomicExpressionFormulas()

void storm::logic::QuantileFormula::gatherAtomicExpressionFormulas ( std::vector< std::shared_ptr< AtomicExpressionFormula const > > &  atomicExpressionFormulas) const
overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 70 of file QuantileFormula.cpp.

◆ gatherAtomicLabelFormulas()

void storm::logic::QuantileFormula::gatherAtomicLabelFormulas ( std::vector< std::shared_ptr< AtomicLabelFormula const > > &  atomicLabelFormulas) const
overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 74 of file QuantileFormula.cpp.

◆ gatherReferencedRewardModels()

void storm::logic::QuantileFormula::gatherReferencedRewardModels ( std::set< std::string > &  referencedRewardModels) const
overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 78 of file QuantileFormula.cpp.

◆ getBoundVariable() [1/2]

storm::expressions::Variable const & storm::logic::QuantileFormula::getBoundVariable ( ) const

Definition at line 50 of file QuantileFormula.cpp.

◆ getBoundVariable() [2/2]

storm::expressions::Variable const & storm::logic::QuantileFormula::getBoundVariable ( uint64_t  index) const

Definition at line 56 of file QuantileFormula.cpp.

◆ getBoundVariables()

std::vector< storm::expressions::Variable > const & storm::logic::QuantileFormula::getBoundVariables ( ) const

Definition at line 62 of file QuantileFormula.cpp.

◆ getDimension()

uint64_t storm::logic::QuantileFormula::getDimension ( ) const

Definition at line 42 of file QuantileFormula.cpp.

◆ getSubformula()

Formula const & storm::logic::QuantileFormula::getSubformula ( ) const

Definition at line 38 of file QuantileFormula.cpp.

◆ hasNumericalResult()

bool storm::logic::QuantileFormula::hasNumericalResult ( ) const
virtual

Definition at line 30 of file QuantileFormula.cpp.

◆ hasParetoCurveResult()

bool storm::logic::QuantileFormula::hasParetoCurveResult ( ) const
virtual

Definition at line 34 of file QuantileFormula.cpp.

◆ hasQuantitativeResult()

bool storm::logic::QuantileFormula::hasQuantitativeResult ( ) const
overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 26 of file QuantileFormula.cpp.

◆ isMultiDimensional()

bool storm::logic::QuantileFormula::isMultiDimensional ( ) const

Definition at line 46 of file QuantileFormula.cpp.

◆ isQuantileFormula()

bool storm::logic::QuantileFormula::isQuantileFormula ( ) const
overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 22 of file QuantileFormula.cpp.

◆ writeToStream()

std::ostream & storm::logic::QuantileFormula::writeToStream ( std::ostream &  out,
bool  allowParentheses = false 
) const
overridevirtual

Writes the forumla to the given output stream.

Parameters
allowParenthesisif true, the output is potentially surrounded by parentheses depending on whether parentheses are needed to avoid ambiguity when this formula appears as a subformula of some larger formula.
Returns

Implements storm::logic::Formula.

Definition at line 82 of file QuantileFormula.cpp.

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