From 27982fb80fbf8d4bfb457fb206b2e213167430c0 Mon Sep 17 00:00:00 2001 From: Laurent XU Date: Wed, 1 Jun 2016 14:14:13 +0200 Subject: [PATCH] parity: add spot::change_parity() This function changes the parity acceptance of an automaton. * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here * python/spot/impl.i: Add spot/twaalgos/parity.hh * spot/twaalgos/Makefile.am: Add spot/twaalgos/parity.{cc,hh} * tests/core/parity.cc, tests/core/parity.test: Add spot::change_parity() tests * tests/python/parity.ipynb: Add documentation about spot::change_parity() * tests/Makefile.am: Add tests/core/parity.{cc,hh} and tests/python/parity.ipynb * doc/org/tut.org: Add the html page of tests/python/parity.ipynb --- doc/org/tut.org | 2 + python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/parity.cc | 149 +++++ spot/twaalgos/parity.hh | 91 +++ tests/Makefile.am | 6 +- tests/core/parity.cc | 329 ++++++++++ tests/core/parity.test | 25 + tests/python/parity.ipynb | 1311 +++++++++++++++++++++++++++++++++++++ 9 files changed, 1916 insertions(+), 1 deletion(-) create mode 100644 spot/twaalgos/parity.cc create mode 100644 spot/twaalgos/parity.hh create mode 100644 tests/core/parity.cc create mode 100755 tests/core/parity.test create mode 100644 tests/python/parity.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index 706b08c00..208c09c90 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -66,6 +66,8 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/accparse.html][=accparse.ipynb=]] exercises the acceptance condition parser - [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][=acc_cond.ipynb=]] documents the interface for manipulating acceptance conditions +- [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata + in Python - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata in Python - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] diff --git a/python/spot/impl.i b/python/spot/impl.i index 6aa6178a4..4589d114b 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -151,6 +151,7 @@ #include #include #include +#include #include #include #include @@ -582,6 +583,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 133327fa1..e64bb9d11 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -62,6 +62,7 @@ twaalgos_HEADERS = \ minimize.hh \ couvreurnew.hh \ neverclaim.hh \ + parity.hh \ postproc.hh \ powerset.hh \ product.hh \ @@ -125,6 +126,7 @@ libtwaalgos_la_SOURCES = \ couvreurnew.cc \ ndfs_result.hxx \ neverclaim.cc \ + parity.cc \ postproc.cc \ powerset.cc \ product.cc \ diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc new file mode 100644 index 000000000..43f48a9a3 --- /dev/null +++ b/spot/twaalgos/parity.cc @@ -0,0 +1,149 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + unsigned change_set(unsigned x, unsigned num_sets, + bool change_kind, bool change_style) + { + // If the parity acceptance kind is changed, + // then the index of the sets are reversed + if (change_kind) + x = num_sets - x - 1; + // If the parity style is changed, then all the existing acceptance + // sets are shifted + x += change_style; + return x; + } + + void + change_acc(twa_graph_ptr& aut, unsigned num_sets, bool change_kind, + bool change_style, bool output_max, bool input_max) + { + for (auto& e: aut->edge_vector()) + if (e.acc) + { + unsigned msb = (input_max ? e.acc.max_set() : e.acc.min_set()) - 1; + e.acc = acc_cond::mark_t{change_set(msb, num_sets, change_kind, + change_style)}; + } + else if (output_max && change_style) + { + // If the parity is changed, a new set is introduced. + // This new set is used to mark all the transitions of the input + // that don't belong to any acceptance sets. + e.acc.set(0); + } + } + } + + twa_graph_ptr + change_parity(const const_twa_graph_ptr& aut, + parity_kind kind, parity_style style) + { + return change_parity_here(make_twa_graph(aut, twa::prop_set::all()), + kind, style); + } + + twa_graph_ptr + change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style) + { + bool current_max; + bool current_odd; + if (!aut->acc().is_parity(current_max, current_odd, true)) + throw new std::invalid_argument("change_parity: input must have a parity " + "acceptance."); + auto old_num_sets = aut->num_sets(); + + bool output_max = true; + switch (kind) + { + case parity_kind_max: + output_max = true; + break; + case parity_kind_min: + output_max = false; + break; + case parity_kind_same: + output_max = current_max; + break; + case parity_kind_any: + // If we need to change the style we may change the kind not to + // introduce new accset. + output_max = (((style == parity_style_odd && !current_odd) + || (style == parity_style_even && current_odd)) + && old_num_sets % 2 == 0) != current_max; + break; + } + + bool change_kind = current_max != output_max; + bool toggle_style = change_kind && (old_num_sets % 2 == 0); + + bool output_odd = true; + switch (style) + { + case parity_style_odd: + output_odd = true; + break; + case parity_style_even: + output_odd = false; + break; + case parity_style_same: + output_odd = current_odd; + break; + case parity_style_any: + output_odd = current_odd != toggle_style; + // If we need to change the kind we may change the style not to + // introduce new accset. + break; + } + + current_odd = current_odd != toggle_style; + bool change_style = false; + auto num_sets = old_num_sets; + // If the parity neeeds to be changed, then a new acceptance set is created. + // The old acceptance sets are shifted + if (output_odd != current_odd) + { + change_style = true; + ++num_sets; + } + + if (change_kind || change_style) + { + auto new_acc = acc_cond::acc_code::parity(output_max, + output_odd, num_sets); + aut->set_acceptance(num_sets, new_acc); + } + change_acc(aut, old_num_sets, change_kind, + change_style, output_max, current_max); + return aut; + } +} diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh new file mode 100644 index 000000000..385805d2d --- /dev/null +++ b/spot/twaalgos/parity.hh @@ -0,0 +1,91 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include +#include + +namespace spot +{ + /// \addtogroup parity_algorithms Parity algorithms + /// \ingroup twa_algorithms + /// @{ + /// \brief Parity kind type + enum parity_kind + { + /// The new acceptance will be a parity max + parity_kind_max, + /// The new acceptance will be a parity min + parity_kind_min, + /// The new acceptance will keep the kind + parity_kind_same, + /// The new acceptance may change the kind + parity_kind_any + }; + + /// \brief Parity style type + enum parity_style + { + /// The new acceptance will be a parity odd + parity_style_odd, + /// The new acceptance will be a parity even + parity_style_even, + /// The new acceptance will keep the style + parity_style_same, + /// The new acceptance may change the style + parity_style_any + }; + + /// \brief Change the parity acceptance of an automaton + /// + /// The parity acceptance condition of an automaton is characterized by + /// - The kind of the acceptance (min or max). + /// - The parity style, i.e., parity of the sets seen infinitely often + /// (odd or even). + /// - The number of acceptance sets. + /// + /// The output will be an equivalent automaton with the new parity acceptance. + /// The number of acceptance sets may be increased by one. Every transition + /// will belong to at most one acceptance set. The automaton must have a + /// parity acceptance, otherwise an invalid_argument exception is thrown. + /// + /// The parity kind is defined only if the number of acceptance sets + /// is strictly greater than 1. The parity_style is defined only if the number + /// of acceptance sets is non-zero. Some values of kind and style may result + /// in equivalent outputs if the number of acceptance sets of the input + /// automaton is not great enough. + /// + /// \param aut the input automaton + /// + /// \param kind the parity kind of the output automaton + /// + /// \param style the parity style of the output automaton + /// + /// \return the automaton with the new acceptance + /// @{ + SPOT_API twa_graph_ptr + change_parity(const const_twa_graph_ptr& aut, + parity_kind kind, parity_style style); + + SPOT_API twa_graph_ptr + change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style); + /// @} + /// @} +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 9122d38cb..a33a66917 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -82,6 +82,7 @@ check_PROGRAMS = \ core/nequals \ core/nenoform \ core/ngraph \ + core/parity \ core/randtgba \ core/readsat \ core/reduc \ @@ -128,6 +129,7 @@ core_nenoform_SOURCES = core/equalsf.cc core_nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM core_nequals_SOURCES = core/equalsf.cc core_nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE +core_parity_SOURCES = core/parity.cc core_reduc_SOURCES = core/reduc.cc core_reduccmp_SOURCES = core/equalsf.cc core_reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC @@ -301,7 +303,8 @@ TESTS_twa = \ core/cycles.test \ core/acc_word.test \ core/dca.test \ - core/dnfstreett.test + core/dnfstreett.test \ + core/parity.test ############################## PYTHON ############################## @@ -324,6 +327,7 @@ TESTS_ipython = \ python/ltsmin-dve.ipynb \ python/ltsmin-pml.ipynb \ python/piperead.ipynb \ + python/parity.ipynb \ python/product.ipynb \ python/randaut.ipynb \ python/randltl.ipynb \ diff --git a/tests/core/parity.cc b/tests/core/parity.cc new file mode 100644 index 000000000..49193e3a1 --- /dev/null +++ b/tests/core/parity.cc @@ -0,0 +1,329 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#define LAST_AUT result.back().first +#define LAST_NUM_SETS result.back().second +#define NEW_AUT() do { \ + result.emplace_back(spot::random_graph(6, 0.5, &apf, \ + current_bdd, 0, 0, 0.5, true), 0); \ + LAST_NUM_SETS = 0; \ + /* print_hoa need this */ \ + LAST_AUT->prop_state_acc(spot::trival::maybe()); \ +} while (false) + +#define SET_TR(t, value) do { \ + unsigned value_tmp = value; \ + if (value_tmp + 1 > LAST_NUM_SETS) \ + LAST_NUM_SETS = value_tmp + 1; \ + t.acc.set(value_tmp); \ +} while (false) + + +static std::vector> +generate_aut(const spot::bdd_dict_ptr& current_bdd) +{ + spot::atomic_prop_set apf = spot::create_atomic_prop_set(3); + std::vector> result; + // No accset on any transition + NEW_AUT(); + // The same accset on every transitions + NEW_AUT(); + for (auto& t: LAST_AUT->edges()) + SET_TR(t, 0); + + // All used / First unused / Last unused / First and last unused + for (auto incr_ext: { 0, 1 }) + for (auto used: { 1, 2 }) + for (auto modulo: { 4, 5, 6 }) + if (incr_ext + modulo <= 6) + { + NEW_AUT(); + unsigned count = 0; + for (auto& t: LAST_AUT->edges()) + if (std::rand() % used == 0) + { + auto value = ++count % modulo + incr_ext; + SET_TR(t, value); + } + } + + // One-Three in middle not used + for (auto i: { 0, 1 }) + for (auto start: { 1, 2 }) + for (auto unused: { 1, 2, 3 }) + { + NEW_AUT(); + auto count = 0; + for (auto& t: LAST_AUT->edges()) + { + int val = 0; + if (count % (3 + i) < start) + val = count % (3 + i); + else + val = count % (3 + i) + unused; + SET_TR(t, val); + } + } + + // All accset on all transitions + for (auto i: { 0, 1 }) + { + NEW_AUT(); + for (auto& t: LAST_AUT->edges()) + for (auto acc = 0; acc < 5 + i; ++acc) + SET_TR(t, acc); + } + + // Some random automata + std::vector> cont_sets; + for (auto i = 0; i <= 6; ++i) + { + std::vector cont_set; + for (auto j = 0; j < i; ++j) + cont_set.push_back(j); + cont_sets.push_back(cont_set); + } + for (auto min: { 0, 1 }) + { + for (auto num_sets: { 1, 2, 5, 6 }) + for (auto i = 0; i < 10; ++i) + { + NEW_AUT(); + for (auto& t: LAST_AUT->edges()) + { + auto nb_acc = std::rand() % (num_sets - min + 1) + min; + std::random_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); + for (auto j = 0; j < nb_acc; ++j) + SET_TR(t, cont_sets[num_sets][j]); + } + } + for (auto num_sets: {2, 3}) + for (auto even: {0, 1}) + if ((num_sets - 1) * 2 + even < 6) + { + NEW_AUT(); + for (auto& t: LAST_AUT->edges()) + { + auto nb_acc = std::rand() % (num_sets - min + 1) + min; + std::random_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); + for (auto j = 0; j < nb_acc; ++j) + { + auto value = cont_sets[num_sets][j] * 2 + even; + SET_TR(t, value); + } + } + } + } + return result; +} + +static std::vector> +generate_acc() +{ + std::vector> + result; + for (auto max: { true, false }) + for (auto odd: { true, false }) + for (auto num_sets: { 0, 1, 2, 5, 6 }) + result.emplace_back(spot::acc_cond::acc_code::parity(max, odd, + num_sets), max, odd, num_sets); + return result; +} + +static bool is_included(spot::const_twa_graph_ptr left, + spot::const_twa_graph_ptr right, bool first_left) +{ + auto tmp = spot::dualize(right); + auto product = spot::product(left, tmp); + if (!product->is_empty()) + { + std::cerr << "======Not included======" << std::endl; + if (first_left) + std::cerr << "======First automaton======" << std::endl; + else + std::cerr << "======Second automaton======" << std::endl; + spot::print_hoa(std::cerr, left); + std::cerr << std::endl; + if (first_left) + std::cerr << "======Second automaton======" << std::endl; + else + std::cerr << "======First automaton======" << std::endl; + spot::print_hoa(std::cerr, right); + std::cerr << std::endl; + if (first_left) + std::cerr << "======!Second automaton======" << std::endl; + else + std::cerr << "======!First automaton======" << std::endl; + spot::print_hoa(std::cerr, tmp); + std::cerr << std::endl; + if (first_left) + std::cerr << "======First X !Second======" <acc().is_parity(is_max, is_odd)) + return false; + bool target_max; + bool target_odd; + if (aut->num_sets() <= 1 || num_sets <= 1 + || target_kind == spot::parity_kind_any) + target_max = is_max; + else if (target_kind == spot::parity_kind_max) + target_max = true; + else if (target_kind == spot::parity_kind_min) + target_max = false; + else + target_max = origin_max; + if (aut->num_sets() == 0 || num_sets == 0 + || target_style == spot::parity_style_any) + target_odd = is_odd; + else if (target_style == spot::parity_style_odd) + target_odd = true; + else if (target_style == spot::parity_style_even) + target_odd = false; + else + target_odd = origin_odd; + if (!(is_max == target_max && is_odd == target_odd)) + { + std::cerr << "======Wrong accceptance======" << std::endl; + std::string kind[] = { "max", "min", "same", "any" }; + std::string style[] = { "odd", "even", "same", "any" }; + std::cerr << "target: " << kind[target_kind] << ' ' + << style[target_style] << std::endl; + std::cerr << "origin: " << kind[origin_max ? 0 : 1] << ' ' + << style[origin_odd ? 0 : 1] << ' ' + << num_sets << std::endl; + std::cerr << "actually: " << kind[is_max ? 0 : 1] << ' ' + << style[is_odd ? 0 : 1] << ' ' + << aut->num_sets() << std::endl; + std::cerr << std::endl; + return false; + } + return true; +} + +static bool is_almost_colored(spot::const_twa_graph_ptr aut) +{ + for (auto t: aut->edges()) + if (t.acc.count() > 1) + { + std::cerr << "======Not colored======" << std::endl; + spot::print_hoa(std::cerr, aut); + std::cerr << std::endl; + return false; + } + return true; +} + +int main() +{ + auto current_bdd = spot::make_bdd_dict(); + spot::srand(0); + auto parity_kinds = + { + spot::parity_kind_max, + spot::parity_kind_min, + spot::parity_kind_same, + spot::parity_kind_any, + }; + auto parity_styles = + { + spot::parity_style_odd, + spot::parity_style_even, + spot::parity_style_same, + spot::parity_style_any, + }; + + auto acceptance_sets = generate_acc(); + auto automata_tuples = generate_aut(current_bdd); + + unsigned num_automata = automata_tuples.size(); + unsigned num_acceptance = acceptance_sets.size(); + + std::cerr << "num of automata: " << num_automata << '\n'; + std::cerr << "num of acceptance expression: " << num_acceptance << '\n'; + + for (auto acc_tuple: acceptance_sets) + for (auto& aut_tuple: automata_tuples) + { + auto& aut = aut_tuple.first; + auto aut_num_sets = aut_tuple.second; + + auto acc = std::get<0>(acc_tuple); + auto is_max = std::get<1>(acc_tuple); + auto is_odd = std::get<2>(acc_tuple); + auto acc_num_sets = std::get<3>(acc_tuple); + if (aut_num_sets <= acc_num_sets) + { + aut->set_acceptance(acc_num_sets, acc); + // Check change_parity + for (auto kind: parity_kinds) + for (auto style: parity_styles) + { + auto output = spot::change_parity(aut, kind, style); + assert(is_right_parity(output, kind, style, + is_max, is_odd, acc_num_sets) + && "change_parity: wrong acceptance."); + assert(are_equiv(aut, output) + && "change_parity: not equivalent."); + assert(is_almost_colored(output) + && "change_parity: too many acc on a transition"); + } + } + } + return 0; +} diff --git a/tests/core/parity.test b/tests/core/parity.test new file mode 100755 index 000000000..226022240 --- /dev/null +++ b/tests/core/parity.test @@ -0,0 +1,25 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs +set -e + +run 0 ../parity diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb new file mode 100644 index 000000000..a04270c08 --- /dev/null +++ b/tests/python/parity.ipynb @@ -0,0 +1,1311 @@ +{ + "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" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "from IPython.display import display\n", + "import spot\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "heading", + "level": 1, + "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", + "
\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": "heading", + "level": 1, + "metadata": {}, + "source": [ + "Change parity" + ] + }, + { + "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", + "collapsed": false, + "input": [ + "aut_max_odd5 = tuple(spot.automata(\"randaut -A 'parity max odd 5' -Q4 2|\"))[0]\n", + "display(aut_max_odd5.show(\".a\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2779\n", + ") & (Inf(\n", + "\u2778\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2776\n", + ") | Fin(\n", + "\u24ff\n", + "))))\n", + "[parity max odd 5]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2779\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2779\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 2 + }, + { + "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", + "+ \u2205 -> 0" + ] + }, + { + "cell_type": "heading", + "level": 4, + "metadata": {}, + "source": [ + "Result of Parity max odd 5 -> Parity max even 6" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u277a\n", + ") & (Inf(\n", + "\u2779\n", + ") | (Fin(\n", + "\u2778\n", + ") & (Inf(\n", + "\u2777\n", + ") | (Fin(\n", + "\u2776\n", + ") & Inf(\n", + "\u24ff\n", + ")))))\n", + "[parity max even 6]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u277a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u277a\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2779\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 3 + }, + { + "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", + "collapsed": false, + "input": [ + "aut_min_odd5 = tuple(spot.automata(\"randaut -A 'parity min odd 5' -Q4 2|\"))[0]\n", + "display(aut_min_odd5.show(\".a\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ") & (Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2778\n", + ") | Fin(\n", + "\u2779\n", + "))))\n", + "[parity min odd 5]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2779\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2779\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 4 + }, + { + "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", + "+ \u2205 -> \u2205" + ] + }, + { + "cell_type": "heading", + "level": 4, + "metadata": {}, + "source": [ + "Result of Parity min odd 5 -> Parity min even 6" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | (Fin(\n", + "\u2776\n", + ") & (Inf(\n", + "\u2777\n", + ") | (Fin(\n", + "\u2778\n", + ") & (Inf(\n", + "\u2779\n", + ") | Fin(\n", + "\u277a\n", + ")))))\n", + "[parity min even 6]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u277a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2777\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u277a\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2779\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 5 + }, + { + "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", + "collapsed": false, + "input": [ + "aut_max_odd5 = tuple(spot.automata(\"randaut -A 'parity max odd 5' -Q4 2|\"))[0]\n", + "display(aut_max_odd5.show(\".a\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u2779\n", + ") & (Inf(\n", + "\u2778\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2776\n", + ") | Fin(\n", + "\u24ff\n", + "))))\n", + "[parity max odd 5]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u2779\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2779\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2778\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 6 + }, + { + "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", + "+ \u2205 -> \u2205" + ] + }, + { + "cell_type": "heading", + "level": 4, + "metadata": {}, + "source": [ + "Result of Parity max odd 5 ----> Parity min odd 5:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ") & (Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2778\n", + ") | Fin(\n", + "\u2779\n", + "))))\n", + "[parity min odd 5]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "heading", + "level": 4, + "metadata": {}, + "source": [ + "Parity max odd 4 ----> Parity min odd:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut_max_odd4 = tuple(spot.automata(\"randaut -A 'parity max odd 4' -Q4 2|\"))[0]\n", + "display(aut_max_odd4.show(\".a\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2778\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2776\n", + ") | Fin(\n", + "\u24ff\n", + ")))\n", + "[parity max odd 4]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 8 + }, + { + "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", + "+ \u2205 -> \u2205" + ] + }, + { + "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", + "collapsed": false, + "input": [ + "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\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | (Fin(\n", + "\u2776\n", + ") & (Inf(\n", + "\u2777\n", + ") | Fin(\n", + "\u2778\n", + ")))\n", + "[parity min even 4]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2778\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 9 + }, + { + "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", + "+ \u2205 -> \u2205 -> 0 (as the resulting automaton is a parity min)" + ] + }, + { + "cell_type": "heading", + "level": 4, + "metadata": {}, + "source": [ + "Result of Parity max odd 4 ----> Parity min even 5:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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\"))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ") & (Inf(\n", + "\u2776\n", + ") | (Fin(\n", + "\u2777\n", + ") & (Inf(\n", + "\u2778\n", + ") | Fin(\n", + "\u2779\n", + "))))\n", + "[parity min odd 5]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "p0 & !p1\n", + "\u2779\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\u2777\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 10 + } + ], + "metadata": {} + } + ] +}