Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Assignment.cpp
Go to the documentation of this file.
1#include "Assignment.h"
2
3namespace storm {
4namespace prism {
5Assignment::Assignment(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename,
6 uint_fast64_t lineNumber)
7 : LocatedInformation(filename, lineNumber), variable(variable), expression(expression) {
8 // Intentionally left empty.
9}
10
11std::string const& Assignment::getVariableName() const {
12 return variable.getName();
13}
14
16 return variable;
17}
18
20 return this->expression;
21}
22
23Assignment Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
24 return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber());
25}
26
30
32 if (this->expression.isVariable()) {
33 STORM_LOG_ASSERT(this->expression.getVariables().size() == 1, "Invalid number of variables.");
34 return variable == *(this->expression.getVariables().begin());
35 }
36 return false;
37}
38
39std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
40 stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")";
41 return stream;
42}
43
44} // namespace prism
45} // namespace storm
bool isVariable() const
Retrieves whether the expression is a variable.
std::set< storm::expressions::Variable > getVariables() const
Retrieves the set of all variables that appear in the expression.
std::string const & getName() const
Retrieves the name of the variable.
Definition Variable.cpp:46
storm::expressions::Variable const & getVariable() const
Retrieves the variable that is written to by this assignment.
std::string const & getVariableName() const
Retrieves the name of the variable that this assignment targets.
storm::expressions::Expression const & getExpression() const
Retrieves the expression that is assigned to the variable.
bool isIdentity() const
Checks whether the assignment is an identity (lhs equals rhs)
Assignment substitute(std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
Substitutes all variables in the assignment according to the given map.
Assignment 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.
#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