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

#include <liblts_bisim_gj.h>

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

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.

Public Attributes
LTS_TYPE &	m_aut
	automaton that is being reduced

std::vector< state_type_gj >	m_states

std::vector< transition_pointer_pair >	m_outgoing_transitions

std::vector< transition_type >	m_transitions

std::vector< state_index >	m_states_in_blocks

std::vector< block_type >	m_blocks

std::vector< constellation_type >	m_constellations

std::vector< transition_index >	m_BLC_transitions

Protected Types
typedef std::unordered_set< state_index >	set_of_states_type

typedef std::unordered_set< transition_index >	set_of_transitions_type

typedef std::vector< constellation_index >	set_of_constellations_type

typedef std::unordered_map< std::pair< label_index, constellation_index >, set_of_states_type >	label_constellation_to_set_of_states_map

typedef std::unordered_map< std::pair< block_index, label_index >, transition_index >	block_label_to_size_t_map

Protected Member Functions
void	check_transitions (const bool check_temporary_complexity_counters, const bool check_block_to_constellation=true)

bool	check_data_structures (const std::string &tag, const bool initialisation=false, const bool check_temporary_complexity_counters=true)

bool	check_stability (const std::string &tag, const std::vector< label_index > const todo_stack_labels=nullptr, const block_label_to_size_t_map const block_label_to_cotransition=nullptr, const constellation_index old_constellation=-1)

void	add_work_to_same_saC (const bool initialisation, const state_index si, const label_index a, const constellation_index C, const enum check_complexity::counter_type ctr, const unsigned max_value)

void	display_BLC_list (const block_index bi) const

void	print_data_structures (const std::string &header, const bool initialisation=false) const

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

std::string	ptr (const transition_index ti) const

state_index	number_of_states_in_block (const block_index B) const

state_index	number_of_states_in_constellation (const constellation_index C) const

void	swap_states_in_states_in_block (typename std::vector< state_index >::iterator pos1, typename std::vector< state_index >::iterator pos2)

void	swap_states_in_states_in_block (typename std::vector< state_index >::iterator pos1, typename std::vector< state_index >::iterator pos2, typename std::vector< state_index >::iterator pos3)

block_index	split_block_B_into_R_and_BminR (const block_index B, const todo_state_vector &R, std::function< void(const state_index)> update_Ptilde)

bool	swap_in_the_doubly_linked_list_LBC_in_blocks (const transition_index ti, linked_list< BLC_indicators >::iterator new_BLC_block, linked_list< BLC_indicators >::iterator old_BLC_block)

void	update_the_doubly_linked_list_LBC_new_constellation (const block_index index_block_B, const transition &t, const transition_index ti)

transition_index	update_the_doubly_linked_list_LBC_new_block (const block_index old_bi, const block_index new_bi, const transition_index ti)

void	clear_state_counters (bool restrict_to_R=false)

template<std::size_t VARIANT, class MARKED_STATE_TRANSITION_ITERATOR , class UNMARKED_STATE_ITERATOR >
block_index	simple_splitB (const block_index B, const MARKED_STATE_TRANSITION_ITERATOR M_begin, const MARKED_STATE_TRANSITION_ITERATOR M_end, const UNMARKED_STATE_ITERATOR M_co_begin, const UNMARKED_STATE_ITERATOR M_co_end, const bool initialisation, const label_index a, const constellation_index C, bool &M_in_bi, std::function< void(const state_index)> update_Ptilde)

void	make_transition_non_inert (const transition &t)

void	change_non_bottom_state_to_bottom_state (const state_index si, const bool initialisation=false)

template<std::size_t VARIANT, class MARKED_STATE_TRANSITION_ITERATOR , class UNMARKED_STATE_ITERATOR >
block_index	splitB (const block_index B, const MARKED_STATE_TRANSITION_ITERATOR M_begin, const MARKED_STATE_TRANSITION_ITERATOR M_end, const UNMARKED_STATE_ITERATOR M_co_begin, const UNMARKED_STATE_ITERATOR M_co_end, const label_index a, const constellation_index C, bool &M_in_new_block, std::function< void(const block_index, const block_index, const transition_index, const transition_index)> update_block_label_to_cotransition, const bool initialisation=false, std::function< void(const transition_index, const transition_index, const block_index)> process_transition=[](const transition_index, const transition_index, const block_index){}, std::function< void(const state_index)> update_Ptilde=[](const state_index){})

void	accumulate_entries_into_not_investigated (std::vector< label_count_sum_triple > &action_counter, const std::vector< block_index > &todo_stack)

void	accumulate_entries (std::vector< transition_index > &counter)

void	reset_entries (std::vector< label_count_sum_triple > &action_counter, std::vector< block_index > &todo_stack)

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

void	group_in_situ (const std::vector< transition_index >::iterator begin, const std::vector< transition_index >::iterator end, std::vector< block_index > &todo_stack, std::vector< label_count_sum_triple > &value_counter)

void	create_initial_partition ()

void	stabilizeB ()

void	maintain_block_label_to_cotransition (const block_index old_block, const block_index new_block, const transition_index moved_transition, const transition_index alternative_transition, block_label_to_size_t_map &block_label_to_cotransition, const constellation_index ci) const

transition_index	find_inert_co_transition_for_block (const block_index index_block_B, const constellation_index old_constellation)

bool	state_has_outgoing_co_transition (const transition_index transition_to_bi, const constellation_index old_constellation)

bool	some_bottom_state_has_no_outgoing_co_transition (block_index B, std::vector< transition_index >::iterator transitions_begin, std::vector< transition_index >::iterator transitions_end, const constellation_index old_constellation, std::vector< state_index >::iterator &first_unmarked_bottom_state)

bool	W_empty (const set_of_states_type &W, const set_of_states_type &aux, const label_index a, const constellation_index C, std::vector< state_index >::iterator &first_unmarked_bottom_state)

bool	not_all_bottom_states_are_touched (const block_index bi, const std::vector< transition_index >::iterator begin, const std::vector< transition_index >::iterator end, std::vector< state_index >::iterator &first_unmarked_bottom_state)

bool	hatU_does_not_cover_B_bottom (const block_index index_block_B, const constellation_index old_constellation, std::vector< state_index >::iterator first_unmarked_bottom_state)

block_index	select_and_remove_a_block_in_a_non_trivial_constellation (constellation_index &ci)

void	refine_partition_until_it_becomes_stable ()

Protected Attributes
std::vector< state_index >	m_P

todo_state_vector	m_R

todo_state_vector	m_U

std::vector< state_index >	m_U_counter_reset_vector

set_of_constellations_type	m_non_trivial_constellations

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

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 633 of file liblts_bisim_gj.h.

Member Typedef Documentation

◆ block_label_to_size_t_map

template<class LTS_TYPE >

typedef std::unordered_map<std::pair<block_index, label_index>, transition_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::block_label_to_size_t_map

protected

Definition at line 643 of file liblts_bisim_gj.h.

◆ label_constellation_to_set_of_states_map

template<class LTS_TYPE >

typedef std::unordered_map<std::pair<label_index, constellation_index>, set_of_states_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::label_constellation_to_set_of_states_map

protected

Definition at line 642 of file liblts_bisim_gj.h.

◆ set_of_constellations_type

template<class LTS_TYPE >

typedef std::vector<constellation_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::set_of_constellations_type

protected

Definition at line 639 of file liblts_bisim_gj.h.

◆ 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

protected

Definition at line 637 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

protected

Definition at line 638 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 destroys the transitions on the LTS (to save memory) but 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 1291 of file liblts_bisim_gj.h.

Member Function Documentation

◆ accumulate_entries() [1/2]

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

inlineprotected

Definition at line 2634 of file liblts_bisim_gj.h.

◆ accumulate_entries() [2/2]

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::accumulate_entries ( std::vector< transition_index > & counter )

inlineprotected

Definition at line 2610 of file liblts_bisim_gj.h.

◆ accumulate_entries_into_not_investigated()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::accumulate_entries_into_not_investigated	(	std::vector< label_count_sum_triple > &	action_counter,
		const std::vector< block_index > &	todo_stack
	)

inlineprotected

Definition at line 2596 of file liblts_bisim_gj.h.

◆ add_work_to_same_saC()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::add_work_to_same_saC	(	const bool	initialisation,
		const state_index	si,
		const label_index	a,
		const constellation_index	C,
		const enum check_complexity::counter_type	ctr,
		const unsigned	max_value
	)

inlineprotected

Definition at line 1091 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 state_index	si,
		const bool	initialisation = `false`
	)

inlineprotected

Definition at line 2302 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`
	)

inlineprotected

Definition at line 761 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< label_index > *const	todo_stack_labels = `nullptr`,
		const block_label_to_size_t_map *const	block_label_to_cotransition = `nullptr`,
		const constellation_index	old_constellation = `-1`
	)

inlineprotected

Definition at line 966 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	check_temporary_complexity_counters,
		const bool	check_block_to_constellation = `true`
	)

inlineprotected

Definition at line 686 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 ( bool restrict_to_R = false )

inlineprotected

Definition at line 1782 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 ( )

inlineprotected

Definition at line 2744 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_index bi ) const

inlineprotected

Definition at line 1132 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 1349 of file liblts_bisim_gj.h.

◆ find_inert_co_transition_for_block()

template<class LTS_TYPE >

transition_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::find_inert_co_transition_for_block	(	const block_index	index_block_B,
		const constellation_index	old_constellation
	)

inlineprotected

Definition at line 3456 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 1330 of file liblts_bisim_gj.h.

◆ group_in_situ()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::group_in_situ	(	const std::vector< transition_index >::iterator	begin,
		const std::vector< transition_index >::iterator	end,
		std::vector< block_index > &	todo_stack,
		std::vector< label_count_sum_triple > &	value_counter
	)

inlineprotected

Definition at line 2650 of file liblts_bisim_gj.h.

◆ hatU_does_not_cover_B_bottom()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::hatU_does_not_cover_B_bottom	(	const block_index	index_block_B,
		const constellation_index	old_constellation,
		std::vector< state_index >::iterator	first_unmarked_bottom_state
	)

inlineprotected

Definition at line 3695 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 1416 of file liblts_bisim_gj.h.

◆ maintain_block_label_to_cotransition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::maintain_block_label_to_cotransition	(	const block_index	old_block,
		const block_index	new_block,
		const transition_index	moved_transition,
		const transition_index	alternative_transition,
		block_label_to_size_t_map &	block_label_to_cotransition,
		const constellation_index	ci
	)		const

inlineprotected

Definition at line 3412 of file liblts_bisim_gj.h.

◆ make_transition_non_inert()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::make_transition_non_inert ( const transition & t )

inlineprotected

Definition at line 2295 of file liblts_bisim_gj.h.

◆ not_all_bottom_states_are_touched()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::not_all_bottom_states_are_touched	(	const block_index	bi,
		const std::vector< transition_index >::iterator	begin,
		const std::vector< transition_index >::iterator	end,
		std::vector< state_index >::iterator &	first_unmarked_bottom_state
	)

inlineprotected

Definition at line 3647 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 1317 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_index B ) const

inlineprotected

Definition at line 1437 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_index C ) const

inlineprotected

Definition at line 1442 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

inlineprotected

Definition at line 1169 of file liblts_bisim_gj.h.

◆ ptr() [1/2]

template<class LTS_TYPE >

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

inlineprotected

Definition at line 1422 of file liblts_bisim_gj.h.

◆ ptr() [2/2]

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::ptr ( const transition_index ti ) const

inlineprotected

Definition at line 1427 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 ( )

inlineprotected

Definition at line 3785 of file liblts_bisim_gj.h.

◆ reset_entries()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::reset_entries	(	std::vector< label_count_sum_triple > &	action_counter,
		std::vector< block_index > &	todo_stack
	)

inlineprotected

Definition at line 2621 of file liblts_bisim_gj.h.

◆ select_and_remove_a_block_in_a_non_trivial_constellation()

template<class LTS_TYPE >

block_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::select_and_remove_a_block_in_a_non_trivial_constellation ( constellation_index & ci )

inlineprotected

Definition at line 3764 of file liblts_bisim_gj.h.

◆ simple_splitB()

template<class LTS_TYPE >

template<std::size_t VARIANT, class MARKED_STATE_TRANSITION_ITERATOR , class UNMARKED_STATE_ITERATOR >

block_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::simple_splitB	(	const block_index	B,
		const MARKED_STATE_TRANSITION_ITERATOR	M_begin,
		const MARKED_STATE_TRANSITION_ITERATOR	M_end,
		const UNMARKED_STATE_ITERATOR	M_co_begin,
		const UNMARKED_STATE_ITERATOR	M_co_end,
		const bool	initialisation,
		const label_index	a,
		const constellation_index	C,
		bool &	M_in_bi,
		std::function< void(const state_index)>	update_Ptilde
	)

inlineprotected

Definition at line 1818 of file liblts_bisim_gj.h.

◆ some_bottom_state_has_no_outgoing_co_transition()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::some_bottom_state_has_no_outgoing_co_transition	(	block_index	B,
		std::vector< transition_index >::iterator	transitions_begin,
		std::vector< transition_index >::iterator	transitions_end,
		const constellation_index	old_constellation,
		std::vector< state_index >::iterator &	first_unmarked_bottom_state
	)

inlineprotected

Definition at line 3516 of file liblts_bisim_gj.h.

◆ split_block_B_into_R_and_BminR()

template<class LTS_TYPE >

block_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::split_block_B_into_R_and_BminR	(	const block_index	B,
		const todo_state_vector &	R,
		std::function< void(const state_index)>	update_Ptilde
	)

inlineprotected

Definition at line 1482 of file liblts_bisim_gj.h.

◆ splitB()

template<class LTS_TYPE >

template<std::size_t VARIANT, class MARKED_STATE_TRANSITION_ITERATOR , class UNMARKED_STATE_ITERATOR >

block_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::splitB	(	const block_index	B,
		const MARKED_STATE_TRANSITION_ITERATOR	M_begin,
		const MARKED_STATE_TRANSITION_ITERATOR	M_end,
		const UNMARKED_STATE_ITERATOR	M_co_begin,
		const UNMARKED_STATE_ITERATOR	M_co_end,
		const label_index	a,
		const constellation_index	C,
		bool &	M_in_new_block,
		std::function< void(const block_index, const block_index, const transition_index, const transition_index)>	update_block_label_to_cotransition,
		const bool	initialisation = `false`,
		std::function< void(const transition_index, const transition_index, const block_index)>	process_transition = `[](const transition_index, const transition_index, const block_index){}`,
		std::function< void(const state_index)>	update_Ptilde = `[](const state_index){}`
	)

inlineprotected

Definition at line 2355 of file liblts_bisim_gj.h.

◆ stabilizeB()

template<class LTS_TYPE >

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

inlineprotected

Definition at line 3166 of file liblts_bisim_gj.h.

◆ state_has_outgoing_co_transition()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::state_has_outgoing_co_transition	(	const transition_index	transition_to_bi,
		const constellation_index	old_constellation
	)

inlineprotected

Definition at line 3486 of file liblts_bisim_gj.h.

◆ swap_in_the_doubly_linked_list_LBC_in_blocks()

template<class LTS_TYPE >

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

inlineprotected

Definition at line 1592 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	(	typename std::vector< state_index >::iterator	pos1,
		typename std::vector< state_index >::iterator	pos2
	)

inlineprotected

Definition at line 1447 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	(	typename std::vector< state_index >::iterator	pos1,
		typename std::vector< state_index >::iterator	pos2,
		typename std::vector< state_index >::iterator	pos3
	)

inlineprotected

Definition at line 1458 of file liblts_bisim_gj.h.

◆ update_the_doubly_linked_list_LBC_new_block()

template<class LTS_TYPE >

transition_index mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::update_the_doubly_linked_list_LBC_new_block	(	const block_index	old_bi,
		const block_index	new_bi,
		const transition_index	ti
	)

inlineprotected

Definition at line 1709 of file liblts_bisim_gj.h.

◆ update_the_doubly_linked_list_LBC_new_constellation()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::update_the_doubly_linked_list_LBC_new_constellation	(	const block_index	index_block_B,
		const transition &	t,
		const transition_index	ti
	)

inlineprotected

Definition at line 1639 of file liblts_bisim_gj.h.

◆ W_empty()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::W_empty	(	const set_of_states_type &	W,
		const set_of_states_type &	aux,
		const label_index	a,
		const constellation_index	C,
		std::vector< state_index >::iterator &	first_unmarked_bottom_state
	)

inlineprotected

Definition at line 3585 of file liblts_bisim_gj.h.

Member Data Documentation

◆ 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 649 of file liblts_bisim_gj.h.

◆ m_BLC_transitions

template<class LTS_TYPE >

std::vector<transition_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_BLC_transitions

Definition at line 661 of file liblts_bisim_gj.h.

◆ m_blocks

template<class LTS_TYPE >

std::vector<block_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_blocks

Definition at line 659 of file liblts_bisim_gj.h.

◆ m_branching

template<class LTS_TYPE >

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

protected

true iff branching (not strong) bisimulation has been requested

Definition at line 674 of file liblts_bisim_gj.h.

◆ m_constellations

template<class LTS_TYPE >

std::vector<constellation_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_constellations

Definition at line 660 of file liblts_bisim_gj.h.

◆ m_non_trivial_constellations

template<class LTS_TYPE >

set_of_constellations_type mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_non_trivial_constellations

protected

Definition at line 670 of file liblts_bisim_gj.h.

◆ m_outgoing_transitions

template<class LTS_TYPE >

std::vector<transition_pointer_pair> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_outgoing_transitions

Definition at line 654 of file liblts_bisim_gj.h.

◆ m_P

template<class LTS_TYPE >

std::vector<state_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_P

protected

Definition at line 663 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

protected

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 681 of file liblts_bisim_gj.h.

◆ m_R

template<class LTS_TYPE >

todo_state_vector mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_R

protected

Definition at line 667 of file liblts_bisim_gj.h.

◆ m_states

template<class LTS_TYPE >

std::vector<state_type_gj> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_states

Definition at line 652 of file liblts_bisim_gj.h.

◆ m_states_in_blocks

template<class LTS_TYPE >

std::vector<state_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_states_in_blocks

Definition at line 658 of file liblts_bisim_gj.h.

◆ m_transitions

template<class LTS_TYPE >

std::vector<transition_type> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_transitions

Definition at line 657 of file liblts_bisim_gj.h.

◆ m_U

template<class LTS_TYPE >

todo_state_vector mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_U

protected

Definition at line 667 of file liblts_bisim_gj.h.

◆ m_U_counter_reset_vector

template<class LTS_TYPE >

std::vector<state_index> mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >::m_U_counter_reset_vector

protected

Definition at line 668 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

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ block_label_to_size_t_map

◆ label_constellation_to_set_of_states_map

◆ set_of_constellations_type

◆ set_of_states_type

◆ set_of_transitions_type

Constructor & Destructor Documentation

◆ bisim_partitioner_gj()

Member Function Documentation

◆ accumulate_entries() [1/2]

◆ accumulate_entries() [2/2]

◆ accumulate_entries_into_not_investigated()

◆ add_work_to_same_saC()

◆ change_non_bottom_state_to_bottom_state()

◆ check_data_structures()

◆ check_stability()

◆ check_transitions()

◆ clear_state_counters()

◆ create_initial_partition()

◆ display_BLC_list()

◆ finalize_minimized_LTS()

◆ find_inert_co_transition_for_block()

◆ get_eq_class()

◆ group_in_situ()

◆ hatU_does_not_cover_B_bottom()

◆ in_same_class()

◆ maintain_block_label_to_cotransition()

◆ make_transition_non_inert()

◆ not_all_bottom_states_are_touched()

◆ num_eq_classes()

◆ number_of_states_in_block()

◆ number_of_states_in_constellation()

◆ print_data_structures()

◆ ptr() [1/2]

◆ ptr() [2/2]

◆ refine_partition_until_it_becomes_stable()

◆ reset_entries()

◆ select_and_remove_a_block_in_a_non_trivial_constellation()

◆ simple_splitB()

◆ some_bottom_state_has_no_outgoing_co_transition()

◆ split_block_B_into_R_and_BminR()

◆ splitB()

◆ stabilizeB()

◆ state_has_outgoing_co_transition()

◆ swap_in_the_doubly_linked_list_LBC_in_blocks()

◆ swap_states_in_states_in_block() [1/2]

◆ swap_states_in_states_in_block() [2/2]

◆ update_the_doubly_linked_list_LBC_new_block()

◆ update_the_doubly_linked_list_LBC_new_constellation()

◆ W_empty()

Member Data Documentation

◆ m_aut

◆ m_BLC_transitions

◆ m_blocks

◆ m_branching

◆ m_constellations

◆ m_non_trivial_constellations

◆ m_outgoing_transitions

◆ m_P

◆ m_preserve_divergence

◆ m_R

◆ m_states

◆ m_states_in_blocks

◆ m_transitions

◆ m_U

◆ m_U_counter_reset_vector