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
