mcrl2::lts::detail::bisim_dnj::bunch_t Class Reference

bunch of transitions More...

#include <liblts_bisim_dnj.h>

Classes
union	next_nontrivial_and_label_t
	pointer to next non-trivial bunch (in the single-linked list) or label More...

Public Member Functions
	bunch_t (action_block_entry *const new_begin, action_block_entry *const new_end)
	constructor
bool	is_trivial () const
	returns true iff the bunch is trivial
bunch_t *	split_off_small_action_block_slice (part_trans_t &part_tr)
	split off a single action_block-slice from the bunch
template<class LTS_TYPE >
std::string	debug_id_short (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	print a short bunch identification for debugging
template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	print a long bunch identification for debugging
template<class LTS_TYPE >
int	max_work_counter (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	calculates the maximal allowed value for work counters associated with this bunch

Public Attributes
action_block_entry *	begin
	first transition in the bunch
action_block_entry *	end
	pointer past the last transition in the bunch
union mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t	next_nontrivial_and_label
check_complexity::bunch_dnj_counter_t	work_counter

Detailed Description

bunch of transitions

Like a slice, at the end of the algorithm there will be a bunch for every transition in the bisimulation quotient. Therefore, we should try to minimize the size of a bunch as much as possible.

Definition at line 942 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

bunch_t()

mcrl2::lts::detail::bisim_dnj::bunch_t::bunch_t ( action_block_entry *const  new_begin, action_block_entry *const  new_end  )

inline

constructor

Definition at line 977 of file liblts_bisim_dnj.h.

Member Function Documentation

debug_id()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisim_dnj::bunch_t::debug_id ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner ) const

inline

print a long bunch identification for debugging

Definition at line 1017 of file liblts_bisim_dnj.h.

debug_id_short()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisim_dnj::bunch_t::debug_id_short ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner ) const

inline

print a short bunch identification for debugging

Definition at line 1005 of file liblts_bisim_dnj.h.

is_trivial()

bool mcrl2::lts::detail::bisim_dnj::bunch_t::is_trivial ( ) const

inline

returns true iff the bunch is trivial

If this bunch is the last in the list of non-trivial bunches, the convention is that the next pointer points to this bunch itself (to distinguish it from nullptr).

Definition at line 989 of file liblts_bisim_dnj.h.

max_work_counter()

template<class LTS_TYPE >

int mcrl2::lts::detail::bisim_dnj::bunch_t::max_work_counter ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner ) const

inline

calculates the maximal allowed value for work counters associated with this bunch

Work counters may only be nonzero if this bunch is a single-action bunch, i. e. all its transitions have the same action label. Also, only then the size can be calculated as end - begin.

Definition at line 1057 of file liblts_bisim_dnj.h.

Member Data Documentation

begin

action_block_entry* mcrl2::lts::detail::bisim_dnj::bunch_t::begin

first transition in the bunch

Definition at line 946 of file liblts_bisim_dnj.h.

end

action_block_entry* mcrl2::lts::detail::bisim_dnj::bunch_t::end

pointer past the last transition in the bunch

Definition at line 949 of file liblts_bisim_dnj.h.

next_nontrivial_and_label

union mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label

work_counter

check_complexity::bunch_dnj_counter_t mcrl2::lts::detail::bisim_dnj::bunch_t::work_counter

mutable

Definition at line 1078 of file liblts_bisim_dnj.h.

---

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

• lts/include/mcrl2/lts/detail/liblts_bisim_dnj.h