From 7a65bdf6bc381ce57b96b1bddfaa51a9cfd296fc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 28 Mar 2018 10:32:38 +0200 Subject: [PATCH] specialized translation for GF(guarantee) and FG(safety) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This is adapted from a proposition in a paper by J. Esparza, J. Křentínský, and S. Sickert, submitted to LICS'18. We should add proper references to the code and documentation once that paper is accepted. * spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh: New files. * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them. * spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr. * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it possible to call finalize() from the translator subclass. Constify all the do_* functions while we are there. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add a "gf-guarantee" option to decide whether to use the new translation. * bin/spot-x.cc: Document it. * tests/core/dca2.test, tests/core/genltl.test, tests/core/ltl2tgba2.test, tests/core/parity2.test, tests/core/satmin.test, tests/python/automata.ipynb, tests/python/sbacc.py: Adjust test cases. * tests/python/except.py: Add a couple more tests. --- NEWS | 13 + bin/spot-x.cc | 10 +- python/spot/impl.i | 2 + spot/twa/fwd.hh | 5 +- spot/twaalgos/Makefile.am | 2 + spot/twaalgos/gfguarantee.cc | 193 ++ spot/twaalgos/gfguarantee.hh | 96 + spot/twaalgos/postproc.cc | 71 +- spot/twaalgos/postproc.hh | 13 +- spot/twaalgos/translate.cc | 40 +- spot/twaalgos/translate.hh | 4 +- tests/core/dca2.test | 7 +- tests/core/genltl.test | 10 +- tests/core/ltl2tgba2.test | 6 +- tests/core/parity2.test | 400 +++- tests/core/satmin.test | 4 +- tests/python/automata.ipynb | 4174 +++++++++++++++++++--------------- tests/python/except.py | 12 + tests/python/sbacc.py | 10 +- 19 files changed, 3140 insertions(+), 1932 deletions(-) create mode 100644 spot/twaalgos/gfguarantee.cc create mode 100644 spot/twaalgos/gfguarantee.hh diff --git a/NEWS b/NEWS index 62c838c6b..48b5d1bfd 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,19 @@ New in spot 2.5.2.dev (not yet released) simplified to {1} or {SERE} depending on whether SERE accepts the empty word or not. + - gf_guarantee_to_ba() is a specialized construction for + translating formulas of the form GF(guarantee) to BA or DBA, + and fg_safety_to_dca() is a specialized construction for + translating formulas of the form FG(safety) to DCA. These + are slight generalizations of some constructions proposed + by J. Esparza, J. Křentínský, and S. Sickert in a submitted + paper. + + These are now used by the main translation routine, and can be + disabled by passing -x '!gf-guarantee' to ltl2tgba. As an + example, the translation of GF(a <-> XXb) to transition-based + Büchi went from 9 to 5 states using that construction. + Bugs fixed: - "autfilt --cobuchi --small/--det" would turn a transition-based diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 511ff49d3..d5b23ffa3 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -107,6 +107,14 @@ the determinization algorithm.") }, the determinization algorithm.") }, { DOC("det-stutter", "Set to 0 to disable optimizations based on \ the stutter-invariance in the determinization algorithm.") }, + // FIXME: Add bibliographic reference to their paper ASAP. + { DOC("gf-guarantee", "Set to 0 to disable alternate constructions \ +for GF(guarantee)->[D]BA and FG(safety)->DCA. Those constructions \ +are based on work by J. Esparza, J. Křentínský, and S. Sickert. \ +This is enabled by default for medium and high optimization \ +levels. Unless we are building deterministic automata, the \ +resulting automata are compared to the automata built using the \ +more traditional pipeline, and only kept if they are better.") }, { DOC("simul", "Set to 0 to disable simulation-based reductions. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ diff --git a/python/spot/impl.i b/python/spot/impl.i index 9043c6676..9be7eb296 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -131,6 +131,7 @@ #include #include #include +#include #include #include #include @@ -571,6 +572,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twa/fwd.hh b/spot/twa/fwd.hh index 5318e940f..4563f8766 100644 --- a/spot/twa/fwd.hh +++ b/spot/twa/fwd.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// 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. @@ -23,6 +23,9 @@ namespace spot { + class bdd_dict; + typedef std::shared_ptr bdd_dict_ptr; + class twa; typedef std::shared_ptr twa_ptr; typedef std::shared_ptr const_twa_ptr; diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 500115a51..daff17f09 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -49,6 +49,7 @@ twaalgos_HEADERS = \ dualize.hh \ emptiness.hh \ emptiness_stats.hh \ + gfguarantee.hh \ gv04.hh \ hoa.hh \ iscolored.hh \ @@ -114,6 +115,7 @@ libtwaalgos_la_SOURCES = \ dtwasat.cc \ dualize.cc \ emptiness.cc \ + gfguarantee.cc \ gv04.cc \ hoa.cc \ iscolored.cc \ diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc new file mode 100644 index 000000000..9b43c6a0e --- /dev/null +++ b/spot/twaalgos/gfguarantee.cc @@ -0,0 +1,193 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "config.h" +#include "gfguarantee.hh" +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + // F(φ₁)&F(φ₂)&F(φ₃) ≡ F(φ₁ & F(φ₂ & F(φ₃)) + // because we assume this is all under G. + static formula + nest_f(formula input) + { + assert(input.is(op::And)); + formula res = formula::tt(); + unsigned n = input.size(); + do + { + --n; + assert(input[n].is(op::F)); + res = formula::F(formula::And({input[n][0], res})); + } + while (n); + return res; + } + + + static twa_graph_ptr + do_g_f_terminal_inplace(scc_info& si, bool state_based) + { + twa_graph_ptr aut = std::const_pointer_cast(si.get_aut()); + + if (!is_terminal_automaton(aut, &si, true)) + throw std::runtime_error("g_f_terminal() expects a terminal automaton"); + + unsigned ns = si.scc_count(); + std::vector term(ns, false); + for (unsigned n = 0; n < ns; ++n) + if (is_terminal_scc(si, n)) + term[n] = true; + + aut->prop_keep({ false, false, true, false, true, true }); + aut->prop_state_acc(state_based); + aut->prop_inherently_weak(false); + aut->set_buchi(); + + unsigned init = aut->get_init_state_number(); + + if (!state_based) + { + for (auto& e: aut->edges()) + if (term[si.scc_of(e.dst)]) + { + e.dst = init; + e.acc = {0}; + } + else + { + e.acc = {}; + } + } + else + { + // Replace all terminal state by a single accepting state. + unsigned accstate = aut->new_state(); + for (auto& e: aut->edges()) + { + if (term[si.scc_of(e.dst)]) + e.dst = accstate; + e.acc = {}; + } + // This accepting state has the same output as the initial + // state. + for (auto& e: aut->out(init)) + aut->new_edge(accstate, e.dst, e.cond, {0}); + // This is not mandatory, but starting on the accepting + // state helps getting shorter accepting words. + aut->set_init_state(accstate); + } + + aut->purge_unreachable_states(); + return aut; + } + } + + twa_graph_ptr + g_f_terminal_inplace(twa_graph_ptr aut, bool state_based) + { + scc_info si(aut); + return do_g_f_terminal_inplace(si, state_based); + } + + twa_graph_ptr + gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict, + bool deterministic, bool state_based) + { + if (!gf.is(op::G)) + return nullptr; + formula f = gf[0]; + if (!f.is(op::F)) + { + // F(...)&F(...)&... is also OK. + if (!f.is(op::And)) + return nullptr; + for (auto c: f) + if (!c.is(op::F)) + return nullptr; + + f = nest_f(f); + } + twa_graph_ptr aut = ltl_to_tgba_fm(f, dict, true); + twa_graph_ptr reduced = minimize_obligation(aut, f, nullptr, + !deterministic); + scc_info si(reduced); + if (!is_terminal_automaton(aut, &si, true)) + return nullptr; + do_g_f_terminal_inplace(si, state_based); + return reduced; + } + + twa_graph_ptr + gf_guarantee_to_ba(formula gf, const bdd_dict_ptr& dict, + bool deterministic, bool state_based) + { + twa_graph_ptr res = gf_guarantee_to_ba_maybe(gf, dict, + deterministic, state_based); + if (!res) + throw std::runtime_error + ("gf_guarantee_to_ba(): expects a formula of the form GF(guarantee)"); + return res; + } + + twa_graph_ptr + fg_safety_to_dca_maybe(formula fg, const bdd_dict_ptr& dict, + bool state_based) + { + if (!fg.is(op::F)) + return nullptr; + formula g = fg[0]; + if (!g.is(op::G)) + { + // G(...)|G(...)|... is also OK. + if (!g.is(op::Or)) + return nullptr; + for (auto c: g) + if (!c.is(op::G)) + return nullptr; + } + + formula gf = negative_normal_form(fg, true); + twa_graph_ptr res = + gf_guarantee_to_ba_maybe(gf, dict, true, state_based); + if (!res) + return nullptr; + return dualize(res); + } + + twa_graph_ptr + fg_safety_to_dca(formula gf, const bdd_dict_ptr& dict, + bool state_based) + { + twa_graph_ptr res = fg_safety_to_dca_maybe(gf, dict, state_based); + if (!res) + throw std::runtime_error + ("fg_safety_to_dca(): expects a formula of the form FG(safety)"); + return res; + } +} diff --git a/spot/twaalgos/gfguarantee.hh b/spot/twaalgos/gfguarantee.hh new file mode 100644 index 000000000..97611dbdb --- /dev/null +++ b/spot/twaalgos/gfguarantee.hh @@ -0,0 +1,96 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include +#include +#include +#include + +namespace spot +{ + /// \ingroup twa_misc + /// \brief Given a terminal automaton \a f_terminal recognizing + /// some formula F(φ), modify it to recognize GF(φ). + /// + /// If \a state_based is set, the automaton all terminal states are + /// replaced by a unique accepting state that has the same outgoing + /// transitions as the initial state, and the initial state is + /// actually relocated to that accepting state. The latter point is + /// not necessary, but it favors shorter accepting cycles. + /// + /// If \a state_based is not set, all transition going to terminal + /// states are made accepting and redirected to the initial state. + /// + /// This construction is inspired by a similar construction in a + /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert. + SPOT_API twa_graph_ptr + g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false); + + /// \ingroup twa_ltl + /// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property. + /// + /// If the formula \a gf has the form GΦ where Φ matches either F(φ) + /// or F(φ₁)|F(φ₂)|...|F(φₙ), we translate Φ into A_Φ and attempt to + /// minimize it to a WDBA. If \a deterministic is not set, we keep + /// the minimized automaton only if A_Φ is larger. If the resulting + /// automaton is terminal, we then call g_f_terminal_inplace(). + /// + /// Return nullptr if the input formula is not of the supported + /// form. + /// + /// This construction generalized a similar construction in a + /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert in the + /// sense that it will work if Φ represent a safety property, even + /// if it is not a syntactic safety. + SPOT_API twa_graph_ptr + gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict, + bool deterministic = true, bool state_based = false); + + /// \ingroup twa_ltl + /// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property. + /// + /// This is similar to gf_guarantee_to_ba_maybe() except it raises + /// an exception of the input formula is not of the supported form. + SPOT_API twa_graph_ptr + gf_guarantee_to_ba(formula gf, const bdd_dict_ptr& dict, + bool deterministic = true, bool state_based = false); + + /// \ingroup twa_ltl + /// \brief Convert FG(φ) into a DCA if φ is a safety property. + /// + /// This is the dual of gf_guarantee_to_ba_maybe(). See that + /// function for details. + /// + /// Return nullptr if the input formula is not of the supported + /// form. + SPOT_API twa_graph_ptr + fg_safety_to_dca_maybe(formula fg, const bdd_dict_ptr& dict, + bool state_based); + + /// \ingroup twa_ltl + /// \brief Convert FG(φ) into a DCA if φ is a safety property. + /// + /// This is similar to fg_safety_to_dba_maybe() except it raises + /// an exception of the input formula is not of the supported form. + SPOT_API twa_graph_ptr + fg_safety_to_dca(formula fg, const bdd_dict_ptr& dict, + bool state_based = false); +} diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index b443481df..4ad5a8b8b 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -105,7 +105,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_simul(const twa_graph_ptr& a, int opt) + postprocessor::do_simul(const twa_graph_ptr& a, int opt) const { if (!has_separate_sets(a)) return a; @@ -124,7 +124,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt) + postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt) const { if (ba_simul_ <= 0) return a; @@ -143,7 +143,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_degen(const twa_graph_ptr& a) + postprocessor::do_degen(const twa_graph_ptr& a) const { auto d = degeneralize(a, degen_reset_, degen_order_, @@ -153,7 +153,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_degen_tba(const twa_graph_ptr& a) + postprocessor::do_degen_tba(const twa_graph_ptr& a) const { return degeneralize_tba(a, degen_reset_, degen_order_, @@ -162,7 +162,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) + postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const { if (scc_filter_ == 0) return a; @@ -176,7 +176,7 @@ namespace spot } twa_graph_ptr - postprocessor::do_scc_filter(const twa_graph_ptr& a) + postprocessor::do_scc_filter(const twa_graph_ptr& a) const { return do_scc_filter(a, scc_filter_ > 1); } @@ -186,6 +186,36 @@ namespace spot #define SBACC_ (pref_ & SBAcc) #define COLORED_ (pref_ & Colored) + + twa_graph_ptr + postprocessor::finalize(twa_graph_ptr tmp) const + { + if (COMP_) + tmp = complete(tmp); + bool want_parity = type_ & Parity; + if (want_parity && tmp->acc().is_generalized_buchi()) + tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp); + if (SBACC_) + tmp = sbacc(tmp); + if (want_parity) + { + if (COLORED_) + colorize_parity_here(tmp); + parity_kind kind = parity_kind_any; + parity_style style = parity_style_any; + if ((type_ & ParityMin) == ParityMin) + kind = parity_kind_min; + else if ((type_ & ParityMax) == ParityMax) + kind = parity_kind_max; + if ((type_ & ParityOdd) == ParityOdd) + style = parity_style_odd; + else if ((type_ & ParityEven) == ParityEven) + style = parity_style_even; + change_parity_here(tmp, kind, style); + } + return tmp; + } + twa_graph_ptr postprocessor::run(twa_graph_ptr a, formula f) { @@ -199,38 +229,11 @@ namespace spot state_based_ = true; bool via_gba = (type_ == BA) || (type_ == TGBA) || (type_ == Monitor); - bool want_parity = (type_ & Parity) == Parity; + bool want_parity = type_ & Parity; if (COLORED_ && !want_parity) throw std::runtime_error("postprocessor: the Colored setting only works " "for parity acceptance"); - auto finalize = [&](twa_graph_ptr tmp) - { - if (COMP_) - tmp = complete(tmp); - if (want_parity && tmp->acc().is_generalized_buchi()) - tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp); - if (SBACC_) - tmp = sbacc(tmp); - if (want_parity) - { - if (COLORED_) - colorize_parity_here(tmp); - parity_kind kind = parity_kind_any; - parity_style style = parity_style_any; - if ((type_ & ParityMin) == ParityMin) - kind = parity_kind_min; - else if ((type_ & ParityMax) == ParityMax) - kind = parity_kind_max; - if ((type_ & ParityOdd) == ParityOdd) - style = parity_style_odd; - else if ((type_ & ParityEven) == ParityEven) - style = parity_style_even; - change_parity_here(tmp, kind, style); - } - return tmp; - }; - if (!a->is_existential() && // We will probably have to revisit this condition later. // Currently, the intent is that postprocessor should never diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index fd2f48a0f..948b49b96 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -219,12 +219,13 @@ namespace spot twa_graph_ptr run(twa_graph_ptr input, formula f = nullptr); protected: - twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); - twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); - twa_graph_ptr do_degen(const twa_graph_ptr& input); - twa_graph_ptr do_degen_tba(const twa_graph_ptr& input); - twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); - twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); + twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt) const; + twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt) const; + twa_graph_ptr do_degen(const twa_graph_ptr& input) const; + twa_graph_ptr do_degen_tba(const twa_graph_ptr& input) const; + twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg) const; + twa_graph_ptr do_scc_filter(const twa_graph_ptr& a) const; + twa_graph_ptr finalize(twa_graph_ptr tmp) const; output_type type_ = TGBA; int pref_ = Small; diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index d8fb14f3e..bd8277c7c 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -24,6 +24,8 @@ #include #include #include +#include +#include namespace spot { @@ -32,6 +34,7 @@ namespace spot { comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; relabel_bool_ = tls_impl_ = -1; + gf_guarantee_ = level_ != Low; if (!opt) return; @@ -45,6 +48,7 @@ namespace spot skel_simul_ = opt->get("skel-simul", 1); } tls_impl_ = opt->get("tls-impl", -1); + gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_); } void translator::build_simplifier(const bdd_dict_ptr& dict) @@ -96,6 +100,8 @@ namespace spot twa_graph_ptr translator::run(formula* f) { +#define PREF_ (pref_ & (Small | Deterministic)) + bool unambiguous = (pref_ & postprocessor::Unambiguous); if (unambiguous && type_ == postprocessor::Monitor) { @@ -153,12 +159,13 @@ namespace spot simpl_->clear_as_bdd_cache(); twa_graph_ptr aut; + twa_graph_ptr aut2 = nullptr; if (comp_susp_ > 0) { // FIXME: Handle unambiguous_ automata? int skel_wdba = skel_wdba_; if (skel_wdba < 0) - skel_wdba = (pref_ == postprocessor::Deterministic) ? 1 : 2; + skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2; aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0, skel_simul_ == 0, early_susp_ != 0, @@ -166,6 +173,24 @@ namespace spot } else { + if (gf_guarantee_ && PREF_ != Any) + { + bool det = unambiguous || (PREF_ == Deterministic); + bool sba = type_ == BA || (pref_ & SBAcc); + if ((type_ & (BA | Parity | Generic)) || type_ == TGBA) + aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), det, sba); + if (aut2 && (type_ & (BA | Parity)) && (pref_ & Deterministic)) + return finalize(aut2); + if (!aut2 && (type_ & (Generic | Parity | CoBuchi))) + { + aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); + if (aut2 + && (type_ & (CoBuchi | Parity)) + && (pref_ & Deterministic)) + return finalize(aut2); + } + } + bool exprop = unambiguous || level_ == postprocessor::High; aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop, true, false, false, nullptr, nullptr, @@ -173,6 +198,18 @@ namespace spot } aut = this->postprocessor::run(aut, r); + if (aut2) + { + aut2 = this->postprocessor::run(aut2, r); + unsigned s2 = aut2->num_states(); + unsigned s1 = aut->num_states(); + bool d2_more_det = !is_deterministic(aut) && is_deterministic(aut2); + if (((PREF_ == Deterministic) && d2_more_det) + || (s2 < s1) + || (s2 == s1 + && ((aut2->num_sets() < aut2->num_sets()) || d2_more_det))) + aut = std::move(aut2); + } if (!m.empty()) relabel_here(aut, &m); @@ -188,5 +225,4 @@ namespace spot { simpl_->clear_caches(); } - } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 271f72ee3..10eecf908 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -148,6 +148,8 @@ namespace spot int skel_simul_; int relabel_bool_; int tls_impl_; + bool gf_guarantee_; }; /// @} + } diff --git a/tests/core/dca2.test b/tests/core/dca2.test index e14c87ee2..ce0093c72 100755 --- a/tests/core/dca2.test +++ b/tests/core/dca2.test @@ -53,7 +53,8 @@ EOF while read l_f; do ltl2tgba --parity='max odd' "$l_f" > l.hoa - autfilt -q --acceptance-is='Fin(0) | Inf(1)' l.hoa + autfilt -q --acceptance-is='Fin(0) | Inf(1)' l.hoa || + autfilt -q --acceptance-is='Fin(0)' l.hoa while read r_f; do # Dualizing a deterministic transition-based parity automaton # to obtain a transition-based deterministic streett @@ -63,10 +64,10 @@ while read l_f; do ltl2tgba "$r_f" -D --parity='min odd' | autfilt --dualize --gsa > r.hoa # Streett & Streett autfilt r.hoa --name="($l_f)&!($r_f)" --product=l.hoa -S > and.hoa - autfilt -q --acceptance-is=Streett and.hoa + autfilt -q --acceptance-is=Streett-like and.hoa # Streett | Streett autfilt r.hoa --name="($l_f)|!($r_f)" --product-or=l.hoa -S > or.hoa - autfilt -q -v --acceptance-is=Streett or.hoa + autfilt -q -v --acceptance-is=Streett-like or.hoa autcross --language-preserved --verbose -F or.hoa -F and.hoa \ 'autfilt %H --stats=%M | ltl2tgba >%O' \ diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 0250bd346..ff8bbc429 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -150,11 +150,11 @@ ms-phi-r=2,29 ms-phi-s=0,5 ms-phi-s=1,8 ms-phi-s=2,497 -ms-phi-h=0,2 -ms-phi-h=1,4 -ms-phi-h=2,21 -ms-phi-h=3,170 -ms-phi-h=4,1816 +ms-phi-h=0,1 +ms-phi-h=1,3 +ms-phi-h=2,7 +ms-phi-h=3,15 +ms-phi-h=4,31 gf-equiv=0,1 gf-equiv=1,4 gf-equiv=2,8 diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index f88e5dd73..e249d228e 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -132,8 +132,8 @@ sb-patterns,26, 1,1, 1,1, 1,1, 1,1 sb-patterns,27, 2,7, 2,7, 2,7, 2,7 hkrss-patterns,1, 1,2, 1,2, 3,6, 3,6 hkrss-patterns,2, 1,2, 1,2, 3,6, 3,6 -hkrss-patterns,3, 5,36, 5,36, 5,36, 5,36 -hkrss-patterns,4, 9,400, 9,400, 9,400, 9,400 +hkrss-patterns,3, 5,20, 5,20, 5,20, 5,20 +hkrss-patterns,4, 9,400, 17,272, 9,400, 17,272 hkrss-patterns,6, 1,2, 1,2, 3,6, 3,6 hkrss-patterns,7, 2,8, 2,8, 2,8, 2,8 hkrss-patterns,8, 1,1, 1,1, 1,1, 1,1 diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 3759c93bc..09b7d3189 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -33,6 +33,203 @@ done cat >expected<expected2<expected3<expected2<expected4<expected <<'EOF' "!(G((p0) -> ((p1) U (p2))))","15",3 "!(G((p0) -> ((p1) U (p2))))","16",3 "!(G((p0) -> ((p1) U (p2))))","17",3 -"G(F((p0) <-> (X(X(p1)))))","1",9 +"G(F((p0) <-> (X(X(p1)))))","1",7 "G(F((p0) <-> (X(X(p1)))))","2",7 "G(F((p0) <-> (X(X(p1)))))","3",4 "G(F((p0) <-> (X(X(p1)))))","4",4 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index c13ea1afd..745ae3752 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -29,124 +29,142 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "2->1\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100253060> >" + " *' at 0x7fde206230c0> >" ] }, "execution_count": 2, @@ -174,113 +192,131 @@ "data": { "image/svg+xml": [ "\n", - "\n", + "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "2->1\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!c\n", "\n", "\n", "" @@ -313,128 +349,149 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c & d\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!d\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c & d\n", + "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "2->1\n", + "\n", + "\n", + "c & d\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "2->2\n", + "\n", + "\n", + "!d\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "" @@ -493,55 +550,61 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb1002c4fc0> >" + " *' at 0x7fde2053ec60> >" ] }, "execution_count": 6, @@ -564,55 +627,61 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10017ff90> >" + " *' at 0x7fde2053ed50> >" ] }, "execution_count": 7, @@ -642,55 +711,61 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb1002029f0> >" + " *' at 0x7fde2053e870> >" ] }, "execution_count": 8, @@ -743,72 +818,83 @@ "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "c\n", + "\n", + "0->3\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "3->3\n", + "\n", + "\n", + "c\n", "\n", "\n", "" @@ -834,172 +920,199 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "6\n", - "\n", - "\n", - "6\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", "\n", "\n", - "I->6\n", - "\n", - "\n", + "\n", + "I->6\n", + "\n", + "\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", - "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "6->1\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", - "2\n", - "\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", "\n", "\n", - "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", - "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "4\n", - "\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "5\n", - "\n", - "\n", - "5\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", "\n", "\n", - "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "6->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "0->0\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", "\n", "\n", - "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "5->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "" @@ -1035,128 +1148,146 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "0->2\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "2->2\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "3->2\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190660> >" + " *' at 0x7fde2055f840> >" ] }, "execution_count": 12, @@ -1186,82 +1317,92 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190240> >" + " *' at 0x7fde2055f4e0> >" ] }, "execution_count": 13, @@ -1291,96 +1432,109 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "2\n", - "\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "b\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190600> >" + " *' at 0x7fde2055f9c0> >" ] }, "execution_count": 14, @@ -1410,80 +1564,90 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "2->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb1001908a0> >" + " *' at 0x7fde2055f870> >" ] }, "execution_count": 15, @@ -1506,458 +1670,530 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "5\n", - "\n", - "5\n", + "\n", + "5\n", + "\n", + "5\n", "\n", "\n", - "0->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "0->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "6\n", - "\n", - "6\n", + "\n", + "6\n", + "\n", + "6\n", "\n", "\n", - "0->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "1->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "1->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "4->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "4->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "7\n", - "\n", - "7\n", + "\n", + "7\n", + "\n", + "7\n", "\n", "\n", - "5->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "5->7\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "8\n", - "\n", - "8\n", + "\n", + "8\n", + "\n", + "8\n", "\n", "\n", - "5->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "5->8\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "6->7\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "6->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "6->8\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "7->7\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "9\n", - "\n", - "9\n", + "\n", + "9\n", + "\n", + "9\n", "\n", "\n", - "7->9\n", - "\n", - "\n", - "a & b\n", + "\n", + "7->9\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "10\n", - "\n", - "10\n", + "\n", + "10\n", + "\n", + "10\n", "\n", "\n", - "7->10\n", - "\n", - "\n", - "!a & b\n", + "\n", + "7->10\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "8->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "8->8\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "8->9\n", - "\n", - "\n", - "a & b\n", + "\n", + "8->9\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "8->10\n", - "\n", - "\n", - "!a & b\n", + "\n", + "8->10\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "9->9\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "9->9\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "9->10\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "9->10\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", - "11\n", - "\n", - "11\n", + "\n", + "11\n", + "\n", + "11\n", "\n", "\n", - "9->11\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "9->11\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "12\n", - "\n", - "12\n", + "\n", + "12\n", + "\n", + "12\n", "\n", "\n", - "9->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "9->12\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "10->9\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "10->9\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "10->10\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "10->10\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", - "10->11\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "10->11\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "10->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "10->12\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "11->9\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "11->9\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "11->10\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "11->10\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", - "11->11\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "11->11\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "11->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "11->12\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "12->9\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "12->9\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "12->10\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "12->10\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", - "12->11\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "12->11\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "12->12\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "12->12\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10016f9f0> >" + " *' at 0x7fde2055f990> >" ] }, "execution_count": 16, @@ -2044,119 +2280,132 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 361.00 178.45\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190a20> >" + " *' at 0x7fde2055f090> >" ] }, "metadata": {}, @@ -2168,130 +2417,146 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 410.50 188.51\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ") | Inf(\n", - "\n", - ") | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - "))\n", - "[Fin-less 4]\n", + "\n", + "Inf(\n", + "\n", + ") | Inf(\n", + "\n", + ") | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "[Fin-less 4]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100248e10> >" + " *' at 0x7fde2053ea50> >" ] }, "metadata": {}, @@ -2303,147 +2568,168 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!b\n", + "\n", + "1->4\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b\n", + "\n", + "2->4\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a | b\n", + "\n", + "3->4\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10016fb70> >" + " *' at 0x7fde2055fc60> >" ] }, "metadata": {}, @@ -2455,149 +2741,171 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "4\n", - "\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & b\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5\n", - "\n", - "\n", - "5\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "2->5\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!a & b\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "4->0\n", - "\n", - "\n", - "!b\n", + "\n", + "4->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100248e10> >" + " *' at 0x7fde2055fb70> >" ] }, "metadata": {}, @@ -2632,142 +2940,159 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 376.00 186.64\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "2->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190de0> >" + " *' at 0x7fde2055ff00> >" ] }, "execution_count": 21, @@ -2790,55 +3115,61 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb100190d20> >" + " *' at 0x7fde2055ff90> >" ] }, "execution_count": 22, @@ -2861,46 +3192,52 @@ "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "c\n", + "\n", + "1->0\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -2919,44 +3256,50 @@ "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -2975,102 +3318,116 @@ "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")&Inf(\n", + ")&Inf(\n", "\n", - ")\n", - "[gen. Büchi 2]\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "1,1\n", + "\n", + "0\n", + "\n", + "1,1\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", - "1\n", - "\n", - "0,0\n", + "\n", + "1\n", + "\n", + "0,0\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", - "2\n", - "\n", - "0,1\n", + "\n", + "2\n", + "\n", + "0,1\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", - "3\n", - "\n", - "1,0\n", + "\n", + "3\n", + "\n", + "1,0\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "b\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", @@ -3090,102 +3447,116 @@ "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")&Inf(\n", + ")&Inf(\n", "\n", - ")\n", - "[gen. Büchi 2]\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "b\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", @@ -3227,58 +3598,64 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10019c990> >" + " *' at 0x7fde2053eae0> >" ] }, "metadata": {}, @@ -3311,68 +3688,75 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10019c1b0> >" + " *' at 0x7fde2055f780> >" ] }, "execution_count": 25, @@ -3402,68 +3786,51 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "1\n", - "\n", - "1\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", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10019ca20> >" + " *' at 0x7fde2056bc30> >" ] }, "execution_count": 26, @@ -3472,14 +3839,14 @@ } ], "source": [ - "aut = spot.translate('FGa', 'generic', 'deterministic'); aut" + "spot.translate('FGa', 'generic', 'deterministic')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Translation to co-Büchi automaton" + "Translation to state-based co-Büchi automaton" ] }, { @@ -3490,48 +3857,61 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", "" @@ -3546,7 +3926,14 @@ } ], "source": [ - "spot.translate('FGa', 'coBuchi').show('.b')" + "spot.translate('FGa', 'coBuchi', 'deterministic', 'sbacc').show('.b')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Translation to parity automaton. Specifying just `parity max odd` requires a parity acceptance. Adding `colored` ensures that each transition (or state if `sbacc` is also given) has a color, as people usually expect in parity automata." ] }, { @@ -3557,61 +3944,59 @@ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "" + "\n" ], "text/plain": [ - "" + " *' at 0x7fde2056b270> >" ] }, "execution_count": 28, @@ -3620,7 +4005,7 @@ } ], "source": [ - "spot.translate('FGa', 'coBuchi', 'deterministic').show('.b')" + "spot.translate('FGa', 'parity max odd', 'colored')" ] }, { @@ -3641,81 +4026,146 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & b\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10019ca20> >" + " *' at 0x7fde2053eae0> >" ] }, - "execution_count": 29, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\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", + "b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fde2053eae0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ "import buddy\n", - "b = buddy.bdd_ithvar(aut.register_ap('b'))\n", - "for e in aut.edges():\n", + "display(a)\n", + "b = buddy.bdd_ithvar(a.register_ap('b'))\n", + "for e in a.edges():\n", " e.cond &= b\n", - "aut" + "display(a)" ] }, { @@ -3736,68 +4186,64 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & b\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb10019ca20> >" + " *' at 0x7fde2053eae0> >" ] }, "execution_count": 30, @@ -3806,11 +4252,11 @@ } ], "source": [ - "c = buddy.bdd_ithvar(aut.register_ap('c'))\n", - "for e in aut.out(0):\n", + "c = buddy.bdd_ithvar(a.register_ap('c'))\n", + "for e in a.out(0):\n", " if e.dst == 1:\n", " e.cond &= c\n", - "aut" + "a" ] } ], @@ -3830,7 +4276,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4+" + "version": "3.6.5rc1" } }, "nbformat": 4, diff --git a/tests/python/except.py b/tests/python/except.py index 12687ec6a..d8b50af27 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -75,3 +75,15 @@ try: a = r.reduce() except RuntimeError as e: assert "empty cycle" in str(e) + +f = spot.formula('GF(a | Gb)') +try: + spot.gf_guarantee_to_ba(f, spot._bdd_dict) +except RuntimeError as e: + assert "guarantee" in str(e) + +f = spot.formula('FG(a | Fb)') +try: + spot.fg_safety_to_dca(f, spot._bdd_dict) +except RuntimeError as e: + assert "safety" in str(e) diff --git a/tests/python/sbacc.py b/tests/python/sbacc.py index e4efeb738..b0c457846 100644 --- a/tests/python/sbacc.py +++ b/tests/python/sbacc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -50,12 +50,12 @@ h = s.to_str('hoa') assert h == """HOA: v1 States: 2 Start: 0 -AP: 2 "b" "a" +AP: 2 "a" "b" Acceptance: 2 Inf(0) | Inf(1) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 -[1] 1 +[0] 1 State: 1 {1} [t] 1 --END--""" @@ -84,13 +84,13 @@ h = d.to_str('hoa') assert h == """HOA: v1 States: 2 Start: 0 -AP: 2 "b" "a" +AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 -[1] 1 +[0] 1 State: 1 {0} [t] 1 --END--"""