Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IntegerVariable.cpp
Go to the documentation of this file.
2
4
5namespace storm {
6namespace prism {
8 storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression,
9 bool observable, std::string const& filename, uint_fast64_t lineNumber)
10 : Variable(variable, initialValueExpression, observable, filename, lineNumber),
11 lowerBoundExpression(lowerBoundExpression),
12 upperBoundExpression(upperBoundExpression) {
13 // Intentionally left empty.
14}
15
17 return this->lowerBoundExpression.isInitialized();
18}
19
21 STORM_LOG_ASSERT(hasLowerBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName()
22 << "' which is not bounded from below.");
23 return this->lowerBoundExpression;
24}
25
27 return this->upperBoundExpression.isInitialized();
28}
29
31 STORM_LOG_ASSERT(hasUpperBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName()
32 << "' which is not bounded from above.");
33 return this->upperBoundExpression;
34}
35
40 } else {
41 return this->getLowerBoundExpression() <= this->getExpressionVariable();
42 }
43 } else {
45 return this->getExpressionVariable() <= this->getUpperBoundExpression();
46 } else {
47 return this->getExpressionVariable().getManager().boolean(true);
48 }
49 }
50}
51
52IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
53 return IntegerVariable(
58 this->isObservable(), this->getFilename(), this->getLineNumber());
59}
60
70
72 if (!this->hasInitialValue()) {
73 if (this->hasLowerBoundExpression()) {
75 } else {
76 this->setInitialValueExpression(this->getExpressionVariable().getManager().integer(0));
77 }
78 }
79}
80
81std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
82 stream << variable.getName() << ": ";
83 if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) {
84 // The syntax for the case where there is only one bound is not standardized, yet.
85 stream << "[";
86 if (variable.hasLowerBoundExpression()) {
87 stream << variable.getLowerBoundExpression();
88 }
89 stream << "..";
90 if (variable.hasUpperBoundExpression()) {
91 stream << variable.getUpperBoundExpression();
92 }
93 stream << "]";
94 } else {
95 stream << "int";
96 }
97 if (variable.hasInitialValue()) {
98 stream << " init " << variable.getInitialValueExpression();
99 }
100 stream << ";";
101 return stream;
102}
103} // namespace prism
104} // namespace storm
Expression substitute(std::map< Variable, Expression > const &variableToExpressionMap) const
Substitutes all occurrences of the variables according to the given map.
bool isInitialized() const
Checks whether the object encapsulates a base-expression.
Expression substituteNonStandardPredicates() const
Eliminate nonstandard predicates from the expression.
Expression boolean(bool value) const
Creates an expression that characterizes the given boolean literal.
ExpressionManager const & getManager() const
Retrieves the manager responsible for this variable.
Definition Variable.cpp:54
storm::expressions::Expression getRangeExpression() const
Retrieves an expression characterizing the legal range of the variable.
storm::expressions::Expression const & getUpperBoundExpression() const
Retrieves an expression defining the upper bound for this integer variable.
storm::expressions::Expression const & getLowerBoundExpression() const
Retrieves an expression defining the lower bound for this integer variable.
IntegerVariable substituteNonStandardPredicates() const
virtual void createMissingInitialValue() override
Equips the variable with an initial value based on its type if not initial value is present.
IntegerVariable substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the boolean variable according to the given map.
uint_fast64_t getLineNumber() const
Retrieves the line number in which the information was found.
std::string const & getFilename() const
Retrieves the name of the file in which the information was found.
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
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
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
LabParser.cpp.
Definition cli.cpp:18