This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. More...

#include <BisimulationDecomposition.h>

Inheritance diagram for storm::storage::BisimulationDecomposition< ModelType, BlockDataType >:

Collaboration diagram for storm::storage::BisimulationDecomposition< ModelType, BlockDataType >:

[legend]

Classes
struct	Options

Public Types
typedef ModelType::ValueType	ValueType

typedef ModelType::RewardModelType	RewardModelType

Public Types inherited from storm::storage::Decomposition< StateBlock >
typedef StateBlock	block_type

typedef std::vector< block_type >::iterator	iterator

typedef std::vector< block_type >::const_iterator	const_iterator

Public Member Functions
	BisimulationDecomposition (ModelType const &model, Options const &options)
	Decomposes the given model into equivalance classes of a bisimulation.

virtual	~BisimulationDecomposition ()=default

std::shared_ptr< ModelType >	getQuotient () const
	Retrieves the quotient of the model under the computed bisimulation.

void	computeBisimulationDecomposition ()
	Computes the decomposition of the model into bisimulation equivalence classes.

Public Member Functions inherited from storm::storage::Decomposition< StateBlock >
	Decomposition ()
	Creates an empty decomposition.

	Decomposition (Decomposition const &other)
	Creates a decomposition by copying the given decomposition.

	Decomposition (Decomposition &&other)
	Creates a decomposition by moving the given decomposition.

virtual	~Decomposition ()=default
	Default (virtual) deconstructor.

Decomposition &	operator= (Decomposition const &other)
	Assigns the contents of the given decomposition to the current one by copying the contents.

Decomposition &	operator= (Decomposition &&other)
	Assigns the contents of the given decomposition to the current one by moving the contents.

std::size_t	size () const
	Retrieves the number of blocks of this decomposition.

bool	empty () const
	Checks if the decomposition is empty.

iterator	begin ()
	Retrieves an iterator that points to the first block of this decomposition.

const_iterator	begin () const
	Retrieves a const iterator that points to the first block of this decomposition.

iterator	end ()
	Retrieves an iterator that points past the last block of this decomposition.

const_iterator	end () const
	Retrieves a const iterator that points past the last block of this decomposition.

block_type const &	getBlock (uint_fast64_t index) const
	Retrieves the block with the given index.

block_type &	getBlock (uint_fast64_t index)
	Retrieves the block with the given index.

block_type const &	operator[] (uint_fast64_t index) const
	Retrieves the block with the given index.

block_type &	operator[] (uint_fast64_t index)
	Retrieves the block with the given index.

storm::storage::SparseMatrix< ValueType >	extractPartitionDependencyGraph (storm::storage::SparseMatrix< ValueType > const &matrix) const

Protected Member Functions
	BisimulationDecomposition (ModelType const &model, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, Options const &options)
	Decomposes the given model into equivalance classes of a bisimulation.

void	performPartitionRefinement ()
	Performs the partition refinement on the model and thereby computes the equivalence classes under strong bisimulation equivalence.

virtual void	refinePartitionBasedOnSplitter (bisimulation::Block< BlockDataType > &splitter, std::vector< bisimulation::Block< BlockDataType > * > &splitterQueue)=0
	Refines the partition by considering the given splitter.

virtual void	buildQuotient ()=0
	Builds the quotient model based on the previously computed equivalence classes (stored in the blocks of the decomposition.

virtual void	initializeLabelBasedPartition ()
	Initializes the initial partition based on all respected labels.

virtual void	initializeMeasureDrivenPartition ()
	Creates the measure-driven initial partition for reaching psi states from phi states.

virtual void	initialize ()
	A function that can initialize auxiliary data structures.

virtual std::pair< storm::storage::BitVector, storm::storage::BitVector >	getStatesWithProbability01 ()=0
	Computes the set of states with probability 0/1 for satisfying phi until psi.

virtual void	splitInitialPartitionBasedOnRewards ()
	Splits the initial partition based on the (unique) reward model of the current model.

virtual void	splitInitialPartitionBasedOnRewards (std::vector< ValueType > const &rewardVector)
	Splits the initial partition based on the given reward vector.

virtual void	splitInitialPartitionBasedOnActionRewards (std::vector< std::set< ValueType > > const &rewardVector)
	Splits the initial partition based on the given vector of action rewards.

void	extractDecompositionBlocks ()
	Constructs the blocks of the decomposition object based on the current partition.

Protected Attributes
ModelType const &	model

storm::storage::SparseMatrix< ValueType >	backwardTransitions

Options	options

storm::storage::bisimulation::Partition< BlockDataType >	partition

storm::utility::ConstantsComparator< ValueType >	comparator

std::shared_ptr< ModelType >	quotient

Protected Attributes inherited from storm::storage::Decomposition< StateBlock >
std::vector< block_type >	blocks

Detailed Description

template<typename ModelType, typename BlockDataType>
class storm::storage::BisimulationDecomposition< ModelType, BlockDataType >

This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.

Definition at line 45 of file BisimulationDecomposition.h.

Member Typedef Documentation

◆ RewardModelType

template<typename ModelType , typename BlockDataType >

typedef ModelType::RewardModelType storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::RewardModelType

Definition at line 48 of file BisimulationDecomposition.h.

◆ ValueType

template<typename ModelType , typename BlockDataType >

typedef ModelType::ValueType storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::ValueType

Definition at line 47 of file BisimulationDecomposition.h.

Constructor & Destructor Documentation

◆ BisimulationDecomposition() [1/2]

template<typename ModelType , typename BlockDataType >

storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::BisimulationDecomposition	(	ModelType const &	model,
		Options const &	options
	)

Decomposes the given model into equivalance classes of a bisimulation.

Parameters

model	The model to decompose.
options	The options to use during for the decomposition.

Definition at line 182 of file BisimulationDecomposition.cpp.

◆ ~BisimulationDecomposition()

template<typename ModelType , typename BlockDataType >

virtual storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::~BisimulationDecomposition ( )

virtualdefault

◆ BisimulationDecomposition() [2/2]

template<typename ModelType , typename BlockDataType >

storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::BisimulationDecomposition	(	ModelType const &	model,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		Options const &	options
	)

protected

Decomposes the given model into equivalance classes of a bisimulation.

Parameters

model	The model to decompose.
backwardTransition	The backward transitions of the model.
options	The options to use during for the decomposition.

Definition at line 188 of file BisimulationDecomposition.cpp.

Member Function Documentation

◆ buildQuotient()

template<typename ModelType , typename BlockDataType >

virtual void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::buildQuotient ( )

protectedpure virtual

Builds the quotient model based on the previously computed equivalence classes (stored in the blocks of the decomposition.

Implemented in storm::storage::DeterministicModelBisimulationDecomposition< ModelType >, and storm::storage::NondeterministicModelBisimulationDecomposition< ModelType >.

◆ computeBisimulationDecomposition()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::computeBisimulationDecomposition ( )

Computes the decomposition of the model into bisimulation equivalence classes.

If requested, a quotient model is built.

Definition at line 208 of file BisimulationDecomposition.cpp.

◆ extractDecompositionBlocks()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::extractDecompositionBlocks ( )

protected

Constructs the blocks of the decomposition object based on the current partition.

Definition at line 381 of file BisimulationDecomposition.cpp.

◆ getQuotient()

template<typename ModelType , typename BlockDataType >

std::shared_ptr< ModelType > storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::getQuotient ( ) const

Retrieves the quotient of the model under the computed bisimulation.

Returns: The quotient model.

Definition at line 292 of file BisimulationDecomposition.cpp.

◆ getStatesWithProbability01()

template<typename ModelType , typename BlockDataType >

virtual std::pair< storm::storage::BitVector, storm::storage::BitVector > storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::getStatesWithProbability01 ( )

protectedpure virtual

Computes the set of states with probability 0/1 for satisfying phi until psi.

This is used for the measure driven initial partition.

Returns: The states with probability 0 and 1.

Implemented in storm::storage::DeterministicModelBisimulationDecomposition< ModelType >, and storm::storage::NondeterministicModelBisimulationDecomposition< ModelType >.

◆ initialize()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::initialize ( )

protectedvirtual

A function that can initialize auxiliary data structures.

It is called after initializing the initial partition.

Reimplemented in storm::storage::NondeterministicModelBisimulationDecomposition< ModelType >.

Definition at line 376 of file BisimulationDecomposition.cpp.

◆ initializeLabelBasedPartition()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::initializeLabelBasedPartition ( )

protectedvirtual

Initializes the initial partition based on all respected labels.

Reimplemented in storm::storage::DeterministicModelBisimulationDecomposition< ModelType >.

Definition at line 338 of file BisimulationDecomposition.cpp.

◆ initializeMeasureDrivenPartition()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::initializeMeasureDrivenPartition ( )

protectedvirtual

Creates the measure-driven initial partition for reaching psi states from phi states.

Reimplemented in storm::storage::DeterministicModelBisimulationDecomposition< ModelType >.

Definition at line 356 of file BisimulationDecomposition.cpp.

◆ performPartitionRefinement()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::performPartitionRefinement ( )

protected

Performs the partition refinement on the model and thereby computes the equivalence classes under strong bisimulation equivalence.

If required, the quotient model is built and may be retrieved using getQuotient().

Definition at line 258 of file BisimulationDecomposition.cpp.

◆ refinePartitionBasedOnSplitter()

template<typename ModelType , typename BlockDataType >

virtual void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::refinePartitionBasedOnSplitter	(	bisimulation::Block< BlockDataType > &	splitter,
		std::vector< bisimulation::Block< BlockDataType > * > &	splitterQueue
	)

protectedpure virtual

Refines the partition by considering the given splitter.

All blocks that become potential splitters because of this refinement, are marked as splitters and inserted into the splitter vector.

Parameters

splitter	The splitter to use.
splitterVector	The vector into which to insert the newly discovered potential splitters.

◆ splitInitialPartitionBasedOnActionRewards()

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::splitInitialPartitionBasedOnActionRewards ( std::vector< std::set< ValueType > > const & rewardVector )

protectedvirtual

Splits the initial partition based on the given vector of action rewards.

Definition at line 331 of file BisimulationDecomposition.cpp.

◆ splitInitialPartitionBasedOnRewards() [1/2]

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::splitInitialPartitionBasedOnRewards ( )

protectedvirtual

Splits the initial partition based on the (unique) reward model of the current model.

Definition at line 299 of file BisimulationDecomposition.cpp.

◆ splitInitialPartitionBasedOnRewards() [2/2]

template<typename ModelType , typename BlockDataType >

void storm::storage::BisimulationDecomposition< ModelType, BlockDataType >::splitInitialPartitionBasedOnRewards ( std::vector< ValueType > const & rewardVector )