Namespaces
namespace	detail

Classes
class	BeliefSupportTracker
class	MonitorVerifier
class	GenerateMonitorVerifier
class	BeliefStateManager
	This class keeps track of common information of a set of beliefs. More...
class	SparseBeliefState
	SparseBeliefState stores beliefs in a sparse format. More...
class	NondeterministicBeliefTracker
	This tracker implements state estimation for POMDPs. More...
class	ArrayVariableReplacementInformation
struct	Choice
class	Distribution
class	DistributionEntry
struct	JaniNextStateGeneratorScratchMemory
	The actual (private) implementation of JaniNextStateGeneratorScratchMemory, see the corresponding member in JaniNextStateGenerator.h. More...
class	JaniNextStateGenerator
class	NextStateGenerator
class	ActionMask
	Action masks are arguments you can give to the state generator that limit which states are generated. More...
class	StateValuationFunctionMask
	A particular instance of the action mask that uses a callback function to evaluate whether an action should be expanded. More...
struct	ActiveCommandData
class	PrismNextStateGenerator
class	StateBehavior
struct	TransientVariableInformation
struct	TransientVariableData
struct	TransientVariableValuation
struct	BooleanVariableInformation
struct	IntegerVariableInformation
struct	LocationVariableInformation
struct	ObservationLabelInformation
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 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.
template<typename ValueType>
void	unpackStateDifferenceIntoEvaluator (CompressedState const &newState, CompressedState const &oldState, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< ValueType > &evaluator)
	Updates the (non-transient) variable values in the given evaluator from the values of oldState to the values of newState.
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	unpackStateAppendToValuations (CompressedState const &state, VariableInformation const &variableInformation, storm::storage::sparse::ValuationsStorage &valuations)
	Appends the values of the variables in the given state to the valuations object.
void	unpackObservationClassIntoValuations (CompressedState const &observationClass, uint64_t const observationClassIndex, VariableInformation const &variableInformation, storm::storage::sparse::ValuationsStorage &valuations)
	Sets the values of observable variables and observation expressions to the given observationClassIndex of the given valuations.
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)
template storm::json< storm::RationalNumber >	unpackStateIntoJson< storm::RationalNumber > (CompressedState const &state, VariableInformation const &variableInformation, bool onlyObservable)
template storm::json< storm::RationalFunction >	unpackStateIntoJson< storm::RationalFunction > (CompressedState const &state, VariableInformation const &variableInformation, bool onlyObservable)
template void	unpackStateIntoEvaluator< storm::RationalNumber > (CompressedState const &state, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< storm::RationalNumber > &evaluator)
template void	unpackStateIntoEvaluator< storm::RationalFunction > (CompressedState const &state, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< storm::RationalFunction > &evaluator)
template void	unpackStateDifferenceIntoEvaluator< double > (CompressedState const &newState, CompressedState const &oldState, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< double > &evaluator)
template void	unpackStateDifferenceIntoEvaluator< storm::RationalNumber > (CompressedState const &newState, CompressedState const &oldState, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< storm::RationalNumber > &evaluator)
template void	unpackStateDifferenceIntoEvaluator< storm::RationalFunction > (CompressedState const &newState, CompressedState const &oldState, VariableInformation const &variableInformation, storm::expressions::ExpressionEvaluator< storm::RationalFunction > &evaluator)
template<typename ValueType, typename BaseValueType>
ValueType	evaluateLikelihoodExpression (storm::prism::Update const &update, storm::expressions::ExpressionEvaluator< BaseValueType > const &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 23 of file CompressedState.h.

◆ NextStateGeneratorOptions

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

Definition at line 25 of file NextStateGenerator.h.

Enumeration Type Documentation

◆ ModelType

enum class storm::generator::ModelType

strong

Enumerator
DTMC
CTMC
MDP
MA
POMDP
SMG

Definition at line 27 of file NextStateGenerator.h.

Function Documentation

◆ computeObservabilityMask()

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

Parameters

variableInformation

Returns

Definition at line 241 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 322 of file CompressedState.cpp.

◆ createOutOfBoundsState()

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

Parameters

varInfo
roundTo64Bit

Returns

Definition at line 315 of file CompressedState.cpp.

◆ evaluateLikelihoodExpression()

template<typename ValueType, typename BaseValueType>

ValueType storm::generator::evaluateLikelihoodExpression	(	storm::prism::Update const &	update,
		storm::expressions::ExpressionEvaluator< BaseValueType > const &	evaluator )

Definition at line 585 of file PrismNextStateGenerator.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 64 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 212 of file Choice.cpp.

◆ operator==() [1/3]

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

◆ operator==() [2/3]

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

◆ operator==() [3/3]

template<typename ValueType>

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

Definition at line 132 of file NondeterministicBeliefTracker.cpp.

◆ packStateFromValuation()

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

Definition at line 134 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 220 of file CompressedState.cpp.

◆ unpackObservationClassIntoValuations()

void storm::generator::unpackObservationClassIntoValuations	(	CompressedState const &	observationClass,
		uint64_t const	observationClassIndex,
		VariableInformation const &	variableInformation,
		storm::storage::sparse::ValuationsStorage &	valuations )

Sets the values of observable variables and observation expressions to the given observationClassIndex of the given valuations.

Definition at line 215 of file CompressedState.cpp.

◆ unpackStateAppendToValuations()

void storm::generator::unpackStateAppendToValuations	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		storm::storage::sparse::ValuationsStorage &	valuations )

Appends the values of the variables in the given state to the valuations object.

Assumes that the order of variables in the variableInformation and valuations objects are aligned.

Parameters

state	The state.
variableInformation	The variables.
valuations	the valuations to which the variable values should be appended.

Definition at line 209 of file CompressedState.cpp.

◆ unpackStateDifferenceIntoEvaluator()

template<typename ValueType>

void storm::generator::unpackStateDifferenceIntoEvaluator	(	CompressedState const &	newState,
		CompressedState const &	oldState,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< ValueType > &	evaluator )

Updates the (non-transient) variable values in the given evaluator from the values of oldState to the values of newState.

Only the values of variables that differ between the two states are written to the evaluator.

Precondition: The evaluator currently holds the variable values of oldState (e.g., due to a previous call of unpackStateIntoEvaluator(oldState, ...)).

Parameters

newState	The state to unpack.
oldState	The state that is currently loaded into the evaluator.
variableInformation	The information about how the variables are packed within the states.
evaluator	The evaluator into which to load the state.

Definition at line 68 of file CompressedState.cpp.

◆ unpackStateDifferenceIntoEvaluator< double >()

template void storm::generator::unpackStateDifferenceIntoEvaluator< double >	(	CompressedState const &	newState,
		CompressedState const &	oldState,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< double > &	evaluator )

◆ unpackStateDifferenceIntoEvaluator< storm::RationalFunction >()

template void storm::generator::unpackStateDifferenceIntoEvaluator< storm::RationalFunction >	(	CompressedState const &	newState,
		CompressedState const &	oldState,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< storm::RationalFunction > &	evaluator )

◆ unpackStateDifferenceIntoEvaluator< storm::RationalNumber >()

template void storm::generator::unpackStateDifferenceIntoEvaluator< storm::RationalNumber >	(	CompressedState const &	newState,
		CompressedState const &	oldState,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< storm::RationalNumber > &	evaluator )

◆ 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 22 of file CompressedState.cpp.

◆ unpackStateIntoEvaluator< double >()

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

◆ unpackStateIntoEvaluator< storm::RationalFunction >()

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

◆ unpackStateIntoEvaluator< storm::RationalNumber >()

template void storm::generator::unpackStateIntoEvaluator< storm::RationalNumber >	(	CompressedState const &	state,
		VariableInformation const &	variableInformation,
		storm::expressions::ExpressionEvaluator< storm::RationalNumber > &	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 286 of file CompressedState.cpp.

◆ unpackStateIntoJson< double >()

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

◆ unpackStateIntoJson< storm::RationalFunction >()

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

◆ unpackStateIntoJson< storm::RationalNumber >()

template storm::json< storm::RationalNumber > storm::generator::unpackStateIntoJson< storm::RationalNumber >	(	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 114 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 267 of file CompressedState.cpp.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ CompressedState

◆ NextStateGeneratorOptions

Enumeration Type Documentation

◆ ModelType

Function Documentation

◆ computeObservabilityMask()

◆ convertArrayReplacement()

◆ createCompressedState()

◆ createOutOfBoundsState()

◆ evaluateLikelihoodExpression()

◆ getBitWidthLowerUpperBound()

◆ operator<<()

◆ operator==() [1/3]

◆ operator==() [2/3]

◆ operator==() [3/3]

◆ packStateFromValuation()

◆ toString()

◆ unpackObservationClassIntoValuations()

◆ unpackStateAppendToValuations()

◆ unpackStateDifferenceIntoEvaluator()

◆ unpackStateDifferenceIntoEvaluator< double >()

◆ unpackStateDifferenceIntoEvaluator< storm::RationalFunction >()

◆ unpackStateDifferenceIntoEvaluator< storm::RationalNumber >()

◆ unpackStateIntoEvaluator()

◆ unpackStateIntoEvaluator< double >()

◆ unpackStateIntoEvaluator< storm::RationalFunction >()

◆ unpackStateIntoEvaluator< storm::RationalNumber >()

◆ unpackStateIntoJson()

◆ unpackStateIntoJson< double >()

◆ unpackStateIntoJson< storm::RationalFunction >()

◆ unpackStateIntoJson< storm::RationalNumber >()

◆ unpackStateIntoValuation()

◆ unpackStateToObservabilityClass()