mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw Namespace Reference

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  check_complexity
 class for time complexity checks 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_entrystate_info_ptr
 
typedef const state_info_entrystate_info_const_ptr
 
typedef fixed_vector< state_info_ptrpermutation_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_descriptorB_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

◆ 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

◆ B_to_C_iter_t

◆ 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

◆ pred_const_iter_t

◆ pred_iter_t

◆ state_info_const_ptr

◆ state_info_ptr

◆ succ_const_iter_t

◆ succ_iter_t

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
BlueBpointer to the blue block
RedBpointer 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 2136 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.

Parameters
BlueBpointer to the blue block
RedBpointer to the red block

Definition at line 2230 of file liblts_bisim_gjkw.cpp.

◆ swap_permutation()

static void mcrl2::lts::detail::bisim_gjkw::swap_permutation ( permutation_iter_t  s1,
permutation_iter_t  s2 
)
inlinestatic

swap two permutations

Definition at line 369 of file liblts_bisim_gjkw.h.