From 8def8dd30bcb1fdb89c0a19b68ca3c1deea4cf7b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 1 Feb 2017 12:07:20 +0100 Subject: [PATCH] extended getting started guide --- doc/source/getting_started.rst | 30 ++++++++++++++++--- doc/source/index.rst | 2 ++ lib/stormpy/__init__.py | 1 + lib/stormpy/examples/files.py | 4 ++- .../examples/files/pdtmc/parametric_die.pm | 5 ++-- 5 files changed, 35 insertions(+), 7 deletions(-) diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index eafa498..7f87af0 100644 --- a/doc/source/getting_started.rst +++ b/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:: 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. 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:: @@ -104,18 +104,39 @@ The result may contain information about all states. Merely printing does not gi 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 ------------------------------------ .. 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 @@ -129,6 +150,7 @@ Checking parametric models Investigating the model ------------------------------------- +.. seealso:: ``06-getting-started.py`` diff --git a/doc/source/index.rst b/doc/source/index.rst index d55e7ae..9b081c5 100644 --- a/doc/source/index.rst +++ b/doc/source/index.rst @@ -15,6 +15,8 @@ Stormpy Documentation installation getting_started + contributors + Stormpy API Reference ==================================== diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 04e2390..32e577b 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -3,6 +3,7 @@ from .core import * from . import storage from .storage import * from .version import __version__ +import stormpy.logic core._set_up("") diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index fa0e663..d13ca7d 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -9,5 +9,7 @@ def _path(folder, file): prism_dtmc_die = _path("dtmc", "die.pm") """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") -"""Bounded Retransmission Protocol""" \ No newline at end of file +"""Bounded Retransmission Protocol""" diff --git a/lib/stormpy/examples/files/pdtmc/parametric_die.pm b/lib/stormpy/examples/files/pdtmc/parametric_die.pm index bd4e8b1..25b5ec8 100644 --- a/lib/stormpy/examples/files/pdtmc/parametric_die.pm +++ b/lib/stormpy/examples/files/pdtmc/parametric_die.pm @@ -2,6 +2,7 @@ dtmc const double p; +const double q; module die @@ -11,8 +12,8 @@ module die d : [0..6] init 0; [] 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=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);