#include <Partition.h>

Public Member Functions
	Partition (std::size_t numberOfStates)
	Creates a partition with one block consisting of all the states.

	Partition (std::size_t numberOfStates, storm::storage::BitVector const &prob0States, storm::storage::BitVector const &prob1States, std::optional< storm::storage::sparse::state_type > representativeProb1State)
	Creates a partition with three blocks: one with all phi states, one with all psi states and one with all other states.

	Partition ()=default

	Partition (Partition const &other)=default

Partition &	operator= (Partition const &other)=default

	Partition (Partition &&other)=default

Partition &	operator= (Partition &&other)=default

std::size_t	size () const

void	print () const

std::pair< typename std::vector< std::unique_ptr< Block< DataType > > >::iterator, bool >	splitBlock (Block< DataType > &block, storm::storage::sparse::state_type position)

void	sortRange (storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less, bool updatePositions=true)

void	sortBlock (Block< DataType > &block, std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less, bool updatePositions=true)

std::vector< uint_fast64_t >	computeRangesOfEqualValue (uint_fast64_t startIndex, uint_fast64_t endIndex, std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less)

bool	splitBlock (Block< DataType > &block, std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less, std::function< void(Block< DataType > &)> const &newBlockCallback)

bool	splitBlock (Block< DataType > &block, std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less)

bool	split (std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less, std::function< void(Block< DataType > &)> const &newBlockCallback)

bool	split (std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &less)

void	splitStates (Block< DataType > &block, storm::storage::BitVector const &states)

void	splitStates (storm::storage::BitVector const &states)
	Splits all blocks of the partition such that afterwards all blocks contain only states within the given set of states or no such state at all.

void	sortBlock (Block< DataType > const &block)

std::vector< std::unique_ptr< Block< DataType > > > const &	getBlocks () const

std::vector< std::unique_ptr< Block< DataType > > > &	getBlocks ()

bool	check () const

std::vector< storm::storage::sparse::state_type >::iterator	begin (Block< DataType > const &block)

std::vector< storm::storage::sparse::state_type >::const_iterator	begin (Block< DataType > const &block) const

std::vector< storm::storage::sparse::state_type >::iterator	end (Block< DataType > const &block)

std::vector< storm::storage::sparse::state_type >::const_iterator	end (Block< DataType > const &block) const

std::vector< storm::storage::sparse::state_type >::iterator	begin ()

std::vector< storm::storage::sparse::state_type >::const_iterator	begin () const

std::vector< storm::storage::sparse::state_type >::iterator	end ()

std::vector< storm::storage::sparse::state_type >::const_iterator	end () const

void	swapStates (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2)

Block< DataType > &	getBlock (storm::storage::sparse::state_type state)

Block< DataType > const &	getBlock (storm::storage::sparse::state_type state) const

storm::storage::sparse::state_type const &	getPosition (storm::storage::sparse::state_type state) const

storm::storage::sparse::state_type const &	getState (storm::storage::sparse::state_type position) const

void	mapStatesToBlock (Block< DataType > &block, std::vector< storm::storage::sparse::state_type >::iterator first, std::vector< storm::storage::sparse::state_type >::iterator last)

void	mapStatesToPositions (Block< DataType > const &block)

void	mapStatesToPositions (std::vector< storm::storage::sparse::state_type >::const_iterator first, std::vector< storm::storage::sparse::state_type >::const_iterator last)

void	swapStatesAtPositions (storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2)

Detailed Description

template<typename DataType>
class storm::storage::bisimulation::Partition< DataType >

Definition at line 14 of file Partition.h.

Constructor & Destructor Documentation

◆ Partition() [1/5]

template<typename DataType >

storm::storage::bisimulation::Partition< DataType >::Partition ( std::size_t numberOfStates )

Creates a partition with one block consisting of all the states.

Parameters

numberOfStates The number of states the partition holds.

Definition at line 13 of file Partition.cpp.

◆ Partition() [2/5]

template<typename DataType >

storm::storage::bisimulation::Partition< DataType >::Partition	(	std::size_t	numberOfStates,
		storm::storage::BitVector const &	prob0States,
		storm::storage::BitVector const &	prob1States,
		std::optional< storm::storage::sparse::state_type >	representativeProb1State
	)

Creates a partition with three blocks: one with all phi states, one with all psi states and one with all other states.

The former two blocks are marked as being absorbing, because their outgoing transitions shall not be taken into account for future refinement.

Parameters

numberOfStates	The number of states the partition holds.
prob0States	The states which have probability 0 of satisfying phi until psi.
prob1States	The states which have probability 1 of satisfying phi until psi.
representativeProb1State	If the set of prob1States is non-empty, this needs to be a state that is representative for this block in the sense that the state representing this block in the quotient model will receive exactly the atomic propositions of the representative state.

Definition at line 25 of file Partition.cpp.

◆ Partition() [3/5]

template<typename DataType >

storm::storage::bisimulation::Partition< DataType >::Partition ( )

default

◆ Partition() [4/5]

template<typename DataType >

storm::storage::bisimulation::Partition< DataType >::Partition ( Partition< DataType > const & other )

default

◆ Partition() [5/5]

template<typename DataType >

storm::storage::bisimulation::Partition< DataType >::Partition ( Partition< DataType > && other )

default

Member Function Documentation

◆ begin() [1/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::iterator storm::storage::bisimulation::Partition< DataType >::begin ( )

Definition at line 159 of file Partition.cpp.

◆ begin() [2/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::const_iterator storm::storage::bisimulation::Partition< DataType >::begin ( ) const

Definition at line 164 of file Partition.cpp.

◆ begin() [3/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::iterator storm::storage::bisimulation::Partition< DataType >::begin ( Block< DataType > const & block )

Definition at line 131 of file Partition.cpp.

◆ begin() [4/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::const_iterator storm::storage::bisimulation::Partition< DataType >::begin ( Block< DataType > const & block ) const

Definition at line 138 of file Partition.cpp.

◆ check()

template<typename DataType >

bool storm::storage::bisimulation::Partition< DataType >::check ( ) const

Definition at line 329 of file Partition.cpp.

◆ computeRangesOfEqualValue()

template<typename DataType >

std::vector< uint_fast64_t > storm::storage::bisimulation::Partition< DataType >::computeRangesOfEqualValue	(	uint_fast64_t	startIndex,
		uint_fast64_t	endIndex,
		std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less
	)

Definition at line 197 of file Partition.cpp.

◆ end() [1/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::iterator storm::storage::bisimulation::Partition< DataType >::end ( )

Definition at line 169 of file Partition.cpp.

◆ end() [2/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::const_iterator storm::storage::bisimulation::Partition< DataType >::end ( ) const

Definition at line 174 of file Partition.cpp.

◆ end() [3/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::iterator storm::storage::bisimulation::Partition< DataType >::end ( Block< DataType > const & block )

Definition at line 145 of file Partition.cpp.

◆ end() [4/4]

template<typename DataType >

std::vector< storm::storage::sparse::state_type >::const_iterator storm::storage::bisimulation::Partition< DataType >::end ( Block< DataType > const & block ) const

Definition at line 152 of file Partition.cpp.

◆ getBlock() [1/2]

template<typename DataType >

Block< DataType > & storm::storage::bisimulation::Partition< DataType >::getBlock ( storm::storage::sparse::state_type state )

Definition at line 121 of file Partition.cpp.

◆ getBlock() [2/2]

template<typename DataType >

Block< DataType > const & storm::storage::bisimulation::Partition< DataType >::getBlock ( storm::storage::sparse::state_type state ) const

Definition at line 126 of file Partition.cpp.

◆ getBlocks() [1/2]

template<typename DataType >

std::vector< std::unique_ptr< Block< DataType > > > & storm::storage::bisimulation::Partition< DataType >::getBlocks ( )

Definition at line 324 of file Partition.cpp.

◆ getBlocks() [2/2]

template<typename DataType >

std::vector< std::unique_ptr< Block< DataType > > > const & storm::storage::bisimulation::Partition< DataType >::getBlocks ( ) const

Definition at line 319 of file Partition.cpp.

◆ getPosition()

template<typename DataType >

storm::storage::sparse::state_type const & storm::storage::bisimulation::Partition< DataType >::getPosition ( storm::storage::sparse::state_type state ) const

Definition at line 89 of file Partition.cpp.

◆ getState()

template<typename DataType >

storm::storage::sparse::state_type const & storm::storage::bisimulation::Partition< DataType >::getState ( storm::storage::sparse::state_type position ) const

Definition at line 94 of file Partition.cpp.

◆ mapStatesToBlock()

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::mapStatesToBlock	(	Block< DataType > &	block,
		std::vector< storm::storage::sparse::state_type >::iterator	first,
		std::vector< storm::storage::sparse::state_type >::iterator	last
	)

Definition at line 99 of file Partition.cpp.

◆ mapStatesToPositions() [1/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::mapStatesToPositions ( Block< DataType > const & block )

Definition at line 116 of file Partition.cpp.

◆ mapStatesToPositions() [2/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::mapStatesToPositions	(	std::vector< storm::storage::sparse::state_type >::const_iterator	first,
		std::vector< storm::storage::sparse::state_type >::const_iterator	last
	)

Definition at line 107 of file Partition.cpp.

◆ operator=() [1/2]

template<typename DataType >

Partition & storm::storage::bisimulation::Partition< DataType >::operator= ( Partition< DataType > && other )

default

◆ operator=() [2/2]

template<typename DataType >

Partition & storm::storage::bisimulation::Partition< DataType >::operator= ( Partition< DataType > const & other )

default

◆ print()

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::print ( ) const

Definition at line 343 of file Partition.cpp.

◆ size()

template<typename DataType >

std::size_t storm::storage::bisimulation::Partition< DataType >::size ( ) const

Definition at line 364 of file Partition.cpp.

◆ sortBlock() [1/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::sortBlock	(	Block< DataType > &	block,
		std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less,
		bool	updatePositions = `true`
	)

Definition at line 190 of file Partition.cpp.

◆ sortBlock() [2/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::sortBlock ( Block< DataType > const & block )

Definition at line 312 of file Partition.cpp.

◆ sortRange()

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::sortRange	(	storm::storage::sparse::state_type	beginIndex,
		storm::storage::sparse::state_type	endIndex,
		std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less,
		bool	updatePositions = `true`
	)

Definition at line 179 of file Partition.cpp.

◆ split() [1/2]

template<typename DataType >

bool storm::storage::bisimulation::Partition< DataType >::split ( std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const & less )

Definition at line 295 of file Partition.cpp.

◆ split() [2/2]

template<typename DataType >

bool storm::storage::bisimulation::Partition< DataType >::split	(	std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less,
		std::function< void(Block< DataType > &)> const &	newBlockCallback
	)

Definition at line 282 of file Partition.cpp.

◆ splitBlock() [1/3]

template<typename DataType >

bool storm::storage::bisimulation::Partition< DataType >::splitBlock	(	Block< DataType > &	block,
		std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less
	)

Definition at line 276 of file Partition.cpp.

◆ splitBlock() [2/3]

template<typename DataType >

bool storm::storage::bisimulation::Partition< DataType >::splitBlock	(	Block< DataType > &	block,
		std::function< bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const &	less,
		std::function< void(Block< DataType > &)> const &	newBlockCallback
	)

Definition at line 242 of file Partition.cpp.

◆ splitBlock() [3/3]

template<typename DataType >

std::pair< typename std::vector< std::unique_ptr< Block< DataType > > >::iterator, bool > storm::storage::bisimulation::Partition< DataType >::splitBlock	(	Block< DataType > &	block,
		storm::storage::sparse::state_type	position
	)

Definition at line 215 of file Partition.cpp.

◆ splitStates() [1/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::splitStates	(	Block< DataType > &	block,
		storm::storage::BitVector const &	states
	)

Definition at line 300 of file Partition.cpp.

◆ splitStates() [2/2]

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::splitStates ( storm::storage::BitVector const & states )

Splits all blocks of the partition such that afterwards all blocks contain only states within the given set of states or no such state at all.

Definition at line 306 of file Partition.cpp.

◆ swapStates()

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::swapStates	(	storm::storage::sparse::state_type	state1,
		storm::storage::sparse::state_type	state2
	)

Definition at line 74 of file Partition.cpp.

◆ swapStatesAtPositions()

template<typename DataType >

void storm::storage::bisimulation::Partition< DataType >::swapStatesAtPositions	(	storm::storage::sparse::state_type	position1,
		storm::storage::sparse::state_type	position2
	)

Definition at line 80 of file Partition.cpp.

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

src/storm/storage/bisimulation/Block.h
src/storm/storage/bisimulation/Partition.h
src/storm/storage/bisimulation/Partition.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Partition() [1/5]

◆ Partition() [2/5]

◆ Partition() [3/5]

◆ Partition() [4/5]

◆ Partition() [5/5]

Member Function Documentation

◆ begin() [1/4]

◆ begin() [2/4]

◆ begin() [3/4]

◆ begin() [4/4]

◆ check()

◆ computeRangesOfEqualValue()

◆ end() [1/4]

◆ end() [2/4]

◆ end() [3/4]

◆ end() [4/4]

◆ getBlock() [1/2]

◆ getBlock() [2/2]

◆ getBlocks() [1/2]

◆ getBlocks() [2/2]

◆ getPosition()

◆ getState()

◆ mapStatesToBlock()

◆ mapStatesToPositions() [1/2]

◆ mapStatesToPositions() [2/2]

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ print()

◆ size()

◆ sortBlock() [1/2]

◆ sortBlock() [2/2]

◆ sortRange()

◆ split() [1/2]

◆ split() [2/2]

◆ splitBlock() [1/3]

◆ splitBlock() [2/3]

◆ splitBlock() [3/3]

◆ splitStates() [1/2]

◆ splitStates() [2/2]

◆ swapStates()

◆ swapStatesAtPositions()