Browse Source

extended getting started guide

refactoring
Sebastian Junges 8 years ago
parent
commit
8def8dd30b
  1. 30
      doc/source/getting_started.rst
  2. 2
      doc/source/index.rst
  3. 1
      lib/stormpy/__init__.py
  4. 4
      lib/stormpy/examples/files.py
  5. 5
      lib/stormpy/examples/files/pdtmc/parametric_die.pm

30
doc/source/getting_started.rst

@ -75,12 +75,12 @@ In order to label the states accordingly, we should notify storm upon building t
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)
print("Labels: {}".format(model.labels) # {"init", "deadlock", "s=2"})
print("Labels in the model: {}".format(model.labels) # out: Labels in the model: {"init", "deadlock", "s=2"})
Model building however now behaves slightly different: Only the properties passed are preserved, which means that model building might skip parts of the model. Model building however now behaves slightly different: Only the properties passed are preserved, which means that model building might skip parts of the model.
In particular, to check the probability of eventually reaching a state x where s=2, successor states of x are not relevant:: In particular, to check the probability of eventually reaching a state x where s=2, successor states of x are not relevant::
print("Number of states: {}".format(model.nr_states)) # out: 8
print("Number of states: {}".format(model.nr_states)) # out: Number of states: 8
If we consider another property, however, such as:: If we consider another property, however, such as::
@ -104,18 +104,39 @@ The result may contain information about all states. Merely printing does not gi
print(result) # out: [0,1] range print(result) # out: [0,1] range
Instead, we can iterate over the results:
Instead, we can iterate over the results::
assert result.result_for_all_states
for x in result.get_values():
print(x)
.. topic:: Results for all states
Some model checking algorithms do not provide results for all states. In those cases, the result is not valid for all states, and to iterate over them, a different method is required. We will explain this later.
Instantiating parametric models Instantiating parametric models
------------------------------------ ------------------------------------
.. seealso:: ``04-getting-started.py`` .. 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)
In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator::
instantiator = ModelInstantiator(model)
Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows::
point = dict()
parameters = model.collect_probability_parameters()
for x in parameters:
print(x.name)
point[x] = 0.4
instantiated_model = instantiator.instantiate(point)
result = stormpy.model_checking(instantiated_model, properties[0])
Checking parametric models Checking parametric models
@ -129,6 +150,7 @@ Checking parametric models
Investigating the model Investigating the model
------------------------------------- -------------------------------------
.. seealso:: ``06-getting-started.py``

2
doc/source/index.rst

@ -15,6 +15,8 @@ Stormpy Documentation
installation installation
getting_started getting_started
contributors
Stormpy API Reference Stormpy API Reference
==================================== ====================================

1
lib/stormpy/__init__.py

@ -3,6 +3,7 @@ from .core import *
from . import storage from . import storage
from .storage import * from .storage import *
from .version import __version__ from .version import __version__
import stormpy.logic
core._set_up("") core._set_up("")

4
lib/stormpy/examples/files.py

@ -9,5 +9,7 @@ def _path(folder, file):
prism_dtmc_die = _path("dtmc", "die.pm") prism_dtmc_die = _path("dtmc", "die.pm")
"""Knuth Yao Die Example""" """Knuth Yao Die Example"""
prism_pdtmc_die = _path("pdtmc", "parametric_die.pm")
"""Knuth Yao Die -- 2 unfair coins Example"""
prism_dtmc_brp = _path("dtmc", "brp-16-2.pm") prism_dtmc_brp = _path("dtmc", "brp-16-2.pm")
"""Bounded Retransmission Protocol"""
"""Bounded Retransmission Protocol"""

5
lib/stormpy/examples/files/pdtmc/parametric_die.pm

@ -2,6 +2,7 @@
dtmc dtmc
const double p; const double p;
const double q;
module die module die
@ -11,8 +12,8 @@ module die
d : [0..6] init 0; d : [0..6] init 0;
[] s=0 -> p : (s'=1) + (1-p) : (s'=2); [] s=0 -> p : (s'=1) + (1-p) : (s'=2);
[] s=1 -> p : (s'=3) + (1-p) : (s'=4);
[] s=2 -> p : (s'=5) + (1-p) : (s'=6);
[] s=1 -> q : (s'=3) + (1-q) : (s'=4);
[] s=2 -> q : (s'=5) + (1-q) : (s'=6);
[] s=3 -> p : (s'=1) + (1-p) : (s'=7) & (d'=1); [] s=3 -> p : (s'=1) + (1-p) : (s'=7) & (d'=1);
[] s=4 -> p : (s'=7) & (d'=2) + (1-p) : (s'=7) & (d'=3); [] s=4 -> p : (s'=7) & (d'=2) + (1-p) : (s'=7) & (d'=3);
[] s=5 -> p : (s'=7) & (d'=4) + (1-p) : (s'=7) & (d'=5); [] s=5 -> p : (s'=7) & (d'=4) + (1-p) : (s'=7) & (d'=5);

Loading…
Cancel
Save