X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.mli;h=2aa27b3c7894fbd1422350457f3ce75203a4c4fe;hp=a0778a1db564aeb5f101925dff94d66ba33c61ab;hb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615;hpb=969febf12344a3fe3bf793a323b2e88f7b20ebae diff --git a/src/ata.mli b/src/ata.mli index a0778a1..2aa27b3 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -13,94 +13,188 @@ (* *) (***********************************************************************) -(* - Time-stamp: -*) +(** 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 *)