Storm
A Modern Probabilistic Model Checker
|
#include <IntegerVariable.h>
Public Member Functions | |
IntegerVariable ()=default | |
IntegerVariable (IntegerVariable const &other)=default | |
IntegerVariable & | operator= (IntegerVariable const &other)=default |
IntegerVariable (IntegerVariable &&other)=default | |
IntegerVariable & | operator= (IntegerVariable &&other)=default |
IntegerVariable (storm::expressions::Variable const &variable, storm::expressions::Expression const &lowerBoundExpression, storm::expressions::Expression const &upperBoundExpression, storm::expressions::Expression const &initialValueExpression, bool observable, std::string const &filename="", uint_fast64_t lineNumber=0) | |
Creates an integer variable with the given initial value expression. | |
bool | hasLowerBoundExpression () const |
storm::expressions::Expression const & | getLowerBoundExpression () const |
Retrieves an expression defining the lower bound for this integer variable. | |
bool | hasUpperBoundExpression () const |
storm::expressions::Expression const & | getUpperBoundExpression () const |
Retrieves an expression defining the upper bound for this integer variable. | |
storm::expressions::Expression | getRangeExpression () const |
Retrieves an expression characterizing the legal range of the variable. | |
IntegerVariable | substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const |
Substitutes all identifiers in the boolean variable according to the given map. | |
IntegerVariable | substituteNonStandardPredicates () const |
virtual void | createMissingInitialValue () override |
Equips the variable with an initial value based on its type if not initial value is present. | |
![]() | |
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. | |
![]() | |
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, IntegerVariable const &variable) |
Additional Inherited Members | |
![]() | |
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 11 of file IntegerVariable.h.
|
default |
|
default |
|
default |
storm::prism::IntegerVariable::IntegerVariable | ( | storm::expressions::Variable const & | variable, |
storm::expressions::Expression const & | lowerBoundExpression, | ||
storm::expressions::Expression const & | upperBoundExpression, | ||
storm::expressions::Expression const & | initialValueExpression, | ||
bool | observable, | ||
std::string const & | filename = "" , |
||
uint_fast64_t | lineNumber = 0 |
||
) |
Creates an integer variable with the given initial value expression.
variable | The expression variable associated with this variable. |
lowerBoundExpression | A constant expression defining the lower bound of the domain of the variable. |
upperBoundExpression | A constant expression defining the upper bound of the domain of the variable. |
initialValueExpression | A constant expression that defines the initial value of the variable. |
filename | The filename in which the variable is defined. |
lineNumber | The line number in which the variable is defined. |
Definition at line 7 of file IntegerVariable.cpp.
|
overridevirtual |
Equips the variable with an initial value based on its type if not initial value is present.
Implements storm::prism::Variable.
Definition at line 71 of file IntegerVariable.cpp.
storm::expressions::Expression const & storm::prism::IntegerVariable::getLowerBoundExpression | ( | ) | const |
Retrieves an expression defining the lower bound for this integer variable.
Definition at line 20 of file IntegerVariable.cpp.
storm::expressions::Expression storm::prism::IntegerVariable::getRangeExpression | ( | ) | const |
Retrieves an expression characterizing the legal range of the variable.
Only bounds that are defined will be considered in this expression. If neither a lower nor an upper bound is defined, this expression will be equivalent to true.
Definition at line 36 of file IntegerVariable.cpp.
storm::expressions::Expression const & storm::prism::IntegerVariable::getUpperBoundExpression | ( | ) | const |
Retrieves an expression defining the upper bound for this integer variable.
Definition at line 30 of file IntegerVariable.cpp.
bool storm::prism::IntegerVariable::hasLowerBoundExpression | ( | ) | const |
Definition at line 16 of file IntegerVariable.cpp.
bool storm::prism::IntegerVariable::hasUpperBoundExpression | ( | ) | const |
Definition at line 26 of file IntegerVariable.cpp.
|
default |
|
default |
IntegerVariable storm::prism::IntegerVariable::substitute | ( | std::map< storm::expressions::Variable, storm::expressions::Expression > const & | substitution | ) | const |
Substitutes all identifiers in the boolean variable according to the given map.
substitution | The substitution to perform. |
Definition at line 52 of file IntegerVariable.cpp.
IntegerVariable storm::prism::IntegerVariable::substituteNonStandardPredicates | ( | ) | const |
Definition at line 61 of file IntegerVariable.cpp.
|
friend |
Definition at line 81 of file IntegerVariable.cpp.