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

Public Member Functions
	ExplorationThread (StaminaModelBuilder< ValueType, RewardModelType, StateType > parent, uint8_t threadIndex, ControlThread< StateType, RewardModelType, ValueType > &controlThread, uint32_t stateSize, util::StateIndexArray< StateType, ProbabilityState< StateType > > stateMap, std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &generator, std::function< StateType(CompressedState const &)> stateToIdCallback)

uint8_t	getIndex ()

uint32_t	getNumberOfOwnedStates ()

bool	isIdling ()

void	setIsCtmc (bool isCtmc)

void	requestCrossExploration (CompressedState &state, double deltaPi)

void	requestCrossExploration (StateType stateIndex, double deltaPi)

virtual void	mainLoop () override

Public Member Functions inherited from stamina::builder::threads::BaseThread< StateType, RewardModelType, ValueType >
	BaseThread (StaminaModelBuilder< ValueType, RewardModelType, StateType > *parent)

virtual void	mainLoop ()=0

void	startThread ()

const StaminaModelBuilder< ValueType, RewardModelType, StateType > *	getParent ()

void	join ()

void	terminate ()

Protected Member Functions
virtual void	exploreStates ()=0

virtual void	exploreState (StateAndProbability &stateProbability)=0

virtual void	enqueueSuccessors (CompressedState &state)=0

Protected Attributes
std::shared_mutex	crossExplorationQueueMutex

std::deque< std::pair< CompressedState, double > >	crossExplorationQueue

std::deque< StateAndProbability >	mainExplorationQueue

uint32_t	numberOfOwnedStates

bool	idling

ControlThread< StateType, RewardModelType, ValueType > &	controlThread

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

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

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

std::deque< StateAndProbability >	statesTerminatedLastIteration

std::function< StateType(CompressedState const &)>	stateToIdCallback

std::deque< StateIndexAndThread >	statesToRequestCrossExploration

Protected Attributes inherited from stamina::builder::threads::BaseThread< StateType, RewardModelType, ValueType >
bool	finished

Constructor & Destructor Documentation

◆ ExplorationThread()

template<typename StateType , typename RewardModelType , typename ValueType >

stamina::builder::threads::ExplorationThread< StateType, RewardModelType, ValueType >::ExplorationThread	(	StaminaModelBuilder< ValueType, RewardModelType, StateType > *	parent,
		uint8_t	threadIndex,
		ControlThread< StateType, RewardModelType, ValueType > &	controlThread,
		uint32_t	stateSize,
		util::StateIndexArray< StateType, ProbabilityState< StateType > > *	stateMap,
		std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &	generator,
		std::function< StateType(CompressedState const &)>	stateToIdCallback
	)

Constructor. Invokes super's constructor and stores the thread index which cannot change for the life of the thread

Parameters

parent	The model builder who owns this thread
threadIndex	The index of this thread
stateSize	The size of the states
stateMap	Access to the parent class's stateMap

template<typename StateType , typename RewardModelType , typename ValueType >

void stamina::builder::threads::ExplorationThread< StateType, RewardModelType, ValueType >::mainLoop

overridevirtual

Does state exploration or idles until worker thread asks to kill it.

template<typename StateType , typename RewardModelType , typename ValueType >

void stamina::builder::threads::ExplorationThread< StateType, RewardModelType, ValueType >::requestCrossExploration	(	CompressedState &	state,
		double	deltaPi
	)

A function called by other threads to request cross exploration of states already explored but encountered by another thread.

Parameters

state	The state to cross explore.
deltaPi	The difference in reachability to add to that state and push forward to its successors.

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

/home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/threads/ControlThread.h
/home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/threads/ExplorationThread.h
/home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/threads/ExplorationThread.cpp