implements the main algorithm for the stutter equivalence quotient More...

Public Member Functions
	bisim_partitioner_gjkw (LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)

	~bisim_partitioner_gjkw ()

void	replace_transition_system (bool branching, bool preserve_divergence)

state_type	get_eq_class (state_type s) const

bool	in_same_class (state_type s, state_type t) const

Static Public Member Functions
static state_type	num_eq_classes ()

Private Member Functions
void	create_initial_partition_gjkw (bool branching, bool preserve_divergence)

void	refine_partition_until_it_becomes_stable_gjkw ()

bisim_gjkw::block_t *	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 *	postprocess_new_bottom (bisim_gjkw::block_t *RedB)
	Split a block with new bottom states as needed.

Private Attributes
bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >	init_helper

bisim_gjkw::part_state_t	part_st

bisim_gjkw::part_trans_t	part_tr

Detailed Description

template<class LTS_TYPE>
class mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >

implements the main algorithm for the stutter equivalence quotient

Definition at line 1741 of file liblts_bisim_gjkw.h.

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

Public Member Functions