Ltl3tools

LTL3 tools README -=-=-=-=-=-=-=-=-

What you need to properly use the LTL3 tools:

Download:

1. AT&T's fsmlibrary version 4.0. It used to be widely available under a free-to-use license for noncommercial purposes, but now seems to be available only upon request. Perhaps, these folks can help:

   https://github.com/att

   Otherwise use a web search, as many universities still use the library in their courses and offer binaries to download.

2. LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ (tested with version 1.1 of the translator)

3. Optional: AT&T's Graphviz, which includes the programs dot, dotty, etc. Note that most modern Linux systems have these preinstalled.

Then simply copy the binaries of 1. and 2. into the third-party/ directory of the LTL3 tools distribution. (2. may have to be compiled first.)

How to run ltl2mon / the LTL3 tools:

1. Change into the directory where you extracted the package

2. Optional: Check the settings inside ltl2mon (ltl2mon is the main entry point to the LTL3 tools)

3. Run, for example, "./ltl2mon "(! a) U b" | dot -Tps > graph.ps"

How to compile the LTL3 tools:

If you are on i686 GNU/Linux, you do not have to compile the LTL3 tools as there are some statically linked binaries in the bin/ directory. Otherwise, follow these steps to compile the LTL3 tools:

1. Change into the directory where you extracted the package

2. Run "make install"

   Notice, ltl2mon is written in Ocaml. So, you will need an Ocaml tool chain.

For further information read the files AUTHORS and COPYING, or visit http://ltl3tools.sf.net/.