# State-based control of discrete event systems under total observation.
# Control problem solve with the first approach and the state feedback
# function with disabled events.
# copyright Richard St-Denis, Universite de Sherbrooke, 2016.

require 'date'
require 'json'

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

alloy :Problem do
  open SBCDES

  pred c__nbcField[g: (one Automaton), s: (set StateSpace)] {
  # Start with the control specification and
  # generate a sequence of stronger predicates.
    s == nbcField(g, Problem.predicate) }

  pred c__sfbc[g: (one Automaton), f: (set StateSpace ** EventSet)] {
  # Return the state feedback control function (disabled events).
    f == sfbc(g, Problem.predicate) }
end

class SBCDES::StateSpace
  include Arby::Ast::Sig::CustomizableName
end

class SBCDES::EventSet
  include Arby::Ast::Sig::CustomizableName
end

class SBCDES::Automaton
  include Arby::Ast::Sig::CustomizableName

  class << self
    def parse(hash)
      n = hash[:name]
      s = hash[:states].map {|str| SBCDES::StateSpace.new(name: str)}
      e = hash[:events].map {|str| SBCDES::EventSet.new(name: str)}
      i = hash[:initialState].map {|str| s.find_by_name(str)}
      m = hash[:markedStates].map {|str| s.find_by_name(str)}
      c = hash[:ctrlEvents].map {|str| e.find_by_name(str)}
      t = hash[:transition].map {|ary|
            src   = s.find_by_name(ary[0])
            event = e.find_by_name(ary[1])
            dst   = s.find_by_name(ary[2])
            [src, event, dst]}
      self.new(name: n, states: s, events: e,
               initialState: i, markedStates: m,
               ctrlEvents: c, transition: t)
    end
  end
end

module Problem
  class << self
    attr_accessor :predicate

    def parse_automata(filename)
    # read automata
      File.open(filename) {|f|
        JSON.parse(f.read, symbolize_names: true).map {
          |hash| SBCDES::Automaton.parse(hash)}}
    end

    def get_input_data(automaton, filename)
    # read auxiliary data related to the control problem
      File.open(filename) {|f|
        h = JSON.parse(f.read, symbolize_names: true)

        @predicate = Arby::Ast::TupleSet.parse(
          automaton.states.select_atoms_by_names(h[:predicate]))}
    end
  end
end

module Main
  print "Enter a file name (without extension): "
  str = STDIN.gets.strip

  a = Problem.parse_automata('/home/ubuntu/WebPages/'+str+'.json')

  Problem.get_input_data(a[0], '/home/ubuntu/WebPages/'+str+'spec.json')

  t = Time.now
  bnds = Arby::Ast::Bounds.from_atoms(a[0])

  i = 1
  loop do
    sol = Problem.solve(:c__nbcField, bnds)
    q = sol["$c__nbcField_s"]
    print "Iteration #{i}: ";   puts q
    puts "  *** Solving time: #{sol.solving_time}s"
    break unless q != Problem.predicate
    Problem.predicate = q
    i = i + 1
  end

  sol = Problem.solve(:c__sfbc, bnds)
  if sol.satisfiable?
     print "SFBC function (disabled events): "
     puts sol["$c__sfbc_f"]
     puts "  *** Solving time: #{sol.solving_time}s"
  end

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