#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, boost::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 17 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 14 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,
		boost::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 26 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 160 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 165 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 132 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 139 of file Partition.cpp.

◆ check()

template<typename DataType >

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

Definition at line 333 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 201 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 170 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 175 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 146 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 153 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 122 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 127 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 328 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 323 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 90 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 95 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 100 of file Partition.cpp.

◆ mapStatesToPositions() [1/2]

template<typename DataType >

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

Definition at line 117 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 108 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 347 of file Partition.cpp.

◆ size()

template<typename DataType >

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

Definition at line 368 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 194 of file Partition.cpp.

◆ sortBlock() [2/2]

template<typename DataType >

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

Definition at line 316 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 180 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 299 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 286 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 280 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 246 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 219 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 304 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 310 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 75 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 81 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()