Dear spot maintainers,
I am trying to compile spot v2.9.7 from source but my build errors due to
latexmk not being available in the environment. From what I understand from
the log, it is used in making the doc, is there a way to skip this step in
the build?
I built it on ubuntu (gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0) and it did
not complain about latexmk, this only happened when changing to a new
platform (the end goal is to cross compile it).
Any help would be appreciated,
Maxime
I am using a linux platform with gcc:
x86_64-linux-gnu-g++ (GCC) 9.1.0
Here is what I run:
./configure --prefix=${prefix}/spot-build --build=${MACHTYPE}
--host=${target} --disable-python
make -j${nproc} && make install
Here is the partial log:
```
[15:46:03] Making all in doc
[15:46:03] make[2]: Entering directory
'/workspace/srcdir/jlspot/spot-2.9.7/doc'
[15:46:03] Making all in tl
[15:46:03] make[3]: Entering directory
'/workspace/srcdir/jlspot/spot-2.9.7/doc/tl'
[15:46:03] BIBINPUTS='./..' latexmk -pdf -ps- -dvi- -pvc- -e
'$bibtex_use=2' -e '$pdflatex="pdflatex %O
\"\\def\\SpotVersion{2.9.7}\\input{%S}\""' ./tl.tex
[15:46:03] /bin/sh: latexmk: not found
[15:46:03] make[3]: *** [Makefile:1399: tl.pdf] Error 127
[15:46:03] make[3]: Leaving directory
'/workspace/srcdir/jlspot/spot-2.9.7/doc/tl'
[15:46:03] make[2]: *** [Makefile:1319: all-recursive] Error 1
[15:46:03] make[2]: Leaving directory
'/workspace/srcdir/jlspot/spot-2.9.7/doc'
[15:46:03] make[1]: *** [Makefile:1341: all-recursive] Error 1
[15:46:03] make[1]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7'
````
Hi there ADL & all,
Apologies for the not-really-spot question, but the expertise on this
list is quite unique! I'm about to embark on a new project that
relies on BDD. My only experience with BDD libraries was through
using Spot, so I'm familiar with BuDDy, but that's it.
Starting something fresh, I'm pondering what's the best C++ BDD
library available nowadays. I axed through BuDDy and refactored it so
that it's template-only and encapsulated the global variables in a
class (hoping for some performance boost from inlining). While I'm
fairly happy with the result, I now realize that there's been some
progress in the BDD landscape since 1997—crazy! This paper:
https://www.tvandijk.nl/pdf/2015setta.pdf
by the author of Sylvan seems to indicate that Sylvan offers good
performances on a single core, and great perf on multicore. It also
comes with a nice C++ interface.
I guess my question is: If you had to go from scratch today, which BDD
library would you use?
Cheers,
M.
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
