{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"import spot.ltsmin\n",
"# The following line causes the notebook to exit with 77 if 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)"
]
},
{
"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",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"!rm -f test1.dve"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Writing test1.dve\n"
]
}
],
"source": [
"%%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;"
]
},
{
"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",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"m = spot.ltsmin.load('test1.dve')"
]
},
{
"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",
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
"!rm -f test1.dve test1.dve.cpp test1.dve2C"
]
},
{
"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",
"execution_count": 6,
"metadata": {},
"outputs": [],
"source": [
"%%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;"
]
},
{
"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",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"ltsmin model with the following variables:\n",
" a: int\n",
" b: int\n",
" P: ['x']\n",
" Q: ['wait', 'work']"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"m"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[('state_size', 4),\n",
" ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
" ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sorted(m.info().items())"
]
},
{
"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",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74b867eab0> >"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"k = m.kripke([\"a<1\", \"b>2\"])\n",
"k"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"k.show('.<15')"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"k.show('.<0') # unlimited output"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74b860d990> >"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a = spot.translate('\"a<1\" U \"b>2\"'); a"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74b867e5d0> >"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.otf_product(k, a)"
]
},
{
"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",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\{``\\mathit{a < 2}\\textrm{''}, ``\\mathit{b == 1}\\textrm{''}\\}$"
],
"text/plain": [
"{\"a < 2\", \"b == 1\"}"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"')); a"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [],
"source": [
"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() "
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"model_check('\"a<1\" R \"b > 1\"', m)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Instead of `otf_product(x, y).is_empty()` we prefer to call `!x.intersects(y)`. There is also `x.intersecting_run(y)` that can be used to return a counterexample."
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [],
"source": [
"def model_debug(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 ss.intersecting_run(nf)"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" a=0, b=0, Q=0\n",
" | \"a<1\" & !\"b > 1\" & !dead\n",
" a=1, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
" a=2, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & !dead\n",
"Cycle:\n",
" a=3, b=0, Q=0\n",
" | !\"a<1\" & !\"b > 1\" & dead"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"run = model_debug('\"a<1\" R \"b > 1\"', m); run"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This accepting run can be represented as an automaton (the `True` argument requires the state names to be preserved). This can be more readable."
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f74b860ded0> >"
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"run.as_twa(True)"
]
}
],
"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.6.4+"
}
},
"nbformat": 4,
"nbformat_minor": 2
}