(********************************************)
(** Execução de autómatos não deterministas
    com transições codificadas como tabelas
    de Hash para conjuntos de estados       *)
(********************************************)
(** @author: Simão Melo de Sousa, RELEASE-DI-UBI-PT, desousa@di.ubi.pt *)
(** compilação: ocamlopt fsa_set.ml -o ndfa

    versão >=4.07*)
(** documentação: ocamldoc -hide-warnings -html -charset utf8 -short-functors -stars -keep-code -colorize-code  -impl fsa_set.ml *)

(** {1  Estruturas de dados} *)


(** [simbolo] é o tipo para o alfabeto considerado, aumentado do símbolo "epsilon".
    O símbolo "epsilon" tem por representação o valor [None] e
    o caracter c tem por representação [Some c]  *)
type simbolo = char option

let (epsilon:simbolo) = None

(** a fita de entrada é representada por uma lista de símbolos, de tipo [fita] *)
type fita =  simbolo list

(** [Estados]: módulo para a representações dos estados de um autómato.
    representamos estados como inteiros. estruturamos estes tipo com a função [compare] habitual *)
module Estados =
       struct
         type t = int
         let compare  = compare
       end

(** [Sestado]: módulo para conjuntos de estados *)
module Sestado = Set.Make(Estados)

(** tipo dos estados, como abreviatura do tipo Estados.t*)
type estado = Estados.t

(** tipo dos conjuntos de estados, como abreviatura do tipo Sestado.t*)
type estados = Sestado.t

(** [transicoes]: tipo das transições. Codificado como uma hashtable de
    (estado*simbolo) para conjuntos de estados (por causa do não-determinismo) *)
type transicoes =  ((estado*simbolo), estados) Hashtbl.t


(** [maquina]: tipo dos autómatos não deterministas. Um autómato é definido como
    o tuplo (transições, estados iniciais, estados finais) *)
type maquina = (transicoes  * estados  * estados)

(** [configuracao]: tipo das configurações. Uma configuração é um par *)
type configuracao = (estados  * fita)


(** {1 Leitura dos dados} *)

(** [to_fita] é uma função de tradução de [char] para [simbolo].
    O caracter '_' é entendido como o epsilon *)
let to_fita c =  if c='_' then None else (Some c)


(** tradução para o formato transição*)
let triplo a b c =  ((a, to_fita b),c)


(** função utilitária simples*)
let char_of_string s = s.[0]

(** [read_to_set] lê uma linha de inteiros e devolve na forma de uma lista de inteiros  *)
let read_to_list f =  (List.map f (String.split_on_char ' ' (read_line ())))

(** [read_to_set] lê uma linha de inteiros e devolve na forma de um conjunto de inteiros  *)
let read_to_set f =  (*Sestado.of_seq (List.to_seq (List.map f (String.split_on_char ' ' (read_line ()))))*)
(read_line ()) |> (String.split_on_char ' ') |> (List.map f) |> List.to_seq |> Sestado.of_seq

(** [read_transition] lê transições linha a linha até ao fim de ficheiro.
    Formata as transições lidas para o tipo [transicoes] *)
let read_transition ()  =
  let (ht:transicoes) = Hashtbl.create 97 in
  try
    while true do
      let (a,b) = (Scanf.sscanf (read_line ()) " %d %c %d" triplo) in
      let res = try Hashtbl.find ht a with Not_found -> Sestado.empty
      in Hashtbl.replace ht a (Sestado.add b res)
    done; ht
  with _ -> ht

(**
[leitura] lê no formato texto o autómato por executar, e a palavra por reconhecer.
A leitura devolve as estruturas correspondentes.
*)
let leitura () =
  let dados = read_to_list (fun x -> x |> char_of_string |> to_fita) in
  let init_set = read_to_set int_of_string in
  let final_set =  read_to_set int_of_string in
  let transitions = read_transition () in
  (dados,(transitions,init_set,final_set))



(** {1 Execução} *)

(** execução que permite assinalar o fim de uma execução, com o registo da respectiva configuração final *)
exception FIM of configuracao

(** [reach] calcula que estados são alvo de transições directas
    que partem do estado [state] com rótulo [ch] no autómato [maquina]*)
let reach (transicoes,_,_:maquina) (state:estado) (ch:simbolo)  =
  try
    Hashtbl.find transicoes (state,ch)
  with Not_found -> Sestado.empty

(** [reach_states] calcula que estados são alvo de transições directas
    que partem do conjunto de estados [states] com rótulo [ch] no autómato [maquina]*)
let reach_states ((transicoes,_,_) as maq : maquina) (states:estados) (ch:simbolo)  =
  Sestado.fold (fun state acc-> Sestado.union acc (reach maq state ch)) states Sestado.empty

(** [reach_star_aux] é função (recursiva) auxiliar da função [reach_star] e
    calcula que estados são alvo de transições directas e indirectas
    que partem do conjunto de estados [todo] com rótulo [ch] no autómato [maquina].
    Os estados já considerados encontram-se em [final], nunca é considerado
    estados de [final] quando são processados os estados de [todo] -- os estados
    de todo são realmente os estados que restam ainda processar. Após estarem
    devidamente processados, passam para [final]
    Um dos invariantes mantidos é que os estados de [final] são todos atingíveis
    por [ch] a partir de um caminho que parte dos estados de [todo] da chamada inicial.
*)
let rec reach_star_aux ((transicoes,_,_) as maq:maquina) (final:estados) (todo:estados)  (ch:simbolo)=
  if Sestado.is_empty todo then final
  else
    let elt = Sestado.choose todo in
    let new_final = Sestado.add elt final in
    let new_todo = (Sestado.union  (Sestado.remove elt todo) (Sestado.diff (reach maq elt ch) new_final)) in
    reach_star_aux maq new_final new_todo ch

(** [reach_star] calcula que estados são alvo de transições directas e indirectas (i.e. uma ou mais)
    que partem do conjunto de estados [states] com rótulo [ch] no autómato [maquina]*)
let reach_star  (maq:maquina) (states:estados) (ch:simbolo) =
  reach_star_aux maq  Sestado.empty states ch


(** [reach_epsilon] devolve o conjunto de estados para os quais existe um caminho "epsilon"
    que parte dos estados de [states] -- i.e. os estados atingíveis por epsilon
    partindo de [states] *)
let reach_epsilon maq states =  reach_star maq states epsilon


(**
    [next] calcula os estados atingíveis a partir dos estados em [states]
    com o simbolo [simb], combinado com os estados atingíveis por
    transições epsilon a partir daí.
    se não houver estados atingidos, damos a indicação de que se
    terminou a execução
*)
let next ((transicoes,b,c) as maquina) ((states, restante) as config) simb=
  let res =  reach_epsilon maquina (reach_states maquina states simb)  in
  if (Sestado.is_empty res) then raise (FIM config) else res

(**
   [step] realiza um passo de execução do autómato [maquina] a partir da configuração [config].
   se não resta elementos na fita de entrada então damos a indicação de que terminou a execução,
   senão devolvemos a configuração seguinte (considerando o autómato [maquina] e a
   configuração config=(states, a.w):

    (states, a.w) |-'  (states', w)

   em que states' =  (next  maquina config)
*)
let step  ((transicoes,b,c) as maquina) ((states, restante) as config)=
  match restante with
      [] ->  raise (FIM config)
    | a::w ->  (next  maquina config a,w)

(** [step_star] é a função de execução principal. executa repetidamente [step] a partir de uma dada configuração.
    Espera-se que esta seja invocada com a configuração inicial (estendida com todos os estados atingíveis
    com transições epsilon dos estados iniciais)
*)
let rec step_star (maq:maquina) (config:configuracao) =
  step_star maq (step maq config)

(** [is_accepted] é um predicado que detecta se uma configuração
    da execução do autómato (ambos passados em parâmetro) prefigura a aceitação.
    Ou seja o buffer de entrada encontra-se vazio e há pelo menos um estado final na
    configuração
*)
let is_accepted  ((_,_,accept):maquina)  (laqui, restante) =
  restante=[] && not (Sestado.is_empty (Sestado.inter accept laqui))


(** a função [print_output] analisa a configuração final e imprime na
    saída standard o veredicto. *)
let print_output (maq:maquina) (config:configuracao)=
  (if (is_accepted maq config) then "YES" else "NO") |> print_endline


(** [main] função principal *)
let main () =
  let dados,((a,b,c) as maquina) = leitura () in
  try
    step_star maquina ((reach_epsilon maquina b),dados)
  with  FIM x -> print_output maquina x



(*  executa. *)
let () = main ()



(** {1 epílogo}

Exemplo de entrada:

{v a a b a
0
1 2
0 a 0
0 b 1
0 a 3
1 a 2
2 a 3
3 a 1
3 a 2 v}


Resposta:

{v YES v}
*)