Classes
class	B_to_C_descriptor

class	B_to_C_entry

class	bisim_partitioner_gjkw_initialise_helper
	helps with initialising the refinable partition data structure More...

class	block_t
	stores information about a block More...

class	constln_t
	stores information about a constellation More...

class	fixed_vector

class	part_state_t
	refinable partition data structure More...

class	part_trans_t

class	pred_entry

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

class	succ_entry

Typedefs
typedef state_info_entry *	state_info_ptr

typedef const state_info_entry *	state_info_const_ptr

typedef fixed_vector< state_info_ptr >	permutation_t

typedef permutation_t::iterator	permutation_iter_t

typedef permutation_t::const_iterator	permutation_const_iter_t

typedef fixed_vector< B_to_C_entry >::iterator	B_to_C_iter_t

typedef fixed_vector< pred_entry >::iterator	pred_iter_t

typedef fixed_vector< succ_entry >::iterator	succ_iter_t

typedef fixed_vector< B_to_C_entry >::const_iterator	B_to_C_const_iter_t

typedef fixed_vector< pred_entry >::const_iterator	pred_const_iter_t

typedef fixed_vector< succ_entry >::const_iterator	succ_const_iter_t

typedef std::list< B_to_C_descriptor >	B_to_C_desc_list

typedef B_to_C_desc_list::iterator	B_to_C_desc_iter_t

typedef B_to_C_desc_list::const_iterator	B_to_C_desc_const_iter_t

Functions
static void	swap_permutation (permutation_iter_t s1, permutation_iter_t s2)
	swap two permutations

static void	blue_is_smaller (block_t BlueB, block_t RedB, const constln_t *NewC)
	moves temporary counters to normal ones if the blue block is smaller

static void	red_is_smaller (block_t BlueB, block_t RedB)
	moves temporary counters to normal ones if the red block is smaller

Typedef Documentation

◆ B_to_C_const_iter_t

typedef fixed_vector<B_to_C_entry>::const_iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_const_iter_t

Definition at line 144 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_const_iter_t

typedef B_to_C_desc_list::const_iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_const_iter_t

Definition at line 150 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_iter_t

typedef B_to_C_desc_list::iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_iter_t

Definition at line 149 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_list

typedef std::list<B_to_C_descriptor> mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_list

Definition at line 148 of file liblts_bisim_gjkw.h.

◆ B_to_C_iter_t

typedef fixed_vector<B_to_C_entry>::iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_iter_t

Definition at line 140 of file liblts_bisim_gjkw.h.

◆ permutation_const_iter_t

typedef permutation_t::const_iterator mcrl2::lts::detail::bisim_gjkw::permutation_const_iter_t

Definition at line 132 of file liblts_bisim_gjkw.h.

◆ permutation_iter_t

typedef permutation_t::iterator mcrl2::lts::detail::bisim_gjkw::permutation_iter_t

Definition at line 131 of file liblts_bisim_gjkw.h.

◆ permutation_t

typedef fixed_vector<state_info_ptr> mcrl2::lts::detail::bisim_gjkw::permutation_t

Definition at line 130 of file liblts_bisim_gjkw.h.

◆ pred_const_iter_t

typedef fixed_vector<pred_entry>::const_iterator mcrl2::lts::detail::bisim_gjkw::pred_const_iter_t

Definition at line 145 of file liblts_bisim_gjkw.h.

◆ pred_iter_t

typedef fixed_vector<pred_entry>::iterator mcrl2::lts::detail::bisim_gjkw::pred_iter_t

Definition at line 141 of file liblts_bisim_gjkw.h.

◆ state_info_const_ptr

typedef const state_info_entry* mcrl2::lts::detail::bisim_gjkw::state_info_const_ptr

Definition at line 119 of file liblts_bisim_gjkw.h.

◆ state_info_ptr

typedef state_info_entry* mcrl2::lts::detail::bisim_gjkw::state_info_ptr

Definition at line 118 of file liblts_bisim_gjkw.h.

◆ succ_const_iter_t

typedef fixed_vector<succ_entry>::const_iterator mcrl2::lts::detail::bisim_gjkw::succ_const_iter_t

Definition at line 146 of file liblts_bisim_gjkw.h.

◆ succ_iter_t

typedef fixed_vector<succ_entry>::iterator mcrl2::lts::detail::bisim_gjkw::succ_iter_t

Definition at line 142 of file liblts_bisim_gjkw.h.

Function Documentation

◆ blue_is_smaller()

static void mcrl2::lts::detail::bisim_gjkw::blue_is_smaller	(	block_t *	BlueB,
		block_t *	RedB,
		const constln_t *	NewC
	)

static

moves temporary counters to normal ones if the blue block is smaller

When a refinement has finished and the blue block turns out to be smaller, this function moves the corresponding temporary work to the normal counters and cancels the work on the red state counters.

Parameters

BlueB	pointer to the blue block
RedB	pointer to the red block
NewC	(only needed if called after the refinement in line 2.26) pointer to the constellation NewC, i. e. the constellation that was used as the basis of marking states. If blue_is_smaller() is called from another place, this parameter should be nullptr.

Definition at line 2135 of file liblts_bisim_gjkw.cpp.

◆ red_is_smaller()

static void mcrl2::lts::detail::bisim_gjkw::red_is_smaller	(	block_t *	BlueB,
		block_t *	RedB
	)

static

moves temporary counters to normal ones if the red block is smaller

When a refinement has finished and the red block turns out to be smaller, this function moves the corresponding temporary work to the normal counters and cancels the work on the blue state counters.