alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tests: fix some examples

Browse source 
Reported by František Blahoudek.

* tests/python/parity.ipynb: Fix examples and improve some text.
This commit is contained in:
Alexandre Duret-Lutz 2019-04-18 14:41:03 +02:00
parent d3cdabeb6e
commit e6c8c09fd5
1 changed files with 54 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

118
tests/python/parity.ipynb
View file

@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
@ -15,80 +15,64 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"# Definitions and examples"
"# Definitions and examples for parity acceptance"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In Spot a **Parity acceptance** is defined by an **kind**, a **style** and a **numsets** (number of acceptance sets):\n",
"In Spot a **parity acceptance** is defined by a **kind**, a **style** and a **numsets**:\n",
"+ The **kind** can be either **max** or **min**.\n",
"+ The **style** can be either **odd** or **even**.\n",
"+ The **numsets** is the number of acceptance sets used by the parity acceptance.\n",
"+ The **kind** can be either **max** or **min**. The parity kind is well defined only if the **numsets** is strictly greater than 1.\n",
" - **max** odd 4: *Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))*\n",
" - **min** odd 4: *Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))*\n",
"+ The **style** can be either **odd** or **even**. The parity style is well defined only if the **numsets** is non-null.\n",
" - max **odd** 4: *Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))*\n",
" - min **even** 4: *Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))*\n",
"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"**Some parity acceptance examples:**\n",
"<div align=\"center\">\n",
"**numsets = 1:** \n",
"</div>\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:--------------:|:--------------:|\n",
"| **odd** | Fin(1) | Fin(1) | \n",
"| **even** | Inf(0) | Inf(0) |\n",
"\n",
"<br>\n",
"<div align=\"center\">\n",
"**numsets = 2:** \n",
"</div>\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:--------------------:|:--------------------:|\n",
"| **odd** | Inf(1) &#124; Fin(0) | Fin(1) & Inf(0) | \n",
"| **even** | Fin(0) & Inf(1) | Inf(0) &#124; Fin(1) |\n",
"\n",
"\n",
"<br>\n",
"<div align=\"center\">\n",
"**numsets = 3:** \n",
"</div>\n",
" \n",
"| | **max** | **min** |\n",
"|:---------:|:-------------------------------:|:-------------------------------:|\n",
"| **odd** | Fin(2) & (Inf(1) &#124; Fin(0)) | Inf(2) &#124; (Fin(1) & Inf(0)) | \n",
"| **even** | Fin(0) & (Inf(1) &#124; Fin(2)) | Inf(0) &#124; (Fin(1) & Inf(2)) |\n",
"\n",
"<br>\n",
"<div align=\"center\">\n",
"**numsets = 4:** \n",
"</div>\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:-----------------------------------------------:|:-----------------------------------------------:|\n",
"| **odd** | Inf(3) &#124; (Fin(2) & (Inf(1) &#124; Fin(0))) | Fin(3) & (Inf(2) &#124; (Fin(1) & Inf(0))) | \n",
"| **even** | Fin(0) & (Inf(1) &#124; (Fin(2) & Inf(3))) | Inf(0) &#124; (Fin(1) & (Inf(2) &#124; Fin(3))) |\n",
"\n",
"<br>\n",
"According to the given examples, we can remark that:\n",
"+ Given a parity **max**: Acceptance sets with greater indexes are more significant\n",
"+ Given a parity **min**: Acceptance sets with lower indexes are more significant"
"Here are some examples:"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"parity min odd 1 = Fin(0)\n",
"parity min odd 2 = Fin(0) & Inf(1)\n",
"parity min odd 3 = Fin(0) & (Inf(1) | Fin(2))\n",
"parity min odd 4 = Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))\n",
"parity min even 1 = Inf(0)\n",
"parity min even 2 = Inf(0) | Fin(1)\n",
"parity min even 3 = Inf(0) | (Fin(1) & Inf(2))\n",
"parity min even 4 = Inf(0) | (Fin(1) & (Inf(2) | Fin(3)))\n",
"parity max odd 1 = Fin(0)\n",
"parity max odd 2 = Inf(1) | Fin(0)\n",
"parity max odd 3 = Fin(2) & (Inf(1) | Fin(0))\n",
"parity max odd 4 = Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))\n",
"parity max even 1 = Inf(0)\n",
"parity max even 2 = Fin(1) & Inf(0)\n",
"parity max even 3 = Inf(2) | (Fin(1) & Inf(0))\n",
"parity max even 4 = Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))\n"
]
}
],
"source": [
"for kind in ['min', 'max']:\n",
" for style in ['odd', 'even']:\n",
" for sets in range(1, 5):\n",
" name = 'parity {} {} {}'.format(kind, style, sets)\n",
" print('{:17} = {}'.format(name, spot.acc_code(name)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Change parity"
"# Change parity\n",
"\n",
"This section describes the `change_parity()` method, that allows switching between different kinds and styles."
]
},
{
@ -103,7 +87,7 @@
},
{
"cell_type": "code",
"execution_count": 2,
"execution_count": 22,
"metadata": {},
"outputs": [
{
@ -1381,7 +1365,13 @@
"metadata": {},
"source": [
"# Colorize parity\n",
"An automaton with a parity acceptance is not necessarily a parity automaton. It must be colored to be qualified like this.\n",
"\n",
"People working with parity automata usually expect all states (or edges) to be part of some acceptance set. This constraints, which come in addition to the use of a parity acceptance, is what the HOA format call \"colored\".\n",
"\n",
"A *parity automaton* is a *colored* automaton with *parity acceptance*.\n",
"\n",
"Coloring an automaton can be done with the `colorize_parity()` function.\n",
"\n",
"## Parity max\n",
"Transitions with multiple acceptance sets are purified by keeping only the set with the greatest index.\n",
"<br>\n",
@ -2093,7 +2083,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.5"
"version": "3.7.3"
}
},
"nbformat": 4,