mcrl2::lts::signature< LTS_T > Class Template Reference

Base class for signature computation. More...

#include <sigref.h>

Inheritance diagram for mcrl2::lts::signature< LTS_T >:

Public Member Functions
	signature (const LTS_T &lts_)
	Constructor.
virtual void	compute_signature (const std::vector< std::size_t > &partition)=0
	Compute a new signature based on partition.
virtual void	quotient_transitions (std::set< transition > &transitions, const std::vector< std::size_t > &partition)
	Compute the transitions for the quotient according to partition.
virtual const signature_t &	get_signature (std::size_t i) const
	Return the signature for state i.

Protected Attributes
const LTS_T &	m_lts
	The labelled transition system for which the signature is computed.
std::vector< signature_t >	m_sig
	Signature stored per state.

Detailed Description

template<class LTS_T>
class mcrl2::lts::signature< LTS_T >

Base class for signature computation.

Definition at line 29 of file sigref.h.

Constructor & Destructor Documentation

signature()

template<class LTS_T >

mcrl2::lts::signature< LTS_T >::signature ( const LTS_T &  lts_ )

inline

Constructor.

Definition at line 41 of file sigref.h.

Member Function Documentation

compute_signature()

template<class LTS_T >

virtual void mcrl2::lts::signature< LTS_T >::compute_signature ( const std::vector< std::size_t > &  partition )

pure virtual

Compute a new signature based on partition.

Parameters

[in]

partition

The current partition

Implemented in mcrl2::lts::signature_bisim< LTS_T >, mcrl2::lts::signature_branching_bisim< LTS_T >, and mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >.

get_signature()

template<class LTS_T >

virtual const signature_t & mcrl2::lts::signature< LTS_T >::get_signature ( std::size_t  i ) const

inlinevirtual

Return the signature for state i.

Parameters

[in]

i

The state for which to return the signature.

Precondition

i < m_lts.num_states().

Definition at line 66 of file sigref.h.

quotient_transitions()

template<class LTS_T >

virtual void mcrl2::lts::signature< LTS_T >::quotient_transitions ( std::set< transition > &  transitions, const std::vector< std::size_t > &  partition  )

inlinevirtual

Compute the transitions for the quotient according to partition.

Parameters

[in]	partition	The partition that is used to compute the quotient
[out]	transitions	A set to which the transitions of the quotient are written

Reimplemented in mcrl2::lts::signature_branching_bisim< LTS_T >, and mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >.

Definition at line 54 of file sigref.h.

Member Data Documentation

m_lts

template<class LTS_T >

const LTS_T& mcrl2::lts::signature< LTS_T >::m_lts

protected

The labelled transition system for which the signature is computed.

Definition at line 33 of file sigref.h.

m_sig

template<class LTS_T >

std::vector<signature_t> mcrl2::lts::signature< LTS_T >::m_sig

protected

Signature stored per state.

Definition at line 36 of file sigref.h.

---

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

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