alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/README
Alexandre Duret-Lutz 93f6e21759 Install gnulib to make sure we can use argp in ltlfilt. 
* lib/Makefile.am, lib/alloca.c, lib/alloca.in.h, lib/argp-ba.c,
lib/argp-eexst.c, lib/argp-fmtstream.c, lib/argp-fmtstream.h,
lib/argp-fs-xinl.c, lib/argp-help.c, lib/argp-namefrob.h,
lib/argp-parse.c, lib/argp-pin.c, lib/argp-pv.c, lib/argp-pvh.c,
lib/argp-xinl.c, lib/argp.h, lib/asnprintf.c, lib/basename-lgpl.c,
lib/dirname-lgpl.c, lib/dirname.h, lib/dosname.h, lib/errno.in.h,
lib/float+.h, lib/float.c, lib/float.in.h, lib/getopt.c,
lib/getopt.in.h, lib/getopt1.c, lib/getopt_int.h, lib/gettext.h,
lib/intprops.h, lib/itold.c, lib/malloc.c, lib/memchr.c,
lib/memchr.valgrind, lib/mempcpy.c, lib/printf-args.c,
lib/printf-args.h, lib/printf-parse.c, lib/printf-parse.h,
lib/rawmemchr.c, lib/rawmemchr.valgrind, lib/size_max.h,
lib/sleep.c, lib/stdalign.in.h, lib/stdbool.in.h, lib/stddef.in.h,
lib/stdint.in.h, lib/stdio.in.h, lib/stdlib.in.h, lib/strcasecmp.c,
lib/strchrnul.c, lib/strchrnul.valgrind, lib/strerror-override.c,
lib/strerror-override.h, lib/strerror.c, lib/string.in.h,
lib/strings.in.h, lib/stripslash.c, lib/strncasecmp.c,
lib/strndup.c, lib/strnlen.c, lib/sys_types.in.h, lib/sysexits.in.h,
lib/unistd.in.h, lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h,
lib/vsnprintf.c, lib/wchar.in.h, lib/xsize.h, m4/00gnulib.m4,
m4/alloca.m4, m4/argp.m4, m4/dirname.m4, m4/double-slash-root.m4,
m4/errno_h.m4, m4/exponentd.m4, m4/extensions.m4, m4/float_h.m4,
m4/getopt.m4, m4/gnulib-cache.m4, m4/gnulib-common.m4,
m4/gnulib-comp.m4, m4/gnulib-tool.m4, m4/include_next.m4,
m4/intmax_t.m4, m4/inttypes_h.m4, m4/longlong.m4, m4/malloc.m4,
m4/math_h.m4, m4/memchr.m4, m4/mempcpy.m4, m4/mmap-anon.m4,
m4/multiarch.m4, m4/nocrash.m4, m4/off_t.m4, m4/printf.m4,
m4/rawmemchr.m4, m4/size_max.m4, m4/sleep.m4, m4/ssize_t.m4,
m4/stdalign.m4, m4/stdbool.m4, m4/stddef_h.m4, m4/stdint.m4,
m4/stdint_h.m4, m4/stdio_h.m4, m4/stdlib_h.m4, m4/strcase.m4,
m4/strchrnul.m4, m4/strerror.m4, m4/string_h.m4, m4/strings_h.m4,
m4/strndup.m4, m4/strnlen.m4, m4/sys_socket_h.m4, m4/sys_types_h.m4,
m4/sysexits.m4, m4/unistd_h.m4, m4/vasnprintf.m4, m4/vsnprintf.m4,
m4/warn-on-use.m4, m4/wchar_h.m4, m4/wchar_t.m4, m4/wint_t.m4,
m4/xsize.m4, tools/snippet/_Noreturn.h, tools/snippet/arg-nonnull.h,
tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: New files from
gnulib 1af55d85d9762a679b4302d5995f05ccd883e956.
* configure.ac, Makefile.am: Adjust to compile gnulib.
* src/bin/Makefile.am: Adjust to use gnulib.
* README: Mention lib/.
2012-09-07 14:32:10 +02:00

196 lines
7.7 KiB
Text
Raw Blame History

Keeping in touch
================
If you have questions regarding Spot, a bug reports, please send them
to <spot@lrde.epita.fr>. This is a public mailing list which you may
subscribe to at https://www.lrde.epita.fr/mailman/listinfo/spot but you
should feel free to post without subscribing.
We also run an extremely low traffic list for announcements of
new releases of Spot. You may subscribe to that list at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
Installation
============
Requirements
------------
Spot requires a complete installation of Python (version 2.0 or
later). Especially, Python's headers files should be installed. If
you don't have Python installed, you should run configure with
the --disable-python option (see below).
Spot also uses modified versions of BuDDy (a binary decision diagram),
and LBTT (an LTL to Büchi test bench). You do not need to install
these yourself: they are included in this package (directories buddy/
and lbtt/) and will be built and installed alongside of Spot.
Building and installing
-----------------------
Spot follows the traditional `./configure && make && make check &&
make install' process. People unfamiliar with the GNU Build System
should read the file INSTALL for generic instructions.
In addition to its usual options, ./configure will accept some
flags specific to Spot:
--with-gspn=DIR
Turns on GreatSPN support. DIR should designate the root of
GreatSPN source tree. (./configure will then run
DIR/SOURCES/contrib/version.sh to find the GreatSPN build tree.)
GreatSPN had to be modified in order to be used as a library
(thanks Soheib Baarir and Yann Thierry-Mieg for this work), and
presently these modifications are only available on the GreatSPN
CVS repository hosted by the Università di Torino.
--with-included-buddy
--with-included-lbtt
After you have installed Spot the first time, LBTT and a modified
version of BuDDy will be installed. The next time you reconfigure
Spot, configure will detect that these versions are already
installed, and will attempt to use these installed versions
directly (this is in case you had to modify one of these yourself
for another purpose). These two options will *force* the use,
build, and installation of the included versions of these package,
even when compatible versions are already installed.
--without-included-lbtt
Explicitly Turn off the configuration and compilation of LBTT.
This is required on systems (such as MinGW) where LBTT does not
compile.
--disable-python
Turn off the compilation of Python bindings. These bindings are
currently used to run a couple of tests, and to build the CGI
script that translates LTL formulae on-line. You may safely
disable these, especially if you do not have a working Python
installation or if you are attempting some cross-compilation.
--enable-devel
Enable debugging symbols, turn off aggressive optimizations, and
turn on assertions. This option is effective by default in
development versions (version numbers ending with a letter).
It is equivalent to
--enable-debug
--enable-warnings
--enable-assert
--enable-optimizations=-O
--disable-devel
Disable development options. This is the case by default in
releases (version numbers NOT ending with a letter).
It is equivalent to
--disable-debug
--disable-warnings
--disable-assert
--enable-optimizations
Here are the meaning of the fine-tuning options, in case
enable/disable-devel is not enough.
--disable-assert
--enable-assert
Control assertion checking.
--disable-warnings
--enable-warnings
Whether warnings should be output. Note that during development
we consider warnings to be errors.
--disable-debug
--enable-debug
Whether to compile extra debugging code.
--enable-optimizations
--enable-optimizations=FLAGS
--disable-optimizations
Whether the compilation should be optimized. When FLAGS are
given, use these as optimization flags. Otherwise, pick working
flags from a built-in list.
Layout of the source tree
=========================
Core directories
----------------
src/ Sources for libspot.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
kripketest/ Tests for kripke explicit.
ltlast/ LTL abstract syntax tree (including nodes for ELTL).
ltlenv/ LTL environments.
ltlparse/ Parser for LTL formulae.
ltlvisit/ Visitors of LTL formulae.
ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
misc/ Miscellaneous support files.
tgba/ TGBA objects and cousins.
tgbaalgos/ Algorithms on TGBA.
gtec/ Couvreur's Emptiness-Check.
tgbaparse/ Parser for explicit TGBA.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/.
evtgba*/ Ignore these for now.
eltlparse/ Parser for ELTL formulae.
eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
saba/ SABA (State-labeled Alternating Büchi Automata) objects.
sabaalgos/ Algorithms on SABA.
sabatest/ Tests for saba/, sabaalgos/.
neverparse/ Parser for SPIN never claims.
bin/ User tools built using the Spot library.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
tl/ Documentation of the Temporal Logic operators.
spot.html/ HTML reference manual for the library.
bench/ Benchmarks for ...
emptchk/ ... emptiness-check algorithms,
gspn-ssp/ ... various symmetry-based methods with GreatSPN,
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
ltlcounter/ ... translation of a class of LTL formulae,
ltlclasses/ ... translation of more classes of LTL formulae,
scc-stats/ ... SCC statistics after translation of LTL formulae,
split-product/ ... parallelizing gain after splitting LTL automata,
wdba/ ... WDBA minimization (for obligation properties).
wrap/ Wrappers for other languages.
python/ Python bindings for Spot and BuDDy
tests/ Tests for these bindings
ajax/ LTL-to-TGBA translator with web interface, using Ajax.
iface/ Interfaces to other libraries.
dve2/ Interface with DiVinE2.
gspn/ GreatSPN interface.
examples/ Supporting models used by the test cases.
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).
ltdl/ Libtool's portable dlopen() wrapper library.
lib/ Gnulib's portability modules.
Build-system stuff
------------------
m4/ M4 macros used by configure.ac.
tools/ Helper scripts used during the build.
-------------------------------------------------------------------------------
Local Variables:
mode: text
End:
LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann
LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm
LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
LocalWords: formulae optimizations kripkeparse kripketest Automata
LocalWords: neverparse ltlcounter ltlclasses parallelizing automata
LocalWords: wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen
Reference in a new issue View git blame Copy permalink