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	isHOAPathFormula () const
virtual bool	isCumulativeRewardFormula () const
virtual bool	isInstantaneousRewardFormula () const
virtual bool	isReachabilityRewardFormula () const
virtual bool	isLongRunAverageRewardFormula () const
virtual bool	isTotalRewardFormula () const
virtual bool	isReachabilityTimeFormula () const
virtual bool	isGameFormula () const
virtual bool	isBinaryPathFormula () const
virtual bool	isBinaryStateFormula () const
virtual bool	isUnaryPathFormula () const
virtual bool	isUnaryStateFormula () const
bool	isUnaryFormula () const
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
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
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 30 of file Formula.h.

Constructor & Destructor Documentation

~Formula()

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

inlinevirtual

Definition at line 33 of file Formula.h.

Member Function Documentation

accept() [1/2]

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

(

FormulaVisitor const &

visitor

)

const

Definition at line 16 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::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::RewardOperatorFormula, storm::logic::TimeOperatorFormula, storm::logic::TotalRewardFormula, storm::logic::UnaryBooleanPathFormula, storm::logic::UnaryBooleanStateFormula, and storm::logic::UntilFormula.

asAtomicExpressionFormula() [1/2]

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

(

)

Definition at line 293 of file Formula.cpp.

asAtomicExpressionFormula() [2/2]

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

(

)

const

Definition at line 297 of file Formula.cpp.

asAtomicLabelFormula() [1/2]

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

(

)

Definition at line 301 of file Formula.cpp.

asAtomicLabelFormula() [2/2]

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

(

)

const

Definition at line 305 of file Formula.cpp.

asBinaryBooleanStateFormula() [1/2]

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

(

)

Definition at line 269 of file Formula.cpp.

asBinaryBooleanStateFormula() [2/2]

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

(

)

const

Definition at line 273 of file Formula.cpp.

asBinaryPathFormula() [1/2]

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

(

)

Definition at line 381 of file Formula.cpp.

asBinaryPathFormula() [2/2]

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

(

)

const

Definition at line 385 of file Formula.cpp.

asBinaryStateFormula() [1/2]

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

(

)

Definition at line 245 of file Formula.cpp.

asBinaryStateFormula() [2/2]

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

(

)

const

Definition at line 249 of file Formula.cpp.

asBooleanLiteralFormula() [1/2]

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

(

)

Definition at line 285 of file Formula.cpp.

asBooleanLiteralFormula() [2/2]

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

(

)

const

Definition at line 289 of file Formula.cpp.

asBoundedUntilFormula() [1/2]

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

(

)

Definition at line 325 of file Formula.cpp.

asBoundedUntilFormula() [2/2]

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

(

)

const

Definition at line 329 of file Formula.cpp.

asConditionalFormula() [1/2]

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

(

)

Definition at line 261 of file Formula.cpp.

asConditionalFormula() [2/2]

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

(

)

const

Definition at line 265 of file Formula.cpp.

asCumulativeRewardFormula() [1/2]

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

(

)

Definition at line 421 of file Formula.cpp.

asCumulativeRewardFormula() [2/2]

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

(

)

const

Definition at line 425 of file Formula.cpp.

asEventuallyFormula() [1/2]

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

(

)

Definition at line 333 of file Formula.cpp.

asEventuallyFormula() [2/2]

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

(

)

const

Definition at line 337 of file Formula.cpp.

asGameFormula() [1/2]

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

(

)

Definition at line 365 of file Formula.cpp.

asGameFormula() [2/2]

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

(

)

const

Definition at line 369 of file Formula.cpp.

asGloballyFormula() [1/2]

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

(

)

Definition at line 373 of file Formula.cpp.

asGloballyFormula() [2/2]

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

(

)

const

Definition at line 377 of file Formula.cpp.

asHOAPathFormula() [1/2]

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

(

)

Definition at line 309 of file Formula.cpp.

asHOAPathFormula() [2/2]

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

(

)

const

Definition at line 313 of file Formula.cpp.

asInstantaneousRewardFormula() [1/2]

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

(

)

Definition at line 437 of file Formula.cpp.

asInstantaneousRewardFormula() [2/2]

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

(

)

const

Definition at line 441 of file Formula.cpp.

asLongRunAverageOperatorFormula() [1/2]

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

(

)

Definition at line 405 of file Formula.cpp.

asLongRunAverageOperatorFormula() [2/2]

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

(

)

const

Definition at line 409 of file Formula.cpp.

asLongRunAverageRewardFormula() [1/2]

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

(

)

Definition at line 445 of file Formula.cpp.

asLongRunAverageRewardFormula() [2/2]

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

(

)

const

Definition at line 449 of file Formula.cpp.

asMultiObjectiveFormula() [1/2]

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

(

)

Definition at line 229 of file Formula.cpp.

asMultiObjectiveFormula() [2/2]

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

(

)

const

Definition at line 233 of file Formula.cpp.

asNextFormula() [1/2]

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

(

)

Definition at line 397 of file Formula.cpp.

asNextFormula() [2/2]

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

(

)

const

Definition at line 401 of file Formula.cpp.

asOperatorFormula() [1/2]

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

(

)

Definition at line 469 of file Formula.cpp.

asOperatorFormula() [2/2]

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

(

)

const

Definition at line 473 of file Formula.cpp.

asPathFormula() [1/2]

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

(

)

Definition at line 213 of file Formula.cpp.

asPathFormula() [2/2]

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

(

)

const

Definition at line 217 of file Formula.cpp.

asProbabilityOperatorFormula() [1/2]

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

(

)

Definition at line 453 of file Formula.cpp.

asProbabilityOperatorFormula() [2/2]

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

(

)

const

Definition at line 457 of file Formula.cpp.

asQuantileFormula() [1/2]

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

(

)

Definition at line 237 of file Formula.cpp.

asQuantileFormula() [2/2]

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

(

)

const

Definition at line 241 of file Formula.cpp.

asReachabilityProbabilityFormula() [1/2]

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

(

)

Definition at line 349 of file Formula.cpp.

asReachabilityProbabilityFormula() [2/2]

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

(

)

const

Definition at line 353 of file Formula.cpp.

asReachabilityRewardFormula() [1/2]

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

(

)

Definition at line 341 of file Formula.cpp.

asReachabilityRewardFormula() [2/2]

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

(

)

const

Definition at line 345 of file Formula.cpp.

asReachabilityTimeFormula() [1/2]

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

(

)

Definition at line 357 of file Formula.cpp.

asReachabilityTimeFormula() [2/2]

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

(

)

const

Definition at line 361 of file Formula.cpp.

asRewardOperatorFormula() [1/2]

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

(

)

Definition at line 461 of file Formula.cpp.

asRewardOperatorFormula() [2/2]

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

(

)

const

Definition at line 465 of file Formula.cpp.

asSharedPointer() [1/2]

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

(

)

Definition at line 548 of file Formula.cpp.

asSharedPointer() [2/2]

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

(

)

const

Definition at line 552 of file Formula.cpp.

asStateFormula() [1/2]

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

(

)

Definition at line 221 of file Formula.cpp.

asStateFormula() [2/2]

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

(

)

const

Definition at line 225 of file Formula.cpp.

asTimeOperatorFormula() [1/2]

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

(

)

Definition at line 413 of file Formula.cpp.

asTimeOperatorFormula() [2/2]

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

(

)

const

Definition at line 417 of file Formula.cpp.

asTotalRewardFormula() [1/2]

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

(

)

Definition at line 429 of file Formula.cpp.

asTotalRewardFormula() [2/2]

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

(

)

const

Definition at line 433 of file Formula.cpp.

asUnaryBooleanStateFormula() [1/2]

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

(

)

Definition at line 277 of file Formula.cpp.

asUnaryBooleanStateFormula() [2/2]

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

(

)

const

Definition at line 281 of file Formula.cpp.

asUnaryPathFormula() [1/2]

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

(

)

Definition at line 389 of file Formula.cpp.

asUnaryPathFormula() [2/2]

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

(

)

const

Definition at line 393 of file Formula.cpp.

asUnaryStateFormula() [1/2]

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

(

)

Definition at line 253 of file Formula.cpp.

asUnaryStateFormula() [2/2]

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

(

)

const

Definition at line 257 of file Formula.cpp.

asUntilFormula() [1/2]

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

(

)

Definition at line 317 of file Formula.cpp.

asUntilFormula() [2/2]

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

(

)

const

Definition at line 321 of file Formula.cpp.

clone()

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

(

)

const

Definition at line 501 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 556 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 560 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 564 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::InstantaneousRewardFormula, storm::logic::OperatorFormula, storm::logic::UnaryPathFormula, and storm::logic::UnaryStateFormula.

Definition at line 568 of file Formula.cpp.

getAtomicExpressionFormulas()

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

(

)

const

Definition at line 477 of file Formula.cpp.

getAtomicLabelFormulas()

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

(

)

const

Definition at line 483 of file Formula.cpp.

getReferencedRewardModels()

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

(

)

const

Definition at line 495 of file Formula.cpp.

getTrueFormula()

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

static

Definition at line 205 of file Formula.cpp.

getUsedVariables()

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

(

)

const

Definition at line 489 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 188 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 192 of file Formula.cpp.

info()

FormulaInformation storm::logic::Formula::info

(

bool

recurseIntoOperators = true

)

const

Definition at line 201 of file Formula.cpp.

isAtomicExpressionFormula()

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

virtual

Reimplemented in storm::logic::AtomicExpressionFormula.

Definition at line 72 of file Formula.cpp.

isAtomicLabelFormula()

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

virtual

Reimplemented in storm::logic::AtomicLabelFormula.

Definition at line 76 of file Formula.cpp.

isBinaryBooleanPathFormula()

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

virtual

Reimplemented in storm::logic::BinaryBooleanPathFormula.

Definition at line 52 of file Formula.cpp.

isBinaryBooleanStateFormula()

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

virtual

Reimplemented in storm::logic::BinaryBooleanStateFormula.

Definition at line 44 of file Formula.cpp.

isBinaryPathFormula()

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

virtual

Reimplemented in storm::logic::BinaryPathFormula.

Definition at line 104 of file Formula.cpp.

isBinaryStateFormula()

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

virtual

Reimplemented in storm::logic::BinaryStateFormula.

Definition at line 36 of file Formula.cpp.

isBooleanLiteralFormula()

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

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 60 of file Formula.cpp.

isBoundedUntilFormula()

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

virtual

Reimplemented in storm::logic::BoundedUntilFormula.

Definition at line 84 of file Formula.cpp.

isConditionalProbabilityFormula()

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

virtual

Reimplemented in storm::logic::ConditionalFormula.

Definition at line 112 of file Formula.cpp.

isConditionalRewardFormula()

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

virtual

Reimplemented in storm::logic::ConditionalFormula.

Definition at line 116 of file Formula.cpp.

isCumulativeRewardFormula()

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

virtual

Reimplemented in storm::logic::CumulativeRewardFormula.

Definition at line 144 of file Formula.cpp.

isEventuallyFormula()

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

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 88 of file Formula.cpp.

isFalseFormula()

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

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 68 of file Formula.cpp.

isGameFormula()

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

virtual

Reimplemented in storm::logic::GameFormula.

Definition at line 168 of file Formula.cpp.

isGloballyFormula()

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

virtual

Reimplemented in storm::logic::GloballyFormula.

Definition at line 96 of file Formula.cpp.

isHOAPathFormula()

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

virtual

Reimplemented in storm::logic::HOAPathFormula.

Definition at line 100 of file Formula.cpp.

isInFragment()

bool storm::logic::Formula::isInFragment

(

FragmentSpecification const &

fragment

)

const

Definition at line 196 of file Formula.cpp.

isInitialFormula()

bool storm::logic::Formula::isInitialFormula

(

)

const

Definition at line 209 of file Formula.cpp.

isInstantaneousRewardFormula()

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

virtual

Reimplemented in storm::logic::InstantaneousRewardFormula.

Definition at line 148 of file Formula.cpp.

isLongRunAverageOperatorFormula()

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

virtual

Reimplemented in storm::logic::LongRunAverageOperatorFormula.

Definition at line 136 of file Formula.cpp.

isLongRunAverageRewardFormula()

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

virtual

Reimplemented in storm::logic::LongRunAverageRewardFormula.

Definition at line 156 of file Formula.cpp.

isMultiObjectiveFormula()

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

virtual

Reimplemented in storm::logic::MultiObjectiveFormula.

Definition at line 28 of file Formula.cpp.

isNextFormula()

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

virtual

Reimplemented in storm::logic::NextFormula.

Definition at line 132 of file Formula.cpp.

isOperatorFormula()

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

virtual

Reimplemented in storm::logic::OperatorFormula.

Definition at line 180 of file Formula.cpp.

isPathFormula()

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

virtual

Reimplemented in storm::logic::PathFormula.

Definition at line 20 of file Formula.cpp.

isProbabilityOperatorFormula()

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

virtual

Reimplemented in storm::logic::ProbabilityOperatorFormula.

Definition at line 172 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::StateFormula, storm::logic::UnaryBooleanPathFormula, and storm::logic::UntilFormula.

Definition at line 120 of file Formula.cpp.

isQuantileFormula()

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

virtual

Reimplemented in storm::logic::QuantileFormula.

Definition at line 32 of file Formula.cpp.

isReachabilityProbabilityFormula()

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

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 92 of file Formula.cpp.

isReachabilityRewardFormula()

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

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 152 of file Formula.cpp.

isReachabilityTimeFormula()

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

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 164 of file Formula.cpp.

isRewardOperatorFormula()

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

virtual

Reimplemented in storm::logic::RewardOperatorFormula.

Definition at line 176 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 124 of file Formula.cpp.

isStateFormula()

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

virtual

Reimplemented in storm::logic::StateFormula.

Definition at line 24 of file Formula.cpp.

isTimeOperatorFormula()

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

virtual

Reimplemented in storm::logic::TimeOperatorFormula.

Definition at line 140 of file Formula.cpp.

isTimePathFormula()

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

virtual

Reimplemented in storm::logic::EventuallyFormula.

Definition at line 128 of file Formula.cpp.

isTotalRewardFormula()

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

virtual

Reimplemented in storm::logic::TotalRewardFormula.

Definition at line 160 of file Formula.cpp.

isTrueFormula()

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

virtual

Reimplemented in storm::logic::BooleanLiteralFormula.

Definition at line 64 of file Formula.cpp.

isUnaryBooleanPathFormula()

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

virtual

Reimplemented in storm::logic::UnaryBooleanPathFormula.

Definition at line 56 of file Formula.cpp.

isUnaryBooleanStateFormula()

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

virtual

Reimplemented in storm::logic::UnaryBooleanStateFormula.

Definition at line 48 of file Formula.cpp.

isUnaryFormula()

bool storm::logic::Formula::isUnaryFormula

(

)

const

Definition at line 184 of file Formula.cpp.

isUnaryPathFormula()

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

virtual

Reimplemented in storm::logic::UnaryPathFormula.

Definition at line 108 of file Formula.cpp.

isUnaryStateFormula()

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

virtual

Reimplemented in storm::logic::UnaryStateFormula.

Definition at line 40 of file Formula.cpp.

isUntilFormula()

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

virtual

Reimplemented in storm::logic::UntilFormula.

Definition at line 80 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 511 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 522 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 517 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 506 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 527 of file Formula.cpp.

substituteTranscendentalNumbers()

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

(

)

const

Definition at line 532 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 538 of file Formula.cpp.

toPrefixString()

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

(

)

const

Definition at line 582 of file Formula.cpp.

toString()

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

(

)

const

Definition at line 572 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::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::RewardOperatorFormula, storm::logic::TimeOperatorFormula, storm::logic::TotalRewardFormula, storm::logic::UnaryBooleanPathFormula, storm::logic::UnaryBooleanStateFormula, and storm::logic::UntilFormula.

Friends And Related Symbol Documentation

operator<<

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

friend

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