From fd073d1df9efa647bc617caf95ce6b9bd84c3f44 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Apr 2019 14:41:03 +0200 Subject: [PATCH] tests: fix some examples MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by FrantiĊĦek Blahoudek. * tests/python/parity.ipynb: Fix examples and improve some text. --- tests/python/parity.ipynb | 118 +++++++++++++++++--------------------- 1 file changed, 54 insertions(+), 64 deletions(-) diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb index 2b860dd45..efd19e0f7 100644 --- a/tests/python/parity.ipynb +++ b/tests/python/parity.ipynb @@ -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" + " \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": [ - "**Some parity acceptance examples:**\n", - "
\n", - "**numsets = 1:** \n", - "
\n", + "# Change parity\n", "\n", - "| | **max** | **min** |\n", - "|:---------:|:--------------:|:--------------:|\n", - "| **odd** | Fin(1) | Fin(1) | \n", - "| **even** | Inf(0) | Inf(0) |\n", - "\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", - "
\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", - "
\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", - "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" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Change parity" + "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", "
\n", @@ -2093,7 +2083,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.7.3" } }, "nbformat": 4,