{
"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 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 0x7fb8f84f9870> >"
]
},
"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": "markdown",
"metadata": {},
"source": [
"If we have an LTL proposition to check, we can convert it into an automaton using `spot.translate()`, and synchronize that automaton with the Kripke structure using `spot.otf_product()`. This `otf_product()` function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm \"consumes\" it (here the display routine). "
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fb8f84691e0> >"
]
},
"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 0x7fb8f8469360> >"
]
},
"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": [
"$\\{\\unicode{x201C}\\mathit{a < 2}\\unicode{x201D}, \\unicode{x201C}\\mathit{b == 1}\\unicode{x201D}\\}$"
],
"text/plain": [
"spot.atomic_prop_set([spot.formula(\"\\\"a < 2\\\"\"), spot.formula(\"\\\"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",
" nf = spot.formula.Not(f)\n",
" ss = m.kripke(spot.atomic_prop_collect(nf))\n",
" return spot.otf_product(ss, nf.translate()).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",
" nf = spot.formula.Not(f)\n",
" ss = m.kripke(spot.atomic_prop_collect(nf))\n",
" return ss.intersecting_run(nf.translate())"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"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\n",
"\n"
]
}
],
"source": [
"run = model_debug('\"a<1\" R \"b > 1\"', m); print(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 0x7fb8f85624e0> >"
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"run.as_twa(True)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Saving Kripke structures to some file\n",
"\n",
"For experiments, it is sometime useful to save a Kripke structure in the HOA format. The HOA printer will automatically use `state-labels` for Kripke structures."
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"HOA: v1\n",
"States: 22\n",
"Start: 0\n",
"AP: 3 \"a<1\" \"b>2\" \"dead\"\n",
"acc-name: all\n",
"Acceptance: 0 t\n",
"properties: state-labels explicit-labels state-acc\n",
"--BODY--\n",
"State: [0&!1&!2] 0 \"a=0, b=0, Q=0\"\n",
"1 2\n",
"State: [!0&!1&!2] 1 \"a=1, b=0, Q=0\"\n",
"3 4\n",
"State: [0&!1&!2] 2 \"a=0, b=1, Q=0\"\n",
"4 5\n",
"State: [!0&!1&!2] 3 \"a=2, b=0, Q=0\"\n",
"6 7\n",
"State: [!0&!1&!2] 4 \"a=1, b=1, Q=0\"\n",
"7 8\n",
"State: [0&!1&!2] 5 \"a=0, b=2, Q=0\"\n",
"8 9 10\n",
"State: [!0&!1&2] 6 \"a=3, b=0, Q=0\"\n",
"6\n",
"State: [!0&!1&!2] 7 \"a=2, b=1, Q=0\"\n",
"11 12\n",
"State: [!0&!1&!2] 8 \"a=1, b=2, Q=0\"\n",
"12 13 14\n",
"State: [0&1&!2] 9 \"a=0, b=3, Q=0\"\n",
"15\n",
"State: [0&!1&!2] 10 \"a=0, b=2, Q=1\"\n",
"14 15\n",
"State: [!0&!1&2] 11 \"a=3, b=1, Q=0\"\n",
"11\n",
"State: [!0&!1&!2] 12 \"a=2, b=2, Q=0\"\n",
"16 17 18\n",
"State: [!0&1&!2] 13 \"a=1, b=3, Q=0\"\n",
"19\n",
"State: [!0&!1&!2] 14 \"a=1, b=2, Q=1\"\n",
"18 19\n",
"State: [0&1&2] 15 \"a=0, b=3, Q=1\"\n",
"15\n",
"State: [!0&!1&!2] 16 \"a=3, b=2, Q=0\"\n",
"20\n",
"State: [!0&1&!2] 17 \"a=2, b=3, Q=0\"\n",
"21\n",
"State: [!0&!1&!2] 18 \"a=2, b=2, Q=1\"\n",
"20 21 12\n",
"State: [!0&1&2] 19 \"a=1, b=3, Q=1\"\n",
"19\n",
"State: [!0&!1&!2] 20 \"a=3, b=2, Q=1\"\n",
"16\n",
"State: [!0&1&!2] 21 \"a=2, b=3, Q=1\"\n",
"17\n",
"--END--\n"
]
}
],
"source": [
"string = k.to_str('hoa')\n",
"print(string)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You can load this as a Kripke structure by passing the `want_kripke` option to `spot.automaton()`. The type `kripke_graph` stores the Kripke structure explicitely (like a `twa_graph` stores an automaton explicitely), so you may want to avoid it for very large modelsand use it only for development."
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\n"
]
},
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7fb8f84690f0> >"
]
},
"execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"k2 = spot.automaton(string, want_kripke=True)\n",
"print(type(k2))\n",
"k2"
]
}
],
"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.7.2+"
}
},
"nbformat": 4,
"nbformat_minor": 2
}