README 7.44 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
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


14
15
16
17
18
19
20
Installation
============

Requirements
------------

Spot requires a complete installation of Python (version 2.0 or
21
22
23
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).
24
25
26

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
27
28
these yourself: they are included in this package (directories buddy/
and lbtt/) and will be built and installed alongside of Spot.
29
30
31
32
33
34
35
36
37


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.

38
In addition to its usual options, ./configure will accept some
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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
53
54
    After you have installed Spot the first time, LBTT and a modified
    version of BuDDy will be installed.  The next time you reconfigure
55
56
57
58
59
60
61
    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.

62
63
64
65
66
  --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.

67
68
69
70
71
72
73
  --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.

74
75
  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
    turn on assertions.  This option is effective by default in
77
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
    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.
114
115


116
117
118
119
120
121
Layout of the source tree
=========================

Core directories
----------------

122
123
src/              Sources for libspot.
   kripke/        Kripke Structure interface.
124
125
   kripkeparse/   Parser for explicit Kripke.
   kripketest/    Tests for kripke explicit.
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
   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.
   tgbatest/      Tests for tgba/, tgbaalgos/, and tgbaparse/.
   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.
   sanity/        Sanity tests for the whole project.
doc/              Documentation for libspot.
   spot.html/     HTML reference manual.
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,
152
   ltlclasses/    ... translation of more classes of LTL formulae,
153
   scc-stats/     ... SCC statistics after translation of LTL formulae,
154
155
   split-product/ ... parallelizing gain after splitting LTL automata,
   wdba/          ... WDBA minimization (for obligation properties).
156
157
158
wrap/             Wrappers for other languages.
   python/        Python bindings for Spot and BuDDy
      tests/      Tests for these bindings
159
      ajax/       LTL-to-TGBA translator with web interface, using Ajax.
160
iface/            Interfaces to other libraries.
161
   dve2/          Interface with DiVinE2.
162
163
   gspn/          GreatSPN interface.
      examples/   Supporting models used by the test cases.
164
165
166

Third party software
--------------------
167

Guillaume Sadegh's avatar
Guillaume Sadegh committed
168
buddy/            A patched version of BuDDy 2.3 (a BDD library).
169
lbtt/             lbtt 1.2.1 (an LTL to Büchi automata test bench).
170
ltdl/             Libtool's portable dlopen() wrapper library.
171

172
173
Build-system stuff
------------------
174
175
176

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
178
179
180
181
182
183
184
185

-------------------------------------------------------------------------------
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
186
187
188
 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
189
190
191
LocalWords:  formulae optimizations kripkeparse kripketest Automata
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen