mCRL2
Loading...
Searching...
No Matches
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_tsplit_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_entrybegin
 first transition in the bunch
 
action_block_entryend
 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
 
bisim_gjkw::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 1640 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 1675 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 1715 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 1703 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 1687 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 1755 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 1644 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 1647 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

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

Definition at line 1777 of file liblts_bisim_dnj.h.


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