mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE > Class Template Reference

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_tsplit (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_thandle_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 3494 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 3498 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_autLTS that needs to be reduced
new_branchingIf true branching bisimulation is used, otherwise strong bisimulation is applied.
new_preserve_divergenceIf true and branching is true, preserve tau loops on states.

Definition at line 3549 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 4030 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 3699 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 3599 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
sstate whose equivalence class needs to be found
Returns
sequence number of the equivalence class of state s

Definition at line 3581 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_Rblock containing states with new non-inert transitions that need to be stabilised
bbslice_Tprime_Rsplitter 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 5085 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
sfirst state that needs to be compared.
tsecond state that needs to be compared.
Returns
true iff the two states are in the same equivalence class.

Definition at line 3669 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 3568 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 4325 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_Bblock that needs to be refined
splitter_Ttransition set that makes the block unstable
modeindicates 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 4708 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 3535 of file liblts_bisim_dnj.h.

◆ bisim_dnj::pred_entry

template<class LTS_TYPE >
friend class bisim_dnj::pred_entry
friend

Definition at line 3534 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ action_label

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 3522 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 3503 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 3525 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 3506 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 3510 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 3532 of file liblts_bisim_dnj.h.


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