#include <CumulativeRewardFormula.h>

Inheritance diagram for storm::logic::CumulativeRewardFormula:

[legend]

Collaboration diagram for storm::logic::CumulativeRewardFormula:

[legend]

Public Member Functions
	CumulativeRewardFormula (TimeBound const &bound, TimeBoundReference const &timeBoundReference=TimeBoundReference(TimeBoundType::Time), boost::optional< RewardAccumulation > rewardAccumulation=boost::none)

	CumulativeRewardFormula (std::vector< TimeBound > const &bounds, std::vector< TimeBoundReference > const &timeBoundReferences, boost::optional< RewardAccumulation > rewardAccumulation=boost::none)

virtual	~CumulativeRewardFormula ()=default

virtual bool	isCumulativeRewardFormula () const override

virtual bool	isRewardPathFormula () const override

bool	isMultiDimensional () const

unsigned	getDimension () const

virtual boost::any	accept (FormulaVisitor const &visitor, boost::any const &data) const override

virtual void	gatherReferencedRewardModels (std::set< std::string > &referencedRewardModels) 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.

TimeBoundReference const &	getTimeBoundReference () const

TimeBoundReference const &	getTimeBoundReference (unsigned i) const

bool	isBoundStrict () const

bool	isBoundStrict (unsigned i) const

bool	hasIntegerBound () const

bool	hasIntegerBound (unsigned i) const

storm::expressions::Expression const &	getBound () const

storm::expressions::Expression const &	getBound (unsigned i) const

template<typename ValueType >
ValueType	getBound () const

template<typename ValueType >
ValueType	getBound (unsigned i) const

template<typename ValueType >
ValueType	getNonStrictBound () const

std::vector< TimeBound > const &	getBounds () const

bool	hasRewardAccumulation () const

RewardAccumulation const &	getRewardAccumulation () const

std::shared_ptr< CumulativeRewardFormula const >	stripRewardAccumulation () const

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

template<>
double	getBound (unsigned i) const

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

template<>
uint64_t	getBound (unsigned i) const

template<>
double	getNonStrictBound () const

template<>
uint64_t	getNonStrictBound () 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	isProbabilityPathFormula () 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	isBoundedUntilFormula () const

virtual bool	isGloballyFormula () const

virtual bool	isEventuallyFormula () const

virtual bool	isReachabilityProbabilityFormula () const

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

virtual bool	hasQualitativeResult () const

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

virtual void	gatherAtomicExpressionFormulas (std::vector< std::shared_ptr< AtomicExpressionFormula const > > &atomicExpressionFormulas) const

virtual void	gatherAtomicLabelFormulas (std::vector< std::shared_ptr< AtomicLabelFormula const > > &atomicLabelFormulas) 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 11 of file CumulativeRewardFormula.h.

Constructor & Destructor Documentation

◆ CumulativeRewardFormula() [1/2]

storm::logic::CumulativeRewardFormula::CumulativeRewardFormula	(	TimeBound const &	bound,
		TimeBoundReference const &	timeBoundReference = `TimeBoundReference(TimeBoundType::Time)`,
		boost::optional< RewardAccumulation >	rewardAccumulation = `boost::none`
	)

Definition at line 16 of file CumulativeRewardFormula.cpp.

◆ CumulativeRewardFormula() [2/2]

storm::logic::CumulativeRewardFormula::CumulativeRewardFormula	(	std::vector< TimeBound > const &	bounds,
		std::vector< TimeBoundReference > const &	timeBoundReferences,
		boost::optional< RewardAccumulation >	rewardAccumulation = `boost::none`
	)

Definition at line 22 of file CumulativeRewardFormula.cpp.

◆ ~CumulativeRewardFormula()

virtual storm::logic::CumulativeRewardFormula::~CumulativeRewardFormula ( )

virtualdefault

Member Function Documentation

◆ accept()

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

overridevirtual

Implements storm::logic::Formula.

Definition at line 45 of file CumulativeRewardFormula.cpp.

◆ gatherReferencedRewardModels()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 49 of file CumulativeRewardFormula.cpp.

◆ gatherUsedVariables()

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

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 57 of file CumulativeRewardFormula.cpp.

◆ getBound() [1/7]

template double storm::logic::CumulativeRewardFormula::getBound< double > ( ) const

Definition at line 90 of file CumulativeRewardFormula.cpp.

◆ getBound() [2/7]

template<typename ValueType >

ValueType storm::logic::CumulativeRewardFormula::getBound ( ) const

Definition at line 100 of file CumulativeRewardFormula.cpp.

◆ getBound() [3/7]

template<>

double storm::logic::CumulativeRewardFormula::getBound ( unsigned i ) const

Definition at line 106 of file CumulativeRewardFormula.cpp.

◆ getBound() [4/7]

template<>

storm::RationalNumber storm::logic::CumulativeRewardFormula::getBound ( unsigned i ) const

Definition at line 113 of file CumulativeRewardFormula.cpp.

◆ getBound() [5/7]

template<>

uint64_t storm::logic::CumulativeRewardFormula::getBound ( unsigned i ) const

Definition at line 120 of file CumulativeRewardFormula.cpp.

◆ getBound() [6/7]

storm::expressions::Expression const & storm::logic::CumulativeRewardFormula::getBound ( unsigned i ) const

Definition at line 95 of file CumulativeRewardFormula.cpp.

◆ getBound() [7/7]

template<typename ValueType >

ValueType storm::logic::CumulativeRewardFormula::getBound ( unsigned i ) const

◆ getBounds()

std::vector< TimeBound > const & storm::logic::CumulativeRewardFormula::getBounds ( ) const

Definition at line 146 of file CumulativeRewardFormula.cpp.

◆ getDimension()

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

Definition at line 41 of file CumulativeRewardFormula.cpp.

◆ getNonStrictBound() [1/3]

template<>

double storm::logic::CumulativeRewardFormula::getNonStrictBound ( ) const

Definition at line 127 of file CumulativeRewardFormula.cpp.

◆ getNonStrictBound() [2/3]

template<>

uint64_t storm::logic::CumulativeRewardFormula::getNonStrictBound ( ) const

Definition at line 135 of file CumulativeRewardFormula.cpp.

◆ getNonStrictBound() [3/3]

template<typename ValueType >

ValueType storm::logic::CumulativeRewardFormula::getNonStrictBound ( ) const

◆ getRewardAccumulation()

RewardAccumulation const & storm::logic::CumulativeRewardFormula::getRewardAccumulation ( ) const

Definition at line 159 of file CumulativeRewardFormula.cpp.

◆ getTimeBoundReference() [1/2]

TimeBoundReference const & storm::logic::CumulativeRewardFormula::getTimeBoundReference ( ) const

Definition at line 63 of file CumulativeRewardFormula.cpp.

◆ getTimeBoundReference() [2/2]

TimeBoundReference const & storm::logic::CumulativeRewardFormula::getTimeBoundReference ( unsigned i ) const

Definition at line 68 of file CumulativeRewardFormula.cpp.

◆ hasIntegerBound() [1/2]

bool storm::logic::CumulativeRewardFormula::hasIntegerBound ( ) const

Definition at line 81 of file CumulativeRewardFormula.cpp.

◆ hasIntegerBound() [2/2]

bool storm::logic::CumulativeRewardFormula::hasIntegerBound ( unsigned i ) const

Definition at line 86 of file CumulativeRewardFormula.cpp.

◆ hasRewardAccumulation()

bool storm::logic::CumulativeRewardFormula::hasRewardAccumulation ( ) const

Definition at line 155 of file CumulativeRewardFormula.cpp.

◆ isBoundStrict() [1/2]

bool storm::logic::CumulativeRewardFormula::isBoundStrict ( ) const

Definition at line 72 of file CumulativeRewardFormula.cpp.

◆ isBoundStrict() [2/2]

bool storm::logic::CumulativeRewardFormula::isBoundStrict ( unsigned i ) const

Definition at line 77 of file CumulativeRewardFormula.cpp.

◆ isCumulativeRewardFormula()

bool storm::logic::CumulativeRewardFormula::isCumulativeRewardFormula ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 29 of file CumulativeRewardFormula.cpp.

◆ isMultiDimensional()

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

Definition at line 37 of file CumulativeRewardFormula.cpp.

◆ isRewardPathFormula()

bool storm::logic::CumulativeRewardFormula::isRewardPathFormula ( ) const

overridevirtual

Reimplemented from storm::logic::Formula.

Definition at line 33 of file CumulativeRewardFormula.cpp.

◆ restrictToDimension()

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

Definition at line 167 of file CumulativeRewardFormula.cpp.

◆ stripRewardAccumulation()

std::shared_ptr< CumulativeRewardFormula const > storm::logic::CumulativeRewardFormula::stripRewardAccumulation ( ) const

Definition at line 163 of file CumulativeRewardFormula.cpp.

◆ writeToStream()

std::ostream & storm::logic::CumulativeRewardFormula::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 171 of file CumulativeRewardFormula.cpp.

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

src/storm/logic/CumulativeRewardFormula.h
src/storm/logic/CumulativeRewardFormula.cpp

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ CumulativeRewardFormula() [1/2]

◆ CumulativeRewardFormula() [2/2]

◆ ~CumulativeRewardFormula()

Member Function Documentation

◆ accept()

◆ gatherReferencedRewardModels()

◆ gatherUsedVariables()

◆ getBound() [1/7]

◆ getBound() [2/7]

◆ getBound() [3/7]

◆ getBound() [4/7]

◆ getBound() [5/7]

◆ getBound() [6/7]

◆ getBound() [7/7]

◆ getBounds()

◆ getDimension()

◆ getNonStrictBound() [1/3]

◆ getNonStrictBound() [2/3]

◆ getNonStrictBound() [3/3]

◆ getRewardAccumulation()

◆ getTimeBoundReference() [1/2]

◆ getTimeBoundReference() [2/2]

◆ hasIntegerBound() [1/2]

◆ hasIntegerBound() [2/2]

◆ hasRewardAccumulation()

◆ isBoundStrict() [1/2]

◆ isBoundStrict() [2/2]

◆ isCumulativeRewardFormula()

◆ isMultiDimensional()

◆ isRewardPathFormula()

◆ restrictToDimension()

◆ stripRewardAccumulation()

◆ writeToStream()