mcrl2::lts::sigref< LTS_T, Signature > Class Template Reference

Signature based reductions for labelled transition systems. More...

#include <sigref.h>

Public Member Functions
	sigref (LTS_T &lts_)
	Constructor.
void	run ()
	Perform the reduction, modulo the equivalence for which the signature has been passed in as template parameter.

Protected Member Functions
std::string	print_sig (const signature_t &sig)
	Print a signature (for debugging purposes)
void	compute_partition ()
	Compute the partition. Repeatedly updates the signatures, and the partition, until the partition stabilises.
void	quotient ()
	Perform the quotient with respect to the partition that has been computed.

Protected Attributes
std::vector< std::size_t >	m_partition
	Current partition; for each state (std::size_t) the block in which it resides is recorded.
std::size_t	m_count
	The number of blocks in the current partition.
LTS_T &	m_lts
	The LTS that we are reducing.
Signature	m_signature
	Instance of a class performing the signature computation for the current equivalence.

Detailed Description

template<class LTS_T, typename Signature>
class mcrl2::lts::sigref< LTS_T, Signature >

Signature based reductions for labelled transition systems.

The implementation is based on the description in S. Blom, S. Orzan. "Distributed Branching Bisimulation Reduction of State Spaces", in Proc. PDMC 2003.

The specific signature is a parameter of the algorithm.

Definition at line 349 of file sigref.h.

Constructor & Destructor Documentation

sigref()

template<class LTS_T , typename Signature >

mcrl2::lts::sigref< LTS_T, Signature >::sigref ( LTS_T &  lts_ )

inline

Constructor.

Parameters

[in]

lts_

The LTS that is being reduced

Definition at line 448 of file sigref.h.

Member Function Documentation

compute_partition()

template<class LTS_T , typename Signature >

void mcrl2::lts::sigref< LTS_T, Signature >::compute_partition ( )

inlineprotected

Compute the partition. Repeatedly updates the signatures, and the partition, until the partition stabilises.

Definition at line 382 of file sigref.h.

print_sig()

template<class LTS_T , typename Signature >

std::string mcrl2::lts::sigref< LTS_T, Signature >::print_sig ( const signature_t &  sig )

inlineprotected

Print a signature (for debugging purposes)

Definition at line 368 of file sigref.h.

quotient()

template<class LTS_T , typename Signature >

void mcrl2::lts::sigref< LTS_T, Signature >::quotient ( )

inlineprotected

Perform the quotient with respect to the partition that has been computed.

Definition at line 425 of file sigref.h.

run()

template<class LTS_T , typename Signature >

void mcrl2::lts::sigref< LTS_T, Signature >::run ( )

inline

Perform the reduction, modulo the equivalence for which the signature has been passed in as template parameter.

Definition at line 458 of file sigref.h.

Member Data Documentation

m_count

template<class LTS_T , typename Signature >

std::size_t mcrl2::lts::sigref< LTS_T, Signature >::m_count

protected

The number of blocks in the current partition.

Definition at line 358 of file sigref.h.

m_lts

template<class LTS_T , typename Signature >

LTS_T& mcrl2::lts::sigref< LTS_T, Signature >::m_lts

protected

The LTS that we are reducing.

Definition at line 361 of file sigref.h.

m_partition

template<class LTS_T , typename Signature >

std::vector<std::size_t> mcrl2::lts::sigref< LTS_T, Signature >::m_partition

protected

Current partition; for each state (std::size_t) the block in which it resides is recorded.

Definition at line 355 of file sigref.h.

m_signature

template<class LTS_T , typename Signature >

Signature mcrl2::lts::sigref< LTS_T, Signature >::m_signature

protected

Instance of a class performing the signature computation for the current equivalence.

Definition at line 365 of file sigref.h.

---

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

• lts/include/mcrl2/lts/sigref.h