(***********************************************************************)
(*                                                                     *)
(*                               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 = ()