Binary Tree Automata Library (for OCaml) Copyright (C) 2003 Emmanuel Filiot This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA version 1.0 beta contact : filiot@grappa.univ-lille3.fr (********************************************************************) (****** *******) (****** Binary Tree Autamata Library *******) (****** *******) (********************************************************************) VERSION 1.0 AUTHOR Emmanuel Filiot filiot@grappa.univ-lille3.fr DEPENDENCIES ocaml version >= 3.06 with ocamlopt findlib which can be found on http://www.ocaml-programming.de/packages/ INSTALLATION 1) become root by typing `su` if necessary ( typically when writing in the directory specified by the variable dest_dir of findlib.conf requires to be root) 2) type `make install` (you can specify the binary file 'ocamlfind' with the variable OCAMLFIND default:ocamlfind) You can check if the package binary_tree_automata is well installed by using the command : ocamlfind query binary_tree_automata The installation procedure installs all the modules (*.ml *.mli *.cmo *.a *.cmx *.cma *.cmxa) in dest_dir/binary_tree_automata/ where dest_dir is the variable specified in findlib.conf . ABSTRACT The Binary Tree Automata Library provides functions for using classical tree automata with binary trees ( membership, determinization, union, intersection, complementation, printing), e.g. the membership can run only with binary trees. The library also provides functors which allows to create new implementations of the required modules. DESCRIPTION The library is divided into modules, which main ones are : -Automaton : provides the functions enumerated below -Term : provides functions for binary trees -Rules : provides functions for manipulating set of rules -States : provides functions for manipulating set of states -Alphabet : provides functions for manipulating an alphabet A typical .mli of the library include the signature of the module, a functor Make to make an new implementation of the signature, and an implementation of the signature, obtained by the functor application, often named with the same name of the .mli file : For example, the file states.mli look like : > module type STATES = > sig > type t > > ... > > end > > module Make : functor(Toto : TOTO) -> STATES > > module States : STATES Therefore when we speak about the module States, it must be known if it is the module issued from states.ml, or if it is the module States.States . USING THE LIBRARY Example 1 : toto1.ml > open Automaton > > let () = print_string ( Automaton.to_string (Automaton.empty ()) > Example 2 : toto2.ml > open Automaton > open Automaton.Automaton > > let () = print_string (to_string (empty ())) How to compile ? 1) With ocamlfind ocamlfind ocamlc -package binary_tree_automata -c toto.mli ocamlfind ocamlc -package binary_tree_automata -c toto.ml ocamlfind ocamlc -package binary_tree_automata -linkpkg -o run_toto toto.cmo It is the same way with ocamlopt : ocamlfind ocamlopt -package binary_tree_automata -c toto.mli ocamlfind ocamlopt -package binary_tree_automata -c toto.ml ocamlfind ocamlopt -package binary_tree_automata -linkpkg -o run_toto toto.cmx notes : description of -package and -linkpkg options -package : Causes that the package is added to the package list, and that -I options are added for every package, and all direct or indirect ancestors. -linkpkg: Causes that the archives of the packages in the package list and all their direct or indirect ancestors are added in topological order to the command line before the first file to compile or to link. 2) Without ocamlfind with ocamlc ocamlc -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -c toto.mli ocamlc -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -c toto.ml ocamlc -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -o run_toto binary_tree_automata.cma toto.cmo with ocamlopt ocamlopt -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -c toto.mli ocamlopt -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -c toto.ml ocamlopt -I BINARY_TREE_AUTOMATA_LIBRARY_PATH -o run_toto binary_tree_automata.cmxa toto.cmx USING THE LIBRARY IN A TOPLOOP WITH TOPFIND It is possible to use the library in a toploop using the module Topfind provides with FindLib. Here is an example : type the command `ocaml` in a shell. Example : Objective Caml version 3.06 # #use "topfind";; Findlib has been successfully loaded. Additional directives: #require "package";; to load a package #list;; to list the available packages #camlp4o;; to load camlp4 (standard syntax) #camlp4r;; to load camlp4 (revised syntax) Topfind.reset();; to force that packages will be reloaded - : unit = () # #require "binary_tree_automata";; Loading /usr/lib/ocaml/site-lib/binary_tree_automata/binary_tree_automata.cma # open Binary_tree_automata;; Unbound module Binary_tree_automata # open Automaton;; # module A = Automaton ;; module A : sig type symbol = Symbol.Symbol.t and alphabet = Alphabet.Alphabet.t and term = Term.Term.t and states = States.States.t and rules = Rules.Rules.t and automaton = (Alphabet.Alphabet.t, States.States.t, Rules.Rules.t) Automaton.automata_type exception Alphabets_not_equal val debug : bool ref val set_debug : bool -> unit val empty : unit -> automaton val membership : automaton -> term -> bool val to_string : automaton -> string val to_short_string : automaton -> string val determinize : automaton -> automaton val complement : automaton -> automaton val union : automaton -> automaton -> automaton val inter : automaton -> automaton -> automaton val emptyness : automaton -> bool val from_list : string list -> string list -> string list -> (string * string list * string list) list -> automaton end # open Term;; # let automaton1 = Automaton.from_list ["a";"b"] ["q"] ["q"] [("a",[],["q"]);("a",["q";"q"],["q"])] ;; val automaton1 : Automaton.Automaton.automaton = {alphabet = ; states = ; final_states = ; rules = } # print_string (Automaton.to_string automaton1);; ALPHABET : { a b } STATES : {q} FINAL STATES : {q} RULES: a(q,q)->{q} a->{q} - : unit = () # let term1 = N ("a", L "a", L "a");; val term1 : string Term.term_type = N ("a", L "a", L "a") # Automaton.membership automaton1 term1;; - : bool = true # let term2 = N ("a", N ("b", L "a", L "a"), L "a");; val term2 : string Term.term_type = N ("a", N ("b", L "a", L "a"), L "a") # print_string (Term.to_string term2);; a(b(a,a),a)- : unit = () # Automaton.membership automaton1 term2;; - : bool = false EXAMPLES See the examples directory for examples