src/ata.mli

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2013 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   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 (** Implementation of 2-way Selecting Alternating Tree Automata *)
  17
  18
  19 type move = [ `First_child
  20             | `Next_sibling
  21             | `Parent
  22             | `Previous_sibling
  23             | `Stay ]
  24 (** Type of moves an automaton can perform *)
  25
  26 type predicate =
  27     Move of move * State.t  (** In the [move] direction, the automaton must be in the given state *)
  28   | Is_first_child          (** True iff the node is the first child of its parent *)
  29   | Is_next_sibling         (** True iff the node is the next sibling of its parent *)
  30   | Is of Tree.NodeKind.t   (** True iff the node is of the given kind *)
  31   | Has_first_child         (** True iff the node has a first child *)
  32   | Has_next_sibling        (** True iff the node has a next sibling *)
  33 (** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
  34
  35 module Atom : sig
  36   include Hcons.S with type data = predicate
  37   include Common_sig.Printable with type t:= t
  38 end
  39 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
  40
  41 module Formula :
  42   sig
  43     include module type of Boolean.Make(Atom)
  44     val first_child : State.t -> t
  45     val next_sibling : State.t -> t
  46     val parent : State.t -> t
  47     val previous_sibling : State.t -> t
  48     val stay : State.t -> t
  49       (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
  50           of the corresponding [move] atom. *)
  51     val is_first_child : t
  52     val is_next_sibling : t
  53     val has_first_child : t
  54     val has_next_sibling : t
  55       (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
  56           only of the corresponding atom
  57       *)
  58     val is : Tree.NodeKind.t -> t
  59       (** [is k] creates a formula that tests the kind of the current node *)
  60     val is_attribute : t
  61     val is_element : t
  62     val is_processing_instruction : t
  63     val is_comment : t
  64       (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
  65           particular kind *)
  66     val get_states : t -> StateSet.t
  67       (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
  68   end
  69 (** Modules representing the Boolean formulae used in transitions *)
  70
  71 module Transition : Hcons.S with type data = State.t * QNameSet.t * Formula.t
  72 (** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
  73
  74
  75 module TransList : sig
  76   include Hlist.S with type elt = Transition.t
  77   val print : Format.formatter -> ?sep:string -> t -> unit
  78 end
  79 (** Hashconsed lists of transitions, with a printing facility *)
  80
  81
  82 type t
  83 (** 2-way Selecting Alternating Tree Automata *)
  84
  85 val get_states : t -> StateSet.t
  86 (** return the set of states of the automaton *)
  87
  88 val get_selecting_states : t -> StateSet.t
  89 (** return the set of selecting states of the automaton *)
  90
  91 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
  92 (** [get_trans auto l q] return the list of transitions taken by [auto]
  93     for label [l] in state [q]. Takes time proportional to the number of
  94     transitions in the automaton.
  95  *)
  96
  97 val print : Format.formatter -> t -> unit
  98 (** Pretty printing of the automaton *)
  99
 100
 101 module Builder :
 102 sig
 103   type auto = t
 104     (** Alias type for the automata type *)
 105
 106   type t
 107     (** Abstract type for a builder *)
 108
 109   val make : unit -> t
 110     (** Create a fresh builder *)
 111
 112   val add_state : t -> ?selecting:bool -> State.t -> unit
 113     (** Add a state to the set of states of the automaton. The optional argument
 114         [?selecting] (defaulting to [false]) allows to specify whether the state is
 115         selecting. *)
 116
 117   val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
 118     (** Add a transition to the automaton *)
 119
 120   val finalize : t  -> auto
 121     (** Finalize the automaton and return it. Clean-up unused states (states that
 122         do not occur in any transitions and remove instantes of negative [move] atoms
 123         by creating fresh states that accept the complement of the negated state.
 124     *)
 125 end
 126   (** Builder facility for the automaton *)