#include <liblts_bisim.h>

Classes
struct	block

struct	non_bottom_state

Public Member Functions
	bisim_partitioner (LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false)
	Creates a bisimulation partitioner for an LTS.

	~bisim_partitioner ()=default
	Destroys this partitioner.

void	replace_transition_system (const bool branching, const bool preserve_divergences)
	Replaces the transition relation of the current lts by the transitions of the bisimulation reduced transition system.

std::size_t	num_eq_classes () const
	Gives the number of bisimulation equivalence classes of the LTS.

std::size_t	get_eq_class (const std::size_t s) const
	Gives the bisimulation equivalence class number of a state.

bool	in_same_class (const std::size_t s, const std::size_t t) const
	Returns whether two states are in the same bisimulation equivalence class.

mcrl2::state_formulas::state_formula	counter_formula (const std::size_t s, const std::size_t t)
	Creates a state formula that distinguishes state s from state t.

Private Types
typedef std::size_t	block_index_type

typedef std::size_t	state_type

typedef std::size_t	label_type

Private Member Functions
void	create_initial_partition (const bool branching, const bool preserve_divergences)

void	refine_partition_until_it_becomes_stable (const bool branching, const bool preserve_divergence)

void	refine_partion_with_respect_to_divergences (void)

void	split_the_blocks_in_BL (bool &partition_is_unstable, const label_type splitter_label, const block_index_type splitter_block)

void	order_recursively_on_tau_reachability (const state_type s, std::map< state_type, std::vector< state_type > > &inert_transition_map, std::vector< non_bottom_state > &new_non_bottom_states, std::set< state_type > &visited)

void	order_on_tau_reachability (std::vector< non_bottom_state > &non_bottom_states)

mcrl2::state_formulas::state_formula	conjunction (std::set< mcrl2::state_formulas::state_formula > terms) const
	conjunction Creates a conjunction of state formulas

regular_formulas::regular_formula	create_regular_formula (const mcrl2::lps::multi_action &a) const
	create_regular_formula Creates a regular formula that represents action a

regular_formulas::regular_formula	create_regular_formula (const mcrl2::lts::action_label_string &a) const
	create_regular_formula Creates a regular formula that represents action a

mcrl2::state_formulas::state_formula	until_formula (const mcrl2::state_formulas::state_formula &phi1, const label_type &a, const mcrl2::state_formulas::state_formula &phi2)
	until_formula Creates a state formula that corresponds to the until operator phi1phi2 from HMLU

mcrl2::state_formulas::state_formula	counter_formula_aux (const block_index_type B1, const block_index_type B2)

void	check_internal_consistency_of_the_partitioning_data_structure (const bool branching, const bool preserve_divergence) const

Private Attributes
state_type	max_state_index

LTS_TYPE &	aut

bool	branching

bool	store_counter_info

std::vector< block >	blocks

std::vector< state_type >	block_index_of_a_state

std::vector< bool >	block_flags

std::vector< bool >	block_is_in_to_be_processed

std::vector< bool >	state_flags

std::vector< block_index_type >	to_be_processed

std::vector< block_index_type >	BL

std::map< block_index_type, block_index_type >	right_child

std::map< block_index_type, label_type >	split_by_action

std::map< block_index_type, block_index_type >	split_by_block

std::map< block_index_type, std::set< block_index_type > >	r_alpha

std::map< block_index_type, std::set< block_index_type > >	r_tauP

outgoing_transitions_per_state_action_t	outgoing_transitions

int	fresh_var_counter = 0

Detailed Description

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

Definition at line 30 of file liblts_bisim.h.

Member Typedef Documentation

◆ block_index_type

template<class LTS_TYPE >

typedef std::size_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::block_index_type

private

Definition at line 200 of file liblts_bisim.h.

◆ label_type

template<class LTS_TYPE >

typedef std::size_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::label_type

private

Definition at line 202 of file liblts_bisim.h.

◆ state_type

template<class LTS_TYPE >

typedef std::size_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::state_type

private

Definition at line 201 of file liblts_bisim.h.

Constructor & Destructor Documentation

◆ bisim_partitioner()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::bisim_partitioner	(	LTS_TYPE &	l,
		const bool	branching = `false`,
		const bool	preserve_divergence = `false`,
		const bool	generate_counter_examples = `false`
	)

inline

Creates a bisimulation partitioner for an LTS.

This bisimulation partitioner applies the algorithm defined in J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M.S. Paterson, editor, Proceedings 17th ICALP, Warwick, volume 443 of Lecture Notes in Computer Science, pages 626-638. Springer-Verlag, 1990. The only difference is that this algorithm uses actions labels on transitions. Therefore, each list of non_inert_transitions is grouped such that all transitions with the same label are grouped together. Tau transitions (which have as label index the number of labels) occur at the beginning of this list.

If branching is true, then branching bisimulation is used, otherwise strong bisimulation is applied. If preserve_divergence is true, then branching must be true. In this case states with an internal tau loop are considered to be different from states without a tau loop. In this way the divergences are preserved.

The input transition system is not allowed to contain tau loops, except that if preserve_divergence is true tau loops on a single state are allowed as they indicate divergences. Using the scc partitioner the tau loops must first be removed before applying this algorithm.

Warning: Note that when compiled with optimisations, bisimulation partitioning is much faster than compiled without any optimisation. The difference can go up to a factor 10.

Parameters

[in] l Reference to the LTS. The LTS l is only changed if replace_transition_system is called.

Definition at line 53 of file liblts_bisim.h.

◆ ~bisim_partitioner()

template<class LTS_TYPE >

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

default

Destroys this partitioner.

Member Function Documentation

◆ check_internal_consistency_of_the_partitioning_data_structure()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::check_internal_consistency_of_the_partitioning_data_structure	(	const bool	branching,
		const bool	preserve_divergence
	)		const

inlineprivate

Definition at line 975 of file liblts_bisim.h.

◆ conjunction()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::conjunction ( std::set< mcrl2::state_formulas::state_formula > terms ) const

inlineprivate

conjunction Creates a conjunction of state formulas

Parameters

[in] terms The terms of the conjunction

Returns: The conjunctive state formula

Definition at line 833 of file liblts_bisim.h.

◆ counter_formula()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::counter_formula	(	const std::size_t	s,
		const std::size_t	t
	)

Creates a state formula that distinguishes state s from state t.

The states s and t are non bisimilar states. If they are bisimilar an exception is raised. A counter state formula phi is returned, which has the property that s |= phi and not t |= phi. Based on "Computing Distinguishing Formulas for Branching Bisimulation", 1991 by Henri Korver

Parameters

[in]	s	The state number for which the resulting formula should be true
[in]	t	The state number for which the resulting formula should be false

Returns: A distinguishing state formula.

Definition at line 1182 of file liblts_bisim.h.

◆ counter_formula_aux()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::counter_formula_aux	(	const block_index_type	B1,
		const block_index_type	B2
	)

inlineprivate

Definition at line 899 of file liblts_bisim.h.

◆ create_initial_partition()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::create_initial_partition	(	const bool	branching,
		const bool	preserve_divergences
	)

inlineprivate

Definition at line 288 of file liblts_bisim.h.

◆ create_regular_formula() [1/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::create_regular_formula ( const mcrl2::lps::multi_action & a ) const

inlineprivate

create_regular_formula Creates a regular formula that represents action a

In case the action comes from an LTS in the lts format.

Parameters

[in] a The action for which to create a regular formula

Returns: The created regular formula

Definition at line 846 of file liblts_bisim.h.

◆ create_regular_formula() [2/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::create_regular_formula ( const mcrl2::lts::action_label_string & a ) const

inlineprivate

create_regular_formula Creates a regular formula that represents action a

In case the action comes from an LTS in the aut or fsm format.

Parameters

[in] a The action for which to create a regular formula

Returns: The created regular formula

Definition at line 857 of file liblts_bisim.h.

◆ get_eq_class()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::get_eq_class ( const std::size_t s ) const

inline

Gives the bisimulation equivalence class number of a state.

Parameters

[in] s A state number.

Returns: The number of the bisimulation equivalence class to which s belongs.

Definition at line 170 of file liblts_bisim.h.

◆ in_same_class()

template<class LTS_TYPE >

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

inline

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 182 of file liblts_bisim.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::num_eq_classes ( ) const

inline

Gives the number of bisimulation equivalence classes of the LTS.

Returns: The number of bisimulation equivalence classes of the LTS.

Definition at line 161 of file liblts_bisim.h.

◆ order_on_tau_reachability()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::order_on_tau_reachability ( std::vector< non_bottom_state > & non_bottom_states )

inlineprivate

Definition at line 809 of file liblts_bisim.h.

◆ order_recursively_on_tau_reachability()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::order_recursively_on_tau_reachability	(	const state_type	s,
		std::map< state_type, std::vector< state_type > > &	inert_transition_map,
		std::vector< non_bottom_state > &	new_non_bottom_states,
		std::set< state_type > &	visited
	)

inlineprivate

Definition at line 786 of file liblts_bisim.h.

◆ refine_partion_with_respect_to_divergences()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::refine_partion_with_respect_to_divergences ( void )

private

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::refine_partition_until_it_becomes_stable	(	const bool	branching,
		const bool	preserve_divergence
	)

inlineprivate

Definition at line 412 of file liblts_bisim.h.

◆ replace_transition_system()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::replace_transition_system	(	const bool	branching,
		const bool	preserve_divergences
	)

inline

Replaces the transition relation of the current lts by the transitions of the bisimulation reduced transition system.

Each transition (s,l,s') is replaced by a transition (t,l,t') where t and t' are the equivalence classes to which classes of the LTS. If the label l is internal, which is detected using the function is_tau, then it is only returned if t!=t' or preserve_divergence=true. This effectively removes all inert transitions. Duplicates are removed from the transitions in the new lts. Also the number of states and the initial state are adapted by this method.

Precondition: The bisimulation equivalence classes have been computed.

Parameters

[in]	branching	Causes non internal transitions to be removed.
[in]	preserve_divergences	Preserves tau loops on states.

Definition at line 94 of file liblts_bisim.h.

◆ split_the_blocks_in_BL()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::split_the_blocks_in_BL	(	bool &	partition_is_unstable,
		const label_type	splitter_label,
		const block_index_type	splitter_block
	)

inlineprivate

Definition at line 500 of file liblts_bisim.h.

◆ until_formula()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::until_formula	(	const mcrl2::state_formulas::state_formula &	phi1,
		const label_type &	a,
		const mcrl2::state_formulas::state_formula &	phi2
	)

inlineprivate

until_formula Creates a state formula that corresponds to the until operator phi1phi2 from HMLU

This operator intuitively means: "phi1 holds while stuttering until we can do an a-step after which phi2 holds" In the operators of the mu-calculus that mCRL2 supports we can define this as: phi2 || (mu X.phi1 && (<tau>X || phi2)) if a = tau mu X.phi1 && (<tau>X || phi2) else

Parameters

[in]	phi1	The first state formula for the until operator
[in]	a	The action for the until operator
[in]	phi2	The second state formula for the until operator

Returns: A state formula that corresponds to the until operator phi1phi2 from HMLU

Definition at line 874 of file liblts_bisim.h.

Member Data Documentation

◆ aut

template<class LTS_TYPE >

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

private

Definition at line 205 of file liblts_bisim.h.

◆ BL

template<class LTS_TYPE >

std::vector< block_index_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::BL

private

Definition at line 267 of file liblts_bisim.h.

◆ block_flags

template<class LTS_TYPE >

std::vector< bool > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::block_flags

private

Definition at line 262 of file liblts_bisim.h.

◆ block_index_of_a_state

template<class LTS_TYPE >

std::vector< state_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::block_index_of_a_state

private

Definition at line 261 of file liblts_bisim.h.

◆ block_is_in_to_be_processed

template<class LTS_TYPE >

std::vector< bool > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::block_is_in_to_be_processed

private

Definition at line 263 of file liblts_bisim.h.

◆ blocks

template<class LTS_TYPE >

std::vector< block > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::blocks

private

Definition at line 257 of file liblts_bisim.h.

◆ branching

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::branching

private

Definition at line 206 of file liblts_bisim.h.

◆ fresh_var_counter

template<class LTS_TYPE >

int mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::fresh_var_counter = 0

private

Definition at line 285 of file liblts_bisim.h.

◆ max_state_index

template<class LTS_TYPE >

state_type mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::max_state_index

private

Definition at line 204 of file liblts_bisim.h.

◆ outgoing_transitions

template<class LTS_TYPE >

outgoing_transitions_per_state_action_t mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::outgoing_transitions

private

Definition at line 282 of file liblts_bisim.h.

◆ r_alpha

template<class LTS_TYPE >

std::map< block_index_type, std::set < block_index_type > > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::r_alpha

private

Definition at line 278 of file liblts_bisim.h.

◆ r_tauP

template<class LTS_TYPE >

std::map< block_index_type, std::set < block_index_type > > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::r_tauP

private

Definition at line 280 of file liblts_bisim.h.

◆ right_child

template<class LTS_TYPE >

std::map< block_index_type, block_index_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::right_child

private

Definition at line 272 of file liblts_bisim.h.

◆ split_by_action

template<class LTS_TYPE >

std::map< block_index_type, label_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::split_by_action

private

Definition at line 274 of file liblts_bisim.h.

◆ split_by_block

template<class LTS_TYPE >

std::map< block_index_type, block_index_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::split_by_block

private

Definition at line 276 of file liblts_bisim.h.

◆ state_flags

template<class LTS_TYPE >

std::vector< bool > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::state_flags

private

Definition at line 264 of file liblts_bisim.h.

◆ store_counter_info

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::store_counter_info

private

Definition at line 207 of file liblts_bisim.h.

◆ to_be_processed

template<class LTS_TYPE >

std::vector< block_index_type > mcrl2::lts::detail::bisim_partitioner< LTS_TYPE >::to_be_processed

private

Definition at line 266 of file liblts_bisim.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim.h

Classes

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ block_index_type

◆ label_type

◆ state_type

Constructor & Destructor Documentation

◆ bisim_partitioner()

◆ ~bisim_partitioner()

Member Function Documentation

◆ check_internal_consistency_of_the_partitioning_data_structure()

◆ conjunction()

◆ counter_formula()

◆ counter_formula_aux()

◆ create_initial_partition()

◆ create_regular_formula() [1/2]

◆ create_regular_formula() [2/2]

◆ get_eq_class()

◆ in_same_class()

◆ num_eq_classes()

◆ order_on_tau_reachability()

◆ order_recursively_on_tau_reachability()

◆ refine_partion_with_respect_to_divergences()

◆ refine_partition_until_it_becomes_stable()

◆ replace_transition_system()

◆ split_the_blocks_in_BL()

◆ until_formula()

Member Data Documentation

◆ aut

◆ BL

◆ block_flags

◆ block_index_of_a_state

◆ block_is_in_to_be_processed

◆ blocks

◆ branching

◆ fresh_var_counter

◆ max_state_index

◆ outgoing_transitions

◆ r_alpha

◆ r_tauP

◆ right_child

◆ split_by_action

◆ split_by_block

◆ state_flags

◆ store_counter_info

◆ to_be_processed