Spot is an object-oriented model checking library written in C++.
The website moved here.
Spot 1.99.1 is out, get it on the new website.
We are moving. The new website is now hosted at LRDE.
Here are several ways to play with the development version of Spot.
- Spot 1.2.6 is out. This includes a set of small fixes.
- Spot 1.2.5 is out. Some important LTL and PSL translation fixes and some new features for the command-line tools.
- Spot 1.2.4 is out. This maintenance release fixes some issues in the simplification of PSL formulas, translation of the fusion operator, and in the production of testing automata.
- Spot 1.2.3 is out. This is another maintenance release fixing minor issues, and improving statistics reported by our SAT-based minimization technique.
- Spot 1.2.2 is out. This maintenance release fixes a couple of bugs (mostly portability issues).
- Spot 1.2.1 is out. This release improves CSV output, and add CSV input support to several command-line tools.
- Spot 1.1.4 is out. This is yet another maintenance release, fixing a couple of nits in ltlcross, and the translation of some PSL formulas.
- Spot 1.1.3 is out. This maintenance release fix a couple of bugs and add support for the new style of neverclaim output by Spin 6.24 and later.
- Spot 1.1.2 is out. This maintenance release contains two minor fixes, and some documentation cleanup.
- Spot 1.1.1 is out. This release fixes a couple of bugs, and introduce a few small features mainly to the command-line tools.
- Spot 1.1 is out. This release adds compositional suspension, SCC-based optimizations for the degeneralization (two features of described in a paper to appear at Spin'13), a check for stuttering invariant LTL formulas, and some statistics about automata strenghts in ltlcross.
- Spot 1.0.2 is out. This is another maintenance release, fixing a few bugs (the most important being in the web interface).
- Spot 1.0.1 is out. This maintenance releases addresses a couple of minor bugs uncovered in the past three months.
Spot 1.0 is out. This release adds command-line user tools, reverse-simulation reduction, and support for testing automata.
Spot 0.9.2 is out. This maintenance release fixes minor bugs, improves speed, and add support for ltl3ba to the web interface.
- Spot 0.9.1 is out. This maintenance release fixes a couple of bugs, and implements slight speedups to the Couvreur/FM translation.
- Spot 0.9 is out. This adds support for the linear-time fragment of PSL, and contains several improvements to the LTL translation.
- Spot 0.8.3 is out. This maintenance release contains more bug fixes and improves the web interface for ltl2tgba.
- Spot 0.8.2 is out. This maintenance release fixes a couple of bugs, and implements slight speedups to the degeneralization and the Safra complementation.
- Spot 0.8.1 is out. This release fixes a couple more bugs.
- Spot 0.8 is out. This release fixes several bugs reported over the past months, and add a couple of new features like the ability to read DiVinE models.
- Spot 0.7.1 is out. It fixes a bug in WDBA minimization and a couple of minor issues.
- Spot 0.7 is out. Highlight in this release includes some speed improvements and an algorithm to minimize weak deterministic Büchi automata (WDBA).
- Spot 0.6 is out. This release adds support for the W (weak until) and M (strong release) operator, and improve several LTL simplifications rules as well as the degeneralization algorithm.
- Spot 0.5 is out. This release contains more than two years worth of work. It includes new LTL translations algorithms, complementations algorithms, and several bug fixes.
Spot 0.4 is out. These are mainly bug fixes, more LTL simplifications, and the emptiness check for our ACSD'07 paper.
Spot 0.3 is out. These are mainly bug fixes, and Spot's on-line LTL-to-TGBA translator now offers options to compute accepting runs.
Spot 0.2 is out. The main change is a new interface to pass EmptinessCheckOptions to the algorithms from the command line. (This is especially helpful with the emptiness-check benchmarks in directory bench/emptchk/.)