12#ifndef MCRL2_LPS_FIND_REPRESENTATIVE_H
13#define MCRL2_LPS_FIND_REPRESENTATIVE_H
31template <
typename Node,
typename GenerateSuccessors>
36 std::vector<Node> stack;
37 std::map<Node, std::size_t> low;
38 std::map<Node, std::size_t> disc;
40 std::map<Node, std::vector<Node>> successors;
41 std::vector<std::pair<Node, std::size_t>> work;
43 successors[u0] = generate_successors(u0);
44 work.emplace_back(std::make_pair(u0, 0));
48 Node u = work.back().first;
49 std::size_t i = work.back().second;
54 std::size_t k = disc.size();
61 const std::vector<Node>& succ = successors[u];
62 for (std::size_t j = i; j < succ.
size(); j++)
64 const Node& v = succ[j];
65 if (disc.find(v) == disc.end())
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));
73 else if (contains(stack, v))
75 low[u] = std::min(low[u], disc[v]);
82 if (disc[u] == low[u])
88 const auto& v = stack.back();
104 u = work.back().first;
105 low[u] = std::min(low[u], low[v]);
size_type size() const
Returns the number of arguments of this term.
Standard exception class for reporting runtime errors.
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)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...