Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
LValue.h
Go to the documentation of this file.
1#pragma once
2
5
6namespace storm {
7namespace jani {
8
9class LValue {
10 public:
11 explicit LValue(storm::jani::Variable const& variable);
12 LValue(storm::jani::Variable const&, std::vector<storm::expressions::Expression> const& index);
13
14 bool operator==(LValue const& other) const;
15
16 bool isVariable() const;
17 bool isArray() const;
18 bool isArrayAccess() const;
19 bool isFullArrayAccess() const;
20 storm::jani::Variable const& getVariable() const;
21 std::vector<storm::expressions::Expression>& getArrayIndexVector();
22 std::vector<storm::expressions::Expression> const& getArrayIndexVector() const;
23 std::string getName() const;
24
25 bool arrayIndexContainsVariable() const;
26 void setArrayIndex(std::vector<storm::expressions::Expression> const& newIndex);
27
33
34 bool isTransient() const;
35 bool operator<(LValue const& other) const;
36
37 LValue changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) const;
38
39 friend std::ostream& operator<<(std::ostream& stream, LValue const& lvalue);
40
41 private:
42 // The variable being assigned, this can either be the array variable or a variable of a different type
43 storm::jani::Variable const* variable;
44
45 // In case of an array access LValue, this is the accessed index of the array (if existing)
46 std::vector<storm::expressions::Expression> arrayIndexVector;
47};
48} // namespace jani
49} // namespace storm
bool arrayIndexContainsVariable() const
Definition LValue.cpp:50
friend std::ostream & operator<<(std::ostream &stream, LValue const &lvalue)
Definition LValue.cpp:141
bool operator==(LValue const &other) const
Definition LValue.cpp:118
bool isFullArrayAccess() const
Returns true if the lValue refers to an array access.
Definition LValue.cpp:36
std::string getName() const
Definition LValue.cpp:87
void addArrayAccessIndex(storm::expressions::Expression const &index)
Adds an array access index.
Definition LValue.cpp:65
void setArrayIndex(std::vector< storm::expressions::Expression > const &newIndex)
Definition LValue.cpp:60
bool isTransient() const
Definition LValue.cpp:70
LValue changeAssignmentVariables(std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping) const
Definition LValue.cpp:74
bool operator<(LValue const &other) const
Definition LValue.cpp:98
bool isVariable() const
Definition LValue.cpp:20
bool isArray() const
Returns true if the lValue refers to a variable (potentially of type array).
Definition LValue.cpp:24
std::vector< storm::expressions::Expression > & getArrayIndexVector()
Returns the referred variable. In case of an array access, this is the referred array variable.
Definition LValue.cpp:40
bool isArrayAccess() const
Returns true if the lValue refers either to an array variable or to an array access.
Definition LValue.cpp:32
storm::jani::Variable const & getVariable() const
To check if the array is fully accessed, so result will be of the most inner child Type....
Definition LValue.cpp:28
LabParser.cpp.
Definition cli.cpp:18