No Matches
mcrl2::lts::detail::bisim_gjkw::part_trans_t Class Reference

#include <liblts_bisim_gjkw.h>

Public Member Functions

 part_trans_t (trans_type m)
 ~part_trans_t ()
void clear ()
 clear allocated memory
trans_type trans_size () const
void split_inert_to_C (block_t *B)
 handle the transitions from the splitter to its own constellation
succ_iter_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 split_s_inert_out (state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
 Split outgoing transitions of a state in the splitter.
void make_noninert (succ_iter_t const succ_iter)
void new_blue_block_created (block_t *OldB, block_t *NewB)
 handle B_to_C slices after a new blue block has been created
void 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 B_to_C_begin () const
B_to_C_iter_t B_to_C_end ()
pred_const_iter_t pred_end () const
succ_const_iter_t succ_end () const
void assert_stability (const part_state_t &part_st) const
 assert that the data structure is consistent and stable

Private Member Functions

void swap_in (B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
void swap_out (pred_iter_t const pos1, pred_iter_t const pos2)
void swap_B_to_C (succ_iter_t const pos1, succ_iter_t const pos2)
void swap3_B_to_C (succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)

Private Attributes

fixed_vector< pred_entrypred
fixed_vector< succ_entrysucc
fixed_vector< B_to_C_entryB_to_C


template<class LTS_TYPE >
class bisim_partitioner_gjkw_initialise_helper

Detailed Description

Definition at line 1437 of file liblts_bisim_gjkw.h.

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