(* *)
(***********************************************************************)
+(** Implementation of 2-way Selecting Alternating Tree Automata *)
+
+
type move = [ `First_child
| `Next_sibling
| `Parent
| `Previous_sibling
| `Stay ]
-
-type predicate = Move of move * State.t
- | Is_first_child
- | Is_next_sibling
- | Is of Tree.NodeKind.t
- | Has_first_child
- | Has_next_sibling
-
-val is_move : predicate -> bool
-
-module Atom : Boolean.ATOM with type data = predicate
+(** Type of moves an automaton can perform *)
+
+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 Formula :
sig
include module type of Boolean.Make(Atom)
- val mk_atom : predicate -> t
- val mk_kind : Tree.NodeKind.t -> t
- val has_first_child : t
- val has_next_sibling : 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
+ (** [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] *)
end
+(** Modules representing the Boolean formulae used in transitions *)
+module Transition : Hcons.S with type data = State.t * QNameSet.t * Formula.t
+(** 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 * Formula.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;
-}
+val get_states : t -> StateSet.t
+(** return the set of states of the automaton *)
-module Config : Hcons.S with type data = config
-val dummy_config : Config.t
+val get_selecting_states : t -> StateSet.t
+(** return the set of selecting states of the automaton *)
-type t = private {
- id : Uid.t;
- mutable states : StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
- mutable cache2 : TransList.t Cache.N2.t;
- mutable cache4 : Config.t Cache.N4.t;
-}
+val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
+(** [get_trans auto l q] return 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 print : Format.formatter -> t -> unit
+(** Pretty printing of 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
+module Builder :
+sig
+ type auto = t
+ (** Alias type for the automata type *)
+ type t
+ (** Abstract type for a builder *)
-val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
+ val make : unit -> t
+ (** Create a fresh builder *)
-val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
-val print : Format.formatter -> t -> unit
-val complete_transitions : t -> unit
-val cleanup_states : t -> unit
-val normalize_negations : t -> unit
+ val add_state : t -> ?selecting:bool -> State.t -> unit
+ (** Add a state to the set of states of the automaton. The optional argument
+ [?selecting] (defaulting to [false]) allows to specify whether the state is
+ 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