Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::prism::Formula Class Reference

#include <Formula.h>

Inheritance diagram for storm::prism::Formula:
Collaboration diagram for storm::prism::Formula:

Public Member Functions

 Formula (storm::expressions::Variable const &variable, storm::expressions::Expression const &expression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a formula with the given placeholder variable and expression.
 
 Formula (std::string const &name, storm::expressions::Expression const &expression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a formula with the given name and the assigning expression.
 
 Formula (std::string const &name, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates a formula with the given name.
 
 Formula ()=default
 
 Formula (Formula const &other)=default
 
Formulaoperator= (Formula const &other)=default
 
 Formula (Formula &&other)=default
 
Formulaoperator= (Formula &&other)=default
 
std::string const & getName () const
 Retrieves the name that is associated with this formula.
 
bool hasExpressionVariable () const
 Retrieves wheter a placeholder variable is used in expressions to represent this formula.
 
storm::expressions::Variable const & getExpressionVariable () const
 Retrieves the placeholder variable that is used in expressions to represent this formula.
 
storm::expressions::Expression const & getExpression () const
 Retrieves the expression that is associated with this formula.
 
storm::expressions::Type const & getType () const
 Retrieves the return type of the formula, i.e., the return-type of the defining expression.
 
Formula substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all variables in the expression of the formula according to the given map.
 
Formula substituteNonStandardPredicates () const
 
- Public Member Functions inherited from storm::prism::LocatedInformation
 LocatedInformation (std::string const &filename, uint_fast64_t lineNumber)
 Constructs a located information with the given filename and line number.
 
 LocatedInformation ()=default
 
 LocatedInformation (LocatedInformation const &other)=default
 
LocatedInformationoperator= (LocatedInformation const &other)=default
 
 LocatedInformation (LocatedInformation &&other)=default
 
LocatedInformationoperator= (LocatedInformation &&other)=default
 
std::string const & getFilename () const
 Retrieves the name of the file in which the information was found.
 
void setFilename (std::string const &filename)
 Sets the filename of this information.
 
uint_fast64_t getLineNumber () const
 Retrieves the line number in which the information was found.
 
void setLineNumber (uint_fast64_t lineNumber)
 Sets the line number of this information.
 

Friends

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

Detailed Description

Definition at line 14 of file Formula.h.

Constructor & Destructor Documentation

◆ Formula() [1/6]

storm::prism::Formula::Formula ( storm::expressions::Variable const &  variable,
storm::expressions::Expression const &  expression,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Creates a formula with the given placeholder variable and expression.

Parameters
variableThe placeholder variable that is used in expressions to represent this formula.
expressionThe expression associated with this formula.
filenameThe filename in which the transition reward is defined.
lineNumberThe line number in which the transition reward is defined.

Definition at line 5 of file Formula.cpp.

◆ Formula() [2/6]

storm::prism::Formula::Formula ( std::string const &  name,
storm::expressions::Expression const &  expression,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Creates a formula with the given name and the assigning expression.

Parameters
namethe name of the formula.
expressionThe expression associated with this formula.
filenameThe filename in which the transition reward is defined.
lineNumberThe line number in which the transition reward is defined.

Definition at line 11 of file Formula.cpp.

◆ Formula() [3/6]

storm::prism::Formula::Formula ( std::string const &  name,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Creates a formula with the given name.

Parameters
namethe name of the formula.
filenameThe filename in which the transition reward is defined.
lineNumberThe line number in which the transition reward is defined.

Definition at line 16 of file Formula.cpp.

◆ Formula() [4/6]

storm::prism::Formula::Formula ( )
default

◆ Formula() [5/6]

storm::prism::Formula::Formula ( Formula const &  other)
default

◆ Formula() [6/6]

storm::prism::Formula::Formula ( Formula &&  other)
default

Member Function Documentation

◆ getExpression()

storm::expressions::Expression const & storm::prism::Formula::getExpression ( ) const

Retrieves the expression that is associated with this formula.

Returns
The expression that is associated with this formula.

Definition at line 32 of file Formula.cpp.

◆ getExpressionVariable()

storm::expressions::Variable const & storm::prism::Formula::getExpressionVariable ( ) const

Retrieves the placeholder variable that is used in expressions to represent this formula.

Returns
The placeholder variable that is used in expressions to represent this formula.

Definition at line 28 of file Formula.cpp.

◆ getName()

std::string const & storm::prism::Formula::getName ( ) const

Retrieves the name that is associated with this formula.

Returns
The name that is associated with this formula.

Definition at line 20 of file Formula.cpp.

◆ getType()

storm::expressions::Type const & storm::prism::Formula::getType ( ) const

Retrieves the return type of the formula, i.e., the return-type of the defining expression.

Returns
The return type of the formula.

Definition at line 36 of file Formula.cpp.

◆ hasExpressionVariable()

bool storm::prism::Formula::hasExpressionVariable ( ) const

Retrieves wheter a placeholder variable is used in expressions to represent this formula.

Definition at line 24 of file Formula.cpp.

◆ operator=() [1/2]

Formula & storm::prism::Formula::operator= ( Formula &&  other)
default

◆ operator=() [2/2]

Formula & storm::prism::Formula::operator= ( Formula const &  other)
default

◆ substitute()

Formula storm::prism::Formula::substitute ( std::map< storm::expressions::Variable, storm::expressions::Expression > const &  substitution) const

Substitutes all variables in the expression of the formula according to the given map.

Will not substitute the placeholder variable (if given).

Parameters
substitutionThe substitution to perform.
Returns
The resulting formula.

Definition at line 42 of file Formula.cpp.

◆ substituteNonStandardPredicates()

Formula storm::prism::Formula::substituteNonStandardPredicates ( ) const

Definition at line 51 of file Formula.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

Definition at line 60 of file Formula.cpp.


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