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_t *	source_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 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_entry *	end
	pointer past the end of the transitions in the block_bunch array
bunch_t *	bunch
	bunch to which this slice belongs
block_bunch_entry *	marked_begin
	pointer to the first marked transition in the block_bunch array
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 1099 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 1135 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 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

ctr	counter type to which work is assigned
max_value	new value of the counter
partitioner	LTS partitioner (to print error messages if necessary)

Definition at line 1212 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 1164 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 1148 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 1117 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 1121 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 1128 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 1157 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 1108 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 1105 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 1113 of file liblts_bisim_dnj.h.

work_counter

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

mutable

Definition at line 1241 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