#include <liblts_sim.h>

Inheritance diagram for mcrl2::lts::detail::sim_partitioner< LTS_TYPE >:

Classes
struct	state_bucket

Public Member Functions
	sim_partitioner (LTS_TYPE &l)

virtual	~sim_partitioner ()

virtual void	partitioning_algorithm ()

std::vector< mcrl2::lts::transition >	get_transitions () const

std::size_t	num_eq_classes () const

std::size_t	get_eq_class (std::size_t s) const

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

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

Protected Member Functions
void	partitioning_algorithmG ()

void	initialise_datastructures ()

void	refine (bool &change)

void	update ()

void	touch (std::size_t a, std::size_t alpha)

void	untouch (std::size_t alpha)

void	reverse_topological_sort (std::vector< std::size_t > &Sort)

void	dfs_visit (std::size_t u, std::vector< bool > &visited, std::vector< std::size_t > &Sort)

void	initialise_Sigma (std::size_t gamma, std::size_t l)

void	initialise_Pi (std::size_t gamma, std::size_t l)

void	filter (std::size_t S, std::vector< std::vector< bool > > &R, bool B)

void	cleanup (std::size_t alpha, std::size_t beta)

void	initialise_pre_EA ()

void	induce_P_on_Pi ()

std::string	print_Sigma_P ()

std::string	print_Pi_Q ()

std::string	print_Sigma ()

std::string	print_Pi ()

std::string	print_relation (std::size_t s, std::vector< std::vector< bool > > &R)

std::string	print_block (std::size_t b)

std::string	print_structure (hash_table3 *struc)

std::string	print_reverse_topological_sort (const std::vector< std::size_t > &Sort)

Protected Attributes
LTS_TYPE &	aut

mcrl2::lts::outgoing_transitions_per_state_action_t	trans_index

std::size_t	s_Sigma = 0UL

std::size_t	s_Pi = 0UL

std::vector< bool >	state_touched

std::vector< bool >	block_touched

std::vector< state_bucket >	state_buckets

std::vector< std::size_t >	block_Pi

std::vector< std::size_t >	parent

std::vector< std::vector< std::size_t > >	children

std::vector< ptrdiff_t >	contents_t

std::vector< ptrdiff_t >	contents_u

std::vector< std::vector< bool > >	stable

hash_table3 *	exists

hash_table3 *	forall

std::vector< std::vector< std::size_t > >	pre_exists

std::vector< std::vector< std::size_t > >	pre_forall

hash_table3 *	match

std::vector< std::vector< bool > >	P

std::vector< std::vector< bool > >	Q

std::vector< std::size_t >	touched_blocks

std::vector< std::size_t >	contents

Detailed Description

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

Definition at line 24 of file liblts_sim.h.

Constructor & Destructor Documentation

◆ sim_partitioner()

template<class LTS_TYPE >

mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::sim_partitioner ( LTS_TYPE & l )

Creates a partitioner for an LTS.

Parameters

[in] l Pointer to the LTS.

Definition at line 155 of file liblts_sim.h.

◆ ~sim_partitioner()

template<class LTS_TYPE >

mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::~sim_partitioner

virtual

Destroys this partitioner.

Definition at line 164 of file liblts_sim.h.

Member Function Documentation

◆ cleanup()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::cleanup	(	std::size_t	alpha,
		std::size_t	beta
	)

protected

Definition at line 735 of file liblts_sim.h.

◆ dfs_visit()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::dfs_visit	(	std::size_t	u,
		std::vector< bool > &	visited,
		std::vector< std::size_t > &	Sort
	)

protected

Definition at line 476 of file liblts_sim.h.

◆ filter()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::filter	(	std::size_t	S,
		std::vector< std::vector< bool > > &	R,
		bool	B
	)

protected

Definition at line 675 of file liblts_sim.h.

◆ get_eq_class()

template<class LTS_TYPE >

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

Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and excluding) num_eq_classes().

Precondition: The simulation equivalence classes have been computed.

Parameters

[in] s A state number.

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

Definition at line 838 of file liblts_sim.h.

◆ get_transitions()

template<class LTS_TYPE >

std::vector< mcrl2::lts::transition > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::get_transitions

Gives the transition relation on the computed equivalence classes of the LTS. The label numbers of the transitions correspond to the label numbers of the LTS that was passed as an argument to the constructor of this partitioner. The state numbers of the transitions are the equivalence class numbers which range from 0 upto (and excluding) num_eq_classes().

Precondition: The simulation equivalence classes have been computed.

Returns: A vector containing the transitions between the simulation equivalence classes.

Definition at line 780 of file liblts_sim.h.

◆ in_preorder()

template<class LTS_TYPE >

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

Returns whether one state is simulated by another state.

Precondition: The simulation preorder has been computed.

Parameters

[in]	s	A state number.
[in]	t	A state number.

Return values

true	if s is simulated by t;
false	otherwise.

Definition at line 844 of file liblts_sim.h.

◆ in_same_class()

template<class LTS_TYPE >

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

Returns whether two states are in the same simulation equivalence class.

Precondition: The simulation equivalence classes have been computed.

Parameters

[in]	s	A state number.
[in]	t	A state number.

Return values

true	if s and t are in the same simulation equivalence class;
false	otherwise.

Definition at line 850 of file liblts_sim.h.

◆ induce_P_on_Pi()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::induce_P_on_Pi

protected

Definition at line 652 of file liblts_sim.h.

◆ initialise_datastructures()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::initialise_datastructures

protected

Definition at line 235 of file liblts_sim.h.

◆ initialise_Pi()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::initialise_Pi	(	std::size_t	gamma,
		std::size_t	l
	)

protected

Definition at line 291 of file liblts_sim.h.

◆ initialise_pre_EA()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::initialise_pre_EA

protected

Definition at line 641 of file liblts_sim.h.

◆ initialise_Sigma()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::initialise_Sigma	(	std::size_t	gamma,
		std::size_t	l
	)

protected

Definition at line 336 of file liblts_sim.h.

◆ num_eq_classes()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::num_eq_classes

Gives the number of simulation equivalence classes of the LTS.

Precondition: The simulation equivalence classes have been computed.

Returns: The number of simulation equivalence classes of the LTS.

Definition at line 832 of file liblts_sim.h.

◆ partitioning_algorithm()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::partitioning_algorithm

virtual

Computes the simulation equivalence classes and preorder relations of the LTS.

Reimplemented in mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >.

Definition at line 174 of file liblts_sim.h.

◆ partitioning_algorithmG()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::partitioning_algorithmG

protected

Computes the simulation equivalence classes and preorder relations of the LTS.

Precondition: : initialise_datastructures called

Definition at line 182 of file liblts_sim.h.

◆ print_block()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_block ( std::size_t b )

protected

Definition at line 908 of file liblts_sim.h.

◆ print_Pi()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_Pi

protected

Definition at line 896 of file liblts_sim.h.

◆ print_Pi_Q()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_Pi_Q

protected

Definition at line 867 of file liblts_sim.h.

◆ print_relation()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_relation	(	std::size_t	s,
		std::vector< std::vector< bool > > &	R
	)

protected

Definition at line 924 of file liblts_sim.h.

◆ print_reverse_topological_sort()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_reverse_topological_sort ( const std::vector< std::size_t > & Sort )

protected

Definition at line 963 of file liblts_sim.h.

◆ print_Sigma()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_Sigma

protected

Definition at line 876 of file liblts_sim.h.

◆ print_Sigma_P()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_Sigma_P

protected

Definition at line 858 of file liblts_sim.h.

◆ print_structure()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::print_structure ( hash_table3 * struc )

protected

Definition at line 947 of file liblts_sim.h.

◆ refine()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::refine ( bool & change )

protected

Definition at line 351 of file liblts_sim.h.

◆ reverse_topological_sort()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::reverse_topological_sort ( std::vector< std::size_t > & Sort )

protected

Definition at line 463 of file liblts_sim.h.

◆ touch()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::touch	(	std::size_t	a,
		std::size_t	alpha
	)

protected

Definition at line 491 of file liblts_sim.h.

◆ untouch()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::untouch ( std::size_t alpha )

protected

Definition at line 519 of file liblts_sim.h.

◆ update()

template<class LTS_TYPE >

void mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::update

protected

Definition at line 547 of file liblts_sim.h.

Member Data Documentation

◆ aut

template<class LTS_TYPE >

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

protected

Definition at line 96 of file liblts_sim.h.

◆ block_Pi

template<class LTS_TYPE >

std::vector<std::size_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::block_Pi

protected

Definition at line 103 of file liblts_sim.h.

◆ block_touched

template<class LTS_TYPE >

std::vector<bool> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::block_touched

protected

Definition at line 101 of file liblts_sim.h.

◆ children

template<class LTS_TYPE >

std::vector< std::vector<std::size_t> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::children

protected

Definition at line 105 of file liblts_sim.h.

◆ contents

template<class LTS_TYPE >

std::vector<std::size_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::contents

protected

Definition at line 119 of file liblts_sim.h.

◆ contents_t

template<class LTS_TYPE >

std::vector<ptrdiff_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::contents_t

protected

Definition at line 106 of file liblts_sim.h.

◆ contents_u

template<class LTS_TYPE >

std::vector<ptrdiff_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::contents_u

protected

Definition at line 107 of file liblts_sim.h.

◆ exists

template<class LTS_TYPE >

hash_table3* mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::exists

protected

Definition at line 109 of file liblts_sim.h.

◆ forall

template<class LTS_TYPE >

hash_table3* mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::forall

protected

Definition at line 110 of file liblts_sim.h.

◆ match

template<class LTS_TYPE >

hash_table3* mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::match

protected

Definition at line 113 of file liblts_sim.h.

◆ P

template<class LTS_TYPE >

std::vector< std::vector<bool> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::P

protected

Definition at line 114 of file liblts_sim.h.

◆ parent

template<class LTS_TYPE >

std::vector<std::size_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::parent

protected

Definition at line 104 of file liblts_sim.h.

◆ pre_exists

template<class LTS_TYPE >

std::vector< std::vector<std::size_t> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::pre_exists

protected

Definition at line 111 of file liblts_sim.h.

◆ pre_forall

template<class LTS_TYPE >

std::vector< std::vector<std::size_t> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::pre_forall

protected

Definition at line 112 of file liblts_sim.h.

◆ Q

template<class LTS_TYPE >

std::vector< std::vector<bool> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::Q

protected

Definition at line 115 of file liblts_sim.h.

◆ s_Pi

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::s_Pi = 0UL

protected

Definition at line 99 of file liblts_sim.h.

◆ s_Sigma

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::s_Sigma = 0UL

protected

Definition at line 98 of file liblts_sim.h.

◆ stable

template<class LTS_TYPE >

std::vector< std::vector<bool> > mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::stable

protected

Definition at line 108 of file liblts_sim.h.

◆ state_buckets

template<class LTS_TYPE >

std::vector<state_bucket> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::state_buckets

protected

Definition at line 102 of file liblts_sim.h.

◆ state_touched

template<class LTS_TYPE >

std::vector<bool> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::state_touched

protected

Definition at line 100 of file liblts_sim.h.

◆ touched_blocks

template<class LTS_TYPE >

std::vector<std::size_t> mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::touched_blocks

protected

Definition at line 118 of file liblts_sim.h.

◆ trans_index

template<class LTS_TYPE >

mcrl2::lts::outgoing_transitions_per_state_action_t mcrl2::lts::detail::sim_partitioner< LTS_TYPE >::trans_index

protected

Definition at line 97 of file liblts_sim.h.

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

lts/include/mcrl2/lts/detail/liblts_sim.h

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ sim_partitioner()

◆ ~sim_partitioner()

Member Function Documentation

◆ cleanup()

◆ dfs_visit()

◆ filter()

◆ get_eq_class()

◆ get_transitions()

◆ in_preorder()

◆ in_same_class()

◆ induce_P_on_Pi()

◆ initialise_datastructures()

◆ initialise_Pi()

◆ initialise_pre_EA()

◆ initialise_Sigma()

◆ num_eq_classes()

◆ partitioning_algorithm()

◆ partitioning_algorithmG()

◆ print_block()

◆ print_Pi()

◆ print_Pi_Q()

◆ print_relation()

◆ print_reverse_topological_sort()

◆ print_Sigma()

◆ print_Sigma_P()

◆ print_structure()

◆ refine()

◆ reverse_topological_sort()

◆ touch()

◆ untouch()

◆ update()

Member Data Documentation

◆ aut

◆ block_Pi

◆ block_touched

◆ children

◆ contents

◆ contents_t

◆ contents_u

◆ exists

◆ forall

◆ match

◆ P

◆ parent

◆ pre_exists

◆ pre_forall

◆ Q

◆ s_Pi

◆ s_Sigma

◆ stable

◆ state_buckets

◆ state_touched

◆ touched_blocks

◆ trans_index