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
  25 module Move :
  26   sig
  27     type t = move
  28     type 'a table
  29     val create_table : 'a -> 'a table
  30     val get : 'a table -> t -> 'a
  31     val set : 'a table -> t -> 'a -> unit
  32     val iter : (t -> 'a -> unit) -> 'a table -> unit
  33     val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
  34     val for_all : (t -> 'a -> bool) -> 'a table -> bool
  35     val for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool
  36     val exists : (t -> 'a -> bool) -> 'a table -> bool
  37   end
  38
  39 (** Type of moves an automaton can perform *)
  40
  41 type predicate =
  42     Move of move * State.t  (** In the [move] direction,
  43                                 the automaton must be in the given state *)
  44   | Is_first_child          (** True iff
  45                                 the node is the first child of its parent *)
  46   | Is_next_sibling         (** True iff
  47                                 the node is the next sibling of its parent *)
  48   | Is of Tree.NodeKind.t   (** True iff the node is of the given kind *)
  49   | Has_first_child         (** True iff the node has a first child *)
  50   | Has_next_sibling        (** True iff the node has a next sibling *)
  51 (** Type of the predicates that can occur in the Boolean formulae that
  52     are in the transitions of the automaton *)
  53
  54 module Atom : sig
  55   include Hcons.S with type data = predicate
  56   include Common_sig.Printable with type t := t
  57 end
  58 (** Module representing atoms of Boolean formulae, which are simply
  59     hashconsed [predicate]s *)
  60
  61 module Formula :
  62   sig
  63     include module type of Boolean.Make(Atom)
  64     val first_child : State.t -> t
  65     val next_sibling : State.t -> t
  66     val parent : State.t -> t
  67     val previous_sibling : State.t -> t
  68     val stay : State.t -> t
  69     (** [first_child], [next_sibling], [parent], [previous_sibling],
  70         [stay] create a formula which consists only of the
  71         corresponding [move] atom. *)
  72     val is_first_child : t
  73     val is_next_sibling : t
  74     val has_first_child : t
  75     val has_next_sibling : t
  76     (** [is_first_child], [is_next_sibling], [has_first_child],
  77         [has_next_sibling] are constant formulae which consist only
  78         of the corresponding atom *)
  79     val is : Tree.NodeKind.t -> t
  80       (** [is k] creates a formula that tests the kind of the current node *)
  81     val is_attribute : t
  82     val is_element : t
  83     val is_processing_instruction : t
  84     val is_comment : t
  85     (** [is_attribute], [is_element], [is_processing_instruction],
  86         [is_comment] are constant formulae that tests a particular
  87         kind *)
  88     val get_states : t -> StateSet.t
  89     (** [get_state f] retrieves all the states occuring in [move]
  90         predicates in [f] *)
  91     val get_states_by_move : t -> StateSet.t Move.table
  92   end
  93 (** Modules representing the Boolean formulae used in transitions *)
  94
  95 module Transition : sig
  96   include Hcons.S with type data = State.t * QNameSet.t * Formula.t
  97   val print : Format.formatter -> t -> unit
  98 end
  99 (** A [Transition.t] is a hashconsed triple of the state, the set of
 100     labels and the formula *)
 101
 102
 103 module TransList : sig
 104   include Hlist.S with type elt = Transition.t
 105   val print : Format.formatter -> ?sep:string -> t -> unit
 106 end
 107 (** Hashconsed lists of transitions, with a printing facility *)
 108
 109
 110 type t
 111 (** 2-way Selecting Alternating Tree Automata *)
 112
 113 val uid : t -> Uid.t
 114 (** return the internal unique ID of the automaton *)
 115
 116 val get_states : t -> StateSet.t
 117 (** return the set of states of the automaton *)
 118
 119 val get_starting_states : t -> StateSet.t
 120 (** return the set of starting states of the automaton *)
 121
 122 val get_selecting_states : t -> StateSet.t
 123 (** return the set of selecting states of the automaton *)
 124
 125 type rank = { td : StateSet.t;
 126               bu : StateSet.t;
 127               exit : StateSet.t }
 128
 129 val get_states_by_rank : t -> rank array
 130 (** return an array of states (sources, states) ordered by ranks.
 131 *)
 132
 133 val get_max_rank : t -> int
 134 (** return the maximal rank of a state in the automaton, that is the
 135     maximum number of runs needed to fuly evaluate the automaton.
 136 *)
 137
 138 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 139 (** [get_trans auto l q] returns the list of transitions taken by [auto]
 140     for label [l] in state [q]. Takes time proportional to the number of
 141     transitions in the automaton.
 142  *)
 143
 144 val get_form : t -> QNameSet.elt -> State.t -> Formula.t
 145 (** [get_form auto l q] returns a single formula for label [l] in state [q].
 146     Takes time proportional to the number of transitions in the automaton.
 147  *)
 148 val state_prerequisites : move -> t -> State.t -> StateSet.t
 149 (** [state_prerequisites m auto q] returns the set of all states q' such
 150     that [q', _ -> phi] and [m(q)] is in phi
 151 *)
 152
 153 val print : Format.formatter -> t -> unit
 154 (** Pretty printing of the automaton *)
 155
 156 val copy : t -> t
 157 (** [copy a] creates a copy of automaton [a], that is a new automaton with
 158     the same transitions but with fresh states, such that [get_states a] and
 159     [get_states (copy a)] are distinct
 160 *)
 161 val concat : t -> t -> t
 162 (** [concat a a'] creates a new automaton [a''] such that, given a set of tree
 163     nodes [N], [a'' N = a' (a N)].
 164 *)
 165
 166 val merge : t -> t -> t
 167 (** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
 168     in parallel
 169 *)
 170
 171 val union : t -> t -> t
 172 (** [union a a'] creates a new automaton [a''] that selects node
 173     selected by either [a] or [a']
 174 *)
 175
 176 val inter : t -> t -> t
 177 (** [inter a a'] creates a new automaton [a''] that selects node
 178     selected by both [a] and [a']
 179 *)
 180
 181 val neg : t -> t
 182 (** [neg a] creates a new automaton [a'] that selects the nodes not
 183     selected by [a]
 184 *)
 185
 186 val diff : t -> t -> t
 187 (** [diff a a'] creates a new automaton [a''] that select nodes selected
 188     by [a] but not selected by [a']
 189 *)
 190
 191 module Builder :
 192 sig
 193   type auto = t
 194     (** Alias type for the automata type *)
 195
 196   type t
 197     (** Abstract type for a builder *)
 198
 199   val make : unit -> t
 200     (** Create a fresh builder *)
 201
 202   val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
 203   (** Add a state to the set of states of the automaton. The
 204       optional arguments [?starting] and [?selecting] (defaulting
 205       to [false]) allow one to specify whether the state is
 206       starting/selecting. *)
 207
 208   val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
 209     (** Add a transition to the automaton *)
 210
 211   val finalize : t  -> auto
 212 (** Finalize the automaton and return it. Clean-up unused states
 213     (states that do not occur in any transitions and remove
 214     instantes of negative [move] atoms by creating fresh states
 215     that accept the complement of the negated state.  *)
 216 end
 217   (** Builder facility for the automaton *)