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

#include <liblts_bisim_dnj.h>

Public Member Functions

 part_trans_t (trans_type num_transitions, trans_type num_actions)
 constructor
 
 ~part_trans_t ()
 destructor
 
bunch_tget_some_nontrivial ()
 provide some bunch from the list of non-trivial bunches
 
void make_nontrivial (bunch_t *const bunch)
 insert a bunch into the list of nontrivial bunches
 
void make_trivial (bunch_t *const bunch)
 remove a bunch from the list of nontrivial bunches
 
void first_move_transition_to_new_bunch (action_block_entry *const action_block_iter, bunch_t *const bunch_T_a_Bprime, bool const first_transition_of_state)
 transition is moved to a new bunch
 
void second_move_transition_to_new_bunch (action_block_entry *const action_block_iter, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner, bunch_t *const bunch_T_a_Bprime,) bunch_t *const large_splitter_bunch)
 transition is moved to a new bunch, phase 2
 
void adapt_transitions_for_new_block (block_t *const new_block, block_t *const old_block, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) bool const add_new_noninert_to_splitter, const block_bunch_slice_iter_t splitter_T, enum new_block_mode_t const new_block_mode)
 Split all data structures after a new block has been created.
 
template<class LTS_TYPE >
void print_trans (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print all transitions
 

Public Attributes

bisim_gjkw::fixed_vector< succ_entrysucc
 array containing all successor entries
 
bisim_gjkw::fixed_vector< block_bunch_entryblock_bunch
 array containing all block_bunch entries
 
bisim_gjkw::fixed_vector< pred_entrypred
 array containing all predecessor entries
 
action_block_entry *const action_block_begin
 array containing all action_block entries
 
action_block_entry *const action_block_end
 
block_bunch_entryblock_bunch_inert_begin
 pointer to the first inert transition in block_bunch
 
action_block_entryaction_block_inert_begin
 pointer to the first inert transition in action_block
 
const action_block_entryaction_block_orig_inert_begin
 pointer to the first inert transition in the initial partition
 
simple_list< block_bunch_slice_tsplitter_list
 list of unstable block_bunch-slices
 
my_pool< simple_list< block_bunch_slice_t >::entry > storage
 pool for allocation of block_bunch-slices
 
state_type nr_of_new_bottom_states
 number of new bottom states found until now.
 
trans_type nr_of_bunches
 counters to measure progress
 
trans_type nr_of_nontrivial_bunches
 
trans_type nr_of_action_block_slices
 
trans_type nr_of_block_bunch_slices
 

Private Member Functions

succ_entrymove_out_slice_to_new_block (succ_entry *out_slice_end, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_bunch_slice_const_iter_t const splitter_T)
 Adapt the non-inert transitions in an out-slice to a new block.
 
void first_move_transition_to_new_action_block (pred_entry *const pred_iter)
 handle one transition after a block has been split
 
void second_move_transition_to_new_action_block (pred_entry *const pred_iter)
 handle one transition after a block has been split, phase 2
 
bool make_noninert (pred_entry *const old_pred_pos, block_bunch_slice_iter_or_null_t *const new_noninert_block_bunch_ptr)
 adapt data structures for a transition that has become non-inert
 

Private Attributes

bunch_tfirst_nontrivial
 pointer to first non-trivial bunch
 

Detailed Description

Definition at line 2001 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

◆ part_trans_t()

mcrl2::lts::detail::bisim_dnj::part_trans_t::part_trans_t ( trans_type  num_transitions,
trans_type  num_actions 
)
inline

constructor

The constructor sets up the dummy transitions at the beginning and end of the succ, block_bunch and pred arrays. (Dummy transitions in action_block depend on the number of transitions per action label, so they cannot be set up without knowing details about how many transitions have which label.)

Parameters
num_transitionsnumber of transitions of the LTS
num_actionsnumber of action labels of the LTS

Definition at line 2077 of file liblts_bisim_dnj.h.

◆ ~part_trans_t()

mcrl2::lts::detail::bisim_dnj::part_trans_t::~part_trans_t ( )
inline

destructor

Definition at line 2107 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ adapt_transitions_for_new_block()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::adapt_transitions_for_new_block ( block_t *const  new_block,
block_t *const  old_block,
ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) bool const  add_new_noninert_to_splitter,
const block_bunch_slice_iter_t  splitter_T,
enum new_block_mode_t const  new_block_mode 
)
inline

Split all data structures after a new block has been created.

This function splits the block_bunch- and action_block-slices to reflect that some transitions now start or end in the new block. They can no longer be in the same slice as the transitions that start or end in the old block, respectively. It also marks the transitions that have become non-inert as such and finds new bottom states.

Its time complexity is O(1 + |in(new_block)| + |out(new_block)|).

Parameters
new_blockthe new block
old_blockthe old block (from which new_block was split off)
add_new_noninert_to_splitterindicates to which block_bunch-slice new non-inert transitions should be added: if this parameter is false, a new slice is created; if it is true, new non-inert transitions are added to splitter_T. The latter can be done iff splitter_T is the last block_bunch-slice
splitter_Tthe splitter that caused new_block and old_block to separate from each other
new_block_modeindicates whether the new block is U or R

Definition at line 3022 of file liblts_bisim_dnj.h.

◆ first_move_transition_to_new_action_block()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::first_move_transition_to_new_action_block ( pred_entry *const  pred_iter)
inlineprivate

handle one transition after a block has been split

The main task of this method is to move the transition to the correct place in the action_block slice.

This function handles phase 1. Because the new action_block-slice cannot be adapted completely until all transitions into the new block have been handled through phase 1, the next function handles them again in phase 2.

Parameters
pred_itertransition that has to be moved

Definition at line 2654 of file liblts_bisim_dnj.h.

◆ first_move_transition_to_new_bunch()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::first_move_transition_to_new_bunch ( action_block_entry *const  action_block_iter,
bunch_t *const  bunch_T_a_Bprime,
bool const  first_transition_of_state 
)
inline

transition is moved to a new bunch

This (and the next function) have to be called after a transition has changed its bunch. The member function will adapt the transition data structure. It assumes that the transition is non-inert.

The work has to be done in two steps: We call the first step first_move_transition_to_new_bunch() for each transition in the new bunch, and then call second_move_transition_to_new_bunch() again for all these transitions. The reason is that some data structures need to be finalised in the second phase.

The first phase moves all transitions to their correct position in the out-slices and block_bunch-slices, but it doesn't yet create a fully correct new out-slice and block_bunch-slice. It adapts current_out_slice of all states with a transition in the new bunch.

Parameters
action_block_iter_itertransition that has to be changed
bunch_T_a_Bprimethe new bunch in which the transition lies
first_transition_of_statetrue iff this is the first transition of the state, so a new out-slice has to be allocated.

Definition at line 2197 of file liblts_bisim_dnj.h.

◆ get_some_nontrivial()

bunch_t * mcrl2::lts::detail::bisim_dnj::part_trans_t::get_some_nontrivial ( )
inline

provide some bunch from the list of non-trivial bunches

Returns
pointer to a bunch that is in the list of non-trivial bunches

Definition at line 2140 of file liblts_bisim_dnj.h.

◆ make_noninert()

bool mcrl2::lts::detail::bisim_dnj::part_trans_t::make_noninert ( pred_entry *const  old_pred_pos,
block_bunch_slice_iter_or_null_t *const  new_noninert_block_bunch_ptr 
)
inlineprivate

adapt data structures for a transition that has become non-inert

If the action_block-slice and the block_bunch-slice that precede the inert transitions in the respective arrays fit, the transition is added to these arrays instead of creating a new one. This only works if:

  • the action_block-slice has the same target block and the same action as old_pred_pos
  • the block_bunch-slice has the same source block as old_pred_pos
  • the bunch must contain the action_block-slice. If only the last two conditions are fulfilled, we can start a new action_block-slice in the same bunch. (It would be best for this if the R-subblock's block_bunch-slice would be the new one, because that would generally allow to add the new non-inert transitions to the last splitter.)

The state is only marked if is becomes a new bottom state. Otherwise, the marking/unmarking of the state is unchanged.

Parameters
old_pred_posthe transition that needs to be adapted.
[in,out]new_noninert_block_bunch_ptrthe bunch where new non-inert transitions have to be stored. If no such bunch has yet been created, it is nullptr; in that case, make_noninert() creates a new bunch.
Returns
true iff the state became a new bottom state

Definition at line 2796 of file liblts_bisim_dnj.h.

◆ make_nontrivial()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::make_nontrivial ( bunch_t *const  bunch)
inline

insert a bunch into the list of nontrivial bunches

Parameters
bunchthe bunch that has become non-trivial

Definition at line 2148 of file liblts_bisim_dnj.h.

◆ make_trivial()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::make_trivial ( bunch_t *const  bunch)
inline

remove a bunch from the list of nontrivial bunches

Parameters
bunchthe bunch that has become trivial

Definition at line 2165 of file liblts_bisim_dnj.h.

◆ move_out_slice_to_new_block()

succ_entry * mcrl2::lts::detail::bisim_dnj::part_trans_t::move_out_slice_to_new_block ( succ_entry out_slice_end,
ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_bunch_slice_const_iter_t const  splitter_T 
)
inlineprivate

Adapt the non-inert transitions in an out-slice to a new block.

After a block has been split, the outgoing transitions of the new block need to move to the respective block_bunch-slice of the new block.

This function handles all transitions in the out-slice just before out_slice_end, as they all belong to the same block_bunch-slice and can be moved together. However, transitions in splitter_T are excepted: all transitions in splitter_T from all states are transitions of the R-subblock, so if the latter is the new block, then splitter_T can be moved as a whole instead of per-state. In this case, the caller should move splitter_T to the list of stable block_bunch-slices of the R-subblock.

The function returns the beginning of this out-slice (which can become the next out_slice_end). It is meant to be called from the last out-slice back to the first because it inserts stable block_bunch-slices at the beginning of the list for the new block, so it would normally become ordered according to the bunch.

Parameters
out_slice_endThe transition just after the out-slice that is adapted
old_blockThe block in which the source state of the out-slice was before it was split (only needed if we do not use simple lists)
splitter_TThe splitter that made this block split
Returns
the beginning of this out-slice (which can become the next out_slice_end)

Definition at line 2469 of file liblts_bisim_dnj.h.

◆ print_trans()

template<class LTS_TYPE >
void mcrl2::lts::detail::bisim_dnj::part_trans_t::print_trans ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print all transitions

Transitions are printed organised into bunches.

Definition at line 3172 of file liblts_bisim_dnj.h.

◆ second_move_transition_to_new_action_block()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::second_move_transition_to_new_action_block ( pred_entry *const  pred_iter)
inlineprivate

handle one transition after a block has been split, phase 2

Because the new action_block-slice cannot be adapted completely until all transitions into the new block have been handled through phase 1 see the previous function), this function handles them again in phase 2.

Parameters
pred_itertransition that has to be moved

Definition at line 2737 of file liblts_bisim_dnj.h.

◆ second_move_transition_to_new_bunch()

void mcrl2::lts::detail::bisim_dnj::part_trans_t::second_move_transition_to_new_bunch ( action_block_entry *const  action_block_iter,
ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner, bunch_t *const bunch_T_a_Bprime,) bunch_t *const  large_splitter_bunch 
)
inline

transition is moved to a new bunch, phase 2

This (and the previous function) have to be called after a transition has changed its bunch. The member function will adapt the transition data structure. It assumes that the transition is non-inert.

The work has to be done in two steps: We call the first step first_move_transition_to_new_bunch() for each transition in the new bunch, and then call second_move_transition_to_new_bunch() again for all these transitions. The reason is that some data structures need to be finalised/ in the second phase.

The second phase finalizes the new out-slices and block_bunch-slices that were left half-finished by the first phase. It assumes that all block_bunch-slices are registered as stable.

Parameters
action_block_iter_itertransition that has to be changed
large_splitter_bunchthe large splitter_bunch that has been split; the transition has moved from large_splitter_bunch to a new, small bunch.

Definition at line 2350 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ action_block_begin

action_block_entry* const mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_begin

array containing all action_block entries

During initialisation, the transitions are sorted according to their label. Between transitions with different labels there is a dummy entry, to make it easier to check whether there is another transition in the current action_block slice.

The array may be empty, in particular if there are no transitions. In that case, the two pointers (and action_block_inert_begin below) should all be null pointers. Also, front() and back() are undefined; to avoid trouble with these methods, I decided to just store pointers to the beginning and the end of the array.

Definition at line 2033 of file liblts_bisim_dnj.h.

◆ action_block_end

action_block_entry* const mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_end

Definition at line 2034 of file liblts_bisim_dnj.h.

◆ action_block_inert_begin

action_block_entry* mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_inert_begin

pointer to the first inert transition in action_block

Definition at line 2040 of file liblts_bisim_dnj.h.

◆ action_block_orig_inert_begin

const action_block_entry* mcrl2::lts::detail::bisim_dnj::part_trans_t::action_block_orig_inert_begin

pointer to the first inert transition in the initial partition

Definition at line 2043 of file liblts_bisim_dnj.h.

◆ block_bunch

bisim_gjkw::fixed_vector<block_bunch_entry> mcrl2::lts::detail::bisim_dnj::part_trans_t::block_bunch

array containing all block_bunch entries

The first entry is a dummy entry, pointing to a transition not contained in any slice, to make it easier to check whether there is another transition in the current block_bunch.

Definition at line 2014 of file liblts_bisim_dnj.h.

◆ block_bunch_inert_begin

block_bunch_entry* mcrl2::lts::detail::bisim_dnj::part_trans_t::block_bunch_inert_begin

pointer to the first inert transition in block_bunch

Definition at line 2037 of file liblts_bisim_dnj.h.

◆ first_nontrivial

bunch_t* mcrl2::lts::detail::bisim_dnj::part_trans_t::first_nontrivial
private

pointer to first non-trivial bunch

Definition at line 2049 of file liblts_bisim_dnj.h.

◆ nr_of_action_block_slices

trans_type mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_action_block_slices

Definition at line 2066 of file liblts_bisim_dnj.h.

◆ nr_of_block_bunch_slices

trans_type mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_block_bunch_slices

Definition at line 2067 of file liblts_bisim_dnj.h.

◆ nr_of_bunches

trans_type mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_bunches

counters to measure progress

Definition at line 2064 of file liblts_bisim_dnj.h.

◆ nr_of_new_bottom_states

state_type mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_new_bottom_states

number of new bottom states found until now.

Definition at line 2061 of file liblts_bisim_dnj.h.

◆ nr_of_nontrivial_bunches

trans_type mcrl2::lts::detail::bisim_dnj::part_trans_t::nr_of_nontrivial_bunches

Definition at line 2065 of file liblts_bisim_dnj.h.

◆ pred

bisim_gjkw::fixed_vector<pred_entry> mcrl2::lts::detail::bisim_dnj::part_trans_t::pred

array containing all predecessor entries

The first and last entry are dummy entries, pointing to a transition to nullptr, to make it easier to check whether there is another transition to the current state.

Definition at line 2020 of file liblts_bisim_dnj.h.

◆ splitter_list

simple_list<block_bunch_slice_t> mcrl2::lts::detail::bisim_dnj::part_trans_t::splitter_list

list of unstable block_bunch-slices

Definition at line 2046 of file liblts_bisim_dnj.h.

◆ storage

my_pool<simple_list<block_bunch_slice_t>::entry> mcrl2::lts::detail::bisim_dnj::part_trans_t::storage

pool for allocation of block_bunch-slices

Definition at line 2057 of file liblts_bisim_dnj.h.

◆ succ

bisim_gjkw::fixed_vector<succ_entry> mcrl2::lts::detail::bisim_dnj::part_trans_t::succ

array containing all successor entries

The first and last entry are dummy entries, pointing to a transition from nullptr to nullptr, to make it easier to check whether there is another transition from the current state.

Definition at line 2008 of file liblts_bisim_dnj.h.


The documentation for this class was generated from the following file: