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

Class for computing the signature for branching bisimulation. More...

#include <sigref.h>

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

Public Member Functions
	signature_branching_bisim (const LTS_T &lts_)
	Constructor
virtual void	compute_signature (const std::vector< std::size_t > &partition)
virtual void	quotient_transitions (std::set< transition > &transitions, const std::vector< std::size_t > &partition)
Public Member Functions inherited from mcrl2::lts::signature< LTS_T >
	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 Member Functions
void	insert (const std::vector< std::size_t > &partition, const std::size_t t, const std::size_t label_, const std::size_t block)
	Insert function.

Protected Attributes
outgoing_transitions_per_state_t	m_prev_transitions
	Store the incoming transitions per state.
Protected Attributes inherited from mcrl2::lts::signature< LTS_T >
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_branching_bisim< LTS_T >

Class for computing the signature for branching bisimulation.

Definition at line 104 of file sigref.h.

Constructor & Destructor Documentation

signature_branching_bisim()

template<class LTS_T >

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

inline

Constructor

Definition at line 148 of file sigref.h.

Member Function Documentation

compute_signature()

template<class LTS_T >

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

inlinevirtual

This is an overloaded member function, provided for convenience. It differs from the above function only in what argument(s) it accepts.

Implements mcrl2::lts::signature< LTS_T >.

Reimplemented in mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >.

Definition at line 156 of file sigref.h.

insert()

template<class LTS_T >

void mcrl2::lts::signature_branching_bisim< LTS_T >::insert ( const std::vector< std::size_t > &  partition, const std::size_t  t, const std::size_t  label_, const std::size_t  block  )

inlineprotected

Insert function.

Parameters

[in]	partition	The current partition
[in]	t	source state
[in]	label_	transition label
[in]	block	target block

Insert function as described in S. Blom, S. Orzan, "Distributed Branching Bisimulation Reduction of State Spaces", Proc. PDMC 2003.

Inserts the pair (label_, block) in the signature of t, as well as the signatures of all tau-predecessors of t within the same block.

Definition at line 126 of file sigref.h.

quotient_transitions()

template<class LTS_T >

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

inlinevirtual

This is an overloaded member function, provided for convenience. It differs from the above function only in what argument(s) it accepts.

Reimplemented from mcrl2::lts::signature< LTS_T >.

Reimplemented in mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >.

Definition at line 170 of file sigref.h.

Member Data Documentation

m_prev_transitions

template<class LTS_T >

outgoing_transitions_per_state_t mcrl2::lts::signature_branching_bisim< LTS_T >::m_prev_transitions

protected

Store the incoming transitions per state.

Definition at line 111 of file sigref.h.

---

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

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