storm::logic::Formula Class Reference

#include <Formula.h>

Inheritance diagram for storm::logic::Formula:

Collaboration diagram for storm::logic::Formula:

Public Member Functions
virtual	~Formula ()
virtual bool	isPathFormula () const
virtual bool	isStateFormula () const
virtual bool	isConditionalProbabilityFormula () const
virtual bool	isConditionalRewardFormula () const
virtual bool	isProbabilityPathFormula () 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	isBoundedUntilFormula () const
virtual bool	isGloballyFormula () const
virtual bool	isEventuallyFormula () const
virtual bool	isReachabilityProbabilityFormula () const
virtual bool	isWeakUntilFormula () const
virtual bool	isReleaseFormula () 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
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
virtual boost::any	accept (FormulaVisitor const &visitor, boost::any const &data) const =0
void	traverse (std::function< bool(Formula const &)> const &callback) const
	Invokes the given callback on this formula and on its subformulas in pre-order, i.e., a formula is visited before its subformulas.
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
WeakUntilFormula &	asWeakUntilFormula ()
WeakUntilFormula const &	asWeakUntilFormula () const
ReleaseFormula &	asReleaseFormula ()
ReleaseFormula const &	asReleaseFormula () 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
virtual std::ostream &	writeToStream (std::ostream &out, bool allowParentheses=false) const =0
	Writes the forumla to the given output stream.
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
virtual void	gatherReferencedRewardModels (std::set< std::string > &referencedRewardModels) const
virtual void	gatherUsedVariables (std::set< storm::expressions::Variable > &usedVariables) const

Static Public Member Functions
static std::shared_ptr< Formula const >	getTrueFormula ()

Friends
std::ostream &	operator<< (std::ostream &out, Formula const &formula)

Detailed Description

Definition at line 31 of file Formula.h.

Constructor & Destructor Documentation

~Formula()

virtual storm::logic::Formula::~Formula ( )

inlinevirtual

Definition at line 34 of file Formula.h.

Member Function Documentation

accept() [1/2]

boost::any storm::logic::Formula::accept

(

FormulaVisitor const &

visitor

)

const

Definition at line 17 of file Formula.cpp.

accept() [2/2]

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

pure virtual

Implemented in storm::logic::AtomicExpressionFormula, storm::logic::AtomicLabelFormula, storm::logic::BinaryBooleanPathFormula, storm::logic::BinaryBooleanStateFormula, storm::logic::BooleanLiteralFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::CumulativeRewardFormula, storm::logic::DiscountedCumulativeRewardFormula, storm::logic::DiscountedTotalRewardFormula, storm::logic::EventuallyFormula, storm::logic::GameFormula, storm::logic::GloballyFormula, storm::logic::HOAPathFormula, storm::logic::InstantaneousRewardFormula, storm::logic::LongRunAverageOperatorFormula, storm::logic::LongRunAverageRewardFormula, storm::logic::MultiObjectiveFormula, storm::logic::NextFormula, storm::logic::ProbabilityOperatorFormula, storm::logic::QuantileFormula, storm::logic::ReleaseFormula, storm::logic::RewardOperatorFormula, storm::logic::TimeOperatorFormula, storm::logic::TotalRewardFormula, storm::logic::UnaryBooleanPathFormula, storm::logic::UnaryBooleanStateFormula, storm::logic::UntilFormula, and storm::logic::WeakUntilFormula.

asAtomicExpressionFormula() [1/2]

AtomicExpressionFormula & storm::logic::Formula::asAtomicExpressionFormula

(

)

Definition at line 315 of file Formula.cpp.

asAtomicExpressionFormula() [2/2]

AtomicExpressionFormula const & storm::logic::Formula::asAtomicExpressionFormula

(

)

const

Definition at line 319 of file Formula.cpp.

asAtomicLabelFormula() [1/2]

AtomicLabelFormula & storm::logic::Formula::asAtomicLabelFormula

(

)

Definition at line 323 of file Formula.cpp.

asAtomicLabelFormula() [2/2]

AtomicLabelFormula const & storm::logic::Formula::asAtomicLabelFormula

(

)

const

Definition at line 327 of file Formula.cpp.

asBinaryBooleanStateFormula() [1/2]

BinaryBooleanStateFormula & storm::logic::Formula::asBinaryBooleanStateFormula

(

)

Definition at line 291 of file Formula.cpp.

asBinaryBooleanStateFormula() [2/2]

BinaryBooleanStateFormula const & storm::logic::Formula::asBinaryBooleanStateFormula

(

)

const

Definition at line 295 of file Formula.cpp.

asBinaryPathFormula() [1/2]

BinaryPathFormula & storm::logic::Formula::asBinaryPathFormula

(

)

Definition at line 419 of file Formula.cpp.

asBinaryPathFormula() [2/2]

BinaryPathFormula const & storm::logic::Formula::asBinaryPathFormula

(

)

const

Definition at line 423 of file Formula.cpp.

asBinaryStateFormula() [1/2]

BinaryStateFormula & storm::logic::Formula::asBinaryStateFormula

(

)

Definition at line 267 of file Formula.cpp.

asBinaryStateFormula() [2/2]

BinaryStateFormula const & storm::logic::Formula::asBinaryStateFormula

(

)

const

Definition at line 271 of file Formula.cpp.

asBooleanLiteralFormula() [1/2]

BooleanLiteralFormula & storm::logic::Formula::asBooleanLiteralFormula

(

)

Definition at line 307 of file Formula.cpp.

asBooleanLiteralFormula() [2/2]

BooleanLiteralFormula const & storm::logic::Formula::asBooleanLiteralFormula

(

)

const

Definition at line 311 of file Formula.cpp.

asBoundedUntilFormula() [1/2]

BoundedUntilFormula & storm::logic::Formula::asBoundedUntilFormula

(

)

Definition at line 363 of file Formula.cpp.

asBoundedUntilFormula() [2/2]

BoundedUntilFormula const & storm::logic::Formula::asBoundedUntilFormula

(

)

const

Definition at line 367 of file Formula.cpp.

asConditionalFormula() [1/2]

ConditionalFormula & storm::logic::Formula::asConditionalFormula

(

)

Definition at line 283 of file Formula.cpp.

asConditionalFormula() [2/2]

ConditionalFormula const & storm::logic::Formula::asConditionalFormula

(

)

const

Definition at line 287 of file Formula.cpp.

asCumulativeRewardFormula() [1/2]

CumulativeRewardFormula & storm::logic::Formula::asCumulativeRewardFormula

(

)

Definition at line 459 of file Formula.cpp.

asCumulativeRewardFormula() [2/2]

CumulativeRewardFormula const & storm::logic::Formula::asCumulativeRewardFormula

(

)

const

Definition at line 463 of file Formula.cpp.

asDiscountedCumulativeRewardFormula() [1/2]

DiscountedCumulativeRewardFormula & storm::logic::Formula::asDiscountedCumulativeRewardFormula

(

)

Definition at line 475 of file Formula.cpp.

asDiscountedCumulativeRewardFormula() [2/2]

DiscountedCumulativeRewardFormula const & storm::logic::Formula::asDiscountedCumulativeRewardFormula

(

)

const

Definition at line 479 of file Formula.cpp.

asDiscountedTotalRewardFormula() [1/2]

DiscountedTotalRewardFormula & storm::logic::Formula::asDiscountedTotalRewardFormula

(

)

Definition at line 483 of file Formula.cpp.

asDiscountedTotalRewardFormula() [2/2]

DiscountedTotalRewardFormula const & storm::logic::Formula::asDiscountedTotalRewardFormula

(

)

const

Definition at line 486 of file Formula.cpp.

asEventuallyFormula() [1/2]

EventuallyFormula & storm::logic::Formula::asEventuallyFormula

(

)

Definition at line 371 of file Formula.cpp.

asEventuallyFormula() [2/2]

EventuallyFormula const & storm::logic::Formula::asEventuallyFormula

(

)

const

Definition at line 375 of file Formula.cpp.

asGameFormula() [1/2]

GameFormula & storm::logic::Formula::asGameFormula

(

)

Definition at line 403 of file Formula.cpp.

asGameFormula() [2/2]

GameFormula const & storm::logic::Formula::asGameFormula

(

)

const

Definition at line 407 of file Formula.cpp.

asGloballyFormula() [1/2]

GloballyFormula & storm::logic::Formula::asGloballyFormula

(

)

Definition at line 411 of file Formula.cpp.

asGloballyFormula() [2/2]

GloballyFormula const & storm::logic::Formula::asGloballyFormula

(

)

const

Definition at line 415 of file Formula.cpp.

asHOAPathFormula() [1/2]

HOAPathFormula & storm::logic::Formula::asHOAPathFormula

(

)

Definition at line 331 of file Formula.cpp.

asHOAPathFormula() [2/2]

HOAPathFormula const & storm::logic::Formula::asHOAPathFormula

(

)

const

Definition at line 335 of file Formula.cpp.

asInstantaneousRewardFormula() [1/2]

InstantaneousRewardFormula & storm::logic::Formula::asInstantaneousRewardFormula

(

)

Definition at line 490 of file Formula.cpp.

asInstantaneousRewardFormula() [2/2]

InstantaneousRewardFormula const & storm::logic::Formula::asInstantaneousRewardFormula

(

)

const

Definition at line 494 of file Formula.cpp.

asLongRunAverageOperatorFormula() [1/2]

LongRunAverageOperatorFormula & storm::logic::Formula::asLongRunAverageOperatorFormula

(

)

Definition at line 443 of file Formula.cpp.

asLongRunAverageOperatorFormula() [2/2]

LongRunAverageOperatorFormula const & storm::logic::Formula::asLongRunAverageOperatorFormula

(

)

const

Definition at line 447 of file Formula.cpp.

asLongRunAverageRewardFormula() [1/2]

LongRunAverageRewardFormula & storm::logic::Formula::asLongRunAverageRewardFormula

(

)

Definition at line 498 of file Formula.cpp.

asLongRunAverageRewardFormula() [2/2]

LongRunAverageRewardFormula const & storm::logic::Formula::asLongRunAverageRewardFormula

(

)

const

Definition at line 502 of file Formula.cpp.

asMultiObjectiveFormula() [1/2]

MultiObjectiveFormula & storm::logic::Formula::asMultiObjectiveFormula

(

)

Definition at line 251 of file Formula.cpp.

asMultiObjectiveFormula() [2/2]

MultiObjectiveFormula const & storm::logic::Formula::asMultiObjectiveFormula

(

)

const

Definition at line 255 of file Formula.cpp.

asNextFormula() [1/2]

NextFormula & storm::logic::Formula::asNextFormula

(

)

Definition at line 435 of file Formula.cpp.

asNextFormula() [2/2]

NextFormula const & storm::logic::Formula::asNextFormula

(

)

const

Definition at line 439 of file Formula.cpp.

asOperatorFormula() [1/2]

OperatorFormula & storm::logic::Formula::asOperatorFormula

(

)

Definition at line 522 of file Formula.cpp.

asOperatorFormula() [2/2]

OperatorFormula const & storm::logic::Formula::asOperatorFormula

(

)

const

Definition at line 526 of file Formula.cpp.

asPathFormula() [1/2]

PathFormula & storm::logic::Formula::asPathFormula

(

)

Definition at line 235 of file Formula.cpp.

asPathFormula() [2/2]

PathFormula const & storm::logic::Formula::asPathFormula

(

)

const

Definition at line 239 of file Formula.cpp.

asProbabilityOperatorFormula() [1/2]

ProbabilityOperatorFormula & storm::logic::Formula::asProbabilityOperatorFormula

(

)

Definition at line 506 of file Formula.cpp.

asProbabilityOperatorFormula() [2/2]

ProbabilityOperatorFormula const & storm::logic::Formula::asProbabilityOperatorFormula

(

)

const

Definition at line 510 of file Formula.cpp.

asQuantileFormula() [1/2]

QuantileFormula & storm::logic::Formula::asQuantileFormula

(

)

Definition at line 259 of file Formula.cpp.

asQuantileFormula() [2/2]

QuantileFormula const & storm::logic::Formula::asQuantileFormula

(

)

const

Definition at line 263 of file Formula.cpp.

asReachabilityProbabilityFormula() [1/2]

EventuallyFormula & storm::logic::Formula::asReachabilityProbabilityFormula

(

)

Definition at line 387 of file Formula.cpp.

asReachabilityProbabilityFormula() [2/2]

EventuallyFormula const & storm::logic::Formula::asReachabilityProbabilityFormula

(

)

const

Definition at line 391 of file Formula.cpp.

asReachabilityRewardFormula() [1/2]

EventuallyFormula & storm::logic::Formula::asReachabilityRewardFormula

(

)

Definition at line 379 of file Formula.cpp.

asReachabilityRewardFormula() [2/2]

EventuallyFormula const & storm::logic::Formula::asReachabilityRewardFormula

(

)

const

Definition at line 383 of file Formula.cpp.

asReachabilityTimeFormula() [1/2]

EventuallyFormula & storm::logic::Formula::asReachabilityTimeFormula

(

)

Definition at line 395 of file Formula.cpp.

asReachabilityTimeFormula() [2/2]

EventuallyFormula const & storm::logic::Formula::asReachabilityTimeFormula

(

)

const

Definition at line 399 of file Formula.cpp.

asReleaseFormula() [1/2]

ReleaseFormula & storm::logic::Formula::asReleaseFormula

(

)

Definition at line 355 of file Formula.cpp.

asReleaseFormula() [2/2]

ReleaseFormula const & storm::logic::Formula::asReleaseFormula

(

)

const

Definition at line 359 of file Formula.cpp.

asRewardOperatorFormula() [1/2]

RewardOperatorFormula & storm::logic::Formula::asRewardOperatorFormula

(

)

Definition at line 514 of file Formula.cpp.

asRewardOperatorFormula() [2/2]

RewardOperatorFormula const & storm::logic::Formula::asRewardOperatorFormula

(

)

const

Definition at line 518 of file Formula.cpp.

asSharedPointer() [1/2]

std::shared_ptr< Formula const > storm::logic::Formula::asSharedPointer

(

)

Definition at line 601 of file Formula.cpp.

asSharedPointer() [2/2]

std::shared_ptr< Formula const > storm::logic::Formula::asSharedPointer

(

)

const

Definition at line 605 of file Formula.cpp.

asStateFormula() [1/2]

StateFormula & storm::logic::Formula::asStateFormula

(

)

Definition at line 243 of file Formula.cpp.

asStateFormula() [2/2]

StateFormula const & storm::logic::Formula::asStateFormula

(

)

const

Definition at line 247 of file Formula.cpp.

asTimeOperatorFormula() [1/2]

TimeOperatorFormula & storm::logic::Formula::asTimeOperatorFormula

(

)

Definition at line 451 of file Formula.cpp.

asTimeOperatorFormula() [2/2]

TimeOperatorFormula const & storm::logic::Formula::asTimeOperatorFormula

(

)

const

Definition at line 455 of file Formula.cpp.

asTotalRewardFormula() [1/2]

TotalRewardFormula & storm::logic::Formula::asTotalRewardFormula

(

)

Definition at line 467 of file Formula.cpp.

asTotalRewardFormula() [2/2]

TotalRewardFormula const & storm::logic::Formula::asTotalRewardFormula

(

)

const

Definition at line 471 of file Formula.cpp.

asUnaryBooleanStateFormula() [1/2]

UnaryBooleanStateFormula & storm::logic::Formula::asUnaryBooleanStateFormula

(

)

Definition at line 299 of file Formula.cpp.

asUnaryBooleanStateFormula() [2/2]

UnaryBooleanStateFormula const & storm::logic::Formula::asUnaryBooleanStateFormula

(

)

const

Definition at line 303 of file Formula.cpp.

asUnaryPathFormula() [1/2]

UnaryPathFormula & storm::logic::Formula::asUnaryPathFormula

(

)

Definition at line 427 of file Formula.cpp.

asUnaryPathFormula() [2/2]

UnaryPathFormula const & storm::logic::Formula::asUnaryPathFormula

(

)

const

Definition at line 431 of file Formula.cpp.

asUnaryStateFormula() [1/2]

UnaryStateFormula & storm::logic::Formula::asUnaryStateFormula

(

)

Definition at line 275 of file Formula.cpp.

asUnaryStateFormula() [2/2]

UnaryStateFormula const & storm::logic::Formula::asUnaryStateFormula

(

)

const

Definition at line 279 of file Formula.cpp.

asUntilFormula() [1/2]

UntilFormula & storm::logic::Formula::asUntilFormula

(

)

Definition at line 339 of file Formula.cpp.

asUntilFormula() [2/2]

UntilFormula const & storm::logic::Formula::asUntilFormula

(

)

const

Definition at line 343 of file Formula.cpp.

asWeakUntilFormula() [1/2]

WeakUntilFormula & storm::logic::Formula::asWeakUntilFormula

(

)

Definition at line 347 of file Formula.cpp.

asWeakUntilFormula() [2/2]

WeakUntilFormula const & storm::logic::Formula::asWeakUntilFormula

(

)

const

Definition at line 351 of file Formula.cpp.

clone()

std::shared_ptr< Formula > storm::logic::Formula::clone

(

)

const

Definition at line 554 of file Formula.cpp.

gatherAtomicExpressionFormulas()

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

virtual

Reimplemented in storm::logic::AtomicExpressionFormula, storm::logic::BinaryPathFormula, storm::logic::BinaryStateFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::HOAPathFormula, storm::logic::MultiObjectiveFormula, storm::logic::QuantileFormula, storm::logic::UnaryPathFormula, and storm::logic::UnaryStateFormula.

Definition at line 609 of file Formula.cpp.

gatherAtomicLabelFormulas()

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

virtual

Reimplemented in storm::logic::AtomicLabelFormula, storm::logic::BinaryPathFormula, storm::logic::BinaryStateFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::HOAPathFormula, storm::logic::MultiObjectiveFormula, storm::logic::QuantileFormula, storm::logic::UnaryPathFormula, and storm::logic::UnaryStateFormula.

Definition at line 611 of file Formula.cpp.

gatherReferencedRewardModels()

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

virtual

Reimplemented in storm::logic::BinaryPathFormula, storm::logic::BinaryStateFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::CumulativeRewardFormula, storm::logic::HOAPathFormula, storm::logic::MultiObjectiveFormula, storm::logic::QuantileFormula, storm::logic::RewardOperatorFormula, storm::logic::UnaryPathFormula, and storm::logic::UnaryStateFormula.

Definition at line 613 of file Formula.cpp.

gatherUsedVariables()

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

virtual

Reimplemented in storm::logic::AtomicExpressionFormula, storm::logic::BinaryPathFormula, storm::logic::BinaryStateFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::CumulativeRewardFormula, storm::logic::DiscountedCumulativeRewardFormula, storm::logic::DiscountedTotalRewardFormula, storm::logic::InstantaneousRewardFormula, storm::logic::MultiObjectiveFormula, storm::logic::OperatorFormula, storm::logic::UnaryPathFormula, and storm::logic::UnaryStateFormula.

Definition at line 615 of file Formula.cpp.

getAtomicExpressionFormulas()

std::vector< std::shared_ptr< AtomicExpressionFormula const > > storm::logic::Formula::getAtomicExpressionFormulas

(

)

const

Definition at line 530 of file Formula.cpp.

getAtomicLabelFormulas()

std::vector< std::shared_ptr< AtomicLabelFormula const > > storm::logic::Formula::getAtomicLabelFormulas

(

)

const

Definition at line 536 of file Formula.cpp.

getReferencedRewardModels()

std::set< std::string > storm::logic::Formula::getReferencedRewardModels

(

)

const

Definition at line 548 of file Formula.cpp.

getTrueFormula()

std::shared_ptr< Formula const > storm::logic::Formula::getTrueFormula ( )

static

Definition at line 227 of file Formula.cpp.

getUsedVariables()

std::set< storm::expressions::Variable > storm::logic::Formula::getUsedVariables

(

)

const

Definition at line 542 of file Formula.cpp.

hasQualitativeResult()

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

virtual

Reimplemented in storm::logic::BinaryPathFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::GameFormula, storm::logic::HOAPathFormula, storm::logic::MultiObjectiveFormula, storm::logic::OperatorFormula, and storm::logic::UnaryPathFormula.

Definition at line 210 of file Formula.cpp.

hasQuantitativeResult()

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

virtual

Reimplemented in storm::logic::BinaryPathFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::GameFormula, storm::logic::HOAPathFormula, storm::logic::MultiObjectiveFormula, storm::logic::OperatorFormula, storm::logic::QuantileFormula, and storm::logic::UnaryPathFormula.

Definition at line 214 of file Formula.cpp.

info()

FormulaInformation storm::logic::Formula::info

(

bool

recurseIntoOperators = true

)

const

Definition at line 223 of file Formula.cpp.

isAtomicExpressionFormula()

bool storm::logic::Formula::isAtomicExpressionFormula ( ) const

virtual

Reimplemented in storm::logic::AtomicExpressionFormula.

Definition at line 78 of file Formula.cpp.

isAtomicLabelFormula()

bool storm::logic::Formula::isAtomicLabelFormula ( ) const

virtual

Reimplemented in storm::logic::AtomicLabelFormula.

Definition at line 82 of file Formula.cpp.

isBinaryBooleanPathFormula()

bool storm::logic::Formula::isBinaryBooleanPathFormula ( ) const

virtual

Reimplemented in storm::logic::BinaryBooleanPathFormula.

Definition at line 58 of file Formula.cpp.

isBinaryBooleanStateFormula()

bool storm::logic::Formula::isBinaryBooleanStateFormula ( ) const

virtual

Reimplemented in storm::logic::BinaryBooleanStateFormula.

Definition at line 50 of file Formula.cpp.

isBinaryPathFormula()

bool storm::logic::Formula::isBinaryPathFormula ( ) const

virtual

Reimplemented in storm::logic::BinaryPathFormula.

Definition at line 118 of file Formula.cpp.

isBinaryStateFormula()

bool storm::logic::Formula::isBinaryStateFormula ( ) const

virtual

Reimplemented in storm::logic::BinaryStateFormula.

Definition at line 42 of file Formula.cpp.

isBooleanLiteralFormula()

bool storm::logic::Formula::isBooleanLiteralFormula ( ) const

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 66 of file Formula.cpp.

isBoundedUntilFormula()

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

virtual

Reimplemented in storm::logic::BoundedUntilFormula.

Definition at line 90 of file Formula.cpp.

isConditionalProbabilityFormula()

bool storm::logic::Formula::isConditionalProbabilityFormula ( ) const

virtual

Reimplemented in storm::logic::ConditionalFormula.

Definition at line 126 of file Formula.cpp.

isConditionalRewardFormula()

bool storm::logic::Formula::isConditionalRewardFormula ( ) const

virtual

Reimplemented in storm::logic::ConditionalFormula.

Definition at line 130 of file Formula.cpp.

isCumulativeRewardFormula()

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

virtual

Reimplemented in storm::logic::CumulativeRewardFormula, and storm::logic::DiscountedCumulativeRewardFormula.

Definition at line 158 of file Formula.cpp.

isDiscountedCumulativeRewardFormula()

bool storm::logic::Formula::isDiscountedCumulativeRewardFormula ( ) const

virtual

Reimplemented in storm::logic::DiscountedCumulativeRewardFormula.

Definition at line 162 of file Formula.cpp.

isDiscountedTotalRewardFormula()

bool storm::logic::Formula::isDiscountedTotalRewardFormula ( ) const

virtual

Reimplemented in storm::logic::DiscountedTotalRewardFormula.

Definition at line 182 of file Formula.cpp.

isEventuallyFormula()

bool storm::logic::Formula::isEventuallyFormula ( ) const

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 102 of file Formula.cpp.

isFalseFormula()

bool storm::logic::Formula::isFalseFormula ( ) const

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 74 of file Formula.cpp.

isGameFormula()

bool storm::logic::Formula::isGameFormula ( ) const

virtual

Reimplemented in storm::logic::GameFormula.

Definition at line 190 of file Formula.cpp.

isGloballyFormula()

bool storm::logic::Formula::isGloballyFormula ( ) const

virtual

Reimplemented in storm::logic::GloballyFormula.

Definition at line 110 of file Formula.cpp.

isHOAPathFormula()

bool storm::logic::Formula::isHOAPathFormula ( ) const

virtual

Reimplemented in storm::logic::HOAPathFormula.

Definition at line 114 of file Formula.cpp.

isInFragment()

bool storm::logic::Formula::isInFragment

(

FragmentSpecification const &

fragment

)

const

Definition at line 218 of file Formula.cpp.

isInitialFormula()

bool storm::logic::Formula::isInitialFormula

(

)

const

Definition at line 231 of file Formula.cpp.

isInstantaneousRewardFormula()

bool storm::logic::Formula::isInstantaneousRewardFormula ( ) const

virtual

Reimplemented in storm::logic::InstantaneousRewardFormula.

Definition at line 166 of file Formula.cpp.

isLongRunAverageOperatorFormula()

bool storm::logic::Formula::isLongRunAverageOperatorFormula ( ) const

virtual

Reimplemented in storm::logic::LongRunAverageOperatorFormula.

Definition at line 150 of file Formula.cpp.

isLongRunAverageRewardFormula()

bool storm::logic::Formula::isLongRunAverageRewardFormula ( ) const

virtual

Reimplemented in storm::logic::LongRunAverageRewardFormula.

Definition at line 174 of file Formula.cpp.

isMultiObjectiveFormula()

bool storm::logic::Formula::isMultiObjectiveFormula ( ) const

virtual

Reimplemented in storm::logic::MultiObjectiveFormula.

Definition at line 34 of file Formula.cpp.

isNextFormula()

bool storm::logic::Formula::isNextFormula ( ) const

virtual

Reimplemented in storm::logic::NextFormula.

Definition at line 146 of file Formula.cpp.

isOperatorFormula()

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

virtual

Reimplemented in storm::logic::OperatorFormula.

Definition at line 202 of file Formula.cpp.

isPathFormula()

bool storm::logic::Formula::isPathFormula ( ) const

virtual

Reimplemented in storm::logic::PathFormula.

Definition at line 26 of file Formula.cpp.

isProbabilityOperatorFormula()

bool storm::logic::Formula::isProbabilityOperatorFormula ( ) const

virtual

Reimplemented in storm::logic::ProbabilityOperatorFormula.

Definition at line 194 of file Formula.cpp.

isProbabilityPathFormula()

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

virtual

Reimplemented in storm::logic::BinaryBooleanPathFormula, storm::logic::BoundedUntilFormula, storm::logic::EventuallyFormula, storm::logic::GloballyFormula, storm::logic::HOAPathFormula, storm::logic::NextFormula, storm::logic::ReleaseFormula, storm::logic::StateFormula, storm::logic::UnaryBooleanPathFormula, storm::logic::UntilFormula, and storm::logic::WeakUntilFormula.

Definition at line 134 of file Formula.cpp.

isQuantileFormula()

bool storm::logic::Formula::isQuantileFormula ( ) const

virtual

Reimplemented in storm::logic::QuantileFormula.

Definition at line 38 of file Formula.cpp.

isReachabilityProbabilityFormula()

bool storm::logic::Formula::isReachabilityProbabilityFormula ( ) const

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 106 of file Formula.cpp.

isReachabilityRewardFormula()

bool storm::logic::Formula::isReachabilityRewardFormula ( ) const

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 170 of file Formula.cpp.

isReachabilityTimeFormula()

bool storm::logic::Formula::isReachabilityTimeFormula ( ) const

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 186 of file Formula.cpp.

isReleaseFormula()

bool storm::logic::Formula::isReleaseFormula ( ) const

virtual

Reimplemented in storm::logic::ReleaseFormula.

Definition at line 98 of file Formula.cpp.

isRewardOperatorFormula()

bool storm::logic::Formula::isRewardOperatorFormula ( ) const

virtual

Reimplemented in storm::logic::RewardOperatorFormula.

Definition at line 198 of file Formula.cpp.

isRewardPathFormula()

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

virtual

Reimplemented in storm::logic::CumulativeRewardFormula, storm::logic::EventuallyFormula, storm::logic::InstantaneousRewardFormula, storm::logic::LongRunAverageRewardFormula, and storm::logic::TotalRewardFormula.

Definition at line 138 of file Formula.cpp.

isStateFormula()

bool storm::logic::Formula::isStateFormula ( ) const

virtual

Reimplemented in storm::logic::StateFormula.

Definition at line 30 of file Formula.cpp.

isTimeOperatorFormula()

bool storm::logic::Formula::isTimeOperatorFormula ( ) const

virtual

Reimplemented in storm::logic::TimeOperatorFormula.

Definition at line 154 of file Formula.cpp.

isTimePathFormula()

bool storm::logic::Formula::isTimePathFormula ( ) const

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 142 of file Formula.cpp.

isTotalRewardFormula()

bool storm::logic::Formula::isTotalRewardFormula ( ) const

virtual

Reimplemented in storm::logic::DiscountedTotalRewardFormula, and storm::logic::TotalRewardFormula.

Definition at line 178 of file Formula.cpp.

isTrueFormula()

bool storm::logic::Formula::isTrueFormula ( ) const

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 70 of file Formula.cpp.

isUnaryBooleanPathFormula()

bool storm::logic::Formula::isUnaryBooleanPathFormula ( ) const

virtual

Reimplemented in storm::logic::UnaryBooleanPathFormula.

Definition at line 62 of file Formula.cpp.

isUnaryBooleanStateFormula()

bool storm::logic::Formula::isUnaryBooleanStateFormula ( ) const

virtual

Reimplemented in storm::logic::UnaryBooleanStateFormula.

Definition at line 54 of file Formula.cpp.

isUnaryFormula()

bool storm::logic::Formula::isUnaryFormula

(

)

const

Definition at line 206 of file Formula.cpp.

isUnaryPathFormula()

bool storm::logic::Formula::isUnaryPathFormula ( ) const

virtual

Reimplemented in storm::logic::UnaryPathFormula.

Definition at line 122 of file Formula.cpp.

isUnaryStateFormula()

bool storm::logic::Formula::isUnaryStateFormula ( ) const

virtual

Reimplemented in storm::logic::UnaryStateFormula.

Definition at line 46 of file Formula.cpp.

isUntilFormula()

bool storm::logic::Formula::isUntilFormula ( ) const

virtual

Reimplemented in storm::logic::UntilFormula.

Definition at line 86 of file Formula.cpp.

isWeakUntilFormula()

bool storm::logic::Formula::isWeakUntilFormula ( ) const

virtual

Reimplemented in storm::logic::WeakUntilFormula.

Definition at line 94 of file Formula.cpp.

substitute() [1/4]

std::shared_ptr< Formula > storm::logic::Formula::substitute

(

std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &

expressionSubstitution

)

const

Definition at line 564 of file Formula.cpp.

substitute() [2/4]

std::shared_ptr< Formula > storm::logic::Formula::substitute

(

std::map< std::string, std::string > const &

labelSubstitution

)

const

Definition at line 575 of file Formula.cpp.

substitute() [3/4]

std::shared_ptr< Formula > storm::logic::Formula::substitute

(

std::map< std::string, storm::expressions::Expression > const &

labelSubstitution

)

const

Definition at line 570 of file Formula.cpp.

substitute() [4/4]

std::shared_ptr< Formula > storm::logic::Formula::substitute

(

std::map< storm::expressions::Variable, storm::expressions::Expression > const &

substitution

)

const

Definition at line 559 of file Formula.cpp.

substituteRewardModelNames()

std::shared_ptr< Formula > storm::logic::Formula::substituteRewardModelNames

(

std::map< std::string, std::string > const &

rewardModelNameSubstitution

)

const

Definition at line 580 of file Formula.cpp.

substituteTranscendentalNumbers()

std::shared_ptr< Formula > storm::logic::Formula::substituteTranscendentalNumbers

(

)

const

Definition at line 585 of file Formula.cpp.

toExpression()

storm::expressions::Expression storm::logic::Formula::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.

The formula may contain atomic labels, but then the given mapping must provide a corresponding expression. Other than that, only atomic expression formulas and boolean connectives may appear in the formula.

Parameters

manager	The manager responsible for the expressions in the formula and the resulting expression.
A	mapping from labels to the expressions that define them.

Returns

An equivalent expression.

Definition at line 591 of file Formula.cpp.

toPrefixString()

std::string storm::logic::Formula::toPrefixString

(

)

const

Definition at line 627 of file Formula.cpp.

toString()

std::string storm::logic::Formula::toString

(

)

const

Definition at line 617 of file Formula.cpp.

traverse()

void storm::logic::Formula::traverse

(

std::function< bool(Formula const &)> const &

callback

)

const

Invokes the given callback on this formula and on its subformulas in pre-order, i.e., a formula is visited before its subformulas.

Parameters

callback

the subformulas of a formula are only visited if the callback returns true for that formula.

Definition at line 21 of file Formula.cpp.

writeToStream()

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

pure virtual

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

Implemented in storm::logic::AtomicExpressionFormula, storm::logic::AtomicLabelFormula, storm::logic::BinaryBooleanPathFormula, storm::logic::BinaryBooleanStateFormula, storm::logic::BooleanLiteralFormula, storm::logic::BoundedUntilFormula, storm::logic::ConditionalFormula, storm::logic::CumulativeRewardFormula, storm::logic::DiscountedCumulativeRewardFormula, storm::logic::DiscountedTotalRewardFormula, storm::logic::EventuallyFormula, storm::logic::GameFormula, storm::logic::GloballyFormula, storm::logic::HOAPathFormula, storm::logic::InstantaneousRewardFormula, storm::logic::LongRunAverageOperatorFormula, storm::logic::LongRunAverageRewardFormula, storm::logic::MultiObjectiveFormula, storm::logic::NextFormula, storm::logic::OperatorFormula, storm::logic::ProbabilityOperatorFormula, storm::logic::QuantileFormula, storm::logic::ReleaseFormula, storm::logic::RewardOperatorFormula, storm::logic::TimeOperatorFormula, storm::logic::TotalRewardFormula, storm::logic::UnaryBooleanPathFormula, storm::logic::UnaryBooleanStateFormula, storm::logic::UntilFormula, and storm::logic::WeakUntilFormula.

Friends And Related Symbol Documentation

operator<<

std::ostream & operator<< ( std::ostream & out, Formula const & formula )

friend

Definition at line 623 of file Formula.cpp.

---

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

• src/storm/logic/Formula.h
• src/storm/logic/Formula.cpp