Classes
class	action_block_entry
	information about a transition sorted per (action, target block) pair More...

class	block_bunch_entry
	information about a transition grouped per (source block, bunch) pair More...

class	block_bunch_slice_t
	Information about a set of transitions with the same source block, in the same bunch. More...

class	block_t
	stores information about a block More...

class	bunch_t
	bunch of transitions More...

class	iterator_or_counter
	union: either iterator or counter (for initialisation) More...

class	part_state_t
	refinable partition data structure More...

class	part_trans_t

class	permutation_entry
	entry in the permutation array More...

class	pred_entry
	information about a transition sorted per target state More...

class	state_info_entry
	stores information about a single state More...

class	succ_entry
	information about a transition sorted per source state More...

Typedefs
using	permutation_t = fixed_vector< permutation_entry >

using	block_bunch_slice_iter_t = simple_list< block_bunch_slice_t >::iterator

using	block_bunch_slice_const_iter_t = simple_list< block_bunch_slice_t >::const_iterator

using	block_bunch_slice_iter_or_null_t = iterator_or_null_t< block_bunch_slice_t >

Enumerations
enum	new_block_mode_t { new_block_is_U , new_block_is_R }

Functions
template<class LTS_TYPE >
static void	finalise_U_is_smaller (const block_t const block_U, const block_t const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
	moves temporary work counters to normal ones if the U-block is smaller

template<class LTS_TYPE >
static void	finalise_R_is_smaller (const block_t const block_U, const block_t const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
	moves temporary work counters to normal ones if the R-block is smaller

Function Documentation

◆ finalise_R_is_smaller()

template<class LTS_TYPE >

static void mcrl2::lts::detail::bisim_dnj::finalise_R_is_smaller	(	const block_t *const	block_U,
		const block_t *const	block_R,
		const bisim_partitioner_dnj< LTS_TYPE > &	partitioner
	)

static

moves temporary work counters to normal ones if the R-block is smaller

Parameters

block_U	the larger subblock containing the U-states
block_R	the smaller but non-empty subblock containing the R-states
partitioner	the partitioner data structure, used to write diagnostic messages

Definition at line 4824 of file liblts_bisim_dnj.h.

template<class LTS_TYPE >

static void mcrl2::lts::detail::bisim_dnj::finalise_U_is_smaller	(	const block_t *const	block_U,
		const block_t *const	block_R,
		const bisim_partitioner_dnj< LTS_TYPE > &	partitioner
	)

static

moves temporary work counters to normal ones if the U-block is smaller

Parameters

block_U	the smaller subblock containing the U-states (can be nullptr)
block_R	the larger subblock containing the R-states
partitioner	the partitioner data structure, used to write diagnostic messages

Definition at line 4720 of file liblts_bisim_dnj.h.

struct { ... } mcrl2::lts::detail::bisim_dnj::action_label_greater