Classes
class	TransitionInfo

struct	TransitionInfoComparison

Public Types
typedef threads::ControlThread< StateType, RewardModelType, ValueType >::StateAndThreadIndex	StateThreadIndex

Public Member Functions
	StaminaModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > 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, 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)

virtual StateType	getOrAddStateIndex (CompressedState const &state)

StateType	getStateIndexOrAbsorbing (CompressedState const &state)

double	getLocalKappa ()

Protected Member Functions
storm::storage::sparse::StateStorage< StateType >	getStateStorage ()

void	loadPropertyExpressionFromFormula ()

void	connectTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, CompressedState &terminalState, StateType stateId, std::function< StateType(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 (StateType from, StateType to, ValueType probability)

void	createTransition (TransitionInfo transitionInfo)

virtual storm::storage::sparse::ModelComponents< ValueType, RewardModelType >	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::shared_ptr< threads::ControlThread< StateType, RewardModelType, ValueType > >	controlThread

std::vector< std::shared_ptr< threads::ExplorationThread< StateType, RewardModelType, ValueType > > >	explorationThreads

std::function< StateType(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, StateType > >	generator

util::StateMemoryPool< ProbabilityState< StateType > >	memoryPool

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

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

storm::storage::sparse::StateStorage< StateType > &	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< StateType > *	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

◆ StaminaModelBuilder() [1/2]

template<typename ValueType , typename RewardModelType , typename StateType >

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

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 >

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

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 stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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 > > stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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 = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>

virtual void stamina::builder::StaminaModelBuilder< 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
	)

protectedpure virtual

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

Implemented in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaThreadedIterativeModelBuilder< ValueType, RewardModelType, StateType >, and stamina::builder::StaminaThreadedPriorityModelBuilder< ValueType, RewardModelType, StateType >.

◆ buildModelComponents()

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

virtual storm::storage::sparse::ModelComponents< ValueType, RewardModelType > stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::buildModelComponents ( )

protectedpure virtual

Explores state space and truncates the model

Returns: The components of the truncated model

Implemented in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, and stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >.

◆ buildStateLabeling()

template<typename ValueType , typename RewardModelType , typename StateType >

storm::models::sparse::StateLabeling stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::buildStateLabeling

protected

Builds state labeling for our program

Returns: State labeling for our program

◆ connectTerminalStatesToAbsorbing()

template<typename ValueType , typename RewardModelType , typename StateType >

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

◆ createTransition()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::createTransition	(	StateType	from,
		StateType	to,
		ValueType	probability
	)

protected

Inserts a TransitionInfo into transitionsToAdd. This method must NOT be called after flushToTransitionMatrix has cleared transitionsToAdd

◆ flushToTransitionMatrix()

template<typename ValueType , typename RewardModelType , typename StateType >

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

protected

Flushes the elements in transitionsToAdd into the transition matrix

Parameters

transitionMatrixBuilder The transition matrix builder

◆ getOrAddStateIndex()

template<typename ValueType , typename RewardModelType , typename StateType >

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

virtual

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 in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, and stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >.

◆ getPerimeterStates()

template<typename ValueType , typename RewardModelType , typename StateType >

std::vector< StateType > stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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::builder::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 stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::getStateIndexOrAbsorbing ( CompressedState const & state )

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 stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::loadPropertyExpressionFromFormula

protected

Creates and loads the property expression from the formula

◆ reset()

template<typename ValueType , typename RewardModelType , typename StateType >

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

Resets stuff to "fresh" state.

◆ setGenerator()

template<typename ValueType , typename RewardModelType , typename StateType >

void stamina::builder::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::builder::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 stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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 stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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/builder/StaminaModelBuilder.h
/home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/StaminaModelBuilder.cpp

Classes

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Constructor & Destructor Documentation

◆ StaminaModelBuilder() [1/2]

◆ StaminaModelBuilder() [2/2]

Member Function Documentation

◆ accumulateProbabilities()

◆ build()

◆ buildMatrices()

◆ buildModelComponents()

◆ buildStateLabeling()

◆ connectTerminalStatesToAbsorbing()

◆ createTransition()

◆ flushToTransitionMatrix()

◆ getOrAddStateIndex()

◆ getPerimeterStates()

◆ getStateIndexIfKnown()

◆ getStateIndexOrAbsorbing()

◆ loadPropertyExpressionFromFormula()

◆ reset()

◆ setGenerator()

◆ setLocalKappaToGlobal()

◆ setPropertyFormula()

◆ setUpAbsorbingState()