Lean4
/-- The Tarjan's algorithm.
See [Wikipedia](https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm). -/
partial def tarjanDFS (g : Graph) (v : Nat) : StateM TarjanState Unit := do
modify fun s =>
{ visited := s.visited.set! v true, id := s.id.set! v s.time, lowlink := s.lowlink.set! v s.time,
stack := s.stack.push v, onStack := s.onStack.set! v true, time := s.time + 1 }
for edge in g[v]!do
let u := edge.dst
if !(← get).visited[u]! then
tarjanDFS g u
modify fun s => { s with lowlink := s.lowlink.set! v (min s.lowlink[v]! s.lowlink[u]!), }
else if (← get).onStack[u]! then
modify fun s => { s with lowlink := s.lowlink.set! v (min s.lowlink[v]! s.id[u]!), }
if (← get).id[v]! = (← get).lowlink[v]! then
let mut w := 0
while true do
w := (← get).stack.back!
modify fun s =>
{ s with
stack := s.stack.pop
onStack := s.onStack.set! w false
lowlink := s.lowlink.set! w s.lowlink[v]! }
if w = v then
break
