X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fata.ml;h=1015513f2563db0d5ebc669c5d47681c3a8f3004;hp=9e5e57f89d46f98b0799f8c72dccce1e0eff4fc9;hb=ce09a30489dce8ac9e389c8c1525a34d1e02354e;hpb=3b653edd20248b66a005637c2b1e217042cef62b diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 9e5e57f..1015513 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) 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
" State.print q QNameSet.print lab SFormula.print f) l + end let get_trans a states tag = StateSet.fold (fun q acc0 ->