5 Oct
2018
5 Oct
'18
2:18 p.m.
Bonjour Maxime,
On Fri, Oct 5, 2018 at 9:33 AM Maxime Bouton <boutonm(a)stanford.edu> wrote:
Dear Spot maintainers,
I am a PhD student at the Stanford Intelligent Systems Lab (SISL), we are interested in
implementing a Julia wrapper for Spot. So far I have prototyped a very simple version that
calls the binary to write to a .hoa file, then parse the .hoa file and build an automata
structure, I tried it on very simple formulas.
In the coming day I am going to call the c++ api of spot from Julia and extract the
datastructure from it instead of writing my own parser. The idea would be that I can then
manipulate the automata using native Julia objects.
I am looking at this example from the documentation:
https://spot.lrde.epita.fr/tut50.html
The explicit interface seems like what I am looking for, please let me know if I am
missing other relevant examples.
Also this
https://spot.lrde.epita.fr/tut21.html
In the development version of Spot, there is a new page that describes
how the automata are stored:
https:// spot-dev .lrde.epita.fr/ipynb/twagraph-internals.html
(remove the spaces — I don't want Google to see links to this staging server.)
If you are aware of some people working on this please
let us know, we would be happy to contribute and join forces. Would you agree if we name
the Julia package Spot.jl ?
No problem. I'm not aware of any existing bindings besides Python.
I suspect the first issue you'll encounter is that we use BDDs to
label edges. It might make sense to write bindings for our fork of
the BuDDy library first.
(In case some Julia bindings for BuDDy already exist: the C API of the
original BuDDy library is mostly identical to ours. We have a few
additional functions and some substantial changes to the
implementation. Our C++ interface is also different.)
Good luck!
--
Alexandre Duret-Lutz