Storm
A Modern Probabilistic Model Checker
|
#include <Update.h>
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 | |
Update & | operator= (Update const &other)=default |
Update (Update &&other)=default | |
Update & | operator= (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::Expression > | getAsVariableToExpressionMap () 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) | |
![]() | |
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 | |
LocatedInformation & | operator= (LocatedInformation const &other)=default |
LocatedInformation (LocatedInformation &&other)=default | |
LocatedInformation & | operator= (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) |
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.
globalIndex | The global index of the update. |
likelihoodExpression | An expression specifying the likelihood of this update. |
assignments | A assignments to variables. |
filename | The filename in which the update is defined. |
lineNumber | The line number in which the update is defined. |
Definition at line 13 of file Update.cpp.
|
default |
|
default |
|
default |
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.
Definition at line 52 of file Update.cpp.
std::vector< storm::prism::Assignment > & storm::prism::Update::getAssignments | ( | ) |
Retrieves a reference to the map of variable names to their respective assignments.
Definition at line 48 of file Update.cpp.
std::vector< storm::prism::Assignment > const & storm::prism::Update::getAssignments | ( | ) | const |
Retrieves a reference to the map of variable names to their respective assignments.
Definition at line 44 of file Update.cpp.
std::map< storm::expressions::Variable, storm::expressions::Expression > storm::prism::Update::getAsVariableToExpressionMap | ( | ) | const |
Creates a mapping representation of this update.
Definition at line 59 of file Update.cpp.
uint_fast64_t storm::prism::Update::getGlobalIndex | ( | ) | const |
Retrieves the global index of the update, that is, a unique index over all modules.
Definition at line 69 of file Update.cpp.
storm::expressions::Expression const & storm::prism::Update::getLikelihoodExpression | ( | ) | const |
Retrieves the expression for the likelihood of this update.
Definition at line 36 of file Update.cpp.
std::size_t storm::prism::Update::getNumberOfAssignments | ( | ) | const |
Retrieves the number of assignments associated with this update.
Definition at line 40 of file Update.cpp.
Update storm::prism::Update::removeIdentityAssignments | ( | ) | const |
Removes all assignments which do not change the variable.
Definition at line 104 of file Update.cpp.
Update storm::prism::Update::simplify | ( | ) | const |
Simplifies the update in various ways (also removes identity assignments)
Definition at line 115 of file Update.cpp.
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.
substitution | The substitution to perform. |
Definition at line 80 of file Update.cpp.
Update storm::prism::Update::substituteNonStandardPredicates | ( | ) | const |
Definition at line 92 of file Update.cpp.
|
friend |
Definition at line 127 of file Update.cpp.