Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BooleanVariable.cpp
Go to the documentation of this file.
2
4
5namespace storm {
6namespace prism {
7BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable,
8 std::string const& filename, uint_fast64_t lineNumber)
9 : Variable(variable, initialValueExpression, observable, filename, lineNumber) {
10 // Nothing to do here.
11}
12
13BooleanVariable BooleanVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
14 return BooleanVariable(
16 this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(),
17 this->isObservable(), this->getFilename(), this->getLineNumber());
18}
19
26
28 if (!this->hasInitialValue()) {
29 this->setInitialValueExpression(this->getExpressionVariable().getManager().boolean(false));
30 }
31}
32
33std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
34 stream << variable.getName() << ": bool";
35 if (variable.hasInitialValue()) {
36 stream << " init " << variable.getInitialValueExpression();
37 }
38 stream << ";";
39 return stream;
40}
41
42} // namespace prism
43} // namespace storm
virtual void createMissingInitialValue() override
Equips the variable with an initial value based on its type if not initial value is present.
BooleanVariable substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all identifiers in the boolean variable according to the given map.
BooleanVariable substituteNonStandardPredicates() const
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
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
LabParser.cpp.
Definition cli.cpp:18