# Strongly connected component: data are created in the Ruby code.
# Author: Richard St-Denis, Universite de Sherbrooke, 2016.

require 'date'

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

module Main
  nodes = 10.times.map{SCC::Vertex.new}
  dg = SCC::Digraph.new \
         vertices: nodes,
         edges: [
                 [0, 1], [1, 2], [1, 4], [1, 5],
                 [2, 3], [2, 6], [3, 2], [3, 7],
                 [4, 0], [4, 5], [5, 6], [6, 5],
                 [6, 7], [7, 7], [8, 3], [8, 9],
                 [9, 8]
                ].map{|e| e.map{|i| nodes[i]}}

  bnds = Arby::Ast::Bounds.from_atoms(dg)
  t = Time.now
  sol = SCC.solve(:scc, bnds)
  puts "*** Solving time: #{sol.solving_time}s"
  if sol.satisfiable? then
     puts sol['$scc_g'].vertices
  end
  while sol.satisfiable? do
    print sol['$scc_v'];   puts sol['$scc_c']
    sol = sol.next
  end
  puts "*** Execution time: #{Time.now - t}s"
  File.open('/home/ubuntu/TEMP/pure_alloy.als', 'w') {|f| f << SCC.to_als}
end