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) *)
19 (** The type of states *)
22 (** The type of labels of the transitions *)
25 (** The type of transition formulae *)
28 (** The type of ASTAs *)
30 val transition : t -> state -> label -> formula
31 (** Give the formula which must hold for a current state and label *)
33 val transitions : t -> state -> (label*formula) list
34 (** Give the list of labels and formulae from transitions for a given state *)
36 val print : Format.formatter -> t -> unit
37 (** Describe the automaton as text *)
39 val to_file : out_channel -> t -> unit
40 (** Outputs the description of the automaton on the given out_channel *)