Part_refine

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

Classes
class	mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >
	implements the main algorithm for the branching bisimulation quotient More...
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

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 ONLY_IF_DEBUG(, 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
check_complexity::block_counter_t	mcrl2::lts::detail::bisim_gjkw::block_t::work_counter
static permutation_const_iter_t	mcrl2::lts::detail::bisim_gjkw::block_t::perm_begin
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 458 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 1413 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 500 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 1606 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 1338 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 1607 of file liblts_bisim_gjkw.h.

begin() [1/4]

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

inline

Definition at line 593 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 919 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 592 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 917 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 1751 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 1104 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 472 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 623 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 622 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 633 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 632 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 1065 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 1527 of file liblts_bisim_gjkw.h.

constln() [1/4]

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

inline

Definition at line 1973 of file liblts_bisim_gjkw.h.

constln() [2/4]

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

inline

Definition at line 576 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 1968 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 575 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 858 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 785 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 995 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 1297 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 1377 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 1289 of file liblts_bisim_gjkw.h.

end() [1/4]

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

inline

Definition at line 601 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 929 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 600 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 927 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 1348 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 1344 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 1979 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 1782 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 883 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 1720 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 1723 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 875 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 508 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 1787 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 716 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 715 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 724 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 723 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 512 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 911 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 1671 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 1569 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 532 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 897 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 517 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 889 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 755 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 741 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 702 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 698 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 712 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 711 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 543 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 660 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 656 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 676 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 672 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 551 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 1366 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 609 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 608 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 613 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 612 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 1777 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 1685 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 569 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 945 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 950 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 1676 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 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 951 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 1041 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 1517 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 795 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 3004 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 1608 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   ONLY_IF_DEBUG, 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 find 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].

Definition at line 2361 of file liblts_bisim_gjkw.cpp.

refine_partition_until_it_becomes_stable_gjkw()

template<class LTS_TYPE >

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

private

Definition at line 1845 of file liblts_bisim_gjkw.cpp.

replace_transition_system() [1/2]

template<class LTS_TYPE >

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

inline

Definition at line 1770 of file liblts_bisim_gjkw.h.

replace_transition_system() [2/2]

template<class LTS_TYPE >

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.

Each transition (s, l, s') is replaced by a transition (t, l, t'), where t and t' are the equivalence classes of s and s', respectively. If the label l is internal, then the transition is only added if t != t' or preserve_divergence == true. This effectively removes all inert transitions. Duplicates are removed from the transitions in the new LTS.

Note that the number of states nor the initial state are not adapted by this method. These must be set separately.

The code is very much inspired by liblts_bisim_gw.h, which was written by Anton Wijs.

Precondition

The bisimulation equivalence classes have been computed.

Parameters

branching

Causes non-internal transitions to be removed.

Definition at line 1713 of file liblts_bisim_gjkw.cpp.

seqnr()

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

inline

Definition at line 505 of file liblts_bisim_gjkw.h.

set_begin() [1/2]

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

inline

Definition at line 594 of file liblts_bisim_gjkw.h.

set_begin() [2/2]

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

inline

set the iterator to the first state in the constellation

Definition at line 921 of file liblts_bisim_gjkw.h.

set_bottom_begin()

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

inline

Definition at line 624 of file liblts_bisim_gjkw.h.

set_constln()

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

inline

Definition at line 577 of file liblts_bisim_gjkw.h.

set_current_constln()

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

inline

Definition at line 203 of file liblts_bisim_gjkw.h.

set_end() [1/2]

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

inline

Definition at line 602 of file liblts_bisim_gjkw.h.

set_end() [2/2]

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

inline

set the iterator past the last state in the constellation

Definition at line 931 of file liblts_bisim_gjkw.h.

set_inert_begin()

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

inline

Definition at line 717 of file liblts_bisim_gjkw.h.

set_inert_begin_and_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  )

inline

Definition at line 729 of file liblts_bisim_gjkw.h.

set_inert_end()

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

inline

Definition at line 725 of file liblts_bisim_gjkw.h.

set_inert_pred_begin()

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

inline

Definition at line 257 of file liblts_bisim_gjkw.h.

set_inert_succ_begin()

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

inline

Definition at line 292 of file liblts_bisim_gjkw.h.

set_inert_succ_begin_and_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  )

inline

Definition at line 312 of file liblts_bisim_gjkw.h.

set_marked_bottom_begin()

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

inline

Definition at line 703 of file liblts_bisim_gjkw.h.

set_marked_nonbottom_begin()

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

inline

Definition at line 664 of file liblts_bisim_gjkw.h.

set_nonbottom_end()

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

inline

Definition at line 614 of file liblts_bisim_gjkw.h.

set_pred_begin()

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

inline

Definition at line 227 of file liblts_bisim_gjkw.h.

set_pred_end()

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

inline

Definition at line 241 of file liblts_bisim_gjkw.h.

set_slice_begin_or_before_end()

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

inline

Definition at line 1219 of file liblts_bisim_gjkw.h.

set_succ_begin()

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

inline

Definition at line 270 of file liblts_bisim_gjkw.h.

set_succ_end()

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

inline

Definition at line 284 of file liblts_bisim_gjkw.h.

set_unmarked_bottom_end()

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

inline

Definition at line 691 of file liblts_bisim_gjkw.h.

set_unmarked_nonbottom_end()

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

inline

Definition at line 648 of file liblts_bisim_gjkw.h.

SetFromRed()

void mcrl2::lts::detail::bisim_gjkw::block_t::SetFromRed ( B_to_C_desc_iter_t  new_fromred )

inline

set FromRed to an existing element in to_constln

Definition at line 2001 of file liblts_bisim_gjkw.h.

size() [1/2]

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

inline

provides the number of states in the block

Definition at line 539 of file liblts_bisim_gjkw.h.

size() [2/2]

state_type mcrl2::lts::detail::bisim_gjkw::constln_t::size ( ) const

inline

returns number of states in the constellation

Definition at line 937 of file liblts_bisim_gjkw.h.

slice_add_work_to_transns()

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  )

inlinestatic

adds work (for time complexity measurement) to every transition in the slice to which this_ belongs.

adds work (for time complexity measurement) to every transition in the slice.

Definition at line 1316 of file liblts_bisim_gjkw.h.

slice_begin() [1/2]

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

inline

Definition at line 1225 of file liblts_bisim_gjkw.h.

slice_begin() [2/2]

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

inline

Definition at line 1235 of file liblts_bisim_gjkw.h.

slice_begin_or_before_end() [1/2]

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

inline

Definition at line 1209 of file liblts_bisim_gjkw.h.

slice_begin_or_before_end() [2/2]

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

inline

Definition at line 1214 of file liblts_bisim_gjkw.h.

slice_end() [1/2]

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

inlinestatic

Definition at line 1259 of file liblts_bisim_gjkw.h.

slice_end() [2/2]

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

inlinestatic

Definition at line 1245 of file liblts_bisim_gjkw.h.

split_inert_to_C()

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

split_inert_to_C splits the B_to_C slice of block SpB to its own constellation into two slices: one for the inert and one for the non-inert transitions. It is called with SpB just after a constellation is split, as the transitions from SpB to itself (= the inert transitions) now go to a different constellation than the other transitions from SpB to its old constellation. It does, however, not adapt the other transition arrays to reflect that noninert and inert transitions from block SpB would go to different constellations.

Its time complexity is O(1+min{|out_noninert(SpB-->C)|, |inert_out(SpB)|}).

Parameters

SpB	pointer to the splitter block

Definition at line 392 of file liblts_bisim_gjkw.cpp.

split_off_blue()

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)

This function is called after a refinement function has found that the blue subblock is the smaller one. It creates a new block for the blue states.

Parameters

blue_nonbottom_end

iterator past the last blue non-bottom state

Returns

pointer to the new (blue) block

Definition at line 70 of file liblts_bisim_gjkw.cpp.

split_off_red()

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)

This function is called after a refinement function has found that the red subblock is the smaller one. It creates a new block for the red states.

Parameters

red_nonbottom_begin

iterator to the first red non-bottom state

Returns

pointer to the new (red) block

This function is called after a refinement function has found that the red subblock is the smaller one. It creates a new block for the red states.

Both split_off_blue() and split_off_red() unmark all states in the blue subblock and mark all bottom states in the red subblock. (This will help the caller to distinguish old bottom states from new bottom states found after split_off_blue() or split_off_red(), respectively.) The two functions use the same complexity counters because their operations belong together.

Parameters

red_nonbottom_begin

iterator to the first red non-bottom state

Returns

pointer to the new (red) block

Definition at line 149 of file liblts_bisim_gjkw.cpp.

split_off_small_block()

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

inline

split off a single block from the constellation

The function splits the current constellation after its first block or before its last block, whichever is smaller. It creates a new constellation for the split-off block and returns a pointer to the block.

It doesn't matter very much how ties are resolved here: part_tr.change_to_C() is faster if the first block is selected to be split off. part_tr.split_s_inert_out() is faster if the last block is selected.

Definition at line 958 of file liblts_bisim_gjkw.h.

split_s_inert_out()

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.

split_s_inert_out splits the outgoing transitions from s to its own constellation into two: the inert transitions become transitions to the new constellation of which s is now part; the non-inert transitions remain transitions to OldC. Its time complexity is O(1 + min { |out_\nottau(s)|, |out_\tau(s)| }).

Parameters

s	state whose outgoing transitions need to be split
OldC	old constellation (of which the splitter was a part earlier)

Returns

true iff the state also has transitions to OldC

Definition at line 555 of file liblts_bisim_gjkw.cpp.

state_size()

state_type mcrl2::lts::detail::bisim_gjkw::part_state_t::state_size ( ) const

inline

provide size of state space

Returns

the stored size of the state space

Definition at line 1099 of file liblts_bisim_gjkw.h.

succ_begin() [1/2]

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

inline

Definition at line 269 of file liblts_bisim_gjkw.h.

succ_begin() [2/2]

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

inline

iterator to first outgoing transition

Definition at line 268 of file liblts_bisim_gjkw.h.

succ_end() [1/3]

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

inline

Definition at line 280 of file liblts_bisim_gjkw.h.

succ_end() [2/3]

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

inline

iterator past the last outgoing transition

Definition at line 276 of file liblts_bisim_gjkw.h.

succ_end() [3/3]

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

inline

Definition at line 1609 of file liblts_bisim_gjkw.h.

surely_has_no_transition_to()

bool mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_no_transition_to

(

const constln_t *

SpC

)

const

surely_has_transition_to()

bool mcrl2::lts::detail::bisim_gjkw::state_info_entry::surely_has_transition_to

(

const constln_t *

SpC

)

const

swap3_B_to_C()

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  )

inlineprivate

Definition at line 1497 of file liblts_bisim_gjkw.h.

swap_B_to_C()

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

inlineprivate

Definition at line 1482 of file liblts_bisim_gjkw.h.

swap_in()

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  )

inlineprivate

Definition at line 1447 of file liblts_bisim_gjkw.h.

swap_out()

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

inlineprivate

Definition at line 1461 of file liblts_bisim_gjkw.h.

to_constln() [1/2]

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

inline

Definition at line 1358 of file liblts_bisim_gjkw.h.

to_constln() [2/2]

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

inline

compute the goal constellation of the transitions in this slice

Definition at line 1354 of file liblts_bisim_gjkw.h.

trans_size()

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

inline

Definition at line 1536 of file liblts_bisim_gjkw.h.

unmarked_bottom_begin() [1/2]

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

inline

Definition at line 683 of file liblts_bisim_gjkw.h.

unmarked_bottom_begin() [2/2]

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

inline

iterator to the first unmarked bottom state in the block

Definition at line 679 of file liblts_bisim_gjkw.h.

unmarked_bottom_end() [1/2]

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

inline

Definition at line 690 of file liblts_bisim_gjkw.h.

unmarked_bottom_end() [2/2]

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

inline

iterator past the last unmarked bottom state in the block

Definition at line 686 of file liblts_bisim_gjkw.h.

unmarked_bottom_size()

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

inline

provides the number of unmarked bottom states in the block

Definition at line 558 of file liblts_bisim_gjkw.h.

unmarked_nonbottom_begin() [1/2]

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

inline

Definition at line 637 of file liblts_bisim_gjkw.h.

unmarked_nonbottom_begin() [2/2]

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

inline

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

Definition at line 636 of file liblts_bisim_gjkw.h.

unmarked_nonbottom_end() [1/2]

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

inline

Definition at line 644 of file liblts_bisim_gjkw.h.

unmarked_nonbottom_end() [2/2]

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

inline

iterator past the last unmarked non-bottom state in the block

Definition at line 640 of file liblts_bisim_gjkw.h.

~bisim_partitioner_gjkw()

template<class LTS_TYPE >

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

inline

Definition at line 1760 of file liblts_bisim_gjkw.h.

~block_t()

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

inline

Definition at line 497 of file liblts_bisim_gjkw.h.

~constln_t()

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

inline

destructor

Definition at line 870 of file liblts_bisim_gjkw.h.

~part_state_t()

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

inline

destructor

The destructor assumes that the caller has already executed clear() to deallocate the memory for the partition.

Definition at line 1056 of file liblts_bisim_gjkw.h.

~part_trans_t()

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

inline

Definition at line 1522 of file liblts_bisim_gjkw.h.

Variable Documentation

action_block_map

template<class LTS_TYPE >

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

private

Definition at line 1697 of file liblts_bisim_gjkw.h.

aut

template<class LTS_TYPE >

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

private

Definition at line 1658 of file liblts_bisim_gjkw.h.

B_to_C [1/2]

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

Definition at line 1190 of file liblts_bisim_gjkw.h.

B_to_C [2/2]

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

private

Definition at line 1442 of file liblts_bisim_gjkw.h.

B_to_C_slice

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

Definition at line 1311 of file liblts_bisim_gjkw.h.

begin

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

Definition at line 1336 of file liblts_bisim_gjkw.h.

block

block_t* mcrl2::lts::detail::bisim_gjkw::state_info_entry::block

block where the state belongs

Definition at line 186 of file liblts_bisim_gjkw.h.

end

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

Definition at line 1336 of file liblts_bisim_gjkw.h.

extra_kripke_states

template<class LTS_TYPE >

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

private

Definition at line 1693 of file liblts_bisim_gjkw.h.

first

template<class LTS_TYPE >

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

Definition at line 1668 of file liblts_bisim_gjkw.h.

inert_in_per_state

template<class LTS_TYPE >

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

private

Definition at line 1700 of file liblts_bisim_gjkw.h.

inert_out_per_block

template<class LTS_TYPE >

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

private

Definition at line 1701 of file liblts_bisim_gjkw.h.

inert_out_per_state

template<class LTS_TYPE >

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

private

Definition at line 1699 of file liblts_bisim_gjkw.h.

init_helper

template<class LTS_TYPE >

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

private

Definition at line 1744 of file liblts_bisim_gjkw.h.

int_begin [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_begin

private

iterator to the first state of the block

Definition at line 410 of file liblts_bisim_gjkw.h.

int_begin [2/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::int_begin

private

iterator to the first state in the constellation

Definition at line 818 of file liblts_bisim_gjkw.h.

int_bottom_begin

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_bottom_begin

private

iterator to the first bottom state of the block

Definition at line 416 of file liblts_bisim_gjkw.h.

int_constln

constln_t* mcrl2::lts::detail::bisim_gjkw::block_t::int_constln

private

constellation to which the block belongs

Definition at line 440 of file liblts_bisim_gjkw.h.

int_current_constln

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::int_current_constln

private

iterator to first outgoing transition to the constellation of interest

Definition at line 195 of file liblts_bisim_gjkw.h.

int_end [1/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_end

private

iterator past the last state of the block

Definition at line 407 of file liblts_bisim_gjkw.h.

int_end [2/2]

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::constln_t::int_end

private

iterator past the last state in the constellation

Definition at line 815 of file liblts_bisim_gjkw.h.

int_inert_begin

B_to_C_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_inert_begin

private

iterator to the first inert transition of the block

If there are no inert transitions, then inert_begin and inert_end point to the end of the B_to_C-slice containing transitions from the block to its own constellation. If there is no such slice, both are equal to B_to_C.

Definition at line 426 of file liblts_bisim_gjkw.h.

int_inert_end

B_to_C_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_inert_end

private

iterator past the last inert transition of the block

Definition at line 429 of file liblts_bisim_gjkw.h.

int_marked_bottom_begin

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_marked_bottom_begin

private

iterator to the first marked bottom state of the block

Definition at line 419 of file liblts_bisim_gjkw.h.

int_marked_nonbottom_begin

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::block_t::int_marked_nonbottom_begin

private

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

Definition at line 413 of file liblts_bisim_gjkw.h.

int_seqnr

state_type mcrl2::lts::detail::bisim_gjkw::block_t::int_seqnr

private

unique sequence number of this block

After the stuttering equivalence algorithm has terminated, this number is used as a state number in the quotient Kripke structure. (For blocks that contain extra Kripke states, the number is set to BLOCK_NO_SEQNR).

Definition at line 456 of file liblts_bisim_gjkw.h.

int_slice_begin_or_before_end

succ_iter_t mcrl2::lts::detail::bisim_gjkw::succ_entry::int_slice_begin_or_before_end

private

points to the last or the first transition to the same constellation

We need to know, given a transition, which other transitions with the same source state and the same goal constellation there are. This pointer, in most cases, points to the last transition with the same source state and goal constellation, with the exception: If this succ_entry is actually the last transition, then the pointer points to the first such transition. In that way, one can find the first and the last relevant transition with one or two levels of dereferencing.

The advantage of this pointer is that one does not need to allocate a separate data structure containing this information.

Definition at line 1206 of file liblts_bisim_gjkw.h.

noninert_in_per_state

template<class LTS_TYPE >

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

private

Definition at line 1700 of file liblts_bisim_gjkw.h.

noninert_out_per_block

template<class LTS_TYPE >

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

private

Definition at line 1701 of file liblts_bisim_gjkw.h.

noninert_out_per_state

template<class LTS_TYPE >

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

private

Definition at line 1699 of file liblts_bisim_gjkw.h.

nontrivial_first

constln_t * mcrl2::lts::detail::bisim_gjkw::constln_t::nontrivial_first = nullptr

staticprivate

first constellation in the list of non-trivial constellations

Definition at line 828 of file liblts_bisim_gjkw.h.

nontrivial_next

constln_t* mcrl2::lts::detail::bisim_gjkw::constln_t::nontrivial_next

private

next constellation in the list of non-trivial constellations

If this is the last constellation in the list, nontrivial_next points to this very constellation. Consequently, it is possible to check whether some constellation is trivial without an additional variable.

Definition at line 825 of file liblts_bisim_gjkw.h.

notblue

state_type mcrl2::lts::detail::bisim_gjkw::state_info_entry::notblue

number of inert transitions to non-blue states

Definition at line 192 of file liblts_bisim_gjkw.h.

nr_of_blocks

state_type mcrl2::lts::detail::bisim_gjkw::block_t::nr_of_blocks = 0

static

total number of blocks with unique sequence number allocated

Upon starting the stuttering equivalence algorithm, the number of blocks must be zero.

Definition at line 464 of file liblts_bisim_gjkw.h.

nr_of_nonbottom_states

template<class LTS_TYPE >

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

private

Definition at line 1703 of file liblts_bisim_gjkw.h.

nr_of_states

template<class LTS_TYPE >

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

private

Definition at line 1659 of file liblts_bisim_gjkw.h.

nr_of_transitions

template<class LTS_TYPE >

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

private

Definition at line 1661 of file liblts_bisim_gjkw.h.

orig_nr_of_states

template<class LTS_TYPE >

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

private

Definition at line 1660 of file liblts_bisim_gjkw.h.

part_st

template<class LTS_TYPE >

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

private

Definition at line 1745 of file liblts_bisim_gjkw.h.

part_tr

template<class LTS_TYPE >

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

private

Definition at line 1746 of file liblts_bisim_gjkw.h.

perm_begin

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

staticprivate

Definition at line 799 of file liblts_bisim_gjkw.h.

permutation

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

permutation array

This is the central element of the data structure: In this array, states that belong to the same block are stored in adjacent elements, and blocks that belong to the same constellation are stored in adjacent slices.

Definition at line 1023 of file liblts_bisim_gjkw.h.

pos

permutation_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::pos

position of the state in the permutation array

Definition at line 189 of file liblts_bisim_gjkw.h.

postprocess_begin

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

In postprocess_new_bottom(), all transitions from a refined block to the present constellation have to be gone through. Because during this process the refined block may be refined even further, we need postprocess_begin and postprocess_end to store which transitions have to be gone through overall.

If no transitions to this constellation need to be postprocessed, the variable is set to the same value as postprocess_end, preferably to part_trans_t::B_to_C->end().

Definition at line 841 of file liblts_bisim_gjkw.h.

postprocess_end

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

Definition at line 845 of file liblts_bisim_gjkw.h.

pred [1/2]

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

Definition at line 1310 of file liblts_bisim_gjkw.h.

pred [2/2]

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

private

Definition at line 1440 of file liblts_bisim_gjkw.h.

refinable_first

block_t * mcrl2::lts::detail::bisim_gjkw::block_t::refinable_first = nullptr

staticprivate

first block in the list of refinable blocks

Definition at line 449 of file liblts_bisim_gjkw.h.

refinable_next

block_t* mcrl2::lts::detail::bisim_gjkw::block_t::refinable_next

private

next block in the list of refinable blocks

If this is the last block in the list, refinable_next points to this very block. Consequently, it is possible to check whether some block is refinable without an additional variable.

Definition at line 446 of file liblts_bisim_gjkw.h.

s_i_begin

state_info_const_ptr mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_begin

staticprivate

pointer at the first entry in the state_info array

Definition at line 352 of file liblts_bisim_gjkw.h.

s_i_end

state_info_const_ptr mcrl2::lts::detail::bisim_gjkw::state_info_entry::s_i_end

staticprivate

pointer past the last actual entry in the state_info array

state_info actually contains an additional entry that is only used partially, namely to store pointers to the end of the transition slices of the last state. In other words, s_i_end points at this additional, partially used entry.

Definition at line 359 of file liblts_bisim_gjkw.h.

second

template<class LTS_TYPE >

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

Definition at line 1669 of file liblts_bisim_gjkw.h.

sort_key

const state_type mcrl2::lts::detail::bisim_gjkw::constln_t::sort_key

sort key to order constellation-related information

When a constellation is created anew, it it assigned a sort key that is lower than the constellation it came from, but never lower than the sort key of any other constellation that was lower than the original constellation. This ensures that the order of other constellations does not change.

Definition at line 853 of file liblts_bisim_gjkw.h.

source

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

Definition at line 1285 of file liblts_bisim_gjkw.h.

state_in_begin

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_in_begin

private

iterator to first incoming transition

also serves as iterator past the last incoming transition of the previous state.

Definition at line 169 of file liblts_bisim_gjkw.h.

state_inert_in_begin

pred_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_in_begin

private

iterator to first inert incoming transition

Definition at line 177 of file liblts_bisim_gjkw.h.

state_inert_out_begin

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_out_begin

private

iterator to first inert outgoing transition

Definition at line 180 of file liblts_bisim_gjkw.h.

state_inert_out_end

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_inert_out_end

private

iterator past the last inert outgoing transition

Definition at line 183 of file liblts_bisim_gjkw.h.

state_info

fixed_vector<state_info_entry> mcrl2::lts::detail::bisim_gjkw::part_state_t::state_info

private

array with all other information about states

We allocate 1 additional `‘state’' to allow for the iterators past the last transition, as described in the documentation of state_info_entry.

Definition at line 1030 of file liblts_bisim_gjkw.h.

state_out_begin

succ_iter_t mcrl2::lts::detail::bisim_gjkw::state_info_entry::state_out_begin

private

iterator to first outgoing transition

also serves as iterator past the last outgoing transition of the previous state.

Definition at line 174 of file liblts_bisim_gjkw.h.

states_per_block

template<class LTS_TYPE >

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

private

Definition at line 1702 of file liblts_bisim_gjkw.h.

succ [1/2]

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

Definition at line 1284 of file liblts_bisim_gjkw.h.

succ [2/2]

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

private

Definition at line 1441 of file liblts_bisim_gjkw.h.

target

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

Definition at line 1191 of file liblts_bisim_gjkw.h.

to_constln

B_to_C_desc_list mcrl2::lts::detail::bisim_gjkw::block_t::to_constln

list of B_to_C with transitions from this block

This list serves two purposes: it contains all B_to_C_descriptors, so that the constellations reachable from this block can be found; and if this block has transitions to the current splitter SpC\SpB, then the first element of the list points to these transitions.

Definition at line 437 of file liblts_bisim_gjkw.h.

work_counter [1/4]

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

mutable

Definition at line 363 of file liblts_bisim_gjkw.h.

work_counter [2/4]

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

mutable

Definition at line 797 of file liblts_bisim_gjkw.h.

work_counter [3/4]

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

mutable

Definition at line 1302 of file liblts_bisim_gjkw.h.

work_counter [4/4]

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

mutable

Definition at line 1431 of file liblts_bisim_gjkw.h.

Friends

bisim_partitioner_gjkw_initialise_helper [1/2]

template<class LTS_TYPE >

friend class bisim_partitioner_gjkw_initialise_helper

friend

Definition at line 1033 of file liblts_bisim_gjkw.h.

bisim_partitioner_gjkw_initialise_helper [2/2]

template<class LTS_TYPE >

friend class bisim_partitioner_gjkw_initialise_helper

friend

Definition at line 1445 of file liblts_bisim_gjkw.h.

part_state_t [1/2]

friend class part_state_t

friend

Definition at line 361 of file liblts_bisim_gjkw.h.

part_state_t [2/2]

friend class part_state_t

friend

Definition at line 801 of file liblts_bisim_gjkw.h.