Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Friends | List of all members
storm::jani::Assignment Class Reference

#include <Assignment.h>

Public Member Functions

 Assignment (storm::jani::LValue const &lValue, storm::expressions::Expression const &expression, int64_t level=0)
 Creates an assignment of the given expression to the given LValue.
 
 Assignment (storm::jani::Variable const &lValue, storm::expressions::Expression const &, int64_t level=0)
 Creates an assignment of the given expression to the given Variable.
 
 Assignment (Assignment const &)=default
 
bool operator== (Assignment const &other) const
 
bool lValueIsVariable () const
 Returns true if the lValue is a variable.
 
bool lValueIsArrayAccess () const
 Returns true if the lValue is an array access.
 
storm::jani::LValue const & getLValue () const
 Retrieves the lValue that is written in this assignment.
 
storm::jani::LValue & getLValue ()
 Retrieves the lValue that is written in this assignment.
 
storm::jani::Variable const & getVariable () const
 Retrieves the Variable that is written in this assignment.
 
storm::expressions::Variable const & getExpressionVariable () const
 Retrieves the expression variable that is written in this assignment.
 
storm::expressions::Expression const & getAssignedExpression () const
 Retrieves the expression whose value is assigned to the target variable.
 
void setAssignedExpression (storm::expressions::Expression const &expression)
 Sets a new expression that is assigned to the target LValue.
 
void substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution, bool const substituteTranscendentalNumbers)
 Substitutes all variables in all expressions according to the given substitution.
 
bool isTransient () const
 Retrieves whether the assignment assigns to a transient variable.
 
int64_t getLevel () const
 Retrieves the level of the assignment.
 
void setLevel (int64_t level)
 Sets the level.
 
bool isLinear () const
 Checks the assignment for linearity.
 

Friends

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

Detailed Description

Definition at line 11 of file Assignment.h.

Constructor & Destructor Documentation

◆ Assignment() [1/3]

storm::jani::Assignment::Assignment ( storm::jani::LValue const &  lValue,
storm::expressions::Expression const &  expression,
int64_t  level = 0 
)

Creates an assignment of the given expression to the given LValue.

Definition at line 14 of file Assignment.cpp.

◆ Assignment() [2/3]

storm::jani::Assignment::Assignment ( storm::jani::Variable const &  lValue,
storm::expressions::Expression const &  expression,
int64_t  level = 0 
)

Creates an assignment of the given expression to the given Variable.

Definition at line 19 of file Assignment.cpp.

◆ Assignment() [3/3]

storm::jani::Assignment::Assignment ( Assignment const &  )
default

Member Function Documentation

◆ getAssignedExpression()

storm::expressions::Expression const & storm::jani::Assignment::getAssignedExpression ( ) const

Retrieves the expression whose value is assigned to the target variable.

Definition at line 53 of file Assignment.cpp.

◆ getExpressionVariable()

storm::expressions::Variable const & storm::jani::Assignment::getExpressionVariable ( ) const

Retrieves the expression variable that is written in this assignment.

This assumes that the lValue is a variable.

Definition at line 49 of file Assignment.cpp.

◆ getLevel()

int64_t storm::jani::Assignment::getLevel ( ) const

Retrieves the level of the assignment.

Definition at line 78 of file Assignment.cpp.

◆ getLValue() [1/2]

storm::jani::LValue & storm::jani::Assignment::getLValue ( )

Retrieves the lValue that is written in this assignment.

Definition at line 37 of file Assignment.cpp.

◆ getLValue() [2/2]

storm::jani::LValue const & storm::jani::Assignment::getLValue ( ) const

Retrieves the lValue that is written in this assignment.

Definition at line 41 of file Assignment.cpp.

◆ getVariable()

storm::jani::Variable const & storm::jani::Assignment::getVariable ( ) const

Retrieves the Variable that is written in this assignment.

This assumes that the lValue is a variable.

Definition at line 45 of file Assignment.cpp.

◆ isLinear()

bool storm::jani::Assignment::isLinear ( ) const

Checks the assignment for linearity.

Definition at line 86 of file Assignment.cpp.

◆ isTransient()

bool storm::jani::Assignment::isTransient ( ) const

Retrieves whether the assignment assigns to a transient variable.

Definition at line 61 of file Assignment.cpp.

◆ lValueIsArrayAccess()

bool storm::jani::Assignment::lValueIsArrayAccess ( ) const

Returns true if the lValue is an array access.

Definition at line 33 of file Assignment.cpp.

◆ lValueIsVariable()

bool storm::jani::Assignment::lValueIsVariable ( ) const

Returns true if the lValue is a variable.

Definition at line 29 of file Assignment.cpp.

◆ operator==()

bool storm::jani::Assignment::operator== ( Assignment const &  other) const

Definition at line 24 of file Assignment.cpp.

◆ setAssignedExpression()

void storm::jani::Assignment::setAssignedExpression ( storm::expressions::Expression const &  expression)

Sets a new expression that is assigned to the target LValue.

Definition at line 57 of file Assignment.cpp.

◆ setLevel()

void storm::jani::Assignment::setLevel ( int64_t  level)

Sets the level.

Definition at line 82 of file Assignment.cpp.

◆ substitute()

void storm::jani::Assignment::substitute ( std::map< storm::expressions::Variable, storm::expressions::Expression > const &  substitution,
bool const  substituteTranscendentalNumbers 
)

Substitutes all variables in all expressions according to the given substitution.

Definition at line 65 of file Assignment.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

Definition at line 91 of file Assignment.cpp.

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