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

#include <Update.h>

Inheritance diagram for storm::prism::Update:
Collaboration diagram for storm::prism::Update:

Public Member Functions

 Update (uint_fast64_t globalIndex, storm::expressions::Expression const &likelihoodExpression, std::vector< storm::prism::Assignment > const &assignments, std::string const &filename="", uint_fast64_t lineNumber=0)
 Creates an update with the given expression specifying the likelihood and assignments.
 
 Update ()=default
 
 Update (Update const &other)=default
 
Updateoperator= (Update const &other)=default
 
 Update (Update &&other)=default
 
Updateoperator= (Update &&other)=default
 
storm::expressions::Expression const & getLikelihoodExpression () const
 Retrieves the expression for the likelihood of this update.
 
std::size_t getNumberOfAssignments () const
 Retrieves the number of assignments associated with this update.
 
std::vector< storm::prism::Assignment > const & getAssignments () const
 Retrieves a reference to the map of variable names to their respective assignments.
 
std::vector< storm::prism::Assignment > & getAssignments ()
 Retrieves a reference to the map of variable names to their respective assignments.
 
storm::prism::Assignment const & getAssignment (std::string const &variableName) const
 Retrieves a reference to the assignment for the variable with the given name.
 
std::map< storm::expressions::Variable, storm::expressions::ExpressiongetAsVariableToExpressionMap () const
 Creates a mapping representation of this update.
 
uint_fast64_t getGlobalIndex () const
 Retrieves the global index of the update, that is, a unique index over all modules.
 
Update substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
 Substitutes all identifiers in the update according to the given map.
 
Update removeIdentityAssignments () const
 Removes all assignments which do not change the variable.
 
Update substituteNonStandardPredicates () const
 
Update simplify () const
 Simplifies the update in various ways (also removes identity assignments)
 
- 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, Update const &assignment)
 

Detailed Description

Definition at line 12 of file Update.h.

Constructor & Destructor Documentation

◆ Update() [1/4]

storm::prism::Update::Update ( uint_fast64_t  globalIndex,
storm::expressions::Expression const &  likelihoodExpression,
std::vector< storm::prism::Assignment > const &  assignments,
std::string const &  filename = "",
uint_fast64_t  lineNumber = 0 
)

Creates an update with the given expression specifying the likelihood and assignments.

Parameters
globalIndexThe global index of the update.
likelihoodExpressionAn expression specifying the likelihood of this update.
assignmentsA assignments to variables.
filenameThe filename in which the update is defined.
lineNumberThe line number in which the update is defined.

Definition at line 13 of file Update.cpp.

◆ Update() [2/4]

storm::prism::Update::Update ( )
default

◆ Update() [3/4]

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

◆ Update() [4/4]

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

Member Function Documentation

◆ getAssignment()

storm::prism::Assignment const & storm::prism::Update::getAssignment ( std::string const &  variableName) const

Retrieves a reference to the assignment for the variable with the given name.

Returns
A reference to the assignment for the variable with the given name.

Definition at line 52 of file Update.cpp.

◆ getAssignments() [1/2]

std::vector< storm::prism::Assignment > & storm::prism::Update::getAssignments ( )

Retrieves a reference to the map of variable names to their respective assignments.

Returns
A reference to the map of variable names to their respective assignments.

Definition at line 48 of file Update.cpp.

◆ getAssignments() [2/2]

std::vector< storm::prism::Assignment > const & storm::prism::Update::getAssignments ( ) const

Retrieves a reference to the map of variable names to their respective assignments.

Returns
A reference to the map of variable names to their respective assignments.

Definition at line 44 of file Update.cpp.

◆ getAsVariableToExpressionMap()

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Update::getAsVariableToExpressionMap ( ) const

Creates a mapping representation of this update.

Returns
A mapping from variables to expressions.

Definition at line 59 of file Update.cpp.

◆ getGlobalIndex()

uint_fast64_t storm::prism::Update::getGlobalIndex ( ) const

Retrieves the global index of the update, that is, a unique index over all modules.

Returns
The global index of the update.

Definition at line 69 of file Update.cpp.

◆ getLikelihoodExpression()

storm::expressions::Expression const & storm::prism::Update::getLikelihoodExpression ( ) const

Retrieves the expression for the likelihood of this update.

Returns
The expression for the likelihood of this update.

Definition at line 36 of file Update.cpp.

◆ getNumberOfAssignments()

std::size_t storm::prism::Update::getNumberOfAssignments ( ) const

Retrieves the number of assignments associated with this update.

Returns
The number of assignments associated with this update.

Definition at line 40 of file Update.cpp.

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

◆ removeIdentityAssignments()

Update storm::prism::Update::removeIdentityAssignments ( ) const

Removes all assignments which do not change the variable.

Returns
The resulting update.

Definition at line 104 of file Update.cpp.

◆ simplify()

Update storm::prism::Update::simplify ( ) const

Simplifies the update in various ways (also removes identity assignments)

Definition at line 115 of file Update.cpp.

◆ substitute()

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

Substitutes all identifiers in the update according to the given map.

Parameters
substitutionThe substitution to perform.
Returns
The resulting update.

Definition at line 80 of file Update.cpp.

◆ substituteNonStandardPredicates()

Update storm::prism::Update::substituteNonStandardPredicates ( ) const

Definition at line 92 of file Update.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

Definition at line 127 of file Update.cpp.


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