Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Variable.h
Go to the documentation of this file.
1#ifndef STORM_STORAGE_PRISM_VARIABLE_H_
2#define STORM_STORAGE_PRISM_VARIABLE_H_
3
4#include <map>
5
9
10namespace storm {
11namespace prism {
13 public:
14 // Create default implementations of constructors/assignment.
15 Variable(Variable const& otherVariable) = default;
16 Variable& operator=(Variable const& otherVariable) = default;
17 Variable(Variable&& otherVariable) = default;
18 Variable& operator=(Variable&& otherVariable) = default;
19 virtual ~Variable() = default;
20
26 std::string const& getName() const;
27
33 bool hasInitialValue() const;
34
42
48 void setInitialValueExpression(storm::expressions::Expression const& initialValueExpression);
49
56
63
67 bool isObservable() const;
68
72 virtual void createMissingInitialValue() = 0;
73
74 // Make the constructors protected to forbid instantiation of this class.
75 protected:
76 Variable() = default;
77
87 Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable = false,
88 std::string const& filename = "", uint_fast64_t lineNumber = 0);
89
101 Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName,
102 std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, bool observable = false, std::string const& filename = "",
103 uint_fast64_t lineNumber = 0);
104
105 private:
106 // The expression variable associated with this variable.
108
109 // The constant expression defining the initial value of the variable.
110 storm::expressions::Expression initialValueExpression;
111
112 // Whether this variable is a so-called observable. If true, the variable is listed as observable
113 bool observable;
114};
115
116} // namespace prism
117} // namespace storm
118
119#endif /* STORM_STORAGE_PRISM_VARIABLE_H_ */
This class is responsible for managing a set of typed variables and all expressions using these varia...
storm::expressions::Expression const & getInitialValueExpression() const
Retrieves the expression defining the initial value of the variable.
Definition Variable.cpp:32
storm::expressions::Variable const & getExpressionVariable() const
Retrieves the expression variable associated with this variable.
Definition Variable.cpp:40
storm::expressions::Expression getExpression() const
Retrieves the expression associated with this variable.
Definition Variable.cpp:44
virtual ~Variable()=default
void setInitialValueExpression(storm::expressions::Expression const &initialValueExpression)
Sets the expression defining the initial value of the variable.
Definition Variable.cpp:36
std::string const & getName() const
Retrieves the name of the variable.
Definition Variable.cpp:24
bool hasInitialValue() const
Retrieves whether the variable has an initial value.
Definition Variable.cpp:28
bool isObservable() const
Retrieves whether the variable is observable.
Definition Variable.cpp:48
Variable(Variable &&otherVariable)=default
Variable(Variable const &otherVariable)=default
Variable & operator=(Variable const &otherVariable)=default
Variable & operator=(Variable &&otherVariable)=default
virtual void createMissingInitialValue()=0
Equips the variable with an initial value based on its type if not initial value is present.
LabParser.cpp.