{
"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:7574bd022ee68fb7411f60cb675c158f5c1e80c5e79e3197073e2abf5d06262f"
},
"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 the divine is not \n",
"# installed, therefore skipping this test in the test suite.\n",
"spot.ltsmin.require('divine')\n",
"# This is notebook also tests the limitation of the number of states in the GraphViz output\n",
"spot.setup(max_states=10)"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"There are two ways to load a DiVinE model: from a file or from a cell. \n",
"\n",
"Loading from a file\n",
"-------------------\n",
"\n",
"We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm -f test1.dve"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file test1.dve\n",
"int a = 0, b = 0;\n",
"\n",
"process P {\n",
" state x;\n",
" init x;\n",
"\n",
" trans\n",
" x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
" x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
"}\n",
"\n",
"process Q {\n",
" state wait, work;\n",
" init wait;\n",
" trans\n",
" wait -> work { guard b > 1; },\n",
" work -> wait { guard a > 1; };\n",
"}\n",
"\n",
"system async;"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Writing test1.dve\n"
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `spot.ltsmin.load` function compiles the model using the `ltlmin` interface and load it. This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"m = spot.ltsmin.load('test1.dve')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Compiling the model creates all several kinds of files. The `test1.dve` file is converted into a C++ source code `test1.dve.cpp` which is then compiled into a shared library `test1.dve2c`. Becauce `spot.ltsmin.load()` has already loaded this shared library, all those files can be erased. If you do not erase the files, `spot.ltsmin.load()` will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.\n",
"\n",
"For editing and loading DVE file from a notebook, it is a better to use the `%%dve` as shown next."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm -f test1.dve test1.dve.cpp test1.dve2C"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Loading from a notebook cell\n",
"----------------------------\n",
"\n",
"The `%%dve` cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files). The variable name that should receive the model (here `m`) should be indicated on the first line, after `%dve`."
]
},
{
"cell_type": "code",
"collapsed": true,
"input": [
"%%dve m\n",
"int a = 0, b = 0;\n",
"\n",
"process P {\n",
" state x;\n",
" init x;\n",
"\n",
" trans\n",
" x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
" x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
"}\n",
"\n",
"process Q {\n",
" state wait, work;\n",
" init wait;\n",
" trans\n",
" wait -> work { guard b > 1; },\n",
" work -> wait { guard a > 1; };\n",
"}\n",
"\n",
"system async;"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 6
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Working with an ltsmin model\n",
"----------------------------\n",
"\n",
"Printing an ltsmin model shows some information about the variables it contains and their types, however the `info()` methods provide the data in a map that is easier to work with."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"m"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"text": [
"ltsmin model with the following variables:\n",
" a: int\n",
" b: int\n",
" P: ['x']\n",
" Q: ['wait', 'work']"
]
}
],
"prompt_number": 7
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"sorted(m.info().items())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 8,
"text": [
"[('state_size', 4),\n",
" ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
" ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
]
}
],
"prompt_number": 8
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To obtain a Kripke structure, call `kripke` and supply a list of atomic propositions to observe in the model."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"k = m.kripke([\"a<1\", \"b>2\"])\n",
"k"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 9,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f2d78243480> >"
]
}
],
"prompt_number": 9
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"k.show('.<15')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 10,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 10
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"k.show('.<0') # unlimited output"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 11,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 11
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.translate('\"a<1\" U \"b>2\"'); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 12,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f2d78197fc0> >"
]
}
],
"prompt_number": 12
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.otf_product(k, a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 13,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f2d78243360> >"
]
}
],
"prompt_number": 13
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If we want to create a `model_check` function that takes a model and formula, we need to get the list of atomic propositions used in the formula using `atomic_prop_collect()`. This returns an `atomic_prop_set`:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"')); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$\\{``\\mathit{a < 2}\\textrm{''}, ``\\mathit{b == 1}\\textrm{''}\\}$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 14,
"text": [
"{\"a < 2\", \"b == 1\"}"
]
}
],
"prompt_number": 14
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"def model_check(f, m):\n",
" f = spot.formula(f)\n",
" ss = m.kripke(spot.atomic_prop_collect(f))\n",
" nf = spot.formula_Not(f).translate()\n",
" return spot.otf_product(ss, nf).is_empty() "
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 15
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"model_check('\"a<1\" R \"b > 1\"', m)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 16,
"text": [
"False"
]
}
],
"prompt_number": 16
}
],
"metadata": {}
}
]
}