Commit 2927cf38 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: add some doc & tests for the acceptance bindings

* wrap/python/tests/acc_cond.ipynb: New file.
* wrap/python/tests/Makefile.am, doc/org/tut.org: Add it.
* wrap/python/spot_impl.i: Add printer for acc_cond::mark_t.
parent 4993e807
......@@ -50,6 +50,8 @@ real notebooks instead.
generated random automata, which are displayed in a table before and
after acceptance simplification
- [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser
- [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][acc_cond.ipynb]] documents the interface for manipulating acceptance
conditions
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
- [[https://spot.lrde.epita.fr/ipynb/decompose.html][decompose.ipynb]] illustrates the =decompose_strength()= function
- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing
......
......@@ -441,14 +441,6 @@ namespace std {
std::string __str__() { return spot::str_psl(*self); }
}
%extend spot::acc_cond::mark_t {
// http://comments.gmane.org/gmane.comp.programming.swig/14822
mark_t(const std::vector<unsigned>& f)
{
return new spot::acc_cond::mark_t(f.begin(), f.end());
}
}
%extend spot::twa {
void set_name(std::string name)
{
......@@ -487,12 +479,25 @@ namespace std {
}
%extend spot::acc_cond::mark_t {
// http://comments.gmane.org/gmane.comp.programming.swig/14822
mark_t(const std::vector<unsigned>& f)
{
return new spot::acc_cond::mark_t(f.begin(), f.end());
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::twa_run {
......
......@@ -31,6 +31,7 @@ LOG_DRIVER = $(TEST_LOG_DRIVER)
check_SCRIPTS = run
TESTS = \
acc_cond.ipynb \
accparse.ipynb \
accparse2.py \
alarm.py \
......
{
"metadata": {
"name": "",
"signature": "sha256:f11212c3a17ce302ae81974af32b21c1ebda4aa54d8930f03787ce7ed1c9e5f5"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Acceptance conditions\n",
"\n",
"The acceptance condition of an automaton specifies which of its paths are accepting.\n",
"\n",
"The way acceptance conditions are stored in Spot is derived from the way acceptance conditions are specified in the [HOA format](http://adl.github.io/hoaf/). In HOA, acceptance conditions are given as a line of the form:\n",
"\n",
" Acceptance: 3 (Inf(0)&Fin(1))|Inf(2)\n",
"\n",
"The number `3` gives the number of acceptance sets used (numbered from `0` to `2` in that case), while the rest of the line is a positive Boolean formula over terms of the form:\n",
"- `Inf(n)`, that is true if and only if the set `n` is seen infinitely often,\n",
"- `Fin(n)`, that is true if and only if the set `n` should be seen finitely often,\n",
"- `t`, always true,\n",
"- `f`, always false.\n",
"\n",
"The HOA specifications additionally allows terms of the form `Inf(!n)` or `Fin(!n)` but Spot automatically rewrites those away when reading an HOA file.\n",
"\n",
"Note that the number of sets given can be larger than what is actually needed by the acceptance formula.\n",
"\n",
"Transitions in automata can be tagged as being part of some member sets, and a path in the automaton is accepting if the set of acceptance sets visited along this path satify the acceptance condition.\n",
"\n",
"Definining acceptance conditions in Spot involves three different types of C++ objects:\n",
"\n",
"- `spot::acc_cond` is used to represent an acceptance condition, that is: a number of sets and a formula.\n",
"- `spot::acc_cond::acc_code`, is used to represent Boolean formula for the acceptance condition using a kind of byte code (hence the name)\n",
"- `spot::acc_cond::mark_t`, is a type of bit-vector used to represent membership to acceptance sets.\n",
"\n",
"In because Swig's support for nested class is limited, these types are available respectively as `spot.acc_cond`, `spot.acc_code`, and `spot.mark_t` in Python.\n",
"\n",
"## `mark_t`\n",
"\n",
"Let's start with the simpler of these three objects. `mark_t` is a type of bit vector. Its main constructor takes a sequence of set numbers."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mark_t()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"text": [
"{}"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mark_t([0, 2, 3])"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"{0,2,3}"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mark_t((0, 2, 3))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"text": [
"{0,2,3}"
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"As seen above, the sequence of set numbers can be specified using a list or a tuple. While from the Python language point of view, using a tuple is faster than using a list, the overhead to converting all the arguments from Python to C++ and then converting the resuslting back from C++ to Python makes this difference completely negligeable. In the following, we opted to use lists, because brackets are more readable than nested parentheses."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"x = spot.mark_t([0, 2, 3])\n",
"y = spot.mark_t([0, 4])\n",
"print(x | y)\n",
"print(x & y)\n",
"print(x - y)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2,3,4}\n",
"{0}\n",
"{2,3}\n"
]
}
],
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The bits can be set, cleared, and tested using the `set()`, `clear()`, and `has()` methods:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"x.set(5)\n",
"print(x)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2,3,5}\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"x.clear(3)\n",
"print(x)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2,5}\n"
]
}
],
"prompt_number": 7
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(x.has(2))\n",
"print(x.has(3))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"True\n",
"False\n"
]
}
],
"prompt_number": 8
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Left-shifting will increment all set numbers.\n",
"This operation is useful when building the product of two automata: all the set number of one automaton have to be shift by the number of sets used in the other automaton."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"x << 2"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 9,
"text": [
"{2,4,7}"
]
}
],
"prompt_number": 9
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Internally, the `mark_t` stores the bit-vector as an integer. This also implies that we currently do not support more than 32 acceptance sets. The underlaying integer can be retrieved using `.id`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(x)\n",
"print(x.id)\n",
"print(bin(x.id))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2,5}\n",
"37\n",
"0b100101\n"
]
}
],
"prompt_number": 10
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`mark_t` can also be initialized using an integer: in that case the integer is interpreted as a bit vector.\n",
"\n",
"A frequent error is to use `mark_t(n)` when we really mean `mark_t([n])` or `mark_t((n,))`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"# compare\n",
"print(spot.mark_t([5]))\n",
"# with\n",
"print(spot.mark_t(5))\n",
"print(spot.mark_t(0b10101))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{5}\n",
"{0,2}\n",
"{0,2,4}\n"
]
}
],
"prompt_number": 11
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The different sets can be iterated over with the `sets()` method, that returns a tuble with the index of all bits set."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(x)\n",
"print(x.sets())\n",
"for s in x.sets():\n",
" print(s)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2,5}\n",
"(0, 2, 5)\n",
"0\n",
"2\n",
"5\n"
]
}
],
"prompt_number": 12
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`count()` return the number of sets in a `mark_t`:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"x.count()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 13,
"text": [
"3"
]
}
],
"prompt_number": 13
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`lowest()` returns a `mark_t` containing only the lowest set number. This provides another way to iterate overs all set numbers in cases where you need the result as a `mark_t`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mark_t([1,3,5]).lowest()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 14,
"text": [
"{1}"
]
}
],
"prompt_number": 14
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"v = spot.mark_t([1, 3, 5])\n",
"while v: # this stops once v is empty\n",
" b = v.lowest()\n",
" v -= b\n",
" print(b)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{1}\n",
"{3}\n",
"{5}\n"
]
}
],
"prompt_number": 15
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`max_set()` returns the number of the highest set plus one. This is usually used to figure out how many sets we need to declare on the `Acceptance:` line of the HOA format:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.mark_t([1, 3, 5]).max_set()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 16,
"text": [
"6"
]
}
],
"prompt_number": 16
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## `acc_code`\n",
"\n",
"`acc_code` encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in [reverse Polish notation](http://en.wikipedia.org/wiki/Reverse_Polish_notation) in which conjunctions of `Inf(n)` terms, and disjunctions of `Fin(n)` terms are grouped. In particular, the frequently-used genaralized-B\u00fcchi acceptance conditions (like `Inf(0)&Inf(1)&Inf(2)`) are always encoded as a single term (like `Inf({0,1,2})`).\n",
"\n",
"The simplest way to construct an `acc_code` is via the `parse_acc_code()` function."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('(Inf(0)&Fin(1))|Inf(2)')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 17,
"text": [
"(Fin(1) & Inf(0)) | Inf(2)"
]
}
],
"prompt_number": 17
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You may also use a named acceptance condition:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('Rabin 2')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 18,
"text": [
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))"
]
}
],
"prompt_number": 18
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The recognized names are the valide values for `acc-name:` in the [HOA format](http://adl.github.io/hoaf/). Additionally numbers may be replaced by ranges of the form `n..m`, in which case a random number is selected in that range."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_acc_code('Streett 2..4'))\n",
"print(spot.parse_acc_code('Streett 2..4'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) & (Fin(6) | Inf(7))\n",
"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n"
]
}
],
"prompt_number": 19
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It may also be convenient to generate a random acceptance condition:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('random 3..5')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 20,
"text": [
"(Fin(3) | Inf(1)) & (Fin(0)|Fin(2)) & Inf(4)"
]
}
],
"prompt_number": 20
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `to_cnf()` and `to_dnf()` functions can be used to rewrite the formula into Conjunctive or Disjunctive normal forms. This functions will simplify the resulting formulas to make them irredundant."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.parse_acc_code('parity min odd 5')\n",
"a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 21,
"text": [
"Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))"
]
}
],
"prompt_number": 21
},
{