mcrl2::lts::signature_divergence_preserving_branching_bisim

Include file:

#include "mcrl2/lts/sigref.h

class mcrl2::lts::signature_divergence_preserving_branching_bisim

Class for computing the signature for divergence preserving branching bisimulation.

Protected attributes

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

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

Protected member functions

void compute_tau_sccs()

Iterative implementation of Tarjan’s SCC algorithm.

based on an earlier implementation by Sjoerd CranenFor 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.

Public member functions

virtual void compute_signature(const std::vector<std::size_t> &partition)

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]

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

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

signature_divergence_preserving_branching_bisim(const LTS_T &lts_)

Constructor.

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