tut.org 3.13 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
#+TITLE: Code Examples
#+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html


This section contains code examples for using Spot.  This is a work in
8
progress.  Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestions of small tasks you would like
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
9
10
to see illustrated here.

11
12
13
If you have difficulties compiling the C++ examples, check out [[file:compile.org][these
instructions]].

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14
15
16
17
18
19
20
21
* Examples with Shell, Python, and C++

All the following pages show how to perform the same task using the
three interfaces supported by Spot: shell commands, Python, or C++.

- [[file:tut01.org][Parsing and Printing LTL Formulas]]
- [[file:tut02.org][Relabeling Formulas]]
- [[file:tut10.org][Translating an LTL formula into a never claim]]
22
- [[file:tut20.org][Converting a never claim into HOA]]
23
- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
24

25
26
27
* Examples in Python and C++

- [[file:tut03.org][Constructing and transforming formulas]]
28
- [[file:tut21.org][Custom print of an automaton]]
29
- [[file:tut22.org][Creating an automaton by adding states and transitions]]
30
31
32

* Examples in Python only

33
In directory =python/tests=, the [[file:install.org][Spot tarball]] contains a small
34
35
36
37
38
39
40
41
collection of IPython notebooks.  As the name of the directory implies,
these are part of the test suite for the Python bindings, however they
can be interesting to look at if you want to see more code examples.

For convenience, the following links offer static HTML renderings of
these notebooks, but we strongly suggest interactively evaluating the
real notebooks instead.

42
- [[https://spot.lrde.epita.fr/ipynb/formulas.html][=formulas.ipynb=]] covers the basics of LTL/PSL formula parsing and
43
  printing, with some light operations
44
- [[https://spot.lrde.epita.fr/ipynb/automata.html][=automata.ipynb=]] covers translation from formulas to automata,
45
  automata printing, and some lights transformations
46
47
- [[https://spot.lrde.epita.fr/ipynb/automata-io.html][=automata-io.ipynb=]] shows how to save and read automata from files
- [[https://spot.lrde.epita.fr/ipynb/piperead.html][=piperead.ipynb=]] shows how to save and read automata output from other
48
  commands, using pipes
49
- [[https://spot.lrde.epita.fr/ipynb/randaut.html][=randaut.ipynb=]] shows a simple case where the [[file:randaut.org][=randaut=]] commands
50
51
  generated random automata, which are displayed in a table before and
  after acceptance simplification
52
53
- [[https://spot.lrde.epita.fr/ipynb/accparse.html][=accparse.ipynb=]] exercises the acceptance condition parser
- [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][=acc_cond.ipynb=]] documents the interface for manipulating acceptance
54
  conditions
55
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
56
  in Python
57
58
59
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
- [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()= function
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the step necessary to build a testing
60
  automaton