Call to NuSMV fails: error while loading shared libraries libreadline.so.6 (part 2)

[ritaalamino]

I am trying to install in ChromeOS, using beta Linux (Crostini). Everything did fine, but I have a problem with a package. NuSMV on Python3.

I have tried installing pynumsv with pip3, maybe I should change something on settings.cfg (nusmv = ./NuSMV-a/NuSMVa_linux64) but I am not sure how to solve it.

[hklarner]

at the bottom it says "call to NuSMV failed." and it states the command that was used for the test. can you run the command ./usr/lib/<and so on>/NuSMVa_linux64 and post the output here? It should look like this (but obviously doesn't):

*** This is NuSMV-A (compiled on Mon Aug  7 15:29:54 2017)
*** NuSMV-A is an extension of NuSMV 2.6.0
*** For more information on NuSMV-A see <http://github.com/hklarner/NuSMV-A>
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <[email protected]>.
*** Please report bugs to <Please report bugs to <[email protected]>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver. 
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
Input file is (null). You must set the input file before.
Aborting batch mode
NuSMV terminated by a signal
Aborting batch mode

[ritaalamino]

it returned this;

also saw the solution in #7
tried to run
sudo apt-get install libreadline6:i386
and
sudo apt-get install libreadline-dev
still don't work.

and tried also this this codeline electron-userland/electron-builder#993
sudo ln -s libreadline.so.7.0 libreadline.so.6

[hklarner]

Issues with libreadline appear frequently. Usually its resolved by softlinking. It's a good attempt to copy the file in the NuSMV folder but the program doesn't look for shared objects in its root folder.

(1) I will ask someone who has resolved this recently to post instructions
(2) I will ask the NuSMV guys directly to post advice on this issue

[Lauracf]

I had similar problems and I could solve it by creating a softlink. I think the problem might be that the link needs to be created in the right directory so NuSMV can find it.
So first you go to the directory where the link should be:
cd /lib/x86_64-linux-gnu
And then you create the softlink:
sudo ln -s libreadline.so.7.0 libreadline.so.6

[ritaalamino]

It did work. Thank you.

[hklarner]

thanks @Lauracf for your post and @ritaalamino I am reopening the issue to keep it visible in the list of issues. I added the tag "solved".

[carissableker]

@hklarner is readline needed for PyBoolNet? If not, it may be a solution to recompile NumSMV-a.

In NuSMV (and I assume your fork NuSMV-a) readline can be disabled when compiling. See in CMakeLists.txt L18 and optional arguments to cmake at README.txt L366.

cmake .. -ENABLE_READLINE=OFF

[carissableker]

Another fix (only for Linux and Mac I think), that does not require sudo and retains readline:

1. create a lib directory: mkdir lib
2. Symlink to the OS libreadline to lib/libreadline.so.6: ln -s /lib/x86_64-linux-gnu/libreadline.so.X ./lib/libreadline.so.6
3. Add add that directory to the LD_LIBRAY_PATH: LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$PWD/lib/"
   or add export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$PWD/lib/" to your startup script (e.g. .bashrc)

This worked for me, and maybe could be added to setup.py.

[hklarner]

libreadline is not needed for PyBoolNet directly, only for nusmv-a. I think that without libreadline nusmv can not be called with command line arguments. But i am not sure. Recompiling nusmv-a is a problem because I can not compile for mac and windows because I only have a linux machine.