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/.travis.yml b/.travis.yml index 4c79c06..c5c081d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -25,28 +25,34 @@ notifications: # jobs: include: - # docker storm:latest + # Docker Storm master - 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-debug:latest + # 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 + 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 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: @@ -59,3 +65,9 @@ jobs: on: branch: master + # Allow failures of stable versions as new features might have been added + 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 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/CMakeLists.txt b/CMakeLists.txt index c400ebd..af8c593 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,57 +1,43 @@ 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") - +message(STATUS "STORM-INCLUDE-DIR: ${storm_INCLUDE_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/MANIFEST.in b/MANIFEST.in new file mode 100644 index 0000000..bbfd747 --- /dev/null +++ b/MANIFEST.in @@ -0,0 +1,6 @@ +include CMakeLists.txt +recursive-include setup/ *.py +recursive-include cmake/ * +recursive-include src/ * +recursive-include resources/ * +recursive-include lib/stormpy/examples/files/ * diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt index ef03051..62123d9 100644 --- a/cmake/CMakeLists.txt +++ b/cmake/CMakeLists.txt @@ -2,28 +2,28 @@ 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}) +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) 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 +48,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) diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 124c702..765149a 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -8,6 +8,7 @@ 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 + doc/parametric_models \ 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/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/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..947036a 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 ------------------------------------------------ @@ -124,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/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..80ce6c7 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,45 @@ or:: $ pip install -ve . -.. topic:: Specifying which Storm library to use +Optional build arguments +^^^^^^^^^^^^^^^^^^^^^^^^ + +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:: - 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 - + +* *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:: + + $ 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 +---------------------------- + 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). 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() 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/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index f1ee516..9d3829c 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 @@ -18,108 +23,190 @@ 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 _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 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. + """ + 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. - :rtype: SparseDtmc or SparseMdp """ 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_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() + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description, formulae) else: - raise StormError("Not supported non-parametric model constructed") + intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description) + 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 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_symbolic_description(symbolic_description, formulae) + else: + intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description) + 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: - 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() + 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: - raise StormError("Not supported parametric model constructed") + 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 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): @@ -130,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) @@ -137,13 +235,41 @@ 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. :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 + """ + 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. + :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 @@ -163,6 +289,61 @@ 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 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 labelform = eventually_formula.subformula 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/setup.py b/setup.py index 6aba669..deedadd 100755 --- a/setup.py +++ b/setup.py @@ -3,9 +3,8 @@ 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 import setup.helper as setup_helper @@ -15,7 +14,11 @@ 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" + +# 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): @@ -55,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) @@ -187,20 +190,12 @@ 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) -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(), @@ -208,12 +203,25 @@ 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='', - packages=['stormpy', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', - 'stormpy.pars', 'stormpy.dft'], + long_description=long_description, + long_description_content_type='text/markdown', + project_urls={ + 'Documentation': 'https://moves-rwth.github.io/stormpy/', + 'Source': 'https://github.com/moves-rwth/stormpy/', + 'Bug reports': 'https://github.com/moves-rwth/stormpy/issues', + }, + classifiers=[ + 'Intended Audience :: Science/Research', + 'Topic :: Scientific/Engineering', + 'Topic :: Software Development :: Libraries :: Python Modules', + ], + + 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'), @@ -221,9 +229,9 @@ setup( CMakeExtension('storage', subdir='storage'), CMakeExtension('utility', subdir='utility'), CMakeExtension('dft', subdir='dft'), - CMakeExtension('pars', subdir='pars'), - ], - cmdclass={'build_ext': CMakeBuild, 'test': PyTest}, + CMakeExtension('pars', subdir='pars')], + + cmdclass={'build_ext': CMakeBuild}, zip_safe=False, install_requires=['pycarl>=2.0.2'], setup_requires=['pytest-runner'], diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index 7feddd0..6926791 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -1,4 +1,11 @@ #include "bisimulation.h" +#include "storm/models/symbolic/StandardRewardModel.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) { @@ -6,6 +13,8 @@ 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/src/core/core.cpp b/src/core/core.cpp index 104f020..8df3e2e 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 @@ -57,9 +60,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); @@ -70,18 +73,30 @@ std::shared_ptr buildSparseModel(storm::storage::Symbo } } -// Thin wrapper for model building using one formula as argument template std::shared_ptr buildSparseModelWithOptions(storm::storage::SymbolicModelDescription const& modelDescription, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) { return storm::api::buildSparseModel(modelDescription, options, jit, doctor); +} +// 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_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_with_options", &buildSparseModelWithOptions, "Build the model", py::arg("model_description"), py::arg("options"), 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_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), 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") = ""); @@ -97,15 +112,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/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 703e53c..7faafe0 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -1,15 +1,28 @@ #include "modelchecking.h" #include "result.h" +#include "storm/models/symbolic/StandardRewardModel.h" 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 +55,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 7514c9f..45ac4a7 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/src/core/transformation.cpp b/src/core/transformation.cpp new file mode 100644 index 0000000..6db4330 --- /dev/null +++ b/src/core/transformation.cpp @@ -0,0 +1,8 @@ +#include "transformation.h" +#include "storm/models/symbolic/StandardRewardModel.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 9d58ab1..d3a752e 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -8,6 +8,7 @@ #include "core/analysis.h" #include "core/counterexample.h" #include "core/environment.h" +#include "core/transformation.h" PYBIND11_MODULE(core, m) { m.doc() = "core"; @@ -30,4 +31,5 @@ PYBIND11_MODULE(core, m) { define_input(m); define_graph_constraints(m); define_environment(m); + define_transformation(m); } diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 28a328e..e85dd03 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -11,6 +11,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"; @@ -21,7 +23,9 @@ PYBIND11_MODULE(storage, m) { define_bitvector(m); define_model(m); + define_sparse_model(m); define_sparse_matrix(m); + define_symbolic_model(m, "Sylvan"); define_state(m); define_prism(m); define_jani(m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index ec3d43f..f2f49a1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -8,58 +8,65 @@ #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 #include - -using ModelBase = storm::models::ModelBase; -using state_type = storm::storage::sparse::state_type; +// Typedefs 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; - -// Thin wrapper for getting initial states +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; + +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 template -std::vector getInitialStates(Model 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 -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(); -} - // 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 +82,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,117 +106,210 @@ 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") - ; - - // 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); + .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") + .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") + ; +} + + +// Bindings for sparse models +void define_sparse_model(py::module& m) { + + // 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", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") - .def_property_readonly("initial_states", &getInitialStates, "Initial states") - .def_property_readonly("states", [](Model& model) { + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") + .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_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()) ; - 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); + // 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", &Model::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("labeling", &getLabeling, "Labels") + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") + .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", &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")) ; - 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);}) + 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") + ; + +} + + +// 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")) + ; - .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, (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 c779f26..7643d39 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -1,8 +1,10 @@ -#ifndef PYTHON_STORAGE_MODEL_H_ -#define PYTHON_STORAGE_MODEL_H_ +#pragma once #include "common.h" +#include "storm/storage/dd/DdType.h" void define_model(py::module& m); +void define_sparse_model(py::module& m); -#endif /* PYTHON_STORAGE_MODEL_H_ */ +template +void define_symbolic_model(py::module& m, std::string vt_suffix); diff --git a/tests/.gitignore b/tests/.gitignore deleted file mode 100644 index bee8a64..0000000 --- a/tests/.gitignore +++ /dev/null @@ -1 +0,0 @@ -__pycache__ 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 diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index e4df9eb..c8687bc 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -124,6 +124,27 @@ 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) + + 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/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 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(): 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 diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index d3c4b90..2598e3b 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 @@ -133,3 +123,90 @@ class TestModel: 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) diff --git a/travis/build.sh b/travis/build.sh index 745305b..2bbe2e8 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -11,9 +11,9 @@ 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 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 $? ;; 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