From 0f131f2eee8e71113c6298016d94aba1e540f21b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 6 Sep 2022 18:05:52 +0200 Subject: [PATCH] =?UTF-8?q?product:=20B=C3=BCchi|B=C3=BCchi=3DB=C3=BCchi,?= =?UTF-8?q?=20CoB=C3=BCchi&CoB=C3=BCchi=3DCoB=C3=BCchi?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Improve the construction of the above constructions, saving colors. * spot/twaalgos/product.cc: Here. * spot/twaalgos/product.hh, NEWS: Mention it. * tests/core/prodchain.test, tests/core/prodor.test, tests/python/_product_weak.ipynb: Adjust. --- NEWS | 6 +- spot/twaalgos/product.cc | 22 +- spot/twaalgos/product.hh | 43 +- tests/core/prodchain.test | 42 +- tests/core/prodor.test | 8 +- tests/python/_product_weak.ipynb | 8468 ++++++++++++++++++++++-------- 6 files changed, 6449 insertions(+), 2140 deletions(-) diff --git a/NEWS b/NEWS index 5b55ebbdd..66f56e75d 100644 --- a/NEWS +++ b/NEWS @@ -114,10 +114,14 @@ New in spot 2.10.6.dev (not yet released) to obtain a simple model checker (that returns true or false, without counterexample). + - product() learned that the product of two co-Büchi automata + is a co-Büchi automaton. And product_or() learned that the + "or"-product of two Büchi automata is a Büchi automaton. + - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only - twa_graph::merge_states() support it. + twa_graph::merge_states() supports it. Python bindings: diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 7fb70ddd6..243f3768c 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2020, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -122,8 +122,23 @@ namespace spot res->copy_ap_of(left); res->copy_ap_of(right); + auto& lacc = left->acc(); + auto& racc = right->acc(); + bool leftweak = left->prop_weak().is_true(); bool rightweak = right->prop_weak().is_true(); + + // The conjunction of two co-Büchi automata is a co-Büchi automaton. + // The disjunction of two Büchi automata is a Büchi automaton. + // + // The code to handle this case is similar to the weak_weak case, + // except we do not set the weak property on the result. + if (!leftweak + && !rightweak + && ((aop == and_acc && lacc.is_co_buchi() && racc.is_co_buchi()) + || (aop == or_acc && lacc.is_buchi() && racc.is_buchi()))) + goto and_cobuchi_or_buchi; + // We have optimization to the standard product in case one // of the arguments is weak. if (leftweak || rightweak) @@ -132,14 +147,13 @@ namespace spot // t, f, Büchi or co-Büchi. We use co-Büchi only when // t and f cannot be used, and both acceptance conditions // are in {t,f,co-Büchi}. - if (leftweak && rightweak) + if ((leftweak && rightweak)) { weak_weak: res->prop_weak(true); + and_cobuchi_or_buchi: acc_cond::mark_t accmark = {0}; acc_cond::mark_t rejmark = {}; - auto& lacc = left->acc(); - auto& racc = right->acc(); if ((lacc.is_co_buchi() && (racc.is_co_buchi() || racc.num_sets() == 0)) || (lacc.num_sets() == 0 && racc.is_co_buchi())) diff --git a/spot/twaalgos/product.hh b/spot/twaalgos/product.hh index 49ee9acdf..784a3cb49 100644 --- a/spot/twaalgos/product.hh +++ b/spot/twaalgos/product.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2015, 2018-2020 Laboratoire de Recherche et +// Copyright (C) 2014-2015, 2018-2020, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -37,10 +37,14 @@ namespace spot /// The resulting automaton will accept the intersection of both /// languages and have an acceptance condition that is the /// conjunction of the acceptance conditions of the two input - /// automata. In case one of the left or right automaton is weak, - /// the acceptance condition of the result is made simpler: it - /// usually is the acceptance condition of the other argument, + /// automata. + /// + /// As an optionmization, in case one of the left or right automaton + /// is weak, the acceptance condition of the result is made simpler: + /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. + /// Similarly, the product of two co-Büchi automata will be a + /// co-Büchi automaton. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -64,10 +68,14 @@ namespace spot /// languages recognized by each input automaton (with its initial /// state changed) and have an acceptance condition that is the /// conjunction of the acceptance conditions of the two input - /// automata. In case one of the left or right automaton is weak, - /// the acceptance condition of the result is made simpler: it - /// usually is the acceptance condition of the other argument, + /// automata. + /// + /// As an optionmization, in case one of the left or right automaton + /// is weak, the acceptance condition of the result is made simpler: + /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. + /// Similarly, the product of two co-Büchi automata will be a + /// co-Büchi automaton. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -89,10 +97,15 @@ namespace spot /// The resulting automaton will accept the union of both /// languages and have an acceptance condition that is the /// disjunction of the acceptance conditions of the two input - /// automata. In case one of the left or right automaton is weak, - /// the acceptance condition of the result is made simpler: it - /// usually is the acceptance condition of the other argument, + /// automata. + /// + /// As an optionmization, in case one of the left or right automaton + /// is weak, the acceptance condition of the result is made simpler: + /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. + /// Similarly, the product_pr of two Büchi automata will be a + /// Büchi automaton. + /// /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -112,10 +125,14 @@ namespace spot /// recognized by each input automaton (with its initial state /// changed) and have an acceptance condition that is the /// disjunction of the acceptance conditions of the two input - /// automata. In case one of the left or right automaton is weak, - /// the acceptance condition of the result is made simpler: it - /// usually is the acceptance condition of the other argument, + /// automata. + /// + /// As an optionmization, in case one of the left or right automaton + /// is weak, the acceptance condition of the result is made simpler: + /// it usually is the acceptance condition of the other argument, /// therefore avoiding the need to introduce new accepting sets. + /// Similarly, the product_pr of two Büchi automata will be a + /// Büchi automaton. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test index e00422148..9a9c74648 100755 --- a/tests/core/prodchain.test +++ b/tests/core/prodchain.test @@ -32,12 +32,12 @@ for i in *.hoa; do shift done shift -if $MAX_ACCSETS -eq 32; then +if [ $MAX_ACCSETS -eq 32 ]; then autfilt "$@" 2> error && exit 1 grep 'Too many acceptance sets used' error fi -autfilt -B "$@" > result -test "127,253,508,1" = `autfilt --stats=%s,%e,%t,%a result` +autfilt -B --low "$@" > result +test "4,7,16,1" = `autfilt --stats=%s,%e,%t,%a result` set x shift @@ -46,9 +46,37 @@ for i in *.hoa; do shift done shift -if $MAX_ACCSETS -eq 32; then - autfilt "$@" 2> error && exit 1 +autfilt -B --low "$@" > result +test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result` + + +set x +shift +for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ + 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do + ltl2tgba -D --cobuchi -S "{a[*$i]}<>->FGb" > $i.hoa +done +for i in *.hoa; do + set x "$@" --product $i + shift +done +shift +autfilt -D --cobuchi --low -S "$@" > result +test "85,170,174,1" = `autfilt --stats=%s,%e,%t,%a result` + +set x +shift +for i in *.hoa; do + set x "$@" --product-or $i + shift +done +shift +if [ $MAX_ACCSETS -eq 32 ]; then + autfilt --cobuchi -S "$@" 2> error && exit 1 grep 'Too many acceptance sets used' error fi -autfilt -B "$@" > result -test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result` +# FIXME: implement degeneralization for generalized-co-Büchi +# autfilt --cobuchi --low -S "$@" > result +# test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result` + +true diff --git a/tests/core/prodor.test b/tests/core/prodor.test index 03127508b..03d8cd458 100755 --- a/tests/core/prodor.test +++ b/tests/core/prodor.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018, 2021 Laboratoire de Recherche et +# Copyright (C) 2015, 2017-2018, 2021-2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -154,8 +154,8 @@ diff por.hoa exp ltl2tgba -BDH 'GFa' > gfa.hoa ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa -autfilt --product-or gfa.hoa xb.hoa -H > por.hoa -cat por.hoa +autfilt --product-or gfa.hoa xb.hoa -H > por2.hoa +cat por2.hoa cat >exp <\n" ], "text/plain": [ - " *' at 0x7fd90c347ba0> >" + " *' at 0x7f26743d3720> >" ] }, "metadata": {}, @@ -299,11 +313,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -379,12 +393,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -434,11 +448,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -508,11 +522,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -644,12 +658,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -699,11 +713,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -774,11 +788,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1127,6 +1141,226 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -1586,7 +1820,7 @@ "# In a previous version we used to iterate over all possible left automata with \"for left in auts:\"\n", "# however we had trouble with Jupyter on i386, where running the full loop abort with some low-level \n", "# exeptions from Jupyter client. Halving the loop helped for some times, but then the timeout\n", - "# came back. So we do one left automaton at at time.\n", + "# came back. So we do one left automaton at a time.\n", "left = auts[0]\n", "display(left)\n", "for right in auts:\n", @@ -1609,12 +1843,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1660,7 +1894,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347bd0> >" + " *' at 0x7f26743d36c0> >" ] }, "metadata": {}, @@ -1723,11 +1957,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1797,11 +2031,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1933,12 +2167,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1988,11 +2222,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2042,11 +2276,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2108,12 +2342,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -2163,11 +2397,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2217,11 +2451,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2490,6 +2724,224 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -2949,12 +3401,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3000,7 +3452,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347cf0> >" + " *' at 0x7f26743d37e0> >" ] }, "metadata": {}, @@ -3063,11 +3515,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3138,11 +3590,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3274,12 +3726,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3329,11 +3781,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3383,11 +3835,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3449,12 +3901,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3504,11 +3956,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3558,11 +4010,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3831,6 +4283,224 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -4331,7 +5001,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347d50> >" + " *' at 0x7f26743d3870> >" ] }, "metadata": {}, @@ -4575,12 +5245,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -4801,12 +5471,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -5119,44 +5789,192 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Inf(\n", - "\n", - ")\n", - "[Fin-less 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[gen. Streett 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", "\n", "\n", "\n", @@ -5559,6 +6377,1431 @@ "metadata": { "scrolled": false }, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f26743d3900> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "a\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "GFc\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") | Inf(\n", + "\n", + ")\n", + "[Streett 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")|Fin(\n", + "\n", + ")\n", + "[gen. co-Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[Streett-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ")|Fin(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "left = auts[4]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": { + "scrolled": false + }, "outputs": [ { "data": { @@ -5611,7 +7854,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347d80> >" + " *' at 0x7f26743d3990> >" ] }, "metadata": {}, @@ -5856,12 +8099,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -6082,12 +8325,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -6486,6 +8729,193 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | Fin(\n", + "\n", + ")\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -6807,1266 +9237,6 @@ "output_type": "display_data" } ], - "source": [ - "left = auts[4]\n", - "display(left)\n", - "for right in auts:\n", - " display_inline(right, spot.product(left, right), spot.product_or(left, right))" - ] - }, - { - "cell_type": "code", - "execution_count": 9, - "metadata": { - "scrolled": false - }, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fd90c347e40> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "0,2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & !d\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ")\n", - "[Streett-like 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ") | Inf(\n", - "\n", - ")\n", - "[Rabin-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Streett-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ") | (Inf(\n", - "\n", - ") & Fin(\n", - "\n", - "))\n", - "[Rabin-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[Streett-like 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ")|Fin(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", - "[Rabin-like 4]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], "source": [ "left = auts[5]\n", "display(left)\n", @@ -8134,7 +9304,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347ba0> >" + " *' at 0x7f26743d3720> >" ] }, "metadata": {}, @@ -8197,11 +9367,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8263,11 +9433,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8344,12 +9514,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8399,11 +9569,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8522,11 +9692,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8656,12 +9826,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -8711,11 +9881,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8834,11 +10004,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -9241,6 +10411,288 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -9785,12 +11237,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -9836,7 +11288,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347bd0> >" + " *' at 0x7f26743d36c0> >" ] }, "metadata": {}, @@ -9899,11 +11351,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10022,11 +11474,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10156,12 +11608,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10211,11 +11663,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10264,11 +11716,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10331,12 +11783,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -10386,11 +11838,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10439,11 +11891,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10729,6 +12181,238 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -11189,12 +12873,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -11240,7 +12924,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347cf0> >" + " *' at 0x7f26743d37e0> >" ] }, "metadata": {}, @@ -11303,11 +12987,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -11426,11 +13110,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -11560,12 +13244,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -11615,11 +13299,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -11668,11 +13352,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -11735,12 +13419,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -11790,11 +13474,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -11845,11 +13529,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -12137,6 +13821,242 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -12638,7 +14558,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347d50> >" + " *' at 0x7f26743d3870> >" ] }, "metadata": {}, @@ -12938,12 +14858,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -13180,12 +15100,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -13575,6 +15495,164 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -13985,6 +16063,1562 @@ "metadata": { "scrolled": false }, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f26743d3900> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "a\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "GFc\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & (Fin(\n", + "\n", + ") | Inf(\n", + "\n", + "))) | ((Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & (Fin(\n", + "\n", + ") | Inf(\n", + "\n", + ")))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))) | ((Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "left = auts[4]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product_xor(left, right), spot.product_xnor(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": { + "scrolled": false + }, "outputs": [ { "data": { @@ -14037,7 +17671,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347d80> >" + " *' at 0x7f26743d3990> >" ] }, "metadata": {}, @@ -14314,12 +17948,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -14541,12 +18175,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -14956,6 +18590,203 @@ "metadata": {}, "output_type": "display_data" }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "((Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + ")) | ((Fin(\n", + "\n", + ") | Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | ((Fin(\n", + "\n", + ") | Inf(\n", + "\n", + ")) & Inf(\n", + "\n", + "))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "data": { "text/html": [ @@ -15306,7 +19137,7 @@ } ], "source": [ - "left = auts[4]\n", + "left = auts[5]\n", "display(left)\n", "for right in auts:\n", " display_inline(right, spot.product_xor(left, right), spot.product_xnor(left, right))" @@ -15314,7 +19145,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": { "scrolled": false }, @@ -15370,7 +19201,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd90c347e40> >" + " *' at 0x7f26743d3a20> >" ] }, "metadata": {}, @@ -15433,46 +19264,115 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & !d\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & d\n", + "\n", + "\n", + "a & d\n", "\n", "\n", "\n", @@ -15483,30 +19383,30 @@ "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & !d\n", + "\n", + "\n", + "!a & !d\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & d\n", + "\n", + "\n", + "!a & d\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -15521,111 +19421,7 @@ "2->2\n", "\n", "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "0,2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "d\n", + "d\n", "\n", "\n", "\n", @@ -15647,12 +19443,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -15702,87 +19498,6 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", "\n", "\n", @@ -15856,6 +19571,87 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -15874,12 +19670,12 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "Fb\n", - "\n", - "[co-Büchi]\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -15929,87 +19725,6 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", "\n", "\n", @@ -16083,6 +19798,87 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -16146,67 +19942,62 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Fin(\n", - "\n", - ")) | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")))\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & Inf(\n", + "\n", + ")\n", + "[Streett-like 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", + "\n", + "\n", + "!c & !d\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "\n", + "c & d\n", + "\n", "\n", "\n", "\n", @@ -16216,67 +20007,249 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ")) | (Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ") & Fin(\n", - "\n", - "))\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ") | Inf(\n", + "\n", + ")\n", + "[Rabin-like 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", + "\n", + "\n", + "!c & !d\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "FGd\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & Fin(\n", + "\n", + ")\n", + "[Streett-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ")|Fin(\n", + "\n", + "))\n", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", @@ -16344,55 +20317,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & (Fin(\n", - "\n", - ") | Inf(\n", - "\n", - "))) | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) & Fin(\n", - "\n", - "))\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -16402,55 +20368,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ") & (Fin(\n", - "\n", - ") | Inf(\n", - "\n", - ")))\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ") | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -16518,55 +20477,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")) | (Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[Streett-like 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -16576,55 +20528,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "((Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))) | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) & Fin(\n", - "\n", - "))\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ")|Fin(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", + "[Rabin-like 4]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -16639,16 +20584,317 @@ } ], "source": [ - "left = auts[5]\n", + "left = auts[6]\n", "display(left)\n", "for right in auts:\n", - " display_inline(right, spot.product_xor(left, right), spot.product_xnor(left, right))" + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "a1 = spot.translate('GFa')\n", + "a2 = spot.translate('GFb')\n", + "display_inline(spot.product(a1,a2), spot.product_or(a1, a2))" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")|Fin(\n", + "\n", + ")\n", + "[gen. co-Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "a1 = spot.dualize(a1)\n", + "a2 = spot.dualize(a2)\n", + "display_inline(spot.product(a1,a2), spot.product_or(a1, a2))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -16662,7 +20908,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.3rc1" + "version": "3.10.6" } }, "nbformat": 4,