#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
using	block_index_type = std::size_t

using	state_type = std::size_t

using	level_type = std::size_t

using	formula_index_type = std::size_t

using	label_type = std::size_t

using	observation_t = std::pair< label_type, block_index_type >

using	derivatives_t = std::set< observation_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 = 0

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 30 of file liblts_bisim_minimal_depth.h.

Member Typedef Documentation

◆ block_index_type

template<class LTS_TYPE >

using mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::block_index_type = std::size_t

private

Definition at line 125 of file liblts_bisim_minimal_depth.h.

◆ derivatives_t

template<class LTS_TYPE >

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

private

Definition at line 187 of file liblts_bisim_minimal_depth.h.

◆ formula_index_type

template<class LTS_TYPE >

using mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::formula_index_type = std::size_t

private

Definition at line 128 of file liblts_bisim_minimal_depth.h.

◆ label_type

template<class LTS_TYPE >

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

private

Definition at line 129 of file liblts_bisim_minimal_depth.h.

◆ level_type

template<class LTS_TYPE >

using mcrl2::lts::detail::bisim_partitioner_minimal_depth< LTS_TYPE >::level_type = std::size_t

private

Definition at line 127 of file liblts_bisim_minimal_depth.h.

◆ observation_t

template<class LTS_TYPE >

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

private

Definition at line 186 of file liblts_bisim_minimal_depth.h.

◆ state_type

template<class LTS_TYPE >

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

private

Definition at line 126 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 40 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 585 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 568 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 618 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 606 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 \llbracket\phi\rrbracket$ and $t \notin \llbracket\phi\rrbracket$ . 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 111 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 432 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 509 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 118 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 424 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 553 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 251 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 191 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 206 of file liblts_bisim_minimal_depth.h.