Code Examples

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

• Parsing and Printing LTL Formulas
• Relabeling Formulas
• Testing the equivalence of two LTL formulas
• Translating an LTL formula into a never claim
• Translating an LTL formula into a monitor
• Working with LTL formulas with finite semantics
• Converting a never claim into HOA
• Converting Rabin (or Other) to Büchi, and simplifying it
• Removing alternation
• Using ppLTLTT to work with pure-past LTL subformulas

• Constructing and transforming formulas
• Custom print of an automaton
• Printing a Büchi automaton in the "BA format"
• Creating an automaton by adding states and transitions
• Creating an alternating automaton by adding states and transitions
• Iterating over alternating automata
• Solving a safety game to decide direct simulation
• Creating an explicit Kripke structure
• Using the bdd_dict to associate atomic proposition to BDD variables, or allocate anonymous BDD variables (advanced)

• Explicit vs. on-the-fly: two interfaces for exploring automata
• Implementing an on-the-fly Kripke structure

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 operations
• automata.ipynb covers translation from formulas to automata, automata printing, and some lights transformations
• automata-io.ipynb shows how to save and read automata from files
• randaut.ipynb shows a simple case where the randaut commands generated random automata, which are displayed in a table before and after acceptance simplification
• accparse.ipynb exercises the acceptance condition parser
• acc_cond.ipynb documents the interface for manipulating acceptance conditions
• backprop.ipynb solving reachability games by backpropagation
• contains.ipynb demonstrates containment checks between formulas or automata
• split.ipynb illustrates various ways to split labels
• parity.ipynb documents algorithms for manipulating parity automata in Python
• games.ipynb illustrates support for games
• synthesis.ipynb illustrates support for game-based LTL reactive synthesis
• product.ipynb shows how to re-implement the product of two automata in Python
• randltl.ipynb demonstrates a Python-version of randltl
• gen.ipynb show how to generate families of LTL formulas (as done in genltl) or automata (genaut)
• decompose.ipynb illustrates the decompose_strength(), decompose_acc_scc() and decompose_scc() functions
• testingaut.ipynb shows the steps necessary to build a testing automaton
• ltsmin-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 the twa_run and twa_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.
• cav22-figs.ipynb figures from our CAV'22 tool paper.
• alternation.ipynb examples of alternating automata.
• stutter-inv.ipynb working with stutter-invariant formulas properties.
• satmin.ipynb Python interface for SAT-based minimization of deterministic ω-automata.
• twagraph-internals.ipynb Inner workings of the twa_graph class.
• aliases.ipynb Support for HOA aliases.
• zlktree.ipynb demonstration of Zielonka Trees and ACD
• given.ipynb simplification of automata given some apriori knowledge
• ltlf2dfa.ipynb translation between LTLf and MTDFA
• mtdtwa.ipynb support for MTBDD-based deterministic twa