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 &lts_)

Constructor.

Parameters:

• lts_ The LTS that is being reduced