#include <TemplateEdge.h>

Public Member Functions
	TemplateEdge ()=default

	TemplateEdge (TemplateEdge const &)=default

	TemplateEdge (storm::expressions::Expression const &guard)

	TemplateEdge (storm::expressions::Expression const &guard, OrderedAssignments const &assignments, std::vector< TemplateEdgeDestination > const &destinations)

storm::expressions::Expression const &	getGuard () const

void	setGuard (storm::expressions::Expression const &newGuard)

void	addDestination (TemplateEdgeDestination const &destination)

void	finalize (Model const &containingModel)
	Finalizes the building of this edge.

std::size_t	getNumberOfDestinations () const

std::vector< TemplateEdgeDestination > const &	getDestinations () const

std::vector< TemplateEdgeDestination > &	getDestinations ()

TemplateEdgeDestination const &	getDestination (uint64_t index) const

OrderedAssignments const &	getAssignments () const

OrderedAssignments &	getAssignments ()

bool	addTransientAssignment (Assignment const &assignment, bool addToExisting=false)
	Adds a transient assignment to this edge.

storm::storage::FlatSet< storm::expressions::Variable > const &	getWrittenGlobalVariables () const
	Retrieves a set of (global) variables that are written by at least one of the edge's destinations.

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.

void	changeAssignmentVariables (std::map< Variable const *, std::reference_wrapper< Variable const > > const &remapping)
	Changes all variables in assignments based on the given mapping.

void	liftTransientDestinationAssignments (int64_t maxLevel=0)
	Finds the transient assignments common to all destinations and lifts them to the edge.

void	pushAssignmentsToDestinations ()
	Shifts the assingments from the edges to the destinations.

bool	usesVariablesInNonTransientAssignments (std::set< storm::expressions::Variable > const &variables) const
	Checks whether the provided variables appear on the right-hand side of non-transient assignments.

bool	hasTransientEdgeDestinationAssignments () const
	Retrieves whether there is any transient edge destination assignment in the edge.

bool	usesAssignmentLevels (bool onlyTransient=false) const
	Retrieves whether the edge uses an assignment level other than zero.

int64_t const &	getLowestAssignmentLevel () const
	Retrieves the lowest assignment level occurring in a destination assignment.

int64_t const &	getHighestAssignmentLevel () const
	Retrieves the highest assignment level occurring in a destination assignment If no assignment exists, this value is always zero.

bool	isLinear () const
	Checks the template edge for linearity.

bool	hasEdgeDestinationAssignments () const

TemplateEdge	simplifyIndexedAssignments (bool syncronized, VariableSet const &localVars) const
	Simplify Indexed Assignments.

Detailed Description

Definition at line 14 of file TemplateEdge.h.

Constructor & Destructor Documentation

◆ TemplateEdge() [1/4]

storm::jani::TemplateEdge::TemplateEdge ( )

default

◆ TemplateEdge() [2/4]

storm::jani::TemplateEdge::TemplateEdge ( TemplateEdge const & )

default

◆ TemplateEdge() [3/4]

storm::jani::TemplateEdge::TemplateEdge ( storm::expressions::Expression const & guard )

Definition at line 12 of file TemplateEdge.cpp.

◆ TemplateEdge() [4/4]

storm::jani::TemplateEdge::TemplateEdge	(	storm::expressions::Expression const &	guard,
		OrderedAssignments const &	assignments,
		std::vector< TemplateEdgeDestination > const &	destinations
	)

Definition at line 17 of file TemplateEdge.cpp.

Member Function Documentation

◆ addDestination()

void storm::jani::TemplateEdge::addDestination ( TemplateEdgeDestination const & destination )

Definition at line 27 of file TemplateEdge.cpp.

◆ addTransientAssignment()

bool storm::jani::TemplateEdge::addTransientAssignment	(	Assignment const &	assignment,
		bool	addToExisting = `false`
	)

Adds a transient assignment to this edge.

Parameters

assignment	The transient assignment to add.
addToExisting	Determines if adding the assigned expression to an already existing assignment is allowed (if the assigned variable is quantitative).

Returns: True if the assignment was added.

Definition at line 31 of file TemplateEdge.cpp.

◆ changeAssignmentVariables()

void storm::jani::TemplateEdge::changeAssignmentVariables ( std::map< Variable const *, std::reference_wrapper< Variable const > > const & remapping )

Changes all variables in assignments based on the given mapping.

Definition at line 101 of file TemplateEdge.cpp.

◆ finalize()

void storm::jani::TemplateEdge::finalize ( Model const & containingModel )

Finalizes the building of this edge.

Subsequent changes to the edge require another call to this method. Note that this method is invoked by a call to finalize to the containing model.

Definition at line 35 of file TemplateEdge.cpp.

◆ getAssignments() [1/2]

OrderedAssignments & storm::jani::TemplateEdge::getAssignments ( )

Definition at line 84 of file TemplateEdge.cpp.

◆ getAssignments() [2/2]

OrderedAssignments const & storm::jani::TemplateEdge::getAssignments ( ) const

Definition at line 80 of file TemplateEdge.cpp.

◆ getDestination()

TemplateEdgeDestination const & storm::jani::TemplateEdge::getDestination ( uint64_t index ) const

Definition at line 76 of file TemplateEdge.cpp.

◆ getDestinations() [1/2]

std::vector< TemplateEdgeDestination > & storm::jani::TemplateEdge::getDestinations ( )

Definition at line 72 of file TemplateEdge.cpp.

◆ getDestinations() [2/2]

std::vector< TemplateEdgeDestination > const & storm::jani::TemplateEdge::getDestinations ( ) const

Definition at line 68 of file TemplateEdge.cpp.

◆ getGuard()

storm::expressions::Expression const & storm::jani::TemplateEdge::getGuard ( ) const

Definition at line 56 of file TemplateEdge.cpp.

◆ getHighestAssignmentLevel()

int64_t const & storm::jani::TemplateEdge::getHighestAssignmentLevel ( ) const

Retrieves the highest assignment level occurring in a destination assignment If no assignment exists, this value is always zero.

Definition at line 189 of file TemplateEdge.cpp.

◆ getLowestAssignmentLevel()

int64_t const & storm::jani::TemplateEdge::getLowestAssignmentLevel ( ) const

Retrieves the lowest assignment level occurring in a destination assignment.

If no assignment exists, this value is the highest possible integer

Definition at line 185 of file TemplateEdge.cpp.

◆ getNumberOfDestinations()

std::size_t storm::jani::TemplateEdge::getNumberOfDestinations ( ) const

Definition at line 64 of file TemplateEdge.cpp.

◆ getWrittenGlobalVariables()

storm::storage::FlatSet< storm::expressions::Variable > const & storm::jani::TemplateEdge::getWrittenGlobalVariables ( ) const

Retrieves a set of (global) variables that are written by at least one of the edge's destinations.

Definition at line 52 of file TemplateEdge.cpp.

◆ hasEdgeDestinationAssignments()

bool storm::jani::TemplateEdge::hasEdgeDestinationAssignments ( ) const

Definition at line 193 of file TemplateEdge.cpp.

◆ hasTransientEdgeDestinationAssignments()

bool storm::jani::TemplateEdge::hasTransientEdgeDestinationAssignments ( ) const

Retrieves whether there is any transient edge destination assignment in the edge.

Definition at line 164 of file TemplateEdge.cpp.

◆ isLinear()

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

Checks the template edge for linearity.

Definition at line 202 of file TemplateEdge.cpp.

◆ liftTransientDestinationAssignments()

void storm::jani::TemplateEdge::liftTransientDestinationAssignments ( int64_t maxLevel = 0 )

Finds the transient assignments common to all destinations and lifts them to the edge.

Afterwards, these assignments are no longer contained in the destination. Note that this may modify the semantics of the model if assignment levels are being used somewhere in the model.

Definition at line 108 of file TemplateEdge.cpp.

◆ pushAssignmentsToDestinations()

void storm::jani::TemplateEdge::pushAssignmentsToDestinations ( )

Shifts the assingments from the edges to the destinations.

Definition at line 143 of file TemplateEdge.cpp.

◆ setGuard()

void storm::jani::TemplateEdge::setGuard ( storm::expressions::Expression const & newGuard )

Definition at line 60 of file TemplateEdge.cpp.

◆ simplifyIndexedAssignments()

TemplateEdge storm::jani::TemplateEdge::simplifyIndexedAssignments	(	bool	syncronized,
		VariableSet const &	localVars
	)		const

Simplify Indexed Assignments.

Definition at line 212 of file TemplateEdge.cpp.

◆ substitute()

void storm::jani::TemplateEdge::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 88 of file TemplateEdge.cpp.

◆ usesAssignmentLevels()

bool storm::jani::TemplateEdge::usesAssignmentLevels ( bool onlyTransient = false ) const

Retrieves whether the edge uses an assignment level other than zero.

Definition at line 173 of file TemplateEdge.cpp.

◆ usesVariablesInNonTransientAssignments()

bool storm::jani::TemplateEdge::usesVariablesInNonTransientAssignments ( std::set< storm::expressions::Variable > const & variables ) const

Checks whether the provided variables appear on the right-hand side of non-transient assignments.

Definition at line 153 of file TemplateEdge.cpp.

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

src/storm/storage/jani/TemplateEdge.h
src/storm/storage/jani/TemplateEdge.cpp

Public Member Functions