This class defines which action is chosen in a particular state of a non-deterministic model. More...

#include <Scheduler.h>

Public Member Functions
	Scheduler (uint_fast64_t numberOfModelStates, boost::optional< storm::storage::MemoryStructure > const &memoryStructure=boost::none)
	Initializes a scheduler for the given number of model states.

	Scheduler (uint_fast64_t numberOfModelStates, boost::optional< storm::storage::MemoryStructure > &&memoryStructure)

void	setChoice (SchedulerChoice< ValueType > const &choice, uint_fast64_t modelState, uint_fast64_t memoryState=0)
	Sets the choice defined by the scheduler for the given state.

bool	isChoiceSelected (BitVector const &selectedStates, uint64_t memoryState=0) const
	Is the scheduler defined on the states indicated by the selected-states bitvector?

void	clearChoice (uint_fast64_t modelState, uint_fast64_t memoryState=0)
	Clears the choice defined by the scheduler for the given state.

SchedulerChoice< ValueType > const &	getChoice (uint_fast64_t modelState, uint_fast64_t memoryState=0) const
	Gets the choice defined by the scheduler for the given model and memory state.

void	setDontCare (uint_fast64_t modelState, uint_fast64_t memoryState=0, bool setArbitraryChoice=true)
	Set the combination of model state and memoryStructure state to dontCare.

void	unSetDontCare (uint_fast64_t modelState, uint_fast64_t memoryState=0)
	Unset the combination of model state and memoryStructure state to dontCare.

bool	isDontCare (uint_fast64_t modelState, uint64_t memoryState=0) const
	Is the combination of model state and memoryStructure state to reachable?

storm::storage::BitVector	computeActionSupport (std::vector< uint64_t > const &nondeterministicChoiceIndicies) const
	Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state.

bool	isPartialScheduler () const
	Retrieves whether there is a reachable pair of model and memory state for which the choice is undefined.

bool	isDeterministicScheduler () const
	Retrieves whether all defined choices are deterministic.

bool	isMemorylessScheduler () const
	Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state)

uint_fast64_t	getNumberOfMemoryStates () const
	Retrieves the number of memory states this scheduler considers.

boost::optional< storm::storage::MemoryStructure > const &	getMemoryStructure () const
	Retrieves the memory structure associated with this scheduler.

template<typename NewValueType >
Scheduler< NewValueType >	toValueType () const
	Returns a copy of this scheduler with the new value type.

void	printToStream (std::ostream &out, std::shared_ptr< storm::models::sparse::Model< ValueType > > model=nullptr, bool skipUniqueChoices=false, bool skipDontCareStates=false) const
	Prints the scheduler to the given output stream.

void	printJsonToStream (std::ostream &out, std::shared_ptr< storm::models::sparse::Model< ValueType > > model=nullptr, bool skipUniqueChoices=false, bool skipDontCareStates=false) const
	Prints the scheduler in json format to the given output stream.

Detailed Description

template<typename ValueType>
class storm::storage::Scheduler< ValueType >

This class defines which action is chosen in a particular state of a non-deterministic model.

More concretely, a scheduler maps a state s to i if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). A Choice can be undefined, deterministic

Definition at line 18 of file Scheduler.h.

Constructor & Destructor Documentation

◆ Scheduler() [1/2]

template<typename ValueType >

storm::storage::Scheduler< ValueType >::Scheduler	(	uint_fast64_t	numberOfModelStates,
		boost::optional< storm::storage::MemoryStructure > const &	memoryStructure = `boost::none`
	)

Initializes a scheduler for the given number of model states.

Parameters

numberOfModelStates	number of model states
memoryStructure	the considered memory structure. If not given, the scheduler is considered as memoryless.

Definition at line 15 of file Scheduler.cpp.

◆ Scheduler() [2/2]

template<typename ValueType >

storm::storage::Scheduler< ValueType >::Scheduler	(	uint_fast64_t	numberOfModelStates,
		boost::optional< storm::storage::MemoryStructure > &&	memoryStructure
	)

Definition at line 26 of file Scheduler.cpp.

Member Function Documentation

◆ clearChoice()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::clearChoice	(	uint_fast64_t	modelState,
		uint_fast64_t	memoryState = `0`
	)

Clears the choice defined by the scheduler for the given state.

Parameters

modelState	The state of the model for which to clear the choice.
memoryState	The state of the memoryStructure for which to clear the choice.

Definition at line 79 of file Scheduler.cpp.

◆ computeActionSupport()

template<typename ValueType >

storm::storage::BitVector storm::storage::Scheduler< ValueType >::computeActionSupport ( std::vector< uint64_t > const & nondeterministicChoiceIndicies ) const

Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state.

Definition at line 125 of file Scheduler.cpp.

◆ getChoice()

template<typename ValueType >

SchedulerChoice< ValueType > const & storm::storage::Scheduler< ValueType >::getChoice	(	uint_fast64_t	modelState,
		uint_fast64_t	memoryState = `0`
	)		const

Gets the choice defined by the scheduler for the given model and memory state.

Parameters

state	The state for which to get the choice.
memoryState	the memory state which we consider.

Definition at line 86 of file Scheduler.cpp.

◆ getMemoryStructure()

template<typename ValueType >

boost::optional< storm::storage::MemoryStructure > const & storm::storage::Scheduler< ValueType >::getMemoryStructure ( ) const

Retrieves the memory structure associated with this scheduler.

Definition at line 165 of file Scheduler.cpp.

◆ getNumberOfMemoryStates()

template<typename ValueType >

uint_fast64_t storm::storage::Scheduler< ValueType >::getNumberOfMemoryStates ( ) const

Retrieves the number of memory states this scheduler considers.

Definition at line 160 of file Scheduler.cpp.

◆ isChoiceSelected()

template<typename ValueType >

bool storm::storage::Scheduler< ValueType >::isChoiceSelected	(	BitVector const &	selectedStates,
		uint64_t	memoryState = `0`
	)		const

Is the scheduler defined on the states indicated by the selected-states bitvector?

Definition at line 68 of file Scheduler.cpp.

◆ isDeterministicScheduler()

template<typename ValueType >

bool storm::storage::Scheduler< ValueType >::isDeterministicScheduler ( ) const

Retrieves whether all defined choices are deterministic.

Definition at line 150 of file Scheduler.cpp.

◆ isDontCare()

template<typename ValueType >

bool storm::storage::Scheduler< ValueType >::isDontCare	(	uint_fast64_t	modelState,
		uint64_t	memoryState = `0`
	)		const

Is the combination of model state and memoryStructure state to reachable?

Definition at line 120 of file Scheduler.cpp.

◆ isMemorylessScheduler()

template<typename ValueType >

bool storm::storage::Scheduler< ValueType >::isMemorylessScheduler ( ) const

Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state)

Definition at line 155 of file Scheduler.cpp.

◆ isPartialScheduler()

template<typename ValueType >

bool storm::storage::Scheduler< ValueType >::isPartialScheduler ( ) const

Retrieves whether there is a reachable pair of model and memory state for which the choice is undefined.

Definition at line 145 of file Scheduler.cpp.

◆ printJsonToStream()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::printJsonToStream	(	std::ostream &	out,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	model = `nullptr`,
		bool	skipUniqueChoices = `false`,
		bool	skipDontCareStates = `false`
	)		const

Prints the scheduler in json format to the given output stream.

Parameters

out	The output stream
model	If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices). Must be passed if the scheduler is not memoryless.
skipUniqueChoices	If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. Requires a model to be given.
skipDontCareStates	If true, the choice for dontCareStates states is not printed explicitly.

Definition at line 305 of file Scheduler.cpp.

◆ printToStream()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::printToStream	(	std::ostream &	out,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	model = `nullptr`,
		bool	skipUniqueChoices = `false`,
		bool	skipDontCareStates = `false`
	)		const

Prints the scheduler to the given output stream.

Parameters

out	The output stream
model	If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices). Must be passed if the scheduler is not memoryless.
skipUniqueChoices	If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. Requires a model to be given.
skipDontCareStates	If true, the choice for dontCareStates states is not printed explicitly.

Definition at line 170 of file Scheduler.cpp.

◆ setChoice()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::setChoice	(	SchedulerChoice< ValueType > const &	choice,
		uint_fast64_t	modelState,
		uint_fast64_t	memoryState = `0`
	)

Sets the choice defined by the scheduler for the given state.

Parameters

choice	The choice to set for the given state.
modelState	The state of the model for which to set the choice.
memoryState	The state of the memoryStructure for which to set the choice.

Definition at line 37 of file Scheduler.cpp.

◆ setDontCare()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::setDontCare	(	uint_fast64_t	modelState,
		uint_fast64_t	memoryState = `0`,
		bool	setArbitraryChoice = `true`
	)

Set the combination of model state and memoryStructure state to dontCare.

These states are considered unreachable and are ignored when printing the scheduler. If not specified otherwise, an arbitrary choice is set if no choice exists.

Parameters

modelState	The state of the model.
memoryState	The state of the memoryStructure.
memoryState	A flag indicating whether to set an arbitrary choice.

Definition at line 93 of file Scheduler.cpp.

◆ toValueType()

template<typename ValueType >

template<typename NewValueType >

Scheduler< NewValueType > storm::storage::Scheduler< ValueType >::toValueType ( ) const

inline

Returns a copy of this scheduler with the new value type.

Definition at line 117 of file Scheduler.h.

◆ unSetDontCare()

template<typename ValueType >

void storm::storage::Scheduler< ValueType >::unSetDontCare	(	uint_fast64_t	modelState,
		uint_fast64_t	memoryState = `0`
	)

Unset the combination of model state and memoryStructure state to dontCare.

Parameters

modelState	The state of the model.
memoryState	The state of the memoryStructure.

Definition at line 109 of file Scheduler.cpp.

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

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h
src/storm/storage/Scheduler.h
src/storm/storage/Scheduler.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Scheduler() [1/2]

◆ Scheduler() [2/2]

Member Function Documentation

◆ clearChoice()

◆ computeActionSupport()

◆ getChoice()

◆ getMemoryStructure()

◆ getNumberOfMemoryStates()

◆ isChoiceSelected()

◆ isDeterministicScheduler()

◆ isDontCare()

◆ isMemorylessScheduler()

◆ isPartialScheduler()

◆ printJsonToStream()

◆ printToStream()

◆ setChoice()

◆ setDontCare()

◆ toValueType()

◆ unSetDontCare()