Assignment.h

Go to the documentation of this file.

#pragma once
 
#include <functional>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/jani/LValue.h"
 
namespace storm {
namespace jani {
 
class Assignment {
   public:
    Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, int64_t level = 0);
 
    Assignment(storm::jani::Variable const& lValue, storm::expressions::Expression const&, int64_t level = 0);
 
    Assignment(Assignment const&) = default;
    bool operator==(Assignment const& other) const;
 
    bool lValueIsVariable() const;
 
    bool lValueIsArrayAccess() const;
 
    storm::jani::LValue const& getLValue() const;
 
    storm::jani::LValue& getLValue();
 
    storm::jani::Variable const& getVariable() const;
 
    storm::expressions::Variable const& getExpressionVariable() const;
 
    storm::expressions::Expression const& getAssignedExpression() const;
 
    void setAssignedExpression(storm::expressions::Expression const& expression);
 
    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);
 
    bool isTransient() const;
 
    int64_t getLevel() const;
 
    void setLevel(int64_t level);
 
    bool isLinear() const;
 
    friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
 
   private:
    // The lValue being assigned.
    LValue lValue;
 
    // The expression that is being assigned to the lValue.
    storm::expressions::Expression expression;
 
    // The level of the assignment.
    int64_t level;
};
 
struct AssignmentPartialOrderByLevelAndLValue {
    bool operator()(Assignment const& left, Assignment const& right) const;
    bool operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const;
    bool operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const;
    bool operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const;
};
 
}  // namespace jani
}  // namespace storm