# Strongly connected component: data are read from a Json file in the Ruby
#                               code, useful names are used for vertices
#                               and graphs, and the theory is loaded.
# Author: Richard St-Denis, Universite de Sherbrooke, 2016.

require 'date'
require 'json'

require '/home/ubuntu/WebPages/Digraph.rb'

alloy :Problem do
  open SCC

  pred c__scc[g: (one Digraph), r: (set Vertex)] {
    scc(g, Problem.vtx, r) }
end

class SCC::Vertex
  include Arby::Ast::Sig::CustomizableName
end

class SCC::Digraph
  include Arby::Ast::Sig::CustomizableName

  class << self
    def parse(h)
      n = h[:name];
      v = h[:vertices].map {|s| SCC::Vertex.new(name: s)}
      e = h[:edges].map {|ary|
            src = v.find_by_name(ary[0])
            dst = v.find_by_name(ary[1])
            [src, dst]}
      self.new(name:n, vertices:v, edges:e)
    end
  end
end

module Problem
  class << self
    attr_accessor :vtx
  end
end

module Main
  graphs = File.open('/home/ubuntu/WebPages/ex.json') {|f|
    JSON.parse(f.read, symbolize_names: true).map {
      |hash| SCC::Digraph.parse(hash)}}

  dg = graphs[0];
  print "Enter a vertex among #{dg.vertices}: "
  str = STDIN.gets.strip

  t = Time.now
  dg.vertices.atoms.index {|v|
    if v.name == str then
       Problem.vtx = v
       bnds = Arby::Ast::Bounds.from_atoms(dg)
       sol = Problem.solve(:c__scc, bnds)
       puts "*** Solving time: #{sol.solving_time}s"
       puts sol['$c__scc_r']
       break
    end}

  puts "*** Execution time: #{Time.now - t}s"
  File.open('/home/ubuntu/TEMP/pure_alloy.als', 'w') {|f| f << SCC.to_als}
end