Sitemap for Spot
- Spot: a platform for LTL and ω-automata manipulation
- Citing Spot
- Concepts
- Installing Spot
- Command-line tools installed by Spot
autcross
autfilt
- Reading and writing CSV files
dstar2tgba
genaut
genltl
- Exploring the temporal hierarchy of Manna & Pnueli
- Support for the Hanoi Omega Automata (HOA) Format
- Common input and output options for LTL/PSL formulas
ltl2tgba
ltl2tgta
ltlcross
ltldo
ltlfilt
ltlgrind
ltlmix
ltlsynt
- Common output options for automata
randaut
randltl
- SAT-based Minimization of Deterministic ω-Automata
- Code Examples
- Compiling against Spot
- Parsing and Printing LTL Formulas
- Relabeling Formulas
- Constructing and transforming formulas
- Testing the equivalence of two 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
- Custom print of an automaton
- Creating an automaton by adding states and transitions
- Creating an alternating automaton by adding states and transitions
- Iterating over alternating automata
- Printing an automaton in "BA format"
- Converting Rabin (or Other) to Büchi, and simplifying it
- Alternation removal
- Using games to check a simulation
- Explicit vs. on-the-fly: two interfaces for exploring automata
- Implementing an on-the-fly Kripke structure
- Playing with explicit Kripke structures
- The bdd_dict interface (advanced topic)
- Upgrading from Spot 1.2.6