Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/lps/find_representative.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_FIND_REPRESENTATIVE_H
      13             : #define MCRL2_LPS_FIND_REPRESENTATIVE_H
      14             : 
      15             : #include <cstddef>
      16             : #include <vector>
      17             : #include "mcrl2/utilities/detail/container_utility.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace lps {
      22             : 
      23             : /// \brief Search for a unique representative in a graph.
      24             : /// \param u0 The root of the graph.
      25             : /// \param generate_successors A function that generates successors of a node.
      26             : /// \details This function is based on an iterative version of Tarjan's strongly connected components algorithm.
      27             : /// It returns the smallest node of the first SCC that is detected. The first SCC is a TSCC, meaning
      28             : /// that it has no outgoing edges. In a confluent tau graph there is only one TSCC, so this should
      29             : /// guarantee a unique representative.
      30             : /// N.B. The implementation is based on https://llbit.se/?p=3379
      31             : template <typename Node, typename GenerateSuccessors>
      32          18 : Node find_representative(Node& u0, GenerateSuccessors generate_successors)
      33             : {
      34             :   using utilities::detail::contains;
      35             : 
      36          18 :   std::vector<Node> stack;
      37          18 :   std::map<Node, std::size_t> low;
      38          18 :   std::map<Node, std::size_t> disc;
      39             : 
      40          18 :   std::map<Node, std::vector<Node>> successors;
      41          18 :   std::vector<std::pair<Node, std::size_t>> work;
      42             : 
      43          18 :   successors[u0] = generate_successors(u0);
      44          18 :   work.emplace_back(std::make_pair(u0, 0));
      45             : 
      46          48 :   while (!work.empty())
      47             :   {
      48          24 :     Node u = work.back().first;
      49          24 :     std::size_t i = work.back().second;
      50          24 :     work.pop_back();
      51             : 
      52          24 :     if (i == 0)
      53             :     {
      54          24 :       std::size_t k = disc.size();
      55          24 :       disc[u] = k;
      56          24 :       low[u] = k;
      57          24 :       stack.push_back(u);
      58             :     }
      59             : 
      60          24 :     bool recurse = false;
      61          24 :     const std::vector<Node>& succ = successors[u];
      62          24 :     for (std::size_t j = i; j < succ.size(); j++)
      63             :     {
      64           6 :       const Node& v = succ[j];
      65           6 :       if (disc.find(v) == disc.end())
      66             :       {
      67           6 :         successors[v] = generate_successors(v);
      68           6 :         work.emplace_back(std::make_pair(u, j + 1));
      69           6 :         work.emplace_back(std::make_pair(v, 0));
      70           6 :         recurse = true;
      71           6 :         break;
      72             :       }
      73           0 :       else if (contains(stack, v))
      74             :       {
      75           0 :         low[u] = std::min(low[u], disc[v]);
      76             :       }
      77             :     }
      78          24 :     if (recurse)
      79             :     {
      80           6 :       continue;
      81             :     }
      82          18 :     if (disc[u] == low[u])
      83             :     {
      84             :       // an SCC has been found; return the node with the minimum value in this SCC
      85          18 :       Node result = u;
      86           0 :       while (true)
      87             :       {
      88          18 :         const auto& v = stack.back();
      89          18 :         if (v == u)
      90             :         {
      91          18 :           break;
      92             :         }
      93           0 :         if (v < result)
      94             :         {
      95           0 :           result = v;
      96             :         }
      97           0 :         stack.pop_back();
      98             :       }
      99          36 :       return result;
     100          18 :     }
     101           0 :     if (!work.empty())
     102             :     {
     103           0 :       Node v = u;
     104           0 :       u = work.back().first;
     105           0 :       low[u] = std::min(low[u], low[v]);
     106           0 :     }
     107             :   }
     108           0 :   throw mcrl2::runtime_error("find_representative did not find a solution");
     109          18 : }
     110             : 
     111             : } // namespace lps
     112             : 
     113             : } // namespace mcrl2
     114             : 
     115             : #endif // MCRL2_LPS_FIND_REPRESENTATIVE_H