{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"collapsed": false
},
"outputs": [],
"source": [
"from IPython.display import display\n",
"import spot\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Definitions and examples"
]
},
{
"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",
"+ 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",
"\n",
"**numsets = 1:** \n",
"
\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:--------------:|:--------------:|\n",
"| **odd** | Fin(1) | Fin(1) | \n",
"| **even** | Inf(0) | Inf(0) |\n",
"\n",
"\n",
"**numsets = 2:** \n",
"
\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:--------------------:|:--------------------:|\n",
"| **odd** | Inf(1) | Fin(0) | Fin(1) & Inf(0) | \n",
"| **even** | Fin(0) & Inf(1) | Inf(0) | Fin(1) |\n",
"\n",
"\n",
"\n",
"**numsets = 3:** \n",
"
\n",
" \n",
"| | **max** | **min** |\n",
"|:---------:|:-------------------------------:|:-------------------------------:|\n",
"| **odd** | Fin(2) & (Inf(1) | Fin(0)) | Inf(2) | (Fin(1) & Inf(0)) | \n",
"| **even** | Fin(0) & (Inf(1) | Fin(2)) | Inf(0) | (Fin(1) & Inf(2)) |\n",
"\n",
"\n",
"**numsets = 4:** \n",
"
\n",
"\n",
"| | **max** | **min** |\n",
"|:---------:|:-----------------------------------------------:|:-----------------------------------------------:|\n",
"| **odd** | Inf(3) | (Fin(2) & (Inf(1) | Fin(0))) | Fin(3) & (Inf(2) | (Fin(1) & Inf(0))) | \n",
"| **even** | Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) | Inf(0) | (Fin(1) & (Inf(2) | Fin(3))) |\n",
"\n",
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"❹ \n",
") & (Inf( \n",
"❸ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❶ \n",
") | Fin( \n",
"⓿ \n",
")))) \n",
"[parity max odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❶ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❸ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"❺ \n",
") & (Inf( \n",
"❹ \n",
") | (Fin( \n",
"❸ \n",
") & (Inf( \n",
"❷ \n",
") | (Fin( \n",
"❶ \n",
") & Inf( \n",
"⓿ \n",
"))))) \n",
"[parity max even 6] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❺ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
"⓿ \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❷ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❺ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
"⓿ \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"⓿ \n",
") & (Inf( \n",
"❶ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❸ \n",
") | Fin( \n",
"❹ \n",
")))) \n",
"[parity min odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❶ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❸ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Inf( \n",
"⓿ \n",
") | (Fin( \n",
"❶ \n",
") & (Inf( \n",
"❷ \n",
") | (Fin( \n",
"❸ \n",
") & (Inf( \n",
"❹ \n",
") | Fin( \n",
"❺ \n",
"))))) \n",
"[parity min even 6] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❺ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❷ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❺ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"❹ \n",
") & (Inf( \n",
"❸ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❶ \n",
") | Fin( \n",
"⓿ \n",
")))) \n",
"[parity max odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❶ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❸ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"⓿ \n",
") & (Inf( \n",
"❶ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❸ \n",
") | Fin( \n",
"❹ \n",
")))) \n",
"[parity min odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" 3->0 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❸ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
" 1->3 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❶ \n",
" 1->1 \n",
"\n",
"\n",
"p0 & p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Inf( \n",
"❸ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❶ \n",
") | Fin( \n",
"⓿ \n",
"))) \n",
"[parity max odd 4] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"⓿ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
"❷ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Inf( \n",
"⓿ \n",
") | (Fin( \n",
"❶ \n",
") & (Inf( \n",
"❷ \n",
") | Fin( \n",
"❸ \n",
"))) \n",
"[parity min even 4] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❸ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❶ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" \n",
" "
],
"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",
"\n",
"G \n",
"\n",
"Fin( \n",
"⓿ \n",
") & (Inf( \n",
"❶ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❸ \n",
") | Fin( \n",
"❹ \n",
")))) \n",
"[parity min odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❹ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❷ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" \n",
" "
],
"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",
"An automaton with a parity acceptance is not necessarily a parity automaton. It must be colored to be qualified like this.\n",
"## Parity max\n",
"Transitions with multiple acceptance sets are purified by keeping only the set with the greatest index.\n",
"\n",
"\n",
"G \n",
"\n",
"Inf( \n",
"❸ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❶ \n",
") | Fin( \n",
"⓿ \n",
"))) \n",
"[parity max odd 4] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"⓿ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
"❷ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Inf( \n",
"❹ \n",
") | (Fin( \n",
"❸ \n",
") & (Inf( \n",
"❷ \n",
") | (Fin( \n",
"❶ \n",
") & Inf( \n",
"⓿ \n",
")))) \n",
"[parity max even 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❶ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❸ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"⓿ \n",
" \n",
" "
],
"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",
"\n",
"G \n",
"\n",
"Inf( \n",
"❺ \n",
") | (Fin( \n",
"❹ \n",
") & (Inf( \n",
"❸ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❶ \n",
") | Fin( \n",
"⓿ \n",
"))))) \n",
"[parity max odd 6] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❶ \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❶ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❶ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❶ \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"❷ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❶ \n",
" \n",
" "
],
"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",
"\n",
"G \n",
"\n",
"Fin( \n",
"⓿ \n",
") & (Inf( \n",
"❶ \n",
") | (Fin( \n",
"❷ \n",
") & Inf( \n",
"❸ \n",
"))) \n",
"[parity min odd 4] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"⓿ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
"❷ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
" \n",
" "
],
"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": {
"collapsed": false
},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"G \n",
"\n",
"Fin( \n",
"⓿ \n",
") & (Inf( \n",
"❶ \n",
") | (Fin( \n",
"❷ \n",
") & (Inf( \n",
"❸ \n",
") | Fin( \n",
"❹ \n",
")))) \n",
"[parity min odd 5] \n",
"\n",
"\n",
"0 \n",
"\n",
"0 \n",
" I->0 \n",
"\n",
"\n",
" 2 \n",
"\n",
"2 \n",
" 0->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 3 \n",
"\n",
"3 \n",
" 0->3 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 1 \n",
"\n",
"1 \n",
" 2->1 \n",
"\n",
"\n",
"!p0 & p1 \n",
"❹ \n",
" 3->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" 3->3 \n",
"\n",
"\n",
"p0 & !p1 \n",
"⓿ \n",
" 1->0 \n",
"\n",
"\n",
"!p0 & p1 \n",
"⓿ \n",
" 1->2 \n",
"\n",
"\n",
"!p0 & !p1 \n",
"❹ \n",
" \n",
" "
],
"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.5.4"
}
},
"nbformat": 4,
"nbformat_minor": 2
}