{
"cells": [
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [],
"source": [
"from IPython.display import display\n",
"import spot\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Definitions and examples for parity acceptance"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"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",
" \n",
"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\n",
"\n",
"This section describes the `change_parity()` method, that allows switching between different kinds and styles."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## To toggle **style**\n",
"### A new acceptance set is introduced and all the existing sets' indexes are increased by 1.\n",
"#### Parity max odd 5 -> Parity max even\n",
"If the acceptance is a parity **max**, all the transitions that do not belong to any acceptance set will belong to the new set."
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd5 = tuple(spot.automata(\"randaut -A 'parity max odd 5' -Q4 2|\"))[0]\n",
"display(aut_max_odd5.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new indexes of the acceptance sets:\n",
"+ 4 -> 5\n",
"+ 3 -> 4\n",
"+ 2 -> 3\n",
"+ 1 -> 2\n",
"+ 0 -> 1\n",
"+ ∅ -> 0"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Result of Parity max odd 5 -> Parity max even 6"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd5_to_even = spot.change_parity(aut_max_odd5, spot.parity_kind_any, spot.parity_style_even)\n",
"display(aut_max_odd5_to_even.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Parity min odd 5 -> Parity min even\n",
"If the acceptance is a parity **min**, the new acceptance set will not be used."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_min_odd5 = tuple(spot.automata(\"randaut -A 'parity min odd 5' -Q4 2|\"))[0]\n",
"display(aut_min_odd5.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new indexes of the acceptance sets:\n",
"+ 4 -> 5\n",
"+ 3 -> 4\n",
"+ 2 -> 3\n",
"+ 1 -> 2\n",
"+ 0 -> 1\n",
"+ ∅ -> ∅"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Result of Parity min odd 5 -> Parity min even 6"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_min_odd5_to_even = spot.change_parity(aut_min_odd5, spot.parity_kind_any, spot.parity_style_even)\n",
"display(aut_min_odd5_to_even.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### To toggle **kind**\n",
"#### The indexes of the acceptance sets are reversed\n",
"#### Parity max odd 5 ----> Parity min:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd5 = tuple(spot.automata(\"randaut -A 'parity max odd 5' -Q4 2|\"))[0]\n",
"display(aut_max_odd5.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new indexes of the acceptance sets:\n",
"+ 4 -> 0\n",
"+ 3 -> 1\n",
"+ 2 -> 2\n",
"+ 1 -> 3\n",
"+ 0 -> 4\n",
"+ ∅ -> ∅"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Result of Parity max odd 5 ----> Parity min odd 5:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd5_to_min = spot.change_parity(aut_max_odd5, spot.parity_kind_min, spot.parity_style_any)\n",
"display(aut_max_odd5_to_min.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Parity max odd 4 ----> Parity min odd:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4 = tuple(spot.automata(\"randaut -A 'parity max odd 4' -Q4 2|\"))[0]\n",
"display(aut_max_odd4.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new indexes of the acceptance sets:\n",
"+ 3 -> 0\n",
"+ 2 -> 1\n",
"+ 1 -> 2\n",
"+ 0 -> 3\n",
"+ ∅ -> ∅"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Result of Parity max odd 4 ----> Parity min even 4:\n",
"\n",
"If the **numsets** is even and the **kind** is toggled, then the **style** will be toggled too."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4_to_min = spot.change_parity(aut_max_odd4, spot.parity_kind_min, spot.parity_style_any)\n",
"display(aut_max_odd4_to_min.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To keep the same **style** a new acceptance set is introduced, thus the **style** is toggled once again.\n",
"
\n",
"The new indexes of the acceptance sets are:\n",
"\n",
"+ 3 -> 0 -> 1\n",
"+ 2 -> 1 -> 2\n",
"+ 1 -> 2 -> 3\n",
"+ 0 -> 3 -> 4\n",
"+ ∅ -> ∅ -> 0 (as the resulting automaton is a parity min)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### Result of Parity max odd 4 ----> Parity min even 5:"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4_to_min_bis = spot.change_parity(aut_max_odd4, spot.parity_kind_min, spot.parity_style_same)\n",
"display(aut_max_odd4_to_min_bis.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Colorize parity\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",
"
\n",
"If there is a transition that do not belong to any acceptance set, a new acceptance set is introduced at the least significant place.\n",
"
\n",
"The least significant place of a parity max acceptance is where the indexes are the lowest, so all the existing acceptance sets' indexes will be shifted.\n",
"#### Colorize parity max odd 4"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4 = tuple(spot.automata(\"randaut -A 'parity max odd 4' -Q4 2|\"))[0]\n",
"display(aut_max_odd4.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new acceptance sets are:\n",
"+ ∅ -> 0\n",
"+ 0 -> 1\n",
"+ 1 -> 2\n",
"+ 2 -> 3\n",
"+ 3 -> 4\n",
"\n",
"#### The result of colorizing the given parity max odd 4 is"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4_colored = spot.colorize_parity(aut_max_odd4, False)\n",
"display(aut_max_odd4_colored.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You can notice that the **style** has been toggled.\n",
"
\n",
"To prevent colorize_parity from this we can add one extra acceptance set in the acceptance condition.\n",
"\n",
"The new acceptance sets are now:\n",
"+ ∅ -> 1\n",
"+ 0 -> 2\n",
"+ 1 -> 3\n",
"+ 2 -> 4\n",
"+ 3 -> 5\n",
"#### The result of colorizing the given parity max odd 4 without changing the style is"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_max_odd4_colored_bis = spot.colorize_parity(aut_max_odd4, True)\n",
"display(aut_max_odd4_colored_bis.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Parity min\n",
"Transitions with multiple acceptance sets are purified by keeping only the set with the lowest index.\n",
"
\n",
"If there is a transition that do not belong to any acceptance set, a new acceptance set is introduced at the least significant place.\n",
"
\n",
"The least significant place of a parity min acceptance is where the indexes are the greatest.\n",
"#### Colorize parity min odd 4"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_min_odd4 = tuple(spot.automata(\"randaut -A 'parity min odd 4' -Q4 2|\"))[0]\n",
"display(aut_min_odd4.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The new acceptance sets are:\n",
"+ ∅ -> 4\n",
"+ 0 -> 0\n",
"+ 1 -> 1\n",
"+ 2 -> 2\n",
"+ 3 -> 3\n",
"\n",
"#### The result of colorizing the given parity max odd 4 is"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut_min_odd4_colored_bis = spot.colorize_parity(aut_min_odd4, True)\n",
"display(aut_min_odd4_colored_bis.show(\".a\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Remark: colorizing a parity min won't change the **style** of the acceptance."
]
}
],
"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.3"
}
},
"nbformat": 4,
"nbformat_minor": 2
}