mcrl2::lts::signature_branching_bisim

Include file:

#include "mcrl2/lts/sigref.h
class mcrl2::lts::signature_branching_bisim

Class for computing the signature for branching bisimulation.

Protected attributes

outgoing_transitions_per_state_t m_prev_transitions

Store the incoming transitions per state.

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.

Parameters:

  • partition The current partition
  • t source state
  • label_ transition label
  • 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.

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.

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_branching_bisim(const LTS_T &lts_)

Constructor.