storm::bisimulation::detail Namespace Reference

Classes
struct	SignatureRefinementContext
struct	SplitterRefinementContext

Functions
template<typename ValueType>
storm::storage::BitVector	computeDivergentStates (storm::storage::SparseMatrix< ValueType > const &transitions, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, Partition const &partition)
	Computes the states from which no state outside of their own block can be reached.
template<typename ValueType>
storm::storage::BitVector	computeSilentStates (storm::storage::SparseMatrix< ValueType > const &transitions, Partition const &partition)
	Computes the states all of whose transitions stay within their own block.
template<typename ValueType, SignatureMode SignatureMode>
void	refinePartitionBasedOnSignature (SignatureRefinementContext< ValueType, SignatureMode > &context, storm::bisimulation::Partition::Block const pivotBlock, bool const enforcePredecessorExploration)
template<typename ValueType, SplitterRefinementMode Mode> requires (Mode != SplitterRefinementMode::Strong)
void	recomputeSilentStates (SplitterRefinementContext< ValueType, Mode > &context, auto const &candidates)
	Recomputes whether the given candidate states are silent.
template<typename ValueType, SplitterRefinementMode Mode> requires (Mode != SplitterRefinementMode::Strong)
bool	checkSilentStates (SplitterRefinementContext< ValueType, Mode > const &context)
	Checks that the recorded silent states match the current partition.
template<typename ValueType, SplitterRefinementMode Mode>
void	enqueueSubBlocks (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const splitBlock)
	Replaces the given block, which has just been split, by its sub-blocks in the queue of splitters.
template<typename ValueType, SplitterRefinementMode Mode>
void	refineBlockStrong (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const predecessorBlockToSplit)
	Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter.
template<typename ValueType>
void	refineBlockWeak (SplitterRefinementContext< ValueType, SplitterRefinementMode::WeakDiscreteTime > &context, storm::bisimulation::Partition::Block const block, storm::bisimulation::Partition::Block const splitterBlock)
	Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter, conditioned on leaving the own block.
template<typename ValueType, SplitterRefinementMode Mode>
void	refinePartitionBasedOnSplitter (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const splitterBlock)

Function Documentation

checkSilentStates()

template<typename ValueType, SplitterRefinementMode Mode>
requires (Mode != SplitterRefinementMode::Strong)

bool storm::bisimulation::detail::checkSilentStates

(

SplitterRefinementContext< ValueType, Mode > const &

context

)

Checks that the recorded silent states match the current partition.

Useful for sanity checks (e.g. via assertions). Does not assert itself.

Definition at line 103 of file SplitterBasedRefinement.cpp.

computeDivergentStates()

template<typename ValueType>

storm::storage::BitVector storm::bisimulation::detail::computeDivergentStates	(	storm::storage::SparseMatrix< ValueType > const &	transitions,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		Partition const &	partition )

Computes the states from which no state outside of their own block can be reached.

Definition at line 365 of file Initialization.cpp.

computeSilentStates()

template<typename ValueType>

storm::storage::BitVector storm::bisimulation::detail::computeSilentStates	(	storm::storage::SparseMatrix< ValueType > const &	transitions,
		Partition const &	partition )

Computes the states all of whose transitions stay within their own block.

Definition at line 402 of file Initialization.cpp.

enqueueSubBlocks()

template<typename ValueType, SplitterRefinementMode Mode>

void storm::bisimulation::detail::enqueueSubBlocks	(	SplitterRefinementContext< ValueType, Mode > &	context,
		storm::bisimulation::Partition::Block const	splitBlock )

Replaces the given block, which has just been split, by its sub-blocks in the queue of splitters.

For strong bisimulation, the largest sub-block is not enqueued if the given block is not in the queue: then, the partition is already stable with respect to the given block (or becomes stable in the current round). As the probability of moving into the block is the sum of the probabilities of moving into its sub-blocks, stability with respect to all other sub-blocks implies stability with respect to the largest one (with a positive tolerance, up to the accumulated tolerance). This way, every state is only part of logarithmically many splitters. The argument does not carry over to weak bisimulation, where the moves within the own block are unobservable, so that splitting a block changes what is observable for the states of its sub-blocks.

Definition at line 124 of file SplitterBasedRefinement.cpp.

recomputeSilentStates()

template<typename ValueType, SplitterRefinementMode Mode>
requires (Mode != SplitterRefinementMode::Strong)

void storm::bisimulation::detail::recomputeSilentStates	(	SplitterRefinementContext< ValueType, Mode > &	context,
		auto const &	candidates )

Recomputes whether the given candidate states are silent.

Definition at line 90 of file SplitterBasedRefinement.cpp.

refineBlockStrong()

template<typename ValueType, SplitterRefinementMode Mode>

void storm::bisimulation::detail::refineBlockStrong	(	SplitterRefinementContext< ValueType, Mode > &	context,
		storm::bisimulation::Partition::Block const	predecessorBlockToSplit )

Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter.

In WeakDiscreteTime mode this is applied to the blocks whose states carry a reward, for which the moves within the own block are observable. Also applied in WeakContinuousTime mode, where the splitter probabilities are the transition rates and the splitter is not equal to predecessorBlockToSplit.

Definition at line 144 of file SplitterBasedRefinement.cpp.

refineBlockWeak()

template<typename ValueType>

void storm::bisimulation::detail::refineBlockWeak	(	SplitterRefinementContext< ValueType, SplitterRefinementMode::WeakDiscreteTime > &	context,
		storm::bisimulation::Partition::Block const	block,
		storm::bisimulation::Partition::Block const	splitterBlock )

Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter, conditioned on leaving the own block.

The non-silent states are classified by their conditional probabilities. The silent states are classified by the set of different non-silent states they can reach. Specifically, the given block is split into

• several blocks of states that can only reach exactly one class of non-silent state (one such block per distinct conditional probability), and
• a block of states that can reach multiple different classes of non-silent states.

Definition at line 188 of file SplitterBasedRefinement.cpp.

refinePartitionBasedOnSignature()

template<typename ValueType, SignatureMode SignatureMode>

void storm::bisimulation::detail::refinePartitionBasedOnSignature	(	SignatureRefinementContext< ValueType, SignatureMode > &	context,
		storm::bisimulation::Partition::Block const	pivotBlock,
		bool const	enforcePredecessorExploration )

Definition at line 40 of file SignatureBasedRefinement.cpp.

refinePartitionBasedOnSplitter()

template<typename ValueType, SplitterRefinementMode Mode>

void storm::bisimulation::detail::refinePartitionBasedOnSplitter	(	SplitterRefinementContext< ValueType, Mode > &	context,
		storm::bisimulation::Partition::Block const	splitterBlock )

Definition at line 340 of file SplitterBasedRefinement.cpp.