Storm
A Modern Probabilistic Model Checker
|
#include <Formula.h>
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 | |
Formula & | operator= (Formula const &other)=default |
Formula (Formula &&other)=default | |
Formula & | operator= (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 |
![]() | |
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 | |
LocatedInformation & | operator= (LocatedInformation const &other)=default |
LocatedInformation (LocatedInformation &&other)=default | |
LocatedInformation & | operator= (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) |
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.
variable | The placeholder variable that is used in expressions to represent this formula. |
expression | The expression associated with this formula. |
filename | The filename in which the transition reward is defined. |
lineNumber | The line number in which the transition reward is defined. |
Definition at line 5 of file Formula.cpp.
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.
name | the name of the formula. |
expression | The expression associated with this formula. |
filename | The filename in which the transition reward is defined. |
lineNumber | The line number in which the transition reward is defined. |
Definition at line 11 of file Formula.cpp.
storm::prism::Formula::Formula | ( | std::string const & | name, |
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 |
||
) |
Creates a formula with the given name.
name | the name of the formula. |
filename | The filename in which the transition reward is defined. |
lineNumber | The line number in which the transition reward is defined. |
Definition at line 16 of file Formula.cpp.
|
default |
|
default |
|
default |
storm::expressions::Expression const & storm::prism::Formula::getExpression | ( | ) | const |
Retrieves the expression that is associated with this formula.
Definition at line 32 of file Formula.cpp.
storm::expressions::Variable const & storm::prism::Formula::getExpressionVariable | ( | ) | const |
Retrieves the placeholder variable that is used in expressions to represent this formula.
Definition at line 28 of file Formula.cpp.
std::string const & storm::prism::Formula::getName | ( | ) | const |
Retrieves the name that is associated with this formula.
Definition at line 20 of file Formula.cpp.
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.
Definition at line 36 of file Formula.cpp.
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.
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).
substitution | The substitution to perform. |
Definition at line 42 of file Formula.cpp.
Formula storm::prism::Formula::substituteNonStandardPredicates | ( | ) | const |
Definition at line 51 of file Formula.cpp.
|
friend |
Definition at line 60 of file Formula.cpp.