LValue.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/expressions/Expressions.h"
#include "storm/storage/jani/Variable.h"
 
namespace storm {
namespace jani {
 
class LValue {
   public:
    explicit 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;            
    bool isArrayAccess() const;      
    bool isFullArrayAccess() const;  
    storm::jani::Variable const& getVariable() const;  
    std::vector<storm::expressions::Expression>& getArrayIndexVector();
    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);
 
    bool isTransient() const;
    bool operator<(LValue const& other) const;
 
    LValue changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) const;
 
    friend std::ostream& operator<<(std::ostream& stream, LValue const& lvalue);
 
   private:
    // The variable being assigned, this can either be the array variable or a variable of a different type
    storm::jani::Variable const* variable;
 
    // In case of an array access LValue, this is the accessed index of the array (if existing)
    std::vector<storm::expressions::Expression> arrayIndexVector;
};
}  // namespace jani
}  // namespace storm