From a738801edfcffcff73fb4cf3101d00341b5ff714 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 May 2018 18:34:31 +0200 Subject: [PATCH] product: optimize product with weak automata Fixes #350. * spot/twaalgos/product.cc: Implement this change. * NEWS, spot/twaalgos/product.hh: Mention it. * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method. * tests/python/_product_weak.ipynb: New file. * tests/Makefile.am: Add it. * tests/python/automata.ipynb, tests/python/highlighting.ipynb, tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases. --- NEWS | 5 + spot/twa/acc.cc | 26 +- spot/twa/acc.hh | 13 +- spot/twaalgos/product.cc | 220 +- spot/twaalgos/product.hh | 22 +- tests/Makefile.am | 1 + tests/core/prodor.test | 25 +- tests/python/_product_weak.ipynb | 13400 +++++++++++++++++++++++++++++ tests/python/automata.ipynb | 636 +- tests/python/highlighting.ipynb | 177 +- tests/python/product.ipynb | 2428 +++--- 11 files changed, 15348 insertions(+), 1605 deletions(-) create mode 100644 tests/python/_product_weak.ipynb diff --git a/NEWS b/NEWS index c1073d13c..cee198016 100644 --- a/NEWS +++ b/NEWS @@ -89,6 +89,11 @@ New in spot 2.5.3.dev (not yet released) They are most welcome in Python, since we used to redefine them every now and them. + - spot::product() and spot::product_or() learned so produce an + automaton with a simpler acceptance condition if one of the + argument is a weak automaton. In this case the resulting + acceptance condition is (usually) that of the other argument. + - spot::parity_product() and spot::parity_product_or() were dropped. The code was buggy, hard to maintain, and these functions do not seem to be used. diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 92e339cf8..4286c06bc 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1153,12 +1153,22 @@ namespace spot } std::pair - acc_cond::unsat_mark() const + acc_cond::sat_unsat_mark(bool sat) const { - if (is_t()) - return {false, mark_t({})}; - if (!uses_fin_acceptance()) - return {true, mark_t({})}; + if (sat) + { + if (is_f()) + return {false, mark_t({})}; + if (!uses_fin_acceptance()) + return {true, all_sets()}; + } + else + { + if (is_t()) + return {false, mark_t({})}; + if (!uses_fin_acceptance()) + return {true, mark_t({})}; + } auto used = code_.used_sets(); unsigned c = used.count(); @@ -1185,11 +1195,11 @@ namespace spot bdd res = to_bdd_rec(&code_.back(), &r[0]); if (res == bddtrue) - return {false, mark_t({})}; + return {sat, mark_t({})}; if (res == bddfalse) - return {true, mark_t({})}; + return {!sat, mark_t({})}; - bdd cube = bdd_satone(!res); + bdd cube = bdd_satone(sat ? res : !res); mark_t i = {}; while (cube != bddtrue) { diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 93e6a16f2..253cd608b 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1165,10 +1165,21 @@ namespace spot // Return (true, m) if there exist some acceptance mark m that // does not satisfy the acceptance condition. Return (false, 0U) // otherwise. - std::pair unsat_mark() const; + std::pair unsat_mark() const + { + return sat_unsat_mark(false); + } + // Return (true, m) if there exist some acceptance mark m that + // does satisfy the acceptance condition. Return (false, 0U) + // otherwise. + std::pair sat_mark() const + { + return sat_unsat_mark(true); + } protected: bool check_fin_acceptance() const; + std::pair sat_unsat_mark(bool) const; public: static acc_code inf(mark_t mark) diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index df32d2c8b..56a2bcbac 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -40,33 +40,18 @@ namespace spot } }; + + template static - twa_graph_ptr product_aux(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right, - unsigned left_state, - unsigned right_state, - bool and_acc) + void product_main(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state, + twa_graph_ptr res, T merge_acc) { - if (!(left->is_existential() && right->is_existential())) - throw std::runtime_error - ("product() does not support alternating automata"); std::unordered_map s2n; std::deque> todo; - if (left->get_dict() != right->get_dict()) - throw std::runtime_error("product: left and right automata should " - "share their bdd_dict"); - auto res = make_twa_graph(left->get_dict()); - res->copy_ap_of(left); - res->copy_ap_of(right); - auto left_num = left->num_sets(); - auto right_acc = right->get_acceptance() << left_num; - if (and_acc) - right_acc &= left->get_acceptance(); - else - right_acc |= left->get_acceptance(); - res->set_acceptance(left_num + right->num_sets(), right_acc); - auto v = new product_states; res->set_named_prop("product-states", v); @@ -86,10 +71,10 @@ namespace spot }; res->set_init_state(new_state(left_state, right_state)); - if (right_acc.is_f()) + if (res->acc().is_f()) // Do not bother doing any work if the resulting acceptance is // false. - return res; + return; while (!todo.empty()) { auto top = todo.front(); @@ -102,10 +87,192 @@ namespace spot continue; auto dst = new_state(l.dst, r.dst); res->new_edge(top.second, dst, cond, - l.acc | (r.acc << left_num)); + merge_acc(l.acc, r.acc)); // If right is deterministic, we can abort immediately! } } + } + + static + twa_graph_ptr product_aux(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state, + bool and_acc) + { + if (SPOT_UNLIKELY(!(left->is_existential() && right->is_existential()))) + throw std::runtime_error + ("product() does not support alternating automata"); + if (SPOT_UNLIKELY(left->get_dict() != right->get_dict())) + throw std::runtime_error("product: left and right automata should " + "share their bdd_dict"); + + auto res = make_twa_graph(left->get_dict()); + res->copy_ap_of(left); + res->copy_ap_of(right); + + bool leftweak = left->prop_weak().is_true(); + bool rightweak = right->prop_weak().is_true(); + // We have optimization to the standard product in case one + // of the arguments is weak. However these optimizations + // are pointless if the said arguments are "t" or "f". + if ((leftweak || rightweak) + && (left->num_sets() > 0) && (right->num_sets() > 0)) + { + // If both automata are weak, we can restrict the result to + // Büchi or co-Büchi. We will favor Büchi unless the two + // operands are co-Büchi. + if (leftweak && rightweak) + { + weak_weak: + acc_cond::mark_t accmark = {0}; + acc_cond::mark_t rejmark = {}; + if (left->acc().is_co_buchi() && right->acc().is_co_buchi()) + { + res->set_co_buchi(); + std::swap(accmark, rejmark); + } + else + { + res->set_buchi(); + } + res->prop_weak(true); + auto& lacc = left->acc(); + auto& racc = right->acc(); + if (and_acc) + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (lacc.accepting(ml) && racc.accepting(mr)) + return accmark; + else + return rejmark; + }); + else + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (lacc.accepting(ml) || racc.accepting(mr)) + return accmark; + else + return rejmark; + }); + } + else if (!rightweak) + { + if (and_acc) + { + auto rightunsatmark = right->acc().unsat_mark(); + if (!rightunsatmark.first) + { + // Left is weak. Right was not weak, but it is + // always accepting. We can therefore pretend + // that right is weak. + goto weak_weak; + } + res->copy_acceptance_of(right); + acc_cond::mark_t rejmark = rightunsatmark.second; + auto& lacc = left->acc(); + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (lacc.accepting(ml)) + return mr; + else + return rejmark; + }); + } + else + { + auto rightsatmark = right->acc().sat_mark(); + if (!rightsatmark.first) + { + // Left is weak. Right was not weak, but it is + // always rejecting. We can therefore pretend + // that right is weak. + goto weak_weak; + } + res->copy_acceptance_of(right); + acc_cond::mark_t accmark = rightsatmark.second; + auto& lacc = left->acc(); + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (!lacc.accepting(ml)) + return mr; + else + return accmark; + }); + + } + } + else + { + assert(!leftweak); + if (and_acc) + { + auto leftunsatmark = left->acc().unsat_mark(); + if (!leftunsatmark.first) + { + // Right is weak. Left was not weak, but it is + // always accepting. We can therefore pretend + // that left is weak. + goto weak_weak; + } + res->copy_acceptance_of(left); + acc_cond::mark_t rejmark = leftunsatmark.second; + auto& racc = right->acc(); + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (racc.accepting(mr)) + return ml; + else + return rejmark; + }); + } + else + { + auto leftsatmark = left->acc().sat_mark(); + if (!leftsatmark.first) + { + // Right is weak. Left was not weak, but it is + // always rejecting. We can therefore pretend + // that left is weak. + goto weak_weak; + } + res->copy_acceptance_of(left); + acc_cond::mark_t accmark = leftsatmark.second; + auto& racc = right->acc(); + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + if (!racc.accepting(mr)) + return ml; + else + return accmark; + }); + + } + } + } + else // general case + { + auto left_num = left->num_sets(); + auto right_acc = right->get_acceptance() << left_num; + if (and_acc) + right_acc &= left->get_acceptance(); + else + right_acc |= left->get_acceptance(); + res->set_acceptance(left_num + right->num_sets(), right_acc); + + product_main(left, right, left_state, right_state, res, + [&] (acc_cond::mark_t ml, acc_cond::mark_t mr) + { + return ml | (mr << left_num); + }); + + } // The product of two non-deterministic automata could be // deterministic. Likewise for non-complete automata. @@ -147,8 +314,7 @@ namespace spot unsigned left_state, unsigned right_state) { - return product_aux(complete(left), - complete(right), + return product_aux(complete(left), complete(right), left_state, right_state, false); } diff --git a/spot/twaalgos/product.hh b/spot/twaalgos/product.hh index ef8d47374..e07aedb99 100644 --- a/spot/twaalgos/product.hh +++ b/spot/twaalgos/product.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -36,7 +36,10 @@ namespace spot /// The resulting automaton will accept the intersection of both /// languages and have an acceptance condition that is the /// conjunction of the acceptance conditions of the two input - /// automata. + /// automata. In case one of the left or right automaton is weak, + /// the acceptance condition of the result is made simpler: it + /// usually is the acceptance condition of the other argument, + /// therefore avoiding the need to introduce new accepting sets. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -56,7 +59,10 @@ namespace spot /// languages recognized by each input automaton (with its initial /// state changed) and have an acceptance condition that is the /// conjunction of the acceptance conditions of the two input - /// automata. + /// automata. In case one of the left or right automaton is weak, + /// the acceptance condition of the result is made simpler: it + /// usually is the acceptance condition of the other argument, + /// therefore avoiding the need to introduce new accepting sets. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -74,7 +80,10 @@ namespace spot /// The resulting automaton will accept the union of both /// languages and have an acceptance condition that is the /// disjunction of the acceptance conditions of the two input - /// automata. + /// automata. In case one of the left or right automaton is weak, + /// the acceptance condition of the result is made simpler: it + /// usually is the acceptance condition of the other argument, + /// therefore avoiding the need to introduce new accepting sets. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores @@ -94,7 +103,10 @@ namespace spot /// recognized by each input automaton (with its initial state /// changed) and have an acceptance condition that is the /// disjunction of the acceptance conditions of the two input - /// automata. + /// automata. In case one of the left or right automaton is weak, + /// the acceptance condition of the result is made simpler: it + /// usually is the acceptance condition of the other argument, + /// therefore avoiding the need to introduce new accepting sets. /// /// The algorithm also defines a named property called /// "product-states" with type spot::product_states. This stores diff --git a/tests/Makefile.am b/tests/Makefile.am index dceda1b95..bba62bffa 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -383,6 +383,7 @@ TESTS_python = \ python/parsetgba.py \ python/parity.py \ python/prodexpt.py \ + python/_product_weak.ipynb \ python/randgen.py \ python/relabel.py \ python/remfin.py \ diff --git a/tests/core/prodor.test b/tests/core/prodor.test index cf40c57fd..c91a48d8d 100755 --- a/tests/core/prodor.test +++ b/tests/core/prodor.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -106,6 +106,7 @@ diff pand.hoa exp test 2 = `autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa` +# Xb is weak, so the product will still be Büchi ltl2tgba -BDH 'GFa' > gfa.hoa ltl2tgba -BDH 'Xb' > xb.hoa autfilt --product-or gfa.hoa xb.hoa -H > por.hoa @@ -116,14 +117,15 @@ HOA: v1 States: 7 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Inf(0) | Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- -State: 0 {1} +State: 0 {0} [0] 1 [!0] 2 -State: 1 {1} +State: 1 {0} [0&1] 3 [!0&1] 4 [0&!1] 5 @@ -133,13 +135,13 @@ State: 2 [!0&1] 4 [0&!1] 5 [!0&!1] 6 -State: 3 {0 1} +State: 3 {0} [0] 3 [!0] 4 State: 4 {0} [0] 3 [!0] 4 -State: 5 {1} +State: 5 {0} [0] 5 [!0] 6 State: 6 @@ -159,14 +161,15 @@ HOA: v1 States: 7 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Inf(0) | Inf(1) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- -State: 0 {0 1} +State: 0 {0} [0] 1 [!0] 2 -State: 1 {0 1} +State: 1 {0} [0&1] 3 [!0&1] 4 [0&!1] 5 @@ -176,13 +179,13 @@ State: 2 {0} [!0&1] 4 [0&!1] 5 [!0&!1] 6 -State: 3 {0 1} +State: 3 {0} [0] 3 [!0] 4 State: 4 {0} [0] 3 [!0] 4 -State: 5 {1} +State: 5 {0} [0] 5 [!0] 6 State: 6 diff --git a/tests/python/_product_weak.ipynb b/tests/python/_product_weak.ipynb new file mode 100644 index 000000000..b5a233435 --- /dev/null +++ b/tests/python/_product_weak.ipynb @@ -0,0 +1,13400 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Test the optimization of `product()` for weak arguments." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "spot.setup()\n", + "from spot.jupyter import display_inline" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "auts = [a for a in spot.automata(\"\"\"\n", + "HOA: v1\n", + "name: \"a\"\n", + "States: 2\n", + "Start: 1\n", + "AP: 1 \"a\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc deterministic\n", + "properties: stutter-invariant terminal\n", + "--BODY--\n", + "State: 0\n", + "[t] 0\n", + "State: 1\n", + "[0] 0\n", + "--END--\n", + "HOA: v1\n", + "name: \"Fb\"\n", + "States: 2\n", + "Start: 1\n", + "AP: 1 \"b\"\n", + "acc-name: Buchi\n", + "Acceptance: 1 Inf(0)\n", + "properties: trans-labels explicit-labels state-acc complete\n", + "properties: deterministic stutter-invariant terminal\n", + "--BODY--\n", + "State: 0 {0}\n", + "[t] 0\n", + "State: 1\n", + "[0] 0\n", + "[!0] 1\n", + "--END--\n", + "HOA: v1\n", + "name: \"Fb\"\n", + "States: 2\n", + "Start: 1\n", + "AP: 1 \"b\"\n", + "acc-name: co-Buchi\n", + "Acceptance: 1 Fin(0)\n", + "properties: trans-labels explicit-labels state-acc complete\n", + "properties: deterministic stutter-invariant terminal\n", + "--BODY--\n", + "State: 0 \n", + "[t] 0\n", + "State: 1 {0}\n", + "[0] 0\n", + "[!0] 1\n", + "--END--\n", + "HOA: v1\n", + "name: \"GFc\"\n", + "States: 1\n", + "Start: 0\n", + "AP: 1 \"c\"\n", + "acc-name: Buchi\n", + "Acceptance: 1 Inf(0)\n", + "properties: trans-labels explicit-labels trans-acc complete\n", + "properties: deterministic stutter-invariant\n", + "--BODY--\n", + "State: 0\n", + "[!0] 0\n", + "[0] 0 {0}\n", + "--END--\n", + "HOA: v1\n", + "States: 1\n", + "Start: 0\n", + "AP: 1 \"d\"\n", + "Acceptance: 1 Inf(0)&Fin(0)\n", + "--BODY--\n", + "State: 0\n", + "[!0] 0 {0}\n", + "[0] 0\n", + "--END--\n", + "HOA: v1\n", + "States: 1\n", + "Start: 0\n", + "AP: 1 \"d\"\n", + "Acceptance: 1 Inf(0)|Fin(0)\n", + "--BODY--\n", + "State: 0 \n", + "[!0] 0 {0}\n", + "[0] 0\n", + "--END--\n", + "\"\"\")]" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": { + "scrolled": false + }, + "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", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\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\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", + "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", + "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", + "0,1\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", + "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", + "[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", + "0,1\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", + "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", + "\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", + "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", + "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" + }, + { + "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:\n", + " for right in auts:\n", + " display_inline(left, right, spot.product(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": { + "scrolled": false + }, + "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", + "\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", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->2\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", + "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", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "d\n", + "\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", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !d\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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 & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "1,2\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->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "4->2\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", + "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", + "\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", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[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", + ")\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", + "[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", + ") | 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", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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 & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "1,2\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->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "4->2\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", + "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", + "\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", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fb\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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", + ")\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", + "\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", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "GFc\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->2\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", + "\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", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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", + "\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", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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", + "[Fin-less 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", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "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", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "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", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "d\n", + "\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", + ")\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", + "[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", + ")\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", + "[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", + ") & Fin(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !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", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ") & Fin(\n", + "\n", + "))\n", + "[Rabin-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!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", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "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", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "0,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !d\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[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", + "[Rabin-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\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", + ")|Fin(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", + "[Rabin-like 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "for left in auts:\n", + " for right in auts:\n", + " display_inline(left, right, spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.6.5" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index d1e14083a..327b764f0 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -8,6 +8,7 @@ "source": [ "from IPython.display import display\n", "import spot\n", + "from spot.jupyter import display_inline\n", "spot.setup()" ] }, @@ -163,7 +164,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe2c0c80f0> >" + " *' at 0x7f16ec60d690> >" ] }, "execution_count": 2, @@ -600,7 +601,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efccd80> >" + " *' at 0x7f16ec57bc90> >" ] }, "execution_count": 6, @@ -676,7 +677,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efdc180> >" + " *' at 0x7f16ec58a9f0> >" ] }, "execution_count": 7, @@ -759,7 +760,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efdc150> >" + " *' at 0x7f16ec58ab10> >" ] }, "execution_count": 8, @@ -1278,7 +1279,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee7e0> >" + " *' at 0x7f16ec59c840> >" ] }, "execution_count": 12, @@ -1392,7 +1393,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee900> >" + " *' at 0x7f16ec59ca20> >" ] }, "execution_count": 13, @@ -1523,7 +1524,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee7b0> >" + " *' at 0x7f16ec59cab0> >" ] }, "execution_count": 14, @@ -1635,7 +1636,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee810> >" + " *' at 0x7f16ec59cb10> >" ] }, "execution_count": 15, @@ -2180,7 +2181,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efcc9c0> >" + " *' at 0x7f16ec59c210> >" ] }, "execution_count": 16, @@ -2391,7 +2392,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee2a0> >" + " *' at 0x7f16ec59cbd0> >" ] }, "metadata": {}, @@ -2541,7 +2542,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efcce40> >" + " *' at 0x7f16ec57b9c0> >" ] }, "metadata": {}, @@ -2713,7 +2714,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efeec90> >" + " *' at 0x7f16ec59ce40> >" ] }, "metadata": {}, @@ -2888,7 +2889,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efeeba0> >" + " *' at 0x7f16ec59cc90> >" ] }, "metadata": {}, @@ -3074,7 +3075,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efeee40> >" + " *' at 0x7f16ec59cf00> >" ] }, "execution_count": 21, @@ -3150,7 +3151,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efeef30> >" + " *' at 0x7f16ec59c8d0> >" ] }, "execution_count": 22, @@ -3169,123 +3170,151 @@ "outputs": [ { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "text/plain": [ + "True" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.formula('(a W c) & FGa').is_syntactic_persistence()" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "no\n" + ] + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "Inf(\n", + "\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", - "a & !c\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "c\n", - "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", - "\n", - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", "\n", - "I->1\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "\n", - "1->1\n", + "\n", + "\n", + "0->0\n", "\n", "\n", "a & !b\n", "\n", - "\n", + "\n", "\n", - "0\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", + "\n", "\n", - "1->0\n", + "0->1\n", "\n", "\n", "b\n", "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", "\n", "\n", - "" + "
" ], "text/plain": [ - "" + "" ] }, "metadata": {}, @@ -3293,267 +3322,323 @@ }, { "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "text/html": [ + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,1\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "0,1\n", + "\n", + "1,0\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "3\n", - "\n", - "1,0\n", + "\n", + "1,1\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !b & c\n", - "\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "\n", + "\n", "3->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", - "" + "
" ], "text/plain": [ - "" + "" ] }, "metadata": {}, @@ -3563,10 +3648,13 @@ "source": [ "# Using +1 in the display options is a convient way to shift the \n", "# set numbers in the output, as an aid in reading the product.\n", - "a1 = spot.translate('a W c'); display(a1.show('.t'))\n", - "a2 = spot.translate('a U b'); display(a2.show('.t+1'))\n", - "# the product should display pairs of states, unless asked not to (using 1).\n", - "p = spot.product(a1, a2); display(p.show('.t')); display(p.show('.t1'))" + "a1 = spot.translate('GF(a <-> Xa)')\n", + "print(a1.prop_weak())\n", + "a2 = spot.translate('a U b & GFc')\n", + "display_inline(a1.show('.t'), a2.show('.t+1'))\n", + "# the product should display pairs of states, unless asked not to (using '1').\n", + "p = spot.product(a1, a2)\n", + "display_inline(p.show('.t'), p.show('.t1'), per_row=2)" ] }, { @@ -3578,7 +3666,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 25, "metadata": {}, "outputs": [ { @@ -3643,7 +3731,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1effb4b0> >" + " *' at 0x7f16ec52abd0> >" ] }, "metadata": {}, @@ -3667,7 +3755,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 26, "metadata": {}, "outputs": [ { @@ -3743,10 +3831,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efeec90> >" + " *' at 0x7f16ec52ae40> >" ] }, - "execution_count": 25, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -3764,7 +3852,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 27, "metadata": {}, "outputs": [ { @@ -3816,10 +3904,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1efee030> >" + " *' at 0x7f16ec52ab10> >" ] }, - "execution_count": 26, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -3837,7 +3925,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -3905,7 +3993,7 @@ "" ] }, - "execution_count": 27, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -3923,7 +4011,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 29, "metadata": {}, "outputs": [ { @@ -3980,10 +4068,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1effbe10> >" + " *' at 0x7f16ec53da50> >" ] }, - "execution_count": 28, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -4001,7 +4089,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 30, "metadata": {}, "outputs": [ { @@ -4066,7 +4154,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1effb4b0> >" + " *' at 0x7f16ec52abd0> >" ] }, "metadata": {}, @@ -4134,7 +4222,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1effb4b0> >" + " *' at 0x7f16ec52abd0> >" ] }, "metadata": {}, @@ -4159,7 +4247,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 31, "metadata": {}, "outputs": [ { @@ -4224,10 +4312,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbe1effb4b0> >" + " *' at 0x7f16ec52abd0> >" ] }, - "execution_count": 30, + "execution_count": 31, "metadata": {}, "output_type": "execute_result" } diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 69b332f70..370aab3c6 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -240,7 +240,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4c3f0c0> >" + " *' at 0x7f0128edca50> >" ] }, "execution_count": 4, @@ -352,7 +352,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4c3f0f0> >" + " *' at 0x7f0128e4cd50> >" ] }, "execution_count": 5, @@ -462,7 +462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4c3f0c0> >" + " *' at 0x7f0128edca50> >" ] }, "execution_count": 6, @@ -695,7 +695,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b5acc0> >" + " *' at 0x7f0128e4cab0> >" ] }, "execution_count": 8, @@ -892,7 +892,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b5acc0> >" + " *' at 0x7f0128e4cab0> >" ] }, "execution_count": 11, @@ -977,7 +977,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c6f0> >" + " *' at 0x7f0128e6d8a0> >" ] }, "metadata": {}, @@ -1032,7 +1032,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c2a0> >" + " *' at 0x7f0128e6d780> >" ] }, "metadata": {}, @@ -1059,80 +1059,74 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c0f0> >" + " *' at 0x7f0128e6d090> >" ] }, "execution_count": 13, @@ -1157,9 +1151,7 @@ " | !a & b\n", "Cycle:\n", " 0,0\n", - " | !a\t{0}\n", - " 0,0\n", - " | a\t{0,1}" + " | a\t{0}" ] }, "execution_count": 14, @@ -1198,80 +1190,74 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c0f0> >" + " *' at 0x7f0128e6d090> >" ] }, "metadata": {}, @@ -1336,7 +1322,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c6f0> >" + " *' at 0x7f0128e6d8a0> >" ] }, "metadata": {}, @@ -1391,7 +1377,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c2a0> >" + " *' at 0x7f0128e6d780> >" ] }, "metadata": {}, @@ -1623,7 +1609,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c9f0> >" + " *' at 0x7f0128e6db40> >" ] }, "metadata": {}, @@ -1711,7 +1697,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7ca50> >" + " *' at 0x7f0128e6dba0> >" ] }, "metadata": {}, @@ -1808,7 +1794,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7c510> >" + " *' at 0x7f0128e6d180> >" ] }, "metadata": {}, @@ -1976,7 +1962,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7cb70> >" + " *' at 0x7f0128e6dc30> >" ] }, "execution_count": 18, @@ -2144,7 +2130,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7cb70> >" + " *' at 0x7f0128e6dc30> >" ] }, "execution_count": 19, @@ -2307,7 +2293,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f65e4b7cb70> >" + " *' at 0x7f0128e6dc30> >" ] }, "metadata": {}, @@ -2771,6 +2757,13 @@ "spot.highlight_languages(aut)\n", "aut.show('.bas')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index cfdd6e714..afe02367e 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -39,68 +39,53 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -204,204 +189,223 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "0,1\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "2,0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "2,1\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -416,7 +420,7 @@ } ], "source": [ - "a1 = spot.translate('X(a W b)')\n", + "a1 = spot.translate('FGa')\n", "a2 = spot.translate('G(Fc U b)')\n", "prod = spot.product(a1, a2)\n", "display_inline(a1, a2, prod)" @@ -447,68 +451,53 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -604,204 +593,223 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "0,1\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "2,0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "2,1\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -855,68 +863,53 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -1012,167 +1005,189 @@ "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", @@ -1252,7 +1267,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "(a, b)\n", + "(a,)\n", "(c, b)\n", "()\n" ] @@ -1297,68 +1312,53 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -1454,204 +1454,223 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -1668,7 +1687,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "(a, b, c)\n" + "(a, c, b)\n" ] } ], @@ -1742,9 +1761,9 @@ "name": "stdout", "output_type": "stream", "text": [ + "maybe\n", "yes\n", - "yes\n", - "yes\n", + "maybe\n", "maybe\n" ] } @@ -1844,68 +1863,53 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", + "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2001,204 +2005,223 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "0,1\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "2,0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "2,1\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2215,7 +2238,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "yes\n" + "maybe\n" ] } ], @@ -2291,218 +2314,234 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "a & !b & !c\n", "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", "\n", "\n", "" @@ -2518,11 +2557,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "0: (1, 0)\n", - "1: (0, 0)\n", - "2: (0, 1)\n", - "3: (2, 0)\n", - "4: (2, 1)\n" + "0: (0, 0)\n", + "1: (0, 1)\n", + "2: (1, 0)\n", + "3: (1, 1)\n" ] } ], @@ -2551,7 +2589,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "409 µs ± 6.68 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" + "264 µs ± 2.11 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" ] } ], @@ -2568,7 +2606,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "7.02 µs ± 98.5 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" + "4.9 µs ± 45.2 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" ] } ], @@ -2584,6 +2622,22 @@ "\n", "Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++." ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# The case of weak automata\n", + "\n", + "Finally, note that `spot.product()` actually does a bit more: it has some specializations for when one of the argument of the product is marked as weak (as indicated by `prop_weak()`). In this case, the resulting acceptance condition can be simplified a bit." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": {