mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t Class Reference

Information about a set of transitions with the same source block, in the same bunch. More...

#include <liblts_bisim_dnj.h>

Public Member Functions

bool is_stable () const
 returns true iff the block_bunch-slice is registered as stable
 
void make_stable ()
 register that the block_bunch-slice is stable
 
void make_unstable ()
 register that the block_bunch-slice is not stable
 
 block_bunch_slice_t (block_bunch_entry *const new_end, bunch_t *const new_bunch, bool const new_is_stable)
 constructor
 
bool empty () const
 returns true iff the block_bunch-slice is empty
 
block_tsource_block () const
 compute the source block of the transitions in this slice
 
template<class LTS_TYPE >
std::string debug_id (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a block_bunch-slice identification for debugging
 
template<class LTS_TYPE >
bool add_work_to_bottom_transns (enum bisim_gjkw::check_complexity::counter_type const ctr, unsigned const max_value, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 add work to transitions starting in bottom states
 

Public Attributes

block_bunch_entryend
 pointer past the end of the transitions in the block_bunch array
 
bunch_tbunch
 bunch to which this slice belongs
 
block_bunch_entrymarked_begin
 pointer to the first marked transition in the block_bunch array
 
bisim_gjkw::check_complexity::block_bunch_dnj_counter_t work_counter
 

Detailed Description

Information about a set of transitions with the same source block, in the same bunch.

A block_bunch-slices contains the transitions in a single bunch that start in the same block. In the end, we want each block to be stable under its block_bunch-slices, i.e. every bottom state has a transition in every block_bunch-slice of the block. Then, there will be one slice for each transition in the minimised LTS, so we should try to minimize this data structure as much as possible.

Also note that these slices are part of a doubly-linked list. We cannot change this to a singly-linked list because we occasionally delete an element from this list. This would be possible with a single-linked list if we could infer the order of the list somehow, e.g. from the transitions in a bottom state – however, this does not work when a block loses all its bottom states, i.e. when a block splits into a small U and large R but R does not contain any bottom states.

Definition at line 1798 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

◆ block_bunch_slice_t()

mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::block_bunch_slice_t ( block_bunch_entry *const  new_end,
bunch_t *const  new_bunch,
bool const  new_is_stable 
)
inline

constructor

Definition at line 1834 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ add_work_to_bottom_transns()

template<class LTS_TYPE >
bool mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::add_work_to_bottom_transns ( enum bisim_gjkw::check_complexity::counter_type const  ctr,
unsigned const  max_value,
const bisim_partitioner_dnj< LTS_TYPE > &  partitioner 
) const
inline

add work to transitions starting in bottom states

Sometimes an action is done whose time could be accounted for by any transition starting in a bottom state of the block.

Parameters
ctrcounter type to which work is assigned
max_valuenew value of the counter
partitionerLTS partitioner (to print error messages if necessary)

Definition at line 1911 of file liblts_bisim_dnj.h.

◆ debug_id()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::debug_id ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print a block_bunch-slice identification for debugging

Definition at line 1863 of file liblts_bisim_dnj.h.

◆ empty()

bool mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::empty ( ) const
inline

returns true iff the block_bunch-slice is empty

A block_bunch-slice should only become empty if it is unstable.

Definition at line 1847 of file liblts_bisim_dnj.h.

◆ is_stable()

bool mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::is_stable ( ) const
inline

returns true iff the block_bunch-slice is registered as stable

Definition at line 1816 of file liblts_bisim_dnj.h.

◆ make_stable()

void mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::make_stable ( )
inline

register that the block_bunch-slice is stable

Definition at line 1820 of file liblts_bisim_dnj.h.

◆ make_unstable()

void mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::make_unstable ( )
inline

register that the block_bunch-slice is not stable

Definition at line 1827 of file liblts_bisim_dnj.h.

◆ source_block()

block_t * mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::source_block ( ) const
inline

compute the source block of the transitions in this slice

Definition at line 1856 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ bunch

bunch_t* mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::bunch

bunch to which this slice belongs

Definition at line 1807 of file liblts_bisim_dnj.h.

◆ end

block_bunch_entry* mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::end

pointer past the end of the transitions in the block_bunch array

We do not need a begin pointer because we can always walk through the transitions in the slice from end to beginning.

Definition at line 1804 of file liblts_bisim_dnj.h.

◆ marked_begin

block_bunch_entry* mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::marked_begin

pointer to the first marked transition in the block_bunch array

If this pointer is nullptr, then the block_bunch_slice is stable.

Definition at line 1812 of file liblts_bisim_dnj.h.

◆ work_counter

bisim_gjkw::check_complexity::block_bunch_dnj_counter_t mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::work_counter
mutable

Definition at line 1941 of file liblts_bisim_dnj.h.


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