Add a 'trace' mode (must be enabled at build time) that saves the

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

diff --git a/src/auto/ata.ml b/src/auto/ata.ml
index 9e5e57f..1015513 100644 (file)
--- a/src/auto/ata.ml
+++ b/src/auto/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 18:31:19 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-14 19:14:03 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -161,7 +161,17 @@ module Transition = Hcons.Make (struct
     HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int))
 end)
 
-module TransList : Hlist.S with type elt = Transition.t = Hlist.Make(Transition)
+module TransList : sig
+  include Hlist.S with type elt = Transition.t
+  val print : Format.formatter -> t -> unit
+end =
+  struct
+    include Hlist.Make(Transition)
+    let print ppf l =
+      iter (fun t ->
+        let q, lab, f = Transition.node t in
+        fprintf ppf "%a, %a -> %a<br/>" State.print q QNameSet.print lab SFormula.print f) l
+  end
 
 let get_trans a states tag =
   StateSet.fold (fun q acc0 ->