Inheritance diagram for stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >:

Public Member Functions
	StaminaIterativeModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &generator, storm::prism::Program const &modulesFile, storm::generator::NextStateGeneratorOptions const &options)

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

virtual 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) override

StateType	getOrAddStateIndex (CompressedState const &state) override

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

Public Member Functions inherited from stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >
	StaminaModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, uint32_t > > const &generator, storm::prism::Program const &modulesFile, storm::generator::NextStateGeneratorOptions const &options)

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

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

uint32_t	getStateIndexIfKnown (CompressedState const &state)

double	accumulateProbabilities ()

void	reset ()

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

std::vector< uint32_t >	getPerimeterStates ()

void	setLocalKappaToGlobal ()

void	printStateSpaceInformation ()

storm::expressions::Expression *	getPropertyExpression ()

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

virtual uint32_t	getOrAddStateIndex (CompressedState const &state)

uint32_t	getStateIndexOrAbsorbing (CompressedState const &state)

double	getLocalKappa ()

Protected Member Functions
void	flushStatesTerminated ()

void	connectAllTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder)

Protected Member Functions inherited from stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >
storm::storage::sparse::StateStorage< uint32_t >	getStateStorage ()

void	loadPropertyExpressionFromFormula ()

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

virtual 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)=0

void	flushToTransitionMatrix (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder)

void	createTransition (uint32_t from, uint32_t to, ValueType probability)

void	createTransition (TransitionInfo transitionInfo)

virtual storm::storage::sparse::ModelComponents< ValueType, storm::models::sparse::StandardRewardModel< ValueType > >	buildModelComponents ()=0

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)

Protected Attributes
std::deque< std::pair< ProbabilityState< StateType > *, CompressedState > >	statesTerminatedLastIteration

uint64_t	numberOfExploredStates

uint64_t	numberOfExploredStatesSinceLastMessage

Protected Attributes inherited from stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >
std::shared_ptr< threads::ControlThread< uint32_t, storm::models::sparse::StandardRewardModel< ValueType >, ValueType > >	controlThread

std::vector< std::shared_ptr< threads::ExplorationThread< uint32_t, storm::models::sparse::StandardRewardModel< ValueType >, ValueType > > >	explorationThreads

std::function< uint32_t(CompressedState const &)>	terminalStateToIdCallback

storm::expressions::Expression *	propertyExpression

storm::expressions::ExpressionManager *	expressionManager

std::shared_ptr< const storm::logic::Formula >	propertyFormula

std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, uint32_t > >	generator

util::StateMemoryPool< ProbabilityState< uint32_t > >	memoryPool

std::deque< std::pair< ProbabilityState< uint32_t > *, CompressedState > >	statesToExplore

util::StateIndexArray< uint32_t, ProbabilityState< uint32_t > >	stateMap

storm::storage::sparse::StateStorage< uint32_t > &	stateStorage

boost::optional< std::vector< uint_fast64_t > >	stateRemapping

std::vector< std::vector< TransitionInfo > >	transitionsToAdd

storm::generator::NextStateGeneratorOptions const &	options

storm::prism::Program const &	modulesFile

ProbabilityState< uint32_t > *	currentProbabilityState

CompressedState	absorbingState

bool	absorbingWasSetUp

bool	isInit

bool	fresh

uint8_t	iteration

bool	firstIteration

double	localKappa

bool	isCtmc

bool	formulaMatchesExpression

uint64_t	numberTerminal

uint64_t	numberStates

uint64_t	numberTransitions

uint_fast64_t	currentRowGroup

uint_fast64_t	currentRow

Additional Inherited Members
Public Types inherited from stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >
typedef threads::ControlThread< uint32_t, storm::models::sparse::StandardRewardModel< ValueType >, ValueType >::StateAndThreadIndex	StateThreadIndex

Constructor & Destructor Documentation

◆ StaminaIterativeModelBuilder() [1/2]

template<typename ValueType , typename RewardModelType , typename StateType >

stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::StaminaIterativeModelBuilder	(	std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &	generator,
		storm::prism::Program const &	modulesFile,
		storm::generator::NextStateGeneratorOptions const &	options
	)

Constructs a StaminaIterativeModelBuilder with a given storm::generator::PrismNextStateGenerator. Invokes super's constructor

Parameters

generator The generator we are going to use.

◆ StaminaIterativeModelBuilder() [2/2]

template<typename ValueType , typename RewardModelType , typename StateType >

stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::StaminaIterativeModelBuilder	(	storm::prism::Program const &	program,
		storm::generator::NextStateGeneratorOptions const &	generatorOptions = `storm::generator::NextStateGeneratorOptions()`
	)

Constructs a StaminaIterativeModelBuilder with a PRISM program and generatorOptions. Invokes super's constructor

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

◆ buildMatrices()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::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
	)

overridevirtual

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

Implements stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >.

Reimplemented in stamina::builder::StaminaThreadedIterativeModelBuilder< ValueType, RewardModelType, StateType >.

◆ buildModelComponents()

template<typename ValueType , typename RewardModelType , typename StateType >

storm::storage::sparse::ModelComponents< ValueType, RewardModelType > stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::buildModelComponents

overridevirtual

Explores state space and truncates the model

Returns: The components of the truncated model

Implements stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >.

◆ connectAllTerminalStatesToAbsorbing()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::connectAllTerminalStatesToAbsorbing ( storm::storage::SparseMatrixBuilder< ValueType > & transitionMatrixBuilder )

protected

Connects all states which are terminal

◆ flushStatesTerminated()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::flushStatesTerminated

protected

Flushes the states terminated into statesToExplore

◆ getOrAddStateIndex()

template<typename ValueType , typename RewardModelType , typename StateType >

StateType stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::getOrAddStateIndex ( CompressedState const & state )

overridevirtual

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

Reimplemented from stamina::builder::StaminaModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ StaminaIterativeModelBuilder() [1/2]

◆ StaminaIterativeModelBuilder() [2/2]

Member Function Documentation

◆ buildMatrices()

◆ buildModelComponents()

◆ connectAllTerminalStatesToAbsorbing()

◆ flushStatesTerminated()

◆ getOrAddStateIndex()