mcrl2/lps/find_representative.h

Include file:

#include "mcrl2/lps/find_representative.h"

add your file description here.

Functions

Node mcrl2::lps::find_representative(Node &u0, GenerateSuccessors generate_successors)

Search for a unique representative in a graph.

Parameters:

  • u0 The root of the graph.

  • generate_successors A function that generates successors of a node.

This function is based on an iterative version of Tarjan’s strongly connected components algorithm. It returns the smallest node of the first SCC that is detected. The first SCC is a TSCC, meaning that it has no outgoing edges. In a confluent tau graph there is only one TSCC, so this should guarantee a unique representative. N.B. The implementation is based on https://llbit.se/?p=3379