Matthias Volk
7 years ago
113 changed files with 4263 additions and 2418 deletions
-
15.gitignore
-
28.travis.yml
-
18CHANGELOG.md
-
40CMakeLists.txt
-
6MANIFEST.in
-
23cmake/CMakeLists.txt
-
11doc/source/advanced_topics.rst
-
17doc/source/api.rst
-
8doc/source/api/core.rst
-
7doc/source/api/dft.rst
-
7doc/source/api/exceptions.rst
-
7doc/source/api/info.rst
-
7doc/source/api/logic.rst
-
7doc/source/api/pars.rst
-
7doc/source/api/storage.rst
-
7doc/source/api/utility.rst
-
12doc/source/code_stormpy_logic.rst
-
11doc/source/code_stormpy_storage.rst
-
6doc/source/conf.py
-
3doc/source/contributors.rst
-
2doc/source/doc/building_models.rst
-
51doc/source/doc/dfts.rst
-
82doc/source/doc/engines.rst
-
105doc/source/doc/exploration.rst
-
60doc/source/doc/parametric_models.rst
-
4doc/source/doc/reward_models.rst
-
99doc/source/doc/schedulers.rst
-
8doc/source/doc/shortest_paths.rst
-
74doc/source/getting_started.rst
-
12doc/source/index.rst
-
80doc/source/installation.rst
-
37examples/04-getting-started.py
-
26examples/06-getting-started.py
-
29examples/dfts/01-dfts.py
-
30examples/exploration/01-exploration.py
-
38examples/exploration/02-exploration.py
-
17examples/highlevel_models/01-highlevel-models.py
-
41examples/parametric_models/01-parametric-models.py
-
4examples/parametric_models/02-parametric-models.py
-
0examples/reward_models.py
-
19examples/schedulers/01-schedulers.py
-
37examples/schedulers/02-schedulers.py
-
4lib/.gitignore
-
359lib/stormpy/__init__.py
-
2lib/stormpy/_version.py
-
14lib/stormpy/examples/files.py
-
90lib/stormpy/examples/files/ctmc/dft.drn
-
24lib/stormpy/examples/files/dft/hecs.dft
-
2764lib/stormpy/examples/files/dtmc/brp.jani
-
126lib/stormpy/examples/files/mdp/maze_2.nm
-
139lib/stormpy/examples/files/pomdp/maze_2.prism
-
57setup.py
-
9src/core/bisimulation.cpp
-
61src/core/core.cpp
-
7src/core/core.h
-
63src/core/counterexample.cpp
-
5src/core/counterexample.h
-
42src/core/environment.cpp
-
19src/core/input.cpp
-
32src/core/modelchecking.cpp
-
47src/core/result.cpp
-
43src/core/transformation.cpp
-
5src/core/transformation.h
-
27src/dft/analysis.cpp
-
5src/dft/analysis.h
-
1src/dft/common.h
-
51src/dft/dft.cpp
-
5src/dft/dft.h
-
20src/dft/io.cpp
-
6src/dft/io.h
-
39src/logic/formulae.cpp
-
7src/mod_core.cpp
-
5src/mod_dft.cpp
-
1src/mod_pars.cpp
-
8src/mod_storage.cpp
-
5src/mod_utility.cpp
-
3src/pars/common.h
-
45src/pars/model_instantiator.cpp
-
1src/pars/model_instantiator.h
-
15src/storage/choiceorigins.cpp
-
6src/storage/choiceorigins.h
-
44src/storage/expressions.cpp
-
162src/storage/jani.cpp
-
5src/storage/jani.h
-
3src/storage/labeling.cpp
-
6src/storage/matrix.cpp
-
353src/storage/model.cpp
-
8src/storage/model.h
-
36src/storage/prism.cpp
-
1src/storage/scheduler.cpp
-
10src/utility/chrono.cpp
-
5src/utility/chrono.h
-
32src/utility/smtsolver.cpp
-
5src/utility/smtsolver.h
-
1tests/.gitignore
-
17tests/core/test_bisimulation.py
-
81tests/core/test_modelchecking.py
-
81tests/core/test_transformation.py
-
17tests/dft/test_analysis.py
-
20tests/dft/test_build.py
@ -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 |
|||
@ -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} ${storm-parsers_INCLUDE_DIR} ${storm-counterexamples_INCLUDE_DIR} ${ARGV2} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) |
|||
target_link_libraries(${NAME} PRIVATE storm storm-parsers storm-counterexamples ${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) |
|||
target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${storm-parsers_INCLUDE_DIR} ${storm-counterexamples_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) |
|||
target_link_libraries(${NAME} PRIVATE storm storm-parsers storm-counterexamples) |
|||
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() |
|||
@ -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/ * |
|||
@ -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 |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.dft |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.dft |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.exceptions |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.exceptions |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.info |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.info |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.logic |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.logic |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.pars |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.pars |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.storage |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.storage |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -0,0 +1,7 @@ |
|||
Stormpy.utility |
|||
************************** |
|||
|
|||
.. automodule:: stormpy.utility |
|||
:members: |
|||
:undoc-members: |
|||
:imported-members: |
|||
@ -1,12 +0,0 @@ |
|||
Stormpy.logic |
|||
************************** |
|||
|
|||
.. automodule:: stormpy |
|||
|
|||
|
|||
Members |
|||
========================= |
|||
|
|||
|
|||
.. automodule:: stormpy.logic.logic |
|||
:members: |
|||
@ -1,11 +0,0 @@ |
|||
Stormpy.storage |
|||
************************** |
|||
|
|||
.. automodule:: stormpy |
|||
|
|||
Members |
|||
============================== |
|||
|
|||
.. automodule:: stormpy.storage.storage |
|||
:members: |
|||
|
|||
@ -0,0 +1,51 @@ |
|||
******************* |
|||
Dynamic Fault Trees |
|||
******************* |
|||
|
|||
|
|||
Building DFTs |
|||
============= |
|||
.. seealso:: `01-dfts.py <https://github.com/moves-rwth/stormpy/blob/master/examples/dfts/01-dfts.py>`_ |
|||
|
|||
Dynamic fault trees can be loaded from either the Galileo format or from a custom JSON form. |
|||
A file containing the DFT in the Galileo format can be loaded via ``load_dft_galileo_file(path)``. |
|||
The custom JSON format can be loaded from a file via ``load_dft_json_file(path)`` or directly from a string via ``load_dft_json_string(path)``. |
|||
We start by loading a simple DFT containing an AND gate from JSON:: |
|||
|
|||
>>> import stormpy |
|||
>>> import stormpy.dft |
|||
>>> import stormpy.examples |
|||
>>> import stormpy.examples.files |
|||
>>> path_json = stormpy.examples.files.dft_json_and |
|||
>>> dft_small = stormpy.dft.load_dft_json_file(path_json) |
|||
>>> print(dft_small) |
|||
Top level index: 2, Nr BEs2 |
|||
|
|||
Next we load a more complex DFT from the Galileo format:: |
|||
|
|||
>>> path_galileo = stormpy.examples.files.dft_galileo_hecs |
|||
>>> dft = stormpy.dft.load_dft_galileo_file(path_galileo) |
|||
|
|||
After loading the DFT, we can display some common statistics about the model:: |
|||
|
|||
>>> print("DFT with {} elements.".format(dft.nr_elements())) |
|||
DFT with 23 elements. |
|||
>>> print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic())) |
|||
DFT has 13 BEs and 2 dynamic elements. |
|||
|
|||
|
|||
Analyzing DFTs |
|||
============== |
|||
.. seealso:: `01-dfts.py <https://github.com/moves-rwth/stormpy/blob/master/examples/dfts/01-dfts.py>`_ |
|||
|
|||
The next step is to analyze the DFT via ``analyze_dft(dft, formula)``. |
|||
Here we can use all standard properties as described in :ref:`getting-started-building-properties`. |
|||
In our example we compute the `Mean-time-to-failure (MTTF)`:: |
|||
|
|||
>>> formula_str = "T=? [ F \"failed\" ]" |
|||
>>> formulas = stormpy.parse_properties(formula_str) |
|||
>>> results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) |
|||
>>> result = results[0] |
|||
>>> print("MTTF: {:.2f}".format(result)) |
|||
MTTF: 363.89 |
|||
|
|||
@ -0,0 +1,82 @@ |
|||
*************** |
|||
Engines |
|||
*************** |
|||
|
|||
Background |
|||
===================== |
|||
|
|||
Storm supports different engines for building and checking a model. A detailed comparison of the different engines provided in Storm can be found on the `Storm website <http://www.stormchecker.org/documentation/usage/engines.html>`_. |
|||
|
|||
|
|||
Sparse engine |
|||
=============================== |
|||
|
|||
In all of the examples so far we used the default sparse engine: |
|||
|
|||
>>> import stormpy.examples |
|||
>>> import stormpy.examples.files |
|||
>>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die) |
|||
>>> properties = stormpy.parse_properties_for_prism_program('P=? [F "one"]', prism_program) |
|||
>>> sparse_model = stormpy.build_sparse_model(prism_program, properties) |
|||
>>> print(type(sparse_model)) |
|||
<class 'stormpy.storage.storage.SparseDtmc'> |
|||
>>> print("Number of states: {}".format(sparse_model.nr_states)) |
|||
Number of states: 13 |
|||
>>> print("Number of transitions: {}".format(sparse_model.nr_transitions)) |
|||
Number of transitions: 20 |
|||
|
|||
The model checking was also done in the sparse engine: |
|||
|
|||
>>> sparse_result = stormpy.check_model_sparse(sparse_model, properties[0]) |
|||
>>> initial_state = sparse_model.initial_states[0] |
|||
>>> print(sparse_result.at(initial_state)) |
|||
0.16666666666666666 |
|||
|
|||
|
|||
Symbolic engine |
|||
=============================== |
|||
|
|||
Instead of using the sparse engine, one can also use a symbolic representation in terms of `binary decision diagrams (BDDs)`. |
|||
To use the symbolic (dd) engine, we use the symbolic versions for the building and model checking: |
|||
|
|||
>>> symbolic_model = stormpy.build_symbolic_model(prism_program, properties) |
|||
>>> print(type(symbolic_model)) |
|||
<class 'stormpy.storage.storage.SymbolicSylvanDtmc'> |
|||
>>> print("Number of states: {}".format(symbolic_model.nr_states)) |
|||
Number of states: 13 |
|||
>>> print("Number of transitions: {}".format(symbolic_model.nr_transitions)) |
|||
Number of transitions: 20 |
|||
>>> symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0]) |
|||
>>> print(symbolic_result) |
|||
[0, 1] (range) |
|||
|
|||
We can also filter the computed results and only consider the initial states: |
|||
|
|||
>>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model) |
|||
>>> symbolic_result.filter(filter) |
|||
>>> print(symbolic_result.min) |
|||
0.16666650772094727 |
|||
|
|||
It is also possible to first build the model symbolically and then transform it into a sparse model: |
|||
|
|||
>>> print(type(symbolic_model)) |
|||
<class 'stormpy.storage.storage.SymbolicSylvanDtmc'> |
|||
>>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model) |
|||
>>> print(type(transformed_model)) |
|||
<class 'stormpy.storage.storage.SparseDtmc'> |
|||
|
|||
|
|||
Hybrid engine |
|||
=============================== |
|||
|
|||
A third possibility is to use the hybrid engine, a combination of sparse and dd engines. |
|||
It first builds the model symbolically. |
|||
The actual model checking is then performed with the engine which is deemed most suitable for the given task. |
|||
|
|||
>>> print(type(symbolic_model)) |
|||
<class 'stormpy.storage.storage.SymbolicSylvanDtmc'> |
|||
>>> hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0]) |
|||
>>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model) |
|||
>>> hybrid_result.filter(filter) |
|||
>>> print(hybrid_result) |
|||
0.166667 |
|||
@ -0,0 +1,105 @@ |
|||
**************** |
|||
Exploring Models |
|||
**************** |
|||
|
|||
Background |
|||
===================== |
|||
|
|||
Often, stormpy is used as a testbed for new algorithms. |
|||
An essential step is to transfer the (low-level) descriptions of an MDP or other state-based model into |
|||
an own algorithm. In this section, we discuss some of the functionality. |
|||
|
|||
Reading MDPs |
|||
===================== |
|||
|
|||
.. seealso:: `01-exploration.py <https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/01-exploration.py>`_ |
|||
|
|||
In :doc:`../getting_started`, we briefly iterated over a DTMC. In this section, we explore an MDP:: |
|||
|
|||
>>> import doctest |
|||
>>> doctest.ELLIPSIS_MARKER = '-etc-' # doctest:+ELLIPSIS |
|||
>>> import stormpy |
|||
>>> import stormpy.examples |
|||
>>> import stormpy.examples.files |
|||
>>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze) |
|||
>>> prop = "R=? [F \"goal\"]" |
|||
|
|||
>>> properties = stormpy.parse_properties_for_prism_program(prop, program, None) |
|||
>>> model = stormpy.build_model(program, properties) |
|||
|
|||
The iteration over the model is as before, but now, for every action, we can have several transitions:: |
|||
|
|||
>>> for state in model.states: |
|||
... if state.id in model.initial_states: |
|||
... print("State {} is initial".format(state.id)) |
|||
... for action in state.actions: |
|||
... for transition in action.transitions: |
|||
... print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column)) |
|||
-etc- |
|||
|
|||
The output (omitted for brievety) contains sentences like:: |
|||
|
|||
From state 1 by action 0, with probability 1.0, go to state 2 |
|||
From state 1 by action 1, with probability 1.0, go to state 1 |
|||
|
|||
|
|||
|
|||
Internally, storm can hold hints to the origin of the actions, which may be helpful to give meaning and for debugging. |
|||
As the availability and the encoding of this data depends on the input model, we discuss these features in :doc:`highlevel_models`. |
|||
|
|||
|
|||
Storm currently supports deterministic rewards on states or actions. More information can be found in :doc:`reward_models`. |
|||
|
|||
|
|||
Reading POMDPs |
|||
====================== |
|||
.. seealso:: `02-exploration.py <https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/01-exploration.py>`_ |
|||
|
|||
|
|||
Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before. |
|||
|
|||
>>> import stormpy |
|||
>>> import stormpy.examples |
|||
>>> import stormpy.examples.files |
|||
>>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) |
|||
>>> prop = "R=? [F \"goal\"]" |
|||
>>> properties = stormpy.parse_properties_for_prism_program(prop, program, None) |
|||
>>> model = stormpy.build_model(program, properties) |
|||
|
|||
Indeed, all that changed in the code above is the example we use. |
|||
And, that the model type now is a POMDP:: |
|||
|
|||
>>> print(model.model_type) |
|||
ModelType.POMDP |
|||
|
|||
Additionally, POMDPs have a set of observations, which are internally just numbered by an integer from 0 to the number of observations -1 :: |
|||
|
|||
>>> print(model.nr_observations) |
|||
8 |
|||
>>> for state in model.states: |
|||
... print("State {} has observation id {}".format(state.id, model.observations[state.id])) |
|||
State 0 has observation id 6 |
|||
State 1 has observation id 1 |
|||
State 2 has observation id 4 |
|||
State 3 has observation id 7 |
|||
State 4 has observation id 4 |
|||
State 5 has observation id 3 |
|||
State 6 has observation id 0 |
|||
State 7 has observation id 0 |
|||
State 8 has observation id 0 |
|||
State 9 has observation id 0 |
|||
State 10 has observation id 0 |
|||
State 11 has observation id 0 |
|||
State 12 has observation id 2 |
|||
State 13 has observation id 2 |
|||
State 14 has observation id 4 |
|||
State 15 has observation id 5 |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
Reading MAs |
|||
====================== |
|||
|
|||
To be continued... |
|||
@ -0,0 +1,60 @@ |
|||
***************** |
|||
Parametric Models |
|||
***************** |
|||
|
|||
|
|||
|
|||
Instantiating parametric models |
|||
=============================== |
|||
.. seealso:: `01-parametric-models.py <https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/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 <https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/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) |
|||
|
|||
@ -0,0 +1,99 @@ |
|||
*********************** |
|||
Working with Schedulers |
|||
*********************** |
|||
|
|||
In non-deterministic models the notion of a scheduler (or policy) is important. |
|||
The scheduler determines which action to take at each state. |
|||
|
|||
For a given reachability property, Storm can return the scheduler realizing the resulting probability. |
|||
|
|||
Examining Schedulers for MDPs |
|||
============================= |
|||
|
|||
.. seealso:: `01-schedulers.py <https://github.com/moves-rwth/stormpy/blob/master/examples/schedulers/01-schedulers.py>`_ |
|||
|
|||
As in :doc:`../getting_started`, we import some required modules and build a model from the example files:: |
|||
|
|||
>>> import stormpy |
|||
>>> import stormpy.core |
|||
>>> import stormpy.examples |
|||
>>> import stormpy.examples.files |
|||
|
|||
>>> path = stormpy.examples.files.prism_mdp_coin_2_2 |
|||
>>> formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" |
|||
>>> program = stormpy.parse_prism_program(path) |
|||
>>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program) |
|||
>>> model = stormpy.build_model(program, formulas) |
|||
|
|||
Next we check the model and make sure to extract the scheduler: |
|||
|
|||
>>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) |
|||
|
|||
The result then contains the scheduler we want: |
|||
|
|||
>>> assert result.has_scheduler |
|||
>>> scheduler = result.scheduler |
|||
>>> assert scheduler.memoryless |
|||
>>> assert scheduler.deterministic |
|||
>>> print(scheduler) |
|||
___________________________________________________________________ |
|||
Fully defined memoryless deterministic scheduler: |
|||
model state: choice(s) |
|||
0 0 |
|||
1 0 |
|||
2 1 |
|||
3 0 |
|||
-etc- |
|||
|
|||
To get the information which action the scheduler chooses in which state, we can simply iterate over the states: |
|||
|
|||
>>> for state in model.states: |
|||
... choice = scheduler.get_choice(state) |
|||
... action = choice.get_deterministic_choice() |
|||
... print("In state {} choose action {}".format(state, action)) |
|||
In state 0 choose action 0 |
|||
In state 1 choose action 0 |
|||
In state 2 choose action 1 |
|||
In state 3 choose action 0 |
|||
In state 4 choose action 0 |
|||
In state 5 choose action 0 |
|||
-etc- |
|||
|
|||
|
|||
Examining Schedulers for Markov automata |
|||
======================================== |
|||
|
|||
.. seealso:: `02-schedulers.py <https://github.com/moves-rwth/stormpy/blob/master/examples/schedulers/02-schedulers.py>`_ |
|||
|
|||
Currently there is no support yet for scheduler extraction on MAs. |
|||
However, if the timing information is not relevant for the property, we can circumvent this lack by first transforming the MA to an MDP. |
|||
|
|||
We build the model as before: |
|||
|
|||
>>> path = stormpy.examples.files.prism_ma_simple |
|||
>>> formula_str = "Tmin=? [ F s=4 ]" |
|||
|
|||
>>> program = stormpy.parse_prism_program(path, False, True) |
|||
>>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program) |
|||
>>> ma = stormpy.build_model(program, formulas) |
|||
|
|||
Next we transform the continuous-time model into a discrete-time model. |
|||
Note that all timing information is lost at this point. |
|||
|
|||
>>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) |
|||
>>> assert mdp.model_type == stormpy.ModelType.MDP |
|||
|
|||
After the transformation we have obtained an MDP where we can extract the scheduler as shown before: |
|||
|
|||
>>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) |
|||
>>> scheduler = result.scheduler |
|||
>>> print(scheduler) |
|||
___________________________________________________________________ |
|||
Fully defined memoryless deterministic scheduler: |
|||
model state: choice(s) |
|||
0 1 |
|||
1 0 |
|||
2 0 |
|||
3 0 |
|||
4 0 |
|||
-etc- |
|||
@ -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__': |
|||
|
|||
@ -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() |
|||
@ -0,0 +1,29 @@ |
|||
import stormpy |
|||
import stormpy.dft |
|||
|
|||
import stormpy.examples |
|||
import stormpy.examples.files |
|||
|
|||
|
|||
def example_dfts_01(): |
|||
# Load from JSON |
|||
path_json = stormpy.examples.files.dft_json_and |
|||
dft_small = stormpy.dft.load_dft_json_file(path_json) |
|||
print(dft_small) |
|||
|
|||
# Load from Galileo |
|||
path = stormpy.examples.files.dft_galileo_hecs |
|||
dft = stormpy.dft.load_dft_galileo_file(path) |
|||
print("DFT with {} elements.".format(dft.nr_elements())) |
|||
print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic())) |
|||
|
|||
# Analyze |
|||
formula_str = "T=? [ F \"failed\" ]" |
|||
formulas = stormpy.parse_properties(formula_str) |
|||
results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) |
|||
result = results[0] |
|||
print(result) |
|||
|
|||
|
|||
if __name__ == '__main__': |
|||
example_dfts_01() |
|||
@ -0,0 +1,30 @@ |
|||
import stormpy |
|||
import stormpy.core |
|||
|
|||
import stormpy.examples |
|||
import stormpy.examples.files |
|||
|
|||
|
|||
def example_exploration_01(): |
|||
""" |
|||
Example to exploration of MDPs. |
|||
:return: |
|||
""" |
|||
program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) |
|||
prop = "R=? [F \"goal\"]" |
|||
properties = stormpy.parse_properties_for_prism_program(prop, program, None) |
|||
model = stormpy.build_model(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 {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), |
|||
transition.column)) |
|||
|
|||
|
|||
if __name__ == '__main__': |
|||
example_exploration_01() |
|||
@ -0,0 +1,38 @@ |
|||
import stormpy |
|||
import stormpy.core |
|||
|
|||
import stormpy.examples |
|||
import stormpy.examples.files |
|||
|
|||
|
|||
def example_exploration_02(): |
|||
""" |
|||
Example to exploration of POMDPs. |
|||
:return: |
|||
""" |
|||
program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) |
|||
prop = "R=? [F \"goal\"]" |
|||
properties = stormpy.parse_properties_for_prism_program(prop, program, None) |
|||
model = stormpy.build_model(program, properties) |
|||
print(model.model_type) |
|||
# Internally, POMDPs are just MDPs with additional observation information. |
|||
# Thus, data structure exploration for MDPs can be applied as before. |
|||
initial_state = model.initial_states[0] |
|||
|
|||
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 {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), |
|||
transition.column)) |
|||
|
|||
print(model.nr_observations) |
|||
|
|||
for state in model.states: |
|||
print("State {} has observation id {}".format(state.id, model.observations[state.id])) |
|||
|
|||
|
|||
|
|||
if __name__ == '__main__': |
|||
example_exploration_02() |
|||
@ -0,0 +1,17 @@ |
|||
import stormpy |
|||
import stormpy.core |
|||
|
|||
import stormpy.examples |
|||
import stormpy.examples.files |
|||
|
|||
|
|||
def example_highlevel_models(): |
|||
path = stormpy.examples.files.prism_pdtmc_die |
|||
prism_program = stormpy.parse_prism_program(path) |
|||
for c in prism_program.constants: |
|||
print("constant {} with type {} is {} defined".format(c.name, c.type, "" if c.defined else "not")) |
|||
|
|||
|
|||
|
|||
if __name__ == '__main__': |
|||
example_highlevel_models() |
|||
@ -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() |
|||
@ -0,0 +1,37 @@ |
|||
import stormpy |
|||
import stormpy.core |
|||
|
|||
import stormpy.examples |
|||
import stormpy.examples.files |
|||
|
|||
|
|||
def example_schedulers_02(): |
|||
path = stormpy.examples.files.prism_ma_simple |
|||
formula_str = "Tmin=? [ F s=4 ]" |
|||
|
|||
program = stormpy.parse_prism_program(path, False, True) |
|||
formulas = stormpy.parse_properties_for_prism_program(formula_str, program) |
|||
ma = stormpy.build_model(program, formulas) |
|||
assert ma.model_type == stormpy.ModelType.MA |
|||
|
|||
# Convert MA to MDP |
|||
mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) |
|||
assert mdp.model_type == stormpy.ModelType.MDP |
|||
initial_state = mdp.initial_states[0] |
|||
assert initial_state == 0 |
|||
|
|||
result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) |
|||
assert result.has_scheduler |
|||
scheduler = result.scheduler |
|||
print(scheduler) |
|||
assert scheduler.memoryless |
|||
assert scheduler.deterministic |
|||
|
|||
for state in mdp.states: |
|||
choice = scheduler.get_choice(state) |
|||
action = choice.get_deterministic_choice() |
|||
print("In state {} choose action {}".format(state, action)) |
|||
|
|||
|
|||
if __name__ == '__main__': |
|||
example_schedulers_02() |
|||
@ -1,4 +0,0 @@ |
|||
*.so |
|||
__pycache__/ |
|||
stormpy.egg-info/ |
|||
**/_config.py |
|||
@ -1 +1 @@ |
|||
__version__ = "1.2.0" |
|||
__version__ = "1.3.0" |
|||
@ -0,0 +1,24 @@ |
|||
toplevel "n0"; |
|||
"n0" or "n116" "n137" "n120" "n21"; |
|||
"n137" wsp "n139" "n9"; |
|||
"n120" wsp "n118" "n134" "n10"; |
|||
"n21" 3of5 "n111" "n109" "n117" "n110" "n112"; |
|||
"n110" or "n18" "n7"; |
|||
"n117" or "n17" "n7"; |
|||
"n109" or "n15" "n23"; |
|||
"n112" or "n19" "n13"; |
|||
"n13" and "n23" "n7"; |
|||
"n111" or "n14" "n23"; |
|||
"n116" lambda=0.0018 dorm=0.0; |
|||
"n139" lambda=2.0E-5 dorm=0.0; |
|||
"n10" lambda=0.001 dorm=0.0; |
|||
"n118" lambda=0.002 dorm=0.0; |
|||
"n18" lambda=6.0E-4 dorm=0.0; |
|||
"n17" lambda=6.0E-4 dorm=0.0; |
|||
"n15" lambda=6.0E-4 dorm=0.0; |
|||
"n19" lambda=6.0E-4 dorm=0.0; |
|||
"n7" lambda=5.0E-4 dorm=0.0; |
|||
"n23" lambda=5.0E-4 dorm=0.0; |
|||
"n14" lambda=6.0E-4 dorm=0.0; |
|||
"n134" lambda=0.002 dorm=0.0; |
|||
"n9" lambda=1.0E-5 dorm=0.0; |
|||
2764
lib/stormpy/examples/files/dtmc/brp.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,126 @@ |
|||
|
|||
|
|||
// maze example (POMDP) |
|||
// slightly extends that presented in |
|||
// Littman, Cassandra and Kaelbling |
|||
// Learning policies for partially observable environments: Scaling up |
|||
// Technical Report CS, Brown University |
|||
// gxn 29/01/16 |
|||
// Made into a MDP for documentation of stormpy. |
|||
|
|||
// state space (value of variable "s") |
|||
|
|||
// 0 1 2 3 4 |
|||
// 5 6 7 |
|||
// 8 9 10 |
|||
// 11 13 12 |
|||
|
|||
// 13 is the target |
|||
|
|||
mdp |
|||
|
|||
|
|||
module maze |
|||
|
|||
s : [-1..13]; |
|||
|
|||
// initialisation |
|||
[] s=-1 -> 1/13 : (s'=0) |
|||
+ 1/13 : (s'=1) |
|||
+ 1/13 : (s'=2) |
|||
+ 1/13 : (s'=3) |
|||
+ 1/13 : (s'=4) |
|||
+ 1/13 : (s'=5) |
|||
+ 1/13 : (s'=6) |
|||
+ 1/13 : (s'=7) |
|||
+ 1/13 : (s'=8) |
|||
+ 1/13 : (s'=9) |
|||
+ 1/13 : (s'=10) |
|||
+ 1/13 : (s'=11) |
|||
+ 1/13 : (s'=12); |
|||
|
|||
// moving around the maze |
|||
|
|||
[east] s=0 -> (s'=1); |
|||
[west] s=0 -> (s'=0); |
|||
[north] s=0 -> (s'=0); |
|||
[south] s=0 -> (s'=5); |
|||
|
|||
[east] s=1 -> (s'=2); |
|||
[west] s=1 -> (s'=0); |
|||
[north] s=1 -> (s'=1); |
|||
[south] s=1 -> (s'=1); |
|||
|
|||
[east] s=2 -> (s'=3); |
|||
[west] s=2 -> (s'=1); |
|||
[north] s=2 -> (s'=2); |
|||
[south] s=2 -> (s'=6); |
|||
|
|||
[east] s=3 -> (s'=4); |
|||
[west] s=3 -> (s'=2); |
|||
[north] s=3 -> (s'=3); |
|||
[south] s=3 -> (s'=3); |
|||
|
|||
[east] s=4 -> (s'=4); |
|||
[west] s=4 -> (s'=3); |
|||
[north] s=4 -> (s'=4); |
|||
[south] s=4 -> (s'=7); |
|||
|
|||
[east] s=5 -> (s'=5); |
|||
[west] s=5 -> (s'=5); |
|||
[north] s=5 -> (s'=0); |
|||
[south] s=5 -> (s'=8); |
|||
|
|||
[east] s=6 -> (s'=6); |
|||
[west] s=6 -> (s'=6); |
|||
[north] s=6 -> (s'=2); |
|||
[south] s=6 -> (s'=9); |
|||
|
|||
[east] s=7 -> (s'=7); |
|||
[west] s=7 -> (s'=7); |
|||
[north] s=7 -> (s'=4); |
|||
[south] s=7 -> (s'=10); |
|||
|
|||
[east] s=8 -> (s'=8); |
|||
[west] s=8 -> (s'=8); |
|||
[north] s=8 -> (s'=5); |
|||
[south] s=8 -> (s'=11); |
|||
|
|||
[east] s=9 -> (s'=9); |
|||
[west] s=9 -> (s'=9); |
|||
[north] s=9 -> (s'=6); |
|||
[south] s=9 -> (s'=13); |
|||
|
|||
[east] s=10 -> (s'=9); |
|||
[west] s=10 -> (s'=9); |
|||
[north] s=10 -> (s'=7); |
|||
[south] s=10 -> (s'=12); |
|||
[east] s=11 -> (s'=11); |
|||
[west] s=11 -> (s'=11); |
|||
[north] s=11 -> (s'=8); |
|||
[south] s=11 -> (s'=11); |
|||
|
|||
[east] s=12 -> (s'=12); |
|||
[west] s=12 -> (s'=12); |
|||
[north] s=12 -> (s'=10); |
|||
[south] s=12 -> (s'=12); |
|||
|
|||
// loop when we reach the target |
|||
[done] s=13 -> true; |
|||
|
|||
endmodule |
|||
|
|||
// reward structure (number of steps to reach the target) |
|||
rewards |
|||
|
|||
[east] true : 1; |
|||
[west] true : 1; |
|||
[north] true : 1; |
|||
[south] true : 1; |
|||
|
|||
endrewards |
|||
|
|||
// target observation |
|||
label "goal" = s=13; |
|||
|
|||
|
|||
@ -0,0 +1,139 @@ |
|||
|
|||
|
|||
// maze example (POMDP) |
|||
// slightly extends that presented in |
|||
// Littman, Cassandra and Kaelbling |
|||
// Learning policies for partially observable environments: Scaling up |
|||
// Technical Report CS, Brown University |
|||
// gxn 29/01/16 |
|||
|
|||
// state space (value of variable "s") |
|||
|
|||
// 0 1 2 3 4 |
|||
// 5 6 7 |
|||
// 8 9 10 |
|||
// 11 13 12 |
|||
|
|||
// 13 is the target |
|||
|
|||
pomdp |
|||
|
|||
// can observe the walls and target |
|||
observables |
|||
o |
|||
endobservables |
|||
// o=0 - observation in initial state |
|||
// o=1 - west and north walls (s0) |
|||
// o=2 - north and south ways (s1 and s3) |
|||
// o=3 - north wall (s2) |
|||
// o=4 - east and north way (s4) |
|||
// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10) |
|||
// o=6 - east, west and south walls (s11 and s12) |
|||
// o=7 - the target (s13) |
|||
|
|||
module maze |
|||
|
|||
s : [-1..13]; |
|||
o : [0..7]; |
|||
|
|||
// initialisation |
|||
[] s=-1 -> 1/13 : (s'=0) & (o'=1) |
|||
+ 1/13 : (s'=1) & (o'=2) |
|||
+ 1/13 : (s'=2) & (o'=3) |
|||
+ 1/13 : (s'=3) & (o'=2) |
|||
+ 1/13 : (s'=4) & (o'=4) |
|||
+ 1/13 : (s'=5) & (o'=5) |
|||
+ 1/13 : (s'=6) & (o'=5) |
|||
+ 1/13 : (s'=7) & (o'=5) |
|||
+ 1/13 : (s'=8) & (o'=5) |
|||
+ 1/13 : (s'=9) & (o'=5) |
|||
+ 1/13 : (s'=10) & (o'=5) |
|||
+ 1/13 : (s'=11) & (o'=6) |
|||
+ 1/13 : (s'=12) & (o'=6); |
|||
|
|||
// moving around the maze |
|||
|
|||
[east] s=0 -> (s'=1) & (o'=2); |
|||
[west] s=0 -> (s'=0); |
|||
[north] s=0 -> (s'=0); |
|||
[south] s=0 -> (s'=5) & (o'=5); |
|||
|
|||
[east] s=1 -> (s'=2) & (o'=3); |
|||
[west] s=1 -> (s'=0) & (o'=1); |
|||
[north] s=1 -> (s'=1); |
|||
[south] s=1 -> (s'=1); |
|||
|
|||
[east] s=2 -> (s'=3) & (o'=2); |
|||
[west] s=2 -> (s'=1) & (o'=2); |
|||
[north] s=2 -> (s'=2); |
|||
[south] s=2 -> (s'=6) & (o'=5); |
|||
|
|||
[east] s=3 -> (s'=4) & (o'=4); |
|||
[west] s=3 -> (s'=2) & (o'=2); |
|||
[north] s=3 -> (s'=3); |
|||
[south] s=3 -> (s'=3); |
|||
|
|||
[east] s=4 -> (s'=4); |
|||
[west] s=4 -> (s'=3) & (o'=2); |
|||
[north] s=4 -> (s'=4); |
|||
[south] s=4 -> (s'=7) & (o'=5); |
|||
|
|||
[east] s=5 -> (s'=5); |
|||
[west] s=5 -> (s'=5); |
|||
[north] s=5 -> (s'=0) & (o'=1); |
|||
[south] s=5 -> (s'=8); |
|||
|
|||
[east] s=6 -> (s'=6); |
|||
[west] s=6 -> (s'=6); |
|||
[north] s=6 -> (s'=2) & (o'=3); |
|||
[south] s=6 -> (s'=9); |
|||
|
|||
[east] s=7 -> (s'=7); |
|||
[west] s=7 -> (s'=7); |
|||
[north] s=7 -> (s'=4) & (o'=4); |
|||
[south] s=7 -> (s'=10); |
|||
|
|||
[east] s=8 -> (s'=8); |
|||
[west] s=8 -> (s'=8); |
|||
[north] s=8 -> (s'=5); |
|||
[south] s=8 -> (s'=11) & (o'=6); |
|||
|
|||
[east] s=9 -> (s'=9); |
|||
[west] s=9 -> (s'=9); |
|||
[north] s=9 -> (s'=6); |
|||
[south] s=9 -> (s'=13) & (o'=7); |
|||
|
|||
[east] s=10 -> (s'=9); |
|||
[west] s=10 -> (s'=9); |
|||
[north] s=10 -> (s'=7); |
|||
[south] s=10 -> (s'=12) & (o'=6); |
|||
|
|||
[east] s=11 -> (s'=11); |
|||
[west] s=11 -> (s'=11); |
|||
[north] s=11 -> (s'=8) & (o'=5); |
|||
[south] s=11 -> (s'=11); |
|||
|
|||
[east] s=12 -> (s'=12); |
|||
[west] s=12 -> (s'=12); |
|||
[north] s=12 -> (s'=10) & (o'=5); |
|||
[south] s=12 -> (s'=12); |
|||
|
|||
// loop when we reach the target |
|||
[done] s=13 -> true; |
|||
|
|||
endmodule |
|||
|
|||
// reward structure (number of steps to reach the target) |
|||
rewards |
|||
|
|||
[east] true : 1; |
|||
[west] true : 1; |
|||
[north] true : 1; |
|||
[south] true : 1; |
|||
|
|||
endrewards |
|||
|
|||
// target observation |
|||
label "goal" = o=7; |
|||
|
|||
|
|||
@ -0,0 +1,63 @@ |
|||
#include <algorithm>
|
|||
|
|||
#include "counterexample.h"
|
|||
#include "storm/environment/Environment.h"
|
|||
#include "storm-counterexamples/api/counterexamples.h"
|
|||
|
|||
|
|||
using namespace storm::counterexamples; |
|||
|
|||
// Define python bindings
|
|||
void define_counterexamples(py::module& m) { |
|||
|
|||
|
|||
py::class_<boost::container::flat_set<uint_fast64_t>>(m, "FlatSet", "Container to pass to program") |
|||
.def(py::init<>()) |
|||
.def(py::init<boost::container::flat_set<uint64_t>>(), "other"_a) |
|||
.def("insert", [](boost::container::flat_set<uint_fast64_t>& flatset, uint64_t value) {flatset.insert(value);}) |
|||
.def("is_subset_of", [](boost::container::flat_set<uint64_t> const& left, boost::container::flat_set<uint64_t> const& right) {return std::includes(right.begin(), right.end(), left.begin(), left.end()); }) |
|||
.def("insert_set", [](boost::container::flat_set<uint64_t>& left, boost::container::flat_set<uint64_t> const& additional) { for(auto const& i : additional) {left.insert(i);}}) |
|||
.def("__str__", [](boost::container::flat_set<uint64_t> const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); }) |
|||
.def("__len__", [](boost::container::flat_set<uint64_t> const& set) { return set.size();}) |
|||
.def("__iter__", [](boost::container::flat_set<uint_fast64_t> &v) { |
|||
return py::make_iterator(v.begin(), v.end()); |
|||
}, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ |
|||
; |
|||
|
|||
using CexGeneratorStats = SMTMinimalLabelSetGenerator<double>::GeneratorStats; |
|||
|
|||
py::class_<CexGeneratorStats>(m, "SMTCounterExampleGeneratorStats", "Stats for highlevel counterexample generation") |
|||
.def(py::init<>()) |
|||
.def_readonly("analysis_time", &CexGeneratorStats::analysisTime) |
|||
.def_readonly("setup_time", &CexGeneratorStats::setupTime) |
|||
.def_readonly("model_checking_time", &CexGeneratorStats::modelCheckingTime) |
|||
.def_readonly("solver_time", &CexGeneratorStats::solverTime) |
|||
.def_readonly("cut_time", &CexGeneratorStats::cutTime) |
|||
.def_readonly("iterations", &CexGeneratorStats::iterations); |
|||
|
|||
using CexGeneratorOptions = SMTMinimalLabelSetGenerator<double>::Options; |
|||
py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation") |
|||
.def(py::init<>()) |
|||
.def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible) |
|||
.def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability) |
|||
.def_readwrite("silent", &CexGeneratorOptions::silent) |
|||
.def_readwrite("add_backward_implication_cuts", &CexGeneratorOptions::addBackwardImplicationCuts) |
|||
.def_readwrite("use_dynamic_constraints", &CexGeneratorOptions::useDynamicConstraints) |
|||
.def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples) |
|||
.def_readwrite("continue_after_first_counterexample", &CexGeneratorOptions::continueAfterFirstCounterexampleUntil) |
|||
.def_readwrite("maximum_iterations_after_counterexample", &CexGeneratorOptions::maximumExtraIterations) |
|||
; |
|||
py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend"). |
|||
def_static("precompute", &SMTMinimalLabelSetGenerator<double>::precompute, "Precompute input for counterexample generation", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula")). |
|||
def_static("build", &SMTMinimalLabelSetGenerator<double>::computeCounterexampleLabelSet, "Compute counterexample", py::arg("env"), py::arg("stats"), py::arg("symbolic_model"), py::arg("model"), py::arg("cex_input"), py::arg("dontcare"), py::arg("options")) |
|||
|
|||
|
|||
; |
|||
|
|||
using CexInput = SMTMinimalLabelSetGenerator<double>::CexInput; |
|||
py::class_<CexInput>(m, "SMTCounterExampleInput", "Precomputed input for counterexample generation") |
|||
.def("add_reward_and_threshold", &CexInput::addRewardThresholdCombination, "add another reward structure and threshold", py::arg("reward_name"), py::arg("threshold")); |
|||
|
|||
|
|||
|
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_counterexamples(py::module& m); |
|||
@ -1,10 +1,52 @@ |
|||
#include "environment.h"
|
|||
#include "src/helpers.h"
|
|||
#include "storm/environment/Environment.h"
|
|||
#include "storm/environment/solver/SolverEnvironment.h"
|
|||
#include "storm/environment/solver/EigenSolverEnvironment.h"
|
|||
#include "storm/environment/solver/GmmxxSolverEnvironment.h"
|
|||
#include "storm/environment/solver/GameSolverEnvironment.h"
|
|||
#include "storm/environment/solver/NativeSolverEnvironment.h"
|
|||
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
|
|||
#include "storm/environment/solver/MultiplierEnvironment.h"
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
|
|||
void define_environment(py::module& m) { |
|||
py::enum_<storm::solver::EquationSolverType>(m, "EquationSolverType", "Solver type for equation systems") |
|||
.value("native", storm::solver::EquationSolverType::Native) |
|||
.value("eigen", storm::solver::EquationSolverType::Eigen) |
|||
.value("elimination", storm::solver::EquationSolverType::Elimination) |
|||
.value("gmmxx", storm::solver::EquationSolverType::Gmmxx) |
|||
.value("topological", storm::solver::EquationSolverType::Topological) |
|||
; |
|||
|
|||
py::enum_<storm::solver::MinMaxMethod>(m, "MinMaxMethod", "Method for min-max equation systems") |
|||
.value("policy_iteration", storm::solver::MinMaxMethod::PolicyIteration) |
|||
.value("value_iteration", storm::solver::MinMaxMethod::ValueIteration) |
|||
.value("linear_programming", storm::solver::MinMaxMethod::LinearProgramming) |
|||
.value("topological", storm::solver::MinMaxMethod::Topological) |
|||
.value("rational_search", storm::solver::MinMaxMethod::RationalSearch) |
|||
.value("interval_iteration", storm::solver::MinMaxMethod::IntervalIteration) |
|||
.value("sound_value_iteration", storm::solver::MinMaxMethod::SoundValueIteration) |
|||
.value("topological_cuda", storm::solver::MinMaxMethod::TopologicalCuda) |
|||
; |
|||
|
|||
|
|||
py::class_<storm::Environment>(m, "Environment", "Environment") |
|||
.def(py::init<>(), "Construct default environment") |
|||
.def_property_readonly("solver_environment", [](storm::Environment& env) -> auto& {return env.solver();}, "solver part of environment") |
|||
; |
|||
|
|||
py::class_<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers") |
|||
.def("set_force_sound", &storm::SolverEnvironment::setForceSoundness, "force soundness", py::arg("new_value") = true) |
|||
.def("set_linear_equation_solver_type", &storm::SolverEnvironment::setLinearEquationSolverType, "set solver type to use", py::arg("new_value"), py::arg("set_from_default") = false) |
|||
.def_property_readonly("minmax_solver_environment", [](storm::SolverEnvironment& senv) -> auto& { return senv.minMax(); }) |
|||
; |
|||
|
|||
py::class_<storm::MinMaxSolverEnvironment>(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers") |
|||
.def_property("method", &storm::MinMaxSolverEnvironment::getMethod, [](storm::MinMaxSolverEnvironment& mmenv, storm::solver::MinMaxMethod const& m) { mmenv.setMethod(m, false); } ) |
|||
.def_property("precision", &storm::MinMaxSolverEnvironment::getPrecision, &storm::MinMaxSolverEnvironment::setPrecision); |
|||
|
|||
|
|||
|
|||
} |
|||
|
|||
@ -0,0 +1,43 @@ |
|||
#include "transformation.h"
|
|||
#include "storm/api/transformation.h"
|
|||
#include "storm/models/symbolic/StandardRewardModel.h"
|
|||
#include "storm/transformer/SubsystemBuilder.h"
|
|||
|
|||
// Thin wrappers.
|
|||
template<typename VT> |
|||
storm::transformer::SubsystemBuilderReturnType<VT> constructSubsystem(storm::models::sparse::Model<VT> const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates, storm::transformer::SubsystemBuilderOptions options) { |
|||
return storm::transformer::buildSubsystem(originalModel, subsystemStates, subsystemActions, keepUnreachableStates, options); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { |
|||
return storm::api::transformContinuousToDiscreteTimeSparseModel(model, formulas); |
|||
} |
|||
|
|||
void define_transformation(py::module& m) { |
|||
// Transform model
|
|||
m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, double>, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); |
|||
m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); |
|||
|
|||
m.def("_transform_to_discrete_time_model", &transformContinuousToDiscreteTimeSparseModel<double>, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); |
|||
m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel<storm::RationalFunction>, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); |
|||
|
|||
py::class_<storm::transformer::SubsystemBuilderReturnType<double>>(m, "SubsystemBuilderReturnTypeDouble", "Result of the construction of a subsystem") |
|||
.def_readonly("model", &storm::transformer::SubsystemBuilderReturnType<double>::model, "the submodel") |
|||
.def_readonly("new_to_old_state_mapping", &storm::transformer::SubsystemBuilderReturnType<double>::newToOldStateIndexMapping, "for each state in result, the state index in the original model") |
|||
.def_readonly("new_to_old_action_mapping", &storm::transformer::SubsystemBuilderReturnType<double>::newToOldActionIndexMapping, "for each action in result, the action index in the original model") |
|||
.def_readonly("kept_actions", &storm::transformer::SubsystemBuilderReturnType<double>::keptActions, "Actions of the subsystem available in the original system") |
|||
; |
|||
|
|||
py::class_<storm::transformer::SubsystemBuilderOptions>(m, "SubsystemBuilderOptions", "Options for constructing the subsystem") |
|||
.def(py::init<>()) |
|||
.def_readwrite("check_transitions_outside", &storm::transformer::SubsystemBuilderOptions::checkTransitionsOutside) |
|||
.def_readwrite("build_state_mapping", &storm::transformer::SubsystemBuilderOptions::buildStateMapping) |
|||
.def_readwrite("build_action_mapping", &storm::transformer::SubsystemBuilderOptions::buildActionMapping) |
|||
.def_readwrite("build_kept_actions", &storm::transformer::SubsystemBuilderOptions::buildKeptActions) |
|||
; |
|||
|
|||
|
|||
m.def("_construct_subsystem_double", &constructSubsystem<double>, "build a subsystem of a sparse model"); |
|||
|
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_transformation(py::module& m); |
|||
@ -0,0 +1,27 @@ |
|||
#include "analysis.h"
|
|||
|
|||
#include "storm-dft/parser/DFTJsonParser.h"
|
|||
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
|
|||
#include "storm-dft/storage/dft/DFTIsomorphism.h"
|
|||
|
|||
|
|||
// Thin wrapper for DFT analysis
|
|||
template<typename ValueType> |
|||
//std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH) {
|
|||
std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevant) { |
|||
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false); |
|||
|
|||
std::vector<ValueType> results; |
|||
for (auto result : dftResults) { |
|||
results.push_back(boost::get<ValueType>(result)); |
|||
} |
|||
return results; |
|||
} |
|||
|
|||
|
|||
// Define python bindings
|
|||
void define_analysis(py::module& m) { |
|||
|
|||
m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=std::set<size_t>(), py::arg("dc_for_relevant")=true); |
|||
|
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_analysis(py::module& m); |
|||
@ -1 +1,2 @@ |
|||
#include "src/common.h" |
|||
#include "storm-dft/api/storm-dft.h" |
|||
@ -1,34 +1,35 @@ |
|||
#include "dft.h"
|
|||
#include "storm-dft/parser/DFTJsonParser.h"
|
|||
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
|
|||
#include "src/helpers.h"
|
|||
#include "storm-dft/storage/dft/DFT.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm-dft/settings/modules/FaultTreeSettings.h"
|
|||
#include "storm-dft/storage/dft/DFTIsomorphism.h"
|
|||
|
|||
// Thin wrapper for model building using one formula as argument
|
|||
template<typename ValueType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModelFromJsonDft(std::string const& jsonDft, bool symred) { |
|||
// Build DFT
|
|||
storm::parser::DFTJsonParser<ValueType> parser; |
|||
storm::storage::DFT<ValueType> dft = parser.parseJson(jsonDft); |
|||
// Build model
|
|||
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry; |
|||
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); |
|||
if (symred) { |
|||
auto colouring = dft.colourDFT(); |
|||
symmetries = dft.findSymmetries(colouring); |
|||
} |
|||
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, true); |
|||
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions({}, true); |
|||
builder.buildModel(labeloptions, 0, 0.0); |
|||
return builder.getModel(); |
|||
} |
|||
|
|||
|
|||
template<typename ValueType> using DFT = storm::storage::DFT<ValueType>; |
|||
|
|||
|
|||
void define_dft(py::module& m) { |
|||
|
|||
m.def("_set_up", []() { |
|||
storm::settings::addModule<storm::settings::modules::FaultTreeSettings>(); |
|||
}, "Initialize Storm-dft"); |
|||
// Build model
|
|||
m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft<double>, "Build the model", py::arg("jsonDft"), py::arg("symred") = false); |
|||
m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft<storm::RationalFunction>, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false); |
|||
|
|||
|
|||
// DFT class
|
|||
py::class_<DFT<double>, std::shared_ptr<DFT<double>>>(m, "DFT", "DFT") |
|||
.def("nr_elements", &DFT<double>::nrElements, "Total number of elements") |
|||
.def("nr_be", &DFT<double>::nrBasicElements, "Number of basic elements") |
|||
.def("nr_dynamic", &DFT<double>::nrDynamicElements, "Number of dynamic elements") |
|||
.def("can_have_nondeterminism", &DFT<double>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices") |
|||
.def("__str__", &DFT<double>::getInfoString) |
|||
; |
|||
|
|||
py::class_<DFT<storm::RationalFunction>, std::shared_ptr<DFT<storm::RationalFunction>>>(m, "ParametricDFT", "Parametric DFT") |
|||
.def("nr_elements", &DFT<storm::RationalFunction>::nrElements, "Total number of elements") |
|||
.def("nr_be", &DFT<storm::RationalFunction>::nrBasicElements, "Number of basic elements") |
|||
.def("nr_dynamic", &DFT<storm::RationalFunction>::nrDynamicElements, "Number of dynamic elements") |
|||
.def("can_have_nondeterminism", &DFT<storm::RationalFunction>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices") |
|||
.def("__str__", &DFT<storm::RationalFunction>::getInfoString) |
|||
; |
|||
|
|||
} |
|||
@ -1,8 +1,5 @@ |
|||
#ifndef PYTHON_DFT_DFT_H_ |
|||
#define PYTHON_DFT_DFT_H_ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_dft(py::module& m); |
|||
|
|||
#endif /* PYTHON_DFT_DFT_H_ */ |
|||
@ -0,0 +1,20 @@ |
|||
#include "io.h"
|
|||
#include "src/helpers.h"
|
|||
|
|||
|
|||
// Define python bindings
|
|||
void define_input(py::module& m) { |
|||
|
|||
// Load DFT input
|
|||
m.def("load_dft_galileo_file", &storm::api::loadDFTGalileoFile<double>, "Load DFT from Galileo file", py::arg("path")); |
|||
// Parse Jani model
|
|||
m.def("load_dft_json_file", &storm::api::loadDFTJsonFile<double>, "Load DFT from JSON file", py::arg("path")); |
|||
m.def("load_dft_json_string", &storm::api::loadDFTJsonString<double>, "Load DFT from JSON string", py::arg("json_string")); |
|||
} |
|||
|
|||
void define_output(py::module& m) { |
|||
|
|||
// Export DFT
|
|||
m.def("export_dft_json_file", &storm::api::exportDFTToJsonFile<double>, "Export DFT to JSON file", py::arg("dft"), py::arg("path")); |
|||
m.def("export_dft_json_string", &storm::api::exportDFTToJsonString<double>, "Export DFT to JSON string", py::arg("dft")); |
|||
} |
|||
@ -0,0 +1,6 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_input(py::module& m); |
|||
void define_output(py::module& m); |
|||
@ -1,9 +1,14 @@ |
|||
#include "common.h"
|
|||
|
|||
#include "utility/shortestPaths.h"
|
|||
#include "utility/smtsolver.h"
|
|||
#include "utility/chrono.h"
|
|||
|
|||
|
|||
PYBIND11_MODULE(utility, m) { |
|||
m.doc() = "Utilities for Storm"; |
|||
|
|||
define_ksp(m); |
|||
define_smt(m); |
|||
define_chrono(m); |
|||
} |
|||
@ -1,3 +1,6 @@ |
|||
#include "src/common.h" |
|||
|
|||
#include "storm-pars/api/storm-pars.h" |
|||
|
|||
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" |
|||
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" |
|||
@ -0,0 +1,15 @@ |
|||
#include "choiceorigins.h"
|
|||
#include "storm/storage/sparse/JaniChoiceOrigins.h"
|
|||
#include "storm/storage/jani/Model.h"
|
|||
|
|||
void define_origins(py::module& m) { |
|||
using ChoiceOrigins = storm::storage::sparse::ChoiceOrigins; |
|||
py::class_<ChoiceOrigins, std::shared_ptr<ChoiceOrigins>> co(m, "ChoiceOrigins", "This class represents the origin of choices of a model in terms of the input model spec."); |
|||
co.def("get_identifier_info", &ChoiceOrigins::getIdentifierInfo, "identifier"_a, "human readable string") |
|||
.def("get_choice_info", &ChoiceOrigins::getChoiceInfo, "identifier"_a, "human readable string") ; |
|||
using JaniChoiceOrigins = storm::storage::sparse::JaniChoiceOrigins; |
|||
py::class_<JaniChoiceOrigins, std::shared_ptr<JaniChoiceOrigins>>(m, "JaniChoiceOrigins", "This class represents for each choice the origin in the jani spec.", co) |
|||
.def_property_readonly("model", &JaniChoiceOrigins::getModel, "retrieves the associated JANI model") |
|||
.def("get_edge_index_set", [](JaniChoiceOrigins const& co, uint64_t choice) -> auto& { return co.getEdgeIndexSet(choice); }, "returns the set of edges that induced the choice", py::arg("choice_index")) |
|||
; |
|||
} |
|||
@ -0,0 +1,6 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
|
|||
void define_origins(py::module& m); |
|||
@ -0,0 +1,162 @@ |
|||
#include "jani.h"
|
|||
#include <storm/storage/jani/Model.h>
|
|||
#include <storm/storage/jani/JSONExporter.h>
|
|||
#include <storm/storage/expressions/ExpressionManager.h>
|
|||
#include <storm/logic/RewardAccumulationEliminationVisitor.h>
|
|||
#include "src/helpers.h"
|
|||
|
|||
using namespace storm::jani; |
|||
|
|||
std::string janiToString(Model const& m) { |
|||
std::stringstream str; |
|||
JsonExporter::toStream(m, {}, str); |
|||
return str.str(); |
|||
} |
|||
|
|||
void define_jani(py::module& m) { |
|||
|
|||
py::class_<Model, std::shared_ptr<Model>> md(m, "JaniModel", "A Jani Model"); |
|||
md.def(py::init<Model>(), "other_model"_a) |
|||
.def_property_readonly("name", &Model::getName, "model name") |
|||
.def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") |
|||
.def("set_model_type", &Model::setModelType, "Sets (only) the model type") |
|||
.def_property_readonly("automata", [](const Model& model) -> auto& {return model.getAutomata();}, "get automata") |
|||
.def_property_readonly("global_variables", [](const Model& model) -> auto& {return model.getGlobalVariables();}) |
|||
.def_property_readonly("constants", [](const Model& model) -> auto& {return model.getConstants();}, "get constants") |
|||
.def("get_constant", &Model::getConstant, "name"_a, "get constant by name") |
|||
.def("restrict_edges", &Model::restrictEdges, "restrict model to edges given by set", py::arg("edge_set")) |
|||
.def_property_readonly("expression_manager", &Model::getExpressionManager, "get expression manager", pybind11::return_value_policy::reference_internal) |
|||
.def_property_readonly("has_undefined_constants", &Model::hasUndefinedConstants, "Flag if program has undefined constants") |
|||
.def_property_readonly("undefined_constants_are_graph_preserving", &Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") |
|||
.def("__str__", &janiToString) |
|||
.def_property("initial_states_restriction", &Model::getInitialStatesRestriction, &Model::setInitialStatesRestriction, "initial states restriction") |
|||
.def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map")) |
|||
.def("substitute_constants", &Model::substituteConstants, "substitute constants") |
|||
.def("remove_constant", &Model::removeConstant, "remove a constant. Make sure the constant does not appear in the model.", "constant_name"_a) |
|||
.def("get_automaton_index", &Model::getAutomatonIndex, "name"_a, "get index for automaton name") |
|||
.def("add_automaton", &Model::addAutomaton, "automaton"_a, "add an automaton (with a unique name)") |
|||
.def("set_standard_system_composition", &Model::setStandardSystemComposition, "sets the composition to the standard composition") |
|||
.def("replace_automaton", &Model::replaceAutomaton, "index"_a, "new_automaton"_a, "replace automaton at index") |
|||
.def("check_valid", &Model::checkValid, "Some basic checks to ensure validity") |
|||
.def("substitute_functions", [](Model& model) {model.substituteFunctions();}, "substitute functions") |
|||
.def_static("encode_automaton_and_edge_index", &Model::encodeAutomatonAndEdgeIndices, "get edge/automaton-index") |
|||
.def_static("decode_automaton_and_edge_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index") |
|||
.def("make_standard_compliant", &Model::makeStandardJaniCompliant, "make standard JANI compliant") |
|||
.def("has_standard_composition", &Model::hasStandardComposition, "is the composition the standard composition") |
|||
.def("finalize", &Model::finalize,"finalizes the model. After this action, be careful changing the data structure.") |
|||
.def("to_dot", [](Model& model) {std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }) |
|||
; |
|||
|
|||
py::class_<Automaton, std::shared_ptr<Automaton>> automaton(m, "JaniAutomaton", "A Jani Automation"); |
|||
automaton.def(py::init<std::string, storm::expressions::Variable>()) |
|||
.def_property_readonly("edges",[](const Automaton& a) -> auto& { |
|||
return a.getEdges(); |
|||
}, "get edges") |
|||
.def_property_readonly("name", &Automaton::getName) |
|||
.def_property_readonly("location_variable", &Automaton::getLocationExpressionVariable) |
|||
.def_property_readonly("variables", [](Automaton& aut) -> VariableSet& {return aut.getVariables();}, py::return_value_policy::reference_internal) |
|||
.def_property_readonly("locations", [](Automaton& aut) -> auto& {return aut.getLocations();}) |
|||
.def("add_location", &Automaton::addLocation, "location"_a, "adds a new location, returns the index") |
|||
.def("add_initial_location", [](Automaton& aut, uint64_t index) { aut.addInitialLocation(index); }, "index"_a) |
|||
.def_property_readonly("initial_location_indices", &Automaton::getInitialLocationIndices) |
|||
.def_property("initial_states_restriction", [](Automaton& aut) { aut.getInitialStatesExpression(); }, &Automaton::setInitialStatesRestriction, "initial state restriction") |
|||
.def("add_edge", &Automaton::addEdge, "edge"_a) |
|||
|
|||
; |
|||
|
|||
py::class_<Edge, std::shared_ptr<Edge>> edge(m, "JaniEdge", "A Jani Edge"); |
|||
edge.def(py::init<uint64_t, uint64_t, boost::optional<storm::expressions::Expression>, std::shared_ptr<TemplateEdge>, std::vector<std::pair<uint64_t, storm::expressions::Expression>>>(), |
|||
"source_location_index"_a, "action_index"_a, "rate"_a, "template_edge"_a, "destinations_with_probabilities"_a) |
|||
.def_property_readonly("source_location_index", &Edge::getSourceLocationIndex, "index for source location") |
|||
.def_property_readonly("destinations", [](Edge const& e) -> auto& { |
|||
return e.getDestinations(); |
|||
}, "edge destinations") |
|||
.def_property_readonly("action_index", &Edge::getActionIndex, "action index") |
|||
.def_property_readonly("template_edge", &Edge::getTemplateEdge, "template edge") |
|||
.def_property_readonly("rate", &Edge::getOptionalRate, "edge rate") |
|||
.def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations") |
|||
.def_property_readonly("guard", &Edge::getGuard, "edge guard") |
|||
.def_property("color", &Edge::getColor, &Edge::setColor, "color for the edge") |
|||
.def("substitute", &Edge::substitute, py::arg("mapping")) |
|||
.def("has_silent_action", &Edge::hasSilentAction, "Is the edge labelled with the silent action") |
|||
; |
|||
|
|||
py::class_<TemplateEdge, std::shared_ptr<TemplateEdge>> templateEdge(m, "JaniTemplateEdge", "Template edge, internal data structure for edges"); |
|||
templateEdge.def(py::init<storm::expressions::Expression>()) |
|||
.def_property_readonly("assignments", [](TemplateEdge& te) -> auto& { return te.getAssignments(); }) |
|||
.def_property("guard", &TemplateEdge::getGuard, &TemplateEdge::setGuard) |
|||
.def_property_readonly("destinations",[](TemplateEdge& te) -> auto& { return te.getDestinations(); }) |
|||
.def("add_destination", &TemplateEdge::addDestination) |
|||
; |
|||
|
|||
py::class_<EdgeDestination, std::shared_ptr<EdgeDestination>> edgeDestination(m, "JaniEdgeDestination", "Destination in Jani"); |
|||
edgeDestination.def_property_readonly("target_location_index", &EdgeDestination::getLocationIndex) |
|||
.def_property_readonly("probability", &EdgeDestination::getProbability) |
|||
.def_property_readonly("assignments", &EdgeDestination::getOrderedAssignments) |
|||
; |
|||
|
|||
py::class_<TemplateEdgeDestination, std::shared_ptr<TemplateEdgeDestination>> templateEdgeDestination(m, "JaniTemplateEdgeDestination", "Template edge destination, internal data structure for edge destinations"); |
|||
templateEdgeDestination.def(py::init<OrderedAssignments>(), "ordered_assignments"_a) |
|||
.def_property_readonly("assignments", [](TemplateEdgeDestination& ted) -> auto& {return ted.getOrderedAssignments();}); |
|||
|
|||
py::class_<OrderedAssignments, std::shared_ptr<OrderedAssignments>> orderedAssignments(m, "JaniOrderedAssignments", "Set of assignments"); |
|||
orderedAssignments.def("__iter__", [](OrderedAssignments &v) { |
|||
return py::make_iterator(v.begin(), v.end()); |
|||
}, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ |
|||
.def("__str__", &streamToString<OrderedAssignments>) |
|||
.def("clone", &OrderedAssignments::clone, "clone assignments (performs a deep copy)") |
|||
.def("substitute", &OrderedAssignments::substitute, "substitute in rhs according to given substitution map", "substitution_map"_a) |
|||
.def("add", [](OrderedAssignments& oa, Assignment const& newAssignment, bool addToExisting) {return oa.add(newAssignment, addToExisting); }, "new_assignment"_a, "add_to_existing"_a = false) |
|||
; |
|||
|
|||
py::class_<Assignment, std::shared_ptr<Assignment>> assignment(m, "JaniAssignment", "Jani Assignment"); |
|||
assignment.def(py::init<Variable const&,storm::expressions::Expression const&,int64_t>(), "lhs"_a, "rhs"_a, "lvl"_a = 0) |
|||
.def("__str__", &streamToString<Assignment>) |
|||
.def_property("expression", &Assignment::getAssignedExpression, &Assignment::setAssignedExpression) |
|||
; |
|||
|
|||
py::class_<Location, std::shared_ptr<Location>> location(m, "JaniLocation", "A Location in JANI"); |
|||
location.def_property_readonly("name", &Location::getName, "name of the location") |
|||
.def_property_readonly("assignments", [](Location& loc) {loc.getAssignments();}, "location assignments") |
|||
; |
|||
|
|||
py::class_<VariableSet, std::shared_ptr<VariableSet>> variableSet(m, "JaniVariableSet", "Jani Set of Variables"); |
|||
variableSet.def(py::init<>()) |
|||
.def("__iter__", [](VariableSet &v) { |
|||
return py::make_iterator(v.begin(), v.end()); |
|||
}, py::keep_alive<0, 1>()) |
|||
.def("add_variable", [](VariableSet& vs, Variable& v) -> void { vs.addVariable(v); }) |
|||
.def("add_bounded_integer_variable", [](VariableSet& vs, BoundedIntegerVariable& v) -> auto& { return vs.addVariable(v); /*return vs.getVariable(v.getExpressionVariable());*/ }, py::return_value_policy::reference_internal, "variable"_a) |
|||
.def("empty", &VariableSet::empty, "is there a variable in the set?") |
|||
.def("get_variable_by_name", [](VariableSet& v, std::string const& name) -> auto& { return v.getVariable(name);}) |
|||
.def("get_variable_by_expr_variable", [](VariableSet& v, storm::expressions::Variable const& var) -> auto& { return v.getVariable(var);}) |
|||
; |
|||
|
|||
py::class_<Variable, std::shared_ptr<Variable>> variable(m, "JaniVariable", "A Variable in JANI"); |
|||
variable.def_property_readonly("name", &Variable::getName, "name of constant") |
|||
.def_property_readonly("expression_variable", &Variable::getExpressionVariable, "expression variable for this variable") |
|||
; |
|||
|
|||
py::class_<BoundedIntegerVariable, std::shared_ptr<BoundedIntegerVariable>> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable); |
|||
bivariable.def(py::init<std::string, storm::expressions::Variable, storm::expressions::Expression, storm::expressions::Expression, storm::expressions::Expression>(), |
|||
"name"_a, "expression_variable"_a, "init_value"_a, "lower_bound"_a, "upper_bound"_a) |
|||
.def(py::init<std::string, storm::expressions::Variable, storm::expressions::Expression, storm::expressions::Expression>(), |
|||
"name"_a, "expression_variable"_a, "lower_bound"_a, "upper_bound"_a);; |
|||
|
|||
py::class_<Constant, std::shared_ptr<Constant>> constant(m, "JaniConstant", "A Constant in JANI"); |
|||
constant.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression") |
|||
.def_property_readonly("name", &Constant::getName, "name of constant") |
|||
.def_property_readonly("type", &Constant::getType, "type of constant") |
|||
.def_property_readonly("expression_variable", &Constant::getExpressionVariable, "expression variable for this constant") |
|||
; |
|||
|
|||
|
|||
m.def("eliminate_reward_accumulations", [](const Model& model, std::vector<Property>& properties) { |
|||
storm::logic::RewardAccumulationEliminationVisitor v(model); |
|||
v.eliminateRewardAccumulations(properties); |
|||
return properties; |
|||
}, "Eliminate reward accumulations", py::arg("model"), py::arg("properties")); |
|||
|
|||
|
|||
|
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "common.h" |
|||
|
|||
void define_jani(py::module& m); |
|||
@ -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<storm::dd::DdType DdType> |
|||
void define_symbolic_model(py::module& m, std::string vt_suffix); |
|||
@ -0,0 +1,10 @@ |
|||
#include "chrono.h"
|
|||
#include "src/helpers.h"
|
|||
|
|||
#include <chrono>
|
|||
|
|||
void define_chrono(py::module& m) { |
|||
py::class_<std::chrono::milliseconds>(m, "milliseconds") |
|||
.def("count", &std::chrono::milliseconds::count) |
|||
.def("__str__", [](std::chrono::milliseconds const& t) { std::stringstream strstr; strstr << t.count(); return strstr.str(); }); |
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "src/common.h" |
|||
|
|||
void define_chrono(py::module& m); |
|||
@ -0,0 +1,32 @@ |
|||
#include "smtsolver.h"
|
|||
#include <storm/solver/Z3SmtSolver.h>
|
|||
#include "storm/storage/expressions/ExpressionManager.h"
|
|||
|
|||
void define_smt(py::module& m) { |
|||
using SmtSolver = storm::solver::SmtSolver; |
|||
using Z3SmtSolver = storm::solver::Z3SmtSolver; |
|||
using ModelReference = storm::solver::SmtSolver::ModelReference; |
|||
|
|||
py::enum_<SmtSolver::CheckResult>(m, "SmtCheckResult", "Result type") |
|||
.value("Sat", SmtSolver::CheckResult::Sat) |
|||
.value("Unsat", SmtSolver::CheckResult::Unsat) |
|||
.value("Unknown", SmtSolver::CheckResult::Unknown) |
|||
; |
|||
|
|||
py::class_<ModelReference, std::shared_ptr<ModelReference >> modelref(m, "ModelReference", "Lightweight Wrapper around results"); |
|||
modelref.def("get_boolean_value", &ModelReference::getBooleanValue, "get a value for a boolean variable", py::arg("variable")) |
|||
.def("get_integer_value", &ModelReference::getIntegerValue, "get a value for an integer variable", py::arg("variable")) |
|||
.def("get_rational_value", &ModelReference::getRationalValue, "get a value (as double) for an rational variable", py::arg("variable")); |
|||
|
|||
|
|||
py::class_<SmtSolver> smtsolver(m, "SmtSolver", "Generic Storm SmtSolver Wrapper"); |
|||
smtsolver.def("push", &SmtSolver::push, "push") |
|||
.def("pop", [](SmtSolver& solver, uint64_t n) {solver.pop(n);}, "pop", py::arg("levels")) |
|||
.def("reset", &SmtSolver::reset, "reset") |
|||
.def("add", [](SmtSolver& solver, storm::expressions::Expression const& expr) {solver.add(expr);}, "addconstraint") |
|||
.def("check", &SmtSolver::check, "check") |
|||
.def_property_readonly("model", &SmtSolver::getModel, "get the model"); |
|||
|
|||
py::class_<Z3SmtSolver> z3solver(m, "Z3SmtSolver", "z3 API for storm smtsolver wrapper", smtsolver); |
|||
z3solver.def(pybind11::init<storm::expressions::ExpressionManager&>()); |
|||
} |
|||
@ -0,0 +1,5 @@ |
|||
#pragma once |
|||
|
|||
#include "src/common.h" |
|||
|
|||
void define_smt(py::module& m); |
|||
@ -1 +0,0 @@ |
|||
__pycache__ |
|||
@ -0,0 +1,81 @@ |
|||
import stormpy |
|||
import stormpy.logic |
|||
from helpers.helper import get_example_path |
|||
|
|||
import math |
|||
|
|||
|
|||
class TestTransformation: |
|||
|
|||
def test_transform_symbolic_dtmc_to_sparse(self): |
|||
program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) |
|||
symbolic_model = stormpy.build_symbolic_model(program) |
|||
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.SymbolicSylvanDtmc |
|||
sparse_model = stormpy.transform_to_sparse_model(symbolic_model) |
|||
assert sparse_model.nr_states == 8607 |
|||
assert sparse_model.nr_transitions == 15113 |
|||
assert sparse_model.model_type == stormpy.ModelType.DTMC |
|||
assert not sparse_model.supports_parameters |
|||
assert type(sparse_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 |
|||
|
|||
def test_transform_continuous_to_discrete_time_model_ctmc(self): |
|||
ctmc = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) |
|||
formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") |
|||
assert ctmc.nr_states == 16 |
|||
assert ctmc.nr_transitions == 33 |
|||
assert len(ctmc.initial_states) == 1 |
|||
initial_state = ctmc.initial_states[0] |
|||
assert initial_state == 1 |
|||
result = stormpy.model_checking(ctmc, formulas[0]) |
|||
assert math.isclose(result.at(initial_state), 4.166666667) |
|||
|
|||
dtmc, dtmc_formulas = stormpy.transform_to_discrete_time_model(ctmc, formulas) |
|||
assert dtmc.nr_states == 16 |
|||
assert dtmc.nr_transitions == 33 |
|||
assert len(dtmc.initial_states) == 1 |
|||
initial_state = dtmc.initial_states[0] |
|||
assert initial_state == 1 |
|||
result = stormpy.model_checking(dtmc, dtmc_formulas[0]) |
|||
assert math.isclose(result.at(initial_state), 4.166666667) |
|||
|
|||
def test_transform_continuous_to_discrete_time_model_ma(self): |
|||
program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) |
|||
formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program) |
|||
ma = stormpy.build_model(program, formulas) |
|||
assert ma.nr_states == 5 |
|||
assert ma.nr_transitions == 8 |
|||
assert ma.model_type == stormpy.ModelType.MA |
|||
assert len(ma.initial_states) == 1 |
|||
initial_state = ma.initial_states[0] |
|||
assert initial_state == 0 |
|||
result = stormpy.model_checking(ma, formulas[0]) |
|||
assert math.isclose(result.at(initial_state), 0.08333333333) |
|||
|
|||
mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) |
|||
assert mdp.nr_states == 5 |
|||
assert mdp.nr_transitions == 8 |
|||
assert mdp.model_type == stormpy.ModelType.MDP |
|||
assert len(mdp.initial_states) == 1 |
|||
initial_state = mdp.initial_states[0] |
|||
assert initial_state == 0 |
|||
result = stormpy.model_checking(mdp, mdp_formulas[0]) |
|||
assert math.isclose(result.at(initial_state), 0.08333333333) |
|||
@ -0,0 +1,17 @@ |
|||
import stormpy |
|||
import stormpy.logic |
|||
from helpers.helper import get_example_path |
|||
|
|||
import math |
|||
from configurations import dft |
|||
|
|||
|
|||
@dft |
|||
class TestAnalysis: |
|||
|
|||
def test_analyze_mttf(self): |
|||
dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) |
|||
formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") |
|||
assert dft.nr_elements() == 3 |
|||
results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) |
|||
assert math.isclose(results[0], 3) |
|||
@ -1,20 +0,0 @@ |
|||
import stormpy |
|||
import stormpy.logic |
|||
from helpers.helper import get_example_path |
|||
|
|||
import math |
|||
from configurations import dft |
|||
|
|||
|
|||
@dft |
|||
class TestBuild: |
|||
def test_build_dft(self): |
|||
model = stormpy.dft.build_sparse_model_from_json_dft(get_example_path("dft", "and.json")) |
|||
formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") |
|||
assert model.nr_states == 4 |
|||
assert model.nr_transitions == 5 |
|||
assert len(model.initial_states) == 1 |
|||
initial_state = model.initial_states[0] |
|||
assert initial_state == 1 |
|||
result = stormpy.model_checking(model, formulas[0]) |
|||
assert math.isclose(result.at(initial_state), 3) |
|||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue