#include <liblts_pbisim_bem.h>

Classes
struct	block_type

struct	distribution_type

struct	step_class_type

struct	tree_type

Public Member Functions
	prob_bisim_partitioner_bem (LTS_TYPE &l, utilities::execution_timer &timer)
	Creates a probabilistic bisimulation partitioner for an PLTS.

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.

std::size_t	get_eq_step_class (const std::size_t d) const
	Gives the bisimulation equivalence step class number of a probabilistic state.

void	replace_transitions ()
	Replaces the transition relation of the current lts by the transitions of the bisimulation reduced transition system.

void	replace_probabilistic_states ()
	Replaces the probabilistic states of the current lts by the probabilistic states of the bisimulation reduced transition system.

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

Private Types
using	block_key_type = std::size_t

using	step_class_key_type = std::size_t

using	state_type = std::size_t

using	label_type = std::size_t

using	distribution_key_type = std::size_t

using	probability_fraction_type = typename LTS_TYPE::probabilistic_state_t::probability_t

Private Member Functions
void	create_initial_partition ()
	Creates the initial partition of step classes and blocks. \detail The blocks are initially partitioned based on the actions that can perform. The step classes are partitioned based on the action that leads to the probabilistic state.

probability_fraction_type	probability_to_block (distribution_type &d, block_type &b)
	Calculates the probability to reach block b from distribution d.

LTS_TYPE::probabilistic_state_t	calculate_new_probabilistic_state (typename LTS_TYPE::probabilistic_state_t ps)

LTS_TYPE::probabilistic_state_t	calculate_equivalent_probabilistic_state (step_class_type &sc)

void	refine_partition_until_it_becomes_stable ()
	Two-phased partitioning algorithm described in page 204. Fig 9. Baier. \detail Refinement of state partition and step partition until no new blocks/step classes are in front of the partition lists.

void	postprocessing_stage ()

Private Attributes
std::list< block_type * >	state_partition

std::list< step_class_type * >	step_partition

std::vector< distribution_type >	distributions

std::deque< step_class_type >	step_classes

std::deque< step_class_type >	equivalent_step_classes

std::deque< block_type >	blocks

std::vector< block_key_type >	block_index_of_a_state

std::vector< step_class_key_type >	step_class_index_of_a_distribution

LTS_TYPE &	aut

Detailed Description

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

Definition at line 21 of file liblts_pbisim_bem.h.

Member Typedef Documentation

◆ block_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::block_key_type = std::size_t

private

Definition at line 135 of file liblts_pbisim_bem.h.

◆ distribution_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::distribution_key_type = std::size_t

private

Definition at line 139 of file liblts_pbisim_bem.h.

◆ label_type

template<class LTS_TYPE >

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

private

Definition at line 138 of file liblts_pbisim_bem.h.

◆ probability_fraction_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::probability_fraction_type = typename LTS_TYPE::probabilistic_state_t::probability_t

private

Definition at line 140 of file liblts_pbisim_bem.h.

◆ state_type

template<class LTS_TYPE >

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

private

Definition at line 137 of file liblts_pbisim_bem.h.

◆ step_class_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::step_class_key_type = std::size_t

private

Definition at line 136 of file liblts_pbisim_bem.h.

Constructor & Destructor Documentation

◆ prob_bisim_partitioner_bem()

template<class LTS_TYPE >

mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::prob_bisim_partitioner_bem	(	LTS_TYPE &	l,
		utilities::execution_timer &	timer
	)

inline

Creates a probabilistic bisimulation partitioner for an PLTS.

This bisimulation partitioner applies the algorithm defined in C. Baier, B. Engelen and M. Majster-Cederbaum. Deciding Bisimilarity and Similarity for Probabilistic Processes. In Journal of Computer and System Sciences 60, 187-237 (2000)

Definition at line 29 of file liblts_pbisim_bem.h.

Member Function Documentation

◆ calculate_equivalent_probabilistic_state()

template<class LTS_TYPE >

LTS_TYPE::probabilistic_state_t mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::calculate_equivalent_probabilistic_state ( step_class_type & sc )

inlineprivate

Definition at line 464 of file liblts_pbisim_bem.h.

◆ calculate_new_probabilistic_state()

template<class LTS_TYPE >

LTS_TYPE::probabilistic_state_t mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::calculate_new_probabilistic_state ( typename LTS_TYPE::probabilistic_state_t ps )

inlineprivate

Definition at line 414 of file liblts_pbisim_bem.h.

◆ create_initial_partition()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::create_initial_partition ( )

inlineprivate

Creates the initial partition of step classes and blocks. \detail The blocks are initially partitioned based on the actions that can perform. The step classes are partitioned based on the action that leads to the probabilistic state.

Definition at line 193 of file liblts_pbisim_bem.h.

◆ get_eq_class()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::prob_bisim_partitioner_bem< 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 52 of file liblts_pbisim_bem.h.

◆ get_eq_step_class()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::get_eq_step_class ( const std::size_t d ) const

inline

Gives the bisimulation equivalence step class number of a probabilistic state.

Parameters

[in] s A probabilistic state number.

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

Definition at line 61 of file liblts_pbisim_bem.h.

◆ in_same_probabilistic_class()

template<class LTS_TYPE >

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

inline

Returns whether two states are in the same probabilistic 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 128 of file liblts_pbisim_bem.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::prob_bisim_partitioner_bem< 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 44 of file liblts_pbisim_bem.h.

◆ postprocessing_stage()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::postprocessing_stage ( )

inlineprivate

Definition at line 714 of file liblts_pbisim_bem.h.

◆ probability_to_block()

template<class LTS_TYPE >

probability_fraction_type mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::probability_to_block	(	distribution_type &	d,
		block_type &	b
	)

inlineprivate

Calculates the probability to reach block b from distribution d.

Parameters

[in] d is a probabilistic state (distribution). b is a block of states.

Returns: The probability to reach block b.

Definition at line 385 of file liblts_pbisim_bem.h.

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::refine_partition_until_it_becomes_stable ( )

inlineprivate

Two-phased partitioning algorithm described in page 204. Fig 9. Baier. \detail Refinement of state partition and step partition until no new blocks/step classes are in front of the partition lists.

Definition at line 482 of file liblts_pbisim_bem.h.

◆ replace_probabilistic_states()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::replace_probabilistic_states ( )

inline

Replaces the probabilistic states of the current lts by the probabilistic states of the bisimulation reduced transition system.

Precondition: The bisimulation step classes have been computed.

Definition at line 98 of file liblts_pbisim_bem.h.

◆ replace_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::replace_transitions ( )

inline

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

Precondition: The bisimulation equivalence classes have been computed.

Definition at line 72 of file liblts_pbisim_bem.h.

Member Data Documentation

◆ aut

template<class LTS_TYPE >

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

private

Definition at line 173 of file liblts_pbisim_bem.h.

◆ block_index_of_a_state

template<class LTS_TYPE >

std::vector<block_key_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::block_index_of_a_state

private

Definition at line 170 of file liblts_pbisim_bem.h.

◆ blocks

template<class LTS_TYPE >

std::deque<block_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::blocks

private

Definition at line 169 of file liblts_pbisim_bem.h.

◆ distributions

template<class LTS_TYPE >

std::vector<distribution_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::distributions

private

Definition at line 166 of file liblts_pbisim_bem.h.

◆ equivalent_step_classes

template<class LTS_TYPE >

std::deque<step_class_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::equivalent_step_classes

private

Definition at line 168 of file liblts_pbisim_bem.h.

◆ state_partition

template<class LTS_TYPE >

std::list<block_type*> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::state_partition

private

Definition at line 164 of file liblts_pbisim_bem.h.

◆ step_class_index_of_a_distribution

template<class LTS_TYPE >

std::vector<step_class_key_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::step_class_index_of_a_distribution

private

Definition at line 171 of file liblts_pbisim_bem.h.

◆ step_classes

template<class LTS_TYPE >

std::deque<step_class_type> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::step_classes

private

Definition at line 167 of file liblts_pbisim_bem.h.

◆ step_partition

template<class LTS_TYPE >

std::list<step_class_type*> mcrl2::lts::detail::prob_bisim_partitioner_bem< LTS_TYPE >::step_partition

private

Definition at line 165 of file liblts_pbisim_bem.h.

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

lts/include/mcrl2/lts/detail/liblts_pbisim_bem.h

Classes

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ block_key_type

◆ distribution_key_type

◆ label_type

◆ probability_fraction_type

◆ state_type

◆ step_class_key_type

Constructor & Destructor Documentation

◆ prob_bisim_partitioner_bem()

Member Function Documentation

◆ calculate_equivalent_probabilistic_state()

◆ calculate_new_probabilistic_state()

◆ create_initial_partition()

◆ get_eq_class()

◆ get_eq_step_class()

◆ in_same_probabilistic_class()

◆ num_eq_classes()

◆ postprocessing_stage()

◆ probability_to_block()

◆ refine_partition_until_it_becomes_stable()

◆ replace_probabilistic_states()

◆ replace_transitions()

Member Data Documentation

◆ aut

◆ block_index_of_a_state

◆ blocks

◆ distributions

◆ equivalent_step_classes

◆ state_partition

◆ step_class_index_of_a_distribution

◆ step_classes

◆ step_partition