mcrl2::lts::detail::bisim_dnj::part_trans_t

class mcrl2::lts::detail::bisim_dnj::part_trans_t

Public attributes

action_block_entry *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.

action_block_entry *action_block_end
action_block_entry *action_block_inert_begin

pointer to the first inert transition in action_block

const action_block_entry *action_block_orig_inert_begin

pointer to the first inert transition in the initial partition

bisim_gjkw::fixed_vector<block_bunch_entry> 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.

block_bunch_entry *block_bunch_inert_begin

pointer to the first inert transition in block_bunch

bisim_gjkw::fixed_vector<pred_entry> 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.

my_pool<simple_list<block_bunch_slice_t>::entry> storage

pool for allocation of block_bunch-slices

bisim_gjkw::fixed_vector<succ_entry> 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.

simple_list<block_bunch_slice_t> unstable_block_bunch

list of unstable block_bunch-slices

Private attributes

bunch_t *first_nontrivial

pointer to first non-trivial bunch

Public member functions

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 use_splitter_for_new_noninert_block_bunch, const block_bunch_slice_iter_t last_splitter, enum new_block_mode_t const new_block_mode)

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_block the new block
  • old_block the old block (from which new_block was split off)
  • use_splitter_for_new_noninert_block_bunch indicates to which block_bunch-slice new non-inert transitions should be added: if this parameter is null, a new slice is created; if it is not null, new non-inert transitions are added to this block_bunch-slice (which must be in the correct position to allow this).
  • last_splitter the splitter that caused new_block and old_block to separate from each other
  • new_block_mode indicates whether the new block is blue or red
void first_move_transition_to_new_bunch(action_block_entry *action_block_iter, bunch_t *bunch_T_a_B, bool const first_transition_of_state)

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_iter transition that has to be changed
  • bunch_T_a_B the new bunch in which the transition lies?
  • first_transition_of_state This is the first transition of the state, so a new out-slice has to be allocated.
bunch_t *get_some_nontrivial()

provide some bunch from the list of non-trivial bunches

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

void make_nontrivial(bunch_t *bunch)

insert a bunch into the list of nontrivial bunches

Parameters:

  • bunch the bunch that has become non-trivial
void make_trivial(bunch_t *bunch)

remove a bunch from the list of nontrivial bunches

Parameters:

  • bunch the bunch that has become trivial
part_trans_t(trans_type num_transitions, trans_type num_actions)

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_transitions number of transitions of the LTS
  • num_actions number of action labels of the LTS
void print_trans(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

print all transitions

Transitions are printed organised into bunches.

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_B,) bunch_t *const large_splitter_bunch)

correct transition data structure after splitting a bunch

transition is moved to a new bunch, phase 2This (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_iter transition that has to be changed
  • large_splitter_bunch the large splitter_bunch that has been split; the transition has moved from large_splitter_bunch to a new, small bunch.
~part_trans_t()

destructor

Private member functions

void first_move_transition_to_new_action_block(pred_entry *pred_iter)

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_iter transition that has to be moved
bool make_noninert(pred_entry *old_pred_pos, block_bunch_slice_iter_or_null_t *new_noninert_block_bunch_ptr)

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 red 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_pos the transition that needs to be adapted. Note that this parameter is passed by value otherwise, as this parameter is not only read at the beginning, it may happen that it is read after the transition has partly already been changed.
  • new_noninert_block_bunch_ptr the 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

succ_entry* 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 last_splitter)

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.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_end The transition just after the out-slice that is adapted
  • old_block The block in which the source state of the out-slice was before it was split
  • last_splitter The splitter that made this block split

Returns: the beginning of this out-slice (which can become the next out_slice_end)

void second_move_transition_to_new_action_block(pred_entry *pred_iter)

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_iter transition that has to be moved