diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5f973ff66..716c63f4e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -287,6 +287,8 @@ publish-unstable:
raspbian:
stage: build
+ only:
+ - branches
tags:
- armv7
script:
diff --git a/NEWS b/NEWS
index 65118ba56..6c412dc49 100644
--- a/NEWS
+++ b/NEWS
@@ -1,8 +1,4 @@
-New in spot 2.8.1.dev (not yet released)
-
- Command-line tools:
-
- - ltl2tgba and ltldo learned a --negate option.
+New in spot 2.8.2.dev (not yet released)
Library:
@@ -34,12 +30,24 @@ New in spot 2.8.1.dev (not yet released)
variants of F[n:m] and G[n:m], but those four are only implemented
as syntactic sugar.
+New in spot 2.8.2 (2019-09-27)
+
+ Command-line tools:
+
+ - ltl2tgba and ltldo learned a --negate option.
+
Bugs fixed:
- Calling "autfilt --dualize" on an alternating automaton with
transition-based acceptance and universal initial states would
fail with "set_init_state() called with nonexisting state".
+ - The numbering of nodes in the AIGER output of ltlsynt was
+ architecture dependent.
+
+ - Various compilation issues. In particular, this release is the
+ first one that can be compiled (as pass tests) on a Raspberry PI.
+
New in spot 2.8.1 (2019-07-18)
Command-line tools:
diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 573569c7f..48018ccec 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -269,6 +269,10 @@ typedef void (*bdd2inthandler)(int,int);
typedef int (*bddsizehandler)(void);
typedef void (*bddfilehandler)(FILE *, int);
typedef void (*bddallsathandler)(signed char*, int);
+// The historical type of bddallsathandler is the following,
+// unfortunately the signedness of char* is implementation defined.
+// Now we have to support both for backward compatibility.
+typedef void (*bddallsathandler_old)(char*, int);
BUDDY_API bddinthandler bdd_error_hook(bddinthandler);
BUDDY_API bddgbchandler bdd_gbc_hook(bddgbchandler);
@@ -613,6 +617,7 @@ protected:
friend bdd bdd_fullsatone(const bdd &);
friend bdd bdd_satprefix(bdd &);
friend void bdd_allsat(const bdd &r, bddallsathandler handler);
+ friend void bdd_allsat(const bdd &r, bddallsathandler_old handler);
friend double bdd_satcount(const bdd &);
friend double bdd_satcountset(const bdd &, const bdd &);
friend double bdd_satcountln(const bdd &);
@@ -829,6 +834,10 @@ inline bdd bdd_satprefix(bdd &r)
inline void bdd_allsat(const bdd &r, bddallsathandler handler)
{ bdd_allsat(r.root, handler); }
+// backward compatibility for C++ users
+inline void bdd_allsat(const bdd &r, bddallsathandler_old handler)
+{ bdd_allsat(r.root, (bddallsathandler)handler); }
+
inline double bdd_satcount(const bdd &r)
{ return bdd_satcount(r.root); }
diff --git a/configure.ac b/configure.ac
index 79d7d6e08..407cda7c3 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
# along with this program. If not, see .
AC_PREREQ([2.63])
-AC_INIT([spot], [2.8.1.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.8.2.dev], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/setup.org b/doc/org/setup.org
index 03863dcd4..c70f965ac 100644
--- a/doc/org/setup.org
+++ b/doc/org/setup.org
@@ -1,11 +1,11 @@
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
#+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html
-#+MACRO: SPOTVERSION 2.8.1
-#+MACRO: LASTRELEASE 2.8.1
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.1.tar.gz][=spot-2.8.1.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-1/NEWS][summary of the changes]]
-#+MACRO: LASTDATE 2019-07-18
+#+MACRO: SPOTVERSION 2.8.2
+#+MACRO: LASTRELEASE 2.8.2
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.2.tar.gz][=spot-2.8.2.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-2/NEWS][summary of the changes]]
+#+MACRO: LASTDATE 2019-09-27
#+ATTR_HTML: :id spotlogo
[[file:spot2.svg]]
diff --git a/tests/python/_product_weak.ipynb b/tests/python/_product_weak.ipynb
index 5defa2ef4..7c31ec51a 100644
--- a/tests/python/_product_weak.ipynb
+++ b/tests/python/_product_weak.ipynb
@@ -24,7 +24,7 @@
"metadata": {},
"outputs": [],
"source": [
- "auts = [a for a in spot.automata(\"\"\"\n",
+ "auts = list(spot.automata(\"\"\"\n",
"HOA: v1\n",
"name: \"a\"\n",
"States: 2\n",
@@ -106,20 +106,40 @@
"[!0] 0 {0}\n",
"[0] 0\n",
"--END--\n",
- "\"\"\")]"
+ "\"\"\"))"
]
},
{
"cell_type": "code",
"execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "6"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "len(auts)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
"metadata": {
"scrolled": false
},
"outputs": [
{
"data": {
- "text/html": [
- "
\n",
+ "image/svg+xml": [
+ "\n",
"\n",
"\n",
+ "\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a \n",
+ " \n",
+ "\n",
+ "\n",
+ "2 \n",
+ "\n",
+ "2,2 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->2 \n",
+ " \n",
+ " \n",
+ "!a \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->2 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ " \n",
+ " \n",
"
"
],
"text/plain": [
@@ -279,54 +378,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -451,6 +502,130 @@
"\n",
"\n",
" \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2 \n",
+ "\n",
+ "\n",
+ "0,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->2 \n",
+ " \n",
+ " \n",
+ "a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "3 \n",
+ "\n",
+ "\n",
+ "2,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->3 \n",
+ " \n",
+ " \n",
+ "!a & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "4 \n",
+ "\n",
+ "2,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->4 \n",
+ " \n",
+ " \n",
+ "!a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->2 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "3->3 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "4->3 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "4->4 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ " \n",
+ " \n",
"
"
],
"text/plain": [
@@ -468,54 +643,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -641,6 +768,130 @@
"\n",
"\n",
" \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2 \n",
+ "\n",
+ "\n",
+ "0,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->2 \n",
+ " \n",
+ " \n",
+ "a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "3 \n",
+ "\n",
+ "\n",
+ "2,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->3 \n",
+ " \n",
+ " \n",
+ "!a & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "4 \n",
+ "\n",
+ "2,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->4 \n",
+ " \n",
+ " \n",
+ "!a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->2 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "3->3 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "4->3 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "4->4 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ " \n",
+ " \n",
"
"
],
"text/plain": [
@@ -658,54 +909,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -811,6478 +1014,6 @@
"\n",
"\n",
" \n",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "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",
- ") & 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",
- ") \n",
- "[Rabin-like 1] \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 & !d \n",
- "⓿ \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & 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",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "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",
- ") | 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",
- ") \n",
- "[Streett-like 1] \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 & !d \n",
- "⓿ \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & 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",
- "
"
- ],
- "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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & b \n",
- " \n",
- "\n",
- "\n",
- "2 \n",
- "\n",
- "1,0 \n",
- " \n",
- "\n",
- "\n",
- "0->2 \n",
- " \n",
- " \n",
- "a & !b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "2->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "2->2 \n",
- " \n",
- " \n",
- "!b \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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "0->0 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "0->0 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \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",
- "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",
- ") \n",
- "[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",
- "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",
- "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",
- " \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",
- ") & 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",
- ") \n",
- "[Rabin-like 1] \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 & !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",
- "
"
- ],
- "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",
- ") | 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",
- ") \n",
- "[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 & !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",
- "
"
- ],
- "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",
- "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",
- "[co-Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "\n",
- "1,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 & b \n",
- " \n",
- "\n",
- "\n",
- "2 \n",
- "\n",
- "\n",
- "1,0 \n",
- " \n",
- "\n",
- "\n",
- "0->2 \n",
- " \n",
- " \n",
- "a & !b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "2->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "2->2 \n",
- " \n",
- " \n",
- "!b \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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "0->0 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \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",
- "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",
- "[co-Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "0->0 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \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",
- "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",
- ") \n",
- "[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",
- "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",
- "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",
- " \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",
- ") & 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",
- ") \n",
- "[Rabin-like 1] \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 & !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",
- "
"
- ],
- "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",
- ") | 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",
- ") \n",
- "[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 & !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",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- }
- ],
- "source": [
- "autslen = len(auts)\n",
- "# We have trouble with Jupyter on i386, where running the full loop abort with some low-level \n",
- "# exeptions from Jupyter client. \n",
- "for left in auts[0:autslen//2]:\n",
- " for right in auts:\n",
- " display_inline(left, right, spot.product(left, right))"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 4,
- "metadata": {},
- "outputs": [
- {
- "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",
- "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 & !c \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & c \n",
- "⓿ \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "!c \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",
- "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",
- "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 & !c \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",
- "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",
- " \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",
- "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 & !c \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",
- "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",
- " \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",
- "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",
- ")&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",
- "!c \n",
- " \n",
- "\n",
- "\n",
- "0->0 \n",
- " \n",
- " \n",
- "c \n",
- "⓿ \n",
- "❶ \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",
- ") \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",
- ")&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",
- "0->0 \n",
- " \n",
- " \n",
- "!c & d \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",
- "
"
- ],
- "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",
- ") \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",
- ") & (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",
- "0->0 \n",
- " \n",
- " \n",
- "!c & d \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",
- "
"
- ],
- "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",
- "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",
- ") & Fin( \n",
- "⓿ \n",
- ") \n",
- "[Rabin-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",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & 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",
- "
"
- ],
- "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",
- "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",
- ") & Fin( \n",
- "⓿ \n",
- ") \n",
- "[Rabin-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",
- "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",
- "
"
- ],
- "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",
- "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",
- ") & Fin( \n",
- "⓿ \n",
- ") \n",
- "[Rabin-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",
- "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",
- "
"
- ],
- "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",
- "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",
- ")&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",
- "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",
- ") \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",
- ")&Inf( \n",
- "❶ \n",
- ")) & Fin( \n",
- "⓿ \n",
- ") & Fin( \n",
- "❶ \n",
- ") \n",
- "[Streett-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"
- },
- {
- "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",
- ") \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 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",
- "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",
- ") | 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",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & 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",
- "
"
- ],
- "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",
- "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",
- "
"
- ],
- "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",
- "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",
- "
"
- ],
- "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",
- "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",
- "
"
- ],
- "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",
- ") \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",
- "
"
- ],
- "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",
- ") \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",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- }
- ],
- "source": [
- "for left in auts[autslen//2:]:\n",
- " for right in auts:\n",
- " display_inline(left, right, spot.product(left, right))"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 5,
- "metadata": {},
- "outputs": [
- {
- "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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a \n",
- " \n",
- "\n",
- "\n",
- "2 \n",
- "\n",
- "2,2 \n",
- " \n",
- "\n",
- "\n",
- "0->2 \n",
- " \n",
- " \n",
- "!a \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "2->2 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- " \n",
- " \n",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & b \n",
- " \n",
- "\n",
- "\n",
- "2 \n",
- "\n",
- "\n",
- "0,1 \n",
- " \n",
- "\n",
- "\n",
- "0->2 \n",
- " \n",
- " \n",
- "a & !b \n",
- " \n",
- "\n",
- "\n",
- "3 \n",
- "\n",
- "\n",
- "2,0 \n",
- " \n",
- "\n",
- "\n",
- "0->3 \n",
- " \n",
- " \n",
- "!a & b \n",
- " \n",
- "\n",
- "\n",
- "4 \n",
- "\n",
- "2,1 \n",
- " \n",
- "\n",
- "\n",
- "0->4 \n",
- " \n",
- " \n",
- "!a & !b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "2->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "2->2 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "3->3 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "4->3 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "4->4 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- " \n",
- " \n",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "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",
- "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",
- "[Büchi] \n",
- "\n",
- "\n",
- "\n",
- "0 \n",
- "\n",
- "\n",
- "1,1 \n",
- " \n",
- "\n",
- "\n",
- "I->0 \n",
- " \n",
- " \n",
- " \n",
- "\n",
- "\n",
- "1 \n",
- "\n",
- "\n",
- "0,0 \n",
- " \n",
- "\n",
- "\n",
- "0->1 \n",
- " \n",
- " \n",
- "a & b \n",
- " \n",
- "\n",
- "\n",
- "2 \n",
- "\n",
- "\n",
- "0,1 \n",
- " \n",
- "\n",
- "\n",
- "0->2 \n",
- " \n",
- " \n",
- "a & !b \n",
- " \n",
- "\n",
- "\n",
- "3 \n",
- "\n",
- "\n",
- "2,0 \n",
- " \n",
- "\n",
- "\n",
- "0->3 \n",
- " \n",
- " \n",
- "!a & b \n",
- " \n",
- "\n",
- "\n",
- "4 \n",
- "\n",
- "2,1 \n",
- " \n",
- "\n",
- "\n",
- "0->4 \n",
- " \n",
- " \n",
- "!a & !b \n",
- " \n",
- "\n",
- "\n",
- "1->1 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "2->1 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "2->2 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- "\n",
- "\n",
- "3->3 \n",
- " \n",
- " \n",
- "1 \n",
- " \n",
- "\n",
- "\n",
- "4->3 \n",
- " \n",
- " \n",
- "b \n",
- " \n",
- "\n",
- "\n",
- "4->4 \n",
- " \n",
- " \n",
- "!b \n",
- " \n",
- " \n",
- " \n",
- "
"
- ],
- "text/plain": [
- ""
- ]
- },
- "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",
- "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",
@@ -7404,54 +1135,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -7499,6 +1182,73 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Rabin-like 1] \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 & !d \n",
+ "⓿ \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & 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",
@@ -7613,54 +1363,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -7708,6 +1410,73 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") | Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Streett-like 1] \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 & !d \n",
+ "⓿ \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & 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",
@@ -7810,11 +1579,29 @@
},
"metadata": {},
"output_type": "display_data"
- },
+ }
+ ],
+ "source": [
+ "autslen = len(auts)\n",
+ "# 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",
+ "left = auts[0]\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": 5,
+ "metadata": {},
+ "outputs": [
{
"data": {
- "text/html": [
- "\n",
+ "image/svg+xml": [
+ "\n",
"\n",
"\n",
"\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2 \n",
+ "\n",
+ "1,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->2 \n",
+ " \n",
+ " \n",
+ "a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->2 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -8113,53 +1985,52 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"\n",
- "\n",
- "\n",
+ "\n",
+ "\n",
"\n",
- "Fb \n",
- " \n",
- "[Büchi] \n",
+ " \n",
+ "[Büchi] \n",
"\n",
- "\n",
+ "\n",
"\n",
- "1 \n",
- "\n",
- "1 \n",
+ "0 \n",
+ "\n",
+ "1,1 \n",
" \n",
- "\n",
+ "\n",
"\n",
- "I->1 \n",
- " \n",
- " \n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "b \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",
+ "1 \n",
" \n",
" \n",
" \n",
@@ -8240,61 +2111,6 @@
"\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",
- "Fb \n",
- " \n",
"[co-Büchi] \n",
"\n",
"\n",
@@ -8393,6 +2209,60 @@
" \n",
"\n",
" \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ " \n",
+ " \n",
"
"
],
"text/plain": [
@@ -8410,61 +2280,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -8511,6 +2326,84 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") \n",
+ "[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",
+ "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",
+ "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",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -8603,61 +2496,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -8705,6 +2543,86 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Rabin-like 1] \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 & !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",
@@ -8795,61 +2713,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -8897,6 +2760,85 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") \n",
+ "[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 & !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",
@@ -8980,11 +2922,24 @@
},
"metadata": {},
"output_type": "display_data"
- },
+ }
+ ],
+ "source": [
+ "left = auts[1]\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": 6,
+ "metadata": {},
+ "outputs": [
{
"data": {
- "text/html": [
- "\n",
+ "image/svg+xml": [
+ "\n",
"\n",
"\n",
"\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[co-Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "\n",
+ "1,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 & b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2 \n",
+ "\n",
+ "\n",
+ "1,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->2 \n",
+ " \n",
+ " \n",
+ "a & !b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "2->2 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -9234,61 +3275,6 @@
"\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",
- "Fb \n",
- " \n",
"[Büchi] \n",
"\n",
"\n",
@@ -9387,6 +3373,60 @@
" \n",
"\n",
" \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "
\n",
+ "\n",
+ " \n",
+ "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ " \n",
+ " \n",
"
"
],
"text/plain": [
@@ -9459,61 +3499,60 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
+ "[co-Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ "0 \n",
+ "\n",
+ "\n",
+ "1,1 \n",
+ " \n",
+ "\n",
+ "\n",
+ "I->0 \n",
+ " \n",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1 \n",
+ "\n",
+ "0,0 \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "b \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "1 \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "\n",
+ "\n",
"\n",
"
\n",
@@ -9580,61 +3619,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -9681,6 +3665,84 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") \n",
+ "[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",
+ "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",
+ "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",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -9773,61 +3835,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -9875,6 +3882,86 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Rabin-like 1] \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 & !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",
@@ -9965,61 +4052,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -10067,6 +4099,85 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") \n",
+ "[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 & !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",
@@ -10153,22 +4264,21 @@
}
],
"source": [
- "for left in auts[0:autslen//2]:\n",
- " for right in auts:\n",
- " display_inline(left, right, spot.product_or(left, right))"
+ "left = auts[2]\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": 6,
- "metadata": {
- "scrolled": false
- },
+ "execution_count": 7,
+ "metadata": {},
"outputs": [
{
"data": {
- "text/html": [
- "\n",
+ "image/svg+xml": [
+ "\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 & !c \n",
+ " \n",
+ "\n",
+ "\n",
+ "0->1 \n",
+ " \n",
+ " \n",
+ "a & c \n",
+ "⓿ \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "!c \n",
+ " \n",
+ "\n",
+ "\n",
+ "1->1 \n",
+ " \n",
+ " \n",
+ "c \n",
+ "⓿ \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -10382,51 +4568,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -10483,6 +4624,84 @@
"\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 & !c \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",
+ "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",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -10575,51 +4794,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -10676,6 +4850,84 @@
"\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 & !c \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",
+ "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",
+ " \n",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -10813,43 +5065,45 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"\n",
- "\n",
- "\n",
- "\n",
- "GFc \n",
- " \n",
- "Inf( \n",
- "⓿ \n",
- ") \n",
- "[Büchi] \n",
+ "\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ")&Inf( \n",
+ "❶ \n",
+ ") \n",
+ "[gen. Büchi 2] \n",
"\n",
"\n",
"\n",
"0 \n",
- "\n",
- "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",
+ "c \n",
+ "⓿ \n",
+ "❶ \n",
" \n",
" \n",
" \n",
@@ -10917,51 +5171,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -11009,6 +5218,71 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "(Inf( \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",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!c & d \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",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -11085,51 +5359,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -11177,6 +5406,71 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \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",
+ "0->0 \n",
+ " \n",
+ " \n",
+ "!c & d \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",
+ " \n",
+ "\n",
+ "\n",
+ "\n",
"
\n",
"\n",
@@ -11244,11 +5538,24 @@
},
"metadata": {},
"output_type": "display_data"
- },
+ }
+ ],
+ "source": [
+ "left = auts[3]\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": 8,
+ "metadata": {},
+ "outputs": [
{
"data": {
- "text/html": [
- "\n",
+ "image/svg+xml": [
+ "\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,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",
+ "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",
@@ -11462,52 +5847,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -11564,6 +5903,86 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Rabin-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",
+ "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",
@@ -11654,52 +6073,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -11756,6 +6129,86 @@
"\n",
"\n",
+ "\n",
+ "\n",
+ " \n",
+ "Inf( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "⓿ \n",
+ ") \n",
+ "[Rabin-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",
+ "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",
@@ -11846,52 +6299,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -11944,6 +6351,71 @@
" \n",
"(Inf( \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",
+ "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",
@@ -12061,43 +6533,48 @@
"\n",
"\n",
- "\n",
- "\n",
- " \n",
- "Inf( \n",
- "⓿ \n",
- ") & Fin( \n",
- "⓿ \n",
- ") \n",
- "[Rabin-like 1] \n",
+ "\n",
+ "\n",
+ " \n",
+ "(Inf( \n",
+ "⓿ \n",
+ ")&Inf( \n",
+ "❶ \n",
+ ")) & Fin( \n",
+ "⓿ \n",
+ ") & Fin( \n",
+ "❶ \n",
+ ") \n",
+ "[Streett-like 4] \n",
"\n",
"\n",
"\n",
"0 \n",
- "\n",
- "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",
+ "!d \n",
+ "⓿ \n",
+ "❶ \n",
" \n",
"\n",
"\n",
"0->0 \n",
- " \n",
- " \n",
- "d \n",
+ " \n",
+ " \n",
+ "d \n",
" \n",
" \n",
" \n",
@@ -12170,52 +6647,6 @@
"\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",
@@ -12262,6 +6693,57 @@
"\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",
@@ -12315,11 +6797,24 @@
},
"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": {},
+ "outputs": [
{
"data": {
- "text/html": [
- "\n",
+ "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,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",
+ "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",
@@ -12530,52 +7103,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -12632,6 +7159,85 @@
"\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",
@@ -12724,52 +7330,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -12826,6 +7386,85 @@
"\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",
@@ -12918,52 +7557,6 @@
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\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",
@@ -13010,6 +7603,71 @@
"\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",
@@ -13087,52 +7745,6 @@
"\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",
@@ -13179,6 +7791,57 @@
"\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",
@@ -13288,43 +7951,48 @@
"\n",
"\n",
- "\n",
- "\n",
- " \n",
- "Inf( \n",
- "⓿ \n",
- ") | Fin( \n",
- "⓿ \n",
- ") \n",
- "[Streett-like 1] \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 \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",
+ "!d \n",
+ "⓿ \n",
+ "❶ \n",
" \n",
"\n",
"\n",
"0->0 \n",
- " \n",
- " \n",
- "d \n",
+ " \n",
+ " \n",
+ "d \n",
" \n",
" \n",
" \n",
@@ -13390,9 +8058,10 @@
}
],
"source": [
- "for left in auts[autslen//2:]:\n",
- " for right in auts:\n",
- " display_inline(left, right, spot.product_or(left, right))"
+ "left = auts[5]\n",
+ "display(left)\n",
+ "for right in auts:\n",
+ " display_inline(right, spot.product(left, right), spot.product_or(left, right))"
]
},
{
@@ -13419,7 +8088,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
- "version": "3.6.7rc1"
+ "version": "3.7.4+"
}
},
"nbformat": 4,