Code Examples
Table of Contents
This section contains code examples for using Spot. This is a work in progress. Feel free to send suggestions of small tasks you would like to see illustrated here.
If you have difficulties compiling the C++ examples, check out these instructions.
Reading the concepts page might help if you are not familiar with some of the objects manipulated here.
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++.
Examples in Python and C++
Examples in C++ only
Examples in Python only
In directory python/tests
, the Spot tarball contains a small
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.
formulas.ipynb
covers the basics of LTL/PSL formula parsing and printing, with some light operationsautomata.ipynb
covers translation from formulas to automata, automata printing, and some lights transformationsautomata-io.ipynb
shows how to save and read automata from filespiperead.ipynb
shows how to save and read automata output from other commands, using pipesrandaut.ipynb
shows a simple case where therandaut
commands generated random automata, which are displayed in a table before and after acceptance simplificationaccparse.ipynb
exercises the acceptance condition parseracc_cond.ipynb
documents the interface for manipulating acceptance conditionsproduct.ipynb
shows how to re-implement the product of two automata in Pythonrandltl.ipynb
demonstrates a Python-version ofrandltl
gen.ipynb
show how to generate families of LTL formulas (as done ingenltl
) or automata (genaut
)decompose.ipynb
illustrates thedecompose_strength()
,decompose_acc_scc()
anddecompose_scc()
functionstestingaut.ipynb
shows the steps necessary to build a testing automatonltsmin-dve.ipynb
loading a DiVinE model using the LTSmin interface.ltsmin-pml.ipynb
loading a Promela model using the LTSmin interface.word.ipynb
example for thetwa_run
andtwa_word
classes.highlighting.ipynb
shows how to highlight states or edges in automata.atva16-fig2a.ipynb
first example from our ATVA'16 tool paper.atva16-fig2b.ipynb
second example from our ATVA'16 tool paper.alternation.ipynb
examples of alternating automata.