1 (***********************************************************************)
8 (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
16 (** Implementation of alternating selecting tree automata (ASTA) *)
20 (** The type of states *)
23 (** The type of labels of the transitions *)
26 (** The type of transition formulae *)
29 (** The type of ASTAs *)
31 val transition : t -> state -> label -> formula
32 (** Give the formula which must hold for a current state and label *)
34 val transitions : t -> state -> (label*formula) list
35 (** Give the list of labels and formulae from transitions for a given state *)
38 (** The empty automaton *)
40 val print : Format.formatter -> t -> unit
41 (** Describe the automaton as text *)
43 val to_file : out_channel -> t -> unit
44 (** Outputs the description of the automaton on the given out_channel *)