Classes
class	ActionMask
	Action masks are arguments you can give to the state generator that limit which states are generated. More...

struct	ActiveCommandData

class	ArrayVariableReplacementInformation

class	BeliefStateManager
	This class keeps track of common information of a set of beliefs. More...

class	BeliefSupportTracker

struct	BooleanVariableInformation

struct	Choice

class	Distribution

class	DistributionEntry

struct	IntegerVariableInformation

class	JaniNextStateGenerator

struct	LocationVariableInformation

class	NextStateGenerator

class	NondeterministicBeliefTracker
	This tracker implements state estimation for POMDPs. More...

class	ObservationDenseBeliefState
	ObservationDenseBeliefState stores beliefs in a dense format (per observation). More...

struct	ObservationLabelInformation

class	PrismNextStateGenerator

class	SparseBeliefState
	SparseBeliefState stores beliefs in a sparse format. More...

class	StateBehavior

class	StateValuationFunctionMask
	A particular instance of the action mask that uses a callback function to evaluate whether an action should be expanded. More...

struct	TransientVariableData

struct	TransientVariableInformation

struct	TransientVariableValuation

struct	VariableInformation

Typedefs
typedef storm::storage::BitVector	CompressedState

typedef storm::builder::BuilderOptions	NextStateGeneratorOptions

Enumerations
enum class	ModelType { DTMC , CTMC , MDP , MA , POMDP , SMG }

Functions
template<typename ValueType >
bool	operator== (SparseBeliefState< ValueType > const &lhs, SparseBeliefState< ValueType > const &rhs)

template<typename ValueType >
bool	operator== (ObservationDenseBeliefState< ValueType > const &lhs, ObservationDenseBeliefState< ValueType > const &rhs)

template bool	operator== (SparseBeliefState< double > const &, SparseBeliefState< double > const &)

template bool	operator== (SparseBeliefState< storm::RationalNumber > const &, SparseBeliefState< storm::RationalNumber > const &)

template<typename InfoType >
ArrayVariableReplacementInformation	convertArrayReplacement (typename storm::jani::ArrayEliminatorData::Replacement const &replacement, InfoType const &relevantVariableInfo)

template<typename ValueType , typename StateType >
std::ostream &	operator<< (std::ostream &out, Choice< ValueType, StateType > const &choice)

template<typename ValueType >
void	unpackStateIntoEvaluator (CompressedState const &state, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< ValueType > &evaluator)
	Unpacks the compressed state into the evaluator.

storm::expressions::SimpleValuation	unpackStateIntoValuation (CompressedState const &state, VariableInformation const &variableInformation, storm::expressions::ExpressionManager const &manager)
	Converts the compressed state into an explicit representation in the form of a valuation.

CompressedState	packStateFromValuation (expressions::SimpleValuation const &valuation, VariableInformation const &variableInformation, bool checkOutOfBounds)

void	extractVariableValues (CompressedState const &state, VariableInformation const &variableInformation, std::vector< int64_t > &locationValues, std::vector< bool > &booleanValues, std::vector< int64_t > &integerValues)
	Appends the values of the given variables in the given state to the corresponding result vectors.

std::string	toString (CompressedState const &state, VariableInformation const &variableInformation)
	Returns a (human readable) string representation of the variable valuation encoded by the given state.

storm::storage::BitVector	computeObservabilityMask (VariableInformation const &variableInformation)

uint32_t	unpackStateToObservabilityClass (CompressedState const &state, storm::storage::BitVector const &observationVector, std::unordered_map< storm::storage::BitVector, uint32_t > &observabilityMap, storm::storage::BitVector const &mask)

template<typename ValueType >
storm::json< ValueType >	unpackStateIntoJson (CompressedState const &state, VariableInformation const &variableInformation, bool onlyObservable)

CompressedState	createOutOfBoundsState (VariableInformation const &varInfo, bool roundTo64Bit)

CompressedState	createCompressedState (VariableInformation const &varInfo, std::map< storm::expressions::Variable, storm::expressions::Expression > const &stateDescription, bool checkOutOfBounds)

template storm::json< double >	unpackStateIntoJson< double > (CompressedState const &state, VariableInformation const &variableInformation, bool onlyObservable)

template void	unpackStateIntoEvaluator< double > (CompressedState const &state, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< double > &evaluator)

uint64_t	getBitWidthLowerUpperBound (bool const &hasLowerBound, int64_t &lowerBound, bool const &hasUpperBound, int64_t &upperBound, uint64_t const &reservedBitsForUnboundedVariables)
	Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range.

Typedef Documentation

◆ CompressedState

typedef storm::storage::BitVector storm::generator::CompressedState

Definition at line 21 of file CompressedState.h.

◆ NextStateGeneratorOptions

typedef storm::builder::BuilderOptions storm::generator::NextStateGeneratorOptions

Definition at line 31 of file NextStateGenerator.h.

Enumeration Type Documentation

◆ ModelType

enum class storm::generator::ModelType

strong

Enumerator
DTMC
CTMC
MDP
MA
POMDP
SMG

Definition at line 33 of file NextStateGenerator.h.

Function Documentation

◆ computeObservabilityMask()

storm::storage::BitVector storm::generator::computeObservabilityMask ( VariableInformation const & variableInformation )

Parameters

variableInformation

Returns

Definition at line 119 of file CompressedState.cpp.

◆ convertArrayReplacement()

template<typename InfoType >

ArrayVariableReplacementInformation storm::generator::convertArrayReplacement	(	typename storm::jani::ArrayEliminatorData::Replacement const &	replacement,
		InfoType const &	relevantVariableInfo
	)

Definition at line 28 of file ArrayVariableReplacementInformation.h.

◆ createCompressedState()

CompressedState storm::generator::createCompressedState	(	VariableInformation const &	varInfo,
		std::map< storm::expressions::Variable, storm::expressions::Expression > const &	stateDescription,
		bool	checkOutOfBounds
	)

Definition at line 203 of file CompressedState.cpp.

◆ createOutOfBoundsState()

CompressedState storm::generator::createOutOfBoundsState	(	VariableInformation const &	varInfo,
		bool	roundTo64Bit = `true`
	)

Parameters

varInfo
roundTo64Bit

Returns

Definition at line 196 of file CompressedState.cpp.

◆ extractVariableValues()

void storm::generator::extractVariableValues	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		std::vector< int64_t > &	locationValues,
		std::vector< bool > &	booleanValues,
		std::vector< int64_t > &	integerValues
	)

Appends the values of the given variables in the given state to the corresponding result vectors.

locationValues are inserted before integerValues (relevant if both, locationValues and integerValues actually refer to the same vector)

Parameters

state	The state
variableInformation	The variables
locationValues
booleanValues
integerValues

Definition at line 81 of file CompressedState.cpp.

◆ getBitWidthLowerUpperBound()

uint64_t storm::generator::getBitWidthLowerUpperBound	(	bool const &	hasLowerBound,
		int64_t &	lowerBound,
		bool const &	hasUpperBound,
		int64_t &	upperBound,
		uint64_t const &	reservedBitsForUnboundedVariables
	)

Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range.

Precondition: If has[Lower,Upper]Bound is true, [lower,upper]Bound must be set to the corresponding bound.

Postcondition: lowerBound and upperBound are set to the considered bound for this variable

Parameters

hasLowerBound	shall be true iff there is a lower bound given
lowerBound	a reference to the lower bound value
hasUpperBound	shall be true iff there is an upper bound given
upperBound	a reference to the upper bound
reservedBitsForUnboundedVariables	the number of bits that shall be used to represent unbounded variables

Returns: the number of bits required to represent the final variable range

Definition at line 63 of file VariableInformation.cpp.

◆ operator<<()

template<typename ValueType , typename StateType >

std::ostream & storm::generator::operator<<	(	std::ostream &	out,
		Choice< ValueType, StateType > const &	choice
	)

Definition at line 194 of file Choice.cpp.

◆ operator==() [1/4]

template<typename ValueType >

bool storm::generator::operator==	(	ObservationDenseBeliefState< ValueType > const &	lhs,
		ObservationDenseBeliefState< ValueType > const &	rhs
	)

Definition at line 229 of file NondeterministicBeliefTracker.cpp.

◆ operator==() [2/4]

template bool storm::generator::operator==	(	SparseBeliefState< double > const &	,
		SparseBeliefState< double > const &
	)

◆ operator==() [3/4]

template bool storm::generator::operator==	(	SparseBeliefState< storm::RationalNumber > const &	,
		SparseBeliefState< storm::RationalNumber > const &
	)

◆ operator==() [4/4]

template<typename ValueType >

bool storm::generator::operator==	(	SparseBeliefState< ValueType > const &	lhs,
		SparseBeliefState< ValueType > const &	rhs
	)

Definition at line 131 of file NondeterministicBeliefTracker.cpp.

◆ packStateFromValuation()

CompressedState storm::generator::packStateFromValuation	(	expressions::SimpleValuation const &	valuation,
		VariableInformation const &	variableInformation,
		bool	checkOutOfBounds
	)

Definition at line 57 of file CompressedState.cpp.

◆ toString()

std::string storm::generator::toString	(	CompressedState const &	state,
		VariableInformation const &	variableInformation
	)

Returns a (human readable) string representation of the variable valuation encoded by the given state.

Definition at line 98 of file CompressedState.cpp.

◆ unpackStateIntoEvaluator()

template<typename ValueType >

void storm::generator::unpackStateIntoEvaluator	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< ValueType > &	evaluator
	)

Unpacks the compressed state into the evaluator.

Parameters

state	The state to unpack.
variableInformation	The information about how the variables are packed within the state.
evaluator	The evaluator into which to load the state.

Definition at line 19 of file CompressedState.cpp.

◆ unpackStateIntoEvaluator< double >()

template void storm::generator::unpackStateIntoEvaluator< double >	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< double > &	evaluator
	)

◆ unpackStateIntoJson()

template<typename ValueType >

storm::json< ValueType > storm::generator::unpackStateIntoJson	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		bool	onlyObservable
	)

Template Parameters

ValueType (The ValueType does not matter for the string representation.)

Parameters

state	The state to export
variableInformation	Variable information to extract from the state
onlyObservable	Should we only export the observable information

Returns

Definition at line 164 of file CompressedState.cpp.

◆ unpackStateIntoJson< double >()

template storm::json< double > storm::generator::unpackStateIntoJson< double >	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		bool	onlyObservable
	)

◆ unpackStateIntoValuation()

storm::expressions::SimpleValuation storm::generator::unpackStateIntoValuation	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionManager const &	manager
	)

Converts the compressed state into an explicit representation in the form of a valuation.

Parameters

state	The state to unpack.
variableInformation	The information about how the variables are packed within the state.
manager	The manager responsible for the variables.

Returns: A valuation that corresponds to the compressed state.

Definition at line 37 of file CompressedState.cpp.

◆ unpackStateToObservabilityClass()

uint32_t storm::generator::unpackStateToObservabilityClass	(	CompressedState const &	state,
		storm::storage::BitVector const &	observationVector,
		std::unordered_map< storm::storage::BitVector, uint32_t > &	observabilityMap,
		storm::storage::BitVector const &	mask
	)

Parameters

state
observabilityMap
mask

Returns

Definition at line 145 of file CompressedState.cpp.

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ CompressedState

◆ NextStateGeneratorOptions

Enumeration Type Documentation

◆ ModelType

Function Documentation

◆ computeObservabilityMask()

◆ convertArrayReplacement()

◆ createCompressedState()

◆ createOutOfBoundsState()

◆ extractVariableValues()

◆ getBitWidthLowerUpperBound()

◆ operator<<()

◆ operator==() [1/4]

◆ operator==() [2/4]

◆ operator==() [3/4]

◆ operator==() [4/4]

◆ packStateFromValuation()

◆ toString()

◆ unpackStateIntoEvaluator()

◆ unpackStateIntoEvaluator< double >()

◆ unpackStateIntoJson()

◆ unpackStateIntoJson< double >()

◆ unpackStateIntoValuation()

◆ unpackStateToObservabilityClass()