Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::prism::Assignment Class Reference

#include <Assignment.h>

Inheritance diagram for storm::prism::Assignment:
Collaboration diagram for storm::prism::Assignment:

Public Member Functions

 Assignment (storm::expressions::Variable const &variable, storm::expressions::Expression const &expression, std::string const &filename="", uint_fast64_t lineNumber=0)
 Constructs an assignment using the given variable name and expression.
 
 Assignment ()=default
 
 Assignment (Assignment const &other)=default
 
Assignmentoperator= (Assignment const &other)=default
 
 Assignment (Assignment &&other)=default
 
Assignmentoperator= (Assignment &&other)=default
 
std::string const & getVariableName () const
 Retrieves the name of the variable that this assignment targets.
 
storm::expressions::Variable const & getVariable () const
 Retrieves the variable that is written to by this assignment.
 
storm::expressions::Expression const & getExpression () const
 Retrieves the expression that is assigned to the variable.
 
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
 
bool isIdentity () const
 Checks whether the assignment is an identity (lhs equals rhs)
 
- Public Member Functions inherited from storm::prism::LocatedInformation
 LocatedInformation (std::string const &filename, uint_fast64_t lineNumber)
 Constructs a located information with the given filename and line number.
 
 LocatedInformation ()=default
 
 LocatedInformation (LocatedInformation const &other)=default
 
LocatedInformationoperator= (LocatedInformation const &other)=default
 
 LocatedInformation (LocatedInformation &&other)=default
 
LocatedInformationoperator= (LocatedInformation &&other)=default
 
std::string const & getFilename () const
 Retrieves the name of the file in which the information was found.
 
void setFilename (std::string const &filename)
 Sets the filename of this information.
 
uint_fast64_t getLineNumber () const
 Retrieves the line number in which the information was found.
 
void setLineNumber (uint_fast64_t lineNumber)
 Sets the line number of this information.
 

Friends

std::ostream & operator<< (std::ostream &stream, Assignment const &assignment)
 

Detailed Description

Definition at line 13 of file Assignment.h.

Constructor & Destructor Documentation

◆ Assignment() [1/4]

storm::prism::Assignment::Assignment ( storm::expressions::Variable const &  variable,
storm::expressions::Expression const &  expression,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Constructs an assignment using the given variable name and expression.

Parameters
variableThe variable that this assignment targets.
expressionThe expression to assign to the variable.
filenameThe filename in which the assignment is defined.
lineNumberThe line number in which the assignment is defined.

Definition at line 5 of file Assignment.cpp.

◆ Assignment() [2/4]

storm::prism::Assignment::Assignment ( )
default

◆ Assignment() [3/4]

storm::prism::Assignment::Assignment ( Assignment const &  other)
default

◆ Assignment() [4/4]

storm::prism::Assignment::Assignment ( Assignment &&  other)
default

Member Function Documentation

◆ getExpression()

storm::expressions::Expression const & storm::prism::Assignment::getExpression ( ) const

Retrieves the expression that is assigned to the variable.

Returns
The expression that is assigned to the variable.

Definition at line 19 of file Assignment.cpp.

◆ getVariable()

storm::expressions::Variable const & storm::prism::Assignment::getVariable ( ) const

Retrieves the variable that is written to by this assignment.

Returns
The variable that is written to by this assignment.

Definition at line 15 of file Assignment.cpp.

◆ getVariableName()

std::string const & storm::prism::Assignment::getVariableName ( ) const

Retrieves the name of the variable that this assignment targets.

Returns
The name of the variable that this assignment targets.

Definition at line 11 of file Assignment.cpp.

◆ isIdentity()

bool storm::prism::Assignment::isIdentity ( ) const

Checks whether the assignment is an identity (lhs equals rhs)

Returns
true iff the assignment is of the form a' = a.

Definition at line 31 of file Assignment.cpp.

◆ operator=() [1/2]

Assignment & storm::prism::Assignment::operator= ( Assignment &&  other)
default

◆ operator=() [2/2]

Assignment & storm::prism::Assignment::operator= ( Assignment const &  other)
default

◆ substitute()

Assignment storm::prism::Assignment::substitute ( std::map< storm::expressions::Variable, storm::expressions::Expression > const &  substitution) const

Substitutes all variables in the assignment according to the given map.

Parameters
substitutionThe substitution to perform.
Returns
The resulting assignment.

Definition at line 23 of file Assignment.cpp.

◆ substituteNonStandardPredicates()

Assignment storm::prism::Assignment::substituteNonStandardPredicates ( ) const

Definition at line 27 of file Assignment.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream &  stream,
Assignment const &  assignment 
)
friend

Definition at line 39 of file Assignment.cpp.


The documentation for this class was generated from the following files: