implements the main algorithm for the branching bisimulation quotient More...

#include <liblts_bisim_gj.h>

Public Member Functions
std::size_t	num_eq_classes () const
	Calculate the number of equivalence classes.

state_index	get_eq_class (const state_index si) const
	Get the equivalence class of a state.

void	finalize_minimized_LTS ()
	Adapt the LTS after minimisation.

bool	in_same_class (state_index const s, state_index const t) const
	Check whether two states are in the same equivalence class.

	bisim_partitioner_gj (LTS_TYPE &aut, const bool branching=false, const bool preserve_divergence=false)
	constructor

Public Attributes
LTS_TYPE &	m_aut
	automaton that is being reduced

fixed_vector< state_type_gj >	m_states
	information about states

fixed_vector< outgoing_transition_type >	m_outgoing_transitions
	transitions ordered per source state

fixed_vector< transition_type >	m_transitions

fixed_vector< state_in_block_pointer >	m_states_in_blocks

state_index	no_of_blocks

state_index	no_of_constellations

fixed_vector< transition_index >	m_BLC_transitions

std::clock_t	end_initial_part
	time measurement after creating the initial partition (but before the first call to `stabilizeB()`)

Private Types
typedef std::unordered_set< state_index >	set_of_states_type

typedef std::unordered_set< transition_index >	set_of_transitions_type

Private Member Functions
bool	is_inert_during_init_if_branching (const transition &t) const

bool	is_inert_during_init (const transition &t) const

label_index	label_or_divergence (const transition &t, const label_index divergent_label=-2) const

void	check_transitions (const bool initialisation, const bool check_temporary_complexity_counters, const bool check_block_to_constellation=true) const
	Checks whether the transition data structure is correct.

bool	check_data_structures (const std::string &tag, const bool initialisation=false, const bool check_temporary_complexity_counters=true) const
	Checks whether data structures are consistent.

bool	check_stability (const std::string &tag, const std::vector< std::pair< BLC_list_iterator, BLC_list_iterator > > calM=nullptr, const std::pair< BLC_list_iterator, BLC_list_iterator > calM_elt=nullptr, const constellation_type const old_constellation=null_constellation, const constellation_type const new_constellation=null_constellation) const
	Checks the main invariant of the partition refinement algorithm.

void	display_BLC_list (const block_type *const bi) const
	Prints the list of BLC sets as debug output.

void	print_data_structures (const std::string &header, const bool initialisation=false) const
	Prints the partition refinement data structure as debug output.

std::string	ptr (const transition &t) const

state_index	number_of_states_in_block (const block_type &B) const
	return the number of states in block `B`

state_index	number_of_states_in_constellation (const constellation_type &C) const
	return the number of states in constellation `C`

void	swap_states_in_states_in_block_never_equal (state_in_block_pointer pos1, state_in_block_pointer pos2)
	swap the contents of `pos1` and `pos2`, assuming they are different

void	swap_states_in_states_in_block (state_in_block_pointer pos1, state_in_block_pointer pos2)
	swap the contents of `pos1` and `pos2` if they are different

void	swap_states_in_states_in_block_23_never_equal (state_in_block_pointer pos1, state_in_block_pointer pos2, state_in_block_pointer *pos3)
	Move the contents of `pos1` to `pos2`, those of `pos2` to `pos3` and those of `pos3` to `pos1`

void	swap_states_in_states_in_block (state_in_block_pointer pos1, state_in_block_pointer pos2, state_in_block_pointer *pos3)
	Move the contents of `pos1` to `pos2`, those of `pos2` to `pos3` and those of `pos3` to `pos1`

void	multiple_swap_states_in_states_in_block (state_in_block_pointer pos1, state_in_block_pointer pos2, state_index count, const state_in_block_pointer *assign_work_to, unsigned char const max_B, enum check_complexity::counter_type const ctr=check_complexity::multiple_swap_states_in_block__swap_state_in_small_block)
	Swap the range [`pos1`, `pos1` + `count`) with the range [`pos2`, `pos2` + `count`)

void	mark_BLC_transition (const outgoing_transitions_it out_pos)
	marks the transition indicated by `out_pos`.

void	swap_three_iterators_and_update_m_transitions (const BLC_list_iterator i1, const BLC_list_iterator i2, const BLC_list_iterator i3)
	Move the content of i1 to i2, i2 to i3 and i3 to i1.

bool	swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation (const transition_index ti, linked_list< BLC_indicators >::iterator new_BLC_block, linked_list< BLC_indicators >::iterator old_BLC_block)
	Swap transition `ti` from BLC set `old_BLC_block` to BLC set `new_BLC_block`

bool	update_the_doubly_linked_list_LBC_new_constellation (block_type *const index_block_B, const transition &t, const transition_index ti)
	Move transition `t` with transition index `ti` to a new BLC set.

bool	swap_in_the_doubly_linked_list_LBC_in_blocks_new_block (const transition_index ti, linked_list< BLC_indicators >::iterator new_BLC_block, linked_list< BLC_indicators >::iterator old_BLC_block)
	Swap transition `ti` from BLC set `old_BLC_block` to BLC set `new_BLC_block`

void	update_the_doubly_linked_list_LBC_new_block (block_type const old_bi, block_type const new_bi, const transition_index ti, constellation_type old_constellation, constellation_type const new_constellation)
	Update the BLC list of transition `ti`, which now starts in block `new_bi`

void	clear_state_counters (std::vector< state_in_block_pointer >::const_iterator begin, std::vector< state_in_block_pointer >::const_iterator const end, block_type *const block)
	reset a range of state counters to `undefined`

void	change_non_bottom_state_to_bottom_state (const fixed_vector< state_type_gj >::iterator si)
	Moves the former non-bottom state `si` to the bottom states.

void	make_stable_and_move_to_start_of_BLC (block_type *const from_block, const linked_list< BLC_indicators >::iterator splitter)
	Makes splitter stable and moves it to the beginning of the list.

void	move_nonbottom_states_to (const todo_state_vector &R, state_in_block_pointer *to_pos, state_index new_block_bottom_size)
	Move states in a set to a specific position in `m_states_in_block`

block_type *	update_BLC_sets_new_block (block_type const old_bi, block_type const new_bi, constellation_type const old_constellation, constellation_type const new_constellation)
	Update all BLC sets after a new block has been created.

template<bool initialisation = false>
block_type *	create_new_block (state_in_block_pointer start_bottom_states, state_in_block_pointer const start_non_bottom_states, state_in_block_pointer const end_states, block_type const old_block_index, constellation_type const old_constellation, constellation_type const new_constellation)
	create a new block and adapt the BLC sets, and reset state counters

void	check_incoming_tau_transitions_become_noninert (block_type NewBotSt_block_index, state_in_block_pointer start_bottom, state_in_block_pointer *const end_non_bottom)
	makes incoming transitions from block `NewBotSt_block_index` non-block-inert

linked_list< BLC_indicators >::const_iterator	next_target_constln_in_same_saC (state_in_block_pointer const src, BLC_list_const_iterator const splitter_it) const
	find the next constellation after `splitter_it`'s in the `same_saC` slice of the outgoing transitions

template<bool has_small_splitter, bool has_large_splitter>
block_type *	four_way_splitB (block_type const bi, linked_list< BLC_indicators >::iterator const small_splitter, linked_list< BLC_indicators >::iterator const large_splitter, constellation_type const old_constellation, constellation_type *const new_constellation)
	split a block (using main and co-splitter) into up to four subblocks

transition_index	accumulate_entries (std::vector< transition_index > &action_counter, const std::vector< label_index > &todo_stack) const

void	order_BLC_transitions_single_BLC_set (state_in_block_pointer *const pos, BLC_list_iterator start_same_BLC, const BLC_list_iterator end_same_BLC)
	create one BLC set for the block starting at `pos`

void	order_BLC_transitions (const BLC_list_iterator start_same_BLC, const BLC_list_iterator end_same_BLC, state_in_block_pointer min_block, state_in_block_pointer max_block)
	order `m_BLC_transition` entries according to source block

template<bool initialization = false>
void	stabilizeB ()

void	create_initial_partition ()

linked_list< BLC_indicators >::iterator	find_inert_co_transition_for_block (block_type const index_block_B, const constellation_type const old_constellation, const constellation_type *const new_constellation) const
	find a splitter for the tau-transitions from the new constellation to the old constellation

block_type *	select_and_remove_a_block_in_a_non_trivial_constellation ()
	Select a block that is not the largest block in a non-trivial constellation.

void	refine_partition_until_it_becomes_stable ()

Static Private Member Functions
static LTS_TYPE::labels_size_type	m_aut_apply_hidden_label_map (typename LTS_TYPE::labels_size_type l)

Private Attributes
std::vector< block_type * >	m_blocks_with_new_bottom_states

std::vector< constellation_type * >	m_non_trivial_constellations
	The following variable contains all non-trivial constellations.

std::vector< linked_list< BLC_indicators >::iterator >	m_BLC_indicators_to_be_deleted

const bool	m_branching
	true iff branching (not strong) bisimulation has been requested

const bool	m_preserve_divergence
	true iff divergence-preserving branching bisimulation has been requested

state_index	no_of_new_bottom_states
	number of new bottom states found after constructing the initial partition

transition_index	no_of_non_constellation_inert_BLC_sets
	number of non-inert BLC sets in the partition

Detailed Description

template<class LTS_TYPE>
class mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >

implements the main algorithm for the branching bisimulation quotient

Definition at line 726 of file liblts_bisim_gj.h.

Member Typedef Documentation

◆ set_of_states_type

template<class LTS_TYPE >

typedef std::unordered_set<state_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::set_of_states_type

private

Definition at line 730 of file liblts_bisim_gj.h.

◆ set_of_transitions_type

template<class LTS_TYPE >

typedef std::unordered_set<transition_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::set_of_transitions_type

private

Definition at line 731 of file liblts_bisim_gj.h.

Constructor & Destructor Documentation

◆ bisim_partitioner_gj()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::bisim_partitioner_gj	(	LTS_TYPE &	aut,
		const bool	branching = `false`,
		const bool	preserve_divergence = `false`
	)

inline

constructor

The constructor constructs the data structures and immediately calculates the partition corresponding with the bisimulation quotient. It does not adapt the LTS to represent the quotient's transitions. It is assumed that there are no tau-loops in aut.

Parameters

aut	LTS that needs to be reduced
branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergence	If true and branching is true, preserve tau loops on states.

Definition at line 6691 of file liblts_bisim_gj.h.

Member Function Documentation

◆ accumulate_entries()

template<class LTS_TYPE >

transition_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::accumulate_entries	(	std::vector< transition_index > &	action_counter,
		const std::vector< label_index > &	todo_stack
	)		const

inlineprivate

Definition at line 4924 of file liblts_bisim_gj.h.

◆ change_non_bottom_state_to_bottom_state()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::change_non_bottom_state_to_bottom_state ( const fixed_vector< state_type_gj >::iterator si )

inlineprivate

Moves the former non-bottom state si to the bottom states.

The block of si is not yet inserted into the set of blocks with new bottom states.

Definition at line 2588 of file liblts_bisim_gj.h.

◆ check_data_structures()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::check_data_structures	(	const std::string &	tag,
		const bool	initialisation = `false`,
		const bool	check_temporary_complexity_counters = `true`
	)		const

inlineprivate

Checks whether data structures are consistent.

Returns: true iff all checks pass

Checks whether states are in their blocks; the pointers outgoing transition (-> BLC transition) -> incoming transition -> outgoing transition are consistent; whether the saC slices (source state, action, target constellation) are correct; whether blocks are correct.

Definition at line 925 of file liblts_bisim_gj.h.

◆ check_incoming_tau_transitions_become_noninert()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::check_incoming_tau_transitions_become_noninert	(	block_type *	NewBotSt_block_index,
		state_in_block_pointer *	start_bottom,
		state_in_block_pointer *const	end_non_bottom
	)

inlineprivate

makes incoming transitions from block NewBotSt_block_index non-block-inert

Definition at line 2793 of file liblts_bisim_gj.h.

◆ check_stability()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::check_stability	(	const std::string &	tag,
		const std::vector< std::pair< BLC_list_iterator, BLC_list_iterator > > *	calM = `nullptr`,
		const std::pair< BLC_list_iterator, BLC_list_iterator > *	calM_elt = `nullptr`,
		const constellation_type *const	old_constellation = `null_constellation`,
		const constellation_type *const	new_constellation = `null_constellation`
	)		const

inlineprivate

Checks the main invariant of the partition refinement algorithm.

Returns: true iff the main invariant holds

Checks the following invariant: If a block has a constellation-non-inert transition, then every bottom state has a constellation-non-inert transition with the same label to the same target constellation. It is assumed that the BLC data structure is correct, so we conveniently use that to verify the invariant.

The function can also check a partial invariant while stabilisation has not yet finished. If calM != nullptr, then we have: The above invariant may be violated for BLC sets that are still to be stabilized, as given by the main splitters in calM. (calM_elt indicates how far stabilization has handled calM already.) (block_label_to_cotransition indicates the co-splitters that belong to the main splitters in calM.) It may also be violated for blocks that contain new bottom states, as indicated by m_blocks_with_new_bottom_states.

Additionally, the function ensures that only transitions in BLC sets satisfying the above conditions are marked: Transitions may only be marked in BLC sets that are still to be stabilized, as given by calM (including co-splitters); they may also be marked if they start in new bottom states, as indicated by m_blocks_with_new_bottom_states, or if they start in a singleton block.

Definition at line 1203 of file liblts_bisim_gj.h.

◆ check_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::check_transitions	(	const bool	initialisation,
		const bool	check_temporary_complexity_counters,
		const bool	check_block_to_constellation = `true`
	)		const

inlineprivate

Checks whether the transition data structure is correct.

Returns: true iff all checks pass

Checks whether the pointers incoming transitions -> outgoing transitions -> BLC transitions -> incoming transitions are consistent; whether the pointers from states to incoming and outgoing transitions are consistent; whether the pointers from BLC indicators to BLC sets are consistent.

If check_block_to_constellation, it also checks whether every transition is in one BLC set of its source block.

If check_temporary_complexity_counters, it also checks that no more work is accounted for in temporary complexity counters. If initialisation holds, all states are treated as non-bottom states (so that later one might handle all bottom states as new bottom states in the very first call to stabilizeB()). In any case, the BLC sets need to be fully initialised.

Definition at line 832 of file liblts_bisim_gj.h.

◆ clear_state_counters()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::clear_state_counters	(	std::vector< state_in_block_pointer >::const_iterator	begin,
		std::vector< state_in_block_pointer >::const_iterator const	end,
		block_type *const	block
	)

inlineprivate

reset a range of state counters to undefined

The function is prepared for a situation when we join the block and counter fields together into one block_plus_counter. That is why it checks that only counters of states in block bi are reset.

Definition at line 2572 of file liblts_bisim_gj.h.

◆ create_initial_partition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::create_initial_partition ( )

inlineprivate

Definition at line 5746 of file liblts_bisim_gj.h.

◆ create_new_block()

template<class LTS_TYPE >

template<bool initialisation = false>

block_type * mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::create_new_block	(	state_in_block_pointer *	start_bottom_states,
		state_in_block_pointer *const	start_non_bottom_states,
		state_in_block_pointer *const	end_states,
		block_type *const	old_block_index,
		constellation_type *const	old_constellation,
		constellation_type *const	new_constellation
	)

inlineprivate

create a new block and adapt the BLC sets, and reset state counters

Parameters

start_bottom_states	pointer to the first bottom state of the new block in `m_states_in_blocks`
start_non_bottom_states	pointer to the first non-bottom state of the new block in `m_states_in_blocks`
end_states	pointer past the last state of the new block in `m_states_in_blocks`
constellation	constellation of the new block
old_constellation	old constellation of the most recent constellation-split, used to update the BLC sets

Definition at line 2746 of file liblts_bisim_gj.h.

◆ display_BLC_list()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::display_BLC_list ( const block_type *const bi ) const

inlineprivate

Prints the list of BLC sets as debug output.

Definition at line 1433 of file liblts_bisim_gj.h.

◆ finalize_minimized_LTS()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::finalize_minimized_LTS ( )

inline

Adapt the LTS after minimisation.

After the efficient branching bisimulation minimisation, the information about the quotient LTS is only stored in the partition data structure of the partitioner object. This function exports the information back to the LTS by adapting its states and transitions: it updates the number of states and adds those transitions that are mandated by the partition data structure. If desired, it also creates a vector containing an arbritrary (example) original state per equivalence class.

The main parameter and return value are implicit with this function: a reference to the LTS was stored in the object by the constructor.

Definition at line 1766 of file liblts_bisim_gj.h.

◆ find_inert_co_transition_for_block()

template<class LTS_TYPE >

linked_list< BLC_indicators >::iterator mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::find_inert_co_transition_for_block	(	block_type *const	index_block_B,
		const constellation_type *const	old_constellation,
		const constellation_type *const	new_constellation
	)		const

inlineprivate

find a splitter for the tau-transitions from the new constellation to the old constellation

Parameters

index_block_B	block that forms the new constellation
old_constellation	index of the old constellation

Returns: splitter that contains the tau-transitions from index_block_B to old_constellation

If no such splitter exists, linked_list<BLC_indicators>::end() is returned.

The function uses the fact that the first element of the list block.to_constellation contains the inert transitions (if there are any), and just after splitting the new constellation off from the old one, the element immediately after that the tau-transitions from the new to the old constellation.

Definition at line 6180 of file liblts_bisim_gj.h.

◆ four_way_splitB()

template<class LTS_TYPE >

template<bool has_small_splitter, bool has_large_splitter>

block_type * mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::four_way_splitB	(	block_type *const	bi,
		linked_list< BLC_indicators >::iterator const	small_splitter,
		linked_list< BLC_indicators >::iterator const	large_splitter,
		constellation_type *const	old_constellation,
		constellation_type *const	new_constellation
	)

inlineprivate

split a block (using main and co-splitter) into up to four subblocks

The function can be used in the following ways:

If has_small_splitter: small_splitter contains transitions to the newest constellation new_constellation (or occasionally transitions from the newest constellation); this serves to stabilize block bi after constellation new_constellation was split off from old_constellation. Because the new constellation is known to be small, the main splitter can be read completely.

If has_large_splitter, this is a true four-way-split, and large_splitter consists of transitions with the same label as small_splitter but with target constellation old_constellation. It is unknown whether large_splitter is small or large, but we are able to quickly determine, for states that have a transition in small_splitter, whether they have one in the co-splitter as well (using the start_same_saC pointers).

If !has_large_splitter, then small_splitter contains transitions that have just become non-constellation-inert by splitting the constellation (and the co-splitter would contain transitions that are still constellation-inert).
If !has_small_splitter && has_large_splitter: bi is a block in which every bottom state is new, and it needs to be stabilized under all splitters; in the current call, it is split under large_splitter, which can be treated similar to a co-splitter in the first case. (So there is still no guarantee that large_splitter is small.)

We require that every bottom state with a transition in large_splitter has a marked transition in large_splitter, so that we still can split up the bottom states quickly. (There cannot be many new bottom states, as a state becomes a new bottom state at most once during the whole algorithm.) In all other cases, marked transitions are not required.
If !has_small_splitter && !has_large_splitter: This is a split during initialisation. Block bi is split, and the relevant information about ReachAlw-states is given in the block descriptor. The parameters small_splitter and large_splitter can be ignored. (For bookkeeping, the only constellation present is given in new_constellation.)

The function refines bi into up to four subblocks consisting of the following states:

ReachAlw: states that can reach always all splitters provided, and their block-inert predecessors
AvoidSml: states that cannot inertly reach small_splitter, although small_splitter!=nullptr, and their block-inert predecessors
AvoidLrg: states that cannot inertly reach large_splitter, although large_splitter!=nullptr, and their block-inert predecessors
NewBotSt: states that can block-inertly reach multiple of the above subsets. This will include new bottom states and will later need to be stabilized under all outgoing BLC sets.

The bottom states can always be distributed over the first three subsets; after that, one has to find block-inert predecessors for each subset to extend it. NewBotSt mostly starts out empty, but sometimes a search in one of the other subsets adds a state to it.

To ensure that the search through block-inert predecessors is quick, it is broken off after three subblocks have been completed; all remaining states then must be in the unfinished subblock. In this way, every action during the search for block-inert predecessors can be assigned to a small subblock: either to a state in it, or an incoming or an outgoing transition.

Parameters

bi	index of the block being split
small_splitter	small BLC set under which the block needs to be stabilized
large_splitter	(possibly large) BLC set under which the block needs to be stabilized
old_constellation	target constellation of all co-splitters
new_constellation	newest constellation (target of main splitters), used for bookkeeping

Returns: block index of the ReachAlw subblock if it exists; or null_block if ReachAlw is empty

potential non-bottom states

These vectors contain non-bottom states that have been found when going through predecessors of a subblock.

The variable is declared static to avoid repeated deallocations and reallocations while the algorithm runs many refinements.

proven non-bottom states

These vectors contain all non-bottom states of which the procedure has proven that they are in the respective subblock, unless the corresponding coroutine has been aborted; all their block-inert successors are already in the subblock.

The variable is declared static to avoid repeated deallocations and reallocations while the algorithm runs many refinements.

The fourth entry in this array is for NewBotSt; it should be in the same array to allow to find the three other arrays with coroutine^1, coroutine^2 and coroutine^3.

distribution of bottom states

Bottom states are distributed over the subblocks by placing them in a specific slice of the bottom states of block bi: at the beginning there will be ReachAlw-bottom states, then AvoidLrg-bottom states and at the end AvoidSml-bottom states. The iterators indicate the place where every slice starts; at the same time, this is the end of the previous slice.

next unhandled co-splitter transition

NewBotSt may go through the co-splitter transitions at some point of the algorithm; this iterator is used to store which transition NewBotSt will handle next. (The variable is already declared here just for initialisation.)

Abort if there are too many bottom states in a subblock, used before the coroutines start

This macro applies to ReachAlw, AvoidSml, or AvoidLrg.

If the bottom states alone already cover more than half of a block, the corresponding coroutine does not need to start.

Abort if there are too many states in subblock NewBotSt

: If the states, possibly after adding i additional states, cover more than half of the states in the unfinished subblocks, NewBotSt can be aborted. The parameter i allows to apply the test even before adding a state, to avoid storing data that is immediately going to be abolished.

NewBotSt has only non-bottom states, so we need a macro that is different from the other subblocks.

This macro can be used before the coroutines start or while they run.

Abort if there are too many states in a subblock

: If the states, possibly after adding i additional states, cover more than half of the states in the unfinished subblocks, the coroutine can be aborted. The parameter i allows to apply the test even before adding a state, to avoid storing data that is immediately going to be abolished.

If the coroutine is aborted, its non-bottom state vector is immediately cleared, as it is of no use any more. (Marked counters can be found through potential_non_bottom_states.)

This macro can be used while the coroutines run.

Definition at line 2930 of file liblts_bisim_gj.h.

◆ get_eq_class()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::get_eq_class ( const state_index si ) const

inline

Get the equivalence class of a state.

After running the minimisation algorithm, this function produces the number of the equivalence class of a state. This number is the same as the number of the state in the minimised LTS to which the original state is mapped.

Parameters

s	state whose equivalence class needs to be found

Returns: sequence number of the equivalence class of state s

Definition at line 1748 of file liblts_bisim_gj.h.

◆ in_same_class()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::in_same_class	(	state_index const	s,
		state_index const	t
	)		const

inline

Check whether two states are in the same equivalence class.

Parameters

s	first state that needs to be compared.
t	second state that needs to be compared.

Returns: true iff the two states are in the same equivalence class.

Definition at line 1847 of file liblts_bisim_gj.h.

◆ is_inert_during_init()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::is_inert_during_init ( const transition & t ) const

inlineprivate

The function tests whether transition t is inert during initialisation, i.e. when there is only one source/target block.

Definition at line 793 of file liblts_bisim_gj.h.

◆ is_inert_during_init_if_branching()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::is_inert_during_init_if_branching ( const transition & t ) const

inlineprivate

The function assumes that m_branching is true and tests whether transition t is inert during initialisation under that condition

Definition at line 785 of file liblts_bisim_gj.h.

◆ label_or_divergence()

template<class LTS_TYPE >

label_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::label_or_divergence	(	const transition &	t,
		const label_index	divergent_label = `-2`
	)		const

inlineprivate

The function calculates the label index of transition t, where tau-self-loops get the special index divergent_label if divergence needs to be preserved

Definition at line 801 of file liblts_bisim_gj.h.

◆ m_aut_apply_hidden_label_map()

template<class LTS_TYPE >

static LTS_TYPE::labels_size_type mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_aut_apply_hidden_label_map ( typename LTS_TYPE::labels_size_type l )

inlinestaticprivate

The auxiliary function below can be removed, but is now used to express that the hidden_label_map does not need to be applied, while still leaving it in the code.

Definition at line 777 of file liblts_bisim_gj.h.

◆ make_stable_and_move_to_start_of_BLC()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::make_stable_and_move_to_start_of_BLC	(	block_type *const	from_block,
		const linked_list< BLC_indicators >::iterator	splitter
	)

inlineprivate

Makes splitter stable and moves it to the beginning of the list.

Definition at line 2599 of file liblts_bisim_gj.h.

◆ mark_BLC_transition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::mark_BLC_transition ( const outgoing_transitions_it out_pos )

inlineprivate

marks the transition indicated by out_pos.

(We use an outgoing_transitions_it because it points to the m_BLC_transitions entry that needs to be updated.)

Definition at line 2006 of file liblts_bisim_gj.h.

◆ move_nonbottom_states_to()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::move_nonbottom_states_to	(	const todo_state_vector &	R,
		state_in_block_pointer *	to_pos,
		state_index	new_block_bottom_size
	)

inlineprivate

Move states in a set to a specific position in m_states_in_block

Parameters

R	vector of states that need to be moved
to_pos	position where the first state in `R` needs to move to

The work on this is assigned to the states in vector R.

Definition at line 2630 of file liblts_bisim_gj.h.

◆ multiple_swap_states_in_states_in_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::multiple_swap_states_in_states_in_block	(	state_in_block_pointer *	pos1,
		state_in_block_pointer *	pos2,
		state_index	count,
		const state_in_block_pointer *	assign_work_to,
		unsigned char const	max_B,
		enum check_complexity::counter_type const	ctr = `check_complexity:: multiple_swap_states_in_block__swap_state_in_small_block`
	)

inlineprivate

Swap the range [pos1, pos1 + count) with the range [pos2, pos2 + count)

pos1 must come before pos2. (If the ranges overlap, only swap the non-overlapping part.) The function requires count > 0 and pos1 < pos2 (this is sufficient for how it's used below: to swap new bottom states into their proper places; also, the work counters assume that [assign_work_to, assign_work_to + count) is assigned the work.)

Definition at line 1946 of file liblts_bisim_gj.h.

◆ next_target_constln_in_same_saC()

template<class LTS_TYPE >

linked_list< BLC_indicators >::const_iterator mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::next_target_constln_in_same_saC	(	state_in_block_pointer const	src,
		BLC_list_const_iterator const	splitter_it
	)		const

inlineprivate

find the next constellation after splitter_it's in the same_saC slice of the outgoing transitions

Assumes that the BLC sets are fully initialized.

Definition at line 2827 of file liblts_bisim_gj.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::num_eq_classes ( ) const

inline

Calculate the number of equivalence classes.

The number of equivalence classes (which is valid after the partition has been constructed) is equal to the number of states in the bisimulation quotient.

Definition at line 1735 of file liblts_bisim_gj.h.

◆ number_of_states_in_block()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::number_of_states_in_block ( const block_type & B ) const

inlineprivate

return the number of states in block B

Definition at line 1864 of file liblts_bisim_gj.h.

◆ number_of_states_in_constellation()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::number_of_states_in_constellation ( const constellation_type & C ) const

inlineprivate

return the number of states in constellation C

Definition at line 1870 of file liblts_bisim_gj.h.

◆ order_BLC_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::order_BLC_transitions	(	const BLC_list_iterator	start_same_BLC,
		const BLC_list_iterator	end_same_BLC,
		state_in_block_pointer *	min_block,
		state_in_block_pointer *	max_block
	)

inlineprivate

order m_BLC_transition entries according to source block

Parameters

start_same_BLC	first transition to be handled
end_same_BLC	iterator past the last transition to be handled
min_block	lower bound to the block `start_bottom_states` that can be expected
max_block	upper bound to the block `start_bottom_states` that can be expected

This function assumes that all transitions in the range [start_same_BLC, end_same_BLC) have the same label and the same target constellation. They have source blocks whose field start_bottom_states is in the range [min_block, max_block]. It groups these transitions according to their source blocks and inserts the corresponding linked_list<BLC_indicators> entries in the source blocks. The algorithm used is similar to quicksort, but the pivot value is determined by numeric calculations instead of selection from the data.

The function is intended to be used during initialisation, if one does not use m_BLC_transitions during the first refinements.

Definition at line 4983 of file liblts_bisim_gj.h.

◆ order_BLC_transitions_single_BLC_set()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::order_BLC_transitions_single_BLC_set	(	state_in_block_pointer *const	pos,
		BLC_list_iterator	start_same_BLC,
		const BLC_list_iterator	end_same_BLC
	)

inlineprivate

create one BLC set for the block starting at pos

The BLC set is created, inserted into the list block.to_constellation of the block, and the pointers from transitions to it are adapted. The function also adapts the ref.BLC_transitions pointer of the transitions in the BLC set.

Definition at line 4943 of file liblts_bisim_gj.h.

◆ print_data_structures()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::print_data_structures	(	const std::string &	header,
		const bool	initialisation = `false`
	)		const

inlineprivate

Prints the partition refinement data structure as debug output.

Definition at line 1480 of file liblts_bisim_gj.h.

◆ ptr()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::ptr ( const transition & t ) const

inlineprivate

Definition at line 1853 of file liblts_bisim_gj.h.

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::refine_partition_until_it_becomes_stable ( )

inlineprivate

Definition at line 6282 of file liblts_bisim_gj.h.

◆ select_and_remove_a_block_in_a_non_trivial_constellation()

template<class LTS_TYPE >

block_type * mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::select_and_remove_a_block_in_a_non_trivial_constellation ( )

inlineprivate

Select a block that is not the largest block in a non-trivial constellation.

Returns: the index of such a block

Either the first or the last block of a constellation is selected; also, the constellation bounds are adapted accordingly. However, the caller will have to create a new constellation and set the block's constellation field.

To ensure the time complexity bounds, it is necessary that the block returned contains at most 50% of the states in its constellation. The smaller the better.

Definition at line 6243 of file liblts_bisim_gj.h.

◆ stabilizeB()

template<class LTS_TYPE >

template<bool initialization = false>

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::stabilizeB ( )

inlineprivate

Definition at line 5237 of file liblts_bisim_gj.h.

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_block()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_in_the_doubly_linked_list_LBC_in_blocks_new_block	(	const transition_index	ti,
		linked_list< BLC_indicators >::iterator	new_BLC_block,
		linked_list< BLC_indicators >::iterator	old_BLC_block
	)

inlineprivate

Swap transition ti from BLC set old_BLC_block to BLC set new_BLC_block

Parameters

ti	transition that needs to be swapped
new_BLC_block	new BLC set, where the transition should go to
old_BLC_block	old BLC set, where the transition was in originally

Returns: true iff the last element of old_BLC_block has been removed

It is assumed that the new BLC set is located precisely before the old BLC set in m_BLC_transitions. This routine cannot be used in the initialisation phase, but only during refinement.

The stability state of old and new BLC set is always the same.

Definition at line 2244 of file liblts_bisim_gj.h.

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation	(	const transition_index	ti,
		linked_list< BLC_indicators >::iterator	new_BLC_block,
		linked_list< BLC_indicators >::iterator	old_BLC_block
	)

inlineprivate

Swap transition ti from BLC set old_BLC_block to BLC set new_BLC_block

Parameters

ti	transition that needs to be swapped
new_BLC_block	new BLC set, where the transition should go to
old_BLC_block	old BLC set, where the transition was in originally

Returns: true iff the last element of old_BLC_block has been removed

It is assumed that the new BLC set is located precisely before the old BLC set in m_BLC_transitions. This routine cannot be used in the initialisation phase, but only during refinement.

This variant of the swap routine assumes that transition ti is only marked if it is in a singleton block or in a block containing new bottom states. In both cases, it is not necessary to maintain transition markings; so ti will always be treated as unmarked, and the new BLC set must be stable. (However, it may happen that other transitions in old_BLC_block are marked, and then their marking must be kept.)

Definition at line 2088 of file liblts_bisim_gj.h.

◆ swap_states_in_states_in_block() [1/2]

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_states_in_states_in_block	(	state_in_block_pointer *	pos1,
		state_in_block_pointer *	pos2
	)

inlineprivate

swap the contents of pos1 and pos2 if they are different

Definition at line 1886 of file liblts_bisim_gj.h.

◆ swap_states_in_states_in_block() [2/2]

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_states_in_states_in_block	(	state_in_block_pointer *	pos1,
		state_in_block_pointer *	pos2,
		state_in_block_pointer *	pos3
	)

inlineprivate

Move the contents of pos1 to pos2, those of pos2 to pos3 and those of pos3 to pos1

The function requires that pos3 lies in between pos1 and pos2. The swap is only executed if the positions are different.

Definition at line 1924 of file liblts_bisim_gj.h.

◆ swap_states_in_states_in_block_23_never_equal()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_states_in_states_in_block_23_never_equal	(	state_in_block_pointer *	pos1,
		state_in_block_pointer *	pos2,
		state_in_block_pointer *	pos3
	)

inlineprivate

Move the contents of pos1 to pos2, those of pos2 to pos3 and those of pos3 to pos1

The function requires that pos3 lies in between pos1 and pos2. It also requires that pos2 and pos3 are different.

Definition at line 1898 of file liblts_bisim_gj.h.

◆ swap_states_in_states_in_block_never_equal()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_states_in_states_in_block_never_equal	(	state_in_block_pointer *	pos1,
		state_in_block_pointer *	pos2
	)

inlineprivate

swap the contents of pos1 and pos2, assuming they are different

Definition at line 1877 of file liblts_bisim_gj.h.

◆ swap_three_iterators_and_update_m_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::swap_three_iterators_and_update_m_transitions	(	const BLC_list_iterator	i1,
		const BLC_list_iterator	i2,
		const BLC_list_iterator	i3
	)

inlineprivate

Move the content of i1 to i2, i2 to i3 and i3 to i1.

Definition at line 2043 of file liblts_bisim_gj.h.

◆ update_BLC_sets_new_block()

template<class LTS_TYPE >

block_type * mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::update_BLC_sets_new_block	(	block_type *const	old_bi,
		block_type *const	new_bi,
		constellation_type *const	old_constellation,
		constellation_type *const	new_constellation
	)

inlineprivate

Update all BLC sets after a new block has been created.

Parameters

old_bi	index of the old block from which states have been taken
new_bi	index of the new block
old_constellation	old constellation that was split most recently

The old constellation is used to maintain the order of main/co-splitter pairs in the list of BLC sets (remember that we should have the main splitter immediately before its co-splitter).

Definition at line 2657 of file liblts_bisim_gj.h.

◆ update_the_doubly_linked_list_LBC_new_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::update_the_doubly_linked_list_LBC_new_block	(	block_type *const	old_bi,
		block_type *const	new_bi,
		const transition_index	ti,
		constellation_type *	old_constellation,
		constellation_type *const	new_constellation
	)

inlineprivate

Update the BLC list of transition ti, which now starts in block new_bi

Parameters

old_bi	the former block where the source state of `ti` was in
new_bi	the current block where the source state of `ti` moves to
ti	index of the transition whose source state moved to a new block
old_constellation	target constellation of co-splitters

If the transition was part of a stable BLC set, or is constellation-inert, the new BLC set where it goes to is also stable. If the transition is part of an unstable BLC set, the order of main/co-splitters is maintained. This order states that a co-splitter (i.e. any BLC set with non-constellation-inert transitions whose target state is in old_constellation) immediately precedes its corresponding main splitter (i.e. a BLC set with non-constellation-inert transitions whose target state is in the newest constellation, with the same action labels as the co-splitter).

To maintain the order, it may happen that the old BLC set (where ti comes from) needs to be kept even if it becomes empty; then it will be added to m_BLC_indicators_to_be_deleted for deletion after all transitions of new_bi have been handled.

Definition at line 2308 of file liblts_bisim_gj.h.

◆ update_the_doubly_linked_list_LBC_new_constellation()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::update_the_doubly_linked_list_LBC_new_constellation	(	block_type *const	index_block_B,
		const transition &	t,
		const transition_index	ti
	)

inlineprivate

Move transition t with transition index ti to a new BLC set.

Parameters

index_block_B	block forming a new constellation, at the same time target of `t`
t	transition that needs to be moved
ti	(redundant) transition index of t

Returns: true iff a new BLC set for non-constellation-inert transitions has been created

Called if the target state of transition t switches to a new constellation; at the moment of calling, the new constellation only contains block index_block_B.

If the transition is not constellation-inert (or does not remain constellation-inert), it is moved to a BLC set just after the current BLC set in its list of BLC sets. If no suitable BLC set exists yet, it will be created in that position of the list. In this way, a main splitter (i.e. a BLC set with transitions to the new constellation) will always immediately succeed its co-splitter.

Counting the number of BLC sets requires that the new block still has the old constellation number.

Definition at line 2132 of file liblts_bisim_gj.h.

Member Data Documentation

◆ end_initial_part

template<class LTS_TYPE >

std::clock_t mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::end_initial_part

time measurement after creating the initial partition (but before the first call to stabilizeB())

Definition at line 6678 of file liblts_bisim_gj.h.

◆ m_aut

template<class LTS_TYPE >

LTS_TYPE& mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_aut

automaton that is being reduced

Definition at line 736 of file liblts_bisim_gj.h.

◆ m_BLC_indicators_to_be_deleted

template<class LTS_TYPE >

std::vector<linked_list<BLC_indicators>::iterator> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_BLC_indicators_to_be_deleted

private

Definition at line 762 of file liblts_bisim_gj.h.

◆ m_BLC_transitions

template<class LTS_TYPE >

fixed_vector<transition_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_BLC_transitions

Definition at line 754 of file liblts_bisim_gj.h.

◆ m_blocks_with_new_bottom_states

template<class LTS_TYPE >

std::vector<block_type*> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_blocks_with_new_bottom_states

private

Definition at line 756 of file liblts_bisim_gj.h.

◆ m_branching

template<class LTS_TYPE >

const bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_branching

private

true iff branching (not strong) bisimulation has been requested

Definition at line 765 of file liblts_bisim_gj.h.

◆ m_non_trivial_constellations

template<class LTS_TYPE >

std::vector<constellation_type*> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_non_trivial_constellations

private

The following variable contains all non-trivial constellations.

Definition at line 759 of file liblts_bisim_gj.h.

◆ m_outgoing_transitions

template<class LTS_TYPE >

fixed_vector<outgoing_transition_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_outgoing_transitions

transitions ordered per source state

This array is used to go through the outgoing transitions of a state. The transitions of a given source state are further grouped per action label, and within every action label per target constellation. The invisible label (tau) is always the first label.

Definition at line 747 of file liblts_bisim_gj.h.

◆ m_preserve_divergence

template<class LTS_TYPE >

const bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_preserve_divergence

private

true iff divergence-preserving branching bisimulation has been requested

Note that this field must be false if strong bisimulation has been requested. There is no such thing as divergence-preserving strong bisimulation.

Definition at line 772 of file liblts_bisim_gj.h.

◆ m_states

template<class LTS_TYPE >

fixed_vector<state_type_gj> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_states

information about states

Definition at line 740 of file liblts_bisim_gj.h.

◆ m_states_in_blocks

template<class LTS_TYPE >

fixed_vector<state_in_block_pointer> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_states_in_blocks

Definition at line 751 of file liblts_bisim_gj.h.

◆ m_transitions

template<class LTS_TYPE >

fixed_vector<transition_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_transitions

Definition at line 750 of file liblts_bisim_gj.h.

◆ no_of_blocks

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::no_of_blocks

Definition at line 752 of file liblts_bisim_gj.h.

◆ no_of_constellations

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::no_of_constellations

Definition at line 753 of file liblts_bisim_gj.h.

◆ no_of_new_bottom_states

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::no_of_new_bottom_states

private

number of new bottom states found after constructing the initial partition

This count includes all states that were non-bottom state in the (unstable) trivial partition with a single block.

Definition at line 6274 of file liblts_bisim_gj.h.

◆ no_of_non_constellation_inert_BLC_sets

template<class LTS_TYPE >

transition_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::no_of_non_constellation_inert_BLC_sets

private

number of non-inert BLC sets in the partition

The sets that are in m_BLC_indicators_to_be_deleted are not included in this count. Nor are sets that contain constellation-inert transitions.

Definition at line 6280 of file liblts_bisim_gj.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_gj.h

Public Member Functions

Public Attributes

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ set_of_states_type

◆ set_of_transitions_type

Constructor & Destructor Documentation

◆ bisim_partitioner_gj()

Member Function Documentation

◆ accumulate_entries()

◆ change_non_bottom_state_to_bottom_state()

◆ check_data_structures()

◆ check_incoming_tau_transitions_become_noninert()

◆ check_stability()

◆ check_transitions()

◆ clear_state_counters()

◆ create_initial_partition()

◆ create_new_block()

◆ display_BLC_list()

◆ finalize_minimized_LTS()

◆ find_inert_co_transition_for_block()

◆ four_way_splitB()

◆ get_eq_class()

◆ in_same_class()

◆ is_inert_during_init()

◆ is_inert_during_init_if_branching()

◆ label_or_divergence()

◆ m_aut_apply_hidden_label_map()

◆ make_stable_and_move_to_start_of_BLC()

◆ mark_BLC_transition()

◆ move_nonbottom_states_to()

◆ multiple_swap_states_in_states_in_block()

◆ next_target_constln_in_same_saC()

◆ num_eq_classes()

◆ number_of_states_in_block()

◆ number_of_states_in_constellation()

◆ order_BLC_transitions()

◆ order_BLC_transitions_single_BLC_set()

◆ print_data_structures()

◆ ptr()

◆ refine_partition_until_it_becomes_stable()

◆ select_and_remove_a_block_in_a_non_trivial_constellation()

◆ stabilizeB()

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_block()

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation()

◆ swap_states_in_states_in_block() [1/2]

◆ swap_states_in_states_in_block() [2/2]

◆ swap_states_in_states_in_block_23_never_equal()

◆ swap_states_in_states_in_block_never_equal()

◆ swap_three_iterators_and_update_m_transitions()

◆ update_BLC_sets_new_block()

◆ update_the_doubly_linked_list_LBC_new_block()

◆ update_the_doubly_linked_list_LBC_new_constellation()

Member Data Documentation

◆ end_initial_part

◆ m_aut

◆ m_BLC_indicators_to_be_deleted

◆ m_BLC_transitions

◆ m_blocks_with_new_bottom_states

◆ m_branching

◆ m_non_trivial_constellations

◆ m_outgoing_transitions

◆ m_preserve_divergence

◆ m_states

◆ m_states_in_blocks

◆ m_transitions

◆ no_of_blocks

◆ no_of_constellations

◆ no_of_new_bottom_states

◆ no_of_non_constellation_inert_BLC_sets