From cfd888076c982ff8c2234228f71bdcefe2064f76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 22 Sep 2019 22:01:46 +0200 Subject: [PATCH 01/13] ltl2tgba, ltldo: add a --negate option Suggested by Victor Khomenko. * bin/ltl2tgba.cc, bin/ltldo.cc: Implement it. * doc/org/hierarchy.org: Use it. * tests/core/ltldo2.test: Test it. * bin/common_output.cc: Typo. * NEWS: Mention the new option. --- NEWS | 4 ++++ bin/common_output.cc | 4 ++-- bin/ltl2tgba.cc | 11 ++++++++++- bin/ltldo.cc | 31 +++++++++++++++++++++++++++---- doc/org/hierarchy.org | 4 +--- tests/core/ltldo2.test | 13 ++++++++++++- 6 files changed, 56 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 7707c4312..7201d96e9 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,9 @@ New in spot 2.8.1.dev (not yet released) + Command-line tools: + + - ltl2tgba and ltldo learned a --negate option. + Bugs fixed: - Calling "autfilt --dualize" on an alternating automaton with diff --git a/bin/common_output.cc b/bin/common_output.cc index a264c3332..092a9329f 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -82,7 +82,7 @@ report_not_ltl(spot::formula f, { std::string s = spot::str_psl(f); static const char msg[] = - "formula '%s' cannot be written %s's syntax because it is not LTL"; + "formula '%s' cannot be written in %s's syntax because it is not LTL"; if (filename) error_at_line(2, 0, filename, atoi(linenum), msg, s.c_str(), syn); else diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 7ab4a5933..332b0a81b 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,6 +46,7 @@ the smallest Transition-based Generalized Büchi Automata, \ output in the HOA format.\n\ If multiple formulas are supplied, several automata will be output."; +enum { OPT_NEGATE = 256 }; static const argp_option options[] = { @@ -59,6 +60,7 @@ static const argp_option options[] = "the part of the line after the formula if it " "comes from a column extracted from a CSV file", 4 }, /**************************************************/ + { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 1 }, { "unambiguous", 'U', nullptr, 0, "output unambiguous automata", 2 }, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, @@ -76,6 +78,7 @@ const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; +static bool negate = false; static spot::option_map extra_options; static spot::postprocessor::output_pref unambig = 0; @@ -95,6 +98,9 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; + case OPT_NEGATE: + negate = true; + break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? if (*arg == '-' && !arg[1]) @@ -139,6 +145,9 @@ namespace s.c_str()); } + if (negate) + f = spot::formula::Not(f); + spot::process_timer timer; timer.start(); auto aut = trans.run(&f); diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 1b7afb48a..374d61c78 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,6 +33,7 @@ #include "common_conv.hh" #include "common_finput.hh" #include "common_aoutput.hh" +#include "common_output.hh" #include "common_post.hh" #include "common_trans.hh" #include "common_hoaread.hh" @@ -51,13 +52,15 @@ of input and output as required."; enum { OPT_ERRORS = 256, - OPT_SMALLEST, - OPT_GREATEST, OPT_FAIL_ON_TIMEOUT, + OPT_GREATEST, + OPT_NEGATE, + OPT_SMALLEST, }; static const argp_option options[] = { + { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 1 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Error handling:", 4 }, { "errors", OPT_ERRORS, "abort|warn|ignore", 0, @@ -129,6 +132,7 @@ static bool fail_on_timeout = false; static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection static const char* best_format = "%s,%e"; static int opt_max_count = -1; +static bool negate = false; static char const *const errors_args[] = { @@ -173,6 +177,9 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg) best_format = arg; break; + case OPT_NEGATE: + negate = true; + break; case OPT_SMALLEST: best_type = -1; if (arg) @@ -336,7 +343,17 @@ namespace return 1; } - inputf = input; + if (negate) + { + pf.f = spot::formula::Not(pf.f); + std::ostringstream os; + stream_formula(os, pf.f, filename, std::to_string(linenum).c_str()); + inputf = os.str(); + } + else + { + inputf = input; + } process_formula(pf.f, filename, linenum); return 0; } @@ -464,6 +481,12 @@ main(int argc, char** argv) setup_sig_handler(); + // Usually we print the formula as it was given to us, but + // if --negate is used we have to reformat it. We don't know + // was the input format unless --lbt-input was given, and in + // that case we keep it for output. + output_format = lbt_input ? lbt_output : spot_output; + spot::postprocessor post; post.set_pref(pref | comp | sbacc | colored); post.set_type(type); diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index b0c0e4d80..f0df4c157 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -646,9 +646,7 @@ complementation ourselves: #+NAME: hier-persistence-2 #+BEGIN_SRC sh :exports code -ltlfilt --negate -f FGa | - ltl2tgba -D | - autfilt --complement -d +ltl2tgba --negate -D FGa | autfilt --complement -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results $txt diff --git a/tests/core/ltldo2.test b/tests/core/ltldo2.test index 4d739f39e..4998ce98d 100755 --- a/tests/core/ltldo2.test +++ b/tests/core/ltldo2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +# Copyright (C) 2015-2017, 2019 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -37,3 +37,14 @@ diff aut1.hoa aut2.hoa test "ltl2tgba -D" = \ "`ltldo 'ltl2tgba -D' ltl2tgba -f 'Ga | Gb | Gc' --greatest=%e --stats=%T`" + + +ltldo --negate 'ltl2tgba -D' -f FGa --stats=%f,%s >out.csv +ltldo --negate 'ltl2tgba -D' --lbt-input -f 'F G a' --stats=%f,%s >>out.csv +ltl2tgba --negate -D FGa --stats=%f,%s >>out.csv +cat >expected < Date: Mon, 23 Sep 2019 17:09:54 +0200 Subject: [PATCH 02/13] * doc/org/init.el.in: Work around obsolete ELPA signatures. --- doc/org/init.el.in | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index db416f1ed..ed0820b32 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -3,6 +3,15 @@ (setq debug-on-error t) +;;; Some combination of GNU TLS and Emacs fail to retrieve archive +;;; contents over https. +;;; https://www.reddit.com/r/emacs/comments/cdf48c/failed_to_download_gnu_archive/ +;;; https://debbugs.gnu.org/cgi/bugreport.cgi?bug=34341 +(if (and (version< emacs-version "26.3") (>= libgnutls-version 30600)) + (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")) +; work around obsolete ELPA signatures :-( +(setq package-check-signature 'nil) + (package-initialize) (require 'cl) (setq features-before features) @@ -11,13 +20,6 @@ (print (org-version nil t t)) (print (concat "Org " org-version)) -; Some combination of GNU TLS and Emacs fail to retrieve archive -; contents over https. -; https://www.reddit.com/r/emacs/comments/cdf48c/failed_to_download_gnu_archive/ -; https://debbugs.gnu.org/cgi/bugreport.cgi?bug=34341 -(if (and (version< emacs-version "26.3") (>= libgnutls-version 30600)) - (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")) - ; The Org version that ships with emacs is usually too old. (when (version< org-version "9.1") (warn "Org-mode is too old; attempting to download a more recent version") From a7e4cb4182e5ce3655c0914b9f989e7584b37a57 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Sep 2019 16:56:39 +0200 Subject: [PATCH 03/13] [buddy] fix ARM compilation * src/bddop.c, src/bddx.h, examples/bddtest/bddtest.cxx: Use signed char* instead of char*. --- buddy/examples/bddtest/bddtest.cxx | 4 ++-- buddy/src/bddop.c | 6 +++--- buddy/src/bddx.h | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/buddy/examples/bddtest/bddtest.cxx b/buddy/examples/bddtest/bddtest.cxx index 3e1444e24..3478a65bc 100644 --- a/buddy/examples/bddtest/bddtest.cxx +++ b/buddy/examples/bddtest/bddtest.cxx @@ -8,7 +8,7 @@ static const int varnum = 5; Example of allsat print handler. **************************************************************************/ -void allsatHandlerPrint(char* varset, int size) +void allsatHandlerPrint(signed char* varset, int size) { using namespace std ; for (int v=0; v Date: Tue, 24 Sep 2019 11:48:06 +0200 Subject: [PATCH 04/13] fix ARM builds * spot/misc/bitvect.hh (bitvect_array::at): Fix pointer cast. * spot/twa/bddprint.cc: Adjust to use signed char* explicitly. * spot/twaalgos/gtec/gtec.hh: Work around GCC bug #90309. * .gitlab-ci.yml: Add raspbian build. --- .gitlab-ci.yml | 17 +++++++++++++++++ spot/misc/bitvect.hh | 23 ++++++++++++++--------- spot/twa/bddprint.cc | 8 ++++---- spot/twaalgos/gtec/gtec.hh | 6 +++++- 4 files changed, 40 insertions(+), 14 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 40567ebfa..6db16b71e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -83,6 +83,7 @@ alpine-gcc: - ./configure - make - make check + - make distcheck || { chmod -R u+w ./spot-*; false; } artifacts: when: always paths: @@ -284,3 +285,19 @@ publish-unstable: - dput lrde *.changes - curl -X POST -F ref=master -F token=$TRIGGER_SPOT_WEB -F "variables[spot_branch]=next" https://gitlab.lrde.epita.fr/api/v4/projects/131/trigger/pipeline - curl -X POST -F ref=master -F token=$TRIGGER_SANDBOX https://gitlab.lrde.epita.fr/api/v4/projects/181/trigger/pipeline + +raspbian: + stage: build + tags: + - armv7 + script: + - autoreconf -vfi + - ./configure + - make + - make distcheck || { chmod -R u+w ./spot-*; false; } + artifacts: + when: always + paths: + - ./spot-*/_build/sub/tests/*/*.log + - ./*.log + - ./*.tar.gz diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index cf5771804..330f6045f 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -416,13 +416,6 @@ namespace spot return size_; } - /// Return the bit-vector at \a index. - bitvect& at(const size_t index) - { - SPOT_ASSERT(index < size_); - return *reinterpret_cast(storage() + index * bvsize_); - } - void clear_all() { // FIXME: This could be changed into a large memset if the @@ -431,11 +424,23 @@ namespace spot at(s).clear_all(); } + /// Return the bit-vector at \a index. + bitvect& at(const size_t index) + { + SPOT_ASSERT(index < size_); + // The double cast is to prevent -Wcast-align diagnostics + // about the fact that char* (the type of storage) has a + // smaller required alignment than bitvect*. + auto v = static_cast(storage() + index * bvsize_); + return *static_cast(v); + } + /// Return the bit-vector at \a index. const bitvect& at(const size_t index) const { SPOT_ASSERT(index < size_); - return *reinterpret_cast(storage() + index * bvsize_); + auto v = static_cast(storage() + index * bvsize_); + return *static_cast(v); } friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount, diff --git a/spot/twa/bddprint.cc b/spot/twa/bddprint.cc index a0d4b3625..ea0d84c2c 100644 --- a/spot/twa/bddprint.cc +++ b/spot/twa/bddprint.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2014, 2015, 2018 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2014, 2015, 2018, 2019 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -81,7 +81,7 @@ namespace spot static std::ostream* where; static void - print_sat_handler(char* varset, int size) + print_sat_handler(signed char* varset, int size) { bool not_first = false; for (int v = 0; v < size; ++v) @@ -111,7 +111,7 @@ namespace spot static bool first_done = false; static void - print_accset_handler(char* varset, int size) + print_accset_handler(signed char* varset, int size) { for (int v = 0; v < size; ++v) if (varset[v] > 0) diff --git a/spot/twaalgos/gtec/gtec.hh b/spot/twaalgos/gtec/gtec.hh index c601ca0d1..c3ddcb0c1 100644 --- a/spot/twaalgos/gtec/gtec.hh +++ b/spot/twaalgos/gtec/gtec.hh @@ -125,7 +125,10 @@ namespace spot /// \brief An implementation of the Couvreur99 emptiness-check algorithm. /// /// See the documentation for spot::couvreur99. - class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics + class SPOT_API couvreur99_check: + // We inherit from ec_statistics first to work around GCC bug #90309. + // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=90309#c6 + public ec_statistics, public emptiness_check { public: couvreur99_check(const const_twa_ptr& a, option_map o = option_map()); @@ -160,6 +163,7 @@ namespace spot bool poprem_; /// Number of dead SCC removed by the algorithm. unsigned removed_components; + unsigned get_removed_components() const; unsigned get_vmsize() const; }; From 6bdb135724427584d27b611354bda46edcb3653f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Sep 2019 21:57:25 +0200 Subject: [PATCH 05/13] bin: handle any exception before returning from parse_opt() On some architectures (e.g., ARM, or even some -flto setups on Intel) C++ exceptions to not traverse the C functions. So even if the C++ main() has a try/catch, it will not catch the exception thrown by C++ code called from the argp module (which is compiled in C). * bin/common_setup.cc, bin/common_setup.hh: Define some macros and function to factorize exception handling. * bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc, bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc, bin/common_output.cc, bin/common_post.cc, bin/common_trans.cc, bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc, bin/randaut.cc, bin/randltl.cc: Protect all parse_opt() functions, even those where there is currently no exception risk. --- bin/autcross.cc | 3 +++ bin/autfilt.cc | 3 +++ bin/common_aoutput.cc | 4 ++++ bin/common_color.cc | 8 ++++++-- bin/common_finput.cc | 7 +++++-- bin/common_hoaread.cc | 8 ++++++-- bin/common_output.cc | 4 ++++ bin/common_post.cc | 6 +++++- bin/common_setup.cc | 23 +++++++++++++++++------ bin/common_setup.hh | 7 ++++++- bin/common_trans.cc | 4 ++++ bin/dstar2tgba.cc | 5 ++++- bin/genaut.cc | 3 +++ bin/genltl.cc | 3 +++ bin/ltl2tgba.cc | 3 +++ bin/ltl2tgta.cc | 5 ++++- bin/ltlcross.cc | 3 +++ bin/ltldo.cc | 3 +++ bin/ltlfilt.cc | 3 +++ bin/ltlgrind.cc | 5 ++++- bin/ltlsynt.cc | 3 +++ bin/randaut.cc | 5 ++++- bin/randltl.cc | 5 ++++- 23 files changed, 104 insertions(+), 19 deletions(-) diff --git a/bin/autcross.cc b/bin/autcross.cc index 8a1394ddb..437759429 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -153,6 +153,8 @@ static output_file* bogus_output = nullptr; static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; switch (key) { case 'F': @@ -214,6 +216,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/autfilt.cc b/bin/autfilt.cc index f8cbf7dc4..e0f8279b2 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -688,6 +688,8 @@ product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -1154,6 +1156,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 9e8976da9..8ec651fbc 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -24,6 +24,7 @@ #include "common_aoutput.hh" #include "common_post.hh" #include "common_cout.hh" +#include "common_setup.hh" #include #include @@ -304,6 +305,8 @@ const struct argp aoutput_o_format_argp = { o_options, int parse_opt_aoutput(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -358,6 +361,7 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_color.cc b/bin/common_color.cc index 7b6330356..5c49e2021 100644 --- a/bin/common_color.cc +++ b/bin/common_color.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -19,6 +19,7 @@ #include "common_sys.hh" #include "common_color.hh" +#include "common_setup.hh" #include #include @@ -77,6 +78,8 @@ static const argp_option options_color[] = static int parse_opt_color(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -91,6 +94,7 @@ parse_opt_color(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_finput.cc b/bin/common_finput.cc index f19e64a6b..67e5a4353 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017, 2019 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -62,6 +62,8 @@ const struct argp finput_argp_headless = { options + 1, parse_opt_finput, int parse_opt_finput(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -80,6 +82,7 @@ parse_opt_finput(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_hoaread.cc b/bin/common_hoaread.cc index 809796b0c..919378da4 100644 --- a/bin/common_hoaread.cc +++ b/bin/common_hoaread.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2019 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -18,6 +18,7 @@ // along with this program. If not, see . #include "common_hoaread.hh" +#include "common_setup.hh" #include "argmatch.h" #include "error.h" @@ -72,6 +73,8 @@ static bool parse_bool(const char* opt, const char* arg) static int parse_opt_hoaread(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -81,6 +84,7 @@ parse_opt_hoaread(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_output.cc b/bin/common_output.cc index 092a9329f..e9c61a513 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -20,6 +20,7 @@ #include "common_sys.hh" #include "common_output.hh" #include "common_aoutput.hh" +#include "common_setup.hh" #include #include #include @@ -304,6 +305,8 @@ static std::map> outputfiles; int parse_opt_output(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -344,6 +347,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_post.cc b/bin/common_post.cc index ef97b0a26..e6ebfd29b 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,6 +20,7 @@ #include "common_post.hh" #include "common_r.hh" #include "common_aoutput.hh" +#include "common_setup.hh" #include "error.h" #include "argmatch.h" @@ -154,6 +155,8 @@ static const argp_option options_disabled[] = static int parse_opt_post(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -253,6 +256,7 @@ parse_opt_post(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 99b4eb202..dab5df571 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -150,6 +150,8 @@ static const argp_option options_hidden[] = static int parse_opt_misc(int key, char*, struct argp_state* state) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -170,6 +172,7 @@ parse_opt_misc(int key, char*, struct argp_state* state) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } @@ -181,6 +184,18 @@ const struct argp misc_argp_hidden = { options_hidden, parse_opt_misc, nullptr, nullptr, nullptr, nullptr, nullptr }; +[[noreturn]] void handle_any_exception() +{ + try + { + throw; + } + catch (const std::exception& e) + { + error(2, 0, "%s", e.what()); + } + SPOT_UNREACHABLE(); +} int protected_main(char** progname, std::function mainfun) { @@ -189,13 +204,9 @@ int protected_main(char** progname, std::function mainfun) setup(progname); return mainfun(); } - catch (const std::runtime_error& e) + catch (...) { - error(2, 0, "%s", e.what()); - } - catch (const std::invalid_argument& e) - { - error(2, 0, "%s", e.what()); + handle_any_exception(); } SPOT_UNREACHABLE(); return 2; diff --git a/bin/common_setup.hh b/bin/common_setup.hh index 41f4a71a2..e2fce84e0 100644 --- a/bin/common_setup.hh +++ b/bin/common_setup.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2018 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -31,3 +31,8 @@ extern const struct argp misc_argp_hidden; // Call setup(progname) then Run mainfun() and handle exceptions. int protected_main(char** progname, std::function mainfun); + +// Diagnose exceptions. +[[noreturn]] void handle_any_exception(); +#define BEGIN_EXCEPTION_PROTECT try { (void)0; +#define END_EXCEPTION_PROTECT } catch (...) { handle_any_exception(); } diff --git a/bin/common_trans.cc b/bin/common_trans.cc index bac0c15ba..e3df2316b 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -18,6 +18,7 @@ // along with this program. If not, see . #include "common_trans.hh" +#include "common_setup.hh" #include #include #include @@ -902,6 +903,8 @@ bool opt_relabel = false; static int parse_opt_trans(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; switch (key) { case 't': @@ -930,6 +933,7 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 1abe45f23..3bf5b9393 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -83,6 +83,8 @@ static spot::option_map extra_options; static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -102,6 +104,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/genaut.cc b/bin/genaut.cc index 9e8f1939e..eb2163cab 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -97,11 +97,14 @@ enqueue_job(int pattern, const char* range_str) static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; if (key >= gen::AUT_BEGIN && key < gen::AUT_END) { enqueue_job(key, arg); return 0; } + END_EXCEPTION_PROTECT; return ARGP_ERR_UNKNOWN; } diff --git a/bin/genltl.cc b/bin/genltl.cc index c9f8374bd..6c632de7a 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -261,6 +261,8 @@ enqueue_job(int pattern, const char* range_str = nullptr) static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; if (key >= gen::LTL_BEGIN && key < gen::LTL_END) { enqueue_job(key, arg); @@ -278,6 +280,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 332b0a81b..e24e7e856 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -85,6 +85,8 @@ static spot::postprocessor::output_pref unambig = 0; static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -112,6 +114,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 198b9ccfe..8663f5513 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -109,6 +109,8 @@ bool opt_with_artificial_livelock = false; static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -154,6 +156,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index edb5caa41..efafe7b31 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -440,6 +440,8 @@ std::vector formulas; static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -556,6 +558,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 374d61c78..f3e68c34b 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -164,6 +164,8 @@ const struct argp_child children[] = static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; switch (key) { case OPT_ERRORS: @@ -197,6 +199,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index a5a872012..68b4a1d2c 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -345,6 +345,8 @@ parse_formula_arg(const std::string& input) static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -545,6 +547,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 2e141e863..393656b00 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -131,6 +131,8 @@ namespace static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; switch (key) { case 'm': @@ -177,6 +179,7 @@ parse_opt(int key, char* arg, struct argp_state*) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 99e7410eb..8377b79d6 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -412,6 +412,8 @@ namespace static int parse_opt(int key, char* arg, struct argp_state*) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; switch (key) { case OPT_INPUT: @@ -452,6 +454,7 @@ parse_opt(int key, char* arg, struct argp_state*) verbose = true; break; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/randaut.cc b/bin/randaut.cc index 76e17085a..8a14ae740 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -182,6 +182,8 @@ looks_like_a_range(const char* str) static int parse_opt(int key, char* arg, struct argp_state* as) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -264,6 +266,7 @@ parse_opt(int key, char* arg, struct argp_state* as) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } diff --git a/bin/randltl.cc b/bin/randltl.cc index 47bfdb3bf..cded77171 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche +// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -159,6 +159,8 @@ static bool ap_count_given = false; static int parse_opt(int key, char* arg, struct argp_state* as) { + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; // This switch is alphabetically-ordered. switch (key) { @@ -231,6 +233,7 @@ parse_opt(int key, char* arg, struct argp_state* as) default: return ARGP_ERR_UNKNOWN; } + END_EXCEPTION_PROTECT; return 0; } From 4c0e7bf865843f393d8fbdb73b8469c12e032e5b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Sep 2019 11:44:15 +0200 Subject: [PATCH 06/13] aiger: simplify output code, and fix some function call order * spot/twaalgos/aiger.cc: Simplify some bit operatitions. Force the ordering of operations in aig_and, that was causing a test case to fail on ARM, and greatly simplify the code and data structures used in remove_unused(). * tests/core/ltlsynt.test: Adjust expected output. --- spot/twaalgos/aiger.cc | 91 +++++++++++++++++++++++------------------ tests/core/ltlsynt.test | 10 ++--- 2 files changed, 56 insertions(+), 45 deletions(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 459e82c97..ea8f8ee6e 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -120,7 +120,7 @@ namespace spot unsigned aig_not(unsigned v) { - unsigned not_v = v + 1 - 2 * (v % 2); + unsigned not_v = v ^ 1; assert(var2bdd_.count(v)); var2bdd_[not_v] = !(var2bdd_[v]); bdd2var_[var2bdd_[not_v]] = not_v; @@ -137,9 +137,8 @@ namespace spot return it->second; max_var_ += 2; and_gates_[max_var_] = {v1, v2}; - bdd v1v2 = var2bdd_[v1] & var2bdd_[v2]; - bdd2var_[v1v2] = max_var_; - var2bdd_[max_var_] = v1v2; + bdd2var_[b] = max_var_; + var2bdd_[max_var_] = b; return max_var_; } @@ -152,14 +151,18 @@ namespace spot if (vs.size() == 2) return aig_and(vs[0], vs[1]); unsigned m = vs.size() / 2; - std::vector left(vs.begin(), vs.begin() + m); - std::vector right(vs.begin() + m, vs.end()); - return aig_and(aig_and(left), aig_and(right)); + unsigned left = + aig_and(std::vector(vs.begin(), vs.begin() + m)); + unsigned right = + aig_and(std::vector(vs.begin() + m, vs.end())); + return aig_and(left, right); } unsigned aig_or(unsigned v1, unsigned v2) { - return aig_not(aig_and(aig_not(v1), aig_not(v2))); + unsigned n1 = aig_not(v1); + unsigned n2 = aig_not(v2); + return aig_not(aig_and(n1, n2)); } unsigned aig_or(std::vector vs) @@ -171,45 +174,53 @@ namespace spot unsigned aig_pos(unsigned v) { - return v - v % 2; + + return v & ~1; } void remove_unused() { - std::unordered_set todo; + // Run a DFS on the gates and latches to collect + // all nodes connected to the output. + std::deque todo; + std::vector used(max_var_ / 2 + 1, false); + auto mark = [&](unsigned v) + { + unsigned pos = aig_pos(v); + if (!used[pos/2]) + { + used[pos/2] = 1; + todo.push_back(pos); + } + }; for (unsigned v : outputs_) - todo.insert(aig_pos(v)); - std::unordered_set used; + mark(v); while (!todo.empty()) { - used.insert(todo.begin(), todo.end()); - std::unordered_set todo_next; - for (unsigned v : todo) + unsigned v = todo.front(); + todo.pop_front(); + auto it_and = and_gates_.find(v); + if (it_and != and_gates_.end()) { - auto it_and = and_gates_.find(v); - if (it_and != and_gates_.end()) - { - if (!used.count(aig_pos(it_and->second.first))) - todo_next.insert(aig_pos(it_and->second.first)); - if (!used.count(aig_pos(it_and->second.second))) - todo_next.insert(aig_pos(it_and->second.second)); - } - else if (v <= (num_inputs_ + latches_.size()) * 2 - && v > num_inputs_ * 2) - { - unsigned l = v / 2 - num_inputs_ - 1; - if (!used.count(aig_pos(latches_[l]))) - todo_next.insert(aig_pos(latches_[l])); - } + mark(it_and->second.first); + mark(it_and->second.second); + } + else if (v <= (num_inputs_ + latches_.size()) * 2 + && v > num_inputs_ * 2) + { + mark(latches_[v / 2 - num_inputs_ - 1]); } - todo = todo_next; } - std::unordered_set unused; - for (auto& p : and_gates_) - if (!used.count(p.first)) - unused.insert(p.first); - for (unsigned v : unused) - and_gates_.erase(v); + // Erase and_gates that were not seen in the above + // exploration. + auto e = and_gates_.end(); + for (auto i = and_gates_.begin(); i != e;) + { + if (!used[i->first/2]) + i = and_gates_.erase(i); + else + ++i; + } } void @@ -244,7 +255,7 @@ namespace spot std::vector v(size); for (unsigned i = 0; i < size; ++i) { - v[i] = s % 2; + v[i] = s & 1; s >>= 1; } return v; @@ -277,7 +288,7 @@ namespace spot unsigned st0 = bdd_var(all); for (unsigned i = 0; i < size; ++i) { - b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); + b &= (s & 1) ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); s >>= 1; } } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index bdd0de907..5a1886e8c 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -61,11 +61,11 @@ aag 23 1 2 1 16 26 4 6 28 2 26 30 3 26 -36 29 31 -38 25 36 -40 17 23 -42 13 40 -44 42 38 +36 17 23 +38 13 36 +40 29 31 +42 25 40 +44 38 42 46 25 29 i0 a o0 b From 2fa68cc44d70d23f58043fdf7d9186d4595ff05a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Sep 2019 14:10:09 +0200 Subject: [PATCH 07/13] * doc/org/index.org: Clarify license implications. --- doc/org/index.org | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/org/index.org b/doc/org/index.org index 1d1292bbe..f80f1c939 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -59,9 +59,9 @@ The latest version is *{{{LASTRELEASE}}}* and was released on Spot is distributed under a [[http://www.gnu.org/licenses/gpl-3.0.html][GNU GPL v3 license]]. -A consequence is that if you distribute a tool built using Spot, you -*must* make the source code of that tool available as well, under a -compatible license. +One consequence is that any work based on Spot is covered by that +license as well. For instance if you distribute a tool that [[https://en.wikipedia.org/wiki/GNU_General_Public_License#Linking_and_derived_works][links +with]] Spot, you should distribute the source code of that tool as well. * Staying in touch From 362682c7cd062cc685451e0e24e74a1db0c2bb20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Sep 2019 17:16:28 +0200 Subject: [PATCH 08/13] * .gitlab-ci.yml (arch-gcc-glibcxxdebug): Do not call env. --- .gitlab-ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6db16b71e..5f973ff66 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -116,7 +116,6 @@ arch-gcc-glibcxxdebug: - /wip/ image: registry.lrde.epita.fr/spot-arch script: - - env - autoreconf -vfi - ./configure --enable-devel --enable-c++17 --enable-glibcxx-debug - make From 34cf0491ebe549c02d048a4812fee98fd9330291 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 27 Sep 2019 13:50:20 +0200 Subject: [PATCH 09/13] * tests/python/_product_weak.ipynb: Work around jupyter timeouts. --- tests/python/_product_weak.ipynb | 10463 +++++++---------------------- 1 file changed, 2566 insertions(+), 7897 deletions(-) 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, From 7e44016d38dae01ab7b0f2bf9ff543b9ec777d38 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 27 Sep 2019 18:00:52 +0200 Subject: [PATCH 10/13] [buddy] improve C++ backward compatibility around bdd_allsat change * src/bddx.h (bdd_allsat): Add a version with the old prototype. --- buddy/src/bddx.h | 9 +++++++++ 1 file changed, 9 insertions(+) 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); } From 5bf91077f4525ccac8fadd3d667f5d05d8c7801f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 27 Sep 2019 06:51:00 +0200 Subject: [PATCH 11/13] * .gitlab-ci.yml (raspbian): Restrict to branches. --- .gitlab-ci.yml | 2 ++ 1 file changed, 2 insertions(+) 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: From 1102def717b3bae893dc3f728d1f9090a0212ce8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Sep 2019 15:19:06 +0200 Subject: [PATCH 12/13] Release Spot 2.8.2 * NEWS, configure.ac, doc/org/setup.org: Update version to 2.8.2. --- NEWS | 8 +++++++- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 7201d96e9..2fac860d3 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.8.1.dev (not yet released) +New in spot 2.8.2 (2019-09-27) Command-line tools: @@ -10,6 +10,12 @@ New in spot 2.8.1.dev (not yet released) 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/configure.ac b/configure.ac index 79d7d6e08..b7a4b8354 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], [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]] From cbfcee9449138167af2d2a844333b3a09490eeb3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 27 Sep 2019 06:47:31 +0200 Subject: [PATCH 13/13] Bump version to 2.8.2.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 2fac860d3..6ee7113fa 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.8.2.dev (not yet released) + + Nothing yet. + New in spot 2.8.2 (2019-09-27) Command-line tools: diff --git a/configure.ac b/configure.ac index b7a4b8354..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.2], [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])