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
38
39
40
41
42
43
44
45
46
47
48
49
50
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
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
114
115
116
117
118
119
120
121
122
123
124
125
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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<!-- saved from url=(0040)http://spinroot.com/spin/Man/README.html -->
<HTML><HEAD><TITLE>Spin - Version 6.4 - January 2016</TITLE>
<META http-equiv=Content-Type content="text/html; charset=windows-1252">
<META content="MSHTML 6.00.2800.1276" name=GENERATOR></HEAD>
<BODY bgColor=#ffffff>
<p>
<table width=100%><tr><td width=15%> </td><td width=70%>
<H1><TT><FONT color=#ff0000>SPIN README</FONT></TT></H1>
<ul></ul>
<H2><TT>Overview of this File</TT></H2>
<OL>
<LI><A href="http://spinroot.com/spin/Man/README.html#S2">Downloading Spin</A>
<LI><A href="http://spinroot.com/spin/Man/README.html#S1">Installing Spin</A>
<LI><A href="http://spinroot.com/spin/Man/README.html#S3">Related software
(gcc, cpp, tcl/tk wish, yacc, dot, etch, jspin, erigone, spinja, ltl2ba)</A> </LI></OL>
<HR>
<H2><TT>0. Overview</TT></H2>This readme file contains the guidelines for
downloading and installing Spin and related software on Unix/Linux and Windows
platforms. Refer to <A href="http://spinroot.com/spin/whatispin.html">Spin's
homepage</A> for a general description of Spin, with pointers to <A
href="http://spinroot.com/spin/Man/index.html">manual pages</A>, <A
href="http://spinroot.com/spin/News/index.html">newsletters</A>.
<p>
Spin is distributed freely in source form to encourage research in formal
verification, and to help a support friendly and open exchange of algorithms,
ideas, and tools.
<ul>
<h3><tt>Copyright and License</tt></h3>
The original version of the Spin source code was developed by Gerard Holzmann
at Bell Laboratories between 1980 and 1990. It was first publically released
in January 1991, initially through the Netlib source code repository.
It has been distributed freely since then for research and educational purposes,
without any guarantee of any kind expressed or implied.
On 30 December 2015 Alcatel-Lucent (the company that inherited Bell Laboratories
from AT&T in the trivestiture from 1996) transfered the copyright to all sources
to Gerard Holzmann, explicitly to enable a standard open source release
under the BSD 3-Clause license. Starting with Spin Version 6.4.5 all Spin code,
sources and executables, are now available under the BSD 3-Clause license.
<p>
From the early development of the Plan9 Operating System, Spin has also been
part of that system. This means that versions of the Spin source code can also
be found in the Plan9 distributions. One branch of that code, for instance,
is distributed also by UC Berkeley under a
<a href="http://www.gnu.org/licenses/">GPLv2 license</a> (see
<a href="http://akaros.cs.berkeley.edu/files/Plan9License">UCB</a>).
(Although the sources in that version are still labeled under the older
copyright from AT&T and Lucent Technologies.)
The BSD version of Spin 6.4.5 and later is likely to find its way into
newer distributions of the Plan9 code as well.
</ul>
<p>
<HR>
<H2><TT><A name=S2>1. Downloading Spin</A></TT></H2>Spin runs on Unix,
Solaris, and Linux machines, on most flavors of Windows PCs, and on Macs.
Precompiled binary executables for some popular types of machines are available
in the
<A href="http://spinroot.com/spin/Bin/index.html">Spin Binaries</A>.
<p>
All binaries have an extension that matches the Spin version number,
such as <tt>spin644.exe</tt>. To install the binary, rename it to
<tt>spin.exe</tt> and copy it into your bin directory.
<p>
If you have machine type that is not available there, or if you are
installing Spin for the first time, then follow the more detailed instructions
below.
<ul>
<LI><B>Unix</B> systems: <BR>download the most recent .tar-file with sources,
the graphical interface iSpin, documentation and examples from the <A
href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>, and
continue at <A href="http://spinroot.com/spin/Man/README.html#S1a"><FONT
color=red><B><TT>Step 2a</TT></B></FONT></A>.</LI>
<p></p>
<LI><B>PCs</B> (Windows95/98/2000/NT/XP): <BR>download the most recent
pc_spin*.zip file, with a precompiled Spin executable, the graphical interface
iSpin, and some examples from the <A
href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>, and
continue at <A href="http://spinroot.com/spin/Man/README.html#S1b"><FONT
color=red><B><TT>Step 2b</TT></B></FONT></A>. </LI>
<p></p>
<LI><B>Macs</B> (Mac OS X): <BR>download the most recent .tar-file with sources,
from the <A href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>,
and continue at <A href="http://spinroot.com/spin/Man/README.html#S1c"><FONT
color=red><B><TT>Step 2c</TT></B></FONT></A>.
</LI></ul>
<p>
<HR>
<H2><TT><A name=S1>2. Installing Spin</A></TT></H2>
<ul>
<LI><A href="http://spinroot.com/spin/Man/README.html#S1a"><TT>Unix/Linux
systems</TT> (compiled from the sources)</A>
<LI><A href="http://spinroot.com/spin/Man/README.html#S1b"><TT>Windows
PC's</TT> (using the executable)</A> </LI>
<LI><A href="http://spinroot.com/spin/Man/README.html#S1c"><TT>Macs
</TT> (compiled from the sources, with some patches)</A> </LI></ul><p>
<HR>
<H2><TT><A name=S1a><FONT color=red>2a. Installing Spin on a Unix/Linux
System</A></FONT></TT></H2>
<ul>Place the *.tar.gz file from the <A
href="http://spinroot.com/spin/Src/index.html">Spin Source Distribution</A> in
clean directory, and cd to that directory. If you have a standard Unix/Linux system,
unpack the archive, and compile an executable, for instance as follows: <pre> gunzip *.tar.gz
tar -xf *.tar
cd Src*
make
</pre>
<p>If you are on a SOLARIS system, edit the makefile and add
<TT>-DSOLARIS</TT> to the compiler directives in the makefile before you type
'make'. Similarly, if you use a different C compiler than defined in the
makefile, edit the makefile first. You need to have at least a C compiler and
a copy of yacc.
<p>If all else fails, you can also compile everything with the following line:
<pre> yacc -v -d spin.y; cc -o spin *.c
</pre>
<p>Spin should compile without warnings. Install the executable version of
spin in a directory that is within your default search path (such as your home
bin directory, or /usr/local/bin etc.)
<p>
On Unix/Linux systems Spin assumes that the standard C preprocessor cpp is
stored in file "/lib/cpp". On some systems this is different: check the
comments in the makefile for details if you run into this problem.
<H3><TT>Testing</TT></H3>To test the basic sanity of the Spin executable, or
to get familiar with the basic usage of Spin, cd
to the Examples directory that was created when you unpacked the source archive,
and follow the instructions in README.tests file that is included there.
<H3><TT>Adding iSpin (Unix/Linux)</TT></H3>iSpin is an optional, but highly
recommended, graphical user interface to Spin, written in Tcl/Tk. To obtain
Tcl/Tk, see <A href="http://spinroot.com/spin/Man/README.html#S3">Related
software</A>. The iSpin source can be found the iSpin/ subdirectory that will
is created when you unpack the source tarfile.
<p>iSpin is compatible with Tcl/Tk version 8.4 and 8.5.
<p>iSpin prints the version numbers of Spin, iSpin, and Tcl/Tk when it starts
up. You can also check separately which version of Tcl/Tk you have installed
by executing the following commands in `wish' (a Tcl/Tk command):
<pre> info tclversion
puts $tk_version
</pre>You can find out which version of Spin you have by typing, at a shell
command prompt: <pre> $ spin -V
</pre>
Spin and iSpin need a working version of a C compiler installed on your system.
<p>iSpin can also make use the graph layout program 'dot' if it is available
on your system. For information on 'dot,' see <A
href="http://spinroot.com/spin/Man/README.html#S3">Related software</A>.
<p>To install iSpin run the iSpin/install.sh script (after possibly editing it).
<ul>
<LI>invoke the program by typing<pre> ispin
or
ispin promela_spec
For example:
ispin Spin/Examples/LTL/leader.pml
</pre></LI>
</ul>Check the online Help menus in ispin for more details on routine use.</ul>
<p>
<HR>
<H2><TT><A name=S1b><FONT color=red>2b. Installing Spin on a Windows
PC</FONT></A></TT></H2>
<ul>If you just need to update the Spin executable itself, download a new
version from <A
href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>
If you need more files, e.g. a new copy of iSpin, download the latest
pc_spin*.zip file from <A
href="http://spinroot.com/spin/Src/index.html">http://spinroot.com/spin/Src/index.html</A>
Extract the files from pc_spin*.zip, and copy spin*.exe, renamed spin.exe, into the directory
where all your commands reside and that is within your default search path
(e.g., c:/cygwin/bin/, or c:\apps\spin\) You can find out what your search
path is set to by typing 'set' at an MS-DOS prompt -- this prints a list of
all defined variables in your environment, including the search path that is
used to find executable commands.
(Note that you may need to set the search path in the environment variables)
<p>
If you use Spin from the command line (i.e., without iSpin), be warned that
some command shells, e.g., the MKS Korn-shell, have none-standard rules for
argument parsing (i.e., you can not reliably quote an argument that contains
spaces, such as an LTL formula). In most cases this will not be much of a
problem, except with the conversion of LTL formula with the spin -f option.
Use single-quotes when needed, e.g.: spin -f '[]<>p'
You can circumvent the problem by using inline LTL formula, which are supported
in Spin version 6, or by using sping option -F instead of -f, to read the formula
from a file instead of the command line.
<p>
To run Spin, also with the precompiled version, you need a working
C-compiler and a C-preprocessor, because Spin generates its model checking
software as C-source files that require compilation before a verification can
be performed. This guarantees fast model checking, because each model checker
can be optimized to the specific model being checked. Check, for instance, if
you can compile and run a minimal C program succesfully, e.g.:
<pre>
#include <stdio.h>
int main(void) { printf("hello\n"); }
</pre>
<p>To find a public version of a C compiler and some instructions on how to
install it see <A href="http://spinroot.com/spin/Man/README.html#S3">Related
software</A>.
<H3><TT>Adding iSpin (PC)</TT></H3>To run iSpin on a PC, you need the PC
version of Tcl/Tk, which you can find under <A
href="http://spinroot.com/spin/Man/README.html#S3">Related software</A>.
<p>The ispin*.tcl source is contained in the .zip file of the <A
href="http://spinroot.com/spin/Src/index.html">distribution</A>. Copy the .tcl
file as is into a directory where you plan to work, or put a shortcut to this
file on the Desktop or in the Start Menu. If you keep the extension .tcl, make
sure it is recognized as a 'wish' file by the system, so that ispin starts
when you double click the ispin*.tcl script.
<p>Under cygwin, copy the ispin*.tcl file to /bin/ispin and make it executable
You can now use ispin as a normal Unix-style command,
and you can pass the name of a filename to it, for instance as: <pre> ispin leader
</pre>
<p>An alternative is to start ispin from its source by invoking wish:
<pre> wish -f ispin.tcl
or wish -f /bin/ispin
</pre
(you'll have to know where the source is stored for this to work of course).
<p>
An even more indirect way to force ispin to startup is to first start `wish' from the
Start Menu, under Programs, then select the larger window that comes up (the
command window), and cd to the directory where you've stored the ispin tcl/tk source
file. Then you can then start it up by typing: <pre> source ispin.tcl # or whatever else you've named this
</pre>and you should be up and running.
<p>The PC installation assumes that you have a command called "cpp.exe" or "gcc.exe"
available (which comes with the gnu-c installation). "cpp" is the traditional
name of the C preprocessor. Alternatively, ispin can also use the Visual C++
compiler, which is named cl.exe for preprocessing. To complicate your life
somewhat, if you have a copy of the Borland C++ compiler installed, you'll
notice that this cplusplus compiler was also named cpp.exe -- that's not the
cpp you want. To avoid the name clash, you either have to edit the Spin source
code to give it the full path name of the 'real' cpp.exe and recompile, or use
Spin with the command-line option -Pxxxx where xxxx is the path for cpp.exe.
Or better still (the current default) use gcc for both compilation and for preprocessing.
Nothing much in Spin will work without access to a preprocessor. You can do a
reasonable number of things without a full-blown compiler though (like simulations). The
C-compiler (e.g., gcc) is required for all verifications and for the automata views in
iSpin.
<p>
If iSpin cannot locate the gcc executable on your system, it will put up a warning
message when it first starts up. On recent versions of cygwin
gcc is actually a link from /bin/gcc to /bin/gcc-3 or /bin/gcc-4
<br>Depending on how the name changes, iSpin may not always recognize it.
To fix this -- edit the iSpin source (it's tcl/tk text) and
define CC as <pre> set CC c:/cygwin/bin/gcc-5</pre> or whatever the new name is.
</p></ul>
<p>
<H2><TT><A name=S1c><FONT color=red>2c. Installing Spin on a Mac</FONT></A></TT></H2>
<ul>
Compile Spin from its sources, as described under 2a for Unix systems in general,
while following the suggestions below, which were provided by
Dominik Brettnacher, email: <tt>domi@saargate.de</tt>.
<p>
The C preprocessor on Mac OS X cannot be found in <tt>/lib</tt>.
Change the path in the makefile for the
proper location (<tt>/usr/bin/cpp</tt>), and in addition
also tell the Mac preprocessor to handle its input as
"assembler-with-cpp."
This can be done by adding a flag to cpp, for instance in
the makefile by adding the directive
<ul>
<pre>
-DCPP="\"gcc -E -x c -xassembler-with-cpp\""
</pre>
</ul>
to the definition of <tt>CFLAGS</tt>.
If you prefer <tt>clang</tt>, you can also try if the following works (not tested):
<ul>
<pre>
-DCPP="\"clang -E -x c\""
</pre>
</ul>
</pre>
<p>
<H3><TT>Adding iSpin</TT></H3>
On the Mac, iSpin is known to work correctly with Tcl/Tk Aqua,
which offers a self-contained binary distribution for the Mac.
Use, for instance, "TclTkAquaStandalone", version 8.4.4 from
<ul>
<pre><a href="http://www.maths.mq.edu.au/~steffen/tcltk/TclTkAqua/">http://www.maths.mq.edu.au/~steffen/tcltk/TclTkAqua/</a>
</pre>
</ul>
<p>
Some users reported that on a Mac
iSpin by default places its temporary files into the root directory.
This is nasty if you have admin privileges and probably leads to error
messages if you don't.
To prevent this, add a "cd" statement to iSpin (no arguments, just cd by
itself on a line), as the first command executed.
Place it, for instance, directly after the opening comments in the file.
This makes iSpin use the home directory for these files.
<p>
TclTk Aqua also provides the possibility to start a script when being run.
For instance, to make iSpin start if you launch the TCL interpreter:
move the ispin file into the "Wish Shell.app", as follows:
<ul><pre>
chmod -R u+w Wish\ Shell.app
mkdir Wish\ Shell.app/Contents/Resources/Scripts
mv ispin*.tcl Wish\ Shell.app/Contents/Resources/Scripts/AppMain.tcl
</pre>
</ul>
</ul>
<HR>
<H2><TT><A name=S3>3. Related Software</A></TT></H2>
<ul>Some pointers to public domain versions of related software packages.
Some (e.g, a C compiler) are required to run Spin, but most other packages
are optional extensions or alternatives.
<H3><TT>GCC (needed for Spin)</TT></H3>On Unix/Linux you probably have gcc, or an equivalent,
installed. On the PC you need either a copy of Visual Studio Express (for the cl
command), or an installation of gcc with minimally the executables: gcc.exe,
and cpp.exe in your search path, together with all the standard C library
routines and header files. You can get good free version of all these files
with the <TT>cygwin</TT> toolkit, which is mostly self-installing and
available from: <A href="http://www.cygwin.com/">http://www.cygwin.com/</A>
<BR>See also what's available in <A
href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>.
<H3><TT>Tcl/Tk Wish (needed for iSpin only)</TT></H3>To run iSpin you'll need Tcl/Tk. Tcl/Tk was
written by John Ousterhout (john.ousterhout@eng.sun.com) and is public domain.
It can be obtained (for PCs or Unix) from cygwin, or from: <A
href="http://www.tcl.tk/">http://www.tcl.tk/</A> or also (a more recent extension):
<a href="http://www.activestate.com/Products/ActiveTcl/">
http://www.activestate.com/Products/ActiveTcl/</a><BR>More details can be found
in netnews-group: comp.lang.tcl
<H3><TT>Yacc (optional)</TT></H3>To compile Spin itself from its sources on a
PC, you'll need to have a copy of yacc installed. A public domain version for
a Windows PC can most easily be obtained from <b>cygwin</b>, or also from:
<pre> <A href="ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.Z">ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.Z</A>
</pre>A copy of this file is also available in: <A
href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>
(You don't need yacc on the PC if you use the pre-compiled version of Spin
for the pc in the pc*.zip file from the distribution) Look at the file
make_it.bat for an example on how to perform the compilation.
<br>
On a Unix/Linux/Ubuntu system you can install yacc in the usual way, with apt-get.
<H3><TT>Dot (optional)</TT></H3>Dot is a graph layout tool developed by
Stephen North and colleagues at AT&T (email: north@research.att.com).
iSpin can make use of dot to show a graph layout of the state-machines in the
automata-view option (recommended!).
To obtain Dot, see
<pre>
<A href="http://www.graphviz.org/">http://www.graphviz.org/</A>
</pre>
The are both PC and Unix versions of dot available. For documentation of
dot see, for instance:
<pre><I> A technique for drawing directed graphs</I>,
by Gansner, Koutsofios, North and Vo,
IEEE-TSE, March, 1993.
</pre>
If you accept the default installation on a PC, you will need to define the
location of dot.exe in the ispin source as follows:
<pre>
set DOT "C:/Program\\ Files\ATT\Graphviz/bin/dot.exe"
</pre>
(the line that sets the location of DOT appears near the top of the ispin.tcl file).
<H3><TT>Etch (optional)</TT></H3>
Etch, short for Enhanced Type CHecker, can perform more thorough static
checking than the default SPIN type checker, using type inference to
reconstruct types of channels which can only be incompletely specified
in Promela. The techniques are described in a
<a href="http://spinroot.com/spin/Workshops/ws05/002_paper.pdf">SPIN 2005 tool demo paper</a>.
<br>
The Etch tool can be downloaded from:
<pre>
<a href="http://www.doc.ic.ac.uk/~afd/etch/">http://www.doc.ic.ac.uk/~afd/etch/</a>
</pre>
<h3><tt>TopSpin (optional)</tt></h3>
TopSpin is a symmetry reduction package for Spin, developed by Alastair Donaldson.
It can be applied to a Promela model and, provided that the model adheres to some
restrictions (detailed in a user manual) uses computational group theory to determine
a group of component symmetries associated with the model. The tool can
modify the model checking algorithm used by Spin to exploit the symmetries during
verification, resulting in reduced memory use and in many cases also shorter verification time.
The package can be downloaded from:
<pre>
<a href="http://www.doc.ic.ac.uk/~afd/topspin/">http://www.doc.ic.ac.uk/~afd/topspin/</a>
</pre>
<H3><TT>JSpin (optional)</TT></H3>
jSpin, developed by <a href="http://stwww.weizmann.ac.il/g-cs/benari/">Moti Ben-Ari</a>, is
an alternative to the iSpin GUI written in Java instead of Tcl/Tk. It is meant as a teaching aid. See:
<pre>
<a href="http://stwww.weizmann.ac.il/g-cs/benari/jspin/">http://stwww.weizmann.ac.il/g-cs/benari/jspin/</a>
</pre>
The jSpin tool can be configured for use on Linux and Macs, and can also
run under Windows, with or without cygwin installed (e.g., with mingw).
<br>
The jSpin tool can be downloaded from GoogleCode:
<pre>
<a href="http://code.google.com/p/jspin/">http://code.google.com/p/jspin/</a>
</pre>
<H3><TT>Erigone (optional)</TT></H3>
Erigone, also developed by <a href="http://stwww.weizmann.ac.il/g-cs/benari/">Moti Ben-Ari</a>, is
a reimplementation of a subset of Spin, meant for educational use. Erigone is written in Ada 2005 instead of C.
See:
<pre>
<a href="http://stwww.weizmann.ac.il/g-cs/benari/erigone/">http://stwww.weizmann.ac.il/g-cs/benari/erigone/</a>
</pre>
Erigone can be downloaded from GoogleCode:
<pre>
<a href="http://code.google.com/p/erigone/">http://code.google.com/p/erigone/</a>
</pre>
<H3><TT>SpinJa (optional)</TT></H3>
SpinJa is reimplementation of a subset of Spin in Java,
developed by Marc de Jonge at Twente University in The Netherlands.
A more detailed description of SpinJa was presented at the 2010 Spin Workshop
by Marc de Jonge and Theo Ruys.
The tool can be downloaded from:
<pre>
<a href="http://code.google.com/p/spinja/">http://code.google.com/p/spinja/</a>
</pre>
<H3><TT>Ltl2Ba (optional)</TT></H3>A faster method to generate very small
never claims from LTL formulae, developed by Denis Oddoux and Paul Gastin is
available online in source form:
<pre>
<A href="http://spinroot.com/spin/Src/ltl2ba.tar.gz">http://spinroot.com/spin/Src/ltl2ba.tar.gz</A>
</pre>
The latest version can be obtained from the authors website via:
<pre>
<A href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php">http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php</A>
See also
<A href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php">http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php</A>
</pre>
The C source code can be linked with Spin, or run as a standalone tool.
<p>
For an overview of related conversion tools see:
<a href="http://spot.lip6.fr/wiki/LtlTranslationAlgorithms">http://spot.lip6.fr/wiki/LtlTranslationAlgorithms</a>
<p>
<H3><TT>Swarm (optional)</TT></H3>
See <a href="http://spinroot.com/swarm/">http://spinroot.com/swarm</a>.
<p>
<H3><TT>Runspin and Parsepan (optional)</TT></H3>
Two useful scripts by Theo Ruys, to help with setting up (and remembering)
configurations for multiple verification runs:
<ul>
<li><a href="http://github.com/tcruys/runspin">runspin</a>
<li><a href="http://github.com/tcruys/parsepan">parsepan</a>
</ul>
</ul>
<HR>
<TT>
<TABLE cols=3 width="100%">
<TBODY><TR>
<TD align=left><A href="http://spinroot.com/spin/whatispin.html"><TT>Spin HomePage</TT></A></TD>
<TD></TD>
<TD align=right><FONT size=3><B><TT>
(Page Last Updated: 1 November 2015)
</TT></B></FONT></TD>
</TR></TBODY>
</TABLE>
</TT>
</td><td width=15%> </td></tr></table>
</BODY>
</HTML>
|
