--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(***********************************************************************)
+
+open Format
+
+type state = State.t
+
+type label = QNameSet.t
+
+type formula = Formula.t
+
+module Transition =
+struct
+ type t = state * label * formula
+
+ let compare (st,la,f) (st',la',f') =
+ let x_1 = State.compare st st' in
+ if x_1 != 0 then x_1
+ else let x_2 = QNameSet.compare la la' in
+ if x_2 != 0 then x_2
+ else Formula.compare f f'
+ let st (st,la,f) = st
+ let la (st,la,f) = la
+ let fo (st,la,f) = f
+end
+
+module SetT =
+struct
+ include Set.Make(Transition)
+end
+
+type t = {
+ reco : StateSet.t;
+ selec : StateSet.t;
+ bottom : StateSet.t;
+ top : StateSet.t;
+ trans : SetT.t;
+}
+
+exception Not_found_transition
+exception Transition_not_injective
+
+let transition asta st lab =
+ let filter (s,l,f) =
+ (State.compare s st = 0) && (QNameSet.compare l lab = 0) in
+ let tr_set = SetT.elements (SetT.filter filter asta.trans) in
+ match tr_set with
+ | [] -> raise Not_found_transition
+ | x::y::z -> raise Transition_not_injective
+ | [l] -> Transition.fo l
+
+let transitions asta st =
+ let filter (s,l,f) = State.compare s st = 0 in
+ let rec remove_states l = match l with
+ | [] -> []
+ | (a,s,l) :: tl -> (s,l) :: (remove_states tl) in
+ remove_states (SetT.elements (SetT.filter filter asta.trans))
+
+let print fmt asta = ()
+
+let to_file out asta = ()
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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 *)