Loops and Overloops for Tree Walking Automata: Companion Page

Vincent HUGOT

This web page complements the following paper:

Loops and Overloops for Tree Walking Automata
co-authors: P.C. Héam, O. Kouchnarenko
Springer LNCS – International Conference CIAA’11 (Long Paper)  — March 2011
Additional webpage and slides.

[Go back to my main page].


1 Introduction

This software merely serves to illustrate the algorithms of the paper, which I think is useful given the explosive character of these transformations, which prohibits doing things by hand even for very trivial TWA.

Note about the source code: (in case you read it, which you really don’t need to do)

Although I have some confidence that the code is correct, it is very messy, as it was written before the transformation was fully formalised – and it was not intended to be read by anyone else... Also note that there is a lot of source code which is completely unrelated to TWA – this is in fact my work tool for all kinds of tree automata research. So, in a nutshell: read and use at your own risk.

Related work:

The only other program I known of which implements the TWA → BUTA transformation (loop-based only, of course) is dtwa-tools1, available here, which was developed for this article. However, I am fairly certain the algorithm which it implements is not entirely correct. We have discussed in our paper how the BUTA states given in the proof sketches – 𝕋 × 2Q2 – were surprising, as loops cannot be considered independently of the symbol which supports them. Which is why our loop-based algorithm uses states in Σ × 𝕋 × 2Q2. In dtwa-tools, the implementor followed the proof sketches, and went around the lack of symbol by allowing loops to be closed if there exists a symbol for which there is an ↑-transition which closes the loop (and this is exactly what we did at first, too). However, for the reason discussed in the paper, this may compute more loops than actually exist – and we have given a trivial counter-example.

2 Getting the Proof of Concept

2.1 Precompiled Binaries

Binaries are available for the following operating systems:

2.2 Building From Source

The OCaml source code can be downloaded from my subversion repository at http://vincent-hugot-projects.googlecode.com/svn/trunk/ocaml/TAged-emptiness2/. Note that this repository is in constant evolution, which means that the latest version of the code may have little to do with the binary file you downloaded. For this reason, you may want to download the exact revision corresponding to the binaries you want to compile – or whose code you simply desire to read. This is why the revision number is provided – as annotations of the form (rXXX) – in the above list. Note that the revision number pertains to the whole repository, and not to any specific project in it.

If you want to build the proof of concept from source, you will need to pull at least ocaml/common (shared files) and ocaml/Taged-emptiness2 (the POC), and run setup.sh from common, and then make.sh from the POC’s directory. You will need wget, ocaml, camlp4 (with camlp4-extras), and menhir. Of course, this assumes some “Unix-y” environment, capable of running shell scripts. I work with GNU/Linux (Kubuntu), tested with Cygwin under Windows XP SP3, and assume it would work with a Mac. If you are using the Windows/MinGW or Windows/MVSC version of OCaml, then you will probably have to do a little bit of work to convert the shell scripts into MSDOS BAT files.

3 Using the Program

3.1 The Input

In this section, POC designates the name of the proof-of-concept executable, for instance poc.linux if you downloaded the linux version. The $ indicates a command prompt, regardless of which OS you are actually using.

The program is used in the following way:

$ POC [dbg] [_clean] twa <TWA> <TREE>

EXAMPLE: The output presented in the next section has been generated from a working copy of my subversion repository, using the command :

$ POC _clean twa t/lncs.twa t/ciaa-tree

3.2 The Output

The program generates a PDF file such as this one: . In this section we give a few explanations concerning the contents of such a file.

4 Questions

If you have any questions which are not covered by this document, you are welcome to contact me at vincent.hugot@gmail.com. Time permitting, I will update this page with the answer.

version 0.3
Compiled with Cygwin. Thus you may need the Cygwin DLL to run it.

This document was translated from LATEX by HEVEA.