Sitemap for Spot
autfilt
dstar2tgba
genltl
ltl2tgba
ltl2tgta
ltlcross
ltldo
ltlfilt
ltlgrind
randaut
randltl
- Alternation removal
- Citing Spot
- Code Examples
- Command-line tools installed by Spot
- Common input and output options for LTL/PSL formulas
- Common output options for automata
- Compiling against Spot
- Concepts
- Constructing and transforming formulas
- Converting Rabin (or Other) to Büchi, and simplifying it
- Converting a never claim into HOA
- Creating an alternating automaton by adding states and transitions
- Creating an automaton by adding states and transitions
- Custom print of an automaton
- Explicit vs. on-the-fly: two interfaces for exploring automata
- Exploring the temporal hierarchy of Manna & Pnueli
- Implementing an on-the-fly Kripke structure
- Installing Spot
- Iterating over alternating automata
- Parsing and Printing LTL Formulas
- Reading and writing CSV files
- Relabeling Formulas
- SAT-based Minimization of Deterministic ω-Automata
- Spot: a platform for LTL and ω-automata manipulation
- Support for the Hanoi Omega Automata (HOA) Format
- Testing the equivalence of two formulas
- Translating an LTL formula into a monitor
- Translating an LTL formula into a never claim
- Upgrading from Spot 1.2.6