#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_t *	get_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
fixed_vector< succ_entry >	succ
	array containing all successor entries

fixed_vector< block_bunch_entry >	block_bunch
	array containing all block_bunch entries

fixed_vector< pred_entry >	pred
	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_entry *	block_bunch_inert_begin
	pointer to the first inert transition in block_bunch

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

simple_list< block_bunch_slice_t >	splitter_list
	list of unstable 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_entry *	move_out_slice_to_new_block (succ_entry out_slice_end, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_t const old_block, 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_t *	first_nontrivial
	pointer to first non-trivial bunch

Detailed Description

Definition at line 1301 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_transitions	number of transitions of the LTS
num_actions	number of action labels of the LTS

Definition at line 1377 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 1407 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_block	the new block
old_block	the old block (from which new_block was split off)
add_new_noninert_to_splitter	indicates 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_T	the splitter that caused new_block and old_block to separate from each other
new_block_mode	indicates whether the new block is U or R

Definition at line 2327 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_iter transition that has to be moved

Definition at line 1954 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_iter	transition that has to be changed
bunch_T_a_Bprime	the new bunch in which the transition lies
first_transition_of_state	true iff this is the first transition of the state, so a new out-slice has to be allocated.

Definition at line 1497 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 1440 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_pos	the transition that needs to be adapted.
[in,out]	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

Definition at line 2096 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

bunch the bunch that has become non-trivial

Definition at line 1448 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

bunch the bunch that has become trivial

Definition at line 1465 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_t *const	old_block,
		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_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 (only needed if we do not use simple lists)
splitter_T	The splitter that made this block split

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

Definition at line 1769 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 2477 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_iter transition that has to be moved

Definition at line 2037 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_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.

Definition at line 1650 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 1333 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 1334 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 1340 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 1343 of file liblts_bisim_dnj.h.

◆ block_bunch

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 1314 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 1337 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 1349 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 1366 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 1367 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 1364 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 1361 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 1365 of file liblts_bisim_dnj.h.

◆ pred

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 1320 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 1346 of file liblts_bisim_dnj.h.

◆ succ

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 1308 of file liblts_bisim_dnj.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_dnj.h

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ part_trans_t()

◆ ~part_trans_t()

Member Function Documentation

◆ adapt_transitions_for_new_block()

◆ first_move_transition_to_new_action_block()

◆ first_move_transition_to_new_bunch()

◆ get_some_nontrivial()

◆ make_noninert()

◆ make_nontrivial()

◆ make_trivial()

◆ move_out_slice_to_new_block()

◆ print_trans()

◆ second_move_transition_to_new_action_block()

◆ second_move_transition_to_new_bunch()

Member Data Documentation

◆ action_block_begin

◆ action_block_end

◆ action_block_inert_begin

◆ action_block_orig_inert_begin

◆ block_bunch

◆ block_bunch_inert_begin

◆ first_nontrivial

◆ nr_of_action_block_slices

◆ nr_of_block_bunch_slices

◆ nr_of_bunches

◆ nr_of_new_bottom_states

◆ nr_of_nontrivial_bunches

◆ pred

◆ splitter_list

◆ succ