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

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

Public attributes

bisim_gjkw::fixed_vector<action_block_entry> action_block

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.

action_block_iter_t action_block_inert_begin

pointer to the first inert transition in action_block

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_iter_t 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.

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.

std::list<block_bunch_slice_t> unstable_block_bunch

list of unstable block_bunch-slices

block_bunch_slice_iter_t unstable_block_bunch_postprocess_end

pointer to first unstable block_bunch-slice that is not currently postprocessed

During postprocessing, only the unstable block_bunch-slices that contain transitions from the block withe new non-inert transitions need to be handled. This pointer points to the first unstable block_bunch-slice that does not need to be postprocessed. It cannot be a block_bunch_slice_const_iter_t because we sometimes splice to that point.At other times, this pointer points to the end of the unstable block_bunch-slices.

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(const action_block_iter_t &action_block_iter, 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
  • first_transition_of_state This is the first transition of the state, so a new bunch_slice has to be allocated.
part_trans_t(trans_type num_transitions, trans_type num_actions, state_info_iter_t illegal_state)

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
  • illegal_state an iterator to a dummy state (which can be dereferenced, see the implementation of surely_has_no_transition_in()). This parameter is used to initialize dummy transitions.
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(ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) const action_block_iter_t &action_block_iter, bunch_t *const new_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.

~part_trans_t()

destructor

The destructor also deallocates the bunches, as they are not directly referenced from anywhere.

Private member functions

void first_move_transition_to_new_action_block(const pred_iter_t &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.

bool make_noninert(pred_iter_t const old_pred_pos, iterator_or_null<block_bunch_slice_iter_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_iter_t move_out_slice_to_new_block(ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) succ_iter_t out_slice_end, block_t *const old_block, const block_bunch_slice_const_iter_t &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.

Private static member functions

static void second_move_transition_to_new_action_block(const pred_iter_t &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.