X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.mli;h=8b7851b8c573236df3b9b9b37cd1d8e4c9c41c3c;hp=e4f0ffdfff574a32b4b41e17efac4fc865257708;hb=af9d790ca62e678e8e70ab8d8fa7f804985a75e0;hpb=90ce5857f6cad2ebc753fdbc8e37882a1ff47415 diff --git a/src/ata.mli b/src/ata.mli index e4f0ffd..8b7851b 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -13,88 +13,114 @@ (* *) (***********************************************************************) +(** 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 *)