Hi Jiraphapa,
On Sun, Jun 2, 2019 at 7:48 PM Jiraphapa Jiravaraphan
<jira.jiravaraphan(a)gmail.com> wrote:
I am trying to get Spot 2.7.4 running on macOS
(tarball installation), the command-line tools works properly on terminal, however, trying
to run Python and C++ examples does not work.
$ g++ -std=c++14 kripkeTest.cc -lspot -o kripkeTest
Undefined symbols for architecture x86_64:
"_bdd_addref_nc", referenced from:
This is part of the libbddx library that you should link with. Add
-lbddx to your compilation line, as mentionned on
https://spot.lrde.epita.fr/compile.html#orge42f3fd
For Python: trying to run example on Kripke structure
using source code from
https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html
$ python3
>> import spot
>> import spot.ltsmin
>> spot.ltsmin.require('divine')
divine not available
You should install divine in order to execute this example. The file
tests/ltsmin/README in the tarball contains some instructions about
this, but I seem to recall someone complaining about the fact that
most of the links in this file were dead now (patches welcome). For
what it's worth, the copy we use for generating the Debian package of
divine installed on the sandbox is at
https://gitlab.lrde.epita.fr/spot/divine-ltsmin-deb
(I think there has something to do with the path
because I have to manually add spot directory into pythonpath in order to be able to
import spot even if I use ./configure, make, make install)
It's hard to help without knowing exactly where you installed Spot
(options passed to ./configure). If its in a non-standard directory,
you will need to tell python about it.
Spot's README file has a "Troubleshooting installations" section that
might help a bit.
--
Alexandre Duret-Lutz