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 <http://www.stormchecker.org/>`_. 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):
The bindings themselves have been developed by (lexicographically ordered):
This guide is intended for people which have a basic understanding of probabilistic models and their verification. More details and further pointers to literature can be found on the
This guide is intended for people which have a basic understanding of probabilistic models and their verification. More details and further pointers to literature can be found on the
`storm website <http://www.stormchecker.org/>`_.
`Storm website <http://www.stormchecker.org/>`_.
While we assume some very basic programming concepts, we refrain from using more advanced concepts of python throughout the guide.
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.
We start with a selection of high-level constructs in stormpy, and go into more details afterwards.
One of the easiest is to parse a description of such a Markov chain and to let storm build the chain.
One of the easiest is to parse a description of such a Markov chain and to let Storm build the chain.
Here, we build a Markov chain from a prism program.
Here, we build a Markov chain from a prism program.
Stormpy comes with a small set of examples, which we use here::
Stormpy comes with a small set of examples, which we use here::
@ -74,7 +74,7 @@ Stormpy can be used to parse this. As the variables in the property refer to a p
Notice that properties is now a list of properties containing a single element.
Notice that properties is now a list of properties containing a single element.
However, if we build the model as before, then the appropriate information that the variable s=2 in some states is not present.
However, if we build the model as before, then the appropriate information that the variable s=2 in some states is not present.
In order to label the states accordingly, we should notify storm upon building the model that we would like to preserve given properties.
In order to label the states accordingly, we should notify Storm upon building the model that we would like to preserve given properties.
Storm will then add the labels accordingly::
Storm will then add the labels accordingly::
>>> model = stormpy.build_model(prism_program, properties)
>>> model = stormpy.build_model(prism_program, properties)
@ -91,7 +91,7 @@ If we consider another property, however, such as::
P=? [F s=7 & d=2]
P=? [F s=7 & d=2]
then storm is only skipping exploration of successors of the particular state y where s=7 and d=2. In this model, state y has a self-loop, so effectively, the whole model is explored.
then Storm is only skipping exploration of successors of the particular state y where s=7 and d=2. In this model, state y has a self-loop, so effectively, the whole model is explored.
are both available on your system. To avoid issues, we suggest that both use the same version of `carl <https://smtrat.github.io/carl>`_.
are both available on your system. To avoid issues, we suggest that both use the same version of `carl <https://smtrat.github.io/carl>`_.
The simplest way of ensuring this is to first install carl as explained in the `storm installation guide <http://www.stormchecker.org/documentation/installation/manual-configuration.html#carl>`_.
You can then install storm and pycarl independently.
The simplest way of ensuring this is to first install carl as explained in the `Storm installation guide <http://www.stormchecker.org/documentation/installation/manual-configuration.html#carl>`_.
You can then install Storm and pycarl independently.
..topic:: Virtual Environments
..topic:: Virtual Environments
@ -37,9 +37,9 @@ or::
$ pip install -ve .
$ pip install -ve .
..topic:: Specifying which storm library to use
..topic:: Specifying which Storm library to use
If you have multiple versions of storm or cmake is not able to find your storm version,
If you have multiple versions of Storm or cmake is not able to find your Storm version,
you can specify the `--storm-dir YOUR-PATH-TO-STORM` flag in the build_ext step::
you can specify the `--storm-dir YOUR-PATH-TO-STORM` flag in the build_ext step::
Matthias Volk
7 years ago