Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::prism::Variable Class Referenceabstract

#include <Variable.h>

Inheritance diagram for storm::prism::Variable:
Collaboration diagram for storm::prism::Variable:

Public Member Functions

 Variable (Variable const &otherVariable)=default
 
Variableoperator= (Variable const &otherVariable)=default
 
 Variable (Variable &&otherVariable)=default
 
Variableoperator= (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.
 
- 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.
 

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.
 

Detailed Description

Definition at line 13 of file Variable.h.

Constructor & Destructor Documentation

◆ Variable() [1/5]

storm::prism::Variable::Variable ( Variable const &  otherVariable)
default

◆ Variable() [2/5]

storm::prism::Variable::Variable ( Variable &&  otherVariable)
default

◆ ~Variable()

virtual storm::prism::Variable::~Variable ( )
virtualdefault

◆ Variable() [3/5]

storm::prism::Variable::Variable ( )
protecteddefault

◆ Variable() [4/5]

storm::prism::Variable::Variable ( storm::expressions::Variable const &  variable,
storm::expressions::Expression const &  initialValueExpression,
bool  observable = false,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)
protected

Creates a variable with the given initial value.

Parameters
variableThe associated expression variable.
initialValueExpressionThe constant expression that defines the initial value of the variable.
observableWhether the variable is listed as observable
filenameThe filename in which the variable is defined.
lineNumberThe line number in which the variable is defined.

Definition at line 8 of file Variable.cpp.

◆ Variable() [5/5]

storm::prism::Variable::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 
)
protected

Creates a copy of the given variable and performs the provided renaming.

Parameters
managerThe manager responsible for the variable.
oldVariableThe variable to copy.
newNameNew name of this variable.
renamingA mapping from variables to the expressions with which they are to be replaced.
observableWhether the variable is listed as observable
filenameThe filename in which the variable is defined.
lineNumberThe line number in which the variable is defined.

Definition at line 14 of file Variable.cpp.

Member Function Documentation

◆ createMissingInitialValue()

virtual void storm::prism::Variable::createMissingInitialValue ( )
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.

◆ getExpression()

storm::expressions::Expression storm::prism::Variable::getExpression ( ) const

Retrieves the expression associated with this variable.

Returns
The expression associated with this variable.

Definition at line 44 of file Variable.cpp.

◆ getExpressionVariable()

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

Retrieves the expression variable associated with this variable.

Returns
The expression variable associated with this variable.

Definition at line 40 of file Variable.cpp.

◆ getInitialValueExpression()

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).

Returns
The expression defining the initial value of the variable.

Definition at line 32 of file Variable.cpp.

◆ getName()

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

Retrieves the name of the variable.

Returns
The name of the variable.

Definition at line 24 of file Variable.cpp.

◆ hasInitialValue()

bool storm::prism::Variable::hasInitialValue ( ) const

Retrieves whether the variable has an initial value.

Returns
True iff the variable has an initial value.

Definition at line 28 of file Variable.cpp.

◆ isObservable()

bool storm::prism::Variable::isObservable ( ) const

Retrieves whether the variable is observable.

Definition at line 48 of file Variable.cpp.

◆ operator=() [1/2]

Variable & storm::prism::Variable::operator= ( Variable &&  otherVariable)
default

◆ operator=() [2/2]

Variable & storm::prism::Variable::operator= ( Variable const &  otherVariable)
default

◆ setInitialValueExpression()

void storm::prism::Variable::setInitialValueExpression ( storm::expressions::Expression const &  initialValueExpression)

Sets the expression defining the initial value of the variable.

Parameters
initialValueExpressionThe expression defining the initial value of the variable.

Definition at line 36 of file Variable.cpp.


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