#include <OperatorFormula.h>

Inheritance diagram for storm::logic::OperatorFormula:

[legend]

Collaboration diagram for storm::logic::OperatorFormula:

[legend]

Public Member Functions
	OperatorFormula (std::shared_ptr< Formula const > const &subformula, OperatorInformation const &operatorInformation=OperatorInformation())
virtual	~OperatorFormula ()
bool	hasBound () const
Bound const &	getBound () const
void	setBound (Bound const &newBound)
void	removeBound ()
ComparisonType	getComparisonType () const
void	setComparisonType (ComparisonType newComparisonType)
storm::expressions::Expression const &	getThreshold () const
template<typename ValueType>
ValueType	getThresholdAs () const
void	setThreshold (storm::expressions::Expression const &newThreshold)
bool	hasOptimalityType () const
storm::solver::OptimizationDirection const &	getOptimalityType () const
void	setOptimalityType (storm::solver::OptimizationDirection newOptimalityType)
void	removeOptimalityType ()
virtual bool	isOperatorFormula () const override
OperatorInformation const &	getOperatorInformation () const
virtual bool	hasQualitativeResult () const override
virtual bool	hasQuantitativeResult () const override
virtual void	gatherUsedVariables (std::set< storm::expressions::Variable > &usedVariables) const override
virtual std::ostream &	writeToStream (std::ostream &out, bool allowParentheses=false) const override
	Writes the forumla to the given output stream.
template<>
double	getThresholdAs () const
template<>
storm::RationalNumber	getThresholdAs () const
template<>
storm::RationalFunction	getThresholdAs () const
template<>
storm::Interval	getThresholdAs () const
template<>
storm::RationalInterval	getThresholdAs () const
Public Member Functions inherited from storm::logic::UnaryStateFormula
	UnaryStateFormula (std::shared_ptr< Formula const > subformula)
virtual	~UnaryStateFormula ()
virtual bool	isUnaryStateFormula () const override
Formula const &	getSubformula () const
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
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	isQuantileFormula () 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
bool	isUnaryFormula () const
bool	isInFragment (FragmentSpecification const &fragment) const
FormulaInformation	info (bool recurseIntoOperators=true) const
boost::any	accept (FormulaVisitor const &visitor) const
virtual boost::any	accept (FormulaVisitor const &visitor, boost::any const &data) const =0
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

Protected Attributes
OperatorInformation	operatorInformation

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

Detailed Description

Definition at line 24 of file OperatorFormula.h.

Constructor & Destructor Documentation

◆ OperatorFormula()

storm::logic::OperatorFormula::OperatorFormula	(	std::shared_ptr< Formula const > const &	subformula,
		OperatorInformation const &	operatorInformation = OperatorInformation() )

Definition at line 19 of file OperatorFormula.cpp.

◆ ~OperatorFormula()

virtual storm::logic::OperatorFormula::~OperatorFormula ( )

inlinevirtual

Definition at line 28 of file OperatorFormula.h.

Member Function Documentation

◆ gatherUsedVariables()

void storm::logic::OperatorFormula::gatherUsedVariables ( std::set< storm::expressions::Variable > & usedVariables ) const

overridevirtual

Reimplemented from storm::logic::UnaryStateFormula.

Definition at line 124 of file OperatorFormula.cpp.

◆ getBound()

Bound const & storm::logic::OperatorFormula::getBound ( ) const

Definition at line 80 of file OperatorFormula.cpp.

◆ getComparisonType()

ComparisonType storm::logic::OperatorFormula::getComparisonType ( ) const

Definition at line 28 of file OperatorFormula.cpp.

◆ getOperatorInformation()

OperatorInformation const & storm::logic::OperatorFormula::getOperatorInformation ( ) const

Definition at line 112 of file OperatorFormula.cpp.

◆ getOptimalityType()

OptimizationDirection const & storm::logic::OperatorFormula::getOptimalityType ( ) const

Definition at line 96 of file OperatorFormula.cpp.

◆ getThreshold()

storm::expressions::Expression const & storm::logic::OperatorFormula::getThreshold ( ) const

Definition at line 37 of file OperatorFormula.cpp.

◆ getThresholdAs() [1/6]

template<>

storm::RationalInterval storm::logic::OperatorFormula::getThresholdAs ( ) const

Definition at line 70 of file OperatorFormula.cpp.

◆ getThresholdAs() [2/6]

template<>

storm::Interval storm::logic::OperatorFormula::getThresholdAs ( ) const

Definition at line 63 of file OperatorFormula.cpp.

◆ getThresholdAs() [3/6]

template<>

storm::RationalFunction storm::logic::OperatorFormula::getThresholdAs ( ) const

Definition at line 56 of file OperatorFormula.cpp.

◆ getThresholdAs() [4/6]

template<>

storm::RationalNumber storm::logic::OperatorFormula::getThresholdAs ( ) const

Definition at line 49 of file OperatorFormula.cpp.

◆ getThresholdAs() [5/6]

template<>

double storm::logic::OperatorFormula::getThresholdAs ( ) const

Definition at line 42 of file OperatorFormula.cpp.

◆ getThresholdAs() [6/6]

template<typename ValueType>

ValueType storm::logic::OperatorFormula::getThresholdAs ( ) const

◆ hasBound()

bool storm::logic::OperatorFormula::hasBound ( ) const

Definition at line 24 of file OperatorFormula.cpp.

◆ hasOptimalityType()

bool storm::logic::OperatorFormula::hasOptimalityType ( ) const

Definition at line 92 of file OperatorFormula.cpp.

◆ hasQualitativeResult()

bool storm::logic::OperatorFormula::hasQualitativeResult ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 116 of file OperatorFormula.cpp.

◆ hasQuantitativeResult()

bool storm::logic::OperatorFormula::hasQuantitativeResult ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 120 of file OperatorFormula.cpp.

◆ isOperatorFormula()

bool storm::logic::OperatorFormula::isOperatorFormula ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 108 of file OperatorFormula.cpp.

◆ removeBound()

void storm::logic::OperatorFormula::removeBound ( )

Definition at line 88 of file OperatorFormula.cpp.

◆ removeOptimalityType()

void storm::logic::OperatorFormula::removeOptimalityType ( )

Definition at line 104 of file OperatorFormula.cpp.

◆ setBound()

void storm::logic::OperatorFormula::setBound ( Bound const & newBound )

Definition at line 84 of file OperatorFormula.cpp.

◆ setComparisonType()

void storm::logic::OperatorFormula::setComparisonType ( ComparisonType newComparisonType )

Definition at line 33 of file OperatorFormula.cpp.

◆ setOptimalityType()

void storm::logic::OperatorFormula::setOptimalityType ( storm::solver::OptimizationDirection newOptimalityType )

Definition at line 100 of file OperatorFormula.cpp.

◆ setThreshold()

void storm::logic::OperatorFormula::setThreshold ( storm::expressions::Expression const & newThreshold )

Definition at line 76 of file OperatorFormula.cpp.

◆ writeToStream()

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

overridevirtual

Writes the forumla to the given output stream.

Parameters

allowParenthesis if 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.

Reimplemented in storm::logic::LongRunAverageOperatorFormula, storm::logic::ProbabilityOperatorFormula, storm::logic::RewardOperatorFormula, and storm::logic::TimeOperatorFormula.

Definition at line 131 of file OperatorFormula.cpp.

Member Data Documentation

◆ operatorInformation

OperatorInformation storm::logic::OperatorFormula::operatorInformation

protected

Definition at line 62 of file OperatorFormula.h.

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

src/storm/logic/OperatorFormula.h
src/storm/logic/OperatorFormula.cpp

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ OperatorFormula()

◆ ~OperatorFormula()

Member Function Documentation

◆ gatherUsedVariables()

◆ getBound()

◆ getComparisonType()

◆ getOperatorInformation()

◆ getOptimalityType()

◆ getThreshold()

◆ getThresholdAs() [1/6]

◆ getThresholdAs() [2/6]

◆ getThresholdAs() [3/6]

◆ getThresholdAs() [4/6]

◆ getThresholdAs() [5/6]

◆ getThresholdAs() [6/6]

◆ hasBound()

◆ hasOptimalityType()

◆ hasQualitativeResult()

◆ hasQuantitativeResult()

◆ isOperatorFormula()

◆ removeBound()

◆ removeOptimalityType()

◆ setBound()

◆ setComparisonType()

◆ setOptimalityType()

◆ setThreshold()

◆ writeToStream()

Member Data Documentation

◆ operatorInformation