Jani Location: More...

#include <Location.h>

Public Member Functions
	Location (std::string const &name, std::vector< Assignment > const &transientAssignments={})
	Creates a new location.

	Location (std::string const &name, OrderedAssignments const &assignments)

std::string const &	getName () const
	Retrieves the name of the location.

OrderedAssignments const &	getAssignments () const
	Retrieves the assignments of this location.

OrderedAssignments &	getAssignments ()
	Retrieves the assignments of this location.

void	addTransientAssignment (storm::jani::Assignment const &assignment)
	Adds the given transient assignment to this location.

bool	hasTimeProgressInvariant () const
	Retrieves whether a time progress invariant is attached to this location.

storm::expressions::Expression const &	getTimeProgressInvariant () const
	Retrieves the time progress invariant.

void	setTimeProgressInvariant (storm::expressions::Expression const &expression)
	Sets the time progress invariant of this location.

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	checkValid () const
	Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments.

bool	isLinear () const
	Checks the automaton for linearity.

Detailed Description

Jani Location:

Whereas Jani Locations also support invariants, we do not have support for them (as we do not support any of the allowed model types).

Definition at line 15 of file Location.h.

Constructor & Destructor Documentation

◆ Location() [1/2]

storm::jani::Location::Location	(	std::string const &	name,
		std::vector< Assignment > const &	transientAssignments = `{}`
	)

Creates a new location.

Definition at line 11 of file Location.cpp.

◆ Location() [2/2]

storm::jani::Location::Location	(	std::string const &	name,
		OrderedAssignments const &	assignments
	)

Definition at line 15 of file Location.cpp.

Member Function Documentation

◆ addTransientAssignment()

void storm::jani::Location::addTransientAssignment ( storm::jani::Assignment const & assignment )

Adds the given transient assignment to this location.

Definition at line 31 of file Location.cpp.

◆ changeAssignmentVariables()

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

◆ checkValid()

void storm::jani::Location::checkValid ( ) const

Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments.

Definition at line 62 of file Location.cpp.

◆ getAssignments() [1/2]

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

Retrieves the assignments of this location.

Definition at line 27 of file Location.cpp.

◆ getAssignments() [2/2]

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

Retrieves the assignments of this location.

Definition at line 23 of file Location.cpp.

◆ getName()

std::string const & storm::jani::Location::getName ( ) const

Retrieves the name of the location.

Definition at line 19 of file Location.cpp.

◆ getTimeProgressInvariant()

storm::expressions::Expression const & storm::jani::Location::getTimeProgressInvariant ( ) const

Retrieves the time progress invariant.

Definition at line 40 of file Location.cpp.

◆ hasTimeProgressInvariant()

bool storm::jani::Location::hasTimeProgressInvariant ( ) const

Retrieves whether a time progress invariant is attached to this location.

Definition at line 36 of file Location.cpp.

◆ isLinear()

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

Checks the automaton for linearity.

Definition at line 66 of file Location.cpp.

◆ setTimeProgressInvariant()

void storm::jani::Location::setTimeProgressInvariant ( storm::expressions::Expression const & expression )

Sets the time progress invariant of this location.

Parameters

expression the location invariant (type bool)

Definition at line 44 of file Location.cpp.

◆ substitute()

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

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

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

Public Member Functions