mcrl2::lts::sigref
Include file:
#include "mcrl2/lts/sigref.h

class
mcrl2::lts::
sigref
Signature based reductions for labelled transition systems.
The implementation is based on the description in S. Blom, S. Orzan. “Distributed Branching Bisimulation Reduction of State
Spaces”, in Proc. PDMC 2003.The specific signature is a parameter of the algorithm.
Protected attributes

std::size_t
mcrl2::lts::sigref::
m_count
The number of blocks in the current partition.

LTS_T &
mcrl2::lts::sigref::
m_lts
The LTS that we are reducing.

std::vector<std::size_t>
mcrl2::lts::sigref::
m_partition
Current partition; for each state (std::size_t) the block in which it resides is recorded.

Signature
mcrl2::lts::sigref::
m_signature
Instance of a class performing the signature computation for the current equivalence.
Protected member functions

void
compute_partition
()
Compute the partition. Repeatedly updates the signatures, and the partition, until the partition stabilises.

std::string
print_sig
(const signature_t &sig)
Print a signature (for debugging purposes)

void
quotient
()
Perform the quotient with respect to the partition that has been computed.
Public member functions

void
run
()
Perform the reduction, modulo the equivalence for which the signature has been passed in as template parameter.

sigref
(LTS_T <s_)
Constructor.
Parameters: