alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python/acc_cond.ipynb
Alexandre Duret-Lutz 0d9c81a6d9 acc: extend top_disjuncts and top_conjuncts to acc_cond as well 
* spot/twa/acc.hh, spot/twa/acc.cc: Implement the new methods.
* python/spot/impl.i: Add bindings for vectors of acc_cond.
* tests/python/acc_cond.ipynb: Test the two methods.
* NEWS: Adjust.
2019-03-29 11:41:52 +01:00

1435 lines
34 KiB
Text
Raw Blame History

{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"spot.setup()"
]
},
{
"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",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{}\n"
]
}
],
"source": [
"print(spot.mark_t())"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,3}\n"
]
}
],
"source": [
"print(spot.mark_t([0, 2, 3])) # works with lists"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,3}\n"
]
}
],
"source": [
"print(spot.mark_t((0, 2, 3))) # works with tuples"
]
},
{
"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",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,3,4}\n",
"{0}\n",
"{2,3}\n"
]
}
],
"source": [
"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)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The bits can be set, cleared, and tested using the `set()`, `clear()`, and `has()` methods:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,3,5}\n"
]
}
],
"source": [
"x.set(5)\n",
"print(x)"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,5}\n"
]
}
],
"source": [
"x.clear(3)\n",
"print(x)"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"True\n",
"False\n"
]
}
],
"source": [
"print(x.has(2))\n",
"print(x.has(3))"
]
},
{
"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",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{2,4,7}\n"
]
}
],
"source": [
"print(x << 2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The different sets can be iterated over with the `sets()` method, that returns a tuple with the index of all bits set."
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2,5}\n",
"[0, 2, 5]\n",
"0\n",
"2\n",
"5\n"
]
}
],
"source": [
"print(x)\n",
"print(list(x.sets()))\n",
"for s in x.sets():\n",
" print(s)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`count()` return the number of sets in a `mark_t`:"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"3"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"x.count()"
]
},
{
"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",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.mark_t([1])"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.mark_t([1,3,5]).lowest()"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{1}\n",
"{3}\n",
"{5}\n"
]
}
],
"source": [
"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)"
]
},
{
"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",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"6"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.mark_t([1, 3, 5]).max_set()"
]
},
{
"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üchi 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` by passing a string that represent the formula to build."
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(Inf(0) & Fin(1)) | Inf(2)\n"
]
},
{
"data": {
"text/plain": [
"spot.acc_code(\"(Inf(0) & Fin(1)) | Inf(2)\")"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')\n",
"print(acc) # shows just the formula\n",
"acc # shows the acc_code object"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You may also use a named acceptance condition:"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code('Rabin 2')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The recognized names are the valid 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",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"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"
]
}
],
"source": [
"print(spot.acc_code('Streett 2..4'))\n",
"print(spot.acc_code('Streett 2..4'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It may also be convenient to generate a random acceptance condition. Below we require between 3 and 5 acceptance sets:"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))\")"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code('random 3..5')"
]
},
{
"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",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))\")"
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a = spot.acc_code('parity min odd 5')\n",
"a"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))\")"
]
},
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a.to_cnf()"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))\")"
]
},
"execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a.to_dnf()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++\n",
"\n",
"Operators `|`, `|=`, `&`, `&=`, `<<`, and `<<=` can be used with their obvious semantics.\n",
"Whenever possible, the inplace versions (`|=`, `&=`, `<<=`) should be prefered, because they create less temporary acceptance conditions."
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
"(Fin(4) & Inf(5)) | (Fin(6) & Inf(7))\n"
]
}
],
"source": [
"x = spot.acc_code('Rabin 2')\n",
"y = spot.acc_code('Rabin 2') << 4\n",
"print(x)\n",
"print(y)"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(Fin(4) & Inf(5)) | (Fin(6) & Inf(7)) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
"((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n"
]
}
],
"source": [
"print(x | y)\n",
"print(x & y)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `complement()` method returns the complemented acceptance condition:"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
"(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))\n"
]
}
],
"source": [
"print(x)\n",
"print(x.complement())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Instead of using `acc_code('string')`, it is also possible to build an acceptance formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n",
"\n",
"Remember that in our encoding for the formula, terms like `Inf(1)&Inf(2)` and `Fin(3)|Fin(4)|Fin(5)` are actually stored as `Inf({1,2})` and `Fin({3,4,5})`, where `{1,2}` and `{3,4,5}` are instance of `mark_t`. These terms can be generated with the\n",
"functions `spot.acc_code.inf(mark)` and `spot.acc_code.fin(mark)`.\n",
"\n",
"`Inf({})` is equivalent to `t`, and `Fin({})` is equivalent to `f`, but it's better to use the functions `spot.acc_code.t()` or `spot.acc_code.f()` directly."
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))\")"
]
},
"execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code.inf([1,2]) & spot.acc_code.fin([3,4,5])"
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"t\")"
]
},
"execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code.inf([])"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"t\")"
]
},
"execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code.t()"
]
},
{
"cell_type": "code",
"execution_count": 28,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"f\")"
]
},
"execution_count": 28,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code.fin([])"
]
},
{
"cell_type": "code",
"execution_count": 29,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"f\")"
]
},
"execution_count": 29,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.acc_code.f()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To evaluate an acceptance condition formula on a run, build a `mark_t` containing all the acceptance sets that are seen infinitely often along this run, and call the `accepting()` method."
]
},
{
"cell_type": "code",
"execution_count": 30,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"acc = (Fin(0) & Inf(1)) | Inf(2)\n",
"acc.accepting([0, 1, 2]) = True\n",
"acc.accepting([1, 2]) = True\n",
"acc.accepting([0, 1]) = False\n",
"acc.accepting([0, 2]) = True\n",
"acc.accepting([0]) = False\n",
"acc.accepting([1]) = True\n",
"acc.accepting([2]) = True\n",
"acc.accepting([]) = False\n"
]
}
],
"source": [
"acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n",
"print(\"acc =\", acc)\n",
"for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n",
" print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally the method `used_sets()` returns a `mark_t` with all the sets appearing in the formula:"
]
},
{
"cell_type": "code",
"execution_count": 31,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Fin(0) & Inf(2)\n",
"{0,2}\n",
"3\n"
]
}
],
"source": [
"acc = spot.acc_code('Fin(0) & Inf(2)')\n",
"print(acc)\n",
"print(acc.used_sets())\n",
"print(acc.used_sets().max_set())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `used_inf_fin_sets()` returns a pair of marks instead, the first one with all sets occuring in `Inf`, and the second one with all sets appearing in `Fin`."
]
},
{
"cell_type": "code",
"execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(spot.mark_t([2]), spot.mark_t([0]))"
]
},
"execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.used_inf_fin_sets()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If the top-level operators is a conjunct or disjunct, the following methods returns lists of clauses."
]
},
{
"cell_type": "code",
"execution_count": 33,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"spot.acc_code(\"(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))\")\n",
"(spot.acc_code(\"Fin(0)\"), spot.acc_code(\"Fin(3)\"), spot.acc_code(\"Inf(1) & Fin(2)\"))\n",
"spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\")\n",
"(spot.acc_code(\"Inf(0)\"), spot.acc_code(\"Inf(1)\"), spot.acc_code(\"Fin(2)|Fin(3)\"))\n",
"(spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\"),)\n"
]
}
],
"source": [
"c = spot.acc_code('Fin(0)|(Inf(1)&Fin(2))|Fin(3)')\n",
"print(repr(c))\n",
"print(c.top_disjuncts())\n",
"c = spot.acc_code('Inf(0)&Inf(1)&(Fin(2)|Fin(3))')\n",
"print(repr(c))\n",
"print(c.top_conjuncts())\n",
"# Nothing to split here as the top operator is not a disjunction\n",
"print(c.top_disjuncts())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# `acc_cond`\n",
"\n",
"Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
"This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets. We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
"\n",
"It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1. The extra two sets will have no impact on the language, even if they are used in the automaton.\n",
"\n",
"The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that. But for the purpose of this notebook, let's do it:"
]
},
{
"cell_type": "code",
"execution_count": 34,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For convenience, you can pass the string directly:"
]
},
{
"cell_type": "code",
"execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond(4, 'Rabin 2')\n",
"acc"
]
},
{
"cell_type": "code",
"execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"4"
]
},
"execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.num_sets()"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.get_acceptance()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `acc_cond` object can also be constructed using only a number of sets. In that case, the acceptance condition defaults to `t`, and it can be changed to something else later (using `set_acceptance()`). The number of acceptance sets can also be augmented with `add_sets()`."
]
},
{
"cell_type": "code",
"execution_count": 38,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"t\")"
]
},
"execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond(4)\n",
"acc"
]
},
{
"cell_type": "code",
"execution_count": 39,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(6, \"t\")"
]
},
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.add_sets(2)\n",
"acc"
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(6, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.set_acceptance('Streett 2')\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:"
]
},
{
"cell_type": "code",
"execution_count": 41,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond('Streett 2')\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above is in fact just syntactic sugar for:"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"code = spot.acc_code('Streett 2')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The common scenario of setting generalized Büchi acceptance can be achieved more efficiently by first setting the number of acceptance sets, and then requiring generalized Büchi acceptance:"
]
},
{
"cell_type": "code",
"execution_count": 43,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"Inf(0)&Inf(1)&Inf(2)&Inf(3)\")"
]
},
"execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond(4)\n",
"acc.set_generalized_buchi()\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `acc_cond` class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, `Inf(0)&Inf(1)&Inf(2)&Inf(3)` is only called generalized Büchi if exactly 4 acceptance sets are used. So the following behavior should not be surprising:"
]
},
{
"cell_type": "code",
"execution_count": 44,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"True\n",
"(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"False\n"
]
}
],
"source": [
"print(acc)\n",
"print(acc.is_generalized_buchi())\n",
"acc.add_sets(1)\n",
"print(acc)\n",
"print(acc.is_generalized_buchi())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Similar methods like `is_t()`, `is_f()`, `is_buchi()`, `is_co_buchi()`, `is_generalized_co_buchi()` all return a Boolean.\n",
"\n",
"The `is_rabin()` and `is_streett()` methods, however, return a number of pairs. The number of pairs is always `num_sets()/2` on success, or -1 on failure."
]
},
{
"cell_type": "code",
"execution_count": 45,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
"2\n",
"-1\n"
]
}
],
"source": [
"acc = spot.acc_cond('Rabin 2')\n",
"print(acc)\n",
"print(acc.is_rabin())\n",
"print(acc.is_streett())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The check for parity acceptance returns three Boolean in a list of the form `[matched, max?, odd?]`. If `matched` is `False`, the other values should be ignored."
]
},
{
"cell_type": "code",
"execution_count": 46,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(4, Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))\n",
"[True, False, True]\n",
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"[False, False, False]\n"
]
}
],
"source": [
"acc = spot.acc_cond('parity min odd 4')\n",
"print(acc)\n",
"print(acc.is_parity())\n",
"acc.set_generalized_buchi()\n",
"print(acc)\n",
"print(acc.is_parity())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If the acceptance condition has some known name, it can be retrieved using the `name()` method. By default the name given is a human-readable string close that used in the HOA format, but with proper accents, and support for name like `Streett-like` or `Rabin-like`. The argument `arg` can specify a different style using the same syntax as in `--format='%[arg]g'` when using the command-line tools."
]
},
{
"cell_type": "code",
"execution_count": 47,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"generalized-Büchi 4\n",
"gen. Büchi 4\n",
"generalized-Buchi\n"
]
}
],
"source": [
"print(acc.name())\n",
"print(acc.name(\"d\")) # <- Style used by print_dot(aut, \"a\")\n",
"print(acc.name(\"0\")) # <- no parameters"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`acc_cond` contains a few functions for manipulating `mark_t` instances, these are typically functions that require known the total number of accepting sets declared.\n",
"\n",
"For instance complementing a `mark_t`:"
]
},
{
"cell_type": "code",
"execution_count": 48,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{0,2}\n"
]
}
],
"source": [
"m = spot.mark_t([1, 3])\n",
"print(acc.comp(m))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`all_sets()` returns a `mark_t` listing all the declared sets: "
]
},
{
"cell_type": "code",
"execution_count": 49,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.mark_t([0, 1, 2, 3])"
]
},
"execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.all_sets()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For convencience, the `accepting()` method of `acc_cond` delegates to that of the `acc_code`. \n",
"Any set passed to `accepting()` that is not used by the acceptance formula has no influence."
]
},
{
"cell_type": "code",
"execution_count": 50,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"acc = (4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"acc.accepting([0, 1, 2, 3, 10]) = True\n",
"acc.accepting([1, 2]) = False\n"
]
}
],
"source": [
"print(\"acc =\", acc)\n",
"for x in ([0, 1, 2, 3, 10], [1, 2]):\n",
" print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally the `unsat_mark()` method of `acc_cond` computes an instance of `mark_t` that is unaccepting (i.e., passing this value to `acc.accepting(...)` will return `False` when such a value exist. Not all acceptance conditions have an satisfiable mark. Obviously the `t` acceptance is always satisfiable, and so are all equivalent acceptances (for instance `Fin(1)|Inf(1)`).\n",
"\n",
"For this reason, `unsat_mark()` actually returns a pair: `(bool, mark_t)` where the Boolean is `False` iff the acceptance is always satisfiable. When the Boolean is `True`, then the second element of the pair gives a non-accepting mark."
]
},
{
"cell_type": "code",
"execution_count": 51,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"(True, spot.mark_t([]))\n"
]
}
],
"source": [
"print(acc)\n",
"print(acc.unsat_mark())"
]
},
{
"cell_type": "code",
"execution_count": 52,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(0, t)\n",
"(False, spot.mark_t([]))\n"
]
}
],
"source": [
"acc = spot.acc_cond(0) # use 0 acceptance sets, and the default formula (t)\n",
"print(acc)\n",
"print(acc.unsat_mark())"
]
},
{
"cell_type": "code",
"execution_count": 53,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))\n",
"(True, spot.mark_t([2]))\n"
]
}
],
"source": [
"acc = spot.acc_cond('Streett 2')\n",
"print(acc)\n",
"print(acc.unsat_mark())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`top_conjuncts` and `top_disjuncts` also work on `acc_cond`. In this case they return tuple of `acc_cond` with the same number of sets."
]
},
{
"cell_type": "code",
"execution_count": 54,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\"),)\n",
"(spot.acc_cond(4, \"Fin(0) | Inf(1)\"), spot.acc_cond(4, \"Fin(2) | Inf(3)\"))\n"
]
}
],
"source": [
"print(acc.top_disjuncts())\n",
"print(acc.top_conjuncts())"
]
}
],
"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.3rc1"
}
},
"nbformat": 4,
"nbformat_minor": 2
}
Reference in a new issue View git blame Copy permalink