tut.org 4.36 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
#+TITLE: Code Examples
3
#+DESCRIPTION: Directory of code examples for using Spot in C++11, Python, and shell.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
#+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html


This section contains code examples for using Spot.  This is a work in
9
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
10
11
to see illustrated here.

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

15
16
17
Reading the [[file:concepts.org][concepts page]] might help if you are not familiar with some
of the objects manipulated here.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
18
19
20
21
22
23
24
* 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]]
25
- [[file:tut04.org][Testing the equivalence of two LTL formulas]]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
26
- [[file:tut10.org][Translating an LTL formula into a never claim]]
27
- [[file:tut20.org][Converting a never claim into HOA]]
28
- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29

30
31
32
* Examples in Python and C++

- [[file:tut03.org][Constructing and transforming formulas]]
33
- [[file:tut21.org][Custom print of an automaton]]
34
- [[file:tut22.org][Creating an automaton by adding states and transitions]]
35

36
37
38
39
* Examples in C++ only

- [[file:tut50.org][Explicit vs. on-the-fly: two interfaces for exploring automata]]

40
41
* Examples in Python only

42
In directory =python/tests=, the [[file:install.org][Spot tarball]] contains a small
43
44
45
46
47
48
49
50
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.

51
- [[https://spot.lrde.epita.fr/ipynb/formulas.html][=formulas.ipynb=]] covers the basics of LTL/PSL formula parsing and
52
  printing, with some light operations
53
- [[https://spot.lrde.epita.fr/ipynb/automata.html][=automata.ipynb=]] covers translation from formulas to automata,
54
  automata printing, and some lights transformations
55
56
- [[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
57
  commands, using pipes
58
- [[https://spot.lrde.epita.fr/ipynb/randaut.html][=randaut.ipynb=]] shows a simple case where the [[file:randaut.org][=randaut=]] commands
59
60
  generated random automata, which are displayed in a table before and
  after acceptance simplification
61
62
- [[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
63
  conditions
64
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
65
  in Python
66
67
- [[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
68
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing
69
  automaton
70
71
- [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface.
- [[https://spot.lrde.epita.fr/ipynb/ltsmin-pml.html][=ltsmin-pml.ipynb=]] loading a Promela model using the LTSmin interface.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
72
73
- [[https://spot.lrde.epita.fr/ipynb/word.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes.
- [[https://spot.lrde.epita.fr/ipynb/highlighting.html][=highlighting.ipynb=]] shows how to highlight states or edges in
74
  automata.
75
76
- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].