storm::logic::BoundedUntilFormula Class Reference

#include <BoundedUntilFormula.h>

Inheritance diagram for storm::logic::BoundedUntilFormula:

Collaboration diagram for storm::logic::BoundedUntilFormula:

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	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
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

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 16 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 28 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 41 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 70 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 74 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 86 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 98 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 119 of file BoundedUntilFormula.cpp.

getDimension()

unsigned storm::logic::BoundedUntilFormula::getDimension

(

)

const

Definition at line 162 of file BoundedUntilFormula.cpp.

getLeftSubformula() [1/2]

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

(

)

const

Definition at line 166 of file BoundedUntilFormula.cpp.

getLeftSubformula() [2/2]

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

(

unsigned

i

)

const

Definition at line 171 of file BoundedUntilFormula.cpp.

getLowerBound() [1/5]

template<>

uint64_t storm::logic::BoundedUntilFormula::getLowerBound

(

unsigned

i

)

const

Definition at line 295 of file BoundedUntilFormula.cpp.

getLowerBound() [2/5]

template<>

storm::RationalNumber storm::logic::BoundedUntilFormula::getLowerBound

(

unsigned

i

)

const

Definition at line 274 of file BoundedUntilFormula.cpp.

getLowerBound() [3/5]

template<>

double storm::logic::BoundedUntilFormula::getLowerBound

(

unsigned

i

)

const

Definition at line 255 of file BoundedUntilFormula.cpp.

getLowerBound() [4/5]

template<typename ValueType>

ValueType storm::logic::BoundedUntilFormula::getLowerBound

(

unsigned

i = 0

)

const

getLowerBound() [5/5]

storm::expressions::Expression const & storm::logic::BoundedUntilFormula::getLowerBound

(

unsigned

i = 0

)

const

Definition at line 246 of file BoundedUntilFormula.cpp.

getNonStrictLowerBound() [1/3]

template<>

uint64_t storm::logic::BoundedUntilFormula::getNonStrictLowerBound

(

unsigned

i

)

const

Definition at line 340 of file BoundedUntilFormula.cpp.

getNonStrictLowerBound() [2/3]

template<>

double storm::logic::BoundedUntilFormula::getNonStrictLowerBound

(

unsigned

i

)

const

Definition at line 333 of file BoundedUntilFormula.cpp.

getNonStrictLowerBound() [3/3]

template<typename ValueType>

ValueType storm::logic::BoundedUntilFormula::getNonStrictLowerBound

(

unsigned

i = 0

)

const

getNonStrictUpperBound() [1/3]

template<>

uint64_t storm::logic::BoundedUntilFormula::getNonStrictUpperBound

(

unsigned

i

)

const

Definition at line 322 of file BoundedUntilFormula.cpp.

getNonStrictUpperBound() [2/3]

template<>

double storm::logic::BoundedUntilFormula::getNonStrictUpperBound

(

unsigned

i

)

const

Definition at line 314 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 179 of file BoundedUntilFormula.cpp.

getRightSubformula() [2/2]

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

(

unsigned

i

)

const

Definition at line 184 of file BoundedUntilFormula.cpp.

getTimeBoundReference()

TimeBoundReference const & storm::logic::BoundedUntilFormula::getTimeBoundReference

(

unsigned

i = 0

)

const

Definition at line 192 of file BoundedUntilFormula.cpp.

getUpperBound() [1/5]

template<>

uint64_t storm::logic::BoundedUntilFormula::getUpperBound

(

unsigned

i

)

const

Definition at line 306 of file BoundedUntilFormula.cpp.

getUpperBound() [2/5]

template<>

storm::RationalNumber storm::logic::BoundedUntilFormula::getUpperBound

(

unsigned

i

)

const

Definition at line 286 of file BoundedUntilFormula.cpp.

getUpperBound() [3/5]

template<>

double storm::logic::BoundedUntilFormula::getUpperBound

(

unsigned

i

)

const

Definition at line 266 of file BoundedUntilFormula.cpp.

getUpperBound() [4/5]

template<typename ValueType>

ValueType storm::logic::BoundedUntilFormula::getUpperBound

(

unsigned

i = 0

)

const

getUpperBound() [5/5]

storm::expressions::Expression const & storm::logic::BoundedUntilFormula::getUpperBound

(

unsigned

i = 0

)

const

Definition at line 250 of file BoundedUntilFormula.cpp.

hasIntegerLowerBound()

bool storm::logic::BoundedUntilFormula::hasIntegerLowerBound

(

unsigned

i = 0

)

const

Definition at line 218 of file BoundedUntilFormula.cpp.

hasIntegerUpperBound()

bool storm::logic::BoundedUntilFormula::hasIntegerUpperBound

(

unsigned

i = 0

)

const

Definition at line 242 of file BoundedUntilFormula.cpp.

hasLowerBound() [1/2]

bool storm::logic::BoundedUntilFormula::hasLowerBound

(

)

const

Definition at line 205 of file BoundedUntilFormula.cpp.

hasLowerBound() [2/2]

bool storm::logic::BoundedUntilFormula::hasLowerBound

(

unsigned

i

)

const

Definition at line 214 of file BoundedUntilFormula.cpp.

hasMultiDimensionalSubformulas()

bool storm::logic::BoundedUntilFormula::hasMultiDimensionalSubformulas

(

)

const

Definition at line 156 of file BoundedUntilFormula.cpp.

hasQualitativeResult()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 143 of file BoundedUntilFormula.cpp.

hasQuantitativeResult()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 147 of file BoundedUntilFormula.cpp.

hasUpperBound() [1/2]

bool storm::logic::BoundedUntilFormula::hasUpperBound

(

)

const

Definition at line 229 of file BoundedUntilFormula.cpp.

hasUpperBound() [2/2]

bool storm::logic::BoundedUntilFormula::hasUpperBound

(

unsigned

i

)

const

Definition at line 238 of file BoundedUntilFormula.cpp.

isBoundedUntilFormula()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 62 of file BoundedUntilFormula.cpp.

isLowerBoundStrict()

bool storm::logic::BoundedUntilFormula::isLowerBoundStrict

(

unsigned

i = 0

)

const

Definition at line 197 of file BoundedUntilFormula.cpp.

isMultiDimensional()

bool storm::logic::BoundedUntilFormula::isMultiDimensional

(

)

const

Definition at line 151 of file BoundedUntilFormula.cpp.

isProbabilityPathFormula()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 66 of file BoundedUntilFormula.cpp.

isUpperBoundStrict()

bool storm::logic::BoundedUntilFormula::isUpperBoundStrict

(

unsigned

i = 0

)

const

Definition at line 225 of file BoundedUntilFormula.cpp.

restrictToDimension()

std::shared_ptr< BoundedUntilFormula const > storm::logic::BoundedUntilFormula::restrictToDimension

(

unsigned

i

)

const

Definition at line 354 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 359 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