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

#include <liblts_bisim_gj_lazy_BLC.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_lazy_BLC (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_lb >	m_states
	information about states

fixed_vector< outgoing_transition_type_lb >	m_outgoing_transitions
	transitions ordered per source state

fixed_vector< transition_type_lb >	m_transitions
	transitions ordered per target state

fixed_vector< state_in_block_pointer_lb >	m_states_in_blocks
	states grouped per constellation and block

state_index	no_of_blocks = 1
	number of blocks that have been constructed until now

state_index	no_of_constellations = 1
	number of constellations that have been constructed until now

fixed_vector< transition_index >	m_BLC_transitions
	transitions grouped per super-BLC set

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

Private Types
using	set_of_states_type = std::unordered_set< state_index >

using	set_of_transitions_type = std::unordered_set< transition_index >

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 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_lb const old_constellation=null_constellation_lb, const constellation_type_lb const new_constellation=null_constellation_lb) const
	Checks the main invariant of the partition refinement algorithm.

void	display_BLC_list (const BLC_source_type &blc_src) const
	Prints the list of BLC sets as debug output.

void	print_data_structures (const std::string &header) 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_lb &B) const
	return the number of states in block `B`

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

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

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

void	multiple_swap_states_in_states_in_block (state_in_block_pointer_lb pos1, state_in_block_pointer_lb pos2, state_index count, const state_in_block_pointer_lb *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_lb out_pos)
	marks the transition indicated by `out_pos`.

void	swap_three_iterators_and_update_m_transitions (BLC_list_iterator i1, BLC_list_iterator i2, 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, simple_list< BLC_indicators_lb >::iterator new_BLC_block, simple_list< BLC_indicators_lb >::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_lb &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, simple_list< BLC_indicators_lb >::iterator new_BLC_block, simple_list< BLC_indicators_lb >::iterator old_BLC_block, const bool mark_all_transitions_in_instable_BLC_sets=false)
	Swap transition `ti` from BLC set `old_BLC_block` to BLC set `new_BLC_block`

void	update_small_subblock_counters (state_in_block_pointer_lb start_blocks, state_in_block_pointer_lb splitpoint, state_in_block_pointer_lb *end_blocks, const int split_type=SPLIT_SMALLER)
	update the smallness counters of blocks

void	update_all_small_subblock_counters (state_in_block_pointer_lb start_block, state_in_block_pointer_lb end_block)
	update the smallness counters of blocks when they are split

void	make_BLC_simple_split_off_part (BLC_source_type &BLC_source, state_in_block_pointer_lb const splitpoint, const bool mark_all_transitions_in_instable_BLC_sets, constellation_type_lb old_constellation, constellation_type_lb *const new_constellation, const int split_type=SPLIT_SMALLER)
	Splits the super-BLC sets of `BLC_source` at `splitpoint`

void	make_BLC_simple (block_type_lb &block_index, const bool mark_all_transitions_in_instable_BLC_sets=false, constellation_type_lb const old_constellation=null_constellation_lb, constellation_type_lb const new_constellation=null_constellation_lb)
	Splits the super-BLC set of `block_index` so it is a true BLC set.

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

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

void	make_stable_and_move_to_start_of_BLC (BLC_source_type &from_blc_src, const simple_list< BLC_indicators_lb >::iterator splitter)
	Makes splitter stable and moves it to the beginning of the list.

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

block_type_lb *	create_new_block (state_in_block_pointer_lb start_bottom_states, state_in_block_pointer_lb const start_non_bottom_states, state_in_block_pointer_lb *const end_states, block_type_lb &old_block_index)
	create a new block and adapt the BLC sets, and reset state counters

void	check_incoming_tau_transitions_become_noninert (block_type_lb &NewBotSt_block, state_in_block_pointer_lb start_bottom, state_in_block_pointer_lb const end_non_bottom)
	makes incoming transitions from block `NewBotSt_block` non-block-inert

BLC_indicators_lb *	next_target_constln_in_same_saC (state_in_block_pointer_lb 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

block_type_lb *	four_way_splitB (block_that_needs_refinement_type &bri, constellation_type_lb const old_constellation=null_constellation_lb, constellation_type_lb const new_constellation=null_constellation_lb)
	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
	Accumulate the number of transitions in an array.

void	stabilizeB ()
	Stabilize blocks with new bottom states.

void	refine_super_BLC (BLC_indicators_lb &small_splitter, BLC_indicators_lb *const large_splitter=nullptr)
	refine all predecessors of a super-BLC set

void	create_initial_partition ()
	create the initial partition for (branching) bisimulation

block_type_lb *	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 ()
	refines the partition until it becomes a branching bisimulation

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_lb * >	m_blocks_with_new_bottom_states
	list of blocks that contain new bottom states

block_type_lb *	m_singleton_block_with_new_bottom_states_for_debug

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

std::vector< std::pair< BLC_source_type &, simple_list< BLC_indicators_lb >::iterator > >	m_BLC_indicators_to_be_deleted
	BLC-indicators that will need to be deleted because they have become empty.

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_BLC_source_sets = 1
	counter to store the number of BLC source sets

std::vector< block_that_needs_refinement_type >	blocks_that_need_refinement
	information about blocks that need refinement

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

Detailed Description

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

implements the main algorithm for the branching bisimulation quotient

Definition at line 912 of file liblts_bisim_gj_lazy_BLC.h.

Member Typedef Documentation

◆ set_of_states_type

template<class LTS_TYPE >

using mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::set_of_states_type = std::unordered_set<state_index>

private

Definition at line 916 of file liblts_bisim_gj_lazy_BLC.h.

◆ set_of_transitions_type

template<class LTS_TYPE >

using mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::set_of_transitions_type = std::unordered_set<transition_index>

private

Definition at line 917 of file liblts_bisim_gj_lazy_BLC.h.

Constructor & Destructor Documentation

◆ bisim_partitioner_gj_lazy_BLC()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::bisim_partitioner_gj_lazy_BLC	(	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 7228 of file liblts_bisim_gj_lazy_BLC.h.

Member Function Documentation

◆ accumulate_entries()

template<class LTS_TYPE >

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

inlineprivate

Accumulate the number of transitions in an array.

During initialisation, the algorithm does a counting sort of transitions by action label: first, it counts the transitions per label, then it calls this function to find the position of transitions with a given label. After this function, transitions can be moved easily to an array in order so that they will be sorted.

Definition at line 5222 of file liblts_bisim_gj_lazy_BLC.h.

◆ change_non_bottom_state_to_bottom_state()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::change_non_bottom_state_to_bottom_state ( const fixed_vector< state_type_gj_lb >::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 3019 of file liblts_bisim_gj_lazy_BLC.h.

◆ check_data_structures()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::check_data_structures	(	const std::string &	tag,
		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 1134 of file liblts_bisim_gj_lazy_BLC.h.

◆ check_incoming_tau_transitions_become_noninert()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::check_incoming_tau_transitions_become_noninert	(	block_type_lb &	NewBotSt_block,
		state_in_block_pointer_lb *	start_bottom,
		state_in_block_pointer_lb *const	end_non_bottom
	)

inlineprivate

makes incoming transitions from block NewBotSt_block non-block-inert

Definition at line 3116 of file liblts_bisim_gj_lazy_BLC.h.

◆ check_stability()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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_lb *const	old_constellation = `null_constellation_lb`,
		const constellation_type_lb *const	new_constellation = `null_constellation_lb`
	)		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 1469 of file liblts_bisim_gj_lazy_BLC.h.

◆ check_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 1038 of file liblts_bisim_gj_lazy_BLC.h.

◆ clear_state_counters()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::clear_state_counters	(	std::vector< state_in_block_pointer_lb >::const_iterator	begin,
		std::vector< state_in_block_pointer_lb >::const_iterator const	end,
		block_type_lb &	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 3003 of file liblts_bisim_gj_lazy_BLC.h.

◆ create_initial_partition()

template<class LTS_TYPE >

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

inlineprivate

create the initial partition for (branching) bisimulation

This routine creates an initial partition based on which actions a state can reach inertly. States whose reachable actions are different cannot be (branching) bisimilar. The resulting partition contains one constellation and satisfies the main invariant:

The blocks are stable under the constellations, i.e. if a state in a block has a (non-constellation-inert) transition to a constellation, then every bottom state in the same block has a transition with the same label to the same constellation.

Definition at line 6291 of file liblts_bisim_gj_lazy_BLC.h.

◆ create_new_block()

template<class LTS_TYPE >

block_type_lb * mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::create_new_block	(	state_in_block_pointer_lb *	start_bottom_states,
		state_in_block_pointer_lb *const	start_non_bottom_states,
		state_in_block_pointer_lb *const	end_states,
		block_type_lb &	old_block_index
	)

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`

Returns: a pointer to the newly created block

Definition at line 3075 of file liblts_bisim_gj_lazy_BLC.h.

◆ display_BLC_list()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::display_BLC_list ( const BLC_source_type & blc_src ) const

inlineprivate

Prints the list of BLC sets as debug output.

Definition at line 1704 of file liblts_bisim_gj_lazy_BLC.h.

◆ finalize_minimized_LTS()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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.

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 2056 of file liblts_bisim_gj_lazy_BLC.h.

◆ four_way_splitB()

template<class LTS_TYPE >

block_type_lb * mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::four_way_splitB	(	block_that_needs_refinement_type &	bri,
		constellation_type_lb *const	old_constellation = `null_constellation_lb`,
		constellation_type_lb *const	new_constellation = `null_constellation_lb`
	)

inlineprivate

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

bri contains the main information about how a specific block should be split in up to four parts. Already all transitions in a small splitter have been visited to distribute the states. Also, some transitions of a large splitter may have been handled (including at least the transitions originating in bottom states). In this way, all bottom states have been finally assigned to one of the following three sub-blocks:

ReachAlw: states that can reach always all splitters provided
AvoidSml: states that cannot inertly reach small_splitter, in a situation when small_splitter!=nullptr. (If small_splitter==nullptr, then AvoidSml is empty.)
AvoidLrg: states that cannot inertly reach large_splitter, in a situation when large_splitter!=nullptr. (If large_splitter==nullptr, then AvoidLrg is empty.) Non-bottom states can be "potentially" assigned to one of these three sets, pending any block-inert transitions that might contradict this potential assignment. All this information is stored in bri.

The function extends the sub-blocks to non-bottom states of the block, by looking at its block-inert transitions, and possibly adds a fourth sub-block:

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.

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

Parameters

bri	information about the block being split
old_constellation	contains the old constellation from which `new_constellation` was split off recently. This parameter is needed to maintain the proper sequence of super-BLC sets in their list.
new_constellation	contains the newest constellation, whose creation causes all this work. This parameter is needed to maintain the proper sequence of super-BLC sets in their list.

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

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.

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. The macro returns true if the coroutine is aborted.

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. The macro returns true if the coroutine is aborted.

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. The macro returns true if the coroutine is aborted.

Definition at line 3266 of file liblts_bisim_gj_lazy_BLC.h.

◆ get_eq_class()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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

si	state whose equivalence class needs to be found

Returns: sequence number of the equivalence class of state si

Definition at line 2040 of file liblts_bisim_gj_lazy_BLC.h.

◆ in_same_class()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 2144 of file liblts_bisim_gj_lazy_BLC.h.

◆ is_inert_during_init()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 999 of file liblts_bisim_gj_lazy_BLC.h.

◆ is_inert_during_init_if_branching()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 991 of file liblts_bisim_gj_lazy_BLC.h.

◆ label_or_divergence()

template<class LTS_TYPE >

label_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 1007 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_aut_apply_hidden_label_map()

template<class LTS_TYPE >

static LTS_TYPE::labels_size_type mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 983 of file liblts_bisim_gj_lazy_BLC.h.

◆ make_BLC_simple()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::make_BLC_simple	(	block_type_lb &	block_index,
		const bool	mark_all_transitions_in_instable_BLC_sets = `false`,
		constellation_type_lb *const	old_constellation = `null_constellation_lb`,
		constellation_type_lb *const	new_constellation = `null_constellation_lb`
	)

inlineprivate

Splits the super-BLC set of block_index so it is a true BLC set.

Sometimes it is necessary to find exactly the transitions out of a specific block, with a given label and target constellation; then, the super-BLC set of this block needs to be split. The procedure can be called in two situations:

either as part of four_way_splitB(), namely in line 3.19 (right), when the NewBotSt coroutine has to go through all transitions in the large splitter to find states that cannot be in AvoidLrg. In this case, no transitions are marked, but it is important to keep the relationship between a small and a large splitter in other BLC sets, so that further calls to refine_super_BLC() in line 1.22 can find the correct large splitter super-BLC set. To ensure this, the parameters old_constellation and new_constellation are included. Main splitter BLC sets (with target constellation==new_constellation) follow immediately after co-splitter BLC sets (with target constellation==old_constellation).
or as part of stabilizeB(), namely in lines 5.6 or 5.42, when a large subblock with new bottom states has been found. In this case, transitions may be marked, but there is no need to keep the order of small / large splitter, as stabilizeB() does not stabilize under two splitters together. In this case, we can simplify the marking of a new BLC set that is split off from an unstable BLC set: all transitions can be marked. In this case the parameters old_constellation==nullptr and new_constellation==nullptr.

Definition at line 2942 of file liblts_bisim_gj_lazy_BLC.h.

◆ make_BLC_simple_split_off_part()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::make_BLC_simple_split_off_part	(	BLC_source_type &	BLC_source,
		state_in_block_pointer_lb *const	splitpoint,
		const bool	mark_all_transitions_in_instable_BLC_sets,
		constellation_type_lb *	old_constellation,
		constellation_type_lb *const	new_constellation,
		const int	split_type = `SPLIT_SMALLER`
	)

inlineprivate

Splits the super-BLC sets of BLC_source at splitpoint

This procedure splits the super-BLC sets into two, as one step to creating a single-block BLC source set. The procedure can be called in two situations:

either as part of four_way_splitB(), namely in line 3.19 (right), when the NewBotSt coroutine has to go through all transitions in the large splitter to find states that cannot be in AvoidLrg. In this case, no transitions are marked, but it is important to keep the relationship between a small and a large splitter in other BLC sets, so that further calls to refine_super_BLC() in line 1.22 can find the correct large splitter super-BLC set. To ensure this, the parameters old_constellation and new_constellation are included. Main splitter BLC sets (with target constellation==new_constellation) follow immediately after co-splitter BLC sets (with target constellation==old_constellation).
or as part of stabilizeB(), namely in lines 5.6 or 5.42, when a large subblock with new bottom states has been found. In this case, transitions may be marked, but there is no need to keep the order of small / large splitter, as stabilizeB() does not stabilize under two splitters together. In this case, we can simplify the marking of a new BLC set that is split off from an unstable BLC set: all transitions can be marked. In this case the parameters old_constellation==nullptr and new_constellation==nullptr.

Definition at line 2617 of file liblts_bisim_gj_lazy_BLC.h.

◆ make_stable_and_move_to_start_of_BLC()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::make_stable_and_move_to_start_of_BLC	(	BLC_source_type &	from_blc_src,
		const simple_list< BLC_indicators_lb >::iterator	splitter
	)

inlineprivate

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

Definition at line 3030 of file liblts_bisim_gj_lazy_BLC.h.

◆ mark_BLC_transition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::mark_BLC_transition ( const outgoing_transitions_it_lb out_pos )

inlineprivate

marks the transition indicated by out_pos.

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

Definition at line 2257 of file liblts_bisim_gj_lazy_BLC.h.

◆ move_nonbottom_states_to()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::move_nonbottom_states_to	(	const todo_state_vector_lb &	R,
		state_in_block_pointer_lb *	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 3050 of file liblts_bisim_gj_lazy_BLC.h.

◆ multiple_swap_states_in_states_in_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::multiple_swap_states_in_states_in_block	(	state_in_block_pointer_lb *	pos1,
		state_in_block_pointer_lb *	pos2,
		state_index	count,
		const state_in_block_pointer_lb *	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 2198 of file liblts_bisim_gj_lazy_BLC.h.

◆ next_target_constln_in_same_saC()

template<class LTS_TYPE >

BLC_indicators_lb * mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::next_target_constln_in_same_saC	(	state_in_block_pointer_lb 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 3189 of file liblts_bisim_gj_lazy_BLC.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 2027 of file liblts_bisim_gj_lazy_BLC.h.

◆ number_of_states_in_block()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::number_of_states_in_block ( const block_type_lb & B ) const

inlineprivate

return the number of states in block B

Definition at line 2161 of file liblts_bisim_gj_lazy_BLC.h.

◆ number_of_states_in_constellation()

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::number_of_states_in_constellation ( const constellation_type_lb & C ) const

inlineprivate

return the number of states in constellation C

Definition at line 2167 of file liblts_bisim_gj_lazy_BLC.h.

◆ print_data_structures()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::print_data_structures ( const std::string & header ) const

inlineprivate

Prints the partition refinement data structure as debug output.

Definition at line 1765 of file liblts_bisim_gj_lazy_BLC.h.

◆ ptr()

template<class LTS_TYPE >

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

inlineprivate

Definition at line 2150 of file liblts_bisim_gj_lazy_BLC.h.

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

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

inlineprivate

refines the partition until it becomes a branching bisimulation

This function executes the main loop of the algorithm. It assumes that the partition already satisfies the main invariant:

The blocks are stable under the constellations, i.e. if a state in a block has a (non-constellation-inert) transition to a constellation, then every bottom state in the same block has a transition with the same label to the same constellation.

However, it may be the case that blocks are finer than constellations. This routine then refines constellations and reestablishes the main invariant until every block is equal to a trivial constellation. Then the blocks are (branching) bisimulation equivalence classes.

Definition at line 6657 of file liblts_bisim_gj_lazy_BLC.h.

◆ refine_super_BLC()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::refine_super_BLC	(	BLC_indicators_lb &	small_splitter,
		BLC_indicators_lb *const	large_splitter = `nullptr`
	)

inlineprivate

refine all predecessors of a super-BLC set

The routine should be called when it becomes no longer known whether small_splitter is stable (i.e. whether, if some state has a non-constellation-inert transition in small_splitter, then every bottom state in the same block has a non-constellation-inert transition in small_splitter).

The routine goes through the transitions in small_splitter and refines every block that contains source states of these transitions. It assumes that small_splitter is small enough that one is allowed to visit all its transitions (typically because the target states are in a constellation that is known to be small).

If also large_splitter is given, the routine assumes that every block with non-constellation-inert transitions in small_splitter satisfies the condition: every bottom state has at least a non-constellation-inert transition in one of the two super-BLC sets given. The routine then simultaneously refines as required by large_splitter. However, it is not assumed that large_splitter is small, so the time spent on visiting its transitions is accounted for by other means.

If new bottom states are found, they are isolated by moving them to separate blocks, but these blocks are not further stabilized. A later call to stabilizeB() is required for these. The routine also skips blocks that are already known to contain new bottom states.

Definition at line 6079 of file liblts_bisim_gj_lazy_BLC.h.

◆ select_and_remove_a_block_in_a_non_trivial_constellation()

template<class LTS_TYPE >

block_type_lb * mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 6598 of file liblts_bisim_gj_lazy_BLC.h.

◆ stabilizeB()

template<class LTS_TYPE >

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

inlineprivate

Stabilize blocks with new bottom states.

Calls to refine_super_BLC() and four_way_splitB() may find new bottom states, i.e. states that previously had block-inert transitions, but by refining the blocks these transitions all became non-block-inert. Such states are isolated by moving them to separate blocks (which are appropriately marked), but then such blocks are left alone until the next call to stabilizeB(). This latter routine then specifically stabilizes a block with new bottom states under all reachable labels and constellations.

This variant of stabilizeB() tries to exploit the fact that many blocks with new bottom states are rather small subblocks of their last split; therefore a simple way of working may be sufficient. Only if a block with new bottom states is large, one needs to find the single-block BLC sets to stabilize it. This is one of the situations where "laziness" is not possible.

Definition at line 5262 of file liblts_bisim_gj_lazy_BLC.h.

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_block()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::swap_in_the_doubly_linked_list_LBC_in_blocks_new_block	(	const transition_index	ti,
		simple_list< BLC_indicators_lb >::iterator	new_BLC_block,
		simple_list< BLC_indicators_lb >::iterator	old_BLC_block,
		const bool	mark_all_transitions_in_instable_BLC_sets = `false`
	)

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
mark_all_transitions_in_instable_BLC_sets	if true, all transitions in newly created super-BLC sets (split off from instable super-BLC sets) are marked. Otherwise, just marked transitions will remain marked.

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.

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

Definition at line 2452 of file liblts_bisim_gj_lazy_BLC.h.

◆ swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::swap_in_the_doubly_linked_list_LBC_in_blocks_new_constellation	(	const transition_index	ti,
		simple_list< BLC_indicators_lb >::iterator	new_BLC_block,
		simple_list< BLC_indicators_lb >::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 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 2337 of file liblts_bisim_gj_lazy_BLC.h.

◆ swap_states_in_states_in_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::swap_states_in_states_in_block	(	state_in_block_pointer_lb *	pos1,
		state_in_block_pointer_lb *	pos2
	)

inlineprivate

swap the contents of pos1 and pos2 if they are different

Definition at line 2182 of file liblts_bisim_gj_lazy_BLC.h.

◆ swap_states_in_states_in_block_never_equal()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::swap_states_in_states_in_block_never_equal	(	state_in_block_pointer_lb *	pos1,
		state_in_block_pointer_lb *	pos2
	)

inlineprivate

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

Definition at line 2173 of file liblts_bisim_gj_lazy_BLC.h.

◆ swap_three_iterators_and_update_m_transitions()

template<class LTS_TYPE >

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

inlineprivate

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

Definition at line 2294 of file liblts_bisim_gj_lazy_BLC.h.

◆ update_all_small_subblock_counters()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::update_all_small_subblock_counters	(	state_in_block_pointer_lb *	start_block,
		state_in_block_pointer_lb *	end_block
	)

inlineprivate

update the smallness counters of blocks when they are split

This function should be called just after the block covering the states [start_block, end_block) is refined. Then the smallness counters of all (new) blocks in this range are adapted if allowed.

Definition at line 2565 of file liblts_bisim_gj_lazy_BLC.h.

◆ update_small_subblock_counters()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::update_small_subblock_counters	(	state_in_block_pointer_lb *	start_blocks,
		state_in_block_pointer_lb *	splitpoint,
		state_in_block_pointer_lb *	end_blocks,
		const int	split_type = `SPLIT_SMALLER`
	)

inlineprivate

update the smallness counters of blocks

This function should be called when the slice [start_blocks, end_blocks) is split at splitpoint, for example to split a constellation or a super-BLC source. Then the smallness counters of all blocks in this range are adapted if allowed.

Definition at line 2512 of file liblts_bisim_gj_lazy_BLC.h.

◆ update_the_doubly_linked_list_LBC_new_constellation()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::update_the_doubly_linked_list_LBC_new_constellation	(	block_type_lb &	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.

Definition at line 2382 of file liblts_bisim_gj_lazy_BLC.h.

Member Data Documentation

◆ blocks_that_need_refinement

template<class LTS_TYPE >

std::vector<block_that_needs_refinement_type> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::blocks_that_need_refinement

private

information about blocks that need refinement

Every block that is refined

Definition at line 6051 of file liblts_bisim_gj_lazy_BLC.h.

◆ end_initial_part

template<class LTS_TYPE >

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

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

Definition at line 7215 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_aut

template<class LTS_TYPE >

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

automaton that is being reduced

Definition at line 922 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_BLC_indicators_to_be_deleted

template<class LTS_TYPE >

std::vector<std::pair<BLC_source_type&, simple_list<BLC_indicators_lb>::iterator> > mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_BLC_indicators_to_be_deleted

private

BLC-indicators that will need to be deleted because they have become empty.

When a super-BLC set is split up into multiple parts during a call to refine_super_BLC(), we sometimes cannot delete super-BLC sets that have become empty, because there may be pointers pointing at it. In that situation we add the set to this list so we will remember to delete it later.

Definition at line 968 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_BLC_transitions

template<class LTS_TYPE >

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

transitions grouped per super-BLC set

Definition at line 950 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_blocks_with_new_bottom_states

template<class LTS_TYPE >

std::vector<block_type_lb*> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_blocks_with_new_bottom_states

private

list of blocks that contain new bottom states

Definition at line 953 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_branching

template<class LTS_TYPE >

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

private

true iff branching (not strong) bisimulation has been requested

Definition at line 971 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_non_trivial_constellations

template<class LTS_TYPE >

std::vector<constellation_type_lb*> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_non_trivial_constellations

private

The following variable contains all non-trivial constellations.

Definition at line 959 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_outgoing_transitions

template<class LTS_TYPE >

fixed_vector<outgoing_transition_type_lb> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 933 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_preserve_divergence

template<class LTS_TYPE >

const bool mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< 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 978 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_singleton_block_with_new_bottom_states_for_debug

template<class LTS_TYPE >

block_type_lb* mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_singleton_block_with_new_bottom_states_for_debug

private

Initial value:

=

null_block_lb

mcrl2::lts::detail::bisimulation_gj_lazy_BLC::null_block_lb

constexpr block_type_lb * null_block_lb

Definition liblts_bisim_gj_lazy_BLC.h:100

Definition at line 955 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_states

template<class LTS_TYPE >

fixed_vector<state_type_gj_lb> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_states

information about states

Definition at line 926 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_states_in_blocks

template<class LTS_TYPE >

fixed_vector<state_in_block_pointer_lb> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_states_in_blocks

states grouped per constellation and block

Definition at line 941 of file liblts_bisim_gj_lazy_BLC.h.

◆ m_transitions

template<class LTS_TYPE >

fixed_vector<transition_type_lb> mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::m_transitions

transitions ordered per target state

This array is used to go through the incoming transitions of a state. It has the same order as the array m_aut.get_transitions().

Definition at line 938 of file liblts_bisim_gj_lazy_BLC.h.

◆ no_of_BLC_source_sets

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::no_of_BLC_source_sets = 1

private

counter to store the number of BLC source sets

Definition at line 2591 of file liblts_bisim_gj_lazy_BLC.h.

◆ no_of_blocks

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::no_of_blocks = 1

number of blocks that have been constructed until now

Definition at line 944 of file liblts_bisim_gj_lazy_BLC.h.

◆ no_of_constellations

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::no_of_constellations = 1

number of constellations that have been constructed until now

Definition at line 947 of file liblts_bisim_gj_lazy_BLC.h.

◆ no_of_new_bottom_states

template<class LTS_TYPE >

state_index mcrl2::lts::detail::bisim_partitioner_gj_lazy_BLC< LTS_TYPE >::no_of_new_bottom_states = 0

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 6634 of file liblts_bisim_gj_lazy_BLC.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_gj_lazy_BLC.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_lazy_BLC()

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()

◆ 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_BLC_simple()

◆ make_BLC_simple_split_off_part()

◆ 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()

◆ print_data_structures()

◆ ptr()

◆ refine_partition_until_it_becomes_stable()

◆ refine_super_BLC()

◆ 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()

◆ swap_states_in_states_in_block_never_equal()

◆ swap_three_iterators_and_update_m_transitions()

◆ update_all_small_subblock_counters()

◆ update_small_subblock_counters()

◆ update_the_doubly_linked_list_LBC_new_constellation()

Member Data Documentation

◆ blocks_that_need_refinement

◆ 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_singleton_block_with_new_bottom_states_for_debug

◆ m_states

◆ m_states_in_blocks

◆ m_transitions

◆ no_of_BLC_source_sets

◆ no_of_blocks

◆ no_of_constellations

◆ no_of_new_bottom_states