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

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

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

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

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

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

uint32_t	getOrAddStateIndex (CompressedState const &state) override

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

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

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 ()

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

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 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

Constructor & Destructor Documentation

◆ StaminaThreadedPriorityModelBuilder() [1/2]

template<typename ValueType , typename RewardModelType , typename StateType >

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

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

Parameters

generator The generator we are going to use.

◆ StaminaThreadedPriorityModelBuilder() [2/2]

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

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

Constructs a StaminaThreadedPriorityModelBuilder 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 = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>

void stamina::builder::StaminaThreadedPriorityModelBuilder< 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 >.

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

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

Public Member Functions

Additional Inherited Members

Constructor & Destructor Documentation

◆ StaminaThreadedPriorityModelBuilder() [1/2]

◆ StaminaThreadedPriorityModelBuilder() [2/2]

Member Function Documentation

◆ buildMatrices()