Classes
class	ProbabilityState

struct	ProbabilityStateComparison

Public Member Functions
	StaminaModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &generator)

	StaminaModelBuilder (storm::prism::Program const &program, storm::generator::NextStateGeneratorOptions const &generatorOptions=storm::generator::NextStateGeneratorOptions())

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	build ()

StateType	getStateIndexIfKnown (CompressedState const &state)

double	accumulateProbabilities ()

void	reset ()

void	setGenerator (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > generator)

std::vector< StateType >	getPerimeterStates ()

void	setLocalKappaToGlobal ()

void	printStateSpaceInformation ()

storm::expressions::Expression *	getPropertyExpression ()

void	setPropertyFormula (std::shared_ptr< const storm::logic::Formula > formula, const storm::prism::Program &modulesFile)

Protected Member Functions
void	loadPropertyExpressionFromFormula ()

StateType	getOrAddStateIndex (CompressedState const &state)

StateType	getStateIndexOrAbsorbing (CompressedState const &state)

void	connectTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, CompressedState terminalState, StateType stateId, std::function< StateType(CompressedState const &)> stateToIdCallback)

void	buildMatrices (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, std::vector< RewardModelBuilder< typename RewardModelType::ValueType > > &rewardModelBuilders, StateAndChoiceInformationBuilder &choiceInformationBuilder, boost::optional< storm::storage::BitVector > &markovianChoices, boost::optional< storm::storage::sparse::StateValuationsBuilder > &stateValuationsBuilder)

storm::storage::sparse::ModelComponents< ValueType, RewardModelType >	buildModelComponents ()

storm::models::sparse::StateLabeling	buildStateLabeling ()

void	setUpAbsorbingState (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, std::vector< RewardModelBuilder< typename RewardModelType::ValueType > > &rewardModelBuilders, StateAndChoiceInformationBuilder &choiceInformationBuilder, boost::optional< storm::storage::BitVector > &markovianChoices, boost::optional< storm::storage::sparse::StateValuationsBuilder > &stateValuationsBuilder)

Constructor & Destructor Documentation

◆ StaminaModelBuilder() [1/2]

template<typename ValueType , typename RewardModelType , typename StateType >

StaminaModelBuilder::StaminaModelBuilder ( std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const & generator )

Constructs a StaminaModelBuilder with a given storm::generator::PrismNextStateGenerator

Parameters

generator The generator we are going to use.

◆ StaminaModelBuilder() [2/2]

template<typename ValueType , typename RewardModelType , typename StateType >

StaminaModelBuilder::StaminaModelBuilder	(	storm::prism::Program const &	program,
		storm::generator::NextStateGeneratorOptions const &	generatorOptions = `storm::generator::NextStateGeneratorOptions()`
	)

Constructs a StaminaModelBuilder with a PRISM program and generatorOptions

Parameters

program	The PRISM program we are going to use to build the model with.
generatorOptions	Options for the storm::generator::PrismNextStateGenerator we are going to use.

Member Function Documentation

◆ accumulateProbabilities()

template<typename ValueType , typename RewardModelType , typename StateType >

double StaminaModelBuilder::accumulateProbabilities

Accumulates all probabilities in T Map and returns

◆ build()

template<typename ValueType , typename RewardModelType , typename StateType >

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > StaminaModelBuilder::build

Creates a model with a truncated state space for the program provided during construction. State space is truncated during this method using the STAMINA II truncation method described by Riley Roberts and Zhen Zhang, and corresponding to the same algorithm used in the Java version of STAMINA.

Returns: The truncated model.

◆ buildMatrices()

template<typename ValueType , typename RewardModelType , typename StateType >

void StaminaModelBuilder::buildMatrices	(	storm::storage::SparseMatrixBuilder< ValueType > &	transitionMatrixBuilder,
		std::vector< RewardModelBuilder< typename RewardModelType::ValueType > > &	rewardModelBuilders,
		StateAndChoiceInformationBuilder &	choiceInformationBuilder,
		boost::optional< storm::storage::BitVector > &	markovianChoices,
		boost::optional< storm::storage::sparse::StateValuationsBuilder > &	stateValuationsBuilder
	)

protected

Builds transition matrix of truncated state space for the given program.

Parameters

transitionMatrixBuilder	The builder of the transition matrix.
rewardModelBuilders	The builders for the selected reward models.
choiceInformationBuilder	The builder for the requested information of the choices
markovianChoices	is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
stateValuationsBuilder	if not boost::none, we insert valuations for the corresponding states

◆ buildModelComponents()

template<typename ValueType , typename RewardModelType , typename StateType >

storm::storage::sparse::ModelComponents< ValueType, RewardModelType > StaminaModelBuilder::buildModelComponents

protected

Explores state space and truncates the model

Returns: The components of the truncated model

◆ buildStateLabeling()

template<typename ValueType , typename RewardModelType , typename StateType >

storm::models::sparse::StateLabeling StaminaModelBuilder::buildStateLabeling

protected

Builds state labeling for our program

Returns: State labeling for our program

◆ connectTerminalStatesToAbsorbing()

template<typename ValueType , typename RewardModelType , typename StateType >

void StaminaModelBuilder::connectTerminalStatesToAbsorbing	(	storm::storage::SparseMatrixBuilder< ValueType > &	transitionMatrixBuilder,
		CompressedState	terminalState,
		StateType	stateId,
		std::function< StateType(CompressedState const &)>	stateToIdCallback
	)

protected

Connects all terminal states to the absorbing state

◆ getOrAddStateIndex()

template<typename ValueType , typename RewardModelType , typename StateType >

StateType StaminaModelBuilder::getOrAddStateIndex ( CompressedState const & state )

protected

Gets the state ID of a current state, or adds it to the internal state storage. Performs state exploration and state space truncation from that state.

Parameters

state Pointer to the state we are looking it

Returns: A pair with the state id and whether or not it was already discovered

◆ getPerimeterStates()

template<typename ValueType , typename RewardModelType , typename StateType >

std::vector< StateType > StaminaModelBuilder::getPerimeterStates

Creates and returns a vector of all perimeter states

Returns: a vector of all perimeter states

◆ getStateIndexIfKnown()

template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>

StateType stamina::StaminaModelBuilder< ValueType, RewardModelType, StateType >::getStateIndexIfKnown ( CompressedState const & state )

Gets the state ID of a state known to already exist. This does NOT perform state-space truncation for future states

◆ getStateIndexOrAbsorbing()

template<typename ValueType , typename RewardModelType , typename StateType >

StateType StaminaModelBuilder::getStateIndexOrAbsorbing ( CompressedState const & state )

protected

Alterate state ID grabber. Returns state ID if exists. If it does not, returns the absorbing state This is used as an alternative callback function for terminal (perimeter) states

◆ loadPropertyExpressionFromFormula()

template<typename ValueType , typename RewardModelType , typename StateType >

void StaminaModelBuilder::loadPropertyExpressionFromFormula

protected

Creates and loads the property expression from the formula

◆ reset()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::StaminaModelBuilder< ValueType, RewardModelType, StateType >::reset

Resets stuff to "fresh" state.

◆ setGenerator()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::StaminaModelBuilder< ValueType, RewardModelType, StateType >::setGenerator ( std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > generator )

Sets the generator while deleting the old one

Parameters

generator The new generator

◆ setLocalKappaToGlobal()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::StaminaModelBuilder< ValueType, RewardModelType, StateType >::setLocalKappaToGlobal

Sets the value of κ in Options to what we have stored locally here

◆ setPropertyFormula()

template<typename ValueType , typename RewardModelType , typename StateType >

void StaminaModelBuilder::setPropertyFormula	(	std::shared_ptr< const storm::logic::Formula >	formula,
		const storm::prism::Program &	modulesFile
	)

Sets the property formula for state space truncation optimization. Does not load or create an expression from the formula.

Parameters

formula	The formula to set
modulesFile	The modules file which contains the expressionmanager

◆ setUpAbsorbingState()

template<typename ValueType , typename RewardModelType , typename StateType >

void StaminaModelBuilder::setUpAbsorbingState	(	storm::storage::SparseMatrixBuilder< ValueType > &	transitionMatrixBuilder,
		std::vector< RewardModelBuilder< typename RewardModelType::ValueType > > &	rewardModelBuilders,
		StateAndChoiceInformationBuilder &	choiceInformationBuilder,
		boost::optional< storm::storage::BitVector > &	markovianChoices,
		boost::optional< storm::storage::sparse::StateValuationsBuilder > &	stateValuationsBuilder
	)

protected

Sets up the initial state in the transition matrix

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

/home/josh/Documents/Work/stamina-cplusplus/src/stamina/StaminaModelBuilder.h
/home/josh/Documents/Work/stamina-cplusplus/src/stamina/StaminaModelBuilder.cpp

Classes

Public Member Functions

Protected Member Functions

Constructor & Destructor Documentation

◆ StaminaModelBuilder() [1/2]

◆ StaminaModelBuilder() [2/2]

Member Function Documentation

◆ accumulateProbabilities()

◆ build()

◆ buildMatrices()

◆ buildModelComponents()

◆ buildStateLabeling()

◆ connectTerminalStatesToAbsorbing()

◆ getOrAddStateIndex()

◆ getPerimeterStates()

◆ getStateIndexIfKnown()

◆ getStateIndexOrAbsorbing()

◆ loadPropertyExpressionFromFormula()

◆ reset()

◆ setGenerator()

◆ setLocalKappaToGlobal()

◆ setPropertyFormula()

◆ setUpAbsorbingState()