#include <liblts_branching_bisim_minimal_depth.h>

Classes
struct	block

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

mcrl2::state_formulas::state_formula	dist_formula_mindepth (size_t s, 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	level_type

typedef std::tuple< block_index_type, label_type, block_index_type >	branching_observation_type

typedef std::set< branching_observation_type >	signature_type

typedef std::pair< label_type, state_type >	observation

typedef std::pair< block_index_type, block_index_type >	blockpair_type

Private Member Functions
bool	is_tau (label_type l)

signature_type	get_signature (state_type s)

std::size_t	refine_partition ()

std::pair< block_index_type, block_index_type >	min_split_blockpair (block_index_type b1, block_index_type b2)

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

regular_formulas::regular_formula	make_tau_hat (regular_formulas::regular_formula &f)

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

void	split_and_intersect (std::set< block_index_type > &truths, std::pair< block_index_type, block_index_type > liftedB1B2)

bool	is_dist (std::set< blockpair_type > &dist_blockpairs, std::set< block_index_type > &to_dist)
	is_dist Checks if a given conjunction correctly exludes a set of blocks.

bool	is_dist (const std::set< blockpair_type > &dist_blockpairs, const std::set< block_index_type > &to_dist, std::set< block_index_type > &truths)
	is_dist overloaded to also maintain the truth values computed at the end.

std::vector< mcrl2::state_formulas::state_formula >	filtered_dist_conjunction (std::map< blockpair_type, mcrl2::state_formulas::state_formula > &Phi, std::set< block_index_type > &Tdist, std::set< block_index_type > &Truths)

mcrl2::state_formulas::state_formula	dist_formula (block_index_type block_index1, block_index_type block_index2)

Private Attributes
LTS_TYPE &	m_lts

state_type	initial_l2

state_type	max_state_index = 0

std::map< state_type, std::set< state_type > >	silent_in

std::map< state_type, std::set< state_type > >	silent_out

std::map< state_type, std::vector< observation > >	trans_out

std::map< state_type, std::size_t >	state2num_touched

std::map< state_type, block_index_type >	state2block

std::map< state_type, signature_type >	state2sig

std::vector< state_type >	bottom_states

std::map< level_type, std::set< block_index_type > >	level2blocksidx

std::map< std::pair< block_index_type, block_index_type >, mcrl2::state_formulas::state_formula >	blockpair2formula

std::map< std::pair< block_index_type, block_index_type >, std::set< block_index_type > >	blockpair2truths

std::vector< block >	blocks

Detailed Description

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

Definition at line 34 of file liblts_branching_bisim_minimal_depth.h.

Member Typedef Documentation

◆ block_index_type

template<class LTS_TYPE >

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

private

Definition at line 121 of file liblts_branching_bisim_minimal_depth.h.

◆ blockpair_type

template<class LTS_TYPE >

typedef std::pair<block_index_type, block_index_type> mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::blockpair_type

private

Definition at line 127 of file liblts_branching_bisim_minimal_depth.h.

◆ branching_observation_type

template<class LTS_TYPE >

typedef std::tuple<block_index_type, label_type, block_index_type> mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::branching_observation_type

private

Definition at line 124 of file liblts_branching_bisim_minimal_depth.h.

◆ level_type

template<class LTS_TYPE >

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

private

Definition at line 122 of file liblts_branching_bisim_minimal_depth.h.

◆ observation

template<class LTS_TYPE >

typedef std::pair<label_type, state_type> mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::observation

private

Definition at line 126 of file liblts_branching_bisim_minimal_depth.h.

◆ signature_type

template<class LTS_TYPE >

typedef std::set<branching_observation_type> mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::signature_type

private

Definition at line 125 of file liblts_branching_bisim_minimal_depth.h.

Constructor & Destructor Documentation

◆ branching_bisim_partitioner_minimal_depth()

template<class LTS_TYPE >

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

inline

Creates a branching bisimulation partitioner for an LTS.

This partitioner is specifically for creating minimal depth counter-examples for branching 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_branching_bisim_minimal_depth.h.

Member Function Documentation

◆ conjunction()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::conjunction ( std::vector< mcrl2::state_formulas::state_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 265 of file liblts_branching_bisim_minimal_depth.h.

◆ create_regular_formula() [1/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::branching_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 300 of file liblts_branching_bisim_minimal_depth.h.

◆ create_regular_formula() [2/2]

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::branching_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 lts format.

Parameters

a	The action for which to create a regular formula

Returns: The created regular formula

Definition at line 287 of file liblts_branching_bisim_minimal_depth.h.

◆ dist_formula()

template<class LTS_TYPE >

mcrl2::state_formulas::state_formula mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::dist_formula	(	block_index_type	block_index1,
		block_index_type	block_index2
	)

inlineprivate

Definition at line 401 of file liblts_branching_bisim_minimal_depth.h.

◆ dist_formula_mindepth()

template<class LTS_TYPE >

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

inline

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

The states s and t are non branching 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 "Minimal Depth Distinguishing Formulas without Until for Branching Bisimulation", 2024 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 106 of file liblts_branching_bisim_minimal_depth.h.

◆ filtered_dist_conjunction()

template<class LTS_TYPE >

std::vector< mcrl2::state_formulas::state_formula > mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::filtered_dist_conjunction	(	std::map< blockpair_type, mcrl2::state_formulas::state_formula > &	Phi,
		std::set< block_index_type > &	Tdist,
		std::set< block_index_type > &	Truths
	)

inlineprivate

Definition at line 373 of file liblts_branching_bisim_minimal_depth.h.

◆ get_signature()

template<class LTS_TYPE >

signature_type mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::get_signature ( state_type s )

inlineprivate

Definition at line 177 of file liblts_branching_bisim_minimal_depth.h.

◆ in_same_class()

template<class LTS_TYPE >

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

inline

Definition at line 114 of file liblts_branching_bisim_minimal_depth.h.

◆ is_dist() [1/2]

template<class LTS_TYPE >

bool mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::is_dist	(	const std::set< blockpair_type > &	dist_blockpairs,
		const std::set< block_index_type > &	to_dist,
		std::set< block_index_type > &	truths
	)

inlineprivate

is_dist overloaded to also maintain the truth values computed at the end.

Definition at line 350 of file liblts_branching_bisim_minimal_depth.h.

◆ is_dist() [2/2]

template<class LTS_TYPE >

bool mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::is_dist	(	std::set< blockpair_type > &	dist_blockpairs,
		std::set< block_index_type > &	to_dist
	)

inlineprivate

is_dist Checks if a given conjunction correctly exludes a set of blocks.

Parameters

dist_blockpairs	The blockpairs that were used to generate the conjuncts.
to_dist	The set of blocks that should be excluded by the conjunction, forall b\in to_dist. b\not\in\sem{phi_dist_blockpairs}.

Returns: True if the conjunction correctly excludes the set of blocks, false otherwise.

Definition at line 335 of file liblts_branching_bisim_minimal_depth.h.

◆ is_tau()

template<class LTS_TYPE >

bool mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::is_tau ( label_type l )

inlineprivate

Definition at line 172 of file liblts_branching_bisim_minimal_depth.h.

◆ make_tau_hat()

template<class LTS_TYPE >

regular_formulas::regular_formula mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::make_tau_hat ( regular_formulas::regular_formula & f )

inlineprivate

Definition at line 275 of file liblts_branching_bisim_minimal_depth.h.

◆ min_split_blockpair()

template<class LTS_TYPE >

std::pair< block_index_type, block_index_type > mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::min_split_blockpair	(	block_index_type	b1,
		block_index_type	b2
	)

inlineprivate

Definition at line 249 of file liblts_branching_bisim_minimal_depth.h.

◆ refine_partition()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::refine_partition ( )

inlineprivate

Definition at line 199 of file liblts_branching_bisim_minimal_depth.h.

◆ split_and_intersect()

template<class LTS_TYPE >

void mcrl2::lts::detail::branching_bisim_partitioner_minimal_depth< LTS_TYPE >::split_and_intersect	(	std::set< block_index_type > &	truths,
		std::pair< block_index_type, block_index_type >	liftedB1B2
	)