(* *)
(***********************************************************************)
-(*
- Time-stamp: <Last modified on 2013-04-25 15:15:01 CEST by Kim Nguyen>
-*)
+(** Implementation of 2-way Selecting Alternating Tree Automata *)
-type predicate =
- First_child
- | Next_sibling
- | Parent
- | Previous_sibling
- | Stay
- | Is_first_child
- | Is_next_sibling
- | Is of Tree.NodeKind.t
- | Has_first_child
- | Has_next_sibling
-val is_move : predicate -> bool
+type move = [ `First_child
+ | `Next_sibling
+ | `Parent
+ | `Previous_sibling
+ | `Stay ]
+
+module Move :
+ sig
+ type t = move
+ type 'a table
+ val create_table : 'a -> 'a table
+ val get : 'a table -> t -> 'a
+ val set : 'a table -> t -> 'a -> unit
+ val iter : (t -> 'a -> unit) -> 'a table -> unit
+ val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
+ val for_all : (t -> 'a -> bool) -> 'a table -> bool
+ val for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool
+ val exists : (t -> 'a -> bool) -> 'a table -> bool
+ end
-type atom = predicate * bool * State.t
+(** Type of moves an automaton can perform *)
-module Atom : Formula.ATOM with type data = atom
+type predicate =
+ Move of move * State.t (** In the [move] direction, the automaton must be in the given state *)
+ | Is_first_child (** True iff the node is the first child of its parent *)
+ | Is_next_sibling (** True iff the node is the next sibling of its parent *)
+ | Is of Tree.NodeKind.t (** True iff the node is of the given kind *)
+ | Has_first_child (** True iff the node has a first child *)
+ | Has_next_sibling (** True iff the node has a next sibling *)
+(** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
+
+module Atom : sig
+ include Hcons.S with type data = predicate
+ include Common_sig.Printable with type t := t
+end
+(** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
-module SFormula :
+module Formula :
sig
- include module type of Formula.Make(Atom)
- val mk_atom : predicate -> bool -> State.t -> t
- val mk_kind : Tree.NodeKind.t -> t
- val has_first_child : t
- val has_next_sibling : t
+ include module type of Boolean.Make(Atom)
+ val first_child : State.t -> t
+ val next_sibling : State.t -> t
+ val parent : State.t -> t
+ val previous_sibling : State.t -> t
+ val stay : State.t -> t
+ (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
+ of the corresponding [move] atom. *)
val is_first_child : t
val is_next_sibling : t
+ val has_first_child : t
+ val has_next_sibling : t
+ (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
+ only of the corresponding atom
+ *)
+ val is : Tree.NodeKind.t -> t
+ (** [is k] creates a formula that tests the kind of the current node *)
val is_attribute : t
val is_element : t
val is_processing_instruction : t
val is_comment : t
- val first_child : State.t -> t
- val next_sibling : State.t -> t
- val parent : State.t -> t
- val previous_sibling : State.t -> t
- val stay : State.t -> t
+ (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
+ particular kind *)
val get_states : t -> StateSet.t
+ (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
+ val get_states_by_move : t -> StateSet.t Move.table
end
+(** Modules representing the Boolean formulae used in transitions *)
+module Transition : sig
+ include Hcons.S with type data = State.t * QNameSet.t * Formula.t
+ val print : Format.formatter -> t -> unit
+end
+(** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
-module Transition : Hcons.S with
- type data = State.t * QNameSet.t * SFormula.t
module TransList : sig
include Hlist.S with type elt = Transition.t
val print : Format.formatter -> ?sep:string -> t -> unit
end
+(** Hashconsed lists of transitions, with a printing facility *)
+
+type t
+(** 2-way Selecting Alternating Tree Automata *)
-type node_summary = private int
-val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary
-val dummy_summary : node_summary
-type config = {
- sat : StateSet.t;
- unsat : StateSet.t;
- todo : TransList.t;
- summary : node_summary;
- mutable round : int;
-}
+val uid : t -> Uid.t
+(** return the internal unique ID of the automaton *)
-module Config : Hcons.S with type data = config
+val get_states : t -> StateSet.t
+(** return the set of states of the automaton *)
+val get_starting_states : t -> StateSet.t
+(** return the set of starting states of the automaton *)
-type t = private {
- id : Uid.t;
- mutable states : StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
- mutable cache2 : TransList.t Cache.N2.t;
- mutable cache4 : Config.t Cache.N4.t;
-}
+val get_selecting_states : t -> StateSet.t
+(** return the set of selecting states of the automaton *)
+val get_states_by_rank : t -> StateSet.t array
+(** return an array of states ordered by ranks.
+*)
+val get_max_rank : t -> int
+(** return the maximal rank of a state in the automaton, that is the
+ maximum number of runs needed to fuly evaluate the automaton.
+*)
-val create : StateSet.t -> StateSet.t -> t
-val reset : t -> unit
-val full_reset : t -> unit
val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
+(** [get_trans auto l q] returns the list of transitions taken by [auto]
+ for label [l] in state [q]. Takes time proportional to the number of
+ transitions in the automaton.
+ *)
+val get_form : t -> QNameSet.elt -> State.t -> Formula.t
+(** [get_form auto l q] returns a single formula for label [l] in state [q].
+ Takes time proportional to the number of transitions in the automaton.
+ *)
-val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
-
-val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
val print : Format.formatter -> t -> unit
-val complete_transitions : t -> unit
-val cleanup_states : t -> unit
-val normalize_negations : t -> unit
+(** Pretty printing of the automaton *)
+
+val copy : t -> t
+(** [copy a] creates a copy of automaton [a], that is a new automaton with
+ the same transitions but with fresh states, such that [get_states a] and
+ [get_states (copy a)] are distinct
+*)
+val concat : t -> t -> t
+(** [concat a a'] creates a new automaton [a''] such that, given a set of tree
+ nodes [N], [a'' N = a' (a N)].
+*)
+
+val merge : t -> t -> t
+(** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
+ in parallel
+*)
+
+val union : t -> t -> t
+(** [union a a'] creates a new automaton [a''] that selects node
+ selected by either [a] or [a']
+*)
+
+val inter : t -> t -> t
+(** [inter a a'] creates a new automaton [a''] that selects node
+ selected by both [a] and [a']
+*)
+
+val neg : t -> t
+(** [neg a] creates a new automaton [a'] that selects the nodes not
+ selected by [a]
+*)
+
+val diff : t -> t -> t
+(** [diff a a'] creates a new automaton [a''] that select nodes selected
+ by [a] but not selected by [a']
+*)
+
+module Builder :
+sig
+ type auto = t
+ (** Alias type for the automata type *)
+
+ type t
+ (** Abstract type for a builder *)
+
+ val make : unit -> t
+ (** Create a fresh builder *)
+
+ val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
+ (** Add a state to the set of states of the automaton. The
+ optional arguments [?starting] and [?selecting] (defaulting
+ to [false]) allow one to specify whether the state is
+ starting/selecting. *)
+
+ val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
+ (** Add a transition to the automaton *)
+
+ val finalize : t -> auto
+ (** Finalize the automaton and return it. Clean-up unused states (states that
+ do not occur in any transitions and remove instantes of negative [move] atoms
+ by creating fresh states that accept the complement of the negated state.
+ *)
+end
+ (** Builder facility for the automaton *)
projects / tatoo.git / blobdiff