hi!
With the aid of SPOT I am developing a counter-example guided synthesizer
in python. See [1] if interested for details.
My question is:
I am trying to parse twa_run in python,
namely, parse the labels of the each step (`spot.impl.step`).
Is there a python way to walk through BDD?
(The label is a simple cube expressed in BDD, and I need to convert it into
my internal structure)
(yes, this is rather a question about python interface for buddy)
(no, that is not feature request:) if not possible, I will simply print the
label and parse the string, that is not crucial)
[1]
The idea is
- guess the model,
- then model check it and get a counter-example
- then encode the counter-example into the "guesser" (which uses an SMT
solver)
thanks,
Ayrat
Hello,
I was trying to build Spot on a fresh ArchLinux install, when I came
across this issue:
> $ ./configure ...
> [...]
> checking for swig3.0... no
> checking for swig... no
> [...]
> $ make
> [...]
> swig -c++ -python -py3 -O -nofastproxy -MD -I../buddy/src -MF
> .deps/buddy_wrap.TPcxx ./buddy.i
> make[3]: swig: Command not found
> [...]
> make: *** [Makefile:1163: all] Error 2
If Spot requires Swig, shouldn't `configure` fail ? Or, if Swig is only
required for users who want to build the Python library, shouldn't the
latter not be included in the `all` rule ?
If that's any help, I attached my config.log.
Regards,
--
Clément 'Cigix' Gillard
"EAT SLEEP EAT REPEAT" @skrillbug_bot, 2016-06-23
