storm::logic::CumulativeRewardFormula Class Reference

#include <CumulativeRewardFormula.h>

Inheritance diagram for storm::logic::CumulativeRewardFormula:

Collaboration diagram for storm::logic::CumulativeRewardFormula:

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

Reimplemented in storm::logic::DiscountedCumulativeRewardFormula.

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.

Reimplemented in storm::logic::DiscountedCumulativeRewardFormula.

Definition at line 57 of file CumulativeRewardFormula.cpp.

getBound() [1/7]

template<typename ValueType>

ValueType storm::logic::CumulativeRewardFormula::getBound

(

)

const

Definition at line 100 of file CumulativeRewardFormula.cpp.

getBound() [2/7]

template double storm::logic::CumulativeRewardFormula::getBound< double >

(

)

const

Definition at line 90 of file CumulativeRewardFormula.cpp.

getBound() [3/7]

template<>

uint64_t storm::logic::CumulativeRewardFormula::getBound

(

unsigned

i

)

const

Definition at line 120 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<>

double storm::logic::CumulativeRewardFormula::getBound

(

unsigned

i

)

const

Definition at line 106 of file CumulativeRewardFormula.cpp.

getBound() [6/7]

template<typename ValueType>

ValueType storm::logic::CumulativeRewardFormula::getBound

(

unsigned

i

)

const

getBound() [7/7]

storm::expressions::Expression const & storm::logic::CumulativeRewardFormula::getBound

(

unsigned

i

)

const

Definition at line 95 of file CumulativeRewardFormula.cpp.

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

uint64_t storm::logic::CumulativeRewardFormula::getNonStrictBound

(

)

const

Definition at line 135 of file CumulativeRewardFormula.cpp.

getNonStrictBound() [2/3]

template<>

double storm::logic::CumulativeRewardFormula::getNonStrictBound

(

)

const

Definition at line 127 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.

Reimplemented in storm::logic::DiscountedCumulativeRewardFormula.

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.

Reimplemented in storm::logic::DiscountedCumulativeRewardFormula.

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