Spot
This package provides Julia bindings to the Spot library for LTL and automata manipulation. It relies on Cxx.jl to interface julia with the Spot c++ library.
If you wish to use PyCall
instead and interact with the spot python bindings you should checkout the branch pycall
(linux only).
Installation
For the rendering, Spot requires GraphViz and dot2tex to be installed. In addition, the precompile binaries require gcc
7 or 8 (not needed for Mac).
using Pkg; Pkg.add("Spot.jl")
Usage
LTL Manipulation
Construct LTL formula using a non standard string literal:
f = ltl"FG a -> FG b"
The formula will be automatically parsed by Spot.
LTL to Automata Translation
using Spot
ltl = "FG A"
translator = LTLTranslator(deterministic=true)
a = translate(translator, ltl)
Tutorial
A basic tutorial is available in docs/spot_basic_tutorial.ipynb
Notes
Right now, the wrapping of all the c++ functions present in libspot
is not automatic.
Every function can be called using the Cxx interface.
If you need to wrap a function that has not been wrapped yet, feel free to submit a Pull Request.
Acknowledgement
Thanks to Alexandre Duretz-Lutz for all the help provided.