d02ee34e10
Suggested by Akim Demaille. Fixes #171. * bin/man/spot.x, bin/spot.cc: New files. * bin/man/Makefile.am, bin/Makefile.am: Add them. * doc/org/tools.org, NEWS: Mention the new page.
113 lines
4.8 KiB
Org Mode
113 lines
4.8 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}}
|
|
#+SETUPFILE: setup.org
|
|
#+HTML_LINK_UP: index.html
|
|
|
|
This document introduces command-line tools that are installed with
|
|
the Spot library. We give some examples to highlight possible
|
|
use-cases but shall not attempt to cover all features exhaustively
|
|
(please check the man pages for further inspiration).
|
|
|
|
* Conventions
|
|
|
|
For technical reasons related to the way we generate these pages, we
|
|
use the following convention when rendering shell commands. The
|
|
commands issued to the shell are formatted like this with a cyan line
|
|
on the left:
|
|
|
|
#+NAME: helloworld
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
echo Hello World
|
|
#+END_SRC
|
|
|
|
And the output of such a command is formatted as follows, with a
|
|
magenta line on the left:
|
|
|
|
#+RESULTS: helloworld
|
|
: Hello World
|
|
|
|
Parts of these documents (e.g., lists of options) are actually the
|
|
results of shell commands and will be presented as above, even if the
|
|
corresponding commands are hidden.
|
|
|
|
* Documentation common to multiple tools
|
|
|
|
- [[file:ioltl.org][common input and output options for LTL/PSL formulas]]
|
|
- [[file:oaut.org][common output options for automata]]
|
|
- [[file:hoa.org][input and output support for the HOA format]]
|
|
|
|
* Command-line tools
|
|
|
|
- [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas.
|
|
- [[file:ltlfilt.org][=ltlfilt=]] Filter, convert, and transform LTL/PSL formulas.
|
|
- [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns.
|
|
- [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into Büchi automata.
|
|
- [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata.
|
|
- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-automata translators.
|
|
- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL
|
|
formula.
|
|
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into
|
|
variants of Büchi automata.
|
|
- [[file:randaut.org][=randaut=]] Generate random \omega-automata.
|
|
- [[file:autfilt.org][=autfilt=]] Filter, convert, and transform \omega-automata.
|
|
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
|
|
and [[file:oaut.org][output]] interfaces.
|
|
|
|
* Man pages
|
|
|
|
In addition to the above illustrated documentation, Spot also installs
|
|
man pages for all these tools. These man pages are mostly generated
|
|
automatically from the =--help= output of each tool, and often
|
|
completed with additional text (like examples or bibliography). For
|
|
convenience, you can browse their HTML versions:
|
|
|
|
[[./man/autfilt.1.html][=autfilt=]](1),
|
|
[[./man/dstar2tgba.1.html][=dstar2tgba=]](1),
|
|
[[./man/genltl.1.html][=genltl=]](1),
|
|
[[./man/ltl2tgba.1.html][=ltl2tgba=]](1),
|
|
[[./man/ltl2tgta.1.html][=ltl2tgta=]](1),
|
|
[[./man/ltlcross.1.html][=ltlcross=]](1),
|
|
[[./man/ltldo.1.html][=ltldo=]](1),
|
|
[[./man/ltlfilt.1.html][=ltlfilt=]](1),
|
|
[[./man/randaut.1.html][=randaut=]](1),
|
|
[[./man/randltl.1.html][=randltl=]](1),
|
|
[[./man/spot-x.7.html][=spot-x=]](7),
|
|
[[./man/spot.7.html][=spot=]](7).
|
|
|
|
* Advanced use-cases
|
|
|
|
- [[file:csv.org][Reading and writing CSV files]]
|
|
- [[file:satmin.org][SAT-based minimization of Deterministic ω-Automata]]
|
|
|
|
* Citing
|
|
|
|
If you want to refer to these tools in an article, please cite one of
|
|
the following articles:
|
|
|
|
- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/.
|
|
In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam,
|
|
Oct. 2013. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]])
|
|
|
|
This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
|
|
|
|
- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
|
|
Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
|
|
([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])
|
|
|
|
This describes the translation from LTL to TGBA used by =ltl2tgba=
|
|
and =ltl2tgta=.
|
|
|
|
- *Model checking using generalized testing automata*, /Ala Eddine Ben
|
|
Salem/, /Alexandre Duret-Lutz/, and /Fabrice Kordon/. In
|
|
Transactions on Petri Nets and Other Models of Concurrency (ToPNoC
|
|
VI), 7400:94--112, 2012. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#bensalem.12.topnoc][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/bensalem.12.topnoc.pdf][pdf]])
|
|
|
|
This describes the generalized testing automata produced by =ltl2tgta=.
|
|
|
|
|
|
Check the man page for each tool for additional references about the
|
|
algorithms or data sources used.
|
|
|
|
# LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl
|
|
# LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval
|
|
# LocalWords: setenv concat getenv setq
|