Commit 2776de87 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

More documentation.

* README: Introduce Spot, and point to the documentation.
* wrap/python/ajax/README: Mention ltl3ba 1.0.2.
parent aa2374c5
Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.
It is mainly meant to be used as a C++ library, but it also comes with
a few handy command-line utilities, and some (limited) Python
Keeping in touch
......@@ -113,6 +124,23 @@ enable/disable-devel is not enough.
flags from a built-in list.
Some documentation can be found in the doc/ directory.
- doc/spot.html/ contains documentation for the C++ library.
- doc/tl/tl.pdf contains documentation about the various temporal
logic operators supported by Spot
"make install" will install man pages for command-line tools. (These
man pages can also be found in the src/bin/man/ subdirectory of the
source tree.) Additional documentation about these tools can be
found on-line at
Layout of the source tree
......@@ -170,7 +198,7 @@ Third party software
buddy/ A patched version of BuDDy 2.3 (a BDD library).
lbtt/ lbtt 1.2.1 (an LTL to Büchi automata test bench).
lbtt/ lbtt 1.2.1a (an LTL to Büchi automata test bench).
ltdl/ Libtool's portable dlopen() wrapper library.
lib/ Gnulib's portability modules.
......@@ -10,7 +10,7 @@ GraphViz package, is in the PATH. configure should have picked it up.
The "ltl3ba" tab will only be enabled if ltl3ba is available (as
checked by ./configure) and supports options -v/-U/-T (checked by the
CGI script). Any version strickly greater than 1.0.1 should be OK.
CGI script). These option were introduced into ltl3ba version 1.0.2.
Standalone usage
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment