#include <liblts_bisim_minimal_depth.h>

Classes
struct	block

struct	formula

Public Member Functions
	bisim_partitioner_minimal_depth (LTS_TYPE &l, const std::size_t init_l2)
	Creates a bisimulation partitioner for an LTS.

	~bisim_partitioner_minimal_depth ()=default
	Destroys this partitioner.

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

bool	in_same_class (const std::size_t s, const std::size_t t)

Private Types
typedef std::size_t	block_index_type

typedef std::size_t	state_type

typedef std::size_t	level_type

typedef std::size_t	formula_index_type

typedef std::size_t	label_type

typedef std::pair< label_type, block_index_type >	observation_t

typedef std::set< observation_t >	derivatives_t

Private Member Functions
void	save_transitions ()

void	set_truths (formula &f)
	Compute and set the truth values of a formula f.

bool	refine_partition (level_type lvl)

void	split_BL (level_type lvl)
	Performs the splits based on the blocks in Bsplit and the flags set in state_flags.

label_type	label (observation_t obs)

block_index_type	target (observation_t obs)

formula	distinguish (const block_index_type b1, const block_index_type b2)
	Creates a formula that distinguishes a block b1 from the block b2.

level_type	gca_level (const block_index_type B1, const block_index_type B2)
	Auxiliarry function that computes the level of the greatest common ancestor. In other words a lvl i such that B1 and B2 are i-bisimilar.

block_index_type	lift_block (const block_index_type B1, level_type goal)

mcrl2::state_formulas::state_formula	convert_formula (formula &f)

mcrl2::state_formulas::state_formula	conjunction (std::vector< formula > &conjunctions)
	conjunction Creates a conjunction of state formulas

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

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

Private Attributes
state_type	initial_l2

state_type	max_state_index

LTS_TYPE &	aut

std::set< block_index_type >	partition

std::vector< block >	blocks

std::vector< state_type >	block_index_of_a_state

std::vector< bool >	block_flags

std::vector< bool >	state_flags

std::vector< block_index_type >	to_be_processed

std::vector< block_index_type >	BL

std::map< std::pair< block_index_type, block_index_type >, level_type >	greatest_common_ancestor

Detailed Description

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

Definition at line 34 of file liblts_bisim_minimal_depth.h.

Member Typedef Documentation

◆ block_index_type

template<class LTS_TYPE >

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

private

Definition at line 130 of file liblts_bisim_minimal_depth.h.

◆ derivatives_t

template<class LTS_TYPE >

typedef std::set<observation_t> mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::derivatives_t

private

Definition at line 192 of file liblts_bisim_minimal_depth.h.

◆ formula_index_type

template<class LTS_TYPE >

typedef std::size_t mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::formula_index_type

private

Definition at line 133 of file liblts_bisim_minimal_depth.h.

◆ label_type

template<class LTS_TYPE >

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

private

Definition at line 134 of file liblts_bisim_minimal_depth.h.

◆ level_type

template<class LTS_TYPE >

typedef std::size_t mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::level_type

private

Definition at line 132 of file liblts_bisim_minimal_depth.h.

◆ observation_t

template<class LTS_TYPE >

typedef std::pair<label_type, block_index_type> mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::observation_t

private

Definition at line 191 of file liblts_bisim_minimal_depth.h.

◆ state_type

template<class LTS_TYPE >

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

private

Definition at line 131 of file liblts_bisim_minimal_depth.h.

Constructor & Destructor Documentation

◆ bisim_partitioner_minimal_depth()

template<class LTS_TYPE >

mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::bisim_partitioner_minimal_depth	(	LTS_TYPE &	l,
		const std::size_t	init_l2
	)

inline

Creates a bisimulation partitioner for an LTS.

This partitioner is specifically for creating minimal depth counter-examples for strong bisimulation. It guarantees stability w.r.t. the old partition before considering new splitter blocks. This might cause this implementation to be less efficient than other partitioners.

Parameters

l	Reference to the LTS.
init_l2	reference to the initial state of lts2.

Definition at line 44 of file liblts_bisim_minimal_depth.h.

◆ ~bisim_partitioner_minimal_depth()

template<class LTS_TYPE >

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

default

Destroys this partitioner.

Member Function Documentation

◆ conjunction()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::conjunction ( std::vector< formula > & conjunctions )

inlineprivate

conjunction Creates a conjunction of state formulas

Parameters

terms The terms of the conjunction

Returns: The conjunctive state formula

Definition at line 591 of file liblts_bisim_minimal_depth.h.

◆ convert_formula()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::convert_formula ( formula & f )

inlineprivate

Definition at line 574 of file liblts_bisim_minimal_depth.h.

◆ create_regular_formula() [1/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::bisim_partitioner_minimal_depth< 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

a	The action for which to create a regular formula

Returns: The created regular formula

Definition at line 624 of file liblts_bisim_minimal_depth.h.

◆ create_regular_formula() [2/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::bisim_partitioner_minimal_depth< 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

a	The action for which to create a regular formula

Returns: The created regular formula

Definition at line 612 of file liblts_bisim_minimal_depth.h.

◆ dist_formula_mindepth()

template<class LTS_TYPE >

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

inline

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

The states s and t are non bisimilar states. A distinguishign state formula phi is returned, which has the property that s \in \sem{phi} and t \not\in\sem{phi}. Based on the preprint "Computing minimal distinguishing Hennessey-Milner formulas is NP-hard. But variants are tractable", 2023 by Jan Martens and Jan Friso Groote

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 minimal observation depth distinguishing state formula, that is often also minimum negation-depth and irreducible.

Definition at line 116 of file liblts_bisim_minimal_depth.h.

◆ distinguish()

template<class LTS_TYPE >

formula mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::distinguish	(	const block_index_type	b1,
		const block_index_type	b2
	)

inlineprivate

Creates a formula that distinguishes a block b1 from the block b2.

creates a minimal depth formula that distinguishes b1 and b2.

Returns: A minimal observation depth distinguishing state formula, that is often also minimum negation-depth and irreducible.

Definition at line 441 of file liblts_bisim_minimal_depth.h.

◆ gca_level()

template<class LTS_TYPE >

level_type mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::gca_level	(	const block_index_type	B1,
		const block_index_type	B2
	)

inlineprivate

Auxiliarry function that computes the level of the greatest common ancestor. In other words a lvl i such that B1 and B2 are i-bisimilar.

Definition at line 518 of file liblts_bisim_minimal_depth.h.

◆ in_same_class()

template<class LTS_TYPE >

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

inline

Definition at line 123 of file liblts_bisim_minimal_depth.h.

◆ label()

template<class LTS_TYPE >

label_type mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::label ( observation_t obs )

inlineprivate

Definition at line 433 of file liblts_bisim_minimal_depth.h.

◆ lift_block()

template<class LTS_TYPE >

block_index_type mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::lift_block	(	const block_index_type	B1,
		level_type	goal
	)

inlineprivate

Definition at line 559 of file liblts_bisim_minimal_depth.h.

◆ refine_partition()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::refine_partition ( level_type lvl )

inlineprivate

Definition at line 256 of file liblts_bisim_minimal_depth.h.

◆ save_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::save_transitions ( )

inlineprivate

Definition at line 196 of file liblts_bisim_minimal_depth.h.

◆ set_truths()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::set_truths ( formula & f )

inlineprivate

Compute and set the truth values of a formula f.

Given the formula f we compute the subset of blocks in which f is true. the truthvalues are computed based on the truth values of the different conjuncts and the modality which consists of the label and being negated or not.

Definition at line 211 of file liblts_bisim_minimal_depth.h.