Autowrite is now part of TRAG

Made with Lisp

What is Autowrite

Autowrite is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autowrite is an experimental tool written in Common Lisp for checking properties of term rewrite systems and handling bottom-up term (tree) automata. It is written in Steele Bank Common Lisp ( SBCL). It was initially designed to check call-by-need (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata constructions (determinization, minimization, union, intersection, emptimess,...) and many operations on terms. Recently, fly-automata have been added to the implementation. The transition function of a fly-automaton is a (Lisp) transition function instead of a table of transitions. Fly-automata may be used when the transition table is too big to be stored and can also be infinite in two ways (infinite signature, infinite number of states). A graphical interface interface written using FreeCLIM , the free implementation of the CLIM specification frees the user from any Lisp knowledge. From this interface, one can handle term rewrite systems, term automata and build many term automata related to TRSs and graphs represented as terms; one can check membership to call-by-need classes for the different considered approximations of a given system.

Main features of Autowrite

The principal features of Autowrite are:

Obtaining Autowrite (version 5.1 of TRAG)

The Autowrite distribution is publically available for research purposes.
The Autowrite distribution consists of a Linux gzip-compressed tar file.
The currently supported machines and operating systems are listed below.

  • PC x86_64 under Linux with libc-2.11 (check your libc) Autowrite.tgz
  • Intel with MacOSX and X11 Autowrite.tgz
  • Other architectures can be made available upon request.

    A collection of examples of term rewrite systems to use with Autowrite is included in the Data directory of the distribution.

    Installing Autowrite

    Download the relevant Autowrite.tgz tar file

    Running Autowrite

    At any time from the command line, the user may get help about the current possibilities by clicking on the right-button. Commands are accessible either thru the command line (using completion) or from the menus items. For instance, instead of hitting the Quit button you may type Q ; instead of selecting the Load spec of the File menu, you may type 'Lo Sp '...
    Note that some examples may run for a very long time as the problem of deciding membership to CBN_alpha (can be from exponential to triply exponential).
    Add your own specifications in the Data directory

    Please refer to the Autowrite user's guide to see how to use Autowrite. Also available in Postscript or PDF


    Autograph is now part if the TRAG project (Term Rewriting Automata and Graphs) available on BitBucket:
     git clone 


    Autowrite is used in Autograph for checking properties of graphs of bounded clique-width.

    Contact information

    Should you have any comments or suggestions regarding Autowrite, or ideas on new functionalities that you would like to see in future releases of Autowrite, please send them to


    F. Jacquemard. Decidable approximations of term rewriting systems. In Proc. 7th RTA, volume 1103 of LNCS, pages 362--376, 1996.
    H. Comon. Sequentiality, Monadic Second Order Logic and Tree Automata. Information and Computation, 157:25--51, 2000.
    I.Durand and A.Middeldorp. On the complexity of deciding call-by-need. Technical Report 1194-98, LaBRI, Université de Bordeaux I, 1998.
    I.Durand and A.Middeldorp. On the modularity of deciding call-by-need. In Proc. FoSSaCS'01, volume 2030 of LNCS, pages 199-213, 2001
    I.Durand and A.Middeldorp. Decidable call-by-need computations in term rewriting. Information and Computation, 196:95-126, 2005.
    I. Durand. Autowrite: A tool for term rewrite systems and term automata. Electronic Notes in Theorical Computer Science, volume 124, pages 29-49, 2005
    H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez a nd S. Tison and M. Tommasi. Tree Automata Techniques and Applications.
    B. Courcelle and I. Durand. Verifying monadic second order graph properties with tree automata. Proceedings of the 3rd European Lisp Symposium, pages 7-21, 2010

    Pointers to relevant sites

    Here are some pointers to other sites with similar interests, listed by topic.

    Sites and people

    Term Rewriting
    Steele Bank Common Lisp (SBCL)
    Free CLIM
    Irčne Durand