Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | List of all members
storm::logic::FormulaInformation Class Reference

#include <FormulaInformation.h>

Public Member Functions

 FormulaInformation ()
 
 FormulaInformation (FormulaInformation const &other)=default
 
 FormulaInformation (FormulaInformation &&other)=default
 
FormulaInformation & operator= (FormulaInformation const &other)=default
 
FormulaInformation & operator= (FormulaInformation &&other)=default
 
bool containsRewardOperator () const
 
bool containsNextFormula () const
 
bool containsBoundedUntilFormula () const
 
bool containsCumulativeRewardFormula () const
 
bool containsRewardBoundedFormula () const
 
bool containsLongRunFormula () const
 
bool containsComplexPathFormula () const
 
FormulaInformation join (FormulaInformation const &other)
 
FormulaInformation & setContainsRewardOperator (bool newValue=true)
 
FormulaInformation & setContainsNextFormula (bool newValue=true)
 
FormulaInformation & setContainsBoundedUntilFormula (bool newValue=true)
 
FormulaInformation & setContainsCumulativeRewardFormula (bool newValue=true)
 
FormulaInformation & setContainsRewardBoundedFormula (bool newValue=true)
 
FormulaInformation & setContainsLongRunFormula (bool newValue=true)
 
FormulaInformation & setContainsComplexPathFormula (bool newValue=true)
 

Detailed Description

Definition at line 7 of file FormulaInformation.h.

Constructor & Destructor Documentation

◆ FormulaInformation() [1/3]

storm::logic::FormulaInformation::FormulaInformation ( )

Definition at line 5 of file FormulaInformation.cpp.

◆ FormulaInformation() [2/3]

storm::logic::FormulaInformation::FormulaInformation ( FormulaInformation const &  other)
default

◆ FormulaInformation() [3/3]

storm::logic::FormulaInformation::FormulaInformation ( FormulaInformation &&  other)
default

Member Function Documentation

◆ containsBoundedUntilFormula()

bool storm::logic::FormulaInformation::containsBoundedUntilFormula ( ) const

Definition at line 24 of file FormulaInformation.cpp.

◆ containsComplexPathFormula()

bool storm::logic::FormulaInformation::containsComplexPathFormula ( ) const
Returns
true iff the formula contains nested temporal operators and/or boolean combinations of path formulas (e.g. '"safe" & F "goal"')

Definition at line 40 of file FormulaInformation.cpp.

◆ containsCumulativeRewardFormula()

bool storm::logic::FormulaInformation::containsCumulativeRewardFormula ( ) const

Definition at line 28 of file FormulaInformation.cpp.

◆ containsLongRunFormula()

bool storm::logic::FormulaInformation::containsLongRunFormula ( ) const

Definition at line 36 of file FormulaInformation.cpp.

◆ containsNextFormula()

bool storm::logic::FormulaInformation::containsNextFormula ( ) const

Definition at line 20 of file FormulaInformation.cpp.

◆ containsRewardBoundedFormula()

bool storm::logic::FormulaInformation::containsRewardBoundedFormula ( ) const

Definition at line 32 of file FormulaInformation.cpp.

◆ containsRewardOperator()

bool storm::logic::FormulaInformation::containsRewardOperator ( ) const

Definition at line 16 of file FormulaInformation.cpp.

◆ join()

FormulaInformation storm::logic::FormulaInformation::join ( FormulaInformation const &  other)

Definition at line 44 of file FormulaInformation.cpp.

◆ operator=() [1/2]

FormulaInformation & storm::logic::FormulaInformation::operator= ( FormulaInformation &&  other)
default

◆ operator=() [2/2]

FormulaInformation & storm::logic::FormulaInformation::operator= ( FormulaInformation const &  other)
default

◆ setContainsBoundedUntilFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsBoundedUntilFormula ( bool  newValue = true)

Definition at line 66 of file FormulaInformation.cpp.

◆ setContainsComplexPathFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsComplexPathFormula ( bool  newValue = true)

Definition at line 86 of file FormulaInformation.cpp.

◆ setContainsCumulativeRewardFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsCumulativeRewardFormula ( bool  newValue = true)

Definition at line 71 of file FormulaInformation.cpp.

◆ setContainsLongRunFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsLongRunFormula ( bool  newValue = true)

Definition at line 81 of file FormulaInformation.cpp.

◆ setContainsNextFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsNextFormula ( bool  newValue = true)

Definition at line 61 of file FormulaInformation.cpp.

◆ setContainsRewardBoundedFormula()

FormulaInformation & storm::logic::FormulaInformation::setContainsRewardBoundedFormula ( bool  newValue = true)

Definition at line 76 of file FormulaInformation.cpp.

◆ setContainsRewardOperator()

FormulaInformation & storm::logic::FormulaInformation::setContainsRewardOperator ( bool  newValue = true)

Definition at line 56 of file FormulaInformation.cpp.

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