README 5.66 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
Installation
============

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

Spot requires a complete installation of Python (version 2.0 or
later).  Especially, Python's headers files should be installed.

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 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 additions 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
38
39
    After you have installed Spot the first time, LBTT and a modified
    version of BuDDy will be installed.  The next time you reconfigure
40
41
42
43
44
45
46
47
48
    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.

  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
    turn on assertions.  This option is effective by default in
50
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
    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.
87
88


89
90
91
92
93
94
Layout of the source tree
=========================

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

95
src/            Sources for libspot.
96
   ltlast/      LTL abstract syntax tree (including nodes for ELTL).
97
98
99
100
101
102
   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.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
103
   tgbaalgos/   Algorithms on TGBA.
104
      gtec/     Couvreur's Emptiness-Check.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
105
   tgbaparse/   Parser for explicit TGBA.
106
   tgbatest/    Tests for tgba/, tgbaalgos/, and tgbaparse/.
107
   evtgba*/     Ignore these for now.
108
109
   eltlparse/	Parser for ELTL formulae.
   eltltest/    Tests for ELTL nodes in ltlast/ and eltlparse/.
Guillaume Sadegh's avatar
Guillaume Sadegh committed
110
111
112
   saba/        SABA (State-labeled Alternating Büchi Automata) objects.
   sabaalgos/   Algorithms on SABA.
   sabatest/    Tests for saba/, sabaalgos/.
113
doc/	        Documentation for libspot.
114
   spot.html/   HTML reference manual.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
   spot.latex/  Sources for the PDF manual.  (Not distributed, can be rebuilt.)
116
   spotref.pdf  PDF reference manual.
117
bench/          Benchmarks...
118
119
   emptchk/     ... for emptiness-check algorithms,
   ltl2tgba/    ... for LTL-to-Büchi translation algorithms.
120
121
122
123
124
125
126
wrap/	        Wrappers for other languages.
   python/      Python bindings for Spot and BuDDy
      tests/    Tests for these bindings
      cgi/      Python-based CGI script (ltl-to-tgba translator)
iface/	        Interfaces to other libraries.
   gspn/        GreatSPN interface.
      examples/ Supporting models used by the test cases.
Guillaume Sadegh's avatar
Guillaume Sadegh committed
127
128
   nips/        NIPS interface (to use Promela models).
      nipstest/ Tests for NIPS.
129
130
131

Third party software
--------------------
132

Guillaume Sadegh's avatar
Guillaume Sadegh committed
133
134
135
136
137
138
buddy/            A patched version of BuDDy 2.3 (a BDD library).
lbtt/             lbtt 1.2.0 (an LTL to Büchi automata test bench).
iface/            Interfaces to other libraries.
   nips/          NIPS interface (to use Promela models).
      nips_vm/    NIPS VM 1.2.7 (New Implementation of Promela Semantics
                  Virtual Machine).
139

140
141
Build-system stuff
------------------
142
143
144

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
145
146
147
148
149
150
151
152
153
154

-------------------------------------------------------------------------------
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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
155
 LocalWords:  CGI ltl iface BDD Couvreur's evtgba emptchk