No Matches
mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE > Class Template Reference

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

#include <liblts_bisim_gjkw.h>

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_trefine (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_tpostprocess_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: