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	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
using	state_info_ptr = state_info_entry *

using	state_info_const_ptr = const state_info_entry *

using	permutation_t = fixed_vector< state_info_ptr >

using	permutation_iter_t = permutation_t::iterator

using	permutation_const_iter_t = permutation_t::const_iterator

using	B_to_C_iter_t = fixed_vector< B_to_C_entry >::iterator

using	pred_iter_t = fixed_vector< pred_entry >::iterator

using	succ_iter_t = fixed_vector< succ_entry >::iterator

using	B_to_C_const_iter_t = fixed_vector< B_to_C_entry >::const_iterator

using	pred_const_iter_t = fixed_vector< pred_entry >::const_iterator

using	succ_const_iter_t = fixed_vector< succ_entry >::const_iterator

using	B_to_C_desc_list = std::list< B_to_C_descriptor >

using	B_to_C_desc_iter_t = B_to_C_desc_list::iterator

using	B_to_C_desc_const_iter_t = B_to_C_desc_list::const_iterator

Functions
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

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

Typedef Documentation

◆ B_to_C_const_iter_t

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

Definition at line 141 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_const_iter_t

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

Definition at line 147 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_iter_t

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

Definition at line 146 of file liblts_bisim_gjkw.h.

◆ B_to_C_desc_list

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

Definition at line 145 of file liblts_bisim_gjkw.h.

◆ B_to_C_iter_t

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

Definition at line 137 of file liblts_bisim_gjkw.h.

◆ permutation_const_iter_t

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

Definition at line 129 of file liblts_bisim_gjkw.h.

◆ permutation_iter_t

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

Definition at line 128 of file liblts_bisim_gjkw.h.

◆ permutation_t

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

Definition at line 127 of file liblts_bisim_gjkw.h.

◆ pred_const_iter_t

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

Definition at line 142 of file liblts_bisim_gjkw.h.

◆ pred_iter_t

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

Definition at line 138 of file liblts_bisim_gjkw.h.

◆ state_info_const_ptr

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

Definition at line 116 of file liblts_bisim_gjkw.h.

◆ state_info_ptr

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

Definition at line 115 of file liblts_bisim_gjkw.h.

◆ succ_const_iter_t

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

Definition at line 143 of file liblts_bisim_gjkw.h.

◆ succ_iter_t

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

Definition at line 139 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 2190 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.