Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Friends | List of all members
storm::jani::LValue Class Reference

#include <LValue.h>

Public Member Functions

 LValue (storm::jani::Variable const &variable)
 
 LValue (storm::jani::Variable const &, std::vector< storm::expressions::Expression > const &index)
 
bool operator== (LValue const &other) const
 
bool isVariable () const
 
bool isArray () const
 Returns true if the lValue refers to a variable (potentially of type array).
 
bool isArrayAccess () const
 Returns true if the lValue refers either to an array variable or to an array access.
 
bool isFullArrayAccess () const
 Returns true if the lValue refers to an array access.
 
storm::jani::Variable const & getVariable () const
 To check if the array is fully accessed, so result will be of the most inner child Type. (bool[][] will be bool)
 
std::vector< storm::expressions::Expression > & getArrayIndexVector ()
 Returns the referred variable. In case of an array access, this is the referred array variable.
 
std::vector< storm::expressions::Expression > const & getArrayIndexVector () const
 
std::string getName () const
 
bool arrayIndexContainsVariable () const
 
void setArrayIndex (std::vector< storm::expressions::Expression > const &newIndex)
 
void addArrayAccessIndex (storm::expressions::Expression const &index)
 Adds an array access index.
 
bool isTransient () const
 
bool operator< (LValue const &other) const
 
LValue changeAssignmentVariables (std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping) const
 

Friends

std::ostream & operator<< (std::ostream &stream, LValue const &lvalue)
 

Detailed Description

Definition at line 9 of file LValue.h.

Constructor & Destructor Documentation

◆ LValue() [1/2]

storm::jani::LValue::LValue ( storm::jani::Variable const &  variable)
explicit

Definition at line 11 of file LValue.cpp.

◆ LValue() [2/2]

storm::jani::LValue::LValue ( storm::jani::Variable const &  variable,
std::vector< storm::expressions::Expression > const &  index 
)

Definition at line 15 of file LValue.cpp.

Member Function Documentation

◆ addArrayAccessIndex()

void storm::jani::LValue::addArrayAccessIndex ( storm::expressions::Expression const &  index)

Adds an array access index.

Assumes that the underlying variable is an array variable that isn't fully accessed yet. For example (using array variable a) a will become a[index] and a[1] will become a[1][index].

Definition at line 65 of file LValue.cpp.

◆ arrayIndexContainsVariable()

bool storm::jani::LValue::arrayIndexContainsVariable ( ) const

Definition at line 50 of file LValue.cpp.

◆ changeAssignmentVariables()

LValue storm::jani::LValue::changeAssignmentVariables ( std::map< Variable const *, std::reference_wrapper< Variable const > > const &  remapping) const

Definition at line 74 of file LValue.cpp.

◆ getArrayIndexVector() [1/2]

std::vector< storm::expressions::Expression > & storm::jani::LValue::getArrayIndexVector ( )

Returns the referred variable. In case of an array access, this is the referred array variable.

Definition at line 40 of file LValue.cpp.

◆ getArrayIndexVector() [2/2]

std::vector< storm::expressions::Expression > const & storm::jani::LValue::getArrayIndexVector ( ) const

Definition at line 45 of file LValue.cpp.

◆ getName()

std::string storm::jani::LValue::getName ( ) const

Definition at line 87 of file LValue.cpp.

◆ getVariable()

storm::jani::Variable const & storm::jani::LValue::getVariable ( ) const

To check if the array is fully accessed, so result will be of the most inner child Type. (bool[][] will be bool)

Definition at line 28 of file LValue.cpp.

◆ isArray()

bool storm::jani::LValue::isArray ( ) const

Returns true if the lValue refers to a variable (potentially of type array).

Definition at line 24 of file LValue.cpp.

◆ isArrayAccess()

bool storm::jani::LValue::isArrayAccess ( ) const

Returns true if the lValue refers either to an array variable or to an array access.

Definition at line 32 of file LValue.cpp.

◆ isFullArrayAccess()

bool storm::jani::LValue::isFullArrayAccess ( ) const

Returns true if the lValue refers to an array access.

Definition at line 36 of file LValue.cpp.

◆ isTransient()

bool storm::jani::LValue::isTransient ( ) const

Definition at line 70 of file LValue.cpp.

◆ isVariable()

bool storm::jani::LValue::isVariable ( ) const

Definition at line 20 of file LValue.cpp.

◆ operator<()

bool storm::jani::LValue::operator< ( LValue const &  other) const

Definition at line 98 of file LValue.cpp.

◆ operator==()

bool storm::jani::LValue::operator== ( LValue const &  other) const

Definition at line 118 of file LValue.cpp.

◆ setArrayIndex()

void storm::jani::LValue::setArrayIndex ( std::vector< storm::expressions::Expression > const &  newIndex)

Definition at line 60 of file LValue.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
LValue const &  lvalue 
)
friend

Definition at line 141 of file LValue.cpp.

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