Storm
A Modern Probabilistic Model Checker
|
#include <Variable.h>
Public Member Functions | |
Variable (Variable const &otherVariable)=default | |
Variable & | operator= (Variable const &otherVariable)=default |
Variable (Variable &&otherVariable)=default | |
Variable & | operator= (Variable &&otherVariable)=default |
virtual | ~Variable ()=default |
std::string const & | getName () const |
Retrieves the name of the variable. | |
bool | hasInitialValue () const |
Retrieves whether the variable has an initial value. | |
storm::expressions::Expression const & | getInitialValueExpression () const |
Retrieves the expression defining the initial value of the variable. | |
void | setInitialValueExpression (storm::expressions::Expression const &initialValueExpression) |
Sets the expression defining the initial value of the variable. | |
storm::expressions::Variable const & | getExpressionVariable () const |
Retrieves the expression variable associated with this variable. | |
storm::expressions::Expression | getExpression () const |
Retrieves the expression associated with this variable. | |
bool | isObservable () const |
Retrieves whether the variable is observable. | |
virtual void | createMissingInitialValue ()=0 |
Equips the variable with an initial value based on its type if not initial value is present. | |
![]() | |
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. | |
Protected Member Functions | |
Variable ()=default | |
Variable (storm::expressions::Variable const &variable, storm::expressions::Expression const &initialValueExpression, bool observable=false, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates a variable with the given initial value. | |
Variable (storm::expressions::ExpressionManager &manager, Variable const &oldVariable, std::string const &newName, std::map< storm::expressions::Variable, storm::expressions::Expression > const &renaming, bool observable=false, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates a copy of the given variable and performs the provided renaming. | |
Definition at line 13 of file Variable.h.
|
default |
|
default |
|
virtualdefault |
|
protecteddefault |
|
protected |
Creates a variable with the given initial value.
variable | The associated expression variable. |
initialValueExpression | The constant expression that defines the initial value of the variable. |
observable | Whether the variable is listed as observable |
filename | The filename in which the variable is defined. |
lineNumber | The line number in which the variable is defined. |
Definition at line 8 of file Variable.cpp.
|
protected |
Creates a copy of the given variable and performs the provided renaming.
manager | The manager responsible for the variable. |
oldVariable | The variable to copy. |
newName | New name of this variable. |
renaming | A mapping from variables to the expressions with which they are to be replaced. |
observable | Whether the variable is listed as observable |
filename | The filename in which the variable is defined. |
lineNumber | The line number in which the variable is defined. |
Definition at line 14 of file Variable.cpp.
|
pure virtual |
Equips the variable with an initial value based on its type if not initial value is present.
Implemented in storm::prism::BooleanVariable, storm::prism::ClockVariable, and storm::prism::IntegerVariable.
storm::expressions::Expression storm::prism::Variable::getExpression | ( | ) | const |
Retrieves the expression associated with this variable.
Definition at line 44 of file Variable.cpp.
storm::expressions::Variable const & storm::prism::Variable::getExpressionVariable | ( | ) | const |
Retrieves the expression variable associated with this variable.
Definition at line 40 of file Variable.cpp.
storm::expressions::Expression const & storm::prism::Variable::getInitialValueExpression | ( | ) | const |
Retrieves the expression defining the initial value of the variable.
This can only be called if there is an initial value (expression).
Definition at line 32 of file Variable.cpp.
std::string const & storm::prism::Variable::getName | ( | ) | const |
Retrieves the name of the variable.
Definition at line 24 of file Variable.cpp.
bool storm::prism::Variable::hasInitialValue | ( | ) | const |
Retrieves whether the variable has an initial value.
Definition at line 28 of file Variable.cpp.
bool storm::prism::Variable::isObservable | ( | ) | const |
Retrieves whether the variable is observable.
Definition at line 48 of file Variable.cpp.
void storm::prism::Variable::setInitialValueExpression | ( | storm::expressions::Expression const & | initialValueExpression | ) |
Sets the expression defining the initial value of the variable.
initialValueExpression | The expression defining the initial value of the variable. |
Definition at line 36 of file Variable.cpp.