{
"metadata": {
"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.5.1"
},
"name": "",
"signature": "sha256:bbe178ef6526ace33fca472e0e20c706861b6b033a70d184f5a219c60812d5b7"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"import spot.ltsmin\n",
"# The following line causes the notebook to exit with 77 if spins is not \n",
"# installed, therefore skipping this test in the test suite.\n",
"spot.ltsmin.require('spins')\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"There are two ways to load a Promela model: from a file or from a cell. \n",
"\n",
"Loading from a cell\n",
"-------------------\n",
"\n",
"Using the `%%pml` magic will save the model in a temporary file, call `spins` to compile it, load the resulting shared library, and store the result into an object whose name is passed as an argument to `%%pml`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%pml model\n",
"active proctype P() {\n",
"int a = 0;\n",
"int b = 0;\n",
"x: if\n",
" :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n",
" :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n",
"fi;\n",
"}"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stderr",
"text": [
"SpinS Promela Compiler - version 1.0 (5-Feb-2013)\n",
"(C) University of Twente, Formal Methods and Tools group\n",
"\n",
"Start parsing tmplq2ksakk.pml...done\n",
"\n",
"Optimizing graphs...\n",
" StateMerging changed 0 states/transitions.\n",
" RemoveUselessActions changed 2 states/transitions.\n",
" RemoveUselessGotos changed 2 states/transitions.\n",
" RenumberAll changed 1 states/transitions.\n",
"Optimization done\n",
"\n",
"Generating DM information ...\n",
"Generating DM information done\n",
"\n",
"Generating guard information ...\n",
" Found 0 / 4 ( 0.0%) !MCE guards.\n",
" Found 3 / 8 ( 37.5%) !IMC guards.\n",
" Found 6 / 6 (100.0%) !NES guards.\n",
" Found 6 / 6 (100.0%) !NDS guards.\n",
" Found 6 / 6 (100.0%) !visibilities.\n",
"Generating guard information done\n",
"\n",
"Written C model to /home/adl/git/spot/tests/python/tmplq2ksakk.pml.spins.c\n",
"Compiled C model to tmplq2ksakk.pml.spins\n",
"\n"
]
}
],
"prompt_number": 2
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Yes, the `spins` compiler is quite verbose. Printing the resulting `model` object will show information about the variables in that model. "
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"model"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"ltsmin model with the following variables:\n",
" _nr_pr: int\n",
" P_0._pc: pc\n",
" P_0._pid: pid\n",
" P_0.a: int\n",
" P_0.b: int"
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To instantiate a Kripke structure, one should provide a list of atomic proposition to observe."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"k = model.kripke(['P_0.a < 2', 'P_0.b > 1']); k"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f87ac090240> >"
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"And then from this Kripke structure you can do some model checking using the same functions as illustrated in `ltsmin-dve.ipynb`.\n",
"\n",
"Loading from a `*.pml` file\n",
"---------------------------\n",
"\n",
"Another option is to use `ltsmin.load()` to load a Promela file directly. In order for this test-case to be self-contained, we are going to write the Promela file first, but in practice you probably already have your model."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm -rf test1.pml"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file test1.pml\n",
"active proctype P() {\n",
"int a = 0;\n",
"int b = 0;\n",
"x: if\n",
" :: d_step {a < 3 && b < 3; a = a + 1; } goto x;\n",
" :: d_step {a < 3 && b < 3; b = b + 1; } goto x;\n",
"fi;\n",
"}"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Writing test1.pml\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now load it:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"model2 = spot.ltsmin.load('test1.pml')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 7
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"model2"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 8,
"text": [
"ltsmin model with the following variables:\n",
" _nr_pr: int\n",
" P_0._pc: pc\n",
" P_0._pid: pid\n",
" P_0.a: int\n",
" P_0.b: int"
]
}
],
"prompt_number": 8
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm -f test1.pml test1.pml.spins.c test1.pml.spins"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 9
}
],
"metadata": {}
}
]
}