Represents a partition of a set of consecutive indices. More...

#include <Partition.h>

Classes
struct	BlockCompare
	Orders blocks by their size (ascending) and, for equally sized blocks, by their location in memory. More...
class	NonSuperBlockSet
	Set of blocks that are no proper superblock. More...

Public Types
using	ElementIndex = uint64_t
	The type used to index the elements of the partition.
using	Block = std::span<ElementIndex const>
	A contiguous range of elements that form a (possibly proper super-) block of the partition.
using	OrderedBlockSet = std::set<Block, BlockCompare>
	A set of blocks, ordered by their size (smallest first).
template<typename T>
using	OrderedBlockMap = std::map<Block, T, BlockCompare>
	A map of blocks, ordered by their size (smallest first).

Public Member Functions
	Partition ()=default
	Partition (Partition const &other)=default
Partition &	operator= (Partition const &other)=default
	Partition (Partition &&other) noexcept=default
Partition &	operator= (Partition &&other)=default
	Partition (ElementIndex numElements)
	Creates the partition { {0,1,...,numElements-1} } with a single block that contains all elements.
std::size_t	getNumberOfBlocks () const
	Retrieves the number of blocks.
std::size_t	getNumberOfElements () const
	Retrieves the number of elements.
Block	getUniversalBlock () const
Block	getBlockOfElement (ElementIndex element) const
bool	contains (Block const &block, ElementIndex element) const
bool	isSubBlockOf (Block const &subblock, Block const &superblock) const
bool	isEqualBlock (Block const &lhs, Block const &rhs) const
bool	isSameBlock (ElementIndex const &element1, ElementIndex const &element2) const
bool	isBlockOfElement (Block const &block, ElementIndex const &element) const
bool	checkBlockValidity (Block const &block) const
	Checks if the given block is a valid block in the partition.
bool	isProperSuperBlock (Block const &block) const
template<typename Func> requires std::invocable<Func, Block>
void	forEachBlock (Func const &f) const
	Applies the given function on each block in the partition.
template<typename Func> requires std::invocable<Func, Block>
void	forEachSubBlock (Block const &superBlock, Func const &f) const
	Applies the given function on each block in the given super block.
template<typename SplittingOrder> requires std::invocable<SplittingOrder, ElementIndex, ElementIndex>
bool	splitBlockByOrder (Block const &block, SplittingOrder const &less)
	Splits the given block according to the given order.
template<typename Order, typename Condition> requires std::invocable<Order, ElementIndex, ElementIndex> && std::invocable<Condition, ElementIndex, ElementIndex>
bool	splitBlockByOrder (Block const &block, Order const &less, Condition const &splitCondition)
	Splits the given block according to the given order and splitting condition.
template<typename Condition> requires std::invocable<Condition, ElementIndex, ElementIndex>
bool	splitBlockByClustering (Block const &block, Condition const &condition)
	Splits the given block by anchor-based clustering: repeatedly picks the first not-yet-grouped element as the anchor of a new group, moves every remaining not-yet-grouped element e with !condition(anchor, e) into that group (wherever it currently sits in the block), and finalizes the group once no more such elements remain; then continues with the next not-yet-grouped element as the next anchor.
template<typename SplittingPredicate> requires std::predicate<SplittingPredicate, ElementIndex>
std::pair< Block, Block >	splitBlockByPredicate (Block const &block, SplittingPredicate const &f)
	Splits the given block according to the given predicate.
template<typename SplitRange> requires std::ranges::input_range<std::remove_reference_t<SplitRange>> && std::same_as<std::ranges::range_value_t<std::remove_reference_t<SplitRange>>, ElementIndex>
std::pair< Block, Block >	splitBlockByRange (Block const &block, SplitRange &&r)
	Splits the given block according to the given range of elements.

Detailed Description

Represents a partition of a set of consecutive indices.

Allows efficient access to the blocks of the partition and the elements in each block. Memory is cache-friendly and linear in the number of elements (independent of block count). The downside is that merging blocks is not supported.

Definition at line 20 of file Partition.h.

Member Typedef Documentation

◆ Block

using storm::bisimulation::Partition::Block = std::span<ElementIndex const>

A contiguous range of elements that form a (possibly proper super-) block of the partition.

Note: Splitting a block changes the order of the contained elements.

Definition at line 27 of file Partition.h.

◆ ElementIndex

using storm::bisimulation::Partition::ElementIndex = uint64_t

The type used to index the elements of the partition.

Definition at line 23 of file Partition.h.

◆ OrderedBlockMap

template<typename T>

using storm::bisimulation::Partition::OrderedBlockMap = std::map<Block, T, BlockCompare>

A map of blocks, ordered by their size (smallest first).

Definition at line 54 of file Partition.h.

◆ OrderedBlockSet

using storm::bisimulation::Partition::OrderedBlockSet = std::set<Block, BlockCompare>

A set of blocks, ordered by their size (smallest first).

Definition at line 48 of file Partition.h.

Constructor & Destructor Documentation

◆ Partition() [1/4]

storm::bisimulation::Partition::Partition ( )

default

◆ Partition() [2/4]

storm::bisimulation::Partition::Partition ( Partition const & other )

default

◆ Partition() [3/4]

storm::bisimulation::Partition::Partition ( Partition && other )

defaultnoexcept

◆ Partition() [4/4]

storm::bisimulation::Partition::Partition ( ElementIndex numElements )

explicit

Creates the partition { {0,1,...,numElements-1} } with a single block that contains all elements.

Parameters

numElements the number of elements. Must be positive.

Definition at line 51 of file Partition.cpp.

Member Function Documentation

◆ checkBlockValidity()

bool storm::bisimulation::Partition::checkBlockValidity ( Block const & block ) const

Checks if the given block is a valid block in the partition.

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

Definition at line 134 of file Partition.cpp.

◆ contains()

bool storm::bisimulation::Partition::contains	(	Block const &	block,
		ElementIndex	element ) const

Returns: true iff the given block contains the given element.

Note: this has constant runtime, i.e., is preferable over a linear search over the block

Definition at line 79 of file Partition.cpp.

◆ forEachBlock()

template<typename Func>
requires std::invocable<Func, Block>

void storm::bisimulation::Partition::forEachBlock ( Func const & f ) const

inline

Applies the given function on each block in the partition.

Note: : Splitting the currently processed block in the function is valid. However, the resulting sub-blocks are not processed recursively.

Definition at line 184 of file Partition.h.

◆ forEachSubBlock()

template<typename Func>
requires std::invocable<Func, Block>

void storm::bisimulation::Partition::forEachSubBlock	(	Block const &	superBlock,
		Func const &	f ) const

inline

Applies the given function on each block in the given super block.

For example, if superBlock = {0,1,2,3,4} and the partition currently has blocks {{0}, {1,2,3}, {4}, ...}, the function will be called with the blocks {0}, {1,2,3}, and {4}.

Note: : Splitting the currently processed block in the function is valid. However, the resulting sub-blocks are not processed recursively.

Definition at line 196 of file Partition.h.

◆ getBlockOfElement()

Partition::Block storm::bisimulation::Partition::getBlockOfElement ( ElementIndex element ) const

Returns: the block that contains the given element.

Note: the lifetime of the returned object is limited to the lifetime of this partition.; subsequent operations on this partition (e.g. split) may change the order of the elements in the block, but do not affect the contents. This means that changing the partition while iterating over block contents, i.e., for (auto e : block) { partition.split(...) ... } is not safe.

Definition at line 74 of file Partition.cpp.

◆ getNumberOfBlocks()

std::size_t storm::bisimulation::Partition::getNumberOfBlocks ( ) const

Retrieves the number of blocks.

Only counts those blocks that do not contain other (smaller) blocks

Definition at line 61 of file Partition.cpp.

◆ getNumberOfElements()

std::size_t storm::bisimulation::Partition::getNumberOfElements ( ) const

Retrieves the number of elements.

Definition at line 66 of file Partition.cpp.

◆ getUniversalBlock()

Partition::Block storm::bisimulation::Partition::getUniversalBlock ( ) const

Returns: the block that contains all elements, i.e., the universal block.

Definition at line 70 of file Partition.cpp.

◆ isBlockOfElement()

bool storm::bisimulation::Partition::isBlockOfElement	(	Block const &	block,
		ElementIndex const &	element ) const

Returns: true iff the (smallest known) block of the given element coincides with the given block.

Note: isBlockOfElement(b,e) implies contains(b,e), but the converse is not true as the former only holds if b is the smallest known block containing e.

Definition at line 103 of file Partition.cpp.

◆ isEqualBlock()

bool storm::bisimulation::Partition::isEqualBlock	(	Block const &	lhs,
		Block const &	rhs ) const

Returns: true iff the two given blocks are the same block of this partition.

Note: this has constant runtime, i.e., is preferable over comparing the contents of the blocks

Definition at line 91 of file Partition.cpp.

◆ isProperSuperBlock()

bool storm::bisimulation::Partition::isProperSuperBlock ( Block const & block ) const

Returns: true iff the given block contains multiple sub-block. For example, {1,2,3} is a (proper) super block of {1,2} and {3}.

Definition at line 185 of file Partition.cpp.

◆ isSameBlock()

bool storm::bisimulation::Partition::isSameBlock	(	ElementIndex const &	element1,
		ElementIndex const &	element2 ) const

Returns: true iff the two given elements are in the same block.

Note: this has constant runtime and does not have to look up the blocks themselves

Definition at line 97 of file Partition.cpp.

◆ isSubBlockOf()

bool storm::bisimulation::Partition::isSubBlockOf	(	Block const &	subblock,
		Block const &	superblock ) const

Returns: true iff all elements of the given subblock are contained in the given superblock.

Note: this has constant runtime, i.e., is preferable over a linear search over the block

Definition at line 84 of file Partition.cpp.

◆ operator=() [1/2]

Partition & storm::bisimulation::Partition::operator= ( Partition && other )

default

◆ operator=() [2/2]

Partition & storm::bisimulation::Partition::operator= ( Partition const & other )

default

◆ splitBlockByClustering()

template<typename Condition>
requires std::invocable<Condition, ElementIndex, ElementIndex>

bool storm::bisimulation::Partition::splitBlockByClustering	(	Block const &	block,
		Condition const &	condition )

inline

Splits the given block by anchor-based clustering: repeatedly picks the first not-yet-grouped element as the anchor of a new group, moves every remaining not-yet-grouped element e with !condition(anchor, e) into that group (wherever it currently sits in the block), and finalizes the group once no more such elements remain; then continues with the next not-yet-grouped element as the next anchor.

Unlike splitBlockByOrder, this does not require condition to be consistent with any (total or weak) order over the block's elements.

Parameters

condition returns true for pairs of elements that should not be in the same block; only ever invoked with the (still not-yet-grouped) anchor of the group currently being built as the first argument.

Returns: true iff the block was split, i.e. if the input block is now a proper super block.

Definition at line 288 of file Partition.h.

◆ splitBlockByOrder() [1/2]

template<typename Order, typename Condition>
requires std::invocable<Order, ElementIndex, ElementIndex> && std::invocable<Condition, ElementIndex, ElementIndex>

bool storm::bisimulation::Partition::splitBlockByOrder	(	Block const &	block,
		Order const &	less,
		Condition const &	splitCondition )

inline

Splits the given block according to the given order and splitting condition.

Specifically, the elements in the block are first sorted according to the given order resulting in a (sorted) block [e_0, e_1, e_2, ..., e_m]. Then, indices i_0, i_1, ..., i_k are determined such that

i_0 = 0 and
i_j > i_{j-1} is the smallest number such that condition(e_i_{j-1}, e_{i_j}) is true (or i_j = m+1 if no such number exists). We then split the block into subblocks [e_i_{j-1}, ..., e_{i_j-1}]
Parameters

less must define a strict weak order (required for well-defined sorting)

splitCondition returns true for elements that should not be in the same block as explained above

Returns
true iff the block was split, i.e. if the input block is now a proper super block.

Definition at line 232 of file Partition.h.

◆ splitBlockByOrder() [2/2]

template<typename SplittingOrder>
requires std::invocable<SplittingOrder, ElementIndex, ElementIndex>

bool storm::bisimulation::Partition::splitBlockByOrder	(	Block const &	block,
		SplittingOrder const &	less )

inline

Splits the given block according to the given order.

Specifically, the elements in the block are sorted according to the given order and then the block is split into multiple blocks, divided at every position where the order changes.

Parameters

less	must define a strict weak order (required for well-defined sorting)

Returns: true iff the block was split, i.e. if the input block is now a proper super block.

Definition at line 215 of file Partition.h.

◆ splitBlockByPredicate()

template<typename SplittingPredicate>
requires std::predicate<SplittingPredicate, ElementIndex>

std::pair< Block, Block > storm::bisimulation::Partition::splitBlockByPredicate	(	Block const &	block,
		SplittingPredicate const &	f )

inline

Splits the given block according to the given predicate.

Specifically, the elements in the block are swapped around, such that all elements where the predicate f evaluates to false come first. Then, two sub-blocks are created accordingly. If all elements are true/false, no splitting is performed.

Returns: a pair containing first the 'false' sub-block and then the 'true' sub-block. One of them can be empty.

Definition at line 329 of file Partition.h.

◆ splitBlockByRange()

template<typename SplitRange>
requires std::ranges::input_range<std::remove_reference_t<SplitRange>> && std::same_as<std::ranges::range_value_t<std::remove_reference_t<SplitRange>>, ElementIndex>

std::pair< Block, Block > storm::bisimulation::Partition::splitBlockByRange	(	Block const &	block,
		SplitRange &&	r )

inline

Splits the given block according to the given range of elements.

Specifically, the elements in the block are swapped around, such that all elements that are not in the given range come first. Then, two sub-blocks are created accordingly. If the range is empty or contains all elements of the block, no splitting is performed.

Parameters

r	the input range.

Returns: a pair containing first the sub-block that is not in the range and then the sub-block in the range. One of them can be empty.

Definition at line 362 of file Partition.h.

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

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

less	must define a strict weak order (required for well-defined sorting)
splitCondition	returns true for elements that should not be in the same block as explained above

Classes

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ Block

◆ ElementIndex

◆ OrderedBlockMap

◆ OrderedBlockSet

Constructor & Destructor Documentation

◆ Partition() [1/4]

◆ Partition() [2/4]

◆ Partition() [3/4]

◆ Partition() [4/4]

Member Function Documentation

◆ checkBlockValidity()

◆ contains()

◆ forEachBlock()

◆ forEachSubBlock()

◆ getBlockOfElement()

◆ getNumberOfBlocks()

◆ getNumberOfElements()

◆ getUniversalBlock()

◆ isBlockOfElement()

◆ isEqualBlock()

◆ isProperSuperBlock()

◆ isSameBlock()

◆ isSubBlockOf()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ splitBlockByClustering()

◆ splitBlockByOrder() [1/2]

◆ splitBlockByOrder() [2/2]

◆ splitBlockByPredicate()

◆ splitBlockByRange()