{
"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:c71f218a80ffc2fb08377daa20d703d7c421278e48d625c4f9fca8ff8f59d80a"
},
"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 0x7f1de22e1870> >"
]
}
],
"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 0x7f1dd5f6a630> >"
]
}
],
"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 0x7f1de22e17e0> >"
]
}
],
"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\"'))\n",
"dir(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 17,
"text": [
"['__bool__',\n",
" '__class__',\n",
" '__contains__',\n",
" '__delattr__',\n",
" '__dict__',\n",
" '__dir__',\n",
" '__doc__',\n",
" '__eq__',\n",
" '__format__',\n",
" '__ge__',\n",
" '__getattribute__',\n",
" '__getitem__',\n",
" '__gt__',\n",
" '__hash__',\n",
" '__init__',\n",
" '__iter__',\n",
" '__le__',\n",
" '__len__',\n",
" '__lt__',\n",
" '__module__',\n",
" '__ne__',\n",
" '__new__',\n",
" '__nonzero__',\n",
" '__reduce__',\n",
" '__reduce_ex__',\n",
" '__repr__',\n",
" '__setattr__',\n",
" '__sizeof__',\n",
" '__str__',\n",
" '__subclasshook__',\n",
" '__swig_destroy__',\n",
" '__weakref__',\n",
" 'add',\n",
" 'append',\n",
" 'begin',\n",
" 'clear',\n",
" 'count',\n",
" 'discard',\n",
" 'empty',\n",
" 'end',\n",
" 'equal_range',\n",
" 'erase',\n",
" 'find',\n",
" 'insert',\n",
" 'iterator',\n",
" 'lower_bound',\n",
" 'rbegin',\n",
" 'rend',\n",
" 'size',\n",
" 'swap',\n",
" 'this',\n",
" 'thisown',\n",
" 'upper_bound']"
]
}
],
"prompt_number": 17
},
{
"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": {}
}
]
}