This class represents a (deterministic) memory structure that can be used to encode certain events (such as reaching a set of goal states) into the state space of the model. More...

#include <MemoryStructure.h>

Public Types
typedef std::vector< std::vector< boost::optional< storm::storage::BitVector > > >	TransitionMatrix

Public Member Functions
	MemoryStructure (TransitionMatrix const &transitionMatrix, storm::models::sparse::StateLabeling const &memoryStateLabeling, std::vector< uint_fast64_t > const &initialMemoryStates, bool onlyInitialStatesRelevant=true)
	Creates a memory structure with the given transition matrix, the given memory state labeling, and the given initial states.

	MemoryStructure (TransitionMatrix &&transitionMatrix, storm::models::sparse::StateLabeling &&memoryStateLabeling, std::vector< uint_fast64_t > &&initialMemoryStates, bool onlyInitialStatesRelevant=true)

bool	isOnlyInitialStatesRelevantSet () const

TransitionMatrix const &	getTransitionMatrix () const

storm::models::sparse::StateLabeling const &	getStateLabeling () const

std::vector< uint_fast64_t > const &	getInitialMemoryStates () const

uint_fast64_t	getNumberOfStates () const

uint_fast64_t	getSuccessorMemoryState (uint_fast64_t const &currentMemoryState, uint_fast64_t const &modelTransitionIndex) const

MemoryStructure	product (MemoryStructure const &rhs) const
	Builds the product of this memory structure and the given memory structure.

template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
SparseModelMemoryProduct< ValueType, RewardModelType >	product (storm::models::sparse::Model< ValueType, RewardModelType > const &sparseModel) const
	Builds the product of this memory structure and the given sparse model.

std::string	toString () const

Detailed Description

This class represents a (deterministic) memory structure that can be used to encode certain events (such as reaching a set of goal states) into the state space of the model.

Definition at line 21 of file MemoryStructure.h.

Member Typedef Documentation

◆ TransitionMatrix

typedef std::vector<std::vector<boost::optional<storm::storage::BitVector> > > storm::storage::MemoryStructure::TransitionMatrix

Definition at line 23 of file MemoryStructure.h.

Constructor & Destructor Documentation

◆ MemoryStructure() [1/2]

storm::storage::MemoryStructure::MemoryStructure	(	TransitionMatrix const &	transitionMatrix,
		storm::models::sparse::StateLabeling const &	memoryStateLabeling,
		std::vector< uint_fast64_t > const &	initialMemoryStates,
		bool	onlyInitialStatesRelevant = `true`
	)

Creates a memory structure with the given transition matrix, the given memory state labeling, and the given initial states.

The entry transitionMatrix[m][n] specifies the set of model transitions which trigger a transition from memory state m to memory state n. Transitions are assumed to be deterministic and complete, i.e., the sets in in transitionMatrix[m] form a partition of the transitions of the considered model.

Parameters

transitionMatrix	The transition matrix
memoryStateLabeling	A labeling of the memory states to specify, e.g., accepting states
initialMemoryStates	assigns an initial memory state to each (initial?) state of the model.
onlyInitialStatesRelevant	if true, initial memory states are only provided for each initial model state. Otherwise, an initial memory state is provided for every model state.

Definition at line 14 of file MemoryStructure.cpp.

◆ MemoryStructure() [2/2]

storm::storage::MemoryStructure::MemoryStructure	(	TransitionMatrix &&	transitionMatrix,
		storm::models::sparse::StateLabeling &&	memoryStateLabeling,
		std::vector< uint_fast64_t > &&	initialMemoryStates,
		bool	onlyInitialStatesRelevant = `true`
	)

Definition at line 23 of file MemoryStructure.cpp.

Member Function Documentation

◆ getInitialMemoryStates()

std::vector< uint_fast64_t > const & storm::storage::MemoryStructure::getInitialMemoryStates ( ) const

Definition at line 44 of file MemoryStructure.cpp.

◆ getNumberOfStates()

uint_fast64_t storm::storage::MemoryStructure::getNumberOfStates ( ) const

Definition at line 48 of file MemoryStructure.cpp.

◆ getStateLabeling()

storm::models::sparse::StateLabeling const & storm::storage::MemoryStructure::getStateLabeling ( ) const

Definition at line 40 of file MemoryStructure.cpp.

◆ getSuccessorMemoryState()

uint_fast64_t storm::storage::MemoryStructure::getSuccessorMemoryState	(	uint_fast64_t const &	currentMemoryState,
		uint_fast64_t const &	modelTransitionIndex
	)		const

Definition at line 52 of file MemoryStructure.cpp.

◆ getTransitionMatrix()

MemoryStructure::TransitionMatrix const & storm::storage::MemoryStructure::getTransitionMatrix ( ) const

Definition at line 36 of file MemoryStructure.cpp.

◆ isOnlyInitialStatesRelevantSet()

bool storm::storage::MemoryStructure::isOnlyInitialStatesRelevantSet ( ) const

Definition at line 32 of file MemoryStructure.cpp.

◆ product() [1/2]

MemoryStructure storm::storage::MemoryStructure::product ( MemoryStructure const & rhs ) const

Builds the product of this memory structure and the given memory structure.

The resulting memory structure will have the state labels of both given structures. Throws an exception if the state labelings are not disjoint.

Definition at line 63 of file MemoryStructure.cpp.

◆ product() [2/2]

template<typename ValueType , typename RewardModelType >

SparseModelMemoryProduct< ValueType, RewardModelType > storm::storage::MemoryStructure::product ( storm::models::sparse::Model< ValueType, RewardModelType > const & sparseModel ) const

Builds the product of this memory structure and the given sparse model.

An exception is thrown if the state labelings of this memory structure and the given model are not disjoint.

Definition at line 138 of file MemoryStructure.cpp.

◆ toString()

std::string storm::storage::MemoryStructure::toString ( ) const

Definition at line 143 of file MemoryStructure.cpp.

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

src/storm/storage/memorystructure/MemoryStructure.h
src/storm/storage/memorystructure/MemoryStructure.cpp

Public Types

Public Member Functions