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

Classes

class  action_block_entry
 information about a transition sorted per (action, target block) pair More...
 
class  block_bunch_entry
 information about a transition grouped per (source block, bunch) pair More...
 
class  block_bunch_slice_t
 Information about a set of transitions with the same source block, in the same bunch. More...
 
class  block_t
 stores information about a block More...
 
class  bunch_t
 bunch of transitions More...
 
class  iterator_or_counter
 union: either iterator or counter (for initialisation) More...
 
class  my_pool
 
class  part_state_t
 refinable partition data structure More...
 
class  part_trans_t
 
class  permutation_entry
 entry in the permutation array More...
 
class  pred_entry
 information about a transition sorted per target state More...
 
class  simple_list
 a simple implementation of lists More...
 
class  state_info_entry
 stores information about a single state More...
 
class  succ_entry
 information about a transition sorted per source state More...
 

Typedefs

typedef bisim_gjkw::fixed_vector< permutation_entrypermutation_t
 
typedef simple_list< block_bunch_slice_t >::iterator block_bunch_slice_iter_t
 
typedef simple_list< block_bunch_slice_t >::const_iterator block_bunch_slice_const_iter_t
 
typedef simple_list< block_bunch_slice_t >::iterator_or_null block_bunch_slice_iter_or_null_t
 

Enumerations

enum  new_block_mode_t { new_block_is_U , new_block_is_R }
 

Functions

template<class LTS_TYPE >
static void finalise_U_is_smaller (const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
 moves temporary work counters to normal ones if the U-block is smaller
 
template<class LTS_TYPE >
static void finalise_R_is_smaller (const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
 moves temporary work counters to normal ones if the R-block is smaller
 

Variables

struct { 
 
action_label_greater 
 

Function Documentation

◆ finalise_R_is_smaller()

template<class LTS_TYPE >
static void mcrl2::lts::detail::bisim_dnj::finalise_R_is_smaller ( const block_t *const  block_U,
const block_t *const  block_R,
const bisim_partitioner_dnj< LTS_TYPE > &  partitioner 
)
static

moves temporary work counters to normal ones if the R-block is smaller

Parameters
block_Uthe larger subblock containing the U-states
block_Rthe smaller but non-empty subblock containing the R-states
partitionerthe partitioner data structure, used to write diagnostic messages

Definition at line 5370 of file liblts_bisim_dnj.h.

◆ finalise_U_is_smaller()

template<class LTS_TYPE >
static void mcrl2::lts::detail::bisim_dnj::finalise_U_is_smaller ( const block_t *const  block_U,
const block_t *const  block_R,
const bisim_partitioner_dnj< LTS_TYPE > &  partitioner 
)
static

moves temporary work counters to normal ones if the U-block is smaller

Parameters
block_Uthe smaller subblock containing the U-states (can be nullptr)
block_Rthe larger subblock containing the R-states
partitionerthe partitioner data structure, used to write diagnostic messages

Definition at line 5263 of file liblts_bisim_dnj.h.

Variable Documentation

◆ [struct]

struct { ... } mcrl2::lts::detail::bisim_dnj::action_label_greater