classes to calculate the stutter equivalence quotient of a LTS More...

Classes
class	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >
	helps with initialising the refinable partition data structure More...

class	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key

class	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::KeyHasher

class	mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >
	implements the main algorithm for the branching bisimulation quotient More...

Macros
#define	BLOCK_NO_SEQNR ((state_type) -1)

Functions
const constln_t *	mcrl2::lts::detail::bisim_gjkw::state_info_entry::constln () const
	get constellation where the state belongs

constln_t *	mcrl2::lts::detail::bisim_gjkw::state_info_entry::constln ()

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::current_constln () const

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::current_constln ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_current_constln (succ_iter_t const new_current_constln)

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_begin () const
	iterator to first incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_begin ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_pred_begin (pred_iter_t new_in_begin)

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_end () const
	iterator past the last incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_end ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_pred_end (pred_iter_t new_in_end)

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_begin () const
	iterator to first non-inert incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_begin ()

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_end () const
	iterator past the last non-inert incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_end ()

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_begin () const
	iterator to first inert incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_begin ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_inert_pred_begin (pred_iter_t new_inert_in_begin)

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_end () const
	iterator one past the last inert incoming transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_end ()

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_begin () const
	iterator to first outgoing transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_begin ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_succ_begin (succ_iter_t new_out_begin)

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_end () const
	iterator past the last outgoing transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::succ_end ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_succ_end (succ_iter_t new_out_end)

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_begin () const
	iterator to first inert outgoing transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_begin ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_inert_succ_begin (succ_iter_t const new_inert_out_begin)

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_end () const
	iterator past the last inert outgoing transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_end ()

void	mcrl2::lts::detail::bisim_gjkw::state_info_entry::set_inert_succ_begin_and_end (succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)

bool	mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_transition_to (const constln_t *SpC) const

bool	mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_no_transition_to (const constln_t *SpC) const

std::string	mcrl2::lts::detail::bisim_gjkw::state_info_entry::debug_id_short () const
	print a short state identification for debugging

std::string	mcrl2::lts::detail::bisim_gjkw::state_info_entry::debug_id () const
	print a state identification for debugging

	mcrl2::lts::detail::bisim_gjkw::block_t::block_t (constln_t *const constln_, permutation_iter_t const begin_, permutation_iter_t const end_)
	constructor

	mcrl2::lts::detail::bisim_gjkw::block_t::~block_t ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::assign_seqnr ()
	assigns a unique sequence number

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::seqnr () const

static block_t *	mcrl2::lts::detail::bisim_gjkw::block_t::get_some_refinable ()
	provides an arbitrary refinable block

bool	mcrl2::lts::detail::bisim_gjkw::block_t::is_refinable () const
	checks whether the block is refinable

bool	mcrl2::lts::detail::bisim_gjkw::block_t::make_refinable ()
	makes a block refinable (i. e. inserts it into the respective list)

void	mcrl2::lts::detail::bisim_gjkw::block_t::make_nonrefinable ()
	makes a block non-refinable (i. e. removes it from the respective list)

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::size () const
	provides the number of states in the block

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_size () const
	provides the number of marked bottom states in the block

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::marked_size () const
	provides the number of marked states in the block

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_size () const
	provides the number of unmarked bottom states in the block

bool	mcrl2::lts::detail::bisim_gjkw::block_t::operator< (const block_t &other) const
	compares two blocks for ordering them

const constln_t *	mcrl2::lts::detail::bisim_gjkw::block_t::constln () const
	constellation where the block belongs to

constln_t *	mcrl2::lts::detail::bisim_gjkw::block_t::constln ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_constln (constln_t *new_constln)

B_to_C_descriptor *	mcrl2::lts::detail::bisim_gjkw::block_t::FromRed (const constln_t *SpC)
	read FromRed

void	mcrl2::lts::detail::bisim_gjkw::block_t::SetFromRed (B_to_C_desc_iter_t new_fromred)
	set FromRed to an existing element in to_constln

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::begin () const
	iterator to the first state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::begin ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_begin (permutation_iter_t new_begin)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::end () const
	iterator past the last state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::end ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_end (permutation_iter_t new_end)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_begin () const
	iterator to the first non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_begin ()

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_end () const
	iterator past the last non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_end ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_nonbottom_end (permutation_iter_t new_nonbottom_end)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::bottom_begin () const
	iterator to the first bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::bottom_begin ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_bottom_begin (permutation_iter_t new_bottom_begin)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::bottom_end () const
	iterator past the last bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::bottom_end ()

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_begin () const
	iterator to the first unmarked non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_begin ()

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_end () const
	iterator past the last unmarked non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_nonbottom_end ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_unmarked_nonbottom_end (permutation_iter_t new_unmarked_nonbottom_end)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_begin () const
	iterator to the first marked non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_begin ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_marked_nonbottom_begin (permutation_iter_t new_marked_nonbottom_begin)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_end () const
	iterator one past the last marked non-bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_end ()

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_begin () const
	iterator to the first unmarked bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_begin ()

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_end () const
	iterator past the last unmarked bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::unmarked_bottom_end ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_unmarked_bottom_end (permutation_iter_t new_unmarked_bottom_end)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_begin () const
	iterator to the first marked bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_begin ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_marked_bottom_begin (permutation_iter_t new_marked_bottom_begin)

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_end () const
	iterator past the last marked bottom state in the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_end ()

B_to_C_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::inert_begin () const
	iterator to the first inert transition of the block

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::inert_begin ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_begin (B_to_C_iter_t new_inert_begin)

B_to_C_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::inert_end () const
	iterator past the last inert transition of the block

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::inert_end ()

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_end (B_to_C_iter_t new_inert_end)

void	mcrl2::lts::detail::bisim_gjkw::block_t::set_inert_begin_and_end (B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)

bool	mcrl2::lts::detail::bisim_gjkw::block_t::mark_nonbottom (state_info_ptr s)
	mark a non-bottom state

bool	mcrl2::lts::detail::bisim_gjkw::block_t::mark (state_info_ptr s)
	mark a state

block_t *	mcrl2::lts::detail::bisim_gjkw::block_t::split_off_blue (permutation_iter_t blue_nonbottom_end)
	refine the block (the blue subblock is smaller)

block_t *	mcrl2::lts::detail::bisim_gjkw::block_t::split_off_red (permutation_iter_t red_nonbottom_begin)
	refine the block (the red subblock is smaller)

std::string	mcrl2::lts::detail::bisim_gjkw::block_t::debug_id () const
	print a block identification for debugging

static permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::permutation_begin ()
	provide an iterator to the beginning of the permutation array

	mcrl2::lts::detail::bisim_gjkw::constln_t::constln_t (state_type sort_key_, permutation_iter_t begin_, permutation_iter_t end_, B_to_C_iter_t postprocess_none)
	constructor

	mcrl2::lts::detail::bisim_gjkw::constln_t::~constln_t ()
	destructor

static constln_t *	mcrl2::lts::detail::bisim_gjkw::constln_t::get_some_nontrivial ()
	provides an arbitrary non-trivial constellation

const constln_t *	mcrl2::lts::detail::bisim_gjkw::constln_t::get_nontrivial_next () const
	provides the next non-trivial constellation

void	mcrl2::lts::detail::bisim_gjkw::constln_t::make_trivial ()
	makes a constellation trivial (i. e. removes it from the respective list)

void	mcrl2::lts::detail::bisim_gjkw::constln_t::make_nontrivial ()
	makes a constellation non-trivial (i. e. inserts it into the respective list)

bool	mcrl2::lts::detail::bisim_gjkw::constln_t::is_trivial () const
	returns true iff the constellation is trivial

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::begin () const
	constant iterator to the first state in the constellation

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::begin ()
	iterator to the first state in the constellation

void	mcrl2::lts::detail::bisim_gjkw::constln_t::set_begin (permutation_iter_t new_begin)
	set the iterator to the first state in the constellation

permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::end () const
	constant iterator past the last state in the constellation

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::end ()
	iterator past the last state in the constellation

void	mcrl2::lts::detail::bisim_gjkw::constln_t::set_end (permutation_iter_t new_end)
	set the iterator past the last state in the constellation

state_type	mcrl2::lts::detail::bisim_gjkw::constln_t::size () const
	returns number of states in the constellation

bool	mcrl2::lts::detail::bisim_gjkw::constln_t::operator< (const constln_t &other) const
	compares two constellations for ordering them

bool	mcrl2::lts::detail::bisim_gjkw::constln_t::operator> (const constln_t &other) const

bool	mcrl2::lts::detail::bisim_gjkw::constln_t::operator<= (const constln_t &other) const

bool	mcrl2::lts::detail::bisim_gjkw::constln_t::operator>= (const constln_t &other) const

block_t *	mcrl2::lts::detail::bisim_gjkw::constln_t::split_off_small_block ()
	split off a single block from the constellation

std::string	mcrl2::lts::detail::bisim_gjkw::constln_t::debug_id () const
	print a constellation identification for debugging

	mcrl2::lts::detail::bisim_gjkw::part_state_t::part_state_t (state_type n)
	constructor

	mcrl2::lts::detail::bisim_gjkw::part_state_t::~part_state_t ()
	destructor

void	mcrl2::lts::detail::bisim_gjkw::part_state_t::clear ()
	deallocates constellations and blocks

state_type	mcrl2::lts::detail::bisim_gjkw::part_state_t::state_size () const
	provide size of state space

const block_t *	mcrl2::lts::detail::bisim_gjkw::part_state_t::block (state_type s) const
	find block of a state

void	mcrl2::lts::detail::bisim_gjkw::part_state_t::print_block (const char message, const block_t B, permutation_const_iter_t begin, permutation_const_iter_t end) const
	print a slice of the partition (typically a block)

void	mcrl2::lts::detail::bisim_gjkw::part_state_t::print_part (const part_trans_t &part_tr) const
	print the partition as a tree (per constellation and block)

void	mcrl2::lts::detail::bisim_gjkw::part_state_t::print_trans () const
	print all transitions

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_begin_or_before_end ()

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_begin_or_before_end () const

void	mcrl2::lts::detail::bisim_gjkw::succ_entry::set_slice_begin_or_before_end (succ_iter_t new_value)

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_begin ()

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_begin () const

static succ_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_end (succ_iter_t this_)

static succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_end (succ_const_iter_t this_)

static void	mcrl2::lts::detail::bisim_gjkw::succ_entry::slice_add_work_to_transns (succ_const_iter_t this_, enum check_complexity::counter_type ctr, unsigned max_value)

std::string	mcrl2::lts::detail::bisim_gjkw::pred_entry::debug_id_short () const
	print a short transition identification for debugging

std::string	mcrl2::lts::detail::bisim_gjkw::pred_entry::debug_id () const
	print a transition identification for debugging

	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::B_to_C_descriptor (B_to_C_iter_t begin_, B_to_C_iter_t end_)

const block_t *	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::from_block () const
	compute the source block of the transitions in this slice

block_t *	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::from_block ()

const constln_t *	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::to_constln () const
	compute the goal constellation of the transitions in this slice

constln_t *	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::to_constln ()

bool	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::needs_postprocessing () const
	returns true iff the slice is marked for postprocessing

std::string	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::debug_id () const
	print a B_to_C slice identification for debugging

bool	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::add_work_to_bottom_transns (enum check_complexity::counter_type ctr, unsigned max_value)

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap_in (B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap_out (pred_iter_t const pos1, pred_iter_t const pos2)

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap_B_to_C (succ_iter_t const pos1, succ_iter_t const pos2)

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::swap3_B_to_C (succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)

	mcrl2::lts::detail::bisim_gjkw::part_trans_t::part_trans_t (trans_type m)

	mcrl2::lts::detail::bisim_gjkw::part_trans_t::~part_trans_t ()

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::clear ()
	clear allocated memory

trans_type	mcrl2::lts::detail::bisim_gjkw::part_trans_t::trans_size () const

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::split_inert_to_C (block_t *B)
	handle the transitions from the splitter to its own constellation

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::part_trans_t::change_to_C (pred_iter_t pred_iter, ONLY_IF_DEBUG(constln_t SpC, constln_t NewC,) bool first_transition_of_state, bool first_transition_of_block)
	transition target is moved to a new constellation

bool	mcrl2::lts::detail::bisim_gjkw::part_trans_t::split_s_inert_out (state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
	Split outgoing transitions of a state in the splitter.

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::make_noninert (succ_iter_t const succ_iter)

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_blue_block_created (block_t OldB, block_t NewB)
	handle B_to_C slices after a new blue block has been created

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_red_block_created (block_t OldB, block_t NewB, bool postprocessing)
	handle B_to_C slices after a new red block has been created

B_to_C_const_iter_t	mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_begin () const

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_end ()

pred_const_iter_t	mcrl2::lts::detail::bisim_gjkw::part_trans_t::pred_end () const

succ_const_iter_t	mcrl2::lts::detail::bisim_gjkw::part_trans_t::succ_end () const

void	mcrl2::lts::detail::bisim_gjkw::part_trans_t::assert_stability (const part_state_t &part_st) const
	assert that the data structure is consistent and stable

	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::Key (const label_type &f, const state_type &s)

bool	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::operator== (const Key &other) const

std::size_t	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::KeyHasher::operator() (const Key &k) const

	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::bisim_partitioner_gjkw_initialise_helper (LTS_TYPE &l, bool branching, bool preserve_divergence)
	constructor of the helper class

void	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::init_transitions (part_state_t &part_st, part_trans_t &part_tr, bool branching, bool preserve_divergence)
	initialise the state in part_st and the transitions in part_tr

void	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::replace_transition_system (const part_state_t &part_st, ONLY_IF_DEBUG(bool branching,) bool preserve_divergence)
	Replaces the transition relation of the current LTS by the transitions of the bisimulation-reduced transition system.

state_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::get_nr_of_states () const
	provides the number of states in the Kripke structure

trans_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::get_nr_of_transitions () const
	provides the number of transitions in the Kripke structure

	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::bisim_partitioner_gjkw (LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)

	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::~bisim_partitioner_gjkw ()

void	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::replace_transition_system (bool branching, bool preserve_divergence)

static state_type	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::num_eq_classes ()

state_type	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::get_eq_class (state_type s) const

bool	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::in_same_class (state_type s, state_type t) const

void	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::create_initial_partition_gjkw (bool branching, bool preserve_divergence)

void	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::refine_partition_until_it_becomes_stable_gjkw ()

bisim_gjkw::block_t *	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::refine (bisim_gjkw::block_t RfnB, const bisim_gjkw::constln_t SpC, const bisim_gjkw::B_to_C_descriptor FromRed, bool postprocessing, const bisim_gjkw::constln_t NewC=nullptr)
	refine a block into the part that can reach `SpC` and the part that cannot

bisim_gjkw::block_t *	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::postprocess_new_bottom (bisim_gjkw::block_t *RedB)
	Split a block with new bottom states as needed.

Variables
pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_in_begin
	iterator to first incoming transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_out_begin
	iterator to first outgoing transition

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_in_begin
	iterator to first inert incoming transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_out_begin
	iterator to first inert outgoing transition

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_out_end
	iterator past the last inert outgoing transition

block_t *	mcrl2::lts::detail::bisim_gjkw::state_info_entry::block
	block where the state belongs

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::pos
	position of the state in the permutation array

state_type	mcrl2::lts::detail::bisim_gjkw::state_info_entry::notblue
	number of inert transitions to non-blue states

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::int_current_constln
	iterator to first outgoing transition to the constellation of interest

static state_info_const_ptr	mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_begin
	pointer at the first entry in the `state_info` array

static state_info_const_ptr	mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_end
	pointer past the last actual entry in the `state_info` array

check_complexity::state_counter_t	mcrl2::lts::detail::bisim_gjkw::state_info_entry::work_counter

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_end
	iterator past the last state of the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_begin
	iterator to the first state of the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_marked_nonbottom_begin
	iterator to the first marked non-bottom state of the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_bottom_begin
	iterator to the first bottom state of the block

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_marked_bottom_begin
	iterator to the first marked bottom state of the block

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_inert_begin
	iterator to the first inert transition of the block

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::int_inert_end
	iterator past the last inert transition of the block

B_to_C_desc_list	mcrl2::lts::detail::bisim_gjkw::block_t::to_constln
	list of B_to_C with transitions from this block

constln_t *	mcrl2::lts::detail::bisim_gjkw::block_t::int_constln
	constellation to which the block belongs

block_t *	mcrl2::lts::detail::bisim_gjkw::block_t::refinable_next
	next block in the list of refinable blocks

static block_t *	mcrl2::lts::detail::bisim_gjkw::block_t::refinable_first = nullptr
	first block in the list of refinable blocks

state_type	mcrl2::lts::detail::bisim_gjkw::block_t::int_seqnr
	unique sequence number of this block

static state_type	mcrl2::lts::detail::bisim_gjkw::block_t::nr_of_blocks = 0
	total number of blocks with unique sequence number allocated

static permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::perm_begin

check_complexity::block_counter_t	mcrl2::lts::detail::bisim_gjkw::block_t::work_counter

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::int_end
	iterator past the last state in the constellation

permutation_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::int_begin
	iterator to the first state in the constellation

constln_t *	mcrl2::lts::detail::bisim_gjkw::constln_t::nontrivial_next
	next constellation in the list of non-trivial constellations

static constln_t *	mcrl2::lts::detail::bisim_gjkw::constln_t::nontrivial_first = nullptr
	first constellation in the list of non-trivial constellations

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::postprocess_begin
	iterator to the first transition into this constellation that needs postprocessing

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::constln_t::postprocess_end
	iterator past the last transition into this constellation that needs postprocessing

const state_type	mcrl2::lts::detail::bisim_gjkw::constln_t::sort_key
	sort key to order constellation-related information

permutation_t	mcrl2::lts::detail::bisim_gjkw::part_state_t::permutation
	permutation array

fixed_vector< state_info_entry >	mcrl2::lts::detail::bisim_gjkw::part_state_t::state_info
	array with all other information about states

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::B_to_C

state_info_ptr	mcrl2::lts::detail::bisim_gjkw::succ_entry::target

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::succ_entry::int_slice_begin_or_before_end
	points to the last or the first transition to the same constellation

succ_iter_t	mcrl2::lts::detail::bisim_gjkw::pred_entry::succ

state_info_ptr	mcrl2::lts::detail::bisim_gjkw::pred_entry::source

check_complexity::trans_counter_t	mcrl2::lts::detail::bisim_gjkw::pred_entry::work_counter

pred_iter_t	mcrl2::lts::detail::bisim_gjkw::B_to_C_entry::pred

B_to_C_desc_iter_t	mcrl2::lts::detail::bisim_gjkw::B_to_C_entry::B_to_C_slice

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::end

B_to_C_iter_t	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::begin

check_complexity::B_to_C_counter_t	mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::work_counter

fixed_vector< pred_entry >	mcrl2::lts::detail::bisim_gjkw::part_trans_t::pred

fixed_vector< succ_entry >	mcrl2::lts::detail::bisim_gjkw::part_trans_t::succ

fixed_vector< B_to_C_entry >	mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C

LTS_TYPE &	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::aut

state_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::nr_of_states

const state_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::orig_nr_of_states

trans_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::nr_of_transitions

label_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::first

state_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::second

std::unordered_map< Key, state_type, KeyHasher >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::extra_kripke_states

std::unordered_map< label_type, state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::action_block_map

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::noninert_out_per_state

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::inert_out_per_state

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::noninert_in_per_state

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::inert_in_per_state

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::noninert_out_per_block

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::inert_out_per_block

std::vector< state_type >	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::states_per_block

state_type	mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::nr_of_nonbottom_states

bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::init_helper

bisim_gjkw::part_state_t	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::part_st

bisim_gjkw::part_trans_t	mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::part_tr

Friends
class	mcrl2::lts::detail::bisim_gjkw::state_info_entry::part_state_t

class	mcrl2::lts::detail::bisim_gjkw::block_t::part_state_t

template<class LTS_TYPE >
class	mcrl2::lts::detail::bisim_gjkw::part_state_t::bisim_partitioner_gjkw_initialise_helper

template<class LTS_TYPE >
class	mcrl2::lts::detail::bisim_gjkw::part_trans_t::bisim_partitioner_gjkw_initialise_helper

Detailed Description

classes to calculate the stutter equivalence quotient of a LTS

Macro Definition Documentation

◆ BLOCK_NO_SEQNR

#define BLOCK_NO_SEQNR ((state_type) -1)

Definition at line 460 of file liblts_bisim_gjkw.h.

Function Documentation

◆ add_work_to_bottom_transns()

bool mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::add_work_to_bottom_transns	(	enum check_complexity::counter_type	ctr,
		unsigned	max_value
	)

inline

The function is meant to transfer work temporarily assigned to the B_to_C slice to the transitions in the slice. It is used during handling of new bottom states, so the work is only assigned to transitions that start in a (new) bottom state. If at this moment no such (new) bottom state has been found, the work is kept with the slice and the function returns false. The work should be transferred later (but if there is no later transfer, it should be tested that the function returns true).

Definition at line 1421 of file liblts_bisim_gjkw.h.

◆ assert_stability()

void mcrl2::lts::detail::bisim_gjkw::part_trans_t::assert_stability ( const part_state_t & part_st ) const

assert that the data structure is consistent and stable

The data structure is tested against a large number of assertions to ensure that everything is consistent, e. g. pointers that should point to successors of state s actually point to a transition that starts in s.

Additionally, it is asserted that the partition is stable. i. e. every bottom state in every block can reach exactly the constellations in the list of constellations that should be reachable from it, and every nonbottom state can reach a subset of them.

Definition at line 1019 of file liblts_bisim_gjkw.cpp.

◆ assign_seqnr()

void mcrl2::lts::detail::bisim_gjkw::block_t::assign_seqnr ( )

inline

assigns a unique sequence number

Definition at line 502 of file liblts_bisim_gjkw.h.

◆ B_to_C_begin()

B_to_C_const_iter_t mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_begin ( ) const

inline

Definition at line 1634 of file liblts_bisim_gjkw.h.

◆ B_to_C_descriptor()

mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::B_to_C_descriptor	(	B_to_C_iter_t	begin_,
		B_to_C_iter_t	end_
	)

inline

Definition at line 1345 of file liblts_bisim_gjkw.h.

◆ B_to_C_end()

B_to_C_iter_t mcrl2::lts::detail::bisim_gjkw::part_trans_t::B_to_C_end ( )

inline

Definition at line 1635 of file liblts_bisim_gjkw.h.

◆ begin() [1/4]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::begin ( )

inline

Definition at line 595 of file liblts_bisim_gjkw.h.

◆ begin() [2/4]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::begin ( )

inline

iterator to the first state in the constellation

Definition at line 923 of file liblts_bisim_gjkw.h.

◆ begin() [3/4]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::begin ( ) const

inline

iterator to the first state in the block

Definition at line 594 of file liblts_bisim_gjkw.h.

◆ begin() [4/4]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::begin ( ) const

inline

constant iterator to the first state in the constellation

Definition at line 921 of file liblts_bisim_gjkw.h.

◆ bisim_partitioner_gjkw()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::bisim_partitioner_gjkw	(	LTS_TYPE &	l,
		bool	branching = `false`,
		bool	preserve_divergence = `false`
	)

inline

Definition at line 1779 of file liblts_bisim_gjkw.h.

◆ bisim_partitioner_gjkw_initialise_helper()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::bisim_partitioner_gjkw_initialise_helper	(	LTS_TYPE &	l,
		bool	branching,
		bool	preserve_divergence
	)

constructor of the helper class

Definition at line 1415 of file liblts_bisim_gjkw.cpp.

◆ block()

const block_t * mcrl2::lts::detail::bisim_gjkw::part_state_t::block ( state_type s ) const

inline

find block of a state

Parameters

s	number of the state

Returns: a pointer to the block where state s resides in

Definition at line 1108 of file liblts_bisim_gjkw.h.

◆ block_t()

mcrl2::lts::detail::bisim_gjkw::block_t::block_t	(	constln_t *const	constln_,
		permutation_iter_t const	begin_,
		permutation_iter_t const	end_
	)

inline

constructor

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

Parameters

constln_	constellation to which the block belongs
begin_	initial iterator to the first state of the block
end_	initial iterator past the last state of the block

Definition at line 474 of file liblts_bisim_gjkw.h.

◆ bottom_begin() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::bottom_begin ( )

inline

Definition at line 625 of file liblts_bisim_gjkw.h.

◆ bottom_begin() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::bottom_begin ( ) const

inline

iterator to the first bottom state in the block

Definition at line 624 of file liblts_bisim_gjkw.h.

◆ bottom_end() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::bottom_end ( )

inline

Definition at line 635 of file liblts_bisim_gjkw.h.

◆ bottom_end() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::bottom_end ( ) const

inline

iterator past the last bottom state in the block

Definition at line 634 of file liblts_bisim_gjkw.h.

◆ change_to_C()

succ_iter_t mcrl2::lts::detail::bisim_gjkw::part_trans_t::change_to_C	(	pred_iter_t	pred_iter,
		ONLY_IF_DEBUG(constln_t SpC, constln_t NewC,) bool	first_transition_of_state,
		bool	first_transition_of_block
	)

transition target is moved to a new constellation

part_trans_t::change_to_C has to be called after a transition target has changed its constellation. The member function will adapt the transition data structure. It assumes that the transition is non-inert and that the new constellation does not (yet) have inert incoming transitions. It returns the boundary between transitions to SpC and transitions to NewC in the state's outgoing transition array.

Parameters

pred_iter	transition that has to be changed
SpC	splitter constellation
NewC	new constellation, where the transition goes to now
first_transition_of_state	This is the first transition of the state, so a new constln slice is started.
first_transition_of_block	This is the first transition of the block, so a new B_to_C slice has to be allocated.

Definition at line 474 of file liblts_bisim_gjkw.cpp.

◆ clear() [1/2]

void mcrl2::lts::detail::bisim_gjkw::part_state_t::clear ( )

inline

deallocates constellations and blocks

This function can be called shortly before destructing the partition. Afterwards, the data structure is in a unusable state, as all information on states, blocks and constellations is deleted and deallocated.

Definition at line 1069 of file liblts_bisim_gjkw.h.

◆ clear() [2/2]

void mcrl2::lts::detail::bisim_gjkw::part_trans_t::clear ( )

inline

clear allocated memory

Definition at line 1555 of file liblts_bisim_gjkw.h.

◆ constln() [1/4]

constln_t * mcrl2::lts::detail::bisim_gjkw::state_info_entry::constln ( )

inline

Definition at line 2004 of file liblts_bisim_gjkw.h.

◆ constln() [2/4]

constln_t * mcrl2::lts::detail::bisim_gjkw::block_t::constln ( )

inline

Definition at line 578 of file liblts_bisim_gjkw.h.

◆ constln() [3/4]

const constln_t * mcrl2::lts::detail::bisim_gjkw::state_info_entry::constln ( ) const

inline

get constellation where the state belongs

get the constellation of the state

Definition at line 1999 of file liblts_bisim_gjkw.h.

◆ constln() [4/4]

const constln_t * mcrl2::lts::detail::bisim_gjkw::block_t::constln ( ) const

inline

constellation where the block belongs to

Definition at line 577 of file liblts_bisim_gjkw.h.

◆ constln_t()

mcrl2::lts::detail::bisim_gjkw::constln_t::constln_t	(	state_type	sort_key_,
		permutation_iter_t	begin_,
		permutation_iter_t	end_,
		B_to_C_iter_t	postprocess_none
	)

inline

constructor

Parameters

begin_	iterator to the first state in the constellation
end_	iterator past the last state in the constellation

Definition at line 862 of file liblts_bisim_gjkw.h.

◆ create_initial_partition_gjkw()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::create_initial_partition_gjkw	(	bool	branching,
		bool	preserve_divergence
	)

private

Definition at line 1833 of file liblts_bisim_gjkw.cpp.

◆ current_constln() [1/2]

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::current_constln ( )

inline

Definition at line 202 of file liblts_bisim_gjkw.h.

◆ current_constln() [2/2]

succ_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::current_constln ( ) const

inline

Definition at line 201 of file liblts_bisim_gjkw.h.

◆ debug_id() [1/5]

std::string mcrl2::lts::detail::bisim_gjkw::state_info_entry::debug_id ( ) const

inline

print a state identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 346 of file liblts_bisim_gjkw.h.

◆ debug_id() [2/5]

std::string mcrl2::lts::detail::bisim_gjkw::block_t::debug_id ( ) const

inline

print a block identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 787 of file liblts_bisim_gjkw.h.

◆ debug_id() [3/5]

std::string mcrl2::lts::detail::bisim_gjkw::constln_t::debug_id ( ) const

inline

print a constellation identification for debugging

Definition at line 999 of file liblts_bisim_gjkw.h.

◆ debug_id() [4/5]

std::string mcrl2::lts::detail::bisim_gjkw::pred_entry::debug_id ( ) const

inline

print a transition identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 1301 of file liblts_bisim_gjkw.h.

◆ debug_id() [5/5]

std::string mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::debug_id ( ) const

inline

print a B_to_C slice identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 1384 of file liblts_bisim_gjkw.h.

◆ debug_id_short() [1/2]

std::string mcrl2::lts::detail::bisim_gjkw::state_info_entry::debug_id_short ( ) const

inline

print a short state identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 337 of file liblts_bisim_gjkw.h.

◆ debug_id_short() [2/2]

std::string mcrl2::lts::detail::bisim_gjkw::pred_entry::debug_id_short ( ) const

inline

print a short transition identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 1293 of file liblts_bisim_gjkw.h.

◆ end() [1/4]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::end ( )

inline

Definition at line 603 of file liblts_bisim_gjkw.h.

◆ end() [2/4]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::end ( )

inline

iterator past the last state in the constellation

Definition at line 933 of file liblts_bisim_gjkw.h.

◆ end() [3/4]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::end ( ) const

inline

iterator past the last state in the block

Definition at line 602 of file liblts_bisim_gjkw.h.

◆ end() [4/4]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::end ( ) const

inline

constant iterator past the last state in the constellation

Definition at line 931 of file liblts_bisim_gjkw.h.

◆ from_block() [1/2]

block_t * mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::from_block ( )

inline

Definition at line 1355 of file liblts_bisim_gjkw.h.

◆ from_block() [2/2]

const block_t * mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::from_block ( ) const

inline

compute the source block of the transitions in this slice

Definition at line 1351 of file liblts_bisim_gjkw.h.

◆ FromRed()

B_to_C_descriptor * mcrl2::lts::detail::bisim_gjkw::block_t::FromRed ( const constln_t * SpC )

inline

read FromRed

Definition at line 2010 of file liblts_bisim_gjkw.h.

◆ get_eq_class()

template<class LTS_TYPE >

state_type mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::get_eq_class ( state_type s ) const

inline

Definition at line 1810 of file liblts_bisim_gjkw.h.

◆ get_nontrivial_next()

const constln_t * mcrl2::lts::detail::bisim_gjkw::constln_t::get_nontrivial_next ( ) const

inline

provides the next non-trivial constellation

This (non-static!) function just returns the next non-trivial constellation in the list. Note: If this constellation is the last in the list of non-trivial constellations, the convention is that the next pointer points to this constellation self (to distinguish it from nullptr).

Definition at line 887 of file liblts_bisim_gjkw.h.

◆ get_nr_of_states()

template<class LTS_TYPE >

state_type mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::get_nr_of_states ( ) const

inline

provides the number of states in the Kripke structure

Definition at line 1748 of file liblts_bisim_gjkw.h.

◆ get_nr_of_transitions()

template<class LTS_TYPE >

trans_type mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::get_nr_of_transitions ( ) const

inline

provides the number of transitions in the Kripke structure

Definition at line 1751 of file liblts_bisim_gjkw.h.

◆ get_some_nontrivial()

static constln_t * mcrl2::lts::detail::bisim_gjkw::constln_t::get_some_nontrivial ( )

inlinestatic

provides an arbitrary non-trivial constellation

The static function is implemented in a way to provide the first constellation in the list of non-trivial constellations.

Definition at line 879 of file liblts_bisim_gjkw.h.

◆ get_some_refinable()

static block_t * mcrl2::lts::detail::bisim_gjkw::block_t::get_some_refinable ( )

inlinestatic

provides an arbitrary refinable block

Definition at line 510 of file liblts_bisim_gjkw.h.

◆ in_same_class()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::in_same_class	(	state_type	s,
		state_type	t
	)		const

inline

Definition at line 1815 of file liblts_bisim_gjkw.h.

◆ inert_begin() [1/2]

B_to_C_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::inert_begin ( )

inline

Definition at line 718 of file liblts_bisim_gjkw.h.

◆ inert_begin() [2/2]

B_to_C_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::inert_begin ( ) const

inline

iterator to the first inert transition of the block

Definition at line 717 of file liblts_bisim_gjkw.h.

◆ inert_end() [1/2]

B_to_C_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::inert_end ( )

inline

Definition at line 726 of file liblts_bisim_gjkw.h.

◆ inert_end() [2/2]

B_to_C_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::inert_end ( ) const

inline

iterator past the last inert transition of the block

Definition at line 725 of file liblts_bisim_gjkw.h.

◆ inert_pred_begin() [1/2]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_begin ( )

inline

Definition at line 256 of file liblts_bisim_gjkw.h.

◆ inert_pred_begin() [2/2]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_begin ( ) const

inline

iterator to first inert incoming transition

Definition at line 255 of file liblts_bisim_gjkw.h.

◆ inert_pred_end() [1/2]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_end ( )

inline

Definition at line 265 of file liblts_bisim_gjkw.h.

◆ inert_pred_end() [2/2]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_pred_end ( ) const

inline

iterator one past the last inert incoming transition

Definition at line 264 of file liblts_bisim_gjkw.h.

◆ inert_succ_begin() [1/2]

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_begin ( )

inline

Definition at line 291 of file liblts_bisim_gjkw.h.

◆ inert_succ_begin() [2/2]

succ_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_begin ( ) const

inline

iterator to first inert outgoing transition

Definition at line 290 of file liblts_bisim_gjkw.h.

◆ inert_succ_end() [1/2]

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_end ( )

inline

Definition at line 310 of file liblts_bisim_gjkw.h.

◆ inert_succ_end() [2/2]

succ_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::inert_succ_end ( ) const

inline

iterator past the last inert outgoing transition

Definition at line 309 of file liblts_bisim_gjkw.h.

◆ init_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::init_transitions	(	part_state_t &	part_st,
		part_trans_t &	part_tr,
		bool	branching,
		bool	preserve_divergence
	)

inline

initialise the state in part_st and the transitions in part_tr

Definition at line 1501 of file liblts_bisim_gjkw.cpp.

◆ is_refinable()

bool mcrl2::lts::detail::bisim_gjkw::block_t::is_refinable ( ) const

inline

checks whether the block is refinable

Returns: true if the block is refinable

Definition at line 514 of file liblts_bisim_gjkw.h.

◆ is_trivial()

bool mcrl2::lts::detail::bisim_gjkw::constln_t::is_trivial ( ) const

inline

returns true iff the constellation is trivial

If this constellation is the last in the list of non-trivial constellations, the convention is that the next pointer points to this constellation itself (to distinguish it from nullptr).

Definition at line 915 of file liblts_bisim_gjkw.h.

◆ Key()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::Key	(	const label_type &	f,
		const state_type &	s
	)

inline

Definition at line 1699 of file liblts_bisim_gjkw.h.

◆ make_noninert()

void mcrl2::lts::detail::bisim_gjkw::part_trans_t::make_noninert ( succ_iter_t const succ_iter )

inline

Definition at line 1597 of file liblts_bisim_gjkw.h.

◆ make_nonrefinable()

void mcrl2::lts::detail::bisim_gjkw::block_t::make_nonrefinable ( )

inline

makes a block non-refinable (i. e. removes it from the respective list)

This member function only works if the block is the first one in the list (which will normally be the case).

Definition at line 534 of file liblts_bisim_gjkw.h.

◆ make_nontrivial()

void mcrl2::lts::detail::bisim_gjkw::constln_t::make_nontrivial ( )

inline

makes a constellation non-trivial (i. e. inserts it into the respective list)

Definition at line 901 of file liblts_bisim_gjkw.h.

◆ make_refinable()

bool mcrl2::lts::detail::bisim_gjkw::block_t::make_refinable ( )

inline

makes a block refinable (i. e. inserts it into the respective list)

Returns: true if the block was not refinable before

Definition at line 519 of file liblts_bisim_gjkw.h.

◆ make_trivial()

void mcrl2::lts::detail::bisim_gjkw::constln_t::make_trivial ( )

inline

makes a constellation trivial (i. e. removes it from the respective list)

This member function only works if the constellation is the first one in the list (which will normally be the case).

Definition at line 893 of file liblts_bisim_gjkw.h.

◆ mark()

bool mcrl2::lts::detail::bisim_gjkw::block_t::mark ( state_info_ptr 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. If s is an old bottom state, it is treated as if it already were marked.

Parameters

s	the state that has to be marked

Returns: true if the state was not marked before

Definition at line 757 of file liblts_bisim_gjkw.h.

◆ mark_nonbottom()

bool mcrl2::lts::detail::bisim_gjkw::block_t::mark_nonbottom ( state_info_ptr 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 if the state was not marked before

Definition at line 743 of file liblts_bisim_gjkw.h.

◆ marked_bottom_begin() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_begin ( )

inline

Definition at line 704 of file liblts_bisim_gjkw.h.

◆ marked_bottom_begin() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_begin ( ) const

inline

iterator to the first marked bottom state in the block

Definition at line 700 of file liblts_bisim_gjkw.h.

◆ marked_bottom_end() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_end ( )

inline

Definition at line 714 of file liblts_bisim_gjkw.h.

◆ marked_bottom_end() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_bottom_end ( ) const

inline

iterator past the last marked bottom state in the block

This includes the old bottom states.

Definition at line 713 of file liblts_bisim_gjkw.h.

◆ marked_bottom_size()

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

inline

provides the number of marked bottom states in the block

This size includes the old bottom states.

Definition at line 545 of file liblts_bisim_gjkw.h.

◆ marked_nonbottom_begin() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_begin ( )

inline

Definition at line 662 of file liblts_bisim_gjkw.h.

◆ marked_nonbottom_begin() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_begin ( ) const

inline

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

Definition at line 658 of file liblts_bisim_gjkw.h.

◆ marked_nonbottom_end() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_end ( )

inline

Definition at line 678 of file liblts_bisim_gjkw.h.

◆ marked_nonbottom_end() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::marked_nonbottom_end ( ) const

inline

iterator one past the last marked non-bottom state in the block

Definition at line 674 of file liblts_bisim_gjkw.h.

◆ marked_size()

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

inline

provides the number of marked states in the block

This size includes the old bottom states; in other words, the old bottom states are always regarded as marked.

Definition at line 553 of file liblts_bisim_gjkw.h.

◆ needs_postprocessing()

bool mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor::needs_postprocessing ( ) const

inline

returns true iff the slice is marked for postprocessing

The function uses the data registered with the goal constellation.

Definition at line 1373 of file liblts_bisim_gjkw.h.

◆ new_blue_block_created()

void mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_blue_block_created	(	block_t *	OldB,
		block_t *	NewB
	)

handle B_to_C slices after a new blue block has been created

part_trans_t::new_blue_block_created splits the B_to_C-slices to reflect that some transitions now start in the new block NewB. They can no longer be in the same slice as the transitions that start in the old block. Its time complexity is O(1 + |out(NewB)|).

Parameters

RfnB	the old block that has been refined (now the red subblock)
NewB	the new block (the blue subblock)

Definition at line 666 of file liblts_bisim_gjkw.cpp.

◆ new_red_block_created()

void mcrl2::lts::detail::bisim_gjkw::part_trans_t::new_red_block_created	(	block_t *	OldB,
		block_t *	NewB,
		bool	postprocessing
	)

handle B_to_C slices after a new red block has been created

part_trans_t::new_red_block_created splits the B_to_C-slices to reflect that some transitions now start in the new block NewB. They can no longer be in the same slice as the transitions that start in the old block. Its time complexity is O(1 + |out(NewB)|).

Parameters

RfnB	the old block that has been refined (now the blue subblock)
NewB	the new block (the red subblock)
postprocessing	true iff the refinement happened during postprocessing. (Otherwise, the refinement should preserve the information about `FromRed()`).

Definition at line 837 of file liblts_bisim_gjkw.cpp.

◆ nonbottom_begin() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_begin ( )

inline

Definition at line 611 of file liblts_bisim_gjkw.h.

◆ nonbottom_begin() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_begin ( ) const

inline

iterator to the first non-bottom state in the block

Definition at line 610 of file liblts_bisim_gjkw.h.

◆ nonbottom_end() [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_end ( )

inline

Definition at line 615 of file liblts_bisim_gjkw.h.

◆ nonbottom_end() [2/2]

permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::nonbottom_end ( ) const

inline

iterator past the last non-bottom state in the block

Definition at line 614 of file liblts_bisim_gjkw.h.

◆ noninert_pred_begin() [1/2]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_begin ( )

inline

Definition at line 248 of file liblts_bisim_gjkw.h.

◆ noninert_pred_begin() [2/2]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_begin ( ) const

inline

iterator to first non-inert incoming transition

Definition at line 247 of file liblts_bisim_gjkw.h.

◆ noninert_pred_end() [1/2]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_end ( )

inline

Definition at line 252 of file liblts_bisim_gjkw.h.

◆ noninert_pred_end() [2/2]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::noninert_pred_end ( ) const

inline

iterator past the last non-inert incoming transition

Definition at line 251 of file liblts_bisim_gjkw.h.

◆ num_eq_classes()

template<class LTS_TYPE >

static state_type mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::num_eq_classes ( )

inlinestatic

Definition at line 1805 of file liblts_bisim_gjkw.h.

◆ operator()()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::KeyHasher::operator() ( const Key & k ) const

inline

Definition at line 1713 of file liblts_bisim_gjkw.h.

◆ operator<() [1/2]

bool mcrl2::lts::detail::bisim_gjkw::block_t::operator< ( const block_t & other ) const

inline

compares two blocks for ordering them

The blocks are ordered according to their positions in the permutation array. This is a suitable order, as blocks may be refined, but never swap positions as a whole. Refining will make the new subblocks compare in the same way to other blocks as the original, larger block.

Definition at line 571 of file liblts_bisim_gjkw.h.

◆ operator<() [2/2]

bool mcrl2::lts::detail::bisim_gjkw::constln_t::operator< ( const constln_t & other ) const

inline

compares two constellations for ordering them

Constellations are ordered according to their sort keys. The keys have to be assigned in a way that when a constellation is split, the parts are placed where the split constellation was in the order. This can be achieved by assigning sort keys that are related to the size of the constellation.

Definition at line 949 of file liblts_bisim_gjkw.h.

◆ operator<=()

bool mcrl2::lts::detail::bisim_gjkw::constln_t::operator<= ( const constln_t & other ) const

inline

Definition at line 954 of file liblts_bisim_gjkw.h.

◆ operator==()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key::operator== ( const Key & other ) const

inline

Definition at line 1704 of file liblts_bisim_gjkw.h.

◆ operator>()

bool mcrl2::lts::detail::bisim_gjkw::constln_t::operator> ( const constln_t & other ) const

inline

Definition at line 953 of file liblts_bisim_gjkw.h.

◆ operator>=()

bool mcrl2::lts::detail::bisim_gjkw::constln_t::operator>= ( const constln_t & other ) const

inline

Definition at line 955 of file liblts_bisim_gjkw.h.

◆ part_state_t()

mcrl2::lts::detail::bisim_gjkw::part_state_t::part_state_t ( state_type n )

inline

constructor

The constructor allocates memory, but does not actually initialise the partition. Immediately afterwards, the initialisation helper bisim_partitioner_gjkw_initialise_helper::init_transitions() should be called.

Parameters

n	number of states in the Kripke structure

Definition at line 1045 of file liblts_bisim_gjkw.h.

◆ part_trans_t()

mcrl2::lts::detail::bisim_gjkw::part_trans_t::part_trans_t ( trans_type m )

inline

Definition at line 1545 of file liblts_bisim_gjkw.h.

◆ permutation_begin()

static permutation_const_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::permutation_begin ( )

inlinestatic

provide an iterator to the beginning of the permutation array

This iterator is required to be able to print identifications for debugging. It is only available if compiled in Debug mode.

Definition at line 797 of file liblts_bisim_gjkw.h.

◆ postprocess_new_bottom()

template<class LTS_TYPE >

bisim_gjkw::block_t * mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::postprocess_new_bottom ( bisim_gjkw::block_t * RedB )

private

Split a block with new bottom states as needed.

The function splits RedB by checking whether all new bottom states can reach the constellations that RedB can reach.

When this function starts, it assumes that the old bottom states of RedB are marked and the new ones are not. It is an error if RedB does not contain any new bottom states. The function implements Algorithm 4 of [GJKW 2017]. It first separates the old from the new bottom states; then it walks through all constellations that can be reached from the new bottom states to separate them into smaller, stable subblocks. The return value is the block containing the old bottom states, resulting from the first separation.

Parameters

RedB	block containing new bottom states that need to be stabilised

Returns: the block containing the old bottom states (and every state in RedB that can reach some old bottom state through inert transitions)

Definition at line 3018 of file liblts_bisim_gjkw.cpp.

◆ pred_begin() [1/2]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_begin ( )

inline

Definition at line 226 of file liblts_bisim_gjkw.h.

◆ pred_begin() [2/2]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_begin ( ) const

inline

iterator to first incoming transition

Definition at line 225 of file liblts_bisim_gjkw.h.

◆ pred_end() [1/3]

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_end ( )

inline

Definition at line 237 of file liblts_bisim_gjkw.h.

◆ pred_end() [2/3]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::pred_end ( ) const

inline

iterator past the last incoming transition

Definition at line 233 of file liblts_bisim_gjkw.h.

◆ pred_end() [3/3]

pred_const_iter_t mcrl2::lts::detail::bisim_gjkw::part_trans_t::pred_end ( ) const

inline

Definition at line 1636 of file liblts_bisim_gjkw.h.

◆ print_block()

void mcrl2::lts::detail::bisim_gjkw::part_state_t::print_block	(	const char *	message,
		const block_t *	B,
		permutation_const_iter_t	begin,
		permutation_const_iter_t	end
	)		const

private

print a slice of the partition (typically a block)

If the slice indicated by the parameters is not empty, the states in this slice will be printed.

Parameters

message	text printed as a title if the slice is not empty
B	block that is being printed (it is checked whether states belong to this block)
begin	iterator to the beginning of the slice
end	iterator past the end of the slice

Definition at line 221 of file liblts_bisim_gjkw.cpp.

◆ print_part()

void mcrl2::lts::detail::bisim_gjkw::part_state_t::print_part ( const part_trans_t & part_tr ) const

print the partition as a tree (per constellation and block)

The function prints all constellations (in order); for each constellation it prints the blocks it consists of; and for each block, it lists its states, separated into nonbottom and bottom states.

Parameters

part_tr partition for the transitions

Definition at line 255 of file liblts_bisim_gjkw.cpp.

◆ print_trans()

void mcrl2::lts::detail::bisim_gjkw::part_state_t::print_trans ( ) const

print all transitions

For each state (in order), its outgoing transitions are listed, sorted by goal constellation. The function also indicates where the current constellation pointer of the state points at.

Definition at line 309 of file liblts_bisim_gjkw.cpp.

◆ refine()

template<class LTS_TYPE >

bisim_gjkw::block_t * mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::refine	(	bisim_gjkw::block_t *	RfnB,
		const bisim_gjkw::constln_t *	SpC,
		const bisim_gjkw::B_to_C_descriptor *	FromRed,
		bool	postprocessing,
		const bisim_gjkw::constln_t *	NewC = `nullptr`
	)

private

refine a block into the part that can reach SpC and the part that cannot

At the beginning of a call to refine(), the block RfnB is sliced into these parts:

|          unmarked         |marked |         unmarked         |marked|
|         non-bottom        |non-bot|          bottom          |bottom|

The procedure will partition the block into two parts, called blue'' and red''. The red part can reach the splitter constellation SpC, the blue part cannot. Upon calling refine(), it is known that all marked states are red.

If states with a strong transition to SpC have not yet been found, the parameter FromRed indicates all such transitions, so refine() can easily find their sources. It is required that either some states are marked or a non-nullptr FromRed is supplied. In the latter case, also the current constellation pointer of all unmarked bottom states is set in a way that it makes easy to check whether the state has a transition to SpC. (Some non-bottom states may have their current constellation pointer set similarly; while this is not required, it still speeds up refine().)

refine() works by starting two coroutines to find states in the parts; as soon as the first coroutine finishes, the refinement can be completed.

Refine slices these states further as follows:

                                     refine_blue()    refine_red()
         shared variable            local variable   local variable
     notblue_initialised_end          visited_end     visited_begin
                v                          v                v
| blue  |notblue|notblue|    red    | blue |unknown|not blue|   red   |
|non-bot|  > 0  |undef'd| non-bottom|bottom|bottom | bottom | bottom  |
        ^               ^                          ^
  refine_blue()    block.unmarked_          block.unmarked_
 local variable    nonbottom_end()           bottom_end()
blue_nonbottom_end

blue non-bottom: states of which it is known that they are blue
notblue > 0: states that have an inert transition to some blue state, but for some transition it is not yet known whether they go to a red or a blue state
notblue undefined: for no inert transition it is known whether it goes to a red or a blue state
red non-bottom: states of which it is known that they are red
blue bottom: states of which it is known that they are blue
unknown bottom: states that have not yet been checked
not blue bottom: states of which the blue coroutine has found that they are red, but the red coroutine has not yet handled them
red bottom: states of which everybody knows that they are red

Note that the slices of red non-bottom and the red bottom states may become larger than the marked (non-)bottom states have been at the start of refine(). Upon termination of one of the two coroutines, states whose colour has not yet been determined become known to be of the colour of the unfinished coroutine.

Parameters

RfnB	the block that has to be refined
SpC	the splitter constellation
FromRed	the set of transitions from `RfnB` to `SpC`
size_SpB	(only used for measuring the time complexity, and only if called from line 2.26) the size of the original splitter block SpB, to which the work on red bottom states is ascribed.
postprocessing	true iff `refine()` is called during postprocessing new bottom states

Returns: a pointer to the block that contains the red part of RfnB.

The blue coroutine finds blue states in a block, i. e. states that cannot reach the splitter. It is one of the two coroutines that together implement the fast refinement of block RfnB into states that can reach the splitter SpC (red states) and those that cannot (blue states).

This coroutine assumes that RfnB is nontrivial, i. e. contains at least two states. refine() may be called in two ways: either the initially red states are marked, or a set of transitions from RfnB to SpC is given. In the first case, all unmarked bottom states are blue. In the second case, however, the first thing this coroutine has to do is to decide which bottom states are blue and which ones are not. In that case, it assumes that the current_constln pointer of bottom states is pointing to a place where a transition to SpC could be inserted. If there is already such a transition just before or after that memory location, the bottom state is actually red; otherwise, it is blue.

After having found the blue bottom states, the coroutine proceeds to find blue non-bottom states by walking through the predecessors of the blue states. As soon as can be determined that all inert outgoing transitions of a state lead to (other) blue states, this state is also blue – with one exception: if this state has a (non-inert) transition to the splitter. If refine() was called in the second way, one has to check the outgoing non-inert transitions to find out whether such a transition exists.

As soon as it becomes clear that the blue subblock will be larger, this coroutine is aborted. Otherwise, at the end RfnB is actually split into its two parts, and the coroutine closes with updating the inert-ness of transitions and finding new bottom states. New bottom states will be unmarked bottom states. (It may also happen that the blue subblock is empty; in that case, RfnB is not split.)

The coroutine implements the left-hand side of Algorithm 3 in [GJKW 2017].

The red coroutine finds red states in a block, i. e. states that can reach the splitter. It is one of the two coroutines that together implement the fast refinement of block RfnB into states that can reach the splitter (red states) and those that cannot (blue states).

This coroutine assumes that RfnB is nontrivial, i. e. contains at least two states, and that there is at least one red state in RfnB. The red states can be indicated in one of two ways: either some states of RfnB are marked, or the parameter FromRed indicates the set of transitions from RfnB to the splitter. Exactly one of the two must be chosen: If and only if some states are marked, FromRed should be nullptr.

If FromRed is not nullptr, the coroutine first finds initially red states, i. e. states with a transition to the splitter, and marks them. Note that it may happen that some non-bottom states (or even only non-bottom states) may be initially red as well. When all initially red states are marked, it proceeds to find other red states by walking through the inert predecessors of red states. Every such predecessor is also a red state.

As soon as it becomes clear that the red subblock will be larger, this coroutine is aborted. Otherwise, at the end RfnB is actually split into its two parts, and the coroutine closes with updating the inert-ness of transitions and finding new bottom states. New bottom states will be unmarked bottom states.

The coroutine implements the right-hand side of Algorithm 3 in [GJKW 2017].