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
24 (** Type of moves an automaton can perform *)
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 *)
36 include Hcons.S with type data = predicate
37 include Common_sig.Printable with type t:= t
39 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
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
58 val is : Tree.NodeKind.t -> t
59 (** [is k] creates a formula that tests the kind of the current node *)
62 val is_processing_instruction : t
64 (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
66 val get_states : t -> StateSet.t
67 (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
69 (** Modules representing the Boolean formulae used in transitions *)
71 module Transition : sig
72 include Hcons.S with type data = State.t * QNameSet.t * Formula.t
73 val print : Format.formatter -> t -> unit
75 (** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
78 module TransList : sig
79 include Hlist.S with type elt = Transition.t
80 val print : Format.formatter -> ?sep:string -> t -> unit
82 (** Hashconsed lists of transitions, with a printing facility *)
86 (** 2-way Selecting Alternating Tree Automata *)
89 (** return the internal unique ID of the automaton *)
91 val get_states : t -> StateSet.t
92 (** return the set of states of the automaton *)
94 val get_starting_states : t -> StateSet.t
95 (** return the set of starting states of the automaton *)
97 val get_selecting_states : t -> StateSet.t
98 (** return the set of selecting states of the automaton *)
100 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
101 (** [get_trans auto l q] returns the list of transitions taken by [auto]
102 for label [l] in state [q]. Takes time proportional to the number of
103 transitions in the automaton.
106 val get_form : t -> QNameSet.elt -> State.t -> Formula.t
107 (** [get_form auto l q] returns a single formula for label [l] in state [q].
108 Takes time proportional to the number of transitions in the automaton.
111 val print : Format.formatter -> t -> unit
112 (** Pretty printing of the automaton *)
115 (** [copy a] creates a copy of automaton [a], that is a new automaton with
116 the same transitions but with fresh states, such that [get_states a] and
117 [get_states (copy a)] are distinct
119 val concat : t -> t -> t
120 (** [concat a a'] creates a new automaton [a''] such that, given a set of tree
121 nodes [N], [a'' N = a' (a N)].
124 val merge : t -> t -> t
125 (** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
132 (** Alias type for the automata type *)
135 (** Abstract type for a builder *)
138 (** Create a fresh builder *)
140 val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
141 (** Add a state to the set of states of the automaton. The
142 optional arguments [?starting] and [?selecting] (defaulting
143 to [false]) allow one to specify whether the state is
144 starting/selecting. *)
146 val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
147 (** Add a transition to the automaton *)
149 val finalize : t -> auto
150 (** Finalize the automaton and return it. Clean-up unused states (states that
151 do not occur in any transitions and remove instantes of negative [move] atoms
152 by creating fresh states that accept the complement of the negated state.
155 (** Builder facility for the automaton *)