Spot

This package provides Julia bindings to the Spot library for LTL and automata manipulation. It relies on CxxWrap.jl to interface julia with the Spot c++ library. You can find the c++ code with the wrapped functions in spot_julia, and the build script for the jll file in Yggdrasil.

Installation

using Pkg; Pkg.add("Spot.jl")

For the rendering, Spot requires GraphViz and dot2tex to be installed.

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 and Mosé Giordano for all the help provided in cross compiling Spot.