how to configure stormpy

[xhajnal]

Hello guys, this one is hopefully the last one :D

So I installed prophesy and all dependencies (+tests) without problem:
following prerequisites in the latest commit of a given branch
Carl master14
carl-parser master14
stormpy master
storm stable
compilation and tests with no errors

however when running:

$ python scripts/parameter_synthesis.py load-problem model.pm property.pctl sample
	Traceback (most recent call last):
	  File "scripts/parameter_synthesis.py", line 668, in <module>
	    state = parameter_synthesis.main(standalone_mode=False)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 955, in main
	    rv = self.invoke(ctx)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 1526, in invoke
	    super().invoke(ctx)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 1279, in invoke
	    return ctx.invoke(self.callback, **ctx.params)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 710, in invoke
	    return callback(*args, **kwargs)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/decorators.py", line 71, in new_func
	    return ctx.invoke(f, obj, *args, **kwargs)
	  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 710, in invoke
	    return callback(*args, **kwargs)
	  File "scripts/parameter_synthesis.py", line 99, in parameter_synthesis
	    state.mc = make_modelchecker(state.mc)
	  File "scripts/parameter_synthesis.py", line 625, in make_modelchecker
	    raise RuntimeError("Selected Stormpy as the model checker, however the stormpy dependency is not configured. Use '--mc' to select another model checker, or configure stormpy.")
	RuntimeError: Selected Stormpy as the model checker, however the stormpy dependency is not configured. Use '--mc' to select another model checker, or configure stormpy.

How do I configure stormpy?
Or should I rather checkout Storm+stormpy release 1.6.3?

[volkm]

Prophesy should write a config in prophesy.cfg. Try adapting this config and see if this already helps.

[xhajnal]

Thanks,

I filled following lines as there is no stompy in items:

storm = /home/matej/Git/storm/build/bin/storm
storm-pars = /home/matej/Git/storm/build/bin/storm-pars

but now I got

Stormpy was the preferred model checker, but is not available. Try to fall back to storm.
{}
Traceback (most recent call last):
  File "scripts/parameter_synthesis.py", line 668, in <module>
    state = parameter_synthesis.main(standalone_mode=False)
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 955, in main
    rv = self.invoke(ctx)
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 1547, in invoke
    rv.append(sub_ctx.command.invoke(sub_ctx))
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 1279, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 710, in invoke
    return callback(*args, **kwargs)
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/decorators.py", line 71, in new_func
    return ctx.invoke(f, obj, *args, **kwargs)
  File "/home/matej/anaconda3/envs/py38/lib/python3.8/site-packages/click-8.0.0a1-py3.8.egg/click/core.py", line 710, in invoke
    return callback(*args, **kwargs)
  File "scripts/parameter_synthesis.py", line 115, in load_problem
    state.problem_description.model = open_model_file(model_file)
  File "/home/matej/Git/prophesy/prophesy/input/modelfile.py", line 25, in open_model_file
    return PrismFile(location)
  File "/home/matej/Git/prophesy/prophesy/input/modelfile.py", line 106, in __init__
    check_filepath_for_reading(location)
  File "/home/matej/Git/prophesy/prophesy/util.py", line 146, in check_filepath_for_reading
    raise IOError(filedescription_string + " not found at " + filepath)
OSError: file not found at model.pm

plus some more errors when running scripts/tests
python -m pytest scripts/tests

=========================================================================================== short test summary info ============================================================================================
FAILED scripts/tests/test_find_feasible_solution.py::test_script_sfsmt[brp-brp_16-2-0.9-above] - AssertionError: Stormpy was the preferred model checker, but is not available. Try to fall back to storm.
FAILED scripts/tests/test_find_feasible_solution.py::test_script_sfsmt[brp-brp_16-2-0.9-below] - AssertionError: Stormpy was the preferred model checker, but is not available. Try to fall back to storm.
FAILED scripts/tests/test_parameter_space_partitioning.py::test_script_sfsmt[kydie-kydie--property1-kydie-15/100-z3-quads] - AssertionError: Stormpy was the preferred model checker, but is not available. T...
FAILED scripts/tests/test_parameter_space_partitioning.py::test_script_sfsmt[kydie-kydie--property1-kydie-15/100-z3-rectangles] - AssertionError: Stormpy was the preferred model checker, but is not availab...

[xhajnal]

As stompy was not in PATH (only pythonpaths) it was not added when running python setup.py develop --search-path PATH,

"fixed" by removing prophesy.cfg and dependencies.cfg and running
python setup.py develop --search-path <PATH_TO_STOMPY_MAINDIR>

unfortunately, now the tests got stuck:

matej@Skadi:~/Git/prophesy$ python -m pytest scripts/tests
============================= test session starts ==============================
platform linux -- Python 3.8.5, pytest-6.1.2, py-1.9.0, pluggy-0.13.1
rootdir: /home/matej/Git/prophesy, configfile: tox.ini
collected 41 items                                                             

scripts/tests/test_complete_pipeline.py x

for more than an hour