Storm 1.11.1.1
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 containsDiscountFormula () 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)
 
FormulaInformation & setContainsDiscountFormula (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 25 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 41 of file FormulaInformation.cpp.

◆ containsCumulativeRewardFormula()

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

Definition at line 29 of file FormulaInformation.cpp.

◆ containsDiscountFormula()

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

Definition at line 45 of file FormulaInformation.cpp.

◆ containsLongRunFormula()

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

Definition at line 37 of file FormulaInformation.cpp.

◆ containsNextFormula()

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

Definition at line 21 of file FormulaInformation.cpp.

◆ containsRewardBoundedFormula()

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

Definition at line 33 of file FormulaInformation.cpp.

◆ containsRewardOperator()

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

Definition at line 17 of file FormulaInformation.cpp.

◆ join()

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

Definition at line 49 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 72 of file FormulaInformation.cpp.

◆ setContainsComplexPathFormula()

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

Definition at line 92 of file FormulaInformation.cpp.

◆ setContainsCumulativeRewardFormula()

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

Definition at line 77 of file FormulaInformation.cpp.

◆ setContainsDiscountFormula()

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

Definition at line 97 of file FormulaInformation.cpp.

◆ setContainsLongRunFormula()

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

Definition at line 87 of file FormulaInformation.cpp.

◆ setContainsNextFormula()

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

Definition at line 67 of file FormulaInformation.cpp.

◆ setContainsRewardBoundedFormula()

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

Definition at line 82 of file FormulaInformation.cpp.

◆ setContainsRewardOperator()

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

Definition at line 62 of file FormulaInformation.cpp.

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