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

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_tsplit_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_entrybegin
 iterator to the first state of the block
 
permutation_entrymarked_bottom_begin
 iterator to the first marked bottom state of the block
 
permutation_entrynonbottom_begin
 iterator to the first non-bottom state of the block
 
permutation_entrymarked_nonbottom_begin
 iterator to the first marked non-bottom state of the block
 
permutation_entryend
 iterator past the last state of the block
 
simple_list< block_bunch_slice_tstable_block_bunch
 list of stable block_bunch-slices with transitions from this block
 
const state_type seqnr
 unique sequence number of this block
 
bisim_gjkw::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):

  1. unmarked bottom states
  2. marked bottom states (initially empty)
  3. unmarked non-bottom states
  4. 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 1042 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_begininitial iterator to the first state of the block
new_endinitial iterator past the last state of the block
new_seqnris the sequence number of the new block

Definition at line 1076 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 1099 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 1195 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
sthe state that has to be marked
Returns
true iff the state was not marked before

Definition at line 1163 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
sthe non-bottom state that has to be marked
Returns
true iff the state was not marked before

Definition at line 1146 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 1108 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 1117 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 1090 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 1124 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 1133 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 1046 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 1058 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 1049 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 1055 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 1052 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 1067 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 1062 of file liblts_bisim_dnj.h.

◆ work_counter

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

Definition at line 1209 of file liblts_bisim_dnj.h.


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