liblts_bisim_gj.h File Reference

O(m log n)-time branching bisimulation algorithm published at CONCUR 2025. More...

Go to the source code of this file.

Classes
struct	mcrl2::lts::detail::bisimulation_gj::outgoing_transition_type
	information about a transition stored in m_outgoing_transitions More...
union	mcrl2::lts::detail::bisimulation_gj::outgoing_transition_type::iterator_or_counter
	pointer to the corresponding entry in m_BLC_transitions More...
struct	mcrl2::lts::detail::bisimulation_gj::state_in_block_pointer
	a pointer to a state, i.e. a reference to a state More...
class	mcrl2::lts::detail::bisimulation_gj::todo_state_vector
struct	mcrl2::lts::detail::bisimulation_gj::state_type_gj
	information about a state More...
struct	mcrl2::lts::detail::bisimulation_gj::BLC_indicators
struct	mcrl2::lts::detail::bisimulation_gj::transition_type
struct	mcrl2::lts::detail::bisimulation_gj::block_type
union	mcrl2::lts::detail::bisimulation_gj::block_type::constellation_or_first_unmarked_bottom_state
union	mcrl2::lts::detail::bisimulation_gj::block_type::start_non_bottom_states_or_state_in_reduced_LTS
union	mcrl2::lts::detail::bisimulation_gj::block_type::btc_R
struct	mcrl2::lts::detail::bisimulation_gj::constellation_type
	information about a constellation More...
class	mcrl2::lts::detail::bisim_partitioner_gj< LTS_TYPE >
	implements the main algorithm for the branching bisimulation quotient More...

Namespaces
namespace	mcrl2
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::bisimulation_gj

Macros
#define	INIT_WITHOUT_BLC_SETS
#define	linked_list   simple_list
#define	non_bottom_states_NewBotSt   non_bottom_states[3]
#define	bottom_size(coroutine)
#define	bottom_and_non_bottom_size(coroutine)
#define	abort_if_bottom_size_too_large(coroutine)
#define	abort_if_non_bottom_size_too_large_NewBotSt(i)
#define	abort_if_size_too_large(coroutine, i)
#define	new_start_bottom_states(idx)
#define	new_end_bottom_states(idx)
#define	new_end_bottom_states_NewBotSt    (new_start_bottom_states_plus_one[2])
#define	max_below_pivot   min_block
#define	min_above_pivot   max_block
#define	PRINT_SG_PL(counter, sg_string, pl_string)    (counter) << (1 == (counter) ? (sg_string) : (pl_string))
#define	PRINT_INT_PERCENTAGE(num, denom)    (((num) * 200 + (denom)) / (denom) / 2)

Typedefs
using	mcrl2::lts::detail::bisimulation_gj::state_index = std::size_t
using	mcrl2::lts::detail::bisimulation_gj::transition_index = std::size_t
using	mcrl2::lts::detail::bisimulation_gj::label_index = std::size_t
using	mcrl2::lts::detail::bisimulation_gj::outgoing_transitions_it = fixed_vector< outgoing_transition_type >::iterator
using	mcrl2::lts::detail::bisimulation_gj::outgoing_transitions_const_it = fixed_vector< outgoing_transition_type >::const_iterator
using	mcrl2::lts::detail::bisimulation_gj::BLC_list_iterator = transition_index *
using	mcrl2::lts::detail::bisimulation_gj::BLC_list_iterator_or_null = transition_index *
using	mcrl2::lts::detail::bisimulation_gj::BLC_list_const_iterator = const transition_index *

Enumerations
enum	mcrl2::lts::detail::bisimulation_gj::subblocks { mcrl2::lts::detail::bisimulation_gj::ReachAlw =0 , mcrl2::lts::detail::bisimulation_gj::AvoidSml , mcrl2::lts::detail::bisimulation_gj::AvoidLrg , mcrl2::lts::detail::bisimulation_gj::NewBotSt }

Functions
static constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::marked (enum subblocks subblock)
	base marking value for a subblock
static constexpr bool	mcrl2::lts::detail::bisimulation_gj::is_in_marked_range_of (transition_index counter, enum subblocks subblock)
	checks whether a counter value is a marking for a given subblock
template<class CONTAINER >
static void	mcrl2::lts::detail::bisimulation_gj::clear (CONTAINER &c)
template<class LTS_TYPE >
void	mcrl2::lts::detail::bisimulation_reduce_gj (LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false)
	nonmember functions serving as interface with the rest of mCRL2
template<class LTS_TYPE >
bool	mcrl2::lts::detail::destructive_bisimulation_compare_gj (LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false, const bool 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_gj (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

Variables
constexpr constellation_type *	mcrl2::lts::detail::bisimulation_gj::null_constellation =nullptr
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::null_transition =-1
constexpr label_index	mcrl2::lts::detail::bisimulation_gj::null_action =-1
constexpr state_index	mcrl2::lts::detail::bisimulation_gj::null_state =-1
constexpr block_type *	mcrl2::lts::detail::bisimulation_gj::null_block =nullptr
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::undefined =0
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::marked_range
	the number of counter values that can be used for one subblock
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::marked_NewBotSt =marked(NewBotSt)
	counter value to indicate that a state is in the NewBotSt subset
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::marked_HitSmall =marked_NewBotSt+1

Detailed Description

O(m log n)-time branching bisimulation algorithm published at CONCUR 2025.

This algorithm is similar to liblts_bisim_dnj.h but it does not use bunches (i.e., partitions of transitions) to register which work has already been done. Instead, it uses a normal partition of states, similar to the first O(m log n) algorithm published in 2016/17. This algorithm should be slightly faster, but in particular use less memory than liblts_bisim_dnj.h. Otherwise the functionality is exactly the same.

Definition in file liblts_bisim_gj.h.

Macro Definition Documentation

abort_if_bottom_size_too_large

#define abort_if_bottom_size_too_large

(

coroutine

)

Value:

          ((                                                                    assert(non_bottom_states[(coroutine)].empty()),                \
            bottom_size((coroutine))>no_of_unfinished_states_in_block/2) &&                                                                    \
           (                                                                    assert(std::numeric_limits<state_index>::max()!=               \
                                                                                                            no_of_unfinished_states_in_block), \
            no_of_unfinished_states_in_block=                                                                                                  \
                                       std::numeric_limits<state_index>::max(), assert(m_aut.num_states()<no_of_unfinished_states_in_block/2), \
            status[(coroutine)]=aborted,                                                                                                       \
            true))

abort_if_non_bottom_size_too_large_NewBotSt

#define abort_if_non_bottom_size_too_large_NewBotSt

(

i

)

Value:

          (non_bottom_states_NewBotSt.size()+(i)>                                                                                              \
                                          no_of_unfinished_states_in_block/2 &&                                                                \
           (/* Algorithm 2, Line 2.12                                        */ assert(std::numeric_limits<state_index>::max()!=               \
                                                                                                            no_of_unfinished_states_in_block), \
            no_of_unfinished_states_in_block=                                                                                                  \
                                       std::numeric_limits<state_index>::max(), assert(m_aut.num_states()<no_of_unfinished_states_in_block/2), \
            status_NewBotSt=aborted,                                                                                                           \
            true))

abort_if_size_too_large

#define abort_if_size_too_large	(		coroutine,
			i
	)

Value:

          (bottom_and_non_bottom_size((coroutine))+(i)>                                                                                        \
                                          no_of_unfinished_states_in_block/2 &&                                                                \
           (/* Algorithm 2, Line 2.12                                        */ assert(std::numeric_limits<state_index>::max()!=               \
                                                                                                            no_of_unfinished_states_in_block), \
            no_of_unfinished_states_in_block=                                                                                                  \
                                       std::numeric_limits<state_index>::max(), assert(m_aut.num_states()<no_of_unfinished_states_in_block/2), \
            status[(coroutine)]=aborted,                                                                                                       \
            non_bottom_states[(coroutine)].clear(),                                                                                            \
            true))

bottom_and_non_bottom_size

#define bottom_and_non_bottom_size

(

coroutine

)

Value:

              (                           assert(aborted!=status[(coroutine)]), \
              bottom_size((coroutine))+non_bottom_states[(coroutine)].size())

bottom_size

#define bottom_size

(

coroutine

)

Value:

                                                                                (                                          assert(ReachAlw==(coroutine)||AvoidSml==(coroutine)||AvoidLrg==(coroutine)),  \
                                                                                assert(start_bottom_states[(coroutine)]<=start_bottom_states[(coroutine)+1]), \
              static_cast<state_type>                                         \
                         (std::distance(start_bottom_states[(coroutine)],     \
                                        start_bottom_states[(coroutine)+1])))

INIT_WITHOUT_BLC_SETS

#define INIT_WITHOUT_BLC_SETS

Definition at line 28 of file liblts_bisim_gj.h.

linked_list

#define linked_list   simple_list

Definition at line 38 of file liblts_bisim_gj.h.

max_below_pivot

#define max_below_pivot   min_block

min_above_pivot

#define min_above_pivot   max_block

new_end_bottom_states

#define new_end_bottom_states

(

idx

)

Value:

                                       (                                    assert(1<=(idx)), assert((idx)<=2), \
                                       new_end_bottom_states_plus_one[(idx)-1])

new_end_bottom_states_NewBotSt

#define new_end_bottom_states_NewBotSt    (new_start_bottom_states_plus_one[2])

new_start_bottom_states

#define new_start_bottom_states

(

idx

)

Value:

                                     (                                  assert(1<=(idx)), assert((idx)<=3), \
                                     new_start_bottom_states_plus_one[(idx)-1])

non_bottom_states_NewBotSt

#define non_bottom_states_NewBotSt   non_bottom_states[3]

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
	)		(counter) << (1 == (counter) ? (sg_string) : (pl_string))