mCRL2
Loading...
Searching...
No Matches
liblts_bisim_dnj.h File Reference

O(m log n)-time branching bisimulation algorithm. More...

Go to the source code of this file.

Classes

class  mcrl2::lts::detail::bisim_dnj::iterator_or_counter< Iterator >
 union: either iterator or counter (for initialisation) More...
 
class  mcrl2::lts::detail::bisim_dnj::my_pool< T, BLOCKSIZE >
 
class  mcrl2::lts::detail::bisim_dnj::my_pool< T, BLOCKSIZE >::pool_block_t
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >
 a simple implementation of lists More...
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >::empty_entry
 empty entry, used for the sentinel More...
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >::entry
 list entry More...
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >::const_iterator
 constant iterator class for simple_list More...
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >::iterator
 iterator class for simple_list More...
 
class  mcrl2::lts::detail::bisim_dnj::simple_list< T >::iterator_or_null
 class that stores either an iterator or a null value More...
 
class  mcrl2::lts::detail::bisim_dnj::state_info_entry
 stores information about a single state More...
 
union  mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t
 block where the state belongs More...
 
class  mcrl2::lts::detail::bisim_dnj::permutation_entry
 entry in the permutation array More...
 
class  mcrl2::lts::detail::bisim_dnj::block_t
 stores information about a block More...
 
class  mcrl2::lts::detail::bisim_dnj::part_state_t
 refinable partition data structure More...
 
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...
 
union  mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t
 pointer to next non-trivial bunch (in the single-linked list) or label 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_partitioner_dnj< LTS_TYPE >
 implements the main algorithm for the branching bisimulation quotient More...
 

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::lts
 The main LTS namespace.
 
namespace  mcrl2::lts::detail
 A base class for the lts_dot labelled transition system.
 
namespace  mcrl2::lts::detail::bisim_dnj
 

Macros

#define USE_SIMPLE_LIST
 
#define USE_POOL_ALLOCATOR
 
#define ONLY_IF_POOL_ALLOCATOR(...)   __VA_ARGS__
 
#define ONLY_IF_DEBUG(...)   __VA_ARGS__
 include something in Debug mode
 
#define PRINT_SG_PL(counter, sg_string, pl_string)
 
#define PRINT_INT_PERCENTAGE(num, denom)    (((num) * 200 + (denom)) / (denom) / 2)
 

Typedefs

typedef std::size_t mcrl2::lts::detail::label_type
 type used to store label numbers and counts
 
typedef bisim_gjkw::fixed_vector< permutation_entrymcrl2::lts::detail::bisim_dnj::permutation_t
 
typedef simple_list< block_bunch_slice_t >::iterator mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_t
 
typedef simple_list< block_bunch_slice_t >::const_iterator mcrl2::lts::detail::bisim_dnj::block_bunch_slice_const_iter_t
 
typedef simple_list< block_bunch_slice_t >::iterator_or_null mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_or_null_t
 

Enumerations

enum  mcrl2::lts::detail::bisim_dnj::new_block_mode_t { mcrl2::lts::detail::bisim_dnj::new_block_is_U , mcrl2::lts::detail::bisim_dnj::new_block_is_R }
 

Functions

template<class LTS_TYPE >
static void mcrl2::lts::detail::bisim_dnj::finalise_U_is_smaller (const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
 moves temporary work counters to normal ones if the U-block is smaller
 
template<class LTS_TYPE >
static void mcrl2::lts::detail::bisim_dnj::finalise_R_is_smaller (const block_t *const block_U, const block_t *const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
 moves temporary work counters to normal ones if the R-block is smaller
 
template<class LTS_TYPE >
void mcrl2::lts::detail::bisimulation_reduce_dnj (LTS_TYPE &l, bool const branching=false, bool const preserve_divergence=false)
 Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.
 
template<class LTS_TYPE >
bool mcrl2::lts::detail::destructive_bisimulation_compare_dnj (LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
 Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
 
template<class LTS_TYPE >
bool mcrl2::lts::detail::bisimulation_compare_dnj (const LTS_TYPE &l1, const LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false)
 Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
 

Variables

struct { 
 
mcrl2::lts::detail::bisim_dnj::action_label_greater 
 

Detailed Description

O(m log n)-time branching bisimulation algorithm.

This file implements an efficient partition refinement algorithm for labelled transition systems inspired by Groote / Jansen / Keiren / Wijs (2017) and Valmari (2009) to calculate the branching bisimulation classes of a labelled transition system. Different from the 2017 article, it does not translate the LTS to a Kripke structure, but works on the LTS directly. In this way the memory use can be reduced. The algorithm is described in the conference publication

David N. Jansen, Jan Friso Groote, Jeroen J.A. Keiren, Anton Wijs: An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In: Armin Biere, David Parker (Eds.): Tools and Algorithms for the Construction and Analysis of Systems: TACAS. (LNCS 12070). Springer: Cham,

  1. pp 3-20. https://doi.org/10.1007/978-3-030-45237-7_1

Partition refinement means that the algorithm maintains a partition of the state space of the LTS into `‘blocks’'. A block contains all states in one or several branching bisimulation equivalence classes. Blocks are being refined until every block contains exactly one branching bisimulation equivalence class.

The algorithm divides the non-inert transitions into action_block-slices. An action_block-slice contains all transitions with a given action label into one block. One or more action_block-slices are joined into a bunch. Bunches register which blocks have already been stabilised:

‍Invariant: The blocks are stable under the bunches, i. e. if a block has a transition in a bunch, then every bottom state in this block has a transition in this bunch.

However, if a bunch is non-trivial (i. e., it contains more than one action_block-slice), its slices may split some blocks into finer parts: not all states may have a transition in the same action_block-slice. So, a refinement step consists of moving one small action_block-slice from a non-trivial bunch to a new bunch and then splitting blocks to restore the Invariant. Splitting is always done by finding a small subblock and moving the states in that subblock to a new block. Note that we always handle a small part of some larger unit; that ensures that each state and transition is only touched O(log n) times.

After splitting blocks, some inert transitions may have become non-inert. These transitions mostly need to be inserted into their own bunch. Also, some states may have lost all their inert transitions and become new bottom states. These states need to be handled as well to re-establish the Invariant.

Overall, we spend time as follows:

  • Every transition is moved to a new bunch at most log2(2 * n2) = 2*log2(n) + 1 times. Every move leads to O(1) work.
  • Every state is moved to a new block at most log2(n) times. Every move leads to work proportional to the number of its incoming and outgoing transitions.
  • Every state becomes a new bottom state at most once. When this happens, this leads to work proportional to the number of its outgoing transitions. When summing this up over all states and transitions, we get that the algorithm spends time in O(m log n), where m is the number of transitions and n ist the number of states.
Author
David N. Jansen, Institute of Software, Chinese Academy of Sciences, Beijing, PR China

Definition in file liblts_bisim_dnj.h.

Macro Definition Documentation

◆ ONLY_IF_DEBUG

#define ONLY_IF_DEBUG (   ...)    __VA_ARGS__

include something in Debug mode

In a few places, we have to include an additional parameter to a function in Debug mode. While it is in principle possible to use #ifndef NDEBUG ... #endif, that would lead to distributing the code over many code lines. This macro expands to its arguments in Debug

Definition at line 134 of file liblts_bisim_dnj.h.

◆ ONLY_IF_POOL_ALLOCATOR

#define ONLY_IF_POOL_ALLOCATOR (   ...)    __VA_ARGS__

Definition at line 113 of file liblts_bisim_dnj.h.

◆ PRINT_INT_PERCENTAGE

#define PRINT_INT_PERCENTAGE (   num,
  denom 
)     (((num) * 200 + (denom)) / (denom) / 2)

◆ PRINT_SG_PL

#define PRINT_SG_PL (   counter,
  sg_string,
  pl_string 
)
Value:
(counter) \
<< (1 == (counter) ? (sg_string) : (pl_string))

◆ USE_POOL_ALLOCATOR

#define USE_POOL_ALLOCATOR

Definition at line 106 of file liblts_bisim_dnj.h.

◆ USE_SIMPLE_LIST

#define USE_SIMPLE_LIST

Definition at line 99 of file liblts_bisim_dnj.h.