Bonjour Maxime,

On Fri, Oct 5, 2018 at 9:33 AM Maxime Bouton boutonm@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!