implements the main algorithm for the branching bisimulation quotient More...

#include <liblts_bisim_dnj.h>

Public Member Functions
	bisim_partitioner_dnj (LTS_TYPE &new_aut, bool const new_branching=false, bool const new_preserve_divergence=false)
	constructor

state_type	num_eq_classes () const
	Calculate the number of equivalence classes.

state_type	get_eq_class (state_type const s) const
	Get the equivalence class of a state.

void	finalize_minimized_LTS ()
	Adapt the LTS after minimisation.

bool	in_same_class (state_type const s, state_type const t) const
	Check whether two states are in the same equivalence class.

Private Types
enum	refine_mode_t { extend_from_marked_states , extend_from_marked_states__add_new_noninert_to_splitter , extend_from_splitter }
	modes that determine details of how split() should work More...

Private Member Functions
void	create_initial_partition ()
	Create a partition satisfying the main invariant.

void	assert_stability () const
	assert that the data structure is consistent and stable

void	refine_partition_until_it_becomes_stable ()
	Run (branching) bisimulation minimisation in time O(m log n)

bisim_dnj::block_t *	split (bisim_dnj::block_t *const block_B, const bisim_dnj::block_bunch_slice_iter_t splitter_T, enum refine_mode_t mode)
	Split a block according to a splitter.

bisim_dnj::block_t *	handle_new_noninert_transns (bisim_dnj::block_t *const block_R, bisim_dnj::block_bunch_slice_const_iter_t bbslice_Tprime_R)
	Handle a block with new non-inert transitions.

Private Attributes
LTS_TYPE &	aut
	automaton that is being reduced

bisim_dnj::part_state_t	part_st
	partition of the state space into blocks

bisim_dnj::part_trans_t	part_tr
	partitions of the transitions (with bunches and action_block-slices)

bisim_gjkw::fixed_vector< bisim_dnj::iterator_or_counter< bisim_dnj::action_block_entry * > >	action_label
	action label slices

bool const	branching
	true iff branching (not strong) bisimulation has been requested

bool const	preserve_divergence
	true iff divergence-preserving branching bisimulation has been requested

Friends
class	bisim_dnj::pred_entry

class	bisim_dnj::bunch_t

Detailed Description

template<class LTS_TYPE>
class mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >

implements the main algorithm for the branching bisimulation quotient

Definition at line 3497 of file liblts_bisim_dnj.h.

Member Enumeration Documentation

◆ refine_mode_t

template<class LTS_TYPE >

enum mcrl2::lts::detail::bisim_partitioner_dnj::refine_mode_t

private

modes that determine details of how split() should work

Enumerator
extend_from_marked_states
extend_from_marked_states__add_new_noninert_to_splitter
extend_from_splitter

Definition at line 3501 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

◆ bisim_partitioner_dnj()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::bisim_partitioner_dnj	(	LTS_TYPE &	new_aut,
		bool const	new_branching = `false`,
		bool const	new_preserve_divergence = `false`
	)

inline

constructor

The constructor constructs the data structures and immediately calculates the partition corresponding with the bisimulation quotient. It destroys the transitions on the LTS (to save memory) but does not adapt the LTS to represent the quotient's transitions.

Parameters

new_aut	LTS that needs to be reduced
new_branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
new_preserve_divergence	If true and branching is true, preserve tau loops on states.

Definition at line 3552 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ assert_stability()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::assert_stability ( ) const

inlineprivate

assert that the data structure is consistent and stable

The data structure is tested against a large number of assertions to ensure that everything is consistent, e. g. pointers that should point to successors of state s actually point to a transition that starts in s.

Additionally, it is asserted that the partition is stable. i. e. every bottom state in every block can reach exactly every bunch in the list of bunches that should be reachable from it, and every nonbottom state can reach a subset of them.

Definition at line 4038 of file liblts_bisim_dnj.h.

◆ create_initial_partition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::create_initial_partition ( )

inlineprivate

Create a partition satisfying the main invariant.

Before the actual bisimulation minimisation can start, this function needs to be called to create a partition that satisfies the main invariant of the efficient O(m log n) branching bisimulation minimisation.

It puts all non-inert transitions into a single bunch, containing one action_block-slice for each action label. It creates a single block (or possibly two, if there are states that never will do any visible action). As a side effect, it deletes all transitions from the LTS that is stored with the partitioner; information about the transitions is kept in data structures that are suitable for the efficient algorithm.

For divergence-preserving branching bisimulation, we only need to treat tau-self-loops as non-inert transitions. In other texts, this is sometimes described as temporarily renaming the tau-self-loops to self-loops with a special label. However, as there are no other non-inert tau transitions, we can simply put them in their own action_block-slice, separate from the inert tau transitions. (It would be an error to mix the inert transitions with the self-loops in the same slice.)

Definition at line 3705 of file liblts_bisim_dnj.h.

◆ finalize_minimized_LTS()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::finalize_minimized_LTS ( )

inline

Adapt the LTS after minimisation.

After the efficient branching bisimulation minimisation, the information about the quotient LTS is only stored in the partition data structure of the partitioner object. This function exports the information back to the LTS by adapting its states and transitions: it updates the number of states and adds those transitions that are mandated by the partition data structure. If desired, it also creates a vector containing an arbritrary (example) original state per equivalence class.

The main parameter and return value are implicit with this function: a reference to the LTS was stored in the object by the constructor.

Definition at line 3605 of file liblts_bisim_dnj.h.

◆ get_eq_class()

template<class LTS_TYPE >

state_type mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::get_eq_class ( state_type const s ) const

inline

Get the equivalence class of a state.

After running the minimisation algorithm, this function produces the number of the equivalence class of a state. This number is the same as the number of the state in the minimised LTS to which the original state is mapped.

Parameters

s	state whose equivalence class needs to be found

Returns: sequence number of the equivalence class of state s

Definition at line 3587 of file liblts_bisim_dnj.h.

◆ handle_new_noninert_transns()

template<class LTS_TYPE >

bisim_dnj::block_t * mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::handle_new_noninert_transns	(	bisim_dnj::block_t *const	block_R,
		bisim_dnj::block_bunch_slice_const_iter_t	bbslice_Tprime_R
	)

inlineprivate

Handle a block with new non-inert transitions.

When this function starts, it assumes that the states with a new non-inert transition in block_R are marked. It is an error if it does not contain any marked states.

The function separates the states with new non-inert transitions from those without; as a result, the N-subblock (which contains states with new non-inert transitions) will contain at least one new bottom state (and no old bottom states). It then registers almost all block_bunch-slices of this N-subblock as unstable and marks one transition per block_bunch-slice and new bottom state. Only the block_bunch-slice containing the new non-inert transitions and, if possible, bbslice_Tprime_R are not registered as unstable.

Parameters

block_R	block containing states with new non-inert transitions that need to be stabilised
bbslice_Tprime_R	splitter of the last separation before, i.e. the splitter that made these transitions non-inert (`block_R` should already be stable w.r.t. `bbslice_Tprime_R`).

Returns: the block containing the old bottom states (and every state in block_R that cannot reach any new non-inert transition), i.e. the U-subblock of the separation

Definition at line 5092 of file liblts_bisim_dnj.h.

◆ in_same_class()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::in_same_class	(	state_type const	s,
		state_type const	t
	)		const

inline

Check whether two states are in the same equivalence class.

Parameters

s	first state that needs to be compared.
t	second state that needs to be compared.

Returns: true iff the two states are in the same equivalence class.

Definition at line 3675 of file liblts_bisim_dnj.h.

◆ num_eq_classes()

template<class LTS_TYPE >

state_type mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::num_eq_classes ( ) const

inline

Calculate the number of equivalence classes.

The number of equivalence classes (which is valid after the partition has been constructed) is equal to the number of states in the bisimulation quotient.

Definition at line 3574 of file liblts_bisim_dnj.h.

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::refine_partition_until_it_becomes_stable ( )

inlineprivate

Run (branching) bisimulation minimisation in time O(m log n)

This function assumes that the partitioner object stores a LTS with a partition satisfying the invariant:

‍If a state contains a transition in a bunch, then every bottom state in the same block contains a transition in that bunch.

The function runs the efficient O(m log n) algorithm for branching bisimulation minimisation on the LTS that has been stored in the partitioner: As long as there are nontrivial bunches, it selects one, subdivides it into two bunches and then stabilises the partition for these bunches. As a result, the partition stored in the partitioner will become stable.

Parameters and return value are implicit with this function: the LTS, the partition and the flags of the bisimulation algorithm are all stored in the partitioner object.

Definition at line 4332 of file liblts_bisim_dnj.h.

◆ split()

template<class LTS_TYPE >

bisim_dnj::block_t * mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::split	(	bisim_dnj::block_t *const	block_B,
		const bisim_dnj::block_bunch_slice_iter_t	splitter_T,
		enum refine_mode_t	mode
	)

inlineprivate

Split a block according to a splitter.

The function splits block_B into the R-subblock (states with a transition in splitter_T) and the U-subblock (states without a transition in splitter_T). Depending on mode, the states are primed as follows:

If mode == extend_from_marked_states, then all states with strong transition(s) must have been marked already.
If mode == extend_from_marked_states__add_new_noninert_to_splitter, states are marked as above. The only difference is the handling of new non-inert transitions.
If mode == extend_from_splitter, then no states must be marked; the initial states with a transition in splitter_T are searched by split() itself. Every bottom state with strong transition(s) needs to have at least one marked strong transition.

The function will also adapt all data structures and determine which transitions have changed from inert to non-inert. States with a new non-inert transition will be marked upon returning. Normally, the new non-inert transitions are moved to a new bunch, which will be specially created. However, if mode == extend_from_marked_states__add_new_noninert_to_splitter, then the new non-inert transitions will be added to splitter_T (which must hold transitions that have just become non-inert before this call to split()). If the resulting block contains marked states, the caller has to call handle_new_noninert_transns() to stabilise the block because the new bunch may make the block unstable.

Parameters

block_B	block that needs to be refined
splitter_T	transition set that makes the block unstable
mode	indicates how to find states with a transition in `splitter_T`, as described above

Returns: (a pointer to) the R-subblock. It is an error to call the function with settings that lead to an empty R-subblock. (An empty U-subblock is ok.)

Definition at line 4715 of file liblts_bisim_dnj.h.

Friends And Related Symbol Documentation

◆ bisim_dnj::bunch_t

template<class LTS_TYPE >

friend class bisim_dnj::bunch_t

friend

Definition at line 3538 of file liblts_bisim_dnj.h.

◆ bisim_dnj::pred_entry

template<class LTS_TYPE >

friend class bisim_dnj::pred_entry

friend

Definition at line 3537 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ action_label

template<class LTS_TYPE >

bisim_gjkw::fixed_vector<bisim_dnj::iterator_or_counter< bisim_dnj::action_block_entry*> > mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::action_label

private

action label slices

In part_tr.action_block, no information about the action label is actually stored with the transitions, to save memory. Entry l of this array contains a pointer to the first entry in part_tr.action_block with label l.

During initialisation, entry l of this array contains a counter to indicate how many non-inert transitions with action label l have been found.

Definition at line 3525 of file liblts_bisim_dnj.h.

◆ aut

template<class LTS_TYPE >

LTS_TYPE& mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::aut

private

automaton that is being reduced

Definition at line 3506 of file liblts_bisim_dnj.h.

◆ branching

template<class LTS_TYPE >

bool const mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::branching

private

true iff branching (not strong) bisimulation has been requested

Definition at line 3528 of file liblts_bisim_dnj.h.

◆ part_st

template<class LTS_TYPE >

bisim_dnj::part_state_t mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::part_st

private

partition of the state space into blocks

Definition at line 3509 of file liblts_bisim_dnj.h.

◆ part_tr

template<class LTS_TYPE >

bisim_dnj::part_trans_t mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::part_tr

private

partitions of the transitions (with bunches and action_block-slices)

Definition at line 3513 of file liblts_bisim_dnj.h.

◆ preserve_divergence

template<class LTS_TYPE >

bool const mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >::preserve_divergence

private

true iff divergence-preserving branching bisimulation has been requested

Note that this field must be false if strong bisimulation has been requested. There is no such thing as divergence-preserving strong bisimulation.

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

Private Types

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Enumeration Documentation

◆ refine_mode_t

Constructor & Destructor Documentation

◆ bisim_partitioner_dnj()

Member Function Documentation

◆ assert_stability()

◆ create_initial_partition()

◆ finalize_minimized_LTS()

◆ get_eq_class()

◆ handle_new_noninert_transns()

◆ in_same_class()

◆ num_eq_classes()

◆ refine_partition_until_it_becomes_stable()

◆ split()

Friends And Related Symbol Documentation

◆ bisim_dnj::bunch_t

◆ bisim_dnj::pred_entry

Member Data Documentation

◆ action_label

◆ aut

◆ branching

◆ part_st

◆ part_tr

◆ preserve_divergence