Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Formula.cpp
Go to the documentation of this file.
2
3namespace storm {
4namespace prism {
5Formula::Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename,
6 uint_fast64_t lineNumber)
7 : LocatedInformation(filename, lineNumber), name(variable.getName()), variable(variable), expression(expression) {
8 // Intentionally left empty.
9}
10
11Formula::Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber)
12 : LocatedInformation(filename, lineNumber), name(name), expression(expression) {
13 // Intentionally left empty.
14}
15
16Formula::Formula(std::string const& name, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name) {
17 // Intentionally left empty.
18}
19
20std::string const& Formula::getName() const {
21 return this->name;
22}
23
25 return this->variable.is_initialized();
26}
27
29 return this->variable.get();
30}
31
33 return this->expression;
34}
35
37 assert(this->getExpression().isInitialized());
38 assert(!hasExpressionVariable() || this->getExpressionVariable().getType() == this->getExpression().getType());
39 return this->getExpressionVariable().getType();
40}
41
42Formula Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
43 assert(this->getExpression().isInitialized());
45 return Formula(this->getExpressionVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
46 } else {
47 return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
48 }
49}
50
52 assert(this->getExpression().isInitialized());
55 } else {
56 return Formula(this->getName(), this->getExpression().substituteNonStandardPredicates(), this->getFilename(), this->getLineNumber());
57 }
58}
59
60std::ostream& operator<<(std::ostream& stream, Formula const& formula) {
61 stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";";
62 return stream;
63}
64} // namespace prism
65} // namespace storm
Type const & getType() const
Retrieves the type of the variable.
Definition Variable.cpp:50
Formula substituteNonStandardPredicates() const
Definition Formula.cpp:51
storm::expressions::Expression const & getExpression() const
Retrieves the expression that is associated with this formula.
Definition Formula.cpp:32
bool hasExpressionVariable() const
Retrieves wheter a placeholder variable is used in expressions to represent this formula.
Definition Formula.cpp:24
Formula substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the expression of the formula according to the given map.
Definition Formula.cpp:42
std::string const & getName() const
Retrieves the name that is associated with this formula.
Definition Formula.cpp:20
storm::expressions::Type const & getType() const
Retrieves the return type of the formula, i.e., the return-type of the defining expression.
Definition Formula.cpp:36
storm::expressions::Variable const & getExpressionVariable() const
Retrieves the placeholder variable that is used in expressions to represent this formula.
Definition Formula.cpp:28
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.
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
LabParser.cpp.
Definition cli.cpp:18