#include <Update.h>

Inheritance diagram for storm::prism::Update:

Collaboration diagram for storm::prism::Update:

Public Types
using	ExpressionPair = std::pair< storm::expressions::Expression, storm::expressions::Expression >

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 (uint_fast64_t globalIndex, ExpressionPair const &likelihoodExpressionInterval, 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 (possibly as an interval) and assignments.

	Update ()=default

	Update (Update const &other)=default

Update &	operator= (Update const &other)=default

	Update (Update &&other)=default

Update &	operator= (Update &&other)=default

bool	isLikelihoodInterval () const

storm::expressions::Expression const &	getLikelihoodExpression () const
	Retrieves the expression for the likelihood of this update.

ExpressionPair const &	getLikelihoodExpressionInterval () const
	Retrieves the two expression for the interval 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)

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

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)

Detailed Description

Definition at line 11 of file Update.h.

Member Typedef Documentation

◆ ExpressionPair

using storm::prism::Update::ExpressionPair = std::pair<storm::expressions::Expression, storm::expressions::Expression>

Definition at line 13 of file Update.h.

Constructor & Destructor Documentation

◆ Update() [1/5]

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

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.

◆ Update() [2/5]

storm::prism::Update::Update	(	uint_fast64_t	globalIndex,
		ExpressionPair const &	likelihoodExpressionInterval,
		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 (possibly as an interval) and assignments.

The likelihood is assumed to be an interval iff likelihoodExpressionInterval.second.isInitialized() holds.

Parameters

globalIndex	The global index of the update.
likelihoodExpression	expressions 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 34 of file Update.cpp.

◆ Update() [3/5]

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

default

◆ Update() [4/5]

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

default

◆ Update() [5/5]

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 83 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 79 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 75 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 90 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 100 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.

Precondition: the likelihood is not an interval

Definition at line 61 of file Update.cpp.

◆ getLikelihoodExpressionInterval()

Update::ExpressionPair const & storm::prism::Update::getLikelihoodExpressionInterval ( ) const

Retrieves the two expression for the interval likelihood of this update.

Returns: The expressions representing the likelihood interval [first, second].

Precondition: the likelihood is an interval

Definition at line 66 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 71 of file Update.cpp.

◆ isLikelihoodInterval()

bool storm::prism::Update::isLikelihoodInterval ( ) const

Definition at line 57 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 155 of file Update.cpp.

◆ simplify()

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

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

Definition at line 166 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

substitution The substitution to perform.

Returns: The resulting update.

Definition at line 111 of file Update.cpp.

◆ substituteNonStandardPredicates()

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

Definition at line 133 of file Update.cpp.

Friends And Related Symbol Documentation

◆ operator<<

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

friend

Definition at line 184 of file Update.cpp.

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

src/storm/storage/prism/Update.h
src/storm/storage/prism/Update.cpp

Public Types

Public Member Functions

Friends

Detailed Description

Member Typedef Documentation

◆ ExpressionPair

Constructor & Destructor Documentation

◆ Update() [1/5]

◆ Update() [2/5]

◆ Update() [3/5]

◆ Update() [4/5]

◆ Update() [5/5]

Member Function Documentation

◆ getAssignment()

◆ getAssignments() [1/2]

◆ getAssignments() [2/2]

◆ getAsVariableToExpressionMap()

◆ getGlobalIndex()

◆ getLikelihoodExpression()

◆ getLikelihoodExpressionInterval()

◆ getNumberOfAssignments()

◆ isLikelihoodInterval()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ removeIdentityAssignments()

◆ simplify()

◆ substitute()

◆ substituteNonStandardPredicates()

Friends And Related Symbol Documentation

◆ operator<<