Stormpy Installation: libcarl not being recognized after switching directories

[kevinzhao79]

I'm currently trying to install stormpy, and am running into installation issues. I first tried installing it in a directory /Users/kevinzhao79/People and Robots Lab/RAG-with-Verification/ but quickly ran into issues because one of my folders in the path ("People and Robots Lab") had spaces which interfered with pathing. I then moved all my files into a separate directory (/Users/kevinzhao79/UW-Research/LLM-Verification/) and ran the entire setup for stormpy again (carl-storm, pycarl, and Storm installations all worked) but when tried running pip install -ve . in the stormpy directory I got this error:

ImportError: dlopen(/Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/.eggs/pycarl-2.2.0-py3.11-macosx-14.0-arm64.egg/pycarl/core.cpython-311-darwin.so, 0x0002): Library not loaded: @rpath/libcarl.14.27.dylib

Referenced from: <43E28EA6-4FBA-3D6E-8A83-8750151774D4> /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/.eggs/pycarl-2.2.0-py3.11-macosx-14.0-arm64.egg/pycarl/core.cpython-311-darwin.so

Reason: tried: '/Users/kevinzhao79/People and Robots Lab/RAG-with-Verification/carl-storm/build/libcarl.14.27.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/Users/kevinzhao79/People and Robots Lab/RAG-with-Verification/carl-storm/build/libcarl.14.27.dylib' (no such file), '/Users/kevinzhao79/People and Robots Lab/RAG-with-Verification/carl-storm/build/libcarl.14.27.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/Users/kevinzhao79/People and Robots Lab/RAG-with-Verification/carl-storm/build/libcarl.14.27.dylib' (no such file), '/opt/homebrew/lib/libcarl.14.27.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/opt/homebrew/lib/libcarl.14.27.dylib' (no such file), '/opt/homebrew/lib/libcarl.14.27.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/opt/homebrew/lib/libcarl.14.27.dylib' (no such file)

Clearly, it is still trying to find my libcarl version from my old path, despite me relocating all my files and re-downloading a fresh copy of stormpy and all its dependencies. How am I able to refresh this in order for stormpy to recognize my new file path and compile correctly?

[sjunges]

Hey!

This is unfortunate. Stormpy uses the cmake registry to find these libraries: You could remove the outdated entries from ~/.cmake/packages/carl and ~/.cmake/packages/storm.

Best, Sebastian

[kevinzhao79]

Hi Sebastian!

I tried both changing the outdated versions to the new paths, and deleting the old paths, but the problem still persists. Is there a way for me to regenerate the registries to be up-to-date?

[volkm]

You can try removing all files in .cmake/packages/ and then executing the cmake & make steps once again for the carl and storm repositories. As the build files are still there, it should update the paths but not completely rebuild everything.

[kevinzhao79]

I just tried this, and while the file in .cmake/packages/carl contained the right path /Users/kevinzhao79/UW-Research/LLM-Verification/carl-storm/build and the same with .cmake/packages/storm /Users/kevinzhao79/UW-Research/LLM-Verification/storm/build running the setup command still did not fix the issue, even when deleting and re-cloning stormpy and setting up the venv again.

Could the setup of my parent directory have anything to do with this issue?

[volkm]

Can you execute the storm binaries without issue or do you already get the same problem? You can also try to provide the paths to the carl/storm directory when building pycarl/stormpy, see here.

[kevinzhao79]

Re-compiling pycarl while specifying the path to carl-storm directory fixed the developing issue, but there were other testing issues that arose:

` _ TestStateLabeling.test_label __

self = <test_labeling.TestStateLabeling object at 0x10b693f10>

def test_label(self):
    program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
    formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)
    model = stormpy.build_model(program, formulas)
    labeling = model.labeling
    labels = labeling.get_labels()

  assert len(labels) == 3

E AssertionError: assert 4 == 3 E + where 4 = len({'deadlock', 'init', 'one', 'unexplored'})

tests/storage/test_labeling.py:28: AssertionError __ TestStateLabeling.test_label_parametric __

self = <test_labeling.TestStateLabeling object at 0x10b690450>

def test_label_parametric(self):
    program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
    formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program)
    model = stormpy.build_parametric_model(program, formulas)
    labels = model.labeling.get_labels()

  assert len(labels) == 3

E AssertionError: assert 4 == 3 E + where 4 = len({'(s = 5)', 'deadlock', 'init', 'unexplored'})

tests/storage/testlabeling.py:41: AssertionError ----------------------------------------------------------------------- Captured stdout call ------------------------------------------------------------------------ WARN (FormulaParserGrammar.cpp:333): Identifier `T' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'T' might not be parsed correctly. ____ example_gspns_01 __

def example_gspns_01():
    # Load a GSPN from file (PNML format)
    import_path = stormpy.examples.files.gspn_pnml_simple
    gspn_parser = stormpy.gspn.GSPNParser()

  gspn = gspn_parser.parse(import_path)

E RuntimeError: UnexpectedException: Storm is not compiled with XML support: /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/lib/stormpy/examples/files/gspn/gspn_simple.pnml can not be parsed

examples/gspns/01-gspns.py:12: RuntimeError ----------------------------------------------------------------------- Captured stdout call ------------------------------------------------------------------------ ERROR (GspnParser.cpp:77): Storm is not compiled with XML support: /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/lib/stormpy/examples/files/gspn/gspnsimple.pnml can not be parsed ____ doc/source/doc/gspns.ipynb::Cell 0 ____ Notebook cell execution failed Cell 0: Cell execution caused an exception

Input:

import stormpy import stormpy.gspn import stormpy.examples import stormpy.examples.files

import_path = stormpy.examples.files.gspn_pnml_simple gspn_parser = stormpy.gspn.GSPNParser() gspn = gspn_parser.parse(import_path)

Traceback:

---

RuntimeError Traceback (most recent call last) Cell In[1], line 8 6 import_path = stormpy.examples.files.gspn_pnml_simple 7 gspn_parser = stormpy.gspn.GSPNParser() ----> 8 gspn = gspn_parser.parse(import_path)

RuntimeError: UnexpectedException: Storm is not compiled with XML support: /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/lib/stormpy/examples/files/gspn/gspn_simple.pnml can not be parsed

----------------------------------------------------------------------- Captured stdout call ------------------------------------------------------------------------ ERROR (GspnParser.cpp:77): Storm is not compiled with XML support: /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/lib/stormpy/examples/files/gspn/gspnsimple.pnml can not be parsed ____ doc/source/doc/gspns.ipynb::Cell 1 ____ Notebook cell execution failed Cell 1: Cell execution caused an exception

Input:

print("Name of GSPN: {}.".format(gspn.get_name()))

Traceback:

---

NameError Traceback (most recent call last) Cell In[1], line 1 ----> 1 print("Name of GSPN: {}.".format(gspn.get_name()))

NameError: name 'gspn' is not defined

____ doc/source/doc/gspns.ipynb::Cell 2 _____ Notebook cell execution failed Cell 2: Cell execution caused an exception

Input:

print("Number of places: {}.".format(gspn.get_number_of_places()))

Traceback:

---

NameError Traceback (most recent call last) Cell In[1], line 1 ----> 1 print("Number of places: {}.".format(gspn.get_number_of_places()))

NameError: name 'gspn' is not defined

____ doc/source/doc/gspns.ipynb::Cell 3 _____ Notebook cell execution failed Cell 3: Cell execution caused an exception

Input:

print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))

Traceback:

---

NameError Traceback (most recent call last) Cell In[1], line 1 ----> 1 print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))

NameError: name 'gspn' is not defined

____ doc/source/doc/gspns.ipynb::Cell 4 _____ Notebook cell execution failed Cell 4: Cell execution caused an exception

Input:

print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))

Traceback:

---

NameError Traceback (most recent call last) Cell In[1], line 1 ----> 1 print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))

NameError: name 'gspn' is not defined

====================================================================== short test summary info ====================================================================== FAILED tests/storage/test_labeling.py::TestStateLabeling::test_label - AssertionError: assert 4 == 3 FAILED tests/storage/test_labeling.py::TestStateLabeling::test_label_parametric - AssertionError: assert 4 == 3 FAILED examples/gspns/01-gspns.py::example_gspns_01 - RuntimeError: UnexpectedException: Storm is not compiled with XML support: /Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/lib/stormpy/examples/files/gs... FAILED doc/source/doc/gspns.ipynb::Cell 0 FAILED doc/source/doc/gspns.ipynb::Cell 1 FAILED doc/source/doc/gspns.ipynb::Cell 2 FAILED doc/source/doc/gspns.ipynb::Cell 3 FAILED doc/source/doc/gspns.ipynb::Cell 4 ============================================================= 8 failed, 385 passed, 8 skipped in 53.87s ============================================================= `

I checked #92 #167 and moves-rwth/storm#559, and I wasn't sure if there was a fix on my end that wasn't already fixed when the latest versions of storm ands stormpy were released.

Additionally, when trying to run a script that uses stormpy:

import stormpy

prism_program = stormpy.parse_prism_program("./ferryman_solution.prism")
model = stormpy.build_model(prism_program)

print(f"Number of states: {model.nr_states}")
print(f"Number of transitions: {model.nr_transitions}")
print(f"Labels: {model.labeling.get_labels()}")

I get this error: Traceback (most recent call last): File "/Users/kevinzhao79/UW-Research/LLM-Verification/verifier.py", line 3, in <module> prism_program = stormpy.parse_prism_program("./ferryman_solution.prism") ^^^^^^^^^^^^^^^^^^^^^^^^^^^ AttributeError: module 'stormpy' has no attribute 'parse_prism_program'

[volkm]

Good to hear that the first issue is resolved now. The first pair of failing tests is a current issue and can be ignored from your side. The second pair of tests is due to a missing support for XML parsing, only needed for Petri nets. You can ignore this one as well.

[volkm]

The last issue is more critical because it prevents you from continuing. I am a bit confused because the same function seems to work in the tests you ran. Are you using the same environment for the tests and running the script?

[volkm]

Can you run some of the example in the examples/ directory?

[kevinzhao79]

I tried running both the DTMC and POMDP examples, and both of them gave a error: no module found named stormpy.

(env) (base) kevinzhao79@Kevins-Air LLM-Verification % cd stormpy/examples/building_dtmcs 
(env) (base) kevinzhao79@Kevins-Air building_dtmcs % ls
01-building-dtmcs.py    __pycache__
(env) (base) kevinzhao79@Kevins-Air building_dtmcs % python3 01-building-dtmcs.py 
Traceback (most recent call last):
  File "/Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/examples/building_dtmcs/01-building-dtmcs.py", line 1, in <module>
    import stormpy
ModuleNotFoundError: No module named 'stormpy'
(env) (base) kevinzhao79@Kevins-Air building_dtmcs % ls
01-building-dtmcs.py    __pycache__
(env) (base) kevinzhao79@Kevins-Air building_dtmcs % cd ..
(env) (base) kevinzhao79@Kevins-Air examples % ls
01-getting-started.py   __pycache__             building_mas            exploration             pomdp                   simulator
02-getting-started.py   analysis                building_mdps           gspns                   reward_models
03-getting-started.py   building_ctmcs          building_models         highlevel_models        schedulers
04-getting-started.py   building_dtmcs          dfts                    parametric_models       shortest_paths
(env) (base) kevinzhao79@Kevins-Air examples % cd pomdp
(env) (base) kevinzhao79@Kevins-Air pomdp % ls
01-pomdps.py                    __pycache__                     high-level-observations.py
(env) (base) kevinzhao79@Kevins-Air pomdp % python3 01-pomdps.py 
Traceback (most recent call last):
  File "/Users/kevinzhao79/UW-Research/LLM-Verification/stormpy/examples/pomdp/01-pomdps.py", line 1, in <module>
    import stormpy
ModuleNotFoundError: No module named 'stormpy'
(env) (base) kevinzhao79@Kevins-Air pomdp % 

I'm using the same venv for both my personal script and the example script. I'm not sure if it affects anything, but my stormpy and its dependency folders are inside the same folder as my project:

LLM-Verification

• carl-storm
• pycarl
• Storm
• stormpy
• (my other files)

[volkm]

The folder structure should be fine. Does pip list give you pycarl and stormpy as installed packages?

[kevinzhao79]

Ah, I see. pip didn't recognize stormpy after building it through python3 setup.py develop, so I used pip install -ve . instead and pip recognized it. Re-running the examples was successful and stormpy is working again. Thanks for the help! Marking as closed.

[volkm]

Glad to hear it is working for you now. Good luck with your scripts.