# Strongly connected component: the theory.
# Author: Richard St-Denis, Universite de Sherbrooke, 2016.

alloy :SCC do
  abstract sig Vertex [ ] { }

  abstract sig Digraph [
     vertices: (set Vertex),
     edges: (set Vertex ** Vertex) ] {
       edges.(this.vertices).in? vertices and
       vertices.(this.edges).in? vertices }

  pred scc[g: (one Digraph), v: (one Vertex),
           c: (set Vertex)] {
    c == g.vertices.select {|u|
           u.in? v.*(g.edges) and
           v.in? u.*(g.edges) } }
end