Content deleted Content added
Undid revision 1140819830 by 128.187.116.19 (talk) - that claim would need a source, as it disagrees with the paragraph below Tags: Undo Mobile edit Mobile web edit Advanced mobile edit |
→The algorithm in pseudocode: some more on using lowlink vs index, couldn't find any reliable source with a proof that it worked so wrote some vague FUD Tag: Reverted |
||
Line 80:
When each node finishes recursing, if its lowlink is still set to its index, then it is the root node of a strongly connected component, formed by all of the nodes above it on the stack. The algorithm pops the stack up to and including the current node, and presents all of these nodes as a strongly connected component.
Note that <code>''v''.lowlink := min(''v''.lowlink, ''w''.index)</code> is the correct way to update <code>''v.lowlink''</code> if <code>''w''</code> is on stack. Because <code>''w''</code> is on the stack already, <code>''(v, w)''</code> is a back-edge in the DFS tree and therefore <code>''w''</code> is not in the subtree of <code>''v''</code>. Because <code>''v.lowlink''</code> takes into account nodes reachable only through the nodes in the subtree of <code>''v''</code> we must stop at <code>''w''</code> and use <code>''w.index''</code> instead of <code>''w.lowlink''</code>. Some sources instead use <code>''v''.lowlink := min(''v''.lowlink, ''w''.lowlink)</code>.<ref>{{cite journal |last1=Kordy |first1=Piotr |last2=Langerak |first2=Rom |last3=Mauw |first3=Sjouke |last4=Polderman |first4=Jan Willem |title=A Symbolic Algorithm for the Analysis of Robust Timed Automata |journal=FM 2014: Formal Methods |date=2014 |volume=8442 |pages=351–366 |doi=10.1007/978-3-319-06410-9_25 |url=https://satoss.uni.lu/members/sjouke/papers/KLMP14.pdf}}</ref> This variation appears to work in practice for small graphs but has not been proven correct, so may in fact give erroneous results on large graphs.
== Complexity ==
| |||