#include <BoundedUntilFormula.h>

Inheritance diagram for storm::logic::BoundedUntilFormula:

[legend]

Collaboration diagram for storm::logic::BoundedUntilFormula:

[legend]

Public Member Functions
	BoundedUntilFormula (std::shared_ptr< Formula const > const &leftSubformula, std::shared_ptr< Formula const > const &rightSubformula, boost::optional< TimeBound > const &lowerBound, boost::optional< TimeBound > const &upperBound, TimeBoundReference const &timeBoundReference)

	BoundedUntilFormula (std::shared_ptr< Formula const > const &leftSubformula, std::shared_ptr< Formula const > const &rightSubformula, std::vector< boost::optional< TimeBound > > const &lowerBounds, std::vector< boost::optional< TimeBound > > const &upperBounds, std::vector< TimeBoundReference > const &timeBoundReferences)

	BoundedUntilFormula (std::vector< std::shared_ptr< Formula const > > const &leftSubformulas, std::vector< std::shared_ptr< Formula const > > const &rightSubformulas, std::vector< boost::optional< TimeBound > > const &lowerBounds, std::vector< boost::optional< TimeBound > > const &upperBounds, std::vector< TimeBoundReference > const &timeBoundReferences)

virtual bool	isBoundedUntilFormula () const override

virtual bool	isProbabilityPathFormula () const override

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 void	gatherUsedVariables (std::set< storm::expressions::Variable > &usedVariables) const override

virtual bool	hasQualitativeResult () const override

virtual bool	hasQuantitativeResult () const override

bool	isMultiDimensional () const

bool	hasMultiDimensionalSubformulas () const

unsigned	getDimension () const

Formula const &	getLeftSubformula () const

Formula const &	getLeftSubformula (unsigned i) const

Formula const &	getRightSubformula () const

Formula const &	getRightSubformula (unsigned i) const

TimeBoundReference const &	getTimeBoundReference (unsigned i=0) const

bool	isLowerBoundStrict (unsigned i=0) const

bool	hasLowerBound () const

bool	hasLowerBound (unsigned i) const

bool	hasIntegerLowerBound (unsigned i=0) const

bool	isUpperBoundStrict (unsigned i=0) const

bool	hasUpperBound () const

bool	hasUpperBound (unsigned i) const

bool	hasIntegerUpperBound (unsigned i=0) const

storm::expressions::Expression const &	getLowerBound (unsigned i=0) const

storm::expressions::Expression const &	getUpperBound (unsigned i=0) const

template<typename ValueType >
ValueType	getLowerBound (unsigned i=0) const

template<typename ValueType >
ValueType	getUpperBound (unsigned i=0) const

template<typename ValueType >
ValueType	getNonStrictUpperBound (unsigned i=0) const

template<typename ValueType >
ValueType	getNonStrictLowerBound (unsigned i=0) const

std::shared_ptr< BoundedUntilFormula const >	restrictToDimension (unsigned i) const

virtual std::ostream &	writeToStream (std::ostream &out, bool allowParentheses=false) const override
	Writes the forumla to the given output stream.

template<>
double	getLowerBound (unsigned i) const

template<>
double	getUpperBound (unsigned i) const

template<>
storm::RationalNumber	getLowerBound (unsigned i) const

template<>
storm::RationalNumber	getUpperBound (unsigned i) const

template<>
uint64_t	getLowerBound (unsigned i) const

template<>
uint64_t	getUpperBound (unsigned i) const

template<>
double	getNonStrictUpperBound (unsigned i) const

template<>
uint64_t	getNonStrictUpperBound (unsigned i) const

template<>
double	getNonStrictLowerBound (unsigned i) const

template<>
uint64_t	getNonStrictLowerBound (unsigned i) const

Public Member Functions inherited from storm::logic::PathFormula
virtual	~PathFormula ()

virtual bool	isPathFormula () const override

Public Member Functions inherited from storm::logic::Formula
virtual	~Formula ()

virtual bool	isStateFormula () 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	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	isGloballyFormula () const

virtual bool	isEventuallyFormula () const

virtual bool	isReachabilityProbabilityFormula () const

virtual bool	isHOAPathFormula () const

virtual bool	isCumulativeRewardFormula () const

virtual bool	isInstantaneousRewardFormula () const

virtual bool	isReachabilityRewardFormula () const

virtual bool	isLongRunAverageRewardFormula () const

virtual bool	isTotalRewardFormula () 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

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

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

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

Detailed Description

Definition at line 12 of file BoundedUntilFormula.h.

Constructor & Destructor Documentation

◆ BoundedUntilFormula() [1/3]

storm::logic::BoundedUntilFormula::BoundedUntilFormula	(	std::shared_ptr< Formula const > const &	leftSubformula,
		std::shared_ptr< Formula const > const &	rightSubformula,
		boost::optional< TimeBound > const &	lowerBound,
		boost::optional< TimeBound > const &	upperBound,
		TimeBoundReference const &	timeBoundReference
	)

Definition at line 18 of file BoundedUntilFormula.cpp.

◆ BoundedUntilFormula() [2/3]

storm::logic::BoundedUntilFormula::BoundedUntilFormula	(	std::shared_ptr< Formula const > const &	leftSubformula,
		std::shared_ptr< Formula const > const &	rightSubformula,
		std::vector< boost::optional< TimeBound > > const &	lowerBounds,
		std::vector< boost::optional< TimeBound > > const &	upperBounds,
		std::vector< TimeBoundReference > const &	timeBoundReferences
	)

Definition at line 30 of file BoundedUntilFormula.cpp.

◆ BoundedUntilFormula() [3/3]

storm::logic::BoundedUntilFormula::BoundedUntilFormula	(	std::vector< std::shared_ptr< Formula const > > const &	leftSubformulas,
		std::vector< std::shared_ptr< Formula const > > const &	rightSubformulas,
		std::vector< boost::optional< TimeBound > > const &	lowerBounds,
		std::vector< boost::optional< TimeBound > > const &	upperBounds,
		std::vector< TimeBoundReference > const &	timeBoundReferences
	)

Definition at line 43 of file BoundedUntilFormula.cpp.

Member Function Documentation

◆ accept()

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

overridevirtual

Implements storm::logic::Formula.

Definition at line 72 of file BoundedUntilFormula.cpp.

◆ gatherAtomicExpressionFormulas()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 76 of file BoundedUntilFormula.cpp.

◆ gatherAtomicLabelFormulas()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 88 of file BoundedUntilFormula.cpp.

◆ gatherReferencedRewardModels()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 100 of file BoundedUntilFormula.cpp.

◆ gatherUsedVariables()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 121 of file BoundedUntilFormula.cpp.

◆ getDimension()

unsigned storm::logic::BoundedUntilFormula::getDimension ( ) const

Definition at line 164 of file BoundedUntilFormula.cpp.

◆ getLeftSubformula() [1/2]

Formula const & storm::logic::BoundedUntilFormula::getLeftSubformula ( ) const

Definition at line 168 of file BoundedUntilFormula.cpp.

◆ getLeftSubformula() [2/2]

Formula const & storm::logic::BoundedUntilFormula::getLeftSubformula ( unsigned i ) const

Definition at line 173 of file BoundedUntilFormula.cpp.

◆ getLowerBound() [1/5]

template<>

double storm::logic::BoundedUntilFormula::getLowerBound ( unsigned i ) const

Definition at line 257 of file BoundedUntilFormula.cpp.

◆ getLowerBound() [2/5]

template<>

storm::RationalNumber storm::logic::BoundedUntilFormula::getLowerBound ( unsigned i ) const

Definition at line 276 of file BoundedUntilFormula.cpp.

◆ getLowerBound() [3/5]

template<>

uint64_t storm::logic::BoundedUntilFormula::getLowerBound ( unsigned i ) const

Definition at line 297 of file BoundedUntilFormula.cpp.

◆ getLowerBound() [4/5]

storm::expressions::Expression const & storm::logic::BoundedUntilFormula::getLowerBound ( unsigned i = 0 ) const

Definition at line 248 of file BoundedUntilFormula.cpp.

◆ getLowerBound() [5/5]

template<typename ValueType >

ValueType storm::logic::BoundedUntilFormula::getLowerBound ( unsigned i = 0 ) const

◆ getNonStrictLowerBound() [1/3]

template<>

double storm::logic::BoundedUntilFormula::getNonStrictLowerBound ( unsigned i ) const

Definition at line 335 of file BoundedUntilFormula.cpp.

◆ getNonStrictLowerBound() [2/3]

template<>

uint64_t storm::logic::BoundedUntilFormula::getNonStrictLowerBound ( unsigned i ) const

Definition at line 342 of file BoundedUntilFormula.cpp.

◆ getNonStrictLowerBound() [3/3]

template<typename ValueType >

ValueType storm::logic::BoundedUntilFormula::getNonStrictLowerBound ( unsigned i = 0 ) const

◆ getNonStrictUpperBound() [1/3]

template<>

double storm::logic::BoundedUntilFormula::getNonStrictUpperBound ( unsigned i ) const

Definition at line 316 of file BoundedUntilFormula.cpp.

◆ getNonStrictUpperBound() [2/3]

template<>

uint64_t storm::logic::BoundedUntilFormula::getNonStrictUpperBound ( unsigned i ) const

Definition at line 324 of file BoundedUntilFormula.cpp.

◆ getNonStrictUpperBound() [3/3]

template<typename ValueType >

ValueType storm::logic::BoundedUntilFormula::getNonStrictUpperBound ( unsigned i = 0 ) const

◆ getRightSubformula() [1/2]

Formula const & storm::logic::BoundedUntilFormula::getRightSubformula ( ) const

Definition at line 181 of file BoundedUntilFormula.cpp.

◆ getRightSubformula() [2/2]

Formula const & storm::logic::BoundedUntilFormula::getRightSubformula ( unsigned i ) const

Definition at line 186 of file BoundedUntilFormula.cpp.

◆ getTimeBoundReference()

TimeBoundReference const & storm::logic::BoundedUntilFormula::getTimeBoundReference ( unsigned i = 0 ) const

Definition at line 194 of file BoundedUntilFormula.cpp.

◆ getUpperBound() [1/5]

template<>

double storm::logic::BoundedUntilFormula::getUpperBound ( unsigned i ) const

Definition at line 268 of file BoundedUntilFormula.cpp.

◆ getUpperBound() [2/5]

template<>

storm::RationalNumber storm::logic::BoundedUntilFormula::getUpperBound ( unsigned i ) const

Definition at line 288 of file BoundedUntilFormula.cpp.

◆ getUpperBound() [3/5]

template<>

uint64_t storm::logic::BoundedUntilFormula::getUpperBound ( unsigned i ) const

Definition at line 308 of file BoundedUntilFormula.cpp.

◆ getUpperBound() [4/5]

storm::expressions::Expression const & storm::logic::BoundedUntilFormula::getUpperBound ( unsigned i = 0 ) const

Definition at line 252 of file BoundedUntilFormula.cpp.

◆ getUpperBound() [5/5]

template<typename ValueType >

ValueType storm::logic::BoundedUntilFormula::getUpperBound ( unsigned i = 0 ) const

◆ hasIntegerLowerBound()

bool storm::logic::BoundedUntilFormula::hasIntegerLowerBound ( unsigned i = 0 ) const

Definition at line 220 of file BoundedUntilFormula.cpp.

◆ hasIntegerUpperBound()

bool storm::logic::BoundedUntilFormula::hasIntegerUpperBound ( unsigned i = 0 ) const

Definition at line 244 of file BoundedUntilFormula.cpp.

◆ hasLowerBound() [1/2]

bool storm::logic::BoundedUntilFormula::hasLowerBound ( ) const

Definition at line 207 of file BoundedUntilFormula.cpp.

◆ hasLowerBound() [2/2]

bool storm::logic::BoundedUntilFormula::hasLowerBound ( unsigned i ) const

Definition at line 216 of file BoundedUntilFormula.cpp.

◆ hasMultiDimensionalSubformulas()

bool storm::logic::BoundedUntilFormula::hasMultiDimensionalSubformulas ( ) const

Definition at line 158 of file BoundedUntilFormula.cpp.

◆ hasQualitativeResult()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 145 of file BoundedUntilFormula.cpp.

◆ hasQuantitativeResult()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 149 of file BoundedUntilFormula.cpp.

◆ hasUpperBound() [1/2]

bool storm::logic::BoundedUntilFormula::hasUpperBound ( ) const

Definition at line 231 of file BoundedUntilFormula.cpp.

◆ hasUpperBound() [2/2]

bool storm::logic::BoundedUntilFormula::hasUpperBound ( unsigned i ) const

Definition at line 240 of file BoundedUntilFormula.cpp.

◆ isBoundedUntilFormula()

bool storm::logic::BoundedUntilFormula::isBoundedUntilFormula ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 64 of file BoundedUntilFormula.cpp.

◆ isLowerBoundStrict()

bool storm::logic::BoundedUntilFormula::isLowerBoundStrict ( unsigned i = 0 ) const

Definition at line 199 of file BoundedUntilFormula.cpp.

◆ isMultiDimensional()

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

Definition at line 153 of file BoundedUntilFormula.cpp.

◆ isProbabilityPathFormula()

bool storm::logic::BoundedUntilFormula::isProbabilityPathFormula ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 68 of file BoundedUntilFormula.cpp.

◆ isUpperBoundStrict()

bool storm::logic::BoundedUntilFormula::isUpperBoundStrict ( unsigned i = 0 ) const

Definition at line 227 of file BoundedUntilFormula.cpp.

◆ restrictToDimension()

std::shared_ptr< BoundedUntilFormula const > storm::logic::BoundedUntilFormula::restrictToDimension ( unsigned i ) const

Definition at line 356 of file BoundedUntilFormula.cpp.

◆ writeToStream()

std::ostream & storm::logic::BoundedUntilFormula::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.

Definition at line 361 of file BoundedUntilFormula.cpp.

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

src/storm/logic/BoundedUntilFormula.h
src/storm/logic/BoundedUntilFormula.cpp

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BoundedUntilFormula() [1/3]

◆ BoundedUntilFormula() [2/3]

◆ BoundedUntilFormula() [3/3]

Member Function Documentation

◆ accept()

◆ gatherAtomicExpressionFormulas()

◆ gatherAtomicLabelFormulas()

◆ gatherReferencedRewardModels()

◆ gatherUsedVariables()

◆ getDimension()

◆ getLeftSubformula() [1/2]

◆ getLeftSubformula() [2/2]

◆ getLowerBound() [1/5]

◆ getLowerBound() [2/5]

◆ getLowerBound() [3/5]

◆ getLowerBound() [4/5]

◆ getLowerBound() [5/5]

◆ getNonStrictLowerBound() [1/3]

◆ getNonStrictLowerBound() [2/3]

◆ getNonStrictLowerBound() [3/3]

◆ getNonStrictUpperBound() [1/3]

◆ getNonStrictUpperBound() [2/3]

◆ getNonStrictUpperBound() [3/3]

◆ getRightSubformula() [1/2]

◆ getRightSubformula() [2/2]

◆ getTimeBoundReference()

◆ getUpperBound() [1/5]

◆ getUpperBound() [2/5]

◆ getUpperBound() [3/5]

◆ getUpperBound() [4/5]

◆ getUpperBound() [5/5]

◆ hasIntegerLowerBound()

◆ hasIntegerUpperBound()

◆ hasLowerBound() [1/2]

◆ hasLowerBound() [2/2]

◆ hasMultiDimensionalSubformulas()

◆ hasQualitativeResult()

◆ hasQuantitativeResult()

◆ hasUpperBound() [1/2]

◆ hasUpperBound() [2/2]

◆ isBoundedUntilFormula()

◆ isLowerBoundStrict()

◆ isMultiDimensional()

◆ isProbabilityPathFormula()

◆ isUpperBoundStrict()

◆ restrictToDimension()

◆ writeToStream()