liblts_bisim_gj.h File Reference

O(m log n)-time branching bisimulation algorithm similar to liblts_bisim_dnj.h which does not use bunches, i.e., partitions of transitions. This algorithm should be slightly faster, but in particular use less memory than liblts_bisim_dnj.h. Otherwise the functionality is exactly the same. More...

Go to the source code of this file.

Classes
struct	mcrl2::lts::detail::bisimulation_gj::linked_list_const_iterator< T >
struct	mcrl2::lts::detail::bisimulation_gj::linked_list_iterator< T >
struct	mcrl2::lts::detail::bisimulation_gj::linked_list_node< T >
	Private linked list that uses less memory. More...
struct	mcrl2::lts::detail::bisimulation_gj::global_linked_list_administration< T >
struct	mcrl2::lts::detail::bisimulation_gj::linked_list< T >
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
	information about a block More...
union	mcrl2::lts::detail::bisimulation_gj::block_type::constellation_or_first_unmarked_bottom_state
struct	mcrl2::lts::detail::bisimulation_gj::block_type::constellation_or_first_unmarked_bottom_state::constellation_and_new_bottom_states
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
	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::bisimulation_gj

Macros
#define	INITIAL_PARTITION_WITHOUT_BLC_SETS
#define	use_BLC_transitions   (!initialisation)
#define	use_BLC_transitions   (!initialisation)
#define	use_BLC_transitions   (!initialisation)
#define	use_BLC_transitions   (!initialisation)
#define	max_below_pivot   min_block
#define	min_above_pivot   max_block

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

Functions
template<class CONTAINER >
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_index	mcrl2::lts::detail::bisimulation_gj::null_constellation =-1
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_index	mcrl2::lts::detail::bisimulation_gj::null_block =-1
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::undefined =-1
constexpr transition_index	mcrl2::lts::detail::bisimulation_gj::Rmarked =-2

Detailed Description

O(m log n)-time branching bisimulation algorithm similar to liblts_bisim_dnj.h which does not use bunches, i.e., partitions of transitions. 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

INITIAL_PARTITION_WITHOUT_BLC_SETS

#define INITIAL_PARTITION_WITHOUT_BLC_SETS

Definition at line 40 of file liblts_bisim_gj.h.

max_below_pivot

#define max_below_pivot   min_block

min_above_pivot

#define min_above_pivot   max_block

use_BLC_transitions [1/4]

#define use_BLC_transitions   (!initialisation)

use_BLC_transitions [2/4]

#define use_BLC_transitions   (!initialisation)

use_BLC_transitions [3/4]

#define use_BLC_transitions   (!initialisation)

use_BLC_transitions [4/4]

#define use_BLC_transitions   (!initialisation)