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 : 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 *)
75 module TransList : sig
76 include Hlist.S with type elt = Transition.t
77 val print : Format.formatter -> ?sep:string -> t -> unit
79 (** Hashconsed lists of transitions, with a printing facility *)
83 (** 2-way Selecting Alternating Tree Automata *)
85 val get_states : t -> StateSet.t
86 (** return the set of states of the automaton *)
88 val get_starting_states : t -> StateSet.t
89 (** return the set of starting states of the automaton *)
91 val get_selecting_states : t -> StateSet.t
92 (** return the set of selecting states of the automaton *)
94 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
95 (** [get_trans auto l q] return the list of transitions taken by [auto]
96 for label [l] in state [q]. Takes time proportional to the number of
97 transitions in the automaton.
100 val print : Format.formatter -> t -> unit
101 (** Pretty printing of the automaton *)
107 (** Alias type for the automata type *)
110 (** Abstract type for a builder *)
113 (** Create a fresh builder *)
115 val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
116 (** Add a state to the set of states of the automaton. The
117 optional arguments [?starting] and [?selecting] (defaulting
118 to [false]) allow one to specify whether the state is
119 starting/selecting. *)
121 val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
122 (** Add a transition to the automaton *)
124 val finalize : t -> auto
125 (** Finalize the automaton and return it. Clean-up unused states (states that
126 do not occur in any transitions and remove instantes of negative [move] atoms
127 by creating fresh states that accept the complement of the negated state.
130 (** Builder facility for the automaton *)