1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
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 *)
14 (***********************************************************************)
16 (** Implementation of 2-way Selecting Alternating Tree Automata *)
19 type move = [ `First_child
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
39 (** Type of moves an automaton can perform *)
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 *)
55 include Hcons.S with type data = predicate
56 include Common_sig.Printable with type t := t
58 (** Module representing atoms of Boolean formulae, which are simply
59 hashconsed [predicate]s *)
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 *)
83 val is_processing_instruction : t
85 (** [is_attribute], [is_element], [is_processing_instruction],
86 [is_comment] are constant formulae that tests a particular
88 val get_states : t -> StateSet.t
89 (** [get_state f] retrieves all the states occuring in [move]
91 val get_states_by_move : t -> StateSet.t Move.table
93 (** Modules representing the Boolean formulae used in transitions *)
95 module Transition : sig
96 include Hcons.S with type data = State.t * QNameSet.t * Formula.t
97 val print : Format.formatter -> t -> unit
99 (** A [Transition.t] is a hashconsed triple of the state, the set of
100 labels and the formula *)
103 module TransList : sig
104 include Hlist.S with type elt = Transition.t
105 val print : Format.formatter -> ?sep:string -> t -> unit
107 (** Hashconsed lists of transitions, with a printing facility *)
111 (** 2-way Selecting Alternating Tree Automata *)
114 (** return the internal unique ID of the automaton *)
116 val get_states : t -> StateSet.t
117 (** return the set of states of the automaton *)
119 val get_starting_states : t -> StateSet.t
120 (** return the set of starting states of the automaton *)
122 val get_selecting_states : t -> StateSet.t
123 (** return the set of selecting states of the automaton *)
125 val get_states_by_rank : t -> StateSet.t array
126 (** return an array of states ordered by ranks.
129 val get_max_rank : t -> int
130 (** return the maximal rank of a state in the automaton, that is the
131 maximum number of runs needed to fuly evaluate the automaton.
134 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
135 (** [get_trans auto l q] returns the list of transitions taken by [auto]
136 for label [l] in state [q]. Takes time proportional to the number of
137 transitions in the automaton.
140 val get_form : t -> QNameSet.elt -> State.t -> Formula.t
141 (** [get_form auto l q] returns a single formula for label [l] in state [q].
142 Takes time proportional to the number of transitions in the automaton.
144 val state_prerequisites : move -> t -> State.t -> StateSet.t
145 (** [state_prerequisites m auto q] returns the set of all states q' such
146 that [q', _ -> phi] and [m(q)] is in phi
149 val print : Format.formatter -> t -> unit
150 (** Pretty printing of the automaton *)
153 (** [copy a] creates a copy of automaton [a], that is a new automaton with
154 the same transitions but with fresh states, such that [get_states a] and
155 [get_states (copy a)] are distinct
157 val concat : t -> t -> t
158 (** [concat a a'] creates a new automaton [a''] such that, given a set of tree
159 nodes [N], [a'' N = a' (a N)].
162 val merge : t -> t -> t
163 (** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
167 val union : t -> t -> t
168 (** [union a a'] creates a new automaton [a''] that selects nodes
169 selected by either [a] or [a']
172 val inter : t -> t -> t
173 (** [inter a a'] creates a new automaton [a''] that selects nodes
174 selected both by [a] and [a']
178 (** [neg a] creates a new automaton [a'] that selects the nodes not
182 val diff : t -> t -> t
183 (** [diff a a'] creates a new automaton [a''] that select nodes selected
184 by [a] but not selected by [a']
190 (** Alias type for the automata type *)
193 (** Abstract type for a builder *)
196 (** Create a fresh builder *)
198 val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
199 (** Add a state to the set of states of the automaton. The
200 optional arguments [?starting] and [?selecting] (defaulting
201 to [false]) allow one to specify whether the state is
202 starting/selecting. *)
204 val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
205 (** Add a transition to the automaton *)
207 val finalize : t -> auto
208 (** Finalize the automaton and return it. Clean-up unused states
209 (states that do not occur in any transitions and remove
210 instances of negative [move] atoms by creating fresh states
211 that accept the complement of the negated state. *)
213 (** Builder facility for the automaton *)