Variable.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/storage/prism/LocatedInformation.h"
 
namespace storm {
namespace prism {
class Variable : public LocatedInformation {
   public:
    // Create default implementations of constructors/assignment.
    Variable(Variable const& otherVariable) = default;
    Variable& operator=(Variable const& otherVariable) = default;
    Variable(Variable&& otherVariable) = default;
    Variable& operator=(Variable&& otherVariable) = default;
    virtual ~Variable() = default;

    std::string const& getName() const;

    bool hasInitialValue() const;

    storm::expressions::Expression const& getInitialValueExpression() const;

    void setInitialValueExpression(storm::expressions::Expression const& initialValueExpression);

    storm::expressions::Variable const& getExpressionVariable() const;

    storm::expressions::Expression getExpression() const;

    bool isObservable() const;

    virtual void createMissingInitialValue() = 0;
 
    // Make the constructors protected to forbid instantiation of this class.
   protected:
    Variable() = default;

    Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable = false,
             std::string const& filename = "", uint_fast64_t lineNumber = 0);

    Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName,
             std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, bool observable = false, std::string const& filename = "",
             uint_fast64_t lineNumber = 0);
 
   private:
    // The expression variable associated with this variable.
    storm::expressions::Variable variable;
 
    // The constant expression defining the initial value of the variable.
    storm::expressions::Expression initialValueExpression;
 
    // Whether this variable is a so-called observable. If true, the variable is listed as observable
    bool observable;
};
 
}  // namespace prism
}  // namespace storm