(* *)
(* TAToo *)
(* *)
-(* Lucca Hirschi, ? *)
-(* ? *)
+(* Lucca Hirschi, ? *)
+(* ? *)
(* *)
(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
(* Recherche Scientifique. All rights reserved. This file is *)
(** Implementation of alternating selecting tree automata (ASTA) *)
-type state
+type state = State.t
(** The type of states *)
-type label
+type label = QNameSet.t
(** The type of labels of the transitions *)
-type formula
+type formula = Formula.t
(** The type of transition formulae *)
+type transition = (state*label*formula)
+(** The type of transitions *)
+
type t
(** The type of ASTAs *)
val transitions : t -> state -> (label*formula) list
(** Give the list of labels and formulae from transitions for a given state *)
-val dummy : t
+val empty : t
(** The empty automaton *)
+val any_label : label
+(** Set of all labels which can occur in a tree *)
+
+val new_state : unit -> state
+(** Give a new state (different from all others states) *)
+
+val add_tr : t -> transition -> unit
+(** Add a transition to an asta *)
+
+val add_reco : t -> state -> unit
+(** Add a state to the recognizing states of an asta *)
+
+val add_selec : t -> state -> unit
+(** Add a state to the recognizing states of an asta *)
+
+val add_bot : t -> state -> unit
+(** Add a state to the bottom states of an asta *)
+
+val add_top : t -> state -> unit
+(** Add a state to the top states of an asta *)
+
+val top_states : t -> state list
+(** Give the list of top states of an ASTA *)
+
val print : Format.formatter -> t -> unit
(** Describe the automaton as text *)