#include <liblts_pbisim_grv.h>

Classes
struct	action_block_type

struct	action_constellation_type

struct	action_mark_type

struct	action_state_type

struct	action_transition_type

struct	probabilistic_block_type

struct	probabilistic_constellation_type

struct	probabilistic_mark_type

struct	probabilistic_state_type

struct	probabilistic_transition_type

class	transitions_per_label_t

Public Member Functions
	prob_bisim_partitioner_grv (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)
	Gives the bisimulation equivalence class number of a state.

std::size_t	get_eq_probabilistic_class (const std::size_t s)
	Gives the bisimulation equivalence probabilistic 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_grv (const std::size_t s, const std::size_t t)
	Returns whether two states are in the same probabilistic bisimulation equivalence class.

Protected Types
using	block_key_type = std::size_t

using	constellation_key_type = std::size_t

using	transition_key_type = std::size_t

using	state_key_type = std::size_t

using	label_type = std::size_t

using	probability_label_type = typename LTS_TYPE::probabilistic_state_t::probability_t

using	probability_fraction_type = typename LTS_TYPE::probabilistic_state_t::probability_t

Protected Member Functions
bool	check_data_structure ()

void	print_structure (const std::string &info)

void	create_initial_partition ()

void	preprocessing_stage ()

void	refine_initial_action_block (const std::vector< embedded_list< action_transition_type > > &transitions_per_label)

template<typename LIST_ELEMENT >
void	move_list_element_back (LIST_ELEMENT &s, embedded_list< LIST_ELEMENT > &source_list, embedded_list< LIST_ELEMENT > &dest_list)

template<typename LIST_ELEMENT >
void	move_list_element_front (LIST_ELEMENT &s, embedded_list< LIST_ELEMENT > &source_list, embedded_list< LIST_ELEMENT > &dest_list)
	Move an element of a list to the front of another the list.

void	refine_partition_until_it_becomes_stable ()
	Refine partition until it becomes stable.

void	split_probabilistic_block (probabilistic_block_type &block_to_split, embedded_list< probabilistic_state_type > &states_of_new_block)
	Split a probabilistic block.

void	split_action_block (action_block_type &block_to_split, embedded_list< action_state_type > &states_of_new_block)
	Split an action block.

void	mark_probabilistic (const action_block_type &Bc, std::deque< probabilistic_mark_type > &marked_probabilistic_blocks)
	Gives the probabilistic blocks that are marked by block Bc.

void	mark_action (std::deque< action_mark_type > &marked_action_blocks, const label_type &a, typename embedded_list< action_transition_type >::iterator &action_walker_begin, const typename embedded_list< action_transition_type >::iterator action_walker_end)
	Gives the action blocks that are marked by probabilistic block Bc.

action_block_type *	choose_action_splitter (action_constellation_type *non_trivial_action_const)
	Choose an splitter block from a non trivial constellation.

probabilistic_block_type *	choose_probabilistic_splitter (probabilistic_constellation_type *non_trivial_probabilistic_const)
	Choose an splitter block from a non trivial constellation.

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 (probabilistic_block_type &pb)

Protected Attributes
std::vector< action_transition_type >	action_transitions

std::deque< probabilistic_transition_type >	probabilistic_transitions

std::vector< action_state_type >	action_states

std::vector< probabilistic_state_type >	probabilistic_states

std::deque< action_block_type >	action_blocks

std::deque< probabilistic_block_type >	probabilistic_blocks

std::deque< action_constellation_type >	action_constellations

std::deque< probabilistic_constellation_type >	probabilistic_constellations

std::deque< std::size_t >	state_to_constellation_count

std::stack< action_constellation_type * >	non_trivial_action_constellations

std::stack< probabilistic_constellation_type * >	non_trivial_probabilistic_constellations

std::deque< action_mark_type >	marked_action_blocks

std::deque< probabilistic_mark_type >	marked_probabilistic_blocks

std::vector< std::pair< probability_label_type, probabilistic_state_type * > >	grouped_states_per_probability_in_block

transitions_per_label_t	transitions_per_label

LTS_TYPE &	aut

Detailed Description

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

Definition at line 22 of file liblts_pbisim_grv.h.

Member Typedef Documentation

◆ block_key_type

template<class LTS_TYPE >

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

protected

Definition at line 139 of file liblts_pbisim_grv.h.

◆ constellation_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::constellation_key_type = std::size_t

protected

Definition at line 140 of file liblts_pbisim_grv.h.

◆ label_type

template<class LTS_TYPE >

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

protected

Definition at line 143 of file liblts_pbisim_grv.h.

◆ probability_fraction_type

template<class LTS_TYPE >

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

protected

Definition at line 145 of file liblts_pbisim_grv.h.

◆ probability_label_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::probability_label_type = typename LTS_TYPE::probabilistic_state_t::probability_t

protected

Definition at line 144 of file liblts_pbisim_grv.h.

◆ state_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::state_key_type = std::size_t

protected

Definition at line 142 of file liblts_pbisim_grv.h.

◆ transition_key_type

template<class LTS_TYPE >

using mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::transition_key_type = std::size_t

protected

Definition at line 141 of file liblts_pbisim_grv.h.

Constructor & Destructor Documentation

◆ prob_bisim_partitioner_grv()

template<class LTS_TYPE >

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

inline

Creates a probabilistic bisimulation partitioner for an PLTS.

This bisimulation partitioner applies the algorithm described in "J.F. Groote, H.J. Rivera, E.P. de Vink, An O(mlogn) algorithm for probabilistic bisimulation".

Definition at line 29 of file liblts_pbisim_grv.h.

Member Function Documentation

◆ calculate_equivalent_probabilistic_state()

template<class LTS_TYPE >

LTS_TYPE::probabilistic_state_t mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::calculate_equivalent_probabilistic_state ( probabilistic_block_type & pb )

inlineprotected

Definition at line 1298 of file liblts_pbisim_grv.h.

◆ calculate_new_probabilistic_state()

template<class LTS_TYPE >

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

inlineprotected

Definition at line 1251 of file liblts_pbisim_grv.h.

◆ check_data_structure()

template<class LTS_TYPE >

bool mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::check_data_structure ( )

inlineprotected

Definition at line 346 of file liblts_pbisim_grv.h.

◆ choose_action_splitter()

template<class LTS_TYPE >

action_block_type * mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::choose_action_splitter ( action_constellation_type * non_trivial_action_const )

inlineprotected

Choose an splitter block from a non trivial constellation.

The number of states in the chosen splitter is always less than the half of the non trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.

Definition at line 1173 of file liblts_pbisim_grv.h.

◆ choose_probabilistic_splitter()

template<class LTS_TYPE >

probabilistic_block_type * mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::choose_probabilistic_splitter ( probabilistic_constellation_type * non_trivial_probabilistic_const )

inlineprotected

Choose an splitter block from a non trivial constellation.

The number of states in the chosen splitter is always less than the half of the non trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.

Definition at line 1216 of file liblts_pbisim_grv.h.

◆ create_initial_partition()

template<class LTS_TYPE >

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

inlineprotected

Creates the initial partition.

The blocks are initially partitioned based on the actions that can perform.

Definition at line 443 of file liblts_pbisim_grv.h.

◆ get_eq_class()

template<class LTS_TYPE >

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

inline

Gives the bisimulation equivalence class number of a state.

Parameters

[in] A state number.

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

Definition at line 52 of file liblts_pbisim_grv.h.

◆ get_eq_probabilistic_class()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::get_eq_probabilistic_class ( const std::size_t s )

inline

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

Parameters

[in] A probabilistic state number.

Returns: The number of the probabilistic class to which the state belongs to.

Definition at line 61 of file liblts_pbisim_grv.h.

◆ in_same_probabilistic_class_grv()

template<class LTS_TYPE >

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

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 129 of file liblts_pbisim_grv.h.

◆ mark_action()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::mark_action	(	std::deque< action_mark_type > &	marked_action_blocks,
		const label_type &	a,
		typename embedded_list< action_transition_type >::iterator &	action_walker_begin,
		const typename embedded_list< action_transition_type >::iterator	action_walker_end
	)

inlineprotected

Gives the action blocks that are marked by probabilistic block Bc.

Derives the left, middle and rigth sets of the marked action blocks, based on the incoming action transitions labeled with "a" in block Bc.

Definition at line 1058 of file liblts_pbisim_grv.h.

◆ mark_probabilistic()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::mark_probabilistic	(	const action_block_type &	Bc,
		std::deque< probabilistic_mark_type > &	marked_probabilistic_blocks
	)

inlineprotected

Gives the probabilistic blocks that are marked by block Bc.

Derives the left, middle and rigth sets of the marked probabilistic blocks, based on the incoming probabilistic transitions in block Bc.

Definition at line 928 of file liblts_pbisim_grv.h.

◆ move_list_element_back()

template<class LTS_TYPE >

template<typename LIST_ELEMENT >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::move_list_element_back	(	LIST_ELEMENT &	s,
		embedded_list< LIST_ELEMENT > &	source_list,
		embedded_list< LIST_ELEMENT > &	dest_list
	)

inlineprotected

Definition at line 692 of file liblts_pbisim_grv.h.

◆ move_list_element_front()

template<class LTS_TYPE >

template<typename LIST_ELEMENT >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::move_list_element_front	(	LIST_ELEMENT &	s,
		embedded_list< LIST_ELEMENT > &	source_list,
		embedded_list< LIST_ELEMENT > &	dest_list
	)

inlineprotected

Move an element of a list to the front of another the list.

Definition at line 702 of file liblts_pbisim_grv.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::prob_bisim_partitioner_grv< 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_grv.h.

◆ preprocessing_stage()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::preprocessing_stage ( )

inlineprotected

Definition at line 562 of file liblts_pbisim_grv.h.

◆ print_structure()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::print_structure ( const std::string & info )

inlineprotected

Definition at line 409 of file liblts_pbisim_grv.h.

◆ refine_initial_action_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::refine_initial_action_block ( const std::vector< embedded_list< action_transition_type > > & transitions_per_label )

inlineprotected

Definition at line 621 of file liblts_pbisim_grv.h.

◆ refine_partition_until_it_becomes_stable()

template<class LTS_TYPE >

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

inlineprotected

Refine partition until it becomes stable.

Definition at line 711 of file liblts_pbisim_grv.h.

◆ replace_probabilistic_states()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< 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 classes have been computed.

Definition at line 96 of file liblts_pbisim_grv.h.

◆ replace_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< 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 70 of file liblts_pbisim_grv.h.

◆ split_action_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::split_action_block	(	action_block_type &	block_to_split,
		embedded_list< action_state_type > &	states_of_new_block
	)

inlineprotected

Split an action block.

Creates another block containing the states specified in states_of_new_block. It adds the new block to the same constellation as the current block to split.

Definition at line 891 of file liblts_pbisim_grv.h.

◆ split_probabilistic_block()

template<class LTS_TYPE >

void mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::split_probabilistic_block	(	probabilistic_block_type &	block_to_split,
		embedded_list< probabilistic_state_type > &	states_of_new_block
	)

inlineprotected

Split a probabilistic block.

Creates another block containing the states specified in states_of_new_block. It adds the new block to the same constellation as the current block to split.

Definition at line 856 of file liblts_pbisim_grv.h.

Member Data Documentation

◆ action_blocks

template<class LTS_TYPE >

std::deque<action_block_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::action_blocks

protected

Definition at line 321 of file liblts_pbisim_grv.h.

◆ action_constellations

template<class LTS_TYPE >

std::deque<action_constellation_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::action_constellations

protected

Definition at line 323 of file liblts_pbisim_grv.h.

◆ action_states

template<class LTS_TYPE >

std::vector<action_state_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::action_states

protected

Definition at line 319 of file liblts_pbisim_grv.h.

◆ action_transitions

template<class LTS_TYPE >

std::vector<action_transition_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::action_transitions

protected

Definition at line 317 of file liblts_pbisim_grv.h.

◆ aut

template<class LTS_TYPE >

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

protected

Definition at line 344 of file liblts_pbisim_grv.h.

◆ grouped_states_per_probability_in_block

template<class LTS_TYPE >

std::vector< std::pair<probability_label_type, probabilistic_state_type*> > mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::grouped_states_per_probability_in_block

protected

Definition at line 337 of file liblts_pbisim_grv.h.

◆ marked_action_blocks

template<class LTS_TYPE >

std::deque<action_mark_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::marked_action_blocks

protected

Definition at line 335 of file liblts_pbisim_grv.h.

◆ marked_probabilistic_blocks

template<class LTS_TYPE >

std::deque<probabilistic_mark_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::marked_probabilistic_blocks

protected

Definition at line 336 of file liblts_pbisim_grv.h.

◆ non_trivial_action_constellations

template<class LTS_TYPE >

std::stack<action_constellation_type*> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::non_trivial_action_constellations

protected

Definition at line 331 of file liblts_pbisim_grv.h.

◆ non_trivial_probabilistic_constellations

template<class LTS_TYPE >

std::stack<probabilistic_constellation_type*> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::non_trivial_probabilistic_constellations

protected

Definition at line 332 of file liblts_pbisim_grv.h.

◆ probabilistic_blocks

template<class LTS_TYPE >

std::deque<probabilistic_block_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::probabilistic_blocks

protected

Definition at line 322 of file liblts_pbisim_grv.h.

◆ probabilistic_constellations

template<class LTS_TYPE >

std::deque<probabilistic_constellation_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::probabilistic_constellations

protected

Definition at line 324 of file liblts_pbisim_grv.h.

◆ probabilistic_states

template<class LTS_TYPE >

std::vector<probabilistic_state_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::probabilistic_states

protected

Definition at line 320 of file liblts_pbisim_grv.h.

◆ probabilistic_transitions

template<class LTS_TYPE >

std::deque<probabilistic_transition_type> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::probabilistic_transitions

protected

Definition at line 318 of file liblts_pbisim_grv.h.

◆ state_to_constellation_count

template<class LTS_TYPE >

std::deque<std::size_t> mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::state_to_constellation_count

protected

Definition at line 328 of file liblts_pbisim_grv.h.

◆ transitions_per_label

template<class LTS_TYPE >

transitions_per_label_t mcrl2::lts::detail::prob_bisim_partitioner_grv< LTS_TYPE >::transitions_per_label

protected

Definition at line 341 of file liblts_pbisim_grv.h.

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

lts/include/mcrl2/lts/detail/liblts_pbisim_grv.h

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ block_key_type

◆ constellation_key_type

◆ label_type

◆ probability_fraction_type

◆ probability_label_type

◆ state_key_type

◆ transition_key_type

Constructor & Destructor Documentation

◆ prob_bisim_partitioner_grv()

Member Function Documentation

◆ calculate_equivalent_probabilistic_state()

◆ calculate_new_probabilistic_state()

◆ check_data_structure()

◆ choose_action_splitter()

◆ choose_probabilistic_splitter()

◆ create_initial_partition()

◆ get_eq_class()

◆ get_eq_probabilistic_class()

◆ in_same_probabilistic_class_grv()

◆ mark_action()

◆ mark_probabilistic()

◆ move_list_element_back()

◆ move_list_element_front()

◆ num_eq_classes()

◆ preprocessing_stage()

◆ print_structure()

◆ refine_initial_action_block()

◆ refine_partition_until_it_becomes_stable()

◆ replace_probabilistic_states()

◆ replace_transitions()

◆ split_action_block()

◆ split_probabilistic_block()

Member Data Documentation

◆ action_blocks

◆ action_constellations

◆ action_states

◆ action_transitions

◆ aut

◆ grouped_states_per_probability_in_block

◆ marked_action_blocks

◆ marked_probabilistic_blocks

◆ non_trivial_action_constellations

◆ non_trivial_probabilistic_constellations

◆ probabilistic_blocks

◆ probabilistic_constellations

◆ probabilistic_states

◆ probabilistic_transitions

◆ state_to_constellation_count

◆ transitions_per_label