NewsLetter 38 - September 24, 2003:

LTL to Buchi Automata Converters

Stefano Tonetta and Roberto Sebastiani have announced the availability of their tool called Modella (short for More Deterministic LTL to Automata), which can be used for the conversion of LTL formula into Buchi Automata.

Documentation, test results, and source code for the new tool are available from: http://www.science.unitn.it/~stonetta/modella.html

Besides the algorithm that is builtin to SPIN itself, include the ltl2ba tool developed by Denis Oddoux and Paul Gastin, written in C: http://spinroot.com/spin/Src/ltl2ba.tar.gz and the ``Temporal Massage Parlor'' tool written by Kousha Etessami, written in ML: http://www.bell-labs.com/topic/swdist/.

The New Book

The new Spin book is now finally available at all online booksellers.

   The Spin Model Checker
   Primer and Reference Manual. Gerard J. Holzmann
   Addison-Wesley, ISBN 0-32122-862-6, 608 pgs.

You can order the book at, for instance:
• click: amazon.com
• click: Addison-Wesley
• click: Barnes and Noble
Amazon ships the fastest, and offers free shipping on orders.
Barnes and Noble seem to have the lowest price at the moment, but they do charge for shipping.

Emacs Mode

Eric Engstrom ([email protected]) kindly provided an emacs mode for Promela models. It is now part of the Spin distribution and can be downloaded from:
http://spinroot.com/spin/Src/promela-mode.el

End of Newsletter Nr. 38.

Spin Homepage
Newsletter Index
To subscribe/unsubscribe: [email protected]