Dear Spot team, 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. *For C++:* output from on-the-fly Kripke structure example (from https://spot.lrde.epita.fr/tut51.html) $ g++ -std=c++14 kripkeTest.cc -lspot -o kripkeTest Undefined symbols for architecture x86_64: "_bdd_addref_nc", referenced from: bdd::operator=(bdd const&) in kripkeTest-6ae779.o bdd::bdd(bdd const&) in kripkeTest-6ae779.o bdd::bdd(int) in kripkeTest-6ae779.o "_bdd_apply", referenced from: bdd_apply(bdd const&, bdd const&, int) in kripkeTest-6ae779.o "_bdd_delref_nc", referenced from: bdd::operator=(bdd const&) in kripkeTest-6ae779.o bdd::~bdd() in kripkeTest-6ae779.o "_bdd_not", referenced from: bdd_not(bdd const&) in kripkeTest-6ae779.o "_main", referenced from: implicit entry/start for main executable ld: symbol(s) not found for architecture x86_64 clang: *error: *linker command failed with exit code 1 (use -v to see invocation) (I could only run helloword.cc example) *For Python:* trying to run example on Kripke structure using source code from https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html $ python3 Python 3.7.3 (v3.7.3:ef4ec6ed12, Mar 25 2019, 16:39:00) [GCC 4.2.1 (Apple Inc. build 5666) (dot 3)] on darwin Type "help", "copyright", "credits" or "license" for more information.
import spot
import spot.ltsmin
spot.ltsmin.require('divine')
divine not available (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) Any insights would be appreciated. Best regards, Jiraphapa J.
Hi Jiraphapa, On Sun, Jun 2, 2019 at 7:48 PM Jiraphapa Jiravaraphan <jira.jiravaraphan@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
import spot import spot.ltsmin spot.ltsmin.require('divine')
$ python3 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
Hi Jiraphapa,
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 <https://gitlab.lrde.epita.fr/spot/divine-ltsmin-deb>
I just pushed few patches for MacOSX that should help you for compiling divine. Hope this helps, Etienne
participants (3)
-
Alexandre Duret-Lutz -
Jiraphapa Jiravaraphan -
Renault Etienne