Implement runtime optimisation via Hashing of transitions.

[tatoo.git] / src / auto / ata.ml

diff --git a/src/auto/ata.ml b/src/auto/ata.ml
index 4418996..9e5e57f 100644 (file)
--- a/src/auto/ata.ml
+++ b/src/auto/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-11 00:14:28 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-13 18:31:19 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -153,14 +153,24 @@ let create () = { id = next ();
  }
 
 
+module Transition = Hcons.Make (struct
+  type t = State.t * QNameSet.t * SFormula.t
+  let equal (a, b, c) (d, e, f) =
+    a == d && b == e && c == f
+  let hash (a, b, c) =
+    HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int))
+end)
+
+module TransList : Hlist.S with type elt = Transition.t = Hlist.Make(Transition)
+
 let get_trans a states tag =
   StateSet.fold (fun q acc0 ->
     try
       let trs = Hashtbl.find a.transitions q in
       List.fold_left (fun acc1 (labs, phi) ->
-        if QNameSet.mem tag labs then (q,phi)::acc1 else acc1) acc0 trs
+        if QNameSet.mem tag labs then TransList.cons (Transition.make (q, labs, phi)) acc1 else acc1) acc0 trs
     with Not_found -> acc0
-  ) states []
+  ) states TransList.nil
 
 (*
   [add_trans a q labels f] adds a transition [(q,labels) -> f] to the