mcrl2::lts::detail::bisim_dnj::part_state_t Class Reference

refinable partition data structure More...

#include <liblts_bisim_dnj.h>

Public Member Functions
	part_state_t (state_type const num_states)
	constructor
	~part_state_t ()
	destructor
state_type	state_size () const
	calculate the size of the state space
const block_t *	block (state_type const s) const
	find the block of a state
template<class LTS_TYPE >
void	print_part (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	print the partition per block
template<class LTS_TYPE >
void	assert_consistency (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	asserts that the partition of states is consistent

Public Attributes
permutation_t	permutation
	permutation array
fixed_vector< state_info_entry >	state_info
	array with all other information about states
state_type	nr_of_blocks
	total number of blocks with unique sequence number allocated

Private Member Functions
template<class LTS_TYPE >
void	print_block (const block_t *const B, const char *const message, const permutation_entry *begin_print, const permutation_entry *const end_print, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
	print a slice of the partition (typically a block)

Detailed Description

refinable partition data structure

This class collects all information about a partition of the states.

Definition at line 522 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

part_state_t()

mcrl2::lts::detail::bisim_dnj::part_state_t::part_state_t ( state_type const  num_states )

inline

constructor

The constructor allocates memory and makes the permutation and state_info arrays consistent with each other, but does not actually initialise the partition. Immediately afterwards, the initialisation will be done in bisim_partitioner_dnj::create_initial_partition().

Parameters

num_states

number of states in the LTS

Definition at line 545 of file liblts_bisim_dnj.h.

~part_state_t()

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

inline

destructor

The destructor also deallocates the blocks, as they are not directly referenced from anywhere. This is only necessary if we do not use the pool allocator, as the latter will destroy the blocks wholesale.

Definition at line 570 of file liblts_bisim_dnj.h.

Member Function Documentation

assert_consistency()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_dnj::part_state_t::assert_consistency ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner ) const

inline

asserts that the partition of states is consistent

It also requires that no states are marked.

Parameters

partitioner

LTS partitioner (used to print more details)

Definition at line 665 of file liblts_bisim_dnj.h.

block()

const block_t * mcrl2::lts::detail::bisim_dnj::part_state_t::block ( state_type const  s ) const

inline

find the block of a state

Parameters

s	number of the state

Returns

a pointer to the block where state s resides in

Definition at line 592 of file liblts_bisim_dnj.h.

print_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_dnj::part_state_t::print_block ( const block_t *const  B, const char *const  message, const permutation_entry *  begin_print, const permutation_entry *const  end_print, const bisim_partitioner_dnj< LTS_TYPE > &  partitioner  ) const

inlineprivate

print a slice of the partition (typically a block)

If the slice indicated by the parameters is not empty, the message and the states in this slice will be printed.

Parameters

message	text printed as a title if the slice is not empty
begin_print	iterator to the beginning of the slice
end_print	iterator past the end of the slice
partitioner	LTS partitioner (used to print more details)

Definition at line 606 of file liblts_bisim_dnj.h.

print_part()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_dnj::part_state_t::print_part ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner ) const

inline

print the partition per block

The function prints all blocks in order. For each block, it lists its states, separated into nonbottom and bottom states.

Parameters

partitioner

LTS partitioner (used to print more details)

Definition at line 641 of file liblts_bisim_dnj.h.

state_size()

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

inline

calculate the size of the state space

Returns

the number of states in the LTS

Definition at line 586 of file liblts_bisim_dnj.h.

Member Data Documentation

nr_of_blocks

state_type mcrl2::lts::detail::bisim_dnj::part_state_t::nr_of_blocks

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 537 of file liblts_bisim_dnj.h.

permutation

permutation_t mcrl2::lts::detail::bisim_dnj::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.

Definition at line 529 of file liblts_bisim_dnj.h.

state_info

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

array with all other information about states

Definition at line 532 of file liblts_bisim_dnj.h.

---

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

• lts/include/mcrl2/lts/detail/liblts_bisim_dnj.h