Variable.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <string>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/jani/types/AllJaniTypes.h"
 
namespace storm {
namespace jani {
class Variable {
   public:
    Variable(std::string const& name, JaniType const& type, storm::expressions::Variable const& variable, storm::expressions::Expression const& init,
             bool transient = false);
 
    Variable(std::string const& name, JaniType const& type, storm::expressions::Variable const& variable);
 
    std::unique_ptr<Variable> clone() const;
 
    storm::expressions::Variable const& getExpressionVariable() const;
 
    void setExpressionVariable(storm::expressions::Variable const& newVariable);
 
    std::string const& getName() const;
 
    void setName(std::string const& newName);
 
    bool hasInitExpression() const;
 
    storm::expressions::Expression const& getInitExpression() const;
 
    void setInitExpression(storm::expressions::Expression const& initialExpression);
 
    bool isTransient() const;
 
    JaniType& getType();
    JaniType const& getType() const;
 
    storm::expressions::Expression getRangeExpression() const;
 
    ~Variable();
 
    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);
 
    static std::shared_ptr<Variable> makeVariable(std::string const& name, JaniType const& type, storm::expressions::Variable const& variable,
                                                  boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeBasicTypeVariable(std::string const& name, BasicType::Type const& type, storm::expressions::Variable const& variable,
                                                           boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeBooleanVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                         boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeIntegerVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                         boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeRealVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                      boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeBoundedVariable(std::string const& name, BoundedType::BaseType const& type,
                                                         storm::expressions::Variable const& variable,
                                                         boost::optional<storm::expressions::Expression> const& initValue, bool transient,
                                                         boost::optional<storm::expressions::Expression> const& lowerBound,
                                                         boost::optional<storm::expressions::Expression> const& upperBound);
    static std::shared_ptr<Variable> makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                                boost::optional<storm::expressions::Expression> const& initValue, bool transient,
                                                                boost::optional<storm::expressions::Expression> const& lowerBound,
                                                                boost::optional<storm::expressions::Expression> const& upperBound);
    static std::shared_ptr<Variable> makeBoundedRealVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                             boost::optional<storm::expressions::Expression> const& initValue, bool transient,
                                                             boost::optional<storm::expressions::Expression> const& lowerBound,
                                                             boost::optional<storm::expressions::Expression> const& upperBound);
    static std::shared_ptr<Variable> makeArrayVariable(std::string const& name, JaniType const& baseType, storm::expressions::Variable const& variable,
                                                       boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeClockVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                       boost::optional<storm::expressions::Expression> const& initValue, bool transient);
    static std::shared_ptr<Variable> makeContinuousVariable(std::string const& name, storm::expressions::Variable const& variable,
                                                            boost::optional<storm::expressions::Expression> const& initValue, bool transient);
 
   private:
    std::string name;
    std::unique_ptr<JaniType> type;
    storm::expressions::Variable variable;
    storm::expressions::Expression init;
    bool transient;
};
 
bool operator==(Variable const& lhs, Variable const& rhs);
bool operator!=(Variable const& lhs, Variable const& rhs);
 
}  // namespace jani
}  // namespace storm