./wip/spot, Library for omega automata manipulation and model checking

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 2.7.1, Package name: spot-2.7.1, Maintainer: jihbed.research

Spot is a library for LTL, omega-automata manipulation and model checking.

It has the following notable features:
* Support for LTL (several syntaxes supported) and a subset of the linear
fragment of PSL.
* Support for omega-automata with arbitrary acceptance condition.
* Support for transition-based acceptance (state-based acceptance is supported
by a reduction to transition-based acceptance).
* The automaton parser can read a stream of automata written in any of four
syntaxes (HOA, never claims, LBTT, DSTAR).
* Several algorithms for formula manipulation including: simplifying formulas,
testing implication or equivalence, testing stutter-invariance, removing some
operators by rewriting, translation to automata, testing membership to the
temporal hierarchy of Manna & Pnueli...
* Several algorithms for automata manipulation including: product, emptiness
checks, simulation-based reductions, minimization of weak-DBA, removal of
useless SCCs, acceptance-condition transformations, determinization, SAT-based
minimization of deterministic automata, etc.
* In addition to the C++ interface, most of its algorithms are usable via
command-line tools, and via Python bindings.
* One command-line tool, called ltlcross, is a rewrite of LBTT, but with support
for PSL and automata with arbitrary acceptance conditions.


Required to run:
[devel/doxygen]

Required to build:
[pkgtools/cwrappers]

Master sites:

RMD160: cacb4e4b9e73474b56221db0bec88835769ed493
Filesize: 7002.577 KB

Version history: (Expand)