mcrl2::lts::detail::bisim_dnj::bisim_partitioner_dnj

class mcrl2::lts::detail::bisim_dnj::bisim_partitioner_dnj

implements the main algorithm for the branching bisimulation quotient

Private attributes

bisim_gjkw::fixed_vector<iterator_or_counter<action_block_iter_t>> 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.

LTS_TYPE &aut

automaton that is being reduced

bool const branching

true iff branching (not strong) bisimulation has been requested

part_state_t part_st

partition of the state space into blocks

part_trans_t part_tr

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

bool const preserve_divergence

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.

Friends

friend class bunch_t

friend class pred_entry

Public member functions

bisim_partitioner_dnj(LTS_TYPE &new_aut, bool new_branching = false, bool new_preserve_divergence = false)

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.
void finalize_minimized_LTS(std::vector<std::size_t> *arbitrary_state_per_block)

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.

Parameters:

  • arbitrary_state_per_block If this pointer is != nullptr, the function fills the vector with, per equivalence class, the number of an arbitrary original state in the class.
state_type get_eq_class(state_type s) const

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

bool in_same_class(state_type s, state_type t) const

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.

~bisim_partitioner_dnj()

Public static member functions

static state_type num_eq_classes()

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.

Private member functions

void assert_stability() const

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.

void create_initial_partition()

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

block_t *postprocess_new_noninert(block_t *refine_block, const block_bunch_slice_const_iter_t &last_splitter)

Split a block with new non-inert transitions as needed.

The function splits refine_block by stabilising for all bunches in which it contains transitions.When this function starts, it assumes that the states with a new non-inert transition in refine_block are marked. It is an error if it does not contain any marked states.The function first separates the states with new non-inert transitions from those without; as a result, the red subblock (which contains states with new non-inert transitions) will contain at least one new bottom state. Then it walks through all the bunches that can be reached from this subblock to separate it into smaller, stable subblocks.

Parameters:

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

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

block_t *prepare_for_postprocessing(block_t *refine_block, block_bunch_slice_const_iter_t last_splitter, bool first_preparation)

Prepare a block for postprocesing.

When this function starts, it assumes that the states with a new non-inert transition in refine_block 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 red subblock (which contains states with new non-inert transitions) will contain at least one new bottom state (and no old bottom states). It then sorts the new bottom states according to the first bunch in which they have transitions and marks all block_bunch-slices of refine_block as unstable.

Parameters:

  • refine_block block containing states with new non-inert transitions that need to be stabilised
  • last_splitter splitter of the last separation before, i. e. the splitter that made these transitions non-inert (refine_block should already be stable w. r. t. last_splitter).
  • first_preparation If true, then the function also makes sure that all unstable block_bunch-slice of refine_block are before unstable_block_bunch_postprocess_end.

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

block_t* refine(block_t *const refine_block, const block_bunch_slice_iter_t &splitter, enum refine_mode_t const mode ONLY_IF_DEBUG(, const bunch_t *const new_bunch=nullptr))

Split a block according to a splitter.

The function splits refine_block into the red part (states with a transition in splitter) and the blue part (states without a transition in splitter). Depending on mode, the states are primed as follows:

  • If mode == extend_from_marked_states, then all states with a transition must have been marked already.
  • If mode == extend_from_marked_states_for_init_and_postprocess, 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 are searched by refine() itself.
  • If mode == extend_from_bottom_state_markings_and_splitter, then bottom states with a transition must have been marked already, but there may be non-bottom states that also have a transition, which are searched by refine().

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_for_init_and_postprocess, then the new non-inert transitions will be added to splitter (which must hold transitions that have just become non-inert before this call to refine()). If the resulting block contains marked states, the caller has to call postprocess_new_noninert() to stabilise the block because the new bunch may make the block unstable.

Parameters:

  • refine_block block that needs to be refined
  • splitter transition set that makes the block unstable
  • mode indicates how to find states with a transition in splitter, as described above

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

void refine_partition_until_it_becomes_stable()

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.