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

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

#include <sigref.h>

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

Public Member Functions
	signature_divergence_preserving_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_branching_bisim< LTS_T >
	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	compute_tau_sccs ()
	Iterative implementation of Tarjan's SCC algorithm.
Protected Member Functions inherited from mcrl2::lts::signature_branching_bisim< LTS_T >
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
std::vector< bool >	m_divergent
	Record for each vertex whether it is in a tau-scc.
Protected Attributes inherited from mcrl2::lts::signature_branching_bisim< LTS_T >
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_divergence_preserving_branching_bisim< LTS_T >

Class for computing the signature for divergence preserving branching bisimulation.

Definition at line 184 of file sigref.h.

Constructor & Destructor Documentation

signature_divergence_preserving_branching_bisim()

template<class LTS_T >

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

inline

Constructor.

This initialises m_divergent to record for each vertex whether it is in a tau-scc.

Definition at line 298 of file sigref.h.

Member Function Documentation

compute_signature()

template<class LTS_T >

virtual void mcrl2::lts::signature_divergence_preserving_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.

Compute the signature as in branching bisimulation. In addition, add the (tau, B) for edges s -tau-> t for which s,t in B and m_divergent[t]

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

Definition at line 311 of file sigref.h.

compute_tau_sccs()

template<class LTS_T >

void mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >::compute_tau_sccs ( )

inlineprotected

Iterative implementation of Tarjan's SCC algorithm.

based on an earlier implementation by Sjoerd Cranen

For the non-trivial tau-sccs (i.e. SCCs with more than one state, or single-state SCCs with a tau-loop, we set m_divergent to true.

Definition at line 201 of file sigref.h.

quotient_transitions()

template<class LTS_T >

virtual void mcrl2::lts::signature_divergence_preserving_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_branching_bisim< LTS_T >.

Definition at line 326 of file sigref.h.

Member Data Documentation

m_divergent

template<class LTS_T >

std::vector<bool> mcrl2::lts::signature_divergence_preserving_branching_bisim< LTS_T >::m_divergent

protected

Record for each vertex whether it is in a tau-scc.

Definition at line 192 of file sigref.h.

---

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

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