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)

Friends
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:

Public Member Functions