From e3ad6d6f098809af95ddaf8b1e9bc4ec5cb7b0f4 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kim.nguyen@lri.fr>
Date: Mon, 3 Apr 2017 11:17:25 +0200
Subject: [PATCH] Implement automaton simplification.

---
 src/ata.ml  | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++--
 src/ata.mli |  2 +-
 2 files changed, 56 insertions(+), 3 deletions(-)

diff --git a/src/ata.ml b/src/ata.ml
index c045aaf..7b0dff4 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -176,6 +176,15 @@ struct
     let table = get_states_by_move phi in
     Move.fold (fun _ s acc -> StateSet.union s acc) table StateSet.empty
 
+  let rec rename_state phi qfrom qto =
+    let open Boolean in
+    match expr phi with
+      False | True -> phi
+    | Or (phi1, phi2) -> or_ (rename_state phi1 qfrom qto)  (rename_state phi2 qfrom qto)
+    | And (phi1, phi2) ->  and_ (rename_state phi1 qfrom qto)  (rename_state phi2 qfrom qto)
+    | Atom ({ Atom.node = Move(m, q); }, b) when q == qfrom ->
+      let atm = mk_move m qto in if b then atm else not_ atm
+    | Atom _ -> phi
 end
 
 module Transition =
@@ -417,6 +426,47 @@ let normalize_negations auto =
   done;
   cleanup_states auto
 
+exception Found of State.t * State.t
+
+let simplify_epsilon auto =
+  let rec loop old_states =
+    if old_states != auto.states then begin
+      let old_states = auto.states in
+      try
+        Hashtbl.iter
+          (fun qfrom v -> match v with
+               [ (labels, phi) ] ->
+               if labels == QNameSet.any then begin
+                 match (Formula.expr phi) with
+                   Boolean.Atom ( {Atom.node = Move(`Stay, qto); _ }, true) -> raise (Found (qfrom, qto))
+                 | _ -> ()
+               end
+             | _ -> ()
+          ) auto.transitions
+      with Found (qfrom, qto) ->
+        Hashtbl.remove auto.transitions qfrom;
+        let new_trans = Hashtbl.fold (fun q tr_lst acc ->
+            let new_tr_lst =
+              List.map (fun (lab, phi) ->
+                  (lab, Formula.rename_state phi qfrom qto))
+                tr_lst
+            in
+            (q, new_tr_lst) :: acc) auto.transitions []
+        in
+        Hashtbl.reset auto.transitions;
+        List.iter (fun (q, l) -> Hashtbl.add auto.transitions q l) new_trans;
+        auto.states <- StateSet.remove qfrom auto.states;
+        if (StateSet.mem qfrom auto.starting_states) then
+          auto.starting_states <- StateSet.add qto (StateSet.remove qfrom auto.starting_states);
+        if (StateSet.mem qfrom auto.selecting_states) then
+          auto.selecting_states <- StateSet.add qto (StateSet.remove qfrom auto.selecting_states);
+        loop old_states
+    end
+  in
+  loop StateSet.empty
+
+
+
 (* [compute_dependencies auto] returns a hash table storing for each
    states [q] a Move.table containing the set of states on which [q]
    depends (loosely). [q] depends on [q'] if there is a transition
@@ -496,8 +546,8 @@ let compute_rank auto =
   done;
   let by_rank = Hashtbl.create 17 in
   List.iter (fun (r,s) ->
-    let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
-    Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
+      let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
+      Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
   auto.ranked_states <-
     Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i)
 
@@ -550,9 +600,12 @@ module Builder =
       in
       Hashtbl.replace a.transitions q ntrs
 
+
+
     let finalize a =
       complete_transitions a;
       normalize_negations a;
+      simplify_epsilon a;
       compute_rank a;
       a
   end
diff --git a/src/ata.mli b/src/ata.mli
index 54ed1b4..1f8e863 100644
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -207,7 +207,7 @@ sig
   val finalize : t  -> auto
 (** Finalize the automaton and return it. Clean-up unused states
     (states that do not occur in any transitions and remove
-    instantes of negative [move] atoms by creating fresh states
+    instances of negative [move] atoms by creating fresh states
     that accept the complement of the negated state.  *)
 end
   (** Builder facility for the automaton *)
-- 
2.17.1