You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
480 lines
12 KiB
480 lines
12 KiB
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Getting Started\n",
|
|
"\n",
|
|
"Before starting with this guide, one should follow the instructions for [Installation](installation.ipynb)."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## A Quick Tour through Stormpy\n",
|
|
"\n",
|
|
"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\n",
|
|
"[Storm website](http://www.stormchecker.org/).\n",
|
|
"While we assume some very basic programming concepts, we refrain from using more advanced concepts of python throughout the guide.\n",
|
|
"\n",
|
|
"We start with a selection of high-level constructs in stormpy, and go into more details afterwards. More in-depth examples can be found in the [Advanced Examples](advanced_topics.ipynb).\n",
|
|
"\n",
|
|
"The code examples are also given in the [examples/](https://github.com/moves-rwth/stormpy/blob/master/examples/) folder. These boxes throughout the text will tell you which example contains the code discussed.\n",
|
|
"\n",
|
|
"We start by launching the python 3 interpreter:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"source": [
|
|
"```\n",
|
|
"$ python3\n",
|
|
"```"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"First we import stormpy:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> import stormpy"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Building models\n",
|
|
"\n",
|
|
"[01-getting-started.py](https://github.com/moves-rwth/stormpy/blob/master/examples/01-getting-started.py)\n",
|
|
"\n",
|
|
"There are several ways to create a Markov chain.\n",
|
|
"One of the easiest is to parse a description of such a Markov chain and to let Storm build the chain.\n",
|
|
"\n",
|
|
"Here, we build a Markov chain from a prism program.\n",
|
|
"Stormpy comes with a small set of examples, which we use here:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> import stormpy.examples\n",
|
|
">>> import stormpy.examples.files"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"With this, we can now import the path of our prism file:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> path = stormpy.examples.files.prism_dtmc_die\n",
|
|
">>> prism_program = stormpy.parse_prism_program(path)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The `prism_program` can be translated into a Markov chain:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> model = stormpy.build_model(prism_program)\n",
|
|
">>> print(\"Number of states: {}\".format(model.nr_states))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> print(\"Number of transitions: {}\".format(model.nr_transitions))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"This tells us that the model has 13 states and 20 transitions.\n",
|
|
"\n",
|
|
"Moreover, initial states and deadlocks are indicated with a labelling function. We can see the labels present in the model by:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> print(\"Labels: {}\".format(model.labeling.get_labels()))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"We will investigate ways to examine the model in more detail later in [Investigating the model](#getting-started-investigating-the-model).\n",
|
|
"\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Building properties\n",
|
|
"\n",
|
|
"[02-getting-started.py](https://github.com/moves-rwth/stormpy/blob/master/examples/02-getting-started.py)\n",
|
|
"\n",
|
|
"Storm takes properties in the prism-property format.\n",
|
|
"To express that one is interested in the reachability of any state where the prism program variable `s` is 2, one would formulate:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"source": [
|
|
"```\n",
|
|
"P=? [F s=2]\n",
|
|
"```"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Stormpy can be used to parse this. As the variables in the property refer to a program, the program has to be passed as an additional parameter:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> formula_str = \"P=? [F s=2]\"\n",
|
|
">>> properties = stormpy.parse_properties(formula_str, prism_program)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Notice that properties is now a list of properties containing a single element.\n",
|
|
"\n",
|
|
"However, if we build the model as before, then the appropriate information that the variable `s=2` in some states is not present.\n",
|
|
"In order to label the states accordingly, we should notify Storm upon building the model that we would like to preserve given properties.\n",
|
|
"Storm will then add the labels accordingly:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> model = stormpy.build_model(prism_program, properties)\n",
|
|
">>> print(\"Labels in the model: {}\".format(sorted(model.labeling.get_labels())))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Model building however now behaves slightly different: Only the properties passed are preserved, which means that model building might skip parts of the model.\n",
|
|
"In particular, to check the probability of eventually reaching a state `x` where `s=2`, successor states of `x` are not relevant:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> print(\"Number of states: {}\".format(model.nr_states))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"If we consider another property, however, such as:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"source": [
|
|
"```\n",
|
|
"P=? [F s=7 & d=2]\n",
|
|
"```"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"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.\n",
|
|
"\n",
|
|
"\n",
|
|
"<a id='getting-started-checking-properties'></a>"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Checking properties\n",
|
|
"\n",
|
|
"[03-getting-started.py](https://github.com/moves-rwth/stormpy/blob/master/examples/03-getting-started.py)\n",
|
|
"\n",
|
|
"The last lesson taught us to construct properties and models with matching state labels.\n",
|
|
"Now default checking routines are just a simple command away:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> properties = stormpy.parse_properties(formula_str, prism_program)\n",
|
|
">>> model = stormpy.build_model(prism_program, properties)\n",
|
|
">>> result = stormpy.model_checking(model, properties[0])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"The result may contain information about all states.\n",
|
|
"Instead, we can iterate over the results:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> assert result.result_for_all_states\n",
|
|
">>> for x in result.get_values():\n",
|
|
"... pass # do something with x"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### Results for all states\n",
|
|
"\n",
|
|
"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.\n",
|
|
"\n",
|
|
"A good way to get the result for the initial states is as follows:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> initial_state = model.initial_states[0]\n",
|
|
">>> print(result.at(initial_state))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"\n",
|
|
"<a id='getting-started-investigating-the-model'></a>"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Investigating the model\n",
|
|
"\n",
|
|
"[04-getting-started.py](https://github.com/moves-rwth/stormpy/blob/master/examples/04-getting-started.py)\n",
|
|
"\n",
|
|
"One powerful part of the Storm model checker is to quickly create the Markov chain from higher-order descriptions, as seen above:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> path = stormpy.examples.files.prism_dtmc_die\n",
|
|
">>> prism_program = stormpy.parse_prism_program(path)\n",
|
|
">>> model = stormpy.build_model(prism_program)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"In this example, we will exploit this, and explore the underlying Markov chain of the model.\n",
|
|
"The most basic question might be what the type of the constructed model is:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> print(model.model_type)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"We can also directly explore the underlying state space/matrix.\n",
|
|
"Notice that this code can be applied to both deterministic and non-deterministic models:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> for state in model.states:\n",
|
|
"... for action in state.actions:\n",
|
|
"... for transition in action.transitions:\n",
|
|
"... print(\"From state {}, with probability {}, go to state {}\".format(state, transition.value(), transition.column))"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Let us go into some more details. For DTMCs, each state has (at most) one outgoing probability distribution.\n",
|
|
"Thus:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> for state in model.states:\n",
|
|
"... assert len(state.actions) <= 1"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"We can also check if a state is indeed an initial state. Notice that `model.initial_states` contains state ids, not states.:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {
|
|
"hide-output": false
|
|
},
|
|
"outputs": [],
|
|
"source": [
|
|
">>> for state in model.states:\n",
|
|
"... if state.id in model.initial_states:\n",
|
|
"... pass"
|
|
]
|
|
}
|
|
],
|
|
"metadata": {
|
|
"date": 1598188121.7690735,
|
|
"filename": "getting_started.rst",
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.8.2"
|
|
},
|
|
"title": "Getting Started"
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 4
|
|
}
|