Include file:
#include "mcrl2/lts/sigref.h
mcrl2::lts::
signature_divergence_preserving_branching_bisim
¶Class for computing the signature for divergence preserving branching bisimulation.
mcrl2::lts::signature_divergence_preserving_branching_bisim::
m_divergent
¶Record for each vertex whether it is in a tau-scc.
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.
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]
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 <s_)¶Constructor.
This initialises m_divergent to record for each vertex whether it is in a tau-scc.