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 exists : (t -> 'a -> bool) -> 'a table -> bool
38 (** Type of moves an automaton can perform *)
41 Move of move * State.t (** In the [move] direction, the automaton must be in the given state *)
42 | Is_first_child (** True iff the node is the first child of its parent *)
43 | Is_next_sibling (** True iff the node is the next sibling of its parent *)
44 | Is of Tree.NodeKind.t (** True iff the node is of the given kind *)
45 | Has_first_child (** True iff the node has a first child *)
46 | Has_next_sibling (** True iff the node has a next sibling *)
47 (** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
50 include Hcons.S with type data = predicate
51 include Common_sig.Printable with type t:= t
53 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
57 include module type of Boolean.Make(Atom)
58 val first_child : State.t -> t
59 val next_sibling : State.t -> t
60 val parent : State.t -> t
61 val previous_sibling : State.t -> t
62 val stay : State.t -> t
63 (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
64 of the corresponding [move] atom. *)
65 val is_first_child : t
66 val is_next_sibling : t
67 val has_first_child : t
68 val has_next_sibling : t
69 (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
70 only of the corresponding atom
72 val is : Tree.NodeKind.t -> t
73 (** [is k] creates a formula that tests the kind of the current node *)
76 val is_processing_instruction : t
78 (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
80 val get_states : t -> StateSet.t
81 (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
82 val get_states_by_move : t -> StateSet.t Move.table
84 (** Modules representing the Boolean formulae used in transitions *)
86 module Transition : sig
87 include Hcons.S with type data = State.t * QNameSet.t * Formula.t
88 val print : Format.formatter -> t -> unit
90 (** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
93 module TransList : sig
94 include Hlist.S with type elt = Transition.t
95 val print : Format.formatter -> ?sep:string -> t -> unit
97 (** Hashconsed lists of transitions, with a printing facility *)
101 (** 2-way Selecting Alternating Tree Automata *)
104 (** return the internal unique ID of the automaton *)
106 val get_states : t -> StateSet.t
107 (** return the set of states of the automaton *)
109 val get_starting_states : t -> StateSet.t
110 (** return the set of starting states of the automaton *)
112 val get_selecting_states : t -> StateSet.t
113 (** return the set of selecting states of the automaton *)
115 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
116 (** [get_trans auto l q] returns the list of transitions taken by [auto]
117 for label [l] in state [q]. Takes time proportional to the number of
118 transitions in the automaton.
121 val get_form : t -> QNameSet.elt -> State.t -> Formula.t
122 (** [get_form auto l q] returns a single formula for label [l] in state [q].
123 Takes time proportional to the number of transitions in the automaton.
126 val print : Format.formatter -> t -> unit
127 (** Pretty printing of the automaton *)
130 (** [copy a] creates a copy of automaton [a], that is a new automaton with
131 the same transitions but with fresh states, such that [get_states a] and
132 [get_states (copy a)] are distinct
134 val concat : t -> t -> t
135 (** [concat a a'] creates a new automaton [a''] such that, given a set of tree
136 nodes [N], [a'' N = a' (a N)].
139 val merge : t -> t -> t
140 (** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
144 val union : t -> t -> t
145 (** [union a a'] creates a new automaton [a''] that selects node
146 selected by either [a] or [a']
149 val inter : t -> t -> t
150 (** [inter a a'] creates a new automaton [a''] that selects node
151 selected by both [a] and [a']
155 (** [neg a] creates a new automaton [a'] that selects the nodes not
159 val diff : t -> t -> t
160 (** [diff a a'] creates a new automaton [a''] that select nodes selected
161 by [a] but not selected by [a']
167 (** Alias type for the automata type *)
170 (** Abstract type for a builder *)
173 (** Create a fresh builder *)
175 val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
176 (** Add a state to the set of states of the automaton. The
177 optional arguments [?starting] and [?selecting] (defaulting
178 to [false]) allow one to specify whether the state is
179 starting/selecting. *)
181 val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
182 (** Add a transition to the automaton *)
184 val finalize : t -> auto
185 (** Finalize the automaton and return it. Clean-up unused states (states that
186 do not occur in any transitions and remove instantes of negative [move] atoms
187 by creating fresh states that accept the complement of the negated state.
190 (** Builder facility for the automaton *)