Include file:
#include "mcrl2/lts/sigref.h
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.
m_count
¶The number of blocks in the current partition.
m_lts
¶The LTS that we are reducing.
m_partition
¶Current partition; for each state (std::size_t) the block in which it resides is recorded.
m_signature
¶Instance of a class performing the signature computation for the current equivalence.
compute_partition
()¶Compute the partition. Repeatedly updates the signatures, and the partition, until the partition stabilises.
print_sig
(const signature_t &sig)¶Print a signature (for debugging purposes)
quotient
()¶Perform the quotient with respect to the partition that has been computed.