The state-level information that weak bisimulation requires on top of the partition. More...

#include <WeakBisimulationData.h>

Collaboration diagram for storm::bisimulation::WeakBisimulationData:

Public Member Functions
	WeakBisimulationData (storm::storage::BitVector divergentStates, storm::storage::BitVector stepSensitiveStates, storm::storage::BitVector silentStates)
bool	isDivergent (Partition::Block const &block) const
bool	isStepSensitive (Partition::Block const &block) const
bool	checkBlockHomogeneity (Partition const &partition) const
	Checks that every block of the given partition is homogeneous with respect to divergentStates and stepSensitiveStates.

Public Attributes
storm::storage::BitVector const	divergentStates
	The states from which no state outside of their own block can be reached.
storm::storage::BitVector const	stepSensitiveStates
	The states for which the number of steps taken within their own block is observable, e.g., because they carry a non-zero preserved reward.
storm::storage::BitVector	silentStates
	The states that cannot leave their block in a single step.

Detailed Description

The state-level information that weak bisimulation requires on top of the partition.

Definition at line 27 of file WeakBisimulationData.h.

Constructor & Destructor Documentation

◆ WeakBisimulationData()

storm::bisimulation::WeakBisimulationData::WeakBisimulationData	(	storm::storage::BitVector	divergentStates,
		storm::storage::BitVector	stepSensitiveStates,
		storm::storage::BitVector	silentStates )

Definition at line 9 of file WeakBisimulationData.cpp.

Member Function Documentation

◆ checkBlockHomogeneity()

bool storm::bisimulation::WeakBisimulationData::checkBlockHomogeneity ( Partition const & partition ) const

Checks that every block of the given partition is homogeneous with respect to divergentStates and stepSensitiveStates.

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

Definition at line 27 of file WeakBisimulationData.cpp.

◆ isDivergent()

bool storm::bisimulation::WeakBisimulationData::isDivergent ( Partition::Block const & block ) const

Returns: true iff the states of the given block are divergent.

Definition at line 17 of file WeakBisimulationData.cpp.

◆ isStepSensitive()

bool storm::bisimulation::WeakBisimulationData::isStepSensitive ( Partition::Block const & block ) const

Returns: true iff the number of steps the states of the given block take within the block is observable.

Definition at line 22 of file WeakBisimulationData.cpp.

Member Data Documentation

◆ divergentStates

storm::storage::BitVector const storm::bisimulation::WeakBisimulationData::divergentStates

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

Such a block never exhibits observable behavior, so it is never split. Divergent states are closed under transitions and a state that can leave a block can also leave every sub-block of it, so this never changes during the refinement.

Definition at line 35 of file WeakBisimulationData.h.

◆ silentStates

storm::storage::BitVector storm::bisimulation::WeakBisimulationData::silentStates

The states that cannot leave their block in a single step.

This changes as the partition is refined (a state can only ever go from silent to non-silent) and is kept up to date during refinement.

Definition at line 47 of file WeakBisimulationData.h.

◆ stepSensitiveStates

storm::storage::BitVector const storm::bisimulation::WeakBisimulationData::stepSensitiveStates

The states for which the number of steps taken within their own block is observable, e.g., because they carry a non-zero preserved reward.

These are refined with respect to strong bisimulation.

Definition at line 41 of file WeakBisimulationData.h.

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

src/storm/transformer/bisimulation/WeakBisimulationData.h
src/storm/transformer/bisimulation/WeakBisimulationData.cpp

Public Member Functions

Public Attributes