Part_trans

data structures for transitions used during partition refinement More...

Classes
class	mcrl2::lts::detail::bisim_dnj::succ_entry
	information about a transition sorted per source state More...
class	mcrl2::lts::detail::bisim_dnj::block_bunch_entry
	information about a transition grouped per (source block, bunch) pair More...
class	mcrl2::lts::detail::bisim_dnj::pred_entry
	information about a transition sorted per target state More...
class	mcrl2::lts::detail::bisim_dnj::action_block_entry
	information about a transition sorted per (action, target block) pair More...
class	mcrl2::lts::detail::bisim_dnj::bunch_t
	bunch of transitions More...
class	mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t
	Information about a set of transitions with the same source block, in the same bunch. More...
class	mcrl2::lts::detail::bisim_dnj::part_trans_t
class	mcrl2::lts::detail::bisim_gjkw::succ_entry
class	mcrl2::lts::detail::bisim_gjkw::pred_entry
class	mcrl2::lts::detail::bisim_gjkw::B_to_C_entry
class	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor
class	mcrl2::lts::detail::bisim_gjkw::part_trans_t

Functions
succ_entry *	mcrl2::lts::detail::bisim_dnj::succ_entry::out_slice_begin (ONLY_IF_DEBUG(const fixed_vector< succ_entry > &succ))
	find the beginning of the out-slice
bunch_t *	mcrl2::lts::detail::bisim_dnj::succ_entry::bunch () const
	find the bunch of the transition
template<class LTS_TYPE >
static void	mcrl2::lts::detail::bisim_dnj::succ_entry::add_work_to_out_slice (const bisim_partitioner_dnj< LTS_TYPE > &partitioner, const succ_entry *out_slice_begin, enum check_complexity::counter_type ctr, unsigned max_value)
	assign work to the transitions in an out-slice (i.e. the transitions from one state in a specific bunch)
block_t *	mcrl2::lts::detail::bisim_dnj::block_t::split_off_block (enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) state_type new_seqnr)
	refine a block
bunch_t *	mcrl2::lts::detail::bisim_dnj::bunch_t::split_off_small_action_block_slice (part_trans_t &part_tr)
	split off a single action_block-slice from the bunch

Detailed Description

data structures for transitions used during partition refinement

These definitions provide a partition for transition data structure that can be used for the partition refinement algorithm.

Basically, transitions are stored in four arrays:

• pred: transitions grouped by goal state, to allow finding all predecessors of a goal state. (At the beginning and the end of the pred array, there are dummy entries.)
• succ: transitions grouped by source state and bunch, to allow finding all successors of a source state. Given a transition in this array, it is easy to find all transitions from the same source state in the same bunch. (At the beginning and the end of the succ array, there are dummy entries.)
• action_block: a permutation of the transitions such that transitions in the same bunch are adjacent, and within each bunch transitions with the same action label and target block. (Between two action_block-slices with different actions, there is a dummy entry.)
• block_bunch: a permutation of the transitions such that transitions from the same block in the same bunch are adjacent. (At the beginning of the block_bunch array, there is a dummy entry.) Entries in these four arrays are linked with each other with circular iterators, so that one can find the corresponding entry in another array.

Within this sort order, inert transitions are always placed after non-inert transitions.

state_info_entry and block_t (defined above) contain pointers to the slices of these arrays. For bunches and block_bunch-slices, we additionally create descriptors that hold some information about the slice.

These definitions provide a partition for transition data structure that can be used for the partition refinement algorithm.

Basically, transitions are stored in three arrays:

• pred: transitions ordered by goal state, to allow finding all predecessors of a goal state.
• succ: transitions ordered by source state and goal constellation, to allow finding all successors of a source state. Given a transition in this array, it is easy to find all transitions from the same source state to the same goal constellation. It is possible to find out, in time logarithmic in the out-degree, whether a state has a transition to a given constellation.
• B_to_C: a permutation of the transitions such that transitions from the same source block to the same goal constellation are adjacent. Further, this array does not need a specific sort order.

Within this sort order, inert transitions are always placed after non-inert transitions.

state_info_entry and block_t (defined above) contain pointers to the slices of these arrays. For the incoming transitions, they contain enough information; for the outgoing and the B_to_C-transitions, we additionally use so-called descriptors that show which slice belongs together. The above was the original design described in our publication [Groote/Jansen/Keiren/Wijs 2017]. This code reduces the descriptor for the outgoing transitions to a single pointer, which is stored in the succ array directly.

Function Documentation

add_work_to_out_slice()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_dnj::succ_entry::add_work_to_out_slice ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner, const succ_entry *  out_slice_begin, enum check_complexity::counter_type  ctr, unsigned  max_value  )

inlinestatic

assign work to the transitions in an out-slice (i.e. the transitions from one state in a specific bunch)

register that work has been done for the out-slice containing out_slice_begin

This debugging function is called to account for work that could be assigned to any transition in the out-slice. Just to make sure, we therefore set the corresponding counter ctr for every transition in the out-slice to max_value.

Parameters

partitioner	LTS partitioner
out_slice_begin	pointer to the first transition in the out-slice
ctr	type of the counter that work is assigned to
max_value	new value that the counter should get

This function should be used if work

Parameters

partitioner	the partitioner data structure, used to write diagnostic messages
out_slice_begin	the first transition in the out-slice
ctr	counter type to which work has to be assigned
max_value	new value of the counter

Definition at line 1290 of file liblts_bisim_dnj.h.

bunch()

bunch_t * mcrl2::lts::detail::bisim_dnj::succ_entry::bunch ( ) const

inline

find the bunch of the transition

find the bunch of a transition

Definition at line 1276 of file liblts_bisim_dnj.h.

out_slice_begin()

succ_entry * mcrl2::lts::detail::bisim_dnj::succ_entry::out_slice_begin ( ONLY_IF_DEBUG(const fixed_vector< succ_entry > &succ)  )

inline

find the beginning of the out-slice

Definition at line 1255 of file liblts_bisim_dnj.h.

split_off_block()

block_t * mcrl2::lts::detail::bisim_dnj::block_t::split_off_block ( enum new_block_mode_t  new_block_mode, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) state_type  new_seqnr  )

inline

refine a block

This function is called after a refinement function has found where to split the block into unmarked (U) and marked (R) states. It creates a new block for the smaller subblock.

Parameters

new_block_mode	indicates whether the U- or the R-block should be the new one. (This parameter is necessary in case the two halves have exactly the same size.)
new_seqnr	is the sequence number of the new block
new_block	(if the pool allocator is used) a pointer to an uninitialized block, where the new block will be stored.

Returns

pointer to the new block

This function is called after a refinement function has found where to split the block into unmarked (U) and marked (R) states. It creates a new block for the smaller subblock.

Parameters

new_block_mode	indicates whether the U- or the R-block should be the new one. (This parameter is necessary in case the two halves have exactly the same size.)
new_seqnr	is the sequence number of the new block

Returns

pointer to the new block

Definition at line 2603 of file liblts_bisim_dnj.h.

split_off_small_action_block_slice()

bunch_t * mcrl2::lts::detail::bisim_dnj::bunch_t::split_off_small_action_block_slice ( part_trans_t &  part_tr )

inline

split off a single action_block-slice from the bunch

The function splits the current bunch after its first action_block-slice or before its last action_block-slice, whichever is smaller. It creates a new bunch for the split-off slice and returns a pointer to the new bunch. The caller has to adapt the block_bunch-slices.

The function splits the current bunch after its first action_block-slice or before its last action_block-slice, whichever is smaller. It creates a new bunch for the split-off slice and returns a pointer to the new bunch. The caller has to adapt the block_bunch-slices.

Parameters

part_tr

the data structure containing information about the partition of transitions (needed to find the list of non-trivial bunches)

Returns

pointer to a new bunch containing one small action_block-slice that was originally in this bunch

Definition at line 2708 of file liblts_bisim_dnj.h.