mcrl2::lts::detail::scc_partitioner< LTS_TYPE > Class Template Reference

This class contains an scc partitioner removing inert tau loops. More...

#include <liblts_scc.h>

Public Member Functions
	scc_partitioner (LTS_TYPE &l)
	Creates an scc partitioner for an LTS.
	~scc_partitioner ()=default
	Destroys this partitioner.
void	replace_transition_system (bool preserve_divergence_loops)
	The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
std::size_t	num_eq_classes () const
	Gives the number of bisimulation equivalence classes of the LTS.
std::size_t	get_eq_class (std::size_t s) const
	Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and excluding) num_eq_classes().
bool	in_same_class (std::size_t s, std::size_t t) const
	Returns whether two states are in the same bisimulation equivalence class.

Private Types
using	state_type = std::size_t
using	label_type = std::size_t

Private Member Functions
void	number_sccs ()

Private Attributes
LTS_TYPE &	aut
state_type	equivalence_class_index = 0
std::vector< std::size_t >	block_index_of_a_state

Detailed Description

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

This class contains an scc partitioner removing inert tau loops.

Definition at line 126 of file liblts_scc.h.

Member Typedef Documentation

label_type

template<class LTS_TYPE >

using mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::label_type = std::size_t

private

Definition at line 189 of file liblts_scc.h.

state_type

template<class LTS_TYPE >

using mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::state_type = std::size_t

private

Definition at line 188 of file liblts_scc.h.

Constructor & Destructor Documentation

scc_partitioner()

template<class LTS_TYPE >

mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::scc_partitioner

(

LTS_TYPE &

l

)

Creates an scc partitioner for an LTS.

This scc partitioner calculates a partition of the state space of the transition system l using a straightforward algorithm found in A.V. Aho, J.E. Hopcroft and J.D. Ullman, Data structures and algorithms. Addison Wesley, 1987 on page 224. All states that reside on a loop of internal actions are put in the same equivalence class. The function l.is_tau is used to determine whether an action is internal. Partitioning is done immediately when an instance of this class is created. When applying the function replace_transition_system the automaton l is replaced by (aka shrinked to) the automaton modulo the calculated partition.

Parameters

[in]

l

reference to an LTS.

Definition at line 210 of file liblts_scc.h.

~scc_partitioner()

template<class LTS_TYPE >

mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::~scc_partitioner ( )

default

Destroys this partitioner.

Member Function Documentation

get_eq_class()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::get_eq_class

(

std::size_t

s

)

const

Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and excluding) num_eq_classes().

Parameters

[in]

s

A state number.

Returns

The number of the equivalence class to which s belongs.

Definition at line 294 of file liblts_scc.h.

in_same_class()

template<class LTS_TYPE >

bool mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::in_same_class	(	std::size_t	s,
		std::size_t	t
	)		const

Returns whether two states are in the same bisimulation equivalence class.

Parameters

[in]	s	A state number.
[in]	t	A state number.

Return values

true	if s and t are in the same bisimulation equivalence class;
false	otherwise.

Definition at line 300 of file liblts_scc.h.

num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::num_eq_classes

Gives the number of bisimulation equivalence classes of the LTS.

Returns

The number of bisimulation equivalence classes of the LTS.

Definition at line 288 of file liblts_scc.h.

number_sccs()

template<class LTS_TYPE >

void mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::number_sccs

private

Definition at line 309 of file liblts_scc.h.

replace_transition_system()

template<class LTS_TYPE >

void mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::replace_transition_system

(

bool

preserve_divergence_loops

)

The lts for which this partioner is created is replaced by the lts modulo the calculated partition.

The number of states of the new lts becomes the number of equivalence classes. In each transition the start and end state are replaced by its equivalence class. If a transition has a tau label (which is checked using the function l.is_tau) then it is preserved if either from and to state are different, or preserve_divergence_loops is true. All non tau transitions are always preserved. The label numbers for preserved transitions are not changed.

Parameters

[in]

preserve_divergence_loops

If true preserve a tau loop on states that were part of a larger tau loop in the input transition system. Otherwise idle tau loops are removed.

Definition at line 225 of file liblts_scc.h.

Member Data Documentation

aut

template<class LTS_TYPE >

LTS_TYPE& mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::aut

private

Definition at line 191 of file liblts_scc.h.

block_index_of_a_state

template<class LTS_TYPE >

std::vector< std::size_t > mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::block_index_of_a_state

private

Definition at line 194 of file liblts_scc.h.

equivalence_class_index

template<class LTS_TYPE >

state_type mcrl2::lts::detail::scc_partitioner< LTS_TYPE >::equivalence_class_index = 0

private

Definition at line 193 of file liblts_scc.h.

---

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

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