mCRL2
Loading...
Searching...
No Matches
find_representative.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LPS_FIND_REPRESENTATIVE_H
13#define MCRL2_LPS_FIND_REPRESENTATIVE_H
14
15#include <cstddef>
16#include <vector>
18
19namespace mcrl2 {
20
21namespace lps {
22
31template <typename Node, typename GenerateSuccessors>
32Node find_representative(Node& u0, GenerateSuccessors generate_successors)
33{
35
36 std::vector<Node> stack;
37 std::map<Node, std::size_t> low;
38 std::map<Node, std::size_t> disc;
39
40 std::map<Node, std::vector<Node>> successors;
41 std::vector<std::pair<Node, std::size_t>> work;
42
43 successors[u0] = generate_successors(u0);
44 work.emplace_back(std::make_pair(u0, 0));
45
46 while (!work.empty())
47 {
48 Node u = work.back().first;
49 std::size_t i = work.back().second;
50 work.pop_back();
51
52 if (i == 0)
53 {
54 std::size_t k = disc.size();
55 disc[u] = k;
56 low[u] = k;
57 stack.push_back(u);
58 }
59
60 bool recurse = false;
61 const std::vector<Node>& succ = successors[u];
62 for (std::size_t j = i; j < succ.size(); j++)
63 {
64 const Node& v = succ[j];
65 if (disc.find(v) == disc.end())
66 {
67 successors[v] = generate_successors(v);
68 work.emplace_back(std::make_pair(u, j + 1));
69 work.emplace_back(std::make_pair(v, 0));
70 recurse = true;
71 break;
72 }
73 else if (contains(stack, v))
74 {
75 low[u] = std::min(low[u], disc[v]);
76 }
77 }
78 if (recurse)
79 {
80 continue;
81 }
82 if (disc[u] == low[u])
83 {
84 // an SCC has been found; return the node with the minimum value in this SCC
85 Node result = u;
86 while (true)
87 {
88 const auto& v = stack.back();
89 if (v == u)
90 {
91 break;
92 }
93 if (v < result)
94 {
95 result = v;
96 }
97 stack.pop_back();
98 }
99 return result;
100 }
101 if (!work.empty())
102 {
103 Node v = u;
104 u = work.back().first;
105 low[u] = std::min(low[u], low[v]);
106 }
107 }
108 throw mcrl2::runtime_error("find_representative did not find a solution");
109}
110
111} // namespace lps
112
113} // namespace mcrl2
114
115#endif // MCRL2_LPS_FIND_REPRESENTATIVE_H
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
Standard exception class for reporting runtime errors.
Definition exception.h:27
Node find_representative(Node &u0, GenerateSuccessors generate_successors)
Search for a unique representative in a graph.
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72