# -*- 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 and convert 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-Büchi translators.
- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL
  formula
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert deterministic Rabin or Streett automata into
  Büchi automata.
- [[file:randaut.org][=randaut=]] Generate random automata.
- [[file:autfilt.org][=autfilt=]] Filter and convert automata.
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
  and [[file:oaut.org][output]] interfaces.

* 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