From 717fa454d2e479318ae0e7b2bd37b497c24949b7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 18 Apr 2018 15:15:39 +0200 Subject: [PATCH 01/38] Updated example drn file --- lib/stormpy/examples/files/ctmc/dft.drn | 90 +++++++++++++------------ tests/core/test_modelchecking.py | 2 +- 2 files changed, 47 insertions(+), 45 deletions(-) diff --git a/lib/stormpy/examples/files/ctmc/dft.drn b/lib/stormpy/examples/files/ctmc/dft.drn index 1f1f317..91245df 100644 --- a/lib/stormpy/examples/files/ctmc/dft.drn +++ b/lib/stormpy/examples/files/ctmc/dft.drn @@ -3,71 +3,73 @@ @type: CTMC @parameters +@reward_models + @nr_states 16 @model -state 0 init +state 0 !1 failed action 0 - 1 : 0.5 - 2 : 0.5 - 3 : 0.5 - 4 : 0.5 -state 1 - action 0 - 5 : 0.5 - 9 : 0.5 - 11 : 0.5 -state 2 - action 0 - 5 : 0.5 - 14 : 0.5 - 15 : 0.5 -state 3 + 0 : 1 +state 1 !2 init action 0 + 2 : 0.5 9 : 0.5 - 12 : 0.5 + 13 : 0.5 15 : 0.5 -state 4 - action 0 - 11 : 0.5 - 12 : 0.5 - 14 : 0.5 -state 5 +state 2 !1.5 action 0 + 3 : 0.5 6 : 0.5 8 : 0.5 -state 6 +state 3 !1 action 0 - 7 : 0.5 -state 7 failed + 4 : 0.5 + 5 : 0.5 +state 4 !0.5 + action 0 + 0 : 0.5 +state 5 !0.5 action 0 - 7 : 1 -state 8 + 0 : 0.5 +state 6 !1 action 0 + 4 : 0.5 7 : 0.5 -state 9 +state 7 !0.5 action 0 - 8 : 0.5 - 10 : 0.5 -state 10 + 0 : 0.5 +state 8 !1 action 0 + 5 : 0.5 7 : 0.5 -state 11 +state 9 !1.5 action 0 - 6 : 0.5 + 3 : 0.5 10 : 0.5 -state 12 + 12 : 0.5 +state 10 !1 action 0 - 10 : 0.5 - 13 : 0.5 -state 13 + 4 : 0.5 + 11 : 0.5 +state 11 !0.5 action 0 - 7 : 0.5 -state 14 + 0 : 0.5 +state 12 !1 action 0 - 6 : 0.5 - 13 : 0.5 -state 15 + 5 : 0.5 + 11 : 0.5 +state 13 !1.5 action 0 8 : 0.5 - 13 : 0.5 + 12 : 0.5 + 14 : 0.5 +state 14 !1 + action 0 + 7 : 0.5 + 11 : 0.5 +state 15 !1.5 + action 0 + 6 : 0.5 + 10 : 0.5 + 14 : 0.5 diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index e4df9eb..89cce9e 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -124,6 +124,6 @@ class TestModelChecking: assert model.nr_transitions == 33 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] - assert initial_state == 0 + assert initial_state == 1 result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) From 5ba71f81b5f66651690b6f82dbdcbddca88f9a1c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 18 Apr 2018 17:52:16 +0200 Subject: [PATCH 02/38] Travis: test against stable version of Storm as well --- .travis.yml | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4c79c06..6972611 100644 --- a/.travis.yml +++ b/.travis.yml @@ -25,7 +25,7 @@ notifications: # jobs: include: - # docker storm:latest + # Docker Storm master - os: linux compiler: gcc env: TASK=Test CONFIG=Release DOCKER=storm:travis PYTHON=python3 @@ -33,7 +33,7 @@ jobs: travis/install_linux.sh script: travis/build.sh - # docker storm-debug:latest + # Docker Storm master in debug mode - os: linux compiler: gcc env: TASK=Test CONFIG=Debug DOCKER=storm:travis-debug PYTHON=python3 @@ -41,6 +41,22 @@ jobs: travis/install_linux.sh script: travis/build.sh + # Docker Storm stable + - os: linux + compiler: gcc + env: TASK=Test CONFIG=Release DOCKER=storm:1.2.1 PYTHON=python3 + install: + travis/install_linux.sh + script: + travis/build.sh + # Docker Storm stable in debug mode + - os: linux + compiler: gcc + env: TASK=Test CONFIG=Debug DOCKER=storm:1.2.1-debug PYTHON=python3 + install: + travis/install_linux.sh + script: + travis/build.sh # Documentation - os: linux compiler: gcc @@ -59,3 +75,8 @@ jobs: on: branch: master +allow_failures: + - os: linux + env: TASK=Test CONFIG=Release DOCKER=storm:1.2.1 PYTHON=python3 + - os: linux + env: TASK=Test CONFIG=Debug DOCKER=storm:1.2.1-debug PYTHON=python3 From d6056d71fa877905780a9dc81da2f0c046ba278d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 18 Apr 2018 20:31:44 +0200 Subject: [PATCH 03/38] Travis: try to fix allow_failures --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index 6972611..4ddd9ae 100644 --- a/.travis.yml +++ b/.travis.yml @@ -75,8 +75,11 @@ jobs: on: branch: master +# Allow failures of stable versions as new features might have been added allow_failures: - os: linux + compiler: gcc env: TASK=Test CONFIG=Release DOCKER=storm:1.2.1 PYTHON=python3 - os: linux + compiler: gcc env: TASK=Test CONFIG=Debug DOCKER=storm:1.2.1-debug PYTHON=python3 From 1ac10663252a132dfc191c957ab4fae27af58e26 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 18 Apr 2018 20:39:02 +0200 Subject: [PATCH 04/38] Increased required Storm version --- CHANGELOG.md | 3 +++ setup.py | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8479b19..41f4233 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,9 @@ Changelog Version 1.2.x ------------- +### Version 1.2.x +Requires storm version >= 1.2.2 and pycarl version >= 2.0.2 + ### Version 1.2.0 Requires storm version >= 1.2.0 and pycarl version >= 2.0.2 - Adaptions to changes in Storm diff --git a/setup.py b/setup.py index 6aba669..a8ecc9a 100755 --- a/setup.py +++ b/setup.py @@ -15,7 +15,7 @@ if sys.version_info[0] == 2: sys.exit('Sorry, Python 2.x is not supported') # Minimal storm version required -storm_min_version = "1.2.0" +storm_min_version = "1.2.2" class CMakeExtension(Extension): From a1d7266567b0a3439c15143d888eee702bdf21d1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 20 Apr 2018 16:50:50 +0200 Subject: [PATCH 05/38] Travis: change docker repo --- travis/build.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/travis/build.sh b/travis/build.sh index 745305b..209a1b3 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -11,7 +11,7 @@ linux) docker rm -f stormpy &>/dev/null # Run container set -e - docker run -d -it --name stormpy --privileged mvolk/$DOCKER + docker run -d -it --name stormpy --privileged movesrwth/$DOCKER # Copy local content into container docker exec stormpy mkdir opt/stormpy docker cp . stormpy:/opt/stormpy From aa5c8fb6fe400cea04d129fea09e7c26a1937dd3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 20 Apr 2018 16:51:17 +0200 Subject: [PATCH 06/38] Travis: minor change in travis script --- .travis.yml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4ddd9ae..637416b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -75,11 +75,9 @@ jobs: on: branch: master -# Allow failures of stable versions as new features might have been added -allow_failures: + # Allow failures of stable versions as new features might have been added + allow_failures: - os: linux - compiler: gcc env: TASK=Test CONFIG=Release DOCKER=storm:1.2.1 PYTHON=python3 - os: linux - compiler: gcc env: TASK=Test CONFIG=Debug DOCKER=storm:1.2.1-debug PYTHON=python3 From bb3b2a8f5e6173a93c3c3462accaf0195ab0243a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 20 Apr 2018 17:55:52 +0200 Subject: [PATCH 07/38] Travis: use absolute path --- travis/build.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/travis/build.sh b/travis/build.sh index 209a1b3..2bbe2e8 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -13,7 +13,7 @@ linux) set -e docker run -d -it --name stormpy --privileged movesrwth/$DOCKER # Copy local content into container - docker exec stormpy mkdir opt/stormpy + docker exec stormpy mkdir /opt/stormpy docker cp . stormpy:/opt/stormpy # Install virtualenv docker exec stormpy apt-get update @@ -27,7 +27,7 @@ linux) export PYTHON=$PYTHON; export CONFIG=$CONFIG; export TASK=$TASK; - cd opt/stormpy; + cd /opt/stormpy; travis/build-helper.sh" exit $? ;; From 9b57e37ee4824236c766d64df8550975d2cb317b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 15:08:56 +0200 Subject: [PATCH 08/38] Updated gitignore --- .gitignore | 15 +++++++++++---- lib/.gitignore | 4 ---- tests/.gitignore | 1 - 3 files changed, 11 insertions(+), 9 deletions(-) delete mode 100644 lib/.gitignore delete mode 100644 tests/.gitignore diff --git a/.gitignore b/.gitignore index 6c315c3..6250ed7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,14 @@ *.so -__pycache__ +*.py[cod] +lib/**/_config.py +.eggs/ +*.egg-info/ build/ -*.pye -.idea +dist/ +.idea/ +__pycache__/ +_build/ +.pytest_cache/ +.idea/ + .DS_Store -_config.py diff --git a/lib/.gitignore b/lib/.gitignore deleted file mode 100644 index a34a658..0000000 --- a/lib/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -*.so -__pycache__/ -stormpy.egg-info/ -**/_config.py diff --git a/tests/.gitignore b/tests/.gitignore deleted file mode 100644 index bee8a64..0000000 --- a/tests/.gitignore +++ /dev/null @@ -1 +0,0 @@ -__pycache__ From da81f6cf1ab94ae0ef748550883a69cebb1d405c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 15:10:13 +0200 Subject: [PATCH 09/38] Raise ImportError when using python 2.x --- lib/stormpy/__init__.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index f1ee516..91da0a8 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -1,3 +1,8 @@ +import sys + +if sys.version_info[0] == 2: + raise ImportError('Python 2.x is not supported for stormpy.') + from . import core from .core import * from . import storage From 95da370b4ad85dbecb4dfa87685b627d2f60f3bb Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 16:10:22 +0200 Subject: [PATCH 10/38] Improve distribution --- MANIFEST.in | 5 +++++ setup.py | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 MANIFEST.in diff --git a/MANIFEST.in b/MANIFEST.in new file mode 100644 index 0000000..e66eb4a --- /dev/null +++ b/MANIFEST.in @@ -0,0 +1,5 @@ +include CMakeLists.txt +recursive-include setup/ *.py +recursive-include cmake/ * +recursive-include src/ * +recursive-include resources/ * diff --git a/setup.py b/setup.py index a8ecc9a..77d1f5a 100755 --- a/setup.py +++ b/setup.py @@ -17,6 +17,9 @@ if sys.version_info[0] == 2: # Minimal storm version required storm_min_version = "1.2.2" +# Get the long description from the README file +with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f: + long_description = f.read() class CMakeExtension(Extension): def __init__(self, name, sourcedir='', subdir=''): @@ -210,7 +213,7 @@ setup( maintainer_email="sebastian.junges@cs.rwth-aachen.de", url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", - long_description='', + long_description=long_description, packages=['stormpy', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', 'stormpy.pars', 'stormpy.dft'], package_dir={'': 'lib'}, From 0b6dd8c0d888835fa3a215d1e83037bb6c0120b0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 17:01:36 +0200 Subject: [PATCH 11/38] Fix sphinx warning in comment --- lib/stormpy/__init__.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 91da0a8..8a47e13 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -147,8 +147,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler Perform model checking on model for property. :param model: Model. :param property: Property to check for. - :param only_initial_states: If True, only results for initial states are computed. - If False, results for all states are computed. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler :return: Model checking result. :rtype: CheckResult From a83e2206213c21296557f0d4d5bf9c2db74f6419 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 17:30:57 +0200 Subject: [PATCH 12/38] Updated package information --- setup.py | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/setup.py b/setup.py index 77d1f5a..c4ce901 100755 --- a/setup.py +++ b/setup.py @@ -21,6 +21,7 @@ storm_min_version = "1.2.2" with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f: long_description = f.read() + class CMakeExtension(Extension): def __init__(self, name, sourcedir='', subdir=''): Extension.__init__(self, name, sources=[]) @@ -214,8 +215,24 @@ setup( url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", long_description=long_description, - packages=['stormpy', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', - 'stormpy.pars', 'stormpy.dft'], + project_urls={ + 'Documentation': 'https://moves-rwth.github.io/stormpy/', + 'Source': 'https://github.com/moves-rwth/stormpy/', + 'Tracker': 'https://github.com/moves-rwth/stormpy/issues', + }, + classifiers=[ + 'Intended Audience :: Science/Research', + 'Topic :: Scientific/Engineering', + 'Topic :: Software Development :: Libraries :: Python Modules', + ], + + packages=['stormpy', + 'stormpy.info', + 'stormpy.logic', + 'stormpy.storage', + 'stormpy.utility', + 'stormpy.dft', + 'stormpy.pars'], package_dir={'': 'lib'}, ext_package='stormpy', ext_modules=[CMakeExtension('core', subdir=''), @@ -224,8 +241,8 @@ setup( CMakeExtension('storage', subdir='storage'), CMakeExtension('utility', subdir='utility'), CMakeExtension('dft', subdir='dft'), - CMakeExtension('pars', subdir='pars'), - ], + CMakeExtension('pars', subdir='pars')], + cmdclass={'build_ext': CMakeBuild, 'test': PyTest}, zip_safe=False, install_requires=['pycarl>=2.0.2'], From d0534cd0669b0a95f4a28e7544501aed20c03bcf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 25 Apr 2018 17:44:07 +0200 Subject: [PATCH 13/38] Minor update in project description --- setup.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/setup.py b/setup.py index c4ce901..ae82db1 100755 --- a/setup.py +++ b/setup.py @@ -215,10 +215,11 @@ setup( url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", long_description=long_description, + long_description_content_type='text/text/markdown', project_urls={ 'Documentation': 'https://moves-rwth.github.io/stormpy/', 'Source': 'https://github.com/moves-rwth/stormpy/', - 'Tracker': 'https://github.com/moves-rwth/stormpy/issues', + 'Bug reports': 'https://github.com/moves-rwth/stormpy/issues', }, classifiers=[ 'Intended Audience :: Science/Research', From bef2feceb29c8e0dd103a536af2e424ef784f532 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 26 Apr 2018 19:17:18 +0200 Subject: [PATCH 14/38] Removed fixed lib path in cmake --- CMakeLists.txt | 35 ++++++++++------------------------- cmake/CMakeLists.txt | 12 +++++------- 2 files changed, 15 insertions(+), 32 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index c400ebd..f0d0130 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,57 +1,42 @@ cmake_minimum_required(VERSION 3.0.0) project(pystorm) -option(STORMPY_DISABLE_SIGNATURE_DOC "disables the signature in the documentation" ON) - find_package(storm REQUIRED) add_subdirectory(resources/pybind11) +option(STORMPY_DISABLE_SIGNATURE_DOC "disables the signature in the documentation" ON) + configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/config.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/generated/config.h) message(STATUS "STORM-DIR: ${storm_DIR}") -set(STORMPY_LIB_DIR "${CMAKE_SOURCE_DIR}/lib/stormpy" CACHE STRING "Sets the storm library dir") - function(stormpy_module NAME) - # second, optional argument is LIBRARY_OUTPUT_DIRECTORY, - # defaults to subdir with module name - # third, optional argument are ADDITIONAL_LIBRARIES - # fourth, optional argument are ADDITIONAL_INCLUDES - if(ARGC GREATER 1) - set(LIB_PATH "${ARGV1}") - else() - set(LIB_PATH "${STORMPY_LIB_DIR}/${NAME}") - endif() + # second, optional argument are ADDITIONAL_LIBRARIES + # third, optional argument are ADDITIONAL_INCLUDES file(GLOB_RECURSE "STORM_${NAME}_SOURCES" "${CMAKE_CURRENT_SOURCE_DIR}/src/${NAME}/*.cpp") pybind11_add_module(${NAME} "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_${NAME}.cpp" ${STORM_${NAME}_SOURCES}) - if(ARGC GREATER 2) + if(ARGC GREATER 1) # Additional libraries - target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${ARGV3} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) - target_link_libraries(${NAME} PRIVATE storm ${ARGV2}) + target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${ARGV2} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) + target_link_libraries(${NAME} PRIVATE storm ${ARGV1}) else() target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) target_link_libraries(${NAME} PRIVATE storm) endif() - - # setup.py will override this (because pip may want a different install - # path), but also specifying it here has the advantage that invoking cmake - # manually uses the correct path if the default is used (i.e. the - # STORMPY_LIB_DIR hardcoded above) - set_target_properties(${NAME} PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${LIB_PATH}") endfunction(stormpy_module) -stormpy_module(core "${STORMPY_LIB_DIR}") +stormpy_module(core) stormpy_module(info) stormpy_module(logic) stormpy_module(storage) stormpy_module(utility) if(HAVE_STORM_PARS) - stormpy_module(pars "${STORMPY_LIB_DIR}/pars" storm-pars "${storm-pars_INCLUDE_DIR}") + stormpy_module(pars storm-pars "${storm-pars_INCLUDE_DIR}") endif() if(HAVE_STORM_DFT) - stormpy_module(dft "${STORMPY_LIB_DIR}/dft" storm-dft "${storm-dft_INCLUDE_DIR}") + stormpy_module(dft storm-dft "${storm-dft_INCLUDE_DIR}") endif() diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt index ef03051..bbaf9c4 100644 --- a/cmake/CMakeLists.txt +++ b/cmake/CMakeLists.txt @@ -2,6 +2,11 @@ cmake_minimum_required(VERSION 3.0.0) project(storm-version) find_package(storm REQUIRED) + +# Set configuration +set(STORM_DIR ${storm_DIR}) +set(STORM_VERSION ${storm_VERSION}) + # Check for storm-pars if(EXISTS "${storm_DIR}/lib/libstorm-pars.dylib") set(HAVE_STORM_PARS TRUE) @@ -20,10 +25,6 @@ else() set(HAVE_STORM_DFT FALSE) endif() -# Set configuration -set(STORM_DIR ${storm_DIR}) -set(STORM_VERSION ${storm_VERSION}) - if(HAVE_STORM_PARS) set(HAVE_STORM_PARS_BOOL "True") else() @@ -48,7 +49,4 @@ else() set(STORM_CLN_RF_BOOL "False") endif() - - - configure_file(${CMAKE_CURRENT_SOURCE_DIR}/config.py.in ${CMAKE_CURRENT_BINARY_DIR}/generated/config.py @ONLY) From 19db78e038c30a6527be466dd27736267b44d9ef Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 26 Apr 2018 22:18:22 +0200 Subject: [PATCH 15/38] Fixed typo --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index ae82db1..1519370 100755 --- a/setup.py +++ b/setup.py @@ -215,7 +215,7 @@ setup( url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", long_description=long_description, - long_description_content_type='text/text/markdown', + long_description_content_type='text/markdown', project_urls={ 'Documentation': 'https://moves-rwth.github.io/stormpy/', 'Source': 'https://github.com/moves-rwth/stormpy/', From 0c62edfb0db7f51b617f9cd08ae250bcce5f26d4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 26 Apr 2018 22:18:51 +0200 Subject: [PATCH 16/38] Added missing package in setup.py --- setup.py | 1 + 1 file changed, 1 insertion(+) diff --git a/setup.py b/setup.py index 1519370..6a1a851 100755 --- a/setup.py +++ b/setup.py @@ -228,6 +228,7 @@ setup( ], packages=['stormpy', + 'stormpy.exceptions', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', From 5db3c691526f919a863de18dd752fc830a12a06f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 27 Apr 2018 11:44:10 +0200 Subject: [PATCH 17/38] Updated setup.py --- MANIFEST.in | 1 + setup.py | 15 +++++---------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/MANIFEST.in b/MANIFEST.in index e66eb4a..bbfd747 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -3,3 +3,4 @@ recursive-include setup/ *.py recursive-include cmake/ * recursive-include src/ * recursive-include resources/ * +recursive-include lib/stormpy/examples/files/ * diff --git a/setup.py b/setup.py index 6a1a851..ec81e39 100755 --- a/setup.py +++ b/setup.py @@ -3,7 +3,7 @@ import sys import subprocess import datetime -from setuptools import setup, Extension +from setuptools import setup, Extension, find_packages from setuptools.command.build_ext import build_ext from setuptools.command.test import test from distutils.version import StrictVersion @@ -212,7 +212,7 @@ setup( author_email="matthias.volk@cs.rwth-aachen.de", maintainer="S. Junges", maintainer_email="sebastian.junges@cs.rwth-aachen.de", - url="http://moves.rwth-aachen.de", + url="https://github.com/moves-rwth/stormpy/", description="stormpy - Python Bindings for Storm", long_description=long_description, long_description_content_type='text/markdown', @@ -227,15 +227,10 @@ setup( 'Topic :: Software Development :: Libraries :: Python Modules', ], - packages=['stormpy', - 'stormpy.exceptions', - 'stormpy.info', - 'stormpy.logic', - 'stormpy.storage', - 'stormpy.utility', - 'stormpy.dft', - 'stormpy.pars'], + packages=find_packages('lib'), package_dir={'': 'lib'}, + include_package_data=True, + package_data={'stormpy.examples': ['examples/files/*']}, ext_package='stormpy', ext_modules=[CMakeExtension('core', subdir=''), CMakeExtension('info', subdir='info'), From 4c40ab6ea306d8b54c74c8255a085678c76d051a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 27 Apr 2018 14:27:18 +0200 Subject: [PATCH 18/38] Use pytest-runner --- setup.py | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/setup.py b/setup.py index ec81e39..ef1227c 100755 --- a/setup.py +++ b/setup.py @@ -5,7 +5,6 @@ import datetime from setuptools import setup, Extension, find_packages from setuptools.command.build_ext import build_ext -from setuptools.command.test import test from distutils.version import StrictVersion import setup.helper as setup_helper @@ -197,14 +196,6 @@ class CMakeBuild(build_ext): subprocess.check_call(['cmake', '--build', '.', '--target', ext.name] + build_args, cwd=self.build_temp) -class PyTest(test): - def run_tests(self): - # import here, cause outside the eggs aren't loaded - import pytest - errno = pytest.main(['tests']) - sys.exit(errno) - - setup( name="stormpy", version=setup_helper.obtain_version(), @@ -240,7 +231,7 @@ setup( CMakeExtension('dft', subdir='dft'), CMakeExtension('pars', subdir='pars')], - cmdclass={'build_ext': CMakeBuild, 'test': PyTest}, + cmdclass={'build_ext': CMakeBuild}, zip_safe=False, install_requires=['pycarl>=2.0.2'], setup_requires=['pytest-runner'], From 89ed130335346364006f0e41936c4d563e1ec5f7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 30 Apr 2018 17:43:07 +0200 Subject: [PATCH 19/38] Extended documentation --- doc/source/advanced_topics.rst | 6 +- doc/source/api.rst | 17 +++++ .../{code_stormpy_core.rst => api/core.rst} | 8 --- doc/source/api/dft.rst | 7 ++ doc/source/api/exceptions.rst | 7 ++ doc/source/api/info.rst | 7 ++ doc/source/api/logic.rst | 7 ++ doc/source/api/pars.rst | 7 ++ doc/source/api/storage.rst | 7 ++ doc/source/api/utility.rst | 7 ++ doc/source/code_stormpy_logic.rst | 12 ---- doc/source/code_stormpy_storage.rst | 11 ---- doc/source/conf.py | 2 +- doc/source/contributors.rst | 3 +- doc/source/{ => doc}/building_models.rst | 0 doc/source/{ => doc}/reward_models.rst | 0 doc/source/{ => doc}/shortest_paths.rst | 0 doc/source/getting_started.rst | 10 +-- doc/source/index.rst | 12 +--- doc/source/installation.rst | 66 ++++++++++++++----- 20 files changed, 129 insertions(+), 67 deletions(-) create mode 100644 doc/source/api.rst rename doc/source/{code_stormpy_core.rst => api/core.rst} (53%) create mode 100644 doc/source/api/dft.rst create mode 100644 doc/source/api/exceptions.rst create mode 100644 doc/source/api/info.rst create mode 100644 doc/source/api/logic.rst create mode 100644 doc/source/api/pars.rst create mode 100644 doc/source/api/storage.rst create mode 100644 doc/source/api/utility.rst delete mode 100644 doc/source/code_stormpy_logic.rst delete mode 100644 doc/source/code_stormpy_storage.rst rename doc/source/{ => doc}/building_models.rst (100%) rename doc/source/{ => doc}/reward_models.rst (100%) rename doc/source/{ => doc}/shortest_paths.rst (100%) diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 124c702..7c5d0c0 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -8,6 +8,6 @@ This guide is a collection of examples meant to bridge the gap between the getti :maxdepth: 2 :caption: Contents: - building_models - reward_models - shortest_paths \ No newline at end of file + doc/building_models + doc/reward_models + doc/shortest_paths \ No newline at end of file diff --git a/doc/source/api.rst b/doc/source/api.rst new file mode 100644 index 0000000..f9144c4 --- /dev/null +++ b/doc/source/api.rst @@ -0,0 +1,17 @@ +Stormpy API Reference +==================================== +Work in progress! + +.. toctree:: + :maxdepth: 2 + :caption: Modules: + + api/core + api/info + api/exceptions + api/logic + api/storage + api/utility + + api/dft + api/pars diff --git a/doc/source/code_stormpy_core.rst b/doc/source/api/core.rst similarity index 53% rename from doc/source/code_stormpy_core.rst rename to doc/source/api/core.rst index 4f26fa9..b9a41a1 100644 --- a/doc/source/code_stormpy_core.rst +++ b/doc/source/api/core.rst @@ -5,11 +5,3 @@ Stormpy.core :members: :undoc-members: :imported-members: - -Core members -========================= - - -.. automodule:: stormpy.core - :members: - :undoc-members: diff --git a/doc/source/api/dft.rst b/doc/source/api/dft.rst new file mode 100644 index 0000000..331f60c --- /dev/null +++ b/doc/source/api/dft.rst @@ -0,0 +1,7 @@ +Stormpy.dft +************************** + +.. automodule:: stormpy.dft + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/exceptions.rst b/doc/source/api/exceptions.rst new file mode 100644 index 0000000..8a3e2b2 --- /dev/null +++ b/doc/source/api/exceptions.rst @@ -0,0 +1,7 @@ +Stormpy.exceptions +************************** + +.. automodule:: stormpy.exceptions + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/info.rst b/doc/source/api/info.rst new file mode 100644 index 0000000..8421b2b --- /dev/null +++ b/doc/source/api/info.rst @@ -0,0 +1,7 @@ +Stormpy.info +************************** + +.. automodule:: stormpy.info + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/logic.rst b/doc/source/api/logic.rst new file mode 100644 index 0000000..84d34a9 --- /dev/null +++ b/doc/source/api/logic.rst @@ -0,0 +1,7 @@ +Stormpy.logic +************************** + +.. automodule:: stormpy.logic + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/pars.rst b/doc/source/api/pars.rst new file mode 100644 index 0000000..2c66395 --- /dev/null +++ b/doc/source/api/pars.rst @@ -0,0 +1,7 @@ +Stormpy.pars +************************** + +.. automodule:: stormpy.pars + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/storage.rst b/doc/source/api/storage.rst new file mode 100644 index 0000000..5281904 --- /dev/null +++ b/doc/source/api/storage.rst @@ -0,0 +1,7 @@ +Stormpy.storage +************************** + +.. automodule:: stormpy.storage + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/api/utility.rst b/doc/source/api/utility.rst new file mode 100644 index 0000000..6bfe305 --- /dev/null +++ b/doc/source/api/utility.rst @@ -0,0 +1,7 @@ +Stormpy.utility +************************** + +.. automodule:: stormpy.utility + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/code_stormpy_logic.rst b/doc/source/code_stormpy_logic.rst deleted file mode 100644 index 51c4daf..0000000 --- a/doc/source/code_stormpy_logic.rst +++ /dev/null @@ -1,12 +0,0 @@ -Stormpy.logic -************************** - -.. automodule:: stormpy - - -Members -========================= - - -.. automodule:: stormpy.logic.logic - :members: diff --git a/doc/source/code_stormpy_storage.rst b/doc/source/code_stormpy_storage.rst deleted file mode 100644 index 666f940..0000000 --- a/doc/source/code_stormpy_storage.rst +++ /dev/null @@ -1,11 +0,0 @@ -Stormpy.storage -************************** - -.. automodule:: stormpy - -Members -============================== - -.. automodule:: stormpy.storage.storage - :members: - diff --git a/doc/source/conf.py b/doc/source/conf.py index 2fbcfa8..c1a41d1 100644 --- a/doc/source/conf.py +++ b/doc/source/conf.py @@ -56,7 +56,7 @@ master_doc = 'index' # General information about the project. project = 'stormpy' -copyright = '2016--2017 Moves RWTH Aachen' +copyright = '2016--2018 Moves RWTH Aachen' author = 'Sebastian Junges, Matthias Volk' # The version info for the project you're documenting, acts as replacement for diff --git a/doc/source/contributors.rst b/doc/source/contributors.rst index 464d72b..0961349 100644 --- a/doc/source/contributors.rst +++ b/doc/source/contributors.rst @@ -2,7 +2,8 @@ Contributors ************** -Stormpy is an extension to `Storm `_. As a consequence, developers of Storm contributed significantly to the functionality offered by these Python bindings. +Stormpy is an extension to `Storm `_. +As a consequence, developers of Storm contributed significantly to the functionality offered by these Python bindings. The bindings themselves have been developed by (lexicographically ordered): * Sebastian Junges diff --git a/doc/source/building_models.rst b/doc/source/doc/building_models.rst similarity index 100% rename from doc/source/building_models.rst rename to doc/source/doc/building_models.rst diff --git a/doc/source/reward_models.rst b/doc/source/doc/reward_models.rst similarity index 100% rename from doc/source/reward_models.rst rename to doc/source/doc/reward_models.rst diff --git a/doc/source/shortest_paths.rst b/doc/source/doc/shortest_paths.rst similarity index 100% rename from doc/source/shortest_paths.rst rename to doc/source/doc/shortest_paths.rst diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index b577e11..1649cc6 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -11,15 +11,17 @@ This guide is intended for people which have a basic understanding of probabilis `Storm website `_. While we assume some very basic programming concepts, we refrain from using more advanced concepts of python throughout the guide. -We start with a selection of high-level constructs in stormpy, and go into more details afterwards. More in-depth examples can be found in the :doc:`advanced_examples`. +We start with a selection of high-level constructs in stormpy, and go into more details afterwards. More in-depth examples can be found in the :doc:`advanced_topics`. .. seealso:: The code examples are also given in the `examples/ `_ folder. These boxes throughout the text will tell you which example contains the code discussed. -In order to do this, we import stormpy:: +We start by launching the python 3 interpreter:: + + $ python3 + +First we import stormpy:: >>> import stormpy - >>> import stormpy.core - Building models ------------------------------------------------ diff --git a/doc/source/index.rst b/doc/source/index.rst index 76040e8..74a137d 100644 --- a/doc/source/index.rst +++ b/doc/source/index.rst @@ -19,16 +19,8 @@ Stormpy is a set of python bindings for the probabilistic model checker `Storm < advanced_topics contributors - -Stormpy API Reference -==================================== -.. toctree:: - :maxdepth: 2 - :caption: Modules: - - code_stormpy_core - code_stormpy_logic - code_stormpy_storage + +.. include:: api.rst Indices and tables diff --git a/doc/source/installation.rst b/doc/source/installation.rst index 69d2915..858da51 100644 --- a/doc/source/installation.rst +++ b/doc/source/installation.rst @@ -7,28 +7,46 @@ Requirements Before installing stormpy, make sure -- `pycarl `_ -- `Storm `_ +- Python 3 is available on your system. Stormpy does not work with python 2. +- `pycarl `_ is available. +- `Storm `_ is available on your system. -are both available on your system. To avoid issues, we suggest that both use the same version of `carl `_. +To avoid issues, we suggest that both pycarl and Storm use the same version of `carl `_. The simplest way of ensuring this is to first install carl as explained in the `Storm installation guide `_. You can then install Storm and pycarl independently. -.. topic:: Virtual Environments - - Virtual environments create isolated environments for your projects. This helps to keep your system clean, work with different versions of packages and different versions of python. While it is not required, we recommend the use of - such virtual environments. To get you started, we recommend `this guide `_ or `this primer `_. - Installation Steps ==================== +Virtual Environments +-------------------- + +Virtual environments create isolated environments for your projects. +This helps to keep your system clean, work with different versions of packages and different version of python. +While it is not required, we recommend the use of such virtual environments. To get you started, we recommend +`this guide `_ or +`this primer `_. + +In short you can create a virtual environment ``env`` with:: + + $ pip install virtualenv + $ virtualenv -p python3 env + $ source env/bin/activate + +The last step activates the virtual environment. +Whenever using the environment the console prompt is prefixed with ``(env)``. + + +Building stormpy +---------------- + Clone stormpy into any suitable location:: $ git clone https://github.com/moves-rwth/stormpy.git $ cd stormpy -Here, build stormpy in develop mode using your favourite python distribution way of installing: e.g.:: +Build stormpy in develop mode using your favourite python distribution way of installing: e.g.:: $ python3 setup.py develop @@ -37,17 +55,31 @@ or:: $ pip install -ve . -.. topic:: Specifying which Storm library to use +Optional build arguments +^^^^^^^^^^^^^^^^^^^^^^^^ + +The build step also takes optional arguments for a more advanced configuration of stormpy. + +* *Specifying which Storm library to use* + + If you have multiple versions of Storm or cmake is not able to find your Storm version, + you can specify the ``--storm-dir YOUR-PATH-TO-STORM`` flag in the ``build_ext`` step:: - If you have multiple versions of Storm or cmake is not able to find your Storm version, - you can specify the `--storm-dir YOUR-PATH-TO-STORM` flag in the build_ext step:: - $ python3 setup.py build_ext --storm-dir YOUR-PATH-TO-STORM develop - + +* *Building stormpy in debug mode* + + If you want to build stormpy in debug mode you can add the ``--debug`` flag in the ``build_ext`` step:: + + $ python3 setup.py build_ext --debug develop + + +Testing stormpy installation +---------------------------- + After building, you can run the test files by:: py.test tests/ -If tests pass, you can continue with our :doc:`getting_started`. - - +If the tests pass, you can now use stormpy. +To get started, continue with our :doc:`getting_started`, consult the test files in ``tests/`` or the :doc:`api` (work in progress). From 4daa73372750292c1dca3bb944786822a8608870 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 1 May 2018 20:28:13 +0200 Subject: [PATCH 20/38] Moved documentation for parametric models into own file --- doc/source/advanced_topics.rst | 3 +- doc/source/doc/parametric_models.rst | 61 +++++++++++++++++++ doc/source/getting_started.rst | 49 +-------------- examples/04-getting-started.py | 37 ++++------- examples/06-getting-started.py | 26 -------- .../parametric_models/01-parametric-models.py | 41 +++++++++++++ .../02-parametric-models.py} | 4 +- 7 files changed, 119 insertions(+), 102 deletions(-) create mode 100644 doc/source/doc/parametric_models.rst delete mode 100644 examples/06-getting-started.py create mode 100644 examples/parametric_models/01-parametric-models.py rename examples/{05-getting-started.py => parametric_models/02-parametric-models.py} (95%) diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 7c5d0c0..765149a 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -10,4 +10,5 @@ This guide is a collection of examples meant to bridge the gap between the getti doc/building_models doc/reward_models - doc/shortest_paths \ No newline at end of file + doc/shortest_paths + doc/parametric_models \ No newline at end of file diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst new file mode 100644 index 0000000..c4376c4 --- /dev/null +++ b/doc/source/doc/parametric_models.rst @@ -0,0 +1,61 @@ +***************** +Parametric Models +***************** + + + +Instantiating parametric models +=============================== +.. seealso:: `01-parametric-models.py `_ + +Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters. +If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:: + + >>> import stormpy + >>> import stormpy.examples + >>> import stormpy.examples.files + >>> path = stormpy.examples.files.prism_dtmc_die + >>> prism_program = stormpy.parse_prism_program(path) + >>> formula_str = "P=? [F s=7 & d=2]" + >>> properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + + >>> model = stormpy.build_parametric_model(prism_program, properties) + >>> parameters = model.collect_probability_parameters() + >>> for x in parameters: + ... print(x) + +In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator:: + + >>> import stormpy.pars + >>> instantiator = stormpy.pars.PDtmcInstantiator(model) + +Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:: + + >>> point = dict() + >>> for x in parameters: + ... print(x.name) + ... point[x] = 0.4 + >>> instantiated_model = instantiator.instantiate(point) + >>> result = stormpy.model_checking(instantiated_model, properties[0]) + +Initial states and labels are set as for the parameter-free case. + + +Checking parametric models +========================== +.. seealso:: `02-parametric-models.py `_ + +It is also possible to check the parametric model directly, similar as before in :ref:`getting-started-checking-properties`:: + + >>> result = stormpy.model_checking(model, properties[0]) + >>> initial_state = model.initial_states[0] + >>> func = result.at(initial_state) + +We collect the constraints ensuring that underlying model is well-formed and the graph structure does not change. + + >>> collector = stormpy.ConstraintCollector(model) + >>> for formula in collector.wellformed_constraints: + ... print(formula) + >>> for formula in collector.graph_preserving_constraints: + ... print(formula) + diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index 1649cc6..947036a 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -126,58 +126,11 @@ A good way to get the result for the initial states is as follows:: >>> print(result.at(initial_state)) 0.5 -Instantiating parametric models ------------------------------------- -.. seealso:: `04-getting-started.py `_ - -Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters. -If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:: - - >>> model = stormpy.build_parametric_model(prism_program, properties) - >>> parameters = model.collect_probability_parameters() - >>> for x in parameters: - ... print(x) - -In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator:: - - >>> import stormpy.pars - >>> instantiator = stormpy.pars.PDtmcInstantiator(model) - -Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:: - - >>> point = dict() - >>> for x in parameters: - ... print(x.name) - ... point[x] = 0.4 - >>> instantiated_model = instantiator.instantiate(point) - >>> result = stormpy.model_checking(instantiated_model, properties[0]) - -Initial states and labels are set as for the parameter-free case. - - -Checking parametric models ------------------------------------- -.. seealso:: `05-getting-started.py `_ - -It is also possible to check the parametric model directly, similar as before in :ref:`getting-started-checking-properties`:: - - >>> result = stormpy.model_checking(model, properties[0]) - >>> initial_state = model.initial_states[0] - >>> func = result.at(initial_state) - -We collect the constraints ensuring that underlying model is well-formed and the graph structure does not change. - - >>> collector = stormpy.ConstraintCollector(model) - >>> for formula in collector.wellformed_constraints: - ... print(formula) - >>> for formula in collector.graph_preserving_constraints: - ... print(formula) - .. _getting-started-investigating-the-model: Investigating the model ------------------------------------- -.. seealso:: `06-getting-started.py `_ +.. seealso:: `04-getting-started.py `_ One powerful part of the Storm model checker is to quickly create the Markov chain from higher-order descriptions, as seen above:: diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py index a5c0d60..e1fcd66 100644 --- a/examples/04-getting-started.py +++ b/examples/04-getting-started.py @@ -1,40 +1,27 @@ import stormpy import stormpy.core -import pycarl -import pycarl.core - import stormpy.examples import stormpy.examples.files -import stormpy._config as config - def example_getting_started_04(): - # Check support for parameters - if not config.storm_with_pars: - print("Support parameters is missing. Try building storm-pars.") - return - - import stormpy.pars - path = stormpy.examples.files.prism_pdtmc_die + path = stormpy.examples.files.prism_dtmc_die prism_program = stormpy.parse_prism_program(path) formula_str = "P=? [F s=7 & d=2]" properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) - model = stormpy.build_parametric_model(prism_program, properties) - print("Model supports parameters: {}".format(model.supports_parameters)) - parameters = model.collect_probability_parameters() - assert len(parameters) == 2 - - instantiator = stormpy.pars.PDtmcInstantiator(model) - point = dict() - for x in parameters: - print(x.name) - point[x] = stormpy.RationalRF(0.4) - instantiated_model = instantiator.instantiate(point) - result = stormpy.model_checking(instantiated_model, properties[0]) - print(result) + model = stormpy.build_model(prism_program, properties) + + print(model.model_type) + + for state in model.states: + if state.id in model.initial_states: + print(state) + for action in state.actions: + for transition in action.transitions: + print("From state {}, with probability {}, go to state {}".format(state, transition.value(), + transition.column)) if __name__ == '__main__': diff --git a/examples/06-getting-started.py b/examples/06-getting-started.py deleted file mode 100644 index e8d1378..0000000 --- a/examples/06-getting-started.py +++ /dev/null @@ -1,26 +0,0 @@ -import stormpy -import stormpy.core - -import stormpy.examples -import stormpy.examples.files - -def example_getting_started_06(): - path = stormpy.examples.files.prism_dtmc_die - prism_program = stormpy.parse_prism_program(path) - - formula_str = "P=? [F s=7 & d=2]" - properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) - model = stormpy.build_model(prism_program, properties) - - print(model.model_type) - - for state in model.states: - if state.id in model.initial_states: - print(state) - for action in state.actions: - for transition in action.transitions: - print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) - - -if __name__ == '__main__': - example_getting_started_06() \ No newline at end of file diff --git a/examples/parametric_models/01-parametric-models.py b/examples/parametric_models/01-parametric-models.py new file mode 100644 index 0000000..30c2d4e --- /dev/null +++ b/examples/parametric_models/01-parametric-models.py @@ -0,0 +1,41 @@ +import stormpy +import stormpy.core + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy._config as config + + +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 + path = stormpy.examples.files.prism_pdtmc_die + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + model = stormpy.build_parametric_model(prism_program, properties) + print("Model supports parameters: {}".format(model.supports_parameters)) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + + instantiator = stormpy.pars.PDtmcInstantiator(model) + point = dict() + for x in parameters: + print(x.name) + point[x] = stormpy.RationalRF(0.4) + instantiated_model = instantiator.instantiate(point) + result = stormpy.model_checking(instantiated_model, properties[0]) + print(result) + + +if __name__ == '__main__': + example_parametric_models_01() diff --git a/examples/05-getting-started.py b/examples/parametric_models/02-parametric-models.py similarity index 95% rename from examples/05-getting-started.py rename to examples/parametric_models/02-parametric-models.py index 29403f6..d273c0b 100644 --- a/examples/05-getting-started.py +++ b/examples/parametric_models/02-parametric-models.py @@ -11,7 +11,7 @@ import stormpy.examples.files import stormpy._config as config -def example_getting_started_05(): +def example_parametric_models_02(): # Check support for parameters if not config.storm_with_pars: print("Support parameters is missing. Try building storm-pars.") @@ -45,4 +45,4 @@ def example_getting_started_05(): if __name__ == '__main__': - example_getting_started_05() + example_parametric_models_02() From aad97475725414ca8349b65b8c4432d7fc750e98 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 3 May 2018 13:15:44 +0200 Subject: [PATCH 21/38] Fix for storm-dir --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index ef1227c..c6542a8 100755 --- a/setup.py +++ b/setup.py @@ -58,7 +58,7 @@ class CMakeBuild(build_ext): self.config.write_config("build/build_config.cfg") cmake_args = [] - storm_dir = self.config.get_as_string("storm_dir") + storm_dir = os.path.expanduser(self.config.get_as_string("storm_dir")) if storm_dir: cmake_args += ['-Dstorm_DIR=' + storm_dir] _ = subprocess.check_output(['cmake', os.path.abspath("cmake")] + cmake_args, cwd=build_temp_version) From 61a49dc20b9e660241808c54949ccfbf21bd8e32 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 3 May 2018 13:28:24 +0200 Subject: [PATCH 22/38] Extended doc for build arguments --- doc/source/installation.rst | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/doc/source/installation.rst b/doc/source/installation.rst index 858da51..80ce6c7 100644 --- a/doc/source/installation.rst +++ b/doc/source/installation.rst @@ -58,21 +58,35 @@ or:: Optional build arguments ^^^^^^^^^^^^^^^^^^^^^^^^ -The build step also takes optional arguments for a more advanced configuration of stormpy. +The build step ``build_ext`` also takes optional arguments for a more advanced configuration of stormpy. * *Specifying which Storm library to use* If you have multiple versions of Storm or cmake is not able to find your Storm version, - you can specify the ``--storm-dir YOUR-PATH-TO-STORM`` flag in the ``build_ext`` step:: + you can specify the ``--storm-dir YOUR-PATH-TO-STORM`` flag:: $ python3 setup.py build_ext --storm-dir YOUR-PATH-TO-STORM develop +* *Disabling functionality* + + If you want to disable certain functionality in stormpy from being built you can use the following flags: + + * ``--disable-dft`` to disable support for dynamic fault trees (DFTs) + * ``--disable-pars`` to disable support for parametric models + * *Building stormpy in debug mode* - If you want to build stormpy in debug mode you can add the ``--debug`` flag in the ``build_ext`` step:: + If you want to build stormpy in debug mode you can add the ``--debug`` flag:: $ python3 setup.py build_ext --debug develop +* *Setting number of build threads* + + The build of stormpy uses all available cores per default. + If you want to configure the number of threads manually you can specify the ``--jobs`` (or ``-j``) flag:: + + $ python3 setup.py build_ext --jobs 2 develop + Testing stormpy installation ---------------------------- From b0132b4317d2f1275d263e371a61e6ef78ad5d97 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 16 May 2018 15:21:09 +0200 Subject: [PATCH 23/38] Travis: removed docker installation as the package is already present --- .travis.yml | 10 ------- travis/install_linux.sh | 5 ---- travis/install_osx.sh | 63 ----------------------------------------- 3 files changed, 78 deletions(-) delete mode 100755 travis/install_linux.sh delete mode 100755 travis/install_osx.sh diff --git a/.travis.yml b/.travis.yml index 637416b..c5c081d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -29,40 +29,30 @@ jobs: - os: linux compiler: gcc env: TASK=Test CONFIG=Release DOCKER=storm:travis PYTHON=python3 - install: - travis/install_linux.sh script: travis/build.sh # Docker Storm master in debug mode - os: linux compiler: gcc env: TASK=Test CONFIG=Debug DOCKER=storm:travis-debug PYTHON=python3 - install: - travis/install_linux.sh script: travis/build.sh # Docker Storm stable - os: linux compiler: gcc env: TASK=Test CONFIG=Release DOCKER=storm:1.2.1 PYTHON=python3 - install: - travis/install_linux.sh script: travis/build.sh # Docker Storm stable in debug mode - os: linux compiler: gcc env: TASK=Test CONFIG=Debug DOCKER=storm:1.2.1-debug PYTHON=python3 - install: - travis/install_linux.sh script: travis/build.sh # Documentation - os: linux compiler: gcc env: TASK=Documentation CONFIG=Release DOCKER=storm:travis PYTHON=python3 - install: - travis/install_linux.sh script: travis/build.sh before_deploy: diff --git a/travis/install_linux.sh b/travis/install_linux.sh deleted file mode 100755 index 911b673..0000000 --- a/travis/install_linux.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/bash - -set -e - -sudo apt-get install -qq -y docker diff --git a/travis/install_osx.sh b/travis/install_osx.sh deleted file mode 100755 index b7cec33..0000000 --- a/travis/install_osx.sh +++ /dev/null @@ -1,63 +0,0 @@ -#!/bin/bash -# Script installing dependencies -# Inspired by https://github.com/google/fruit - -set -e - -# Helper for travis folding -travis_fold() { - local action=$1 - local name=$2 - echo -en "travis_fold:${action}:${name}\r" -} - -# Helper for installing packages via homebrew -install_brew_package() { - if brew list -1 | grep -q "^$1\$"; then - # Package is installed, upgrade if needed - brew outdated "$1" || brew upgrade "$@" - else - # Package not installed yet, install. - # If there are conflicts, try overwriting the files (these are in /usr/local anyway so it should be ok). - brew install "$@" || brew link --overwrite gcc49 - fi -} - -# Update packages -travis_fold start brew_update -brew update -travis_fold end brew_update - -travis_fold start brew_install_util -# For md5sum -install_brew_package md5sha1sum -# For `timeout' -install_brew_package coreutils - -which cmake &>/dev/null || install_brew_package cmake - -# Install compiler -case "${COMPILER}" in -gcc-4.8) install_brew_package gcc@4.8 ;; -gcc-4.9) install_brew_package gcc@4.9 ;; -gcc-5) install_brew_package gcc@5 ;; -gcc-6) install_brew_package gcc@6 ;; -clang-default) ;; -clang-3.7) install_brew_package llvm@3.7 --with-clang --with-libcxx;; -clang-3.8) install_brew_package llvm@3.8 --with-clang --with-libcxx;; -clang-3.9) install_brew_package llvm@3.9 --with-clang --with-libcxx;; -clang-4.0) install_brew_package llvm --with-clang --with-libcxx;; -*) echo "Compiler not supported: ${COMPILER}. See travis/install_osx.sh"; exit 1 ;; -esac -travis_fold end brew_install_util - - -# Install dependencies -travis_fold start brew_install_dependencies -install_brew_package gmp --c++11 -install_brew_package cln -install_brew_package ginac -install_brew_package boost --c++11 -install_brew_package python -install_brew_package python3 -travis_fold end brew_install_dependencies From d9b020b1bca4b7fe9a04dc54905e2c3af0663014 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 17 May 2018 15:36:54 +0200 Subject: [PATCH 24/38] Refactored sparse model bindings --- lib/stormpy/__init__.py | 97 +++++++++------------ src/mod_storage.cpp | 1 + src/storage/model.cpp | 188 +++++++++++++++++++++------------------- src/storage/model.h | 1 + 4 files changed, 142 insertions(+), 145 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8a47e13..883cc2c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -22,15 +22,46 @@ except ImportError: core._set_up("") +def _convert_sparse_model(model, parametric=False): + """ + Convert (parametric) model in sparse representation into model corresponding to exact model type. + :param model: Sparse model. + :param parametric: Flag indicating if the model is parametric. + :return: Model corresponding to exact model type. + """ + if parametric: + assert model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_sparse_pdtmc() + elif model.model_type == ModelType.MDP: + return model._as_sparse_pmdp() + elif model.model_type == ModelType.CTMC: + return model._as_sparse_pctmc() + elif model.model_type == ModelType.MA: + return model._as_sparse_pma() + else: + raise StormError("Not supported parametric model constructed") + else: + assert not model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_sparse_dtmc() + elif model.model_type == ModelType.MDP: + return model._as_sparse_mdp() + elif model.model_type == ModelType.CTMC: + return model._as_sparse_ctmc() + elif model.model_type == ModelType.MA: + return model._as_sparse_ma() + else: + raise StormError("Not supported non-parametric model constructed") + def build_model(symbolic_description, properties=None): """ - Build a model from a symbolic description. + Build a model in sparse representation from a symbolic description. :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Model in sparse representation. - :rtype: SparseDtmc or SparseMdp """ if not symbolic_description.undefined_constants_are_graph_preserving: raise StormError("Program still contains undefined constants") @@ -40,91 +71,49 @@ def build_model(symbolic_description, properties=None): intermediate = core._build_sparse_model_from_prism_program(symbolic_description, formulae) else: intermediate = core._build_sparse_model_from_prism_program(symbolic_description) - assert not intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_dtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_mdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_ctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_ma() - else: - raise StormError("Not supported non-parametric model constructed") + return _convert_sparse_model(intermediate, parametric=False) def build_parametric_model(symbolic_description, properties=None): """ - Build a parametric model from a symbolic description. + Build a parametric model in sparse representation from a symbolic description. :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Parametric model in sparse representation. - :rtype: SparseParametricDtmc or SparseParametricMdp """ if not symbolic_description.undefined_constants_are_graph_preserving: raise StormError("Program still contains undefined constants") if properties: formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) else: - formulae = [] - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) - assert intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_pmdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_pctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_pma() - else: - raise StormError("Not supported parametric model constructed") + intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description) + return _convert_sparse_model(intermediate, parametric=True) def build_model_from_drn(file): """ - Build a model from the explicit DRN representation. + Build a model in sparse representation from the explicit DRN representation. :param String file: DRN file containing the model. :return: Model in sparse representation. - :rtype: SparseDtmc or SparseMdp or SparseCTMC or SparseMA """ intermediate = core._build_sparse_model_from_drn(file) - assert not intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_dtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_mdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_ctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_ma() - else: - raise StormError("Not supported non-parametric model constructed") + return _convert_sparse_model(intermediate, parametric=False) def build_parametric_model_from_drn(file): """ - Build a parametric model from the explicit DRN representation. + Build a parametric model in sparse representation from the explicit DRN representation. :param String file: DRN file containing the model. :return: Parametric model in sparse representation. - :rtype: SparseParametricDtmc or SparseParametricMdp or SparseParametricCTMC or SparseParametricMA """ intermediate = core._build_sparse_parametric_model_from_drn(file) - assert intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_pmdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_pctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_pma() - else: - raise StormError("Not supported parametric model constructed") + return _convert_sparse_model(intermediate, parametric=True) + def perform_bisimulation(model, properties, bisimulation_type): diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 4fd3cbd..9907378 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -20,6 +20,7 @@ PYBIND11_MODULE(storage, m) { define_bitvector(m); define_model(m); + define_sparse_model(m); define_sparse_matrix(m); define_state(m); define_prism(m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index ec3d43f..9d0993b 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -13,22 +13,22 @@ #include #include +// Typedefs +using RationalFunction = storm::RationalFunction; +using state_type = storm::storage::sparse::state_type; +template using SparseRewardModel = storm::models::sparse::StandardRewardModel; using ModelBase = storm::models::ModelBase; -using state_type = storm::storage::sparse::state_type; -using RationalFunction = storm::RationalFunction; -using RationalFunctionVariable = storm::RationalFunctionVariable; -template using Model = storm::models::sparse::Model; -template using Dtmc = storm::models::sparse::Dtmc; -template using Mdp = storm::models::sparse::Mdp; -template using Ctmc = storm::models::sparse::Ctmc; -template using MarkovAutomaton = storm::models::sparse::MarkovAutomaton; -template using SparseMatrix = storm::storage::SparseMatrix; -template using RewardModel = storm::models::sparse::StandardRewardModel; +template using SparseModel = storm::models::sparse::Model; +template using SparseDtmc = storm::models::sparse::Dtmc; +template using SparseMdp = storm::models::sparse::Mdp; +template using SparseCtmc = storm::models::sparse::Ctmc; +template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; + // Thin wrapper for getting initial states template -std::vector getInitialStates(Model const& model) { +std::vector getInitialStates(SparseModel const& model) { std::vector initialStates; for (auto entry : model.getInitialStates()) { initialStates.push_back(entry); @@ -38,28 +38,28 @@ std::vector getInitialStates(Model const& model) { // Thin wrapper for getting transition matrix template -SparseMatrix& getTransitionMatrix(Model& model) { +storm::storage::SparseMatrix& getTransitionMatrix(SparseModel& model) { return model.getTransitionMatrix(); } template -storm::storage::SparseMatrix getBackwardTransitionMatrix(storm::models::sparse::Model& model) { - return model.getBackwardTransitions(); +storm::storage::SparseMatrix getBackwardTransitionMatrix(SparseModel const& model) { + return std::move(model.getBackwardTransitions()); } // requires pycarl.Variable -std::set probabilityVariables(Model const& model) { +std::set probabilityVariables(SparseModel const& model) { return storm::models::sparse::getProbabilityParameters(model); } -std::set rewardVariables(Model const& model) { +std::set rewardVariables(SparseModel const& model) { return storm::models::sparse::getRewardParameters(model); } template -std::function const&)> getModelInfoPrinter(std::string name = "Model") { +std::function const&)> getModelInfoPrinter(std::string name = "Model") { // look, C++ has lambdas and stuff! - return [name](Model const& model) { + return [name](storm::models::Model const& model) { std::stringstream ss; model.printModelInformationToStream(ss); @@ -75,11 +75,12 @@ std::function const&)> getModelInfoPrinter(std::st } template -storm::models::sparse::StateLabeling& getLabeling(storm::models::sparse::Model& model) { +storm::models::sparse::StateLabeling& getLabeling(SparseModel& model) { return model.getStateLabeling(); } -// Define python bindings + +// Bindings for general models void define_model(py::module& m) { // ModelType @@ -98,116 +99,121 @@ void define_model(py::module& m) { .def_property_readonly("supports_parameters", &ModelBase::supportsParameters, "Flag whether model supports parameters") .def_property_readonly("has_parameters", &ModelBase::hasParameters, "Flag whether model has parameters") .def_property_readonly("is_exact", &ModelBase::isExact, "Flag whether model is exact") - .def("_as_dtmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as DTMC") - .def("_as_pdtmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pDTMC") - .def("_as_mdp", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as MDP") - .def("_as_pmdp", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pMDP") - .def("_as_ctmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as CTMC") - .def("_as_pctmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pCTMC") - .def("_as_ma", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as MA") - .def("_as_pma", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pMA") + .def("_as_sparse_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse DTMC") + .def("_as_sparse_pdtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pDTMC") + .def("_as_sparse_mdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse MDP") + .def("_as_sparse_pmdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pMDP") + .def("_as_sparse_ctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse CTMC") + .def("_as_sparse_pctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pCTMC") + .def("_as_sparse_ma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse MA") + .def("_as_sparse_pma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pMA") + .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic DTMC") ; +} + + +// Bindings for sparse models +void define_sparse_model(py::module& m) { + // Models - py::class_, std::shared_ptr>> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", modelBase); + py::class_, std::shared_ptr>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); model.def_property_readonly("labeling", &getLabeling, "Labels") - .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") - .def_property_readonly("states", [](Model& model) { + .def_property_readonly("states", [](SparseModel& model) { return SparseModelStates(model); }, "Get states") - .def_property_readonly("reward_models", [](Model& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") - .def("reduce_to_state_based_rewards", &Model::reduceToStateBasedRewards) + .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter()) ; - py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) .def("__str__", getModelInfoPrinter("DTMC")) ; - py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) .def("__str__", getModelInfoPrinter("MDP")) ; - py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) .def("__str__", getModelInfoPrinter("CTMC")) ; - py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) .def("__str__", getModelInfoPrinter("MA")) ; - py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") - .def_property_readonly("has_state_rewards", &RewardModel::hasStateRewards) - .def_property_readonly("has_state_action_rewards", &RewardModel::hasStateActionRewards) - .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) - .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) - .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) - .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") - ; - + py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") + .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) + .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) + .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") + ; - py::class_, std::shared_ptr>> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase); + py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix"); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") - .def_property_readonly("labeling", &getLabeling, "Labels") - .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("labeling", &getLabeling, "Labels") + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") - .def_property_readonly("states", [](Model& model) { - return SparseModelStates(model); + .def_property_readonly("states", [](SparseModel& model) { + return SparseModelStates(model); }, "Get states") - .def_property_readonly("reward_models", [](Model const& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reward_models", [](SparseModel const& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") - .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") - .def("reduce_to_state_based_rewards", &Model::reduceToStateBasedRewards) + .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter("ParametricModel")) ; - py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricDTMC")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricMDP")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricCTMC")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricMA")) ; - py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") - .def_property_readonly("has_state_rewards", &RewardModel::hasStateRewards) - .def_property_readonly("has_state_action_rewards", &RewardModel::hasStateActionRewards) - .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) - .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) - .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) - .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") + py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") + .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) + .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) + .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; } diff --git a/src/storage/model.h b/src/storage/model.h index c779f26..ac91a56 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -4,5 +4,6 @@ #include "common.h" void define_model(py::module& m); +void define_sparse_model(py::module& m); #endif /* PYTHON_STORAGE_MODEL_H_ */ From 0072a3fc980c54b61920b367ddad03e7bd6256ae Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 17 May 2018 17:35:48 +0200 Subject: [PATCH 25/38] Refactoring for sparse models --- src/storage/model.cpp | 36 ++++++++++++++---------------------- src/storage/model.h | 4 +--- 2 files changed, 15 insertions(+), 25 deletions(-) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 9d0993b..c185ae6 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -15,38 +15,32 @@ // Typedefs using RationalFunction = storm::RationalFunction; -using state_type = storm::storage::sparse::state_type; -template using SparseRewardModel = storm::models::sparse::StandardRewardModel; - using ModelBase = storm::models::ModelBase; + template using SparseModel = storm::models::sparse::Model; template using SparseDtmc = storm::models::sparse::Dtmc; template using SparseMdp = storm::models::sparse::Mdp; template using SparseCtmc = storm::models::sparse::Ctmc; template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; +template using SparseRewardModel = storm::models::sparse::StandardRewardModel; + -// Thin wrapper for getting initial states +// Thin wrappers template -std::vector getInitialStates(SparseModel const& model) { - std::vector initialStates; +std::vector getSparseInitialStates(SparseModel const& model) { + std::vector initialStates; for (auto entry : model.getInitialStates()) { initialStates.push_back(entry); } return initialStates; } -// Thin wrapper for getting transition matrix template storm::storage::SparseMatrix& getTransitionMatrix(SparseModel& model) { return model.getTransitionMatrix(); } -template -storm::storage::SparseMatrix getBackwardTransitionMatrix(SparseModel const& model) { - return std::move(model.getBackwardTransitions()); -} - // requires pycarl.Variable std::set probabilityVariables(SparseModel const& model) { return storm::models::sparse::getProbabilityParameters(model); @@ -123,9 +117,7 @@ void define_model(py::module& m) { .def("_as_sparse_pma", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pMA") - .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as symbolic DTMC") + ; } @@ -133,18 +125,17 @@ void define_model(py::module& m) { // Bindings for sparse models void define_sparse_model(py::module& m) { - - // Models + // Models with double numbers py::class_, std::shared_ptr>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); model.def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") - .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") .def_property_readonly("states", [](SparseModel& model) { return SparseModelStates(model); }, "Get states") .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") - .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter()) ; @@ -169,23 +160,24 @@ void define_sparse_model(py::module& m) { .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; + // Parametric models py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix"); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") .def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") - .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") .def_property_readonly("states", [](SparseModel& model) { return SparseModelStates(model); }, "Get states") .def_property_readonly("reward_models", [](SparseModel const& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") - .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter("ParametricModel")) ; diff --git a/src/storage/model.h b/src/storage/model.h index ac91a56..50f4c31 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -1,9 +1,7 @@ -#ifndef PYTHON_STORAGE_MODEL_H_ -#define PYTHON_STORAGE_MODEL_H_ +#pragma once #include "common.h" void define_model(py::module& m); void define_sparse_model(py::module& m); -#endif /* PYTHON_STORAGE_MODEL_H_ */ From 21ecfacc3b69e2f3a6ec5c7c30fe5a6626561d2c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 17 May 2018 17:49:44 +0200 Subject: [PATCH 26/38] Bindings for symbolic models using Sylvan --- src/mod_storage.cpp | 3 ++ src/storage/model.cpp | 105 +++++++++++++++++++++++++++++++++++++++++- src/storage/model.h | 3 ++ 3 files changed, 110 insertions(+), 1 deletion(-) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 9907378..a8d3089 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -10,6 +10,8 @@ #include "storage/labeling.h" #include "storage/expressions.h" +#include "storm/storage/dd/DdType.h" + PYBIND11_MODULE(storage, m) { m.doc() = "Data structures in Storm"; @@ -22,6 +24,7 @@ PYBIND11_MODULE(storage, m) { define_model(m); define_sparse_model(m); define_sparse_matrix(m); + define_symbolic_model(m, "Sylvan"); define_state(m); define_prism(m); define_labeling(m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index c185ae6..f2f49a1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -8,6 +8,12 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/Model.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/MarkovAutomaton.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include #include @@ -24,6 +30,13 @@ template using SparseCtmc = storm::models::sparse::Ctmc using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; template using SparseRewardModel = storm::models::sparse::StandardRewardModel; +template using SymbolicModel = storm::models::symbolic::Model; +template using SymbolicDtmc = storm::models::symbolic::Dtmc; +template using SymbolicMdp = storm::models::symbolic::Mdp; +template using SymbolicCtmc = storm::models::symbolic::Ctmc; +template using SymbolicMarkovAutomaton = storm::models::symbolic::MarkovAutomaton; +template using SymbolicRewardModel = storm::models::symbolic::StandardRewardModel; + // Thin wrappers @@ -117,7 +130,30 @@ void define_model(py::module& m) { .def("_as_sparse_pma", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pMA") - + .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic DTMC") + .def("_as_symbolic_pdtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pDTMC") + .def("_as_symbolic_mdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic MDP") + .def("_as_symbolic_pmdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pMDP") + .def("_as_symbolic_ctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic CTMC") + .def("_as_symbolic_pctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pCTMC") + .def("_as_symbolic_ma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic MA") + .def("_as_symbolic_pma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pMA") ; } @@ -210,3 +246,70 @@ void define_sparse_model(py::module& m) { } + +// Bindings for symbolic models +template +void define_symbolic_model(py::module& m, std::string vt_suffix) { + + // Set class names + std::string prefixClassName = "Symbolic" + vt_suffix; + std::string prefixParametricClassName = "Symbolic" + vt_suffix + "Parametric"; + + + // Models with double numbers + py::class_, std::shared_ptr>, ModelBase> model(m, ("_"+prefixClassName+"Model").c_str(), "A probabilistic model where transitions are represented by doubles and saved in a symbolic representation"); + model.def_property_readonly("reward_models", [](SymbolicModel& model) {return model.getRewardModels(); }, "Reward models") + .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) + .def("__str__", getModelInfoPrinter()) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Dtmc").c_str(), "DTMC in symbolic representation", model) + .def("__str__", getModelInfoPrinter("DTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Mdp").c_str(), "MDP in symbolic representation", model) + .def("__str__", getModelInfoPrinter("MDP")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Ctmc").c_str(), "CTMC in symbolic representation", model) + .def("__str__", getModelInfoPrinter("CTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"MA").c_str(), "MA in symbolic representation", model) + .def("__str__", getModelInfoPrinter("MA")) + ; + + py::class_>(m, (prefixClassName+"RewardModel").c_str(), "Reward structure for symbolic models") + .def_property_readonly("has_state_rewards", &SymbolicRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SymbolicRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SymbolicRewardModel::hasTransitionRewards) + ; + + + // Parametric models + py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, ("_"+prefixParametricClassName+"Model").c_str(), "A probabilistic model where transitions are represented by rational functions and saved in a symbolic representation"); + modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") + .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") + .def_property_readonly("reward_models", [](SymbolicModel const& model) {return model.getRewardModels(); }, "Reward models") + .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) + .def("__str__", getModelInfoPrinter("ParametricModel")) + ; + + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Dtmc").c_str(), "pDTMC in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricDTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Mdp").c_str(), "pMDP in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricMDP")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Ctmc").c_str(), "pCTMC in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricCTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"MA").c_str(), "pMA in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricMA")) + ; + + py::class_>(m, (prefixParametricClassName+"RewardModel").c_str(), "Reward structure for parametric symbolic models") + .def_property_readonly("has_state_rewards", &SymbolicRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SymbolicRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SymbolicRewardModel::hasTransitionRewards) + ; + +} + +template void define_symbolic_model(py::module& m, std::string vt_suffix); diff --git a/src/storage/model.h b/src/storage/model.h index 50f4c31..7643d39 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -1,7 +1,10 @@ #pragma once #include "common.h" +#include "storm/storage/dd/DdType.h" void define_model(py::module& m); void define_sparse_model(py::module& m); +template +void define_symbolic_model(py::module& m, std::string vt_suffix); From cfb6dfbf2f9b7bcf7ead1bc5c1ef220b8ae7f7be Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:53:00 +0200 Subject: [PATCH 27/38] Better naming for sparse model building --- lib/stormpy/__init__.py | 10 +++++----- src/core/core.cpp | 16 ++++++++-------- src/core/core.h | 7 ++----- tests/storage/test_model.py | 14 ++------------ 4 files changed, 17 insertions(+), 30 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 883cc2c..0720ee3 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -22,6 +22,7 @@ except ImportError: core._set_up("") + def _convert_sparse_model(model, parametric=False): """ Convert (parametric) model in sparse representation into model corresponding to exact model type. @@ -68,9 +69,9 @@ def build_model(symbolic_description, properties=None): if properties: formulae = [prop.raw_formula for prop in properties] - intermediate = core._build_sparse_model_from_prism_program(symbolic_description, formulae) + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description, formulae) else: - intermediate = core._build_sparse_model_from_prism_program(symbolic_description) + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, parametric=False) @@ -87,9 +88,9 @@ def build_parametric_model(symbolic_description, properties=None): if properties: formulae = [prop.raw_formula for prop in properties] - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) + intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description, formulae) else: - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description) + intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, parametric=True) @@ -115,7 +116,6 @@ def build_parametric_model_from_drn(file): return _convert_sparse_model(intermediate, parametric=True) - def perform_bisimulation(model, properties, bisimulation_type): """ Perform bisimulation on model. diff --git a/src/core/core.cpp b/src/core/core.cpp index b4b5de6..e0e4af4 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -46,9 +46,9 @@ void define_parse(py::module& m) { ; } -// Thin wrapper for model building using one formula as argument +// Thin wrapper for model building using sparse representation template -std::shared_ptr buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool jit = false, bool doctor = false) { +std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool jit = false, bool doctor = false) { if (formulas.empty()) { // Build all labels and rewards storm::builder::BuilderOptions options(true, true); @@ -61,8 +61,8 @@ std::shared_ptr buildSparseModel(storm::storage::Symbo void define_build(py::module& m) { // Build model - m.def("_build_sparse_model_from_prism_program", &buildSparseModel, "Build the model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); - m.def("_build_sparse_parametric_model_from_prism_program", &buildSparseModel, "Build the parametric model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); @@ -71,15 +71,15 @@ void define_build(py::module& m) { void define_optimality_type(py::module& m) { py::enum_(m, "OptimizationDirection") - .value("Minimize", storm::solver::OptimizationDirection::Minimize) - .value("Maximize", storm::solver::OptimizationDirection::Maximize) - ; + .value("Minimize", storm::solver::OptimizationDirection::Minimize) + .value("Maximize", storm::solver::OptimizationDirection::Maximize) + ; } // Thin wrapper for exporting model template void exportDRN(std::shared_ptr> model, std::string const& file) { - std::ofstream stream; + std::ofstream stream; storm::utility::openFile(file, stream); storm::exporter::explicitExportSparseModel(stream, model, {}); storm::utility::closeFile(stream); diff --git a/src/core/core.h b/src/core/core.h index 51bc696..cf5a0f9 100644 --- a/src/core/core.h +++ b/src/core/core.h @@ -1,5 +1,4 @@ -#ifndef PYTHON_CORE_CORE_H_ -#define PYTHON_CORE_CORE_H_ +#pragma once #include "common.h" @@ -7,6 +6,4 @@ void define_core(py::module& m); void define_parse(py::module& m); void define_build(py::module& m); void define_export(py::module& m); -void define_optimality_type(py::module& m); - -#endif /* PYTHON_CORE_CORE_H_ */ +void define_optimality_type(py::module& m); \ No newline at end of file diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index d3c4b90..12b8326 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -4,7 +4,7 @@ from helpers.helper import get_example_path import pytest -class TestModel: +class TestSparseModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) model = stormpy.build_model(program) @@ -26,7 +26,7 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - def test_build_dtmc_from_prism_program_formulas(self): + def test_build_dtmc_from_prism_program_reward_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) prop = "R=? [F \"done\"]" properties = stormpy.parse_properties_for_prism_program(prop, program, None) @@ -65,16 +65,6 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - def test_build_dtmc(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) - assert model.nr_states == 13 - assert model.nr_transitions == 20 - assert model.model_type == stormpy.ModelType.DTMC - assert not model.supports_parameters - assert type(model) is stormpy.SparseDtmc - def test_build_dtmc_with_undefined_constants(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) assert jani_model.has_undefined_constants From f5a014ed5e082684d03a2a2a965f8e017a7d4eec Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:53:40 +0200 Subject: [PATCH 28/38] Bindings for symbolic model building --- lib/stormpy/__init__.py | 71 +++++++++++++++++++++++++++++++++++++++++ src/core/core.cpp | 17 ++++++++++ 2 files changed, 88 insertions(+) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 0720ee3..161e459 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -56,6 +56,39 @@ def _convert_sparse_model(model, parametric=False): raise StormError("Not supported non-parametric model constructed") +def _convert_symbolic_model(model, parametric=False): + """ + Convert (parametric) model in symbolic representation into model corresponding to exact model type. + :param model: Symbolic model. + :param parametric: Flag indicating if the model is parametric. + :return: Model corresponding to exact model type. + """ + if parametric: + assert model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_symbolic_pdtmc() + elif model.model_type == ModelType.MDP: + return model._as_symbolic_pmdp() + elif model.model_type == ModelType.CTMC: + return model._as_symbolic_pctmc() + elif model.model_type == ModelType.MA: + return model._as_symbolic_pma() + else: + raise StormError("Not supported parametric model constructed") + else: + assert not model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_symbolic_dtmc() + elif model.model_type == ModelType.MDP: + return model._as_symbolic_mdp() + elif model.model_type == ModelType.CTMC: + return model._as_symbolic_ctmc() + elif model.model_type == ModelType.MA: + return model._as_symbolic_ma() + else: + raise StormError("Not supported non-parametric model constructed") + + def build_model(symbolic_description, properties=None): """ Build a model in sparse representation from a symbolic description. @@ -94,6 +127,44 @@ def build_parametric_model(symbolic_description, properties=None): return _convert_sparse_model(intermediate, parametric=True) +def build_symbolic_model(symbolic_description, properties=None): + """ + Build a model in symbolic representation from a symbolic description. + + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Model in symbolic representation. + """ + if not symbolic_description.undefined_constants_are_graph_preserving: + raise StormError("Program still contains undefined constants") + + if properties: + formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description, formulae) + else: + intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description) + return _convert_symbolic_model(intermediate, parametric=False) + + +def build_symbolic_parametric_model(symbolic_description, properties=None): + """ + Build a parametric model in symbolic representation from a symbolic description. + + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Parametric model in symbolic representation. + """ + if not symbolic_description.undefined_constants_are_graph_preserving: + raise StormError("Program still contains undefined constants") + + if properties: + formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description, formulae) + else: + intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description) + return _convert_symbolic_model(intermediate, parametric=True) + + def build_model_from_drn(file): """ Build a model in sparse representation from the explicit DRN representation. diff --git a/src/core/core.cpp b/src/core/core.cpp index e0e4af4..eafd9bd 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -2,7 +2,10 @@ #include "storm/utility/initialize.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/storage/ModelFormulasPair.h" +#include "storm/storage/dd/DdType.h" #include "storm/solver/OptimizationDirection.h" +#include "storm/models/symbolic/StandardRewardModel.h" + void define_core(py::module& m) { // Init @@ -59,10 +62,24 @@ std::shared_ptr> buildSparseModel(storm: } } +// Thin wrapper for model building using symbolic representation +template +std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas) { + if (formulas.empty()) { + // Build full model + return storm::api::buildSymbolicModel(modelDescription, formulas, true); + } else { + // Only build labels necessary for formulas + return storm::api::buildSymbolicModel(modelDescription, formulas, false); + } +} + void define_build(py::module& m) { // Build model m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); + m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); From 54433ca8a38f155003e1040d97c25dcf24ee5939 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:53:50 +0200 Subject: [PATCH 29/38] Tests for symbolic model building --- tests/storage/test_model.py | 87 +++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 12b8326..2598e3b 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -123,3 +123,90 @@ class TestSparseModel: initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states + + +class TestSymbolicSylvanModel: + def test_build_dtmc_from_prism_program(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + model = stormpy.build_symbolic_model(program) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanDtmc + + def test_build_dtmc_from_prism_program_formulas(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + prop = "P=? [F \"one\"]" + properties = stormpy.parse_properties_for_prism_program(prop, program, None) + model = stormpy.build_symbolic_model(program, properties) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert len(model.reward_models) == 0 + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanDtmc + + def test_build_dtmc_from_prism_program_reward_formulas(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + prop = "R=? [F \"done\"]" + properties = stormpy.parse_properties_for_prism_program(prop, program, None) + model = stormpy.build_symbolic_model(program, properties) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert len(model.reward_models) == 1 + assert not model.reward_models["coin_flips"].has_state_rewards + assert model.reward_models["coin_flips"].has_state_action_rewards + assert not model.reward_models["coin_flips"].has_transition_rewards + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanDtmc + + def test_reduce_to_state_based_rewards(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + prop = "R=? [F \"done\"]" + properties = stormpy.parse_properties_for_prism_program(prop, program, None) + model = stormpy.build_symbolic_model(program, properties) + model.reduce_to_state_based_rewards() + assert len(model.reward_models) == 1 + assert model.reward_models["coin_flips"].has_state_rewards + assert not model.reward_models["coin_flips"].has_state_action_rewards + assert not model.reward_models["coin_flips"].has_transition_rewards + + def test_build_dtmc_from_jani_model(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) + description = stormpy.SymbolicModelDescription(jani_model) + constant_definitions = description.parse_constant_definitions("N=16, MAX=2") + instantiated_jani_model = description.instantiate_constants(constant_definitions).as_jani_model() + model = stormpy.build_symbolic_model(instantiated_jani_model) + assert model.nr_states == 677 + assert model.nr_transitions == 867 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanDtmc + + def test_build_mdp(self): + program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + model = stormpy.build_symbolic_model(program, formulas) + assert model.nr_states == 169 + assert model.nr_transitions == 435 + assert model.model_type == stormpy.ModelType.MDP + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanMdp + + def test_build_ctmc(self): + program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) + model = stormpy.build_symbolic_model(program, formulas) + assert model.nr_states == 12 + assert model.nr_transitions == 22 + assert model.model_type == stormpy.ModelType.CTMC + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanCtmc + + def test_build_ma(self): + program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program) + with pytest.raises(Exception): + model = stormpy.build_symbolic_model(program, formulas) From 32f468e92caf625bd01071ac57e72c6873278680 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 13:45:52 +0200 Subject: [PATCH 30/38] Added tests for symbolic parametric models --- tests/pars/test_parametric_model.py | 37 ++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py index d71886a..76e18c2 100644 --- a/tests/pars/test_parametric_model.py +++ b/tests/pars/test_parametric_model.py @@ -7,7 +7,7 @@ from configurations import pars @pars -class TestParametricModel: +class TestSparseParametricModel: def test_build_parametric_dtmc(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) @@ -39,3 +39,38 @@ class TestParametricModel: assert model.model_type == stormpy.ModelType.MDP assert model.supports_parameters assert type(model) is stormpy.SparseParametricMdp + + +@pars +class TestSymbolicParametricModel: + def test_build_parametric_dtmc(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_symbolic_parametric_model(program, formulas) + assert model.nr_states == 613 + assert model.nr_transitions == 803 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert model.has_parameters + assert type(model) is stormpy.SymbolicSylvanParametricDtmc + + def test_build_dtmc_supporting_parameters(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_symbolic_parametric_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert not model.has_parameters + assert type(model) is stormpy.SymbolicSylvanParametricDtmc + + def test_build_parametric_mdp(self): + program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + model = stormpy.build_symbolic_parametric_model(program, formulas) + assert model.nr_states == 169 + assert model.nr_transitions == 435 + assert model.model_type == stormpy.ModelType.MDP + assert model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanParametricMdp From 62f3d3630ed07d2843d5439e7cf8fe7e7be34961 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 15:02:13 +0200 Subject: [PATCH 31/38] Bindings for dd and hybrid model checking --- lib/stormpy/__init__.py | 82 +++++++++++++++++++++++++++++++- src/core/modelchecking.cpp | 22 +++++++-- src/core/result.cpp | 28 +++++++---- tests/core/test_modelchecking.py | 21 ++++++++ tests/pars/test_parametric.py | 28 ++++++++++- 5 files changed, 168 insertions(+), 13 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 161e459..1424892 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -93,6 +93,28 @@ def build_model(symbolic_description, properties=None): """ Build a model in sparse representation from a symbolic description. + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Model in sparse representation. + """ + return build_sparse_model(symbolic_description, properties=properties) + + +def build_parametric_model(symbolic_description, properties=None): + """ + Build a parametric model in sparse representation from a symbolic description. + + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Parametric model in sparse representation. + """ + return build_sparse_parametric_model(symbolic_description, properties=properties) + + +def build_sparse_model(symbolic_description, properties=None): + """ + Build a model in sparse representation from a symbolic description. + :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Model in sparse representation. @@ -108,7 +130,7 @@ def build_model(symbolic_description, properties=None): return _convert_sparse_model(intermediate, parametric=False) -def build_parametric_model(symbolic_description, properties=None): +def build_sparse_parametric_model(symbolic_description, properties=None): """ Build a parametric model in sparse representation from a symbolic description. @@ -203,6 +225,20 @@ def perform_bisimulation(model, properties, bisimulation_type): def model_checking(model, property, only_initial_states=False, extract_scheduler=False): + """ + Perform model checking on model for property. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :param extract_scheduler: If True, try to extract a scheduler + :return: Model checking result. + :rtype: CheckResult + """ + return check_model_sparse(model, property, only_initial_states=only_initial_states, + extract_scheduler=extract_scheduler) + + +def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False): """ Perform model checking on model for property. :param model: Model. @@ -227,6 +263,50 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler return core._model_checking_sparse_engine(model, task) +def check_model_dd(model, property, only_initial_states=False): + """ + Perform model checking using dd engine. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :return: Model checking result. + :rtype: CheckResult + """ + if isinstance(property, Property): + formula = property.raw_formula + else: + formula = property + + if model.supports_parameters: + task = core.ParametricCheckTask(formula, only_initial_states) + return core._parametric_model_checking_dd_engine(model, task) + else: + task = core.CheckTask(formula, only_initial_states) + return core._model_checking_dd_engine(model, task) + + +def check_model_hybrid(model, property, only_initial_states=False): + """ + Perform model checking using hybrid engine. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :return: Model checking result. + :rtype: CheckResult + """ + if isinstance(property, Property): + formula = property.raw_formula + else: + formula = property + + if model.supports_parameters: + task = core.ParametricCheckTask(formula, only_initial_states) + return core._parametric_model_checking_hybrid_engine(model, task) + else: + task = core.CheckTask(formula, only_initial_states) + return core._model_checking_hybrid_engine(model, task) + + def prob01min_states(model, eventually_formula): assert type(eventually_formula) == logic.EventuallyFormula labelform = eventually_formula.subformula diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 703e53c..1084a12 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -4,12 +4,24 @@ template using CheckTask = storm::modelchecker::CheckTask; -// Thin wrapper for model checking +// Thin wrapper for model checking using sparse engine template std::shared_ptr modelCheckingSparseEngine(std::shared_ptr> model, CheckTask const& task) { return storm::api::verifyWithSparseEngine(model, task); } +// Thin wrapper for model checking using dd engine +template +std::shared_ptr modelCheckingDdEngine(std::shared_ptr> model, CheckTask const& task) { + return storm::api::verifyWithDdEngine(model, task); +} + +// Thin wrapper for model checking using hybrid engine +template +std::shared_ptr modelCheckingHybridEngine(std::shared_ptr> model, CheckTask const& task) { + return storm::api::verifyWithHybridEngine(model, task); +} + // Thin wrapper for computing prob01 states template std::pair computeProb01(storm::models::sparse::Dtmc const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { @@ -42,8 +54,12 @@ void define_modelchecking(py::module& m) { ; // Model checking - m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking", py::arg("model"), py::arg("task")); - m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking", py::arg("model"), py::arg("task")); + m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task")); + m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task")); + m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task")); m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_min_double", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); diff --git a/src/core/result.cpp b/src/core/result.cpp index b564e3c..9025c63 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -1,11 +1,9 @@ #include "result.h" #include "storm/analysis/GraphConditions.h" - -// Thin wrapper -template -std::vector getValues(storm::modelchecker::ExplicitQuantitativeCheckResult const& result) { - return result.getValueVector(); -} +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "storm/models/symbolic/StandardRewardModel.h" // Define python bindings void define_result(py::module& m) { @@ -49,6 +47,8 @@ void define_result(py::module& m) { }, py::arg("state"), "Get result for given state") .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ; + py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) + ; // QuantitativeCheckResult py::class_, std::shared_ptr>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult); @@ -56,15 +56,27 @@ void define_result(py::module& m) { .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { return result[state]; }, py::arg("state"), "Get result for given state") - .def("get_values", &getValues, "Get model checking result values for all states") + .def("get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getValueVector();}, "Get model checking result values for all states") .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getScheduler();}, "get scheduler") ; + py::class_, std::shared_ptr>>(m, "SymbolicQuantitativeCheckResult", "Symbolic quantitative model checking result", quantitativeCheckResult) + ; + py::class_, std::shared_ptr>>(m, "HybridQuantitativeCheckResult", "Hybrid quantitative model checking result", quantitativeCheckResult) + .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") + ; + py::class_, std::shared_ptr>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult); py::class_, std::shared_ptr>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult) .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { return result[state]; }, py::arg("state"), "Get result for given state") - .def("get_values", &getValues, "Get model checking result values for all states") + .def("get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) { return res.getValueVector();}, "Get model checking result values for all states") + ; + py::class_, std::shared_ptr>>(m, "SymbolicParametricQuantitativeCheckResult", "Symbolic parametric quantitative model checking result", quantitativeCheckResult) ; + py::class_, std::shared_ptr>>(m, "HybridParametricQuantitativeCheckResult", "Symbolic parametric hybrid quantitative model checking result", quantitativeCheckResult) + .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") + ; + } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 89cce9e..c8687bc 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -127,3 +127,24 @@ class TestModelChecking: assert initial_state == 1 result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) + + def test_model_checking_prism_dd_dtmc(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_symbolic_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + result = stormpy.check_model_dd(model, formulas[0]) + assert type(result) is stormpy.SymbolicQuantitativeCheckResult + + def test_model_checking_prism_hybrid_dtmc(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_symbolic_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + result = stormpy.check_model_hybrid(model, formulas[0]) + assert type(result) is stormpy.HybridQuantitativeCheckResult + values = result.get_values() + assert len(values) == 3 + assert math.isclose(values[0], 0.16666666666666663) diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 71944e4..677a6ff 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -8,7 +8,7 @@ from configurations import pars @pars class TestParametric: - def test_parametric_state_elimination(self): + def test_parametric_model_checking_sparse(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) prop = "P=? [F s=5]" formulas = stormpy.parse_properties_for_prism_program(prop, program) @@ -24,6 +24,32 @@ class TestParametric: one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) assert func.denominator == one + def test_parametric_model_checking_dd(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + prop = "P=? [F s=5]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_parametric_model(program, formulas) + assert model.nr_states == 11 + assert model.nr_transitions == 17 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + result = stormpy.check_model_dd(model, formulas[0]) + assert type(result) is stormpy.SymbolicParametricQuantitativeCheckResult + + def test_parametric_model_checking_hybrid(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + prop = "P=? [F s=5]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_parametric_model(program, formulas) + assert model.nr_states == 11 + assert model.nr_transitions == 17 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + result = stormpy.check_model_hybrid(model, formulas[0]) + assert type(result) is stormpy.HybridParametricQuantitativeCheckResult + values = result.get_values() + assert len(values) == 3 + def test_constraints_collector(self): from pycarl.formula import FormulaType, Relation if stormpy.info.storm_ratfunc_use_cln(): From c30d5a1433f04b1b19d43866d22537779b20c800 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 17:47:02 +0200 Subject: [PATCH 32/38] Symbolic bisimulation --- lib/stormpy/__init__.py | 26 ++++++++++++++++++++++++++ src/core/bisimulation.cpp | 8 ++++++++ tests/core/test_bisimulation.py | 17 ++++++++++++++++- 3 files changed, 50 insertions(+), 1 deletion(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 1424892..7d76643 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -217,6 +217,17 @@ def perform_bisimulation(model, properties, bisimulation_type): :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation. """ + return perform_sparse_bisimulation(model, properties, bisimulation_type) + + +def perform_sparse_bisimulation(model, properties, bisimulation_type): + """ + Perform bisimulation on model in sparse representation. + :param model: Model. + :param properties: Properties to preserve during bisimulation. + :param bisimulation_type: Type of bisimulation (weak or strong). + :return: Model after bisimulation. + """ formulae = [prop.raw_formula for prop in properties] if model.supports_parameters: return core._perform_parametric_bisimulation(model, formulae, bisimulation_type) @@ -224,6 +235,21 @@ def perform_bisimulation(model, properties, bisimulation_type): return core._perform_bisimulation(model, formulae, bisimulation_type) +def perform_symbolic_bisimulation(model, properties): + """ + Perform bisimulation on model in symbolic representation. + :param model: Model. + :param properties: Properties to preserve during bisimulation. + :return: Model after bisimulation. + """ + formulae = [prop.raw_formula for prop in properties] + bisimulation_type = BisimulationType.STRONG + if model.supports_parameters: + return core._perform_symbolic_parametric_bisimulation(model, formulae, bisimulation_type) + else: + return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type) + + def model_checking(model, property, only_initial_states=False, extract_scheduler=False): """ Perform model checking on model for property. diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index 7feddd0..e7746ba 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -1,11 +1,19 @@ #include "bisimulation.h" + +template +std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong) { + return storm::api::performBisimulationMinimization(model, formulas, bisimulationType, storm::dd::bisimulation::SignatureMode::Eager); +} + // Define python bindings void define_bisimulation(py::module& m) { // Bisimulation m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); + m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); + m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); // BisimulationType py::enum_(m, "BisimulationType", "Types of bisimulation") diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index 418defc..b16ccc2 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -31,6 +31,21 @@ class TestBisimulation: assert initial_state_bisim == 34 assert math.isclose(result.at(initial_state), result_bisim.at(initial_state_bisim), rel_tol=1e-4) + def test_symbolic_bisimulation(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) + prop = "P=? [F \"observe0Greater1\"]" + properties = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_model(program, properties) + assert model.nr_states == 7403 + assert model.nr_transitions == 13041 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + model_bisim = stormpy.perform_symbolic_bisimulation(model, properties) + assert model_bisim.nr_states == 65 + assert model_bisim.nr_transitions == 105 + assert model_bisim.model_type == stormpy.ModelType.DTMC + assert not model_bisim.supports_parameters + def test_parametric_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) assert program.nr_modules == 5 @@ -60,4 +75,4 @@ class TestBisimulation: initial_state_bisim = model_bisim.initial_states[0] assert initial_state_bisim == 316 ratFunc_bisim = result_bisim.at(initial_state_bisim) - assert ratFunc == ratFunc_bisim + assert ratFunc == ratFunc_bisim \ No newline at end of file From 054df185c0f49f96052217ea02582745dbc5ca7c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 18:33:29 +0200 Subject: [PATCH 33/38] Transformation from symbolic model to sparse model --- lib/stormpy/__init__.py | 11 ++++++++++ src/core/transformation.cpp | 7 +++++++ src/core/transformation.h | 5 +++++ src/mod_core.cpp | 2 ++ tests/core/test_transformation.py | 35 +++++++++++++++++++++++++++++++ 5 files changed, 60 insertions(+) create mode 100644 src/core/transformation.cpp create mode 100644 src/core/transformation.h create mode 100644 tests/core/test_transformation.py diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 7d76643..9d3829c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -332,6 +332,17 @@ def check_model_hybrid(model, property, only_initial_states=False): task = core.CheckTask(formula, only_initial_states) return core._model_checking_hybrid_engine(model, task) +def transform_to_sparse_model(model): + """ + Transform model in symbolic representation into model in sparse representation. + :param model: Symbolic model. + :return: Sparse model. + """ + if model.supports_parameters: + return core._transform_to_sparse_parametric_model(model) + else: + return core._transform_to_sparse_model(model) + def prob01min_states(model, eventually_formula): assert type(eventually_formula) == logic.EventuallyFormula diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp new file mode 100644 index 0000000..984c0e8 --- /dev/null +++ b/src/core/transformation.cpp @@ -0,0 +1,7 @@ +#include "transformation.h" + +void define_transformation(py::module& m) { + // Transform model + m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model")); + m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model")); +} \ No newline at end of file diff --git a/src/core/transformation.h b/src/core/transformation.h new file mode 100644 index 0000000..d098346 --- /dev/null +++ b/src/core/transformation.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_transformation(py::module& m); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 615a7ef..5a84f58 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -7,6 +7,7 @@ #include "core/input.h" #include "core/analysis.h" #include "core/environment.h" +#include "core/transformation.h" PYBIND11_MODULE(core, m) { m.doc() = "core"; @@ -28,4 +29,5 @@ PYBIND11_MODULE(core, m) { define_input(m); define_graph_constraints(m); define_environment(m); + define_transformation(m); } diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py new file mode 100644 index 0000000..562f85f --- /dev/null +++ b/tests/core/test_transformation.py @@ -0,0 +1,35 @@ +import stormpy +import stormpy.logic +from helpers.helper import get_example_path + + +class TestTransformation: + def test_transform_symbolic_dtmc_to_sparse(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) + model = stormpy.build_symbolic_model(program) + assert model.nr_states == 8607 + assert model.nr_transitions == 15113 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanDtmc + symbolic_model = stormpy.transform_to_sparse_model(model) + assert symbolic_model.nr_states == 8607 + assert symbolic_model.nr_transitions == 15113 + assert symbolic_model.model_type == stormpy.ModelType.DTMC + assert not symbolic_model.supports_parameters + assert type(symbolic_model) is stormpy.SparseDtmc + + def test_transform_symbolic_parametric_dtmc_to_sparse(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + model = stormpy.build_symbolic_parametric_model(program) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert type(model) is stormpy.SymbolicSylvanParametricDtmc + symbolic_model = stormpy.transform_to_sparse_model(model) + assert symbolic_model.nr_states == 13 + assert symbolic_model.nr_transitions == 20 + assert symbolic_model.model_type == stormpy.ModelType.DTMC + assert symbolic_model.supports_parameters + assert type(symbolic_model) is stormpy.SparseParametricDtmc From c42ccaf644f057cb959c37593a877c12826d4a1f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 22 May 2018 10:30:48 +0200 Subject: [PATCH 34/38] Added missing include --- src/core/bisimulation.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index e7746ba..6926791 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -1,4 +1,5 @@ #include "bisimulation.h" +#include "storm/models/symbolic/StandardRewardModel.h" template From 78a56cf73204123eac5e75a546ad856bba9dd537 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 22 May 2018 11:04:39 +0200 Subject: [PATCH 35/38] Added missing include --- src/core/modelchecking.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 1084a12..7faafe0 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -1,5 +1,6 @@ #include "modelchecking.h" #include "result.h" +#include "storm/models/symbolic/StandardRewardModel.h" template using CheckTask = storm::modelchecker::CheckTask; From 5d4c344a9c58f0ccbcd61809900dd35c63afdfd7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 22 May 2018 12:55:59 +0200 Subject: [PATCH 36/38] Added missing include --- src/core/transformation.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index 984c0e8..6db4330 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -1,4 +1,5 @@ #include "transformation.h" +#include "storm/models/symbolic/StandardRewardModel.h" void define_transformation(py::module& m) { // Transform model From 3cced14e294a8b2d503059b2f75c0d0bb90b9ee9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 22 May 2018 14:48:28 +0200 Subject: [PATCH 37/38] Typo --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index c6542a8..deedadd 100755 --- a/setup.py +++ b/setup.py @@ -190,7 +190,7 @@ class CMakeBuild(build_ext): env['CXXFLAGS'] = '{} -DVERSION_INFO=\\"{}\\"'.format(env.get('CXXFLAGS', ''), self.distribution.get_version()) setup_helper.ensure_dir_exists(self.build_temp) - print("Pycarl - CMake args={}".format(cmake_args)) + print("Stormpy - CMake args={}".format(cmake_args)) # Call cmake subprocess.check_call(['cmake', ext.sourcedir] + cmake_args, cwd=self.build_temp, env=env) subprocess.check_call(['cmake', '--build', '.', '--target', ext.name] + build_args, cwd=self.build_temp) From 5cdc14bb0aee2cae9ecb419e6f7aeffee3e4face Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 May 2018 20:05:58 +0200 Subject: [PATCH 38/38] Use find_library to search for storm libs --- CMakeLists.txt | 1 + cmake/CMakeLists.txt | 11 +++++------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f0d0130..af8c593 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -9,6 +9,7 @@ option(STORMPY_DISABLE_SIGNATURE_DOC "disables the signature in the documentatio configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/config.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/generated/config.h) message(STATUS "STORM-DIR: ${storm_DIR}") +message(STATUS "STORM-INCLUDE-DIR: ${storm_INCLUDE_DIR}") function(stormpy_module NAME) # second, optional argument are ADDITIONAL_LIBRARIES diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt index bbaf9c4..62123d9 100644 --- a/cmake/CMakeLists.txt +++ b/cmake/CMakeLists.txt @@ -6,20 +6,19 @@ find_package(storm REQUIRED) # Set configuration set(STORM_DIR ${storm_DIR}) set(STORM_VERSION ${storm_VERSION}) +set(STORM_LIBS ${storm_LIBRARIES}) # Check for storm-pars -if(EXISTS "${storm_DIR}/lib/libstorm-pars.dylib") - set(HAVE_STORM_PARS TRUE) -elseif(EXISTS "${storm_DIR}/lib/libstorm-pars.so") +find_library(STORM_PARS NAMES storm-pars HINTS "${storm_DIR}/lib/") +if(STORM_PARS) set(HAVE_STORM_PARS TRUE) else() set(HAVE_STORM_PARS FALSE) endif() # Check for storm-dft -if(EXISTS "${storm_DIR}/lib/libstorm-dft.dylib") - set(HAVE_STORM_DFT TRUE) -elseif(EXISTS "${storm_DIR}/lib/libstorm-dft.so") +find_library(STORM_DFT NAMES storm-dft HINTS "${storm_DIR}/lib/") +if(STORM_DFT) set(HAVE_STORM_DFT TRUE) else() set(HAVE_STORM_DFT FALSE)