stores information about a block More...

#include <liblts_bisim_dnj.h>

Public Member Functions
	block_t (permutation_entry const new_begin, permutation_entry const new_end, state_type const new_seqnr)
	constructor

state_type	size () const
	provides the number of states in the block

state_type	bottom_size () const
	provides the number of bottom states in the block

state_type	marked_bottom_size () const
	provides the number of marked bottom states in the block

state_type	marked_size () const
	provides the number of marked states in the block

state_type	unmarked_bottom_size () const
	provides the number of unmarked bottom states in the block

state_type	unmarked_nonbottom_size () const
	provides the number of unmarked nonbottom states in the block

bool	mark_nonbottom (permutation_entry *const s)
	mark a non-bottom state

bool	mark (permutation_entry *const s)
	mark a state

block_t *	split_off_block (enum new_block_mode_t new_block_mode, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) ONLY_IF_POOL_ALLOCATOR(my_pool< simple_list< block_bunch_slice_t >::entry > &storage,) state_type new_seqnr)
	refine a block

template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	print a block identification for debugging

Public Attributes
permutation_entry *	begin
	iterator to the first state of the block

permutation_entry *	marked_bottom_begin
	iterator to the first marked bottom state of the block

permutation_entry *	nonbottom_begin
	iterator to the first non-bottom state of the block

permutation_entry *	marked_nonbottom_begin
	iterator to the first marked non-bottom state of the block

permutation_entry *	end
	iterator past the last state of the block

simple_list< block_bunch_slice_t >	stable_block_bunch
	list of stable block_bunch-slices with transitions from this block

const state_type	seqnr
	unique sequence number of this block

check_complexity::block_dnj_counter_t	work_counter

Detailed Description

stores information about a block

A block corresponds to a slice of the permutation array. As the number of blocks is initially unknown, we will allocate instances of this class dynamically.

The slice in the permutation array containing the states of the block is subdivided into the following subslices (in this order):

unmarked bottom states
marked bottom states (initially empty)
unmarked non-bottom states
marked non-bottom states (initially empty)

A state should be marked iff it is a predecessor of the current splitter (through a strong transition). The marking is later extended to the R-states; that are the states with a weak transition to the splitter.

(During the execution of some functions, blocks are subdivided further; however, as these subdivisions are local to a single function, they are not stored here.)

Note that block_t uses the default destructor; therefore, if simple_list is trivially destructible, so is block_t.

Definition at line 344 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

◆ block_t()

mcrl2::lts::detail::bisim_dnj::block_t::block_t	(	permutation_entry *const	new_begin,
		permutation_entry *const	new_end,
		state_type const	new_seqnr
	)

inline

constructor

The constructor initialises the block to: all states are bottom states, no state is marked.

Parameters

new_begin	initial iterator to the first state of the block
new_end	initial iterator past the last state of the block
new_seqnr	is the sequence number of the new block

Definition at line 378 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ bottom_size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::bottom_size ( ) const

inline

provides the number of bottom states in the block

Definition at line 401 of file liblts_bisim_dnj.h.

◆ debug_id()

template<class LTS_TYPE >

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

inline

print a block identification for debugging

Definition at line 497 of file liblts_bisim_dnj.h.

◆ mark()

bool mcrl2::lts::detail::bisim_dnj::block_t::mark ( permutation_entry *const s )

inline

mark a state

Marking is done by moving the state to the slice of the marked bottom or non-bottom states of the block.

Parameters

s	the state that has to be marked

Returns: true iff the state was not marked before

Definition at line 465 of file liblts_bisim_dnj.h.

◆ mark_nonbottom()

bool mcrl2::lts::detail::bisim_dnj::block_t::mark_nonbottom ( permutation_entry *const s )

inline

mark a non-bottom state

Marking is done by moving the state to the slice of the marked non-bottom states of the block.

Parameters

s	the non-bottom state that has to be marked

Returns: true iff the state was not marked before

Definition at line 448 of file liblts_bisim_dnj.h.

◆ marked_bottom_size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::marked_bottom_size ( ) const

inline

provides the number of marked bottom states in the block

Definition at line 410 of file liblts_bisim_dnj.h.

◆ marked_size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::marked_size ( ) const

inline

provides the number of marked states in the block

Definition at line 419 of file liblts_bisim_dnj.h.

◆ size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::size ( ) const

inline

provides the number of states in the block

Definition at line 392 of file liblts_bisim_dnj.h.

◆ unmarked_bottom_size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::unmarked_bottom_size ( ) const

inline

provides the number of unmarked bottom states in the block

Definition at line 426 of file liblts_bisim_dnj.h.

◆ unmarked_nonbottom_size()

state_type mcrl2::lts::detail::bisim_dnj::block_t::unmarked_nonbottom_size ( ) const

inline

provides the number of unmarked nonbottom states in the block

Definition at line 435 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ begin

permutation_entry* mcrl2::lts::detail::bisim_dnj::block_t::begin

iterator to the first state of the block

Definition at line 348 of file liblts_bisim_dnj.h.

◆ end

permutation_entry* mcrl2::lts::detail::bisim_dnj::block_t::end

iterator past the last state of the block

Definition at line 360 of file liblts_bisim_dnj.h.

◆ marked_bottom_begin

permutation_entry* mcrl2::lts::detail::bisim_dnj::block_t::marked_bottom_begin

iterator to the first marked bottom state of the block

Definition at line 351 of file liblts_bisim_dnj.h.

◆ marked_nonbottom_begin

permutation_entry* mcrl2::lts::detail::bisim_dnj::block_t::marked_nonbottom_begin

iterator to the first marked non-bottom state of the block

Definition at line 357 of file liblts_bisim_dnj.h.

◆ nonbottom_begin

permutation_entry* mcrl2::lts::detail::bisim_dnj::block_t::nonbottom_begin

iterator to the first non-bottom state of the block

Definition at line 354 of file liblts_bisim_dnj.h.

◆ seqnr

const state_type mcrl2::lts::detail::bisim_dnj::block_t::seqnr

unique sequence number of this block

After the stuttering equivalence algorithm has terminated, this number is used as a state number in the quotient LTS.

Definition at line 369 of file liblts_bisim_dnj.h.

◆ stable_block_bunch

simple_list<block_bunch_slice_t> mcrl2::lts::detail::bisim_dnj::block_t::stable_block_bunch

list of stable block_bunch-slices with transitions from this block

Definition at line 364 of file liblts_bisim_dnj.h.

◆ work_counter

check_complexity::block_dnj_counter_t mcrl2::lts::detail::bisim_dnj::block_t::work_counter

mutable

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

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ block_t()

Member Function Documentation

◆ bottom_size()

◆ debug_id()

◆ mark()

◆ mark_nonbottom()

◆ marked_bottom_size()

◆ marked_size()

◆ size()

◆ unmarked_bottom_size()

◆ unmarked_nonbottom_size()

Member Data Documentation

◆ begin

◆ end

◆ marked_bottom_begin

◆ marked_nonbottom_begin

◆ nonbottom_begin

◆ seqnr

◆ stable_block_bunch

◆ work_counter