moves-rwth / stormpy

Python Bindings for the Probabilistic Model Checker Storm
https://moves-rwth.github.io/stormpy/
GNU General Public License v3.0
30 stars 16 forks source link

Tests are failing if CLN is not available #114

Closed tquatmann closed 1 year ago

tquatmann commented 1 year ago

Especially relevant for Apple silicon users.

______________________________________________________________________________ TestParametric.test_constraints_collector ______________________________________________________________________________

self = <test_parametric.TestParametric object at 0x123649ad0>

    def test_constraints_collector(self):
        from pycarl.formula import FormulaType, Relation
        if stormpy.info.storm_ratfunc_use_cln():
>           import pycarl.cln.formula

tests/pars/test_parametric.py:82: 
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

    from . import _config

    if not _config.CARL_WITH_CLN:
>       raise ImportError("CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?")
E       ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?

../pycarl/lib/pycarl/cln/__init__.py:4: ImportError
_____________________________________________________________________________________ example_building_models_02 ______________________________________________________________________________________

    def example_building_models_02():

        import stormpy.pars
        if stormpy.info.storm_ratfunc_use_cln():
>           import pycarl.cln as pc

examples/building_models/02-building-models.py:14: 
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

    from . import _config

    if not _config.CARL_WITH_CLN:
>       raise ImportError("CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?")
E       ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?

../pycarl/lib/pycarl/cln/__init__.py:4: ImportError
____________________________________________________________________________________ example_parametric_models_02 _____________________________________________________________________________________

    def example_parametric_models_02():
        # Check support for parameters
        if not config.storm_with_pars:
            print("Support parameters is missing. Try building storm-pars.")
            return

        import stormpy.pars
        from pycarl.formula import FormulaType, Relation
        if stormpy.info.storm_ratfunc_use_cln():
>           import pycarl.cln.formula

examples/parametric_models/02-parametric-models.py:21: 
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

    from . import _config

    if not _config.CARL_WITH_CLN:
>       raise ImportError("CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?")
E       ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?

../pycarl/lib/pycarl/cln/__init__.py:4: ImportError
____________________________________________________________________________________ example_parametric_models_01 _____________________________________________________________________________________

    def example_parametric_models_01():
        # Check support for parameters
        if not config.storm_with_pars:
            print("Support parameters is missing. Try building storm-pars.")
            return

        import stormpy.pars
        from pycarl.formula import FormulaType, Relation
        if stormpy.info.storm_ratfunc_use_cln():
>           import pycarl.cln.formula

examples/pomdp/01-pomdps.py:23: 
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

    from . import _config

    if not _config.CARL_WITH_CLN:
>       raise ImportError("CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?")
E       ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?

../pycarl/lib/pycarl/cln/__init__.py:4: ImportError
======================================================================================= short test summary info =======================================================================================
FAILED tests/core/test_multiobjective.py::TestModelChecking::naive_api_double_no_plotting_test - assert 4 == 6
FAILED tests/pars/test_parametric.py::TestParametric::test_constraints_collector - ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?
FAILED examples/building_models/02-building-models.py::example_building_models_02 - ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?
FAILED examples/parametric_models/02-parametric-models.py::example_parametric_models_02 - ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?
FAILED examples/pomdp/01-pomdps.py::example_parametric_models_01 - ImportError: CLN is not available in the configured carl library! Did you configure carl with -DUSE_CLN_NUMBERS=ON?
============================================================================== 5 failed, 385 passed, 2 skipped in 31.01s ==============================================================================
volkm commented 1 year ago

It seems that Storm/stormpy is still compiled with support for CLN in RF. Is STORM_USE_CLN_RF enabled in Storm?

tquatmann commented 1 year ago

Well, in my case we basically overwrite the settings here.

STORM_USE_CLN_RF is enabled in my CMackeCache.txt but disabled in stormConfig.cmake:

grep CLN stormConfig.cmake 
set(STORM_USE_CLN_EA "OFF")
set(STORM_USE_CLN_RF "OFF")

Edit: Similar in Carl

volkm commented 1 year ago

What values are given in build/temp.macosx-...-version/generated/config.py and in lib/stormpy/info/_config.py?

tquatmann commented 1 year ago
master ~/stormpy/stormpy> cat build/temp.macosx-12-arm64-cpython-311-version/generated/config.py 
# Auto-generated by CMake.

STORM_DIR = "/Users/tim/storm/build"
STORM_VERSION = "1.7.1"
STORM_CLN_EA = False
STORM_CLN_RF = False
STORM_XERCES = True
STORM_SPOT = True
HAVE_STORM_DFT = True
HAVE_STORM_GSPN = True
HAVE_STORM_PARS = True
HAVE_STORM_POMDP = True
?master ~/stormpy/stormpy> cat lib/stormpy/info/_config.py 
# Auto-generated by CMake.

storm_version = "1.7.1"
storm_cln_ea = True
storm_cln_rf = True
stormpy_pybind_version = "2.10.0"
volkm commented 1 year ago

Thanks for the quick answer. Interesting, the values are correctly read from CMake but incorrectly written to the stormpy config file at some point. I will do some digging...

tquatmann commented 1 year ago

Thanks! Let me know if I can be of further help