X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;ds=sidebyside;f=src%2Fasta.mli;fp=src%2Fasta.mli;h=76957e61c35a94c40ddd0e6d8c223a0c714e7cad;hb=f4eb8149f6cdec4f56c4947690e0aa8ce2ff17c2;hp=0000000000000000000000000000000000000000;hpb=e2dce9a8858c17d907ddecc34cd939905a73f0cc;p=tatoo.git

diff --git a/src/asta.mli b/src/asta.mli
new file mode 100644
index 0000000..76957e6
--- /dev/null
+++ b/src/asta.mli
@@ -0,0 +1,40 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                  ?   *)
+(*                  ?   *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Implementation of alternating selecting tree automata (ASTA) *)
+
+type state
+(** The type of states *)
+
+type label
+(** The type of labels of the transitions *)
+
+type formula
+(** The type of transition formulae *)
+
+type t
+(** The type of ASTAs *)
+
+val transition : t -> state -> label -> formula
+(** Give the formula which must hold for a current state and label *)
+
+val transitions : t -> state -> (label*formula) list
+(** Give the list of labels and formulae from transitions for a given state *)
+
+val print : Format.formatter -> t -> unit
+(** Describe the automaton as text *)
+
+val to_file : out_channel -> t -> unit
+(** Outputs the description of the automaton on the given out_channel *)