From f4eb8149f6cdec4f56c4947690e0aa8ce2ff17c2 Mon Sep 17 00:00:00 2001
From: Lucca Hirschi <lucca.hirschi@gmail.com>
Date: Fri, 29 Jun 2012 17:10:18 +0200
Subject: [PATCH] implem asta

---
 src/asta.ml  | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/asta.mli | 40 ++++++++++++++++++++++++++++
 2 files changed, 113 insertions(+)
 create mode 100644 src/asta.ml
 create mode 100644 src/asta.mli

diff --git a/src/asta.ml b/src/asta.ml
new file mode 100644
index 0000000..4e53bcd
--- /dev/null
+++ b/src/asta.ml
@@ -0,0 +1,73 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               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 = ()
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 *)
-- 
2.17.1