diff --git a/NEWS b/NEWS index 4119127cd..f838b27a0 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,12 @@ New in spot 2.6.0.dev (not yet released) as aut.show_storage() in a Jupyter notebook. See https://spot.lrde.epita.fr/ipynb/twagraph-internals.html + - spot::generic_emptiness_check() is a new function that performs + emptiness checks of twa_graph_ptr (i.e., automata not built + on-the-fly) with an *arbitrary* acceptance condition. Its sister + spot::generic_emptiness_check_scc() can be used to decide the + emptiness of an SCC. + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/python/spot/impl.i b/python/spot/impl.i index 397cf7b0b..6a8772b3a 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -128,6 +128,7 @@ #include #include #include +#include #include #include #include @@ -575,6 +576,7 @@ def state_is_accepting(self, src) -> "bool": %include %template(list_step) std::list; %include +%include %include %include %include diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index f1228b6c8..140dad02f 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -2121,4 +2121,62 @@ namespace spot std::swap(c, *this); } + int acc_cond::acc_code::fin_one() const + { + if (empty() || is_f()) + return -1; + const acc_cond::acc_word* pos = &back(); + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + case acc_cond::acc_op::Fin: + return pos[-1].mark.min_set() - 1; + } + } + while (pos >= &front()); + return -1; + } + + acc_cond::mark_t acc_cond::acc_code::fin_unit() const + { + mark_t res = {}; + if (empty() || is_f()) + return res; + const acc_cond::acc_word* pos = &back(); + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Or: + pos -= pos->sub.size + 1; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + case acc_cond::acc_op::Fin: + auto m = pos[-1].mark; + if (m.count() == 1) + res |= m; + pos -= 2; + break; + } + } + while (pos >= &front()); + return res; + } } diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index c0c1e410f..5820ee138 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -886,6 +886,9 @@ namespace spot acc_code complement() const; + mark_t fin_unit() const; + int fin_one() const; + // Return a list of acceptance marks needed to close a cycle // that already visit INF infinitely often, so that the cycle is // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false). @@ -977,6 +980,12 @@ namespace spot { } + /// \brief Copy a part of another acceptance condition + acc_code(const acc_word* other) + : std::vector(other - other->sub.size, other + 1) + { + } + // Calls to_text SPOT_API friend std::ostream& operator<<(std::ostream& os, const acc_code& code); @@ -1399,6 +1408,16 @@ namespace spot /// 'other', (s) shorthand for 'lo0'. std::string name(const char* fmt = "alo") const; + mark_t fin_unit() const + { + return code_.fin_unit(); + } + + int fin_one() const + { + return code_.fin_one(); + } + protected: mark_t all_sets_() const { diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index e8ee78164..1de39842a 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -50,6 +50,7 @@ twaalgos_HEADERS = \ dualize.hh \ emptiness.hh \ emptiness_stats.hh \ + genem.hh \ gfguarantee.hh \ gv04.hh \ hoa.hh \ @@ -117,6 +118,7 @@ libtwaalgos_la_SOURCES = \ dtwasat.cc \ dualize.cc \ emptiness.cc \ + genem.cc \ gfguarantee.cc \ gv04.cc \ hoa.cc \ diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc new file mode 100644 index 000000000..0bcec63b8 --- /dev/null +++ b/spot/twaalgos/genem.cc @@ -0,0 +1,222 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement +// 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 +#include + +namespace spot +{ + namespace + { + class temporary_acc_set + { + twa_graph_ptr aut_; + acc_cond old_acc_; + + public: + temporary_acc_set(const const_twa_graph_ptr& aut, + acc_cond new_acc) + : aut_(std::const_pointer_cast(aut)), + old_acc_(aut->acc()) + { + set(new_acc); + } + + void set(acc_cond new_acc) + { + aut_->set_acceptance(new_acc); + } + + ~temporary_acc_set() + { + aut_->set_acceptance(old_acc_); + } + }; + + bool scc_split_check(const scc_info& si, unsigned scc, + acc_cond::mark_t tocut, + bool (*ec_scc)(const scc_info& si, + unsigned scc, + acc_cond::mark_t tocut)) + { + struct filter_data_t { + const scc_info& lower_si; + unsigned lower_scc; + acc_cond::mark_t cut_sets; + } + data = {si, scc, tocut}; + + scc_info::edge_filter filter = + [](const twa_graph::edge_storage_t& e, unsigned dst, + void* filter_data) -> scc_info::edge_filter_choice + { + auto& data = *reinterpret_cast(filter_data); + if (data.lower_si.scc_of(dst) != data.lower_scc) + return scc_info::edge_filter_choice::ignore; + if (data.cut_sets & e.acc) + return scc_info::edge_filter_choice::cut; + return scc_info::edge_filter_choice::keep; + }; + + // We want to remove tocut from the acceptance condition right + // now, because hopefully this will convert the acceptance + // condition into a Fin-less one, and then we do not have to + // recurse it. + acc_cond::mark_t sets = si.acc_sets_of(scc) - tocut; + auto& autacc = si.get_aut()->acc(); + acc_cond acc = autacc.restrict_to(sets); + acc = acc.remove(si.common_sets_of(scc), false); + temporary_acc_set tmp(si.get_aut(), acc); + scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data, + scc_info_options::STOP_ON_ACC); + if (upper_si.one_accepting_scc() >= 0) + return false; + if (!acc.uses_fin_acceptance()) + return true; + unsigned nscc = upper_si.scc_count(); + for (unsigned scc = 0; scc < nscc; ++scc) + if (!ec_scc(upper_si, scc, tocut)) + return false; + return true; + } + + template + bool generic_emptiness_check_for_scc_nocopy(const scc_info& si, + unsigned scc, + acc_cond::mark_t + tocut = {}) + { + if (si.is_rejecting_scc(scc)) + return true; + acc_cond::mark_t sets = si.acc_sets_of(scc); + auto& autacc = si.get_aut()->acc(); + acc_cond acc = autacc.restrict_to(sets); + acc = acc.remove(si.common_sets_of(scc), false); + if (acc.is_f()) + return true; + if (acc.is_t()) + return false; + temporary_acc_set tmp(si.get_aut(), acc); + if (acc_cond::mark_t fu = acc.fin_unit()) + return scc_split_check + (si, scc, tocut | fu, + generic_emptiness_check_for_scc_nocopy); + + if (deal_with_disjunct) + { + acc_cond::acc_code& code = acc.get_acceptance(); + assert(!code.empty()); + auto pos = &code.back(); + auto start = &code.front(); + assert(pos - pos->sub.size == start); + if (pos->sub.op == acc_cond::acc_op::Or) + { + do + { + --pos; + if (pos->sub.op != acc_cond::acc_op::Inf) + { + acc_cond::acc_code one(pos); + tmp.set(one); + if (si.get_aut()->acc().uses_fin_acceptance()) + { + acc_cond::mark_t plus = {}; + if (acc_cond::mark_t fu = one.fin_unit()) + plus = fu; + if (!scc_split_check + (si, scc, tocut | plus, + generic_emptiness_check_for_scc_nocopy + )) + return false; + } + } + pos -= pos->sub.size; + } + while (pos > start); + return true; + } + if (pos->sub.op == acc_cond::acc_op::Fin) + { + tmp.set(acc_cond::acc_code()); + for (unsigned d: pos[-1].mark.sets()) + if (!scc_split_check + (si, scc, + tocut | acc_cond::mark_t({d}), + generic_emptiness_check_for_scc_nocopy + )) + return false; + return true; + } + } + + int fo = acc.fin_one(); + assert(fo >= 0); + // Try to accept when Fin(fo) == true + if (!scc_split_check + (si, scc, tocut | acc_cond::mark_t({(unsigned) fo}), + generic_emptiness_check_for_scc_nocopy + )) + return false; + // Try to accept when Fin(fo) == false + tmp.set(acc.remove({(unsigned) fo}, false)); + return generic_emptiness_check_for_scc_nocopy + (si, scc, tocut); + return true; + } + + template + bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut) + { + cleanup_acceptance_here(aut, false); + auto& aut_acc = aut->acc(); + if (aut_acc.is_f()) + return true; + if (!aut->acc().uses_fin_acceptance()) + return aut->is_empty(); + + scc_info si(aut, scc_info_options::STOP_ON_ACC + | scc_info_options::TRACK_STATES); + if (si.one_accepting_scc() >= 0) + return false; + + unsigned nscc = si.scc_count(); + for (unsigned scc = 0; scc < nscc; ++scc) + if (!generic_emptiness_check_for_scc_nocopy + (si, scc)) + return false; + return true; + } + } + + bool generic_emptiness_check(const const_twa_graph_ptr& aut) + { + auto aut_ = std::const_pointer_cast(aut); + acc_cond old = aut_->acc(); + bool res = generic_emptiness_check_main_nocopy(aut_); + aut_->set_acceptance(old); + return res; + } + + bool generic_emptiness_check_for_scc(const scc_info& si, + unsigned scc) + { + return generic_emptiness_check_for_scc_nocopy(si, scc); + } +} diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh new file mode 100644 index 000000000..76957ac8e --- /dev/null +++ b/spot/twaalgos/genem.hh @@ -0,0 +1,35 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement +// 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 + +namespace spot +{ + /// \ingroup emptiness_check_algorithms + /// \brief Emptiness check of on automaton, for any acceptance condition. + SPOT_API bool + generic_emptiness_check(const const_twa_graph_ptr& aut); + + /// \ingroup emptiness_check_algorithms + /// \brief Emptiness check of one SCC, for any acceptance condition. + SPOT_API bool + generic_emptiness_check_for_scc(const scc_info& si, unsigned scc); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 6b2b0501e..0f6f72bdd 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -375,6 +375,7 @@ TESTS_python = \ python/dualize.py \ python/except.py \ python/gen.py \ + python/genem.py \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/genem.py b/tests/python/genem.py new file mode 100644 index 000000000..0b67665dd --- /dev/null +++ b/tests/python/genem.py @@ -0,0 +1,169 @@ +import spot + +a1 = spot.automaton(''' +HOA: v1 name: "aut" States: 4 Start: 0 AP: 0 +Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) +--BODY-- +State: 0 [t] 0 {0} [t] 1 {0 2} +State: 1 [t] 2 +State: 2 [t] 1 [t] 0 {0} [t] 3 {3} +State: 3 [t] 2 {1} [t] 0 +--END--''') + +a2 = spot.automaton(''' +HOA: v1 States: 7 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) & Fin(2) +& Inf(1) properties: trans-labels explicit-labels trans-acc --BODY-- +State: 0 [2] 1 [!0&!2] 2 [0&!2] 3 [0&!2] 4 State: 1 [!0 | 1] 1 {1 2} +[0&!1] 5 {1} State: 2 [t] 2 {0} State: 3 [!0&!2] 2 [0&!2] 3 State: 4 +[0&!1&2] 1 [!0&2 | 1&2] 1 {2} [!0&!2] 6 {2} [0&!1&!2] 4 [0&1&!2] 4 {2} +State: 5 [!0 | 1] 1 {2} [0&!1] 5 State: 6 [0&!1] 6 {0} [!0 | 1] 6 {0 +2} --END--''') + +a3 = spot.automaton(''' +HOA: v1 States: 11 Start: 0 AP: 3 "a" "b" "c" Acceptance: 5 (Fin(0) +| Inf(1)) & (Fin(2) | Inf(3)) & Fin(4) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&!1&!2] 1 {1} [0&!1&!2] +2 {1} [!0&!2] 3 {1} [0&1&!2] 4 {1} [0&1&!2] 5 {1} [0&!1&2] 6 {1} [!0&2 | +1&2] 7 {1} State: 1 [0&!1&!2] 1 {0 2} [!0&!2] 3 {0 2} [0&1&!2] 4 {0 2} +State: 2 [0&!1&!2] 2 {0 2} [!0&!2] 8 {0 2 4} [0&1&!2] 5 {0 2 4} [0&!1&2] +6 {0 2} [!0&2 | 1&2] 7 {0 2 4} State: 3 [0&!1] 9 {1 2} [!0 | 1] 3 {1 2} +State: 4 [0&!1&!2] 1 {1 2} [!0&!2] 3 {1 2} [0&1&!2] 4 {1 2} State: 5 +[0&!1&!2] 2 {1 2} [!0&!2] 8 {1 2 4} [0&1&!2] 5 {1 2 4} [0&!1&2] 6 {1 2} +[!0&2 | 1&2] 7 {1 2 4} State: 6 [0&!1] 6 {0 3} [!0 | 1] 7 {0 3 4} State: +7 [0&!1] 6 {1 3} [!0 | 1] 7 {1 3 4} State: 8 [0&!1] 10 {1 2} [!0 | 1] +8 {1 2 4} State: 9 [0&!1] 9 {0 2} [!0 | 1] 3 {0 2} State: 10 [0&!1] +10 {0 2} [!0 | 1] 8 {0 2 4} --END--''') + +a4 = spot.automaton(''' +HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 6 ((Fin(0) & +Inf(1)) | (Fin(2) & Inf(3))) & Fin(4) & Inf(5) properties: trans-labels +explicit-labels state-acc complete properties: deterministic --BODY-- +State: 0 {2 4} [0&2] 1 [!0&2] 2 [!0&!1&!2] 3 [!0&1&!2] 4 [0&!2] 5 State: +1 {1 2 4} [!0] 6 [0] 1 State: 2 {1 2 5} [!0] 6 [0] 1 State: 3 {1 2 4} +[t] 3 State: 4 {1 2 4} [!0&2] 6 [0&2] 1 [!1&!2] 3 [0&1&!2] 4 [!0&1&!2] +7 State: 5 {1 2 4} [!0&2] 6 [0&2] 1 [!0&!1&!2] 3 [0&!2] 5 [!0&1&!2] +7 State: 6 {2 5} [!0] 6 [0] 1 State: 7 {3 4} [!0&2] 6 [0&2] 1 [!1&!2] +3 [0&1&!2] 4 [!0&1&!2] 7 --END--''') + +a5 = spot.automaton(""" +HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" Acceptance: 5 ((Inf(4) +| Fin(0)) & Fin(1)) | (Inf(2)&Inf(3)) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&!1] 2 State: 1 [!0&!1] +9 {3} [!0&1] 7 {0 1 2} State: 2 [!0&1] 1 [0&!1] 3 {1 2} [!0&1] 2 {3} +[0&!1] 5 {1 4} State: 3 [0&!1] 5 {0 3} [!0&!1] 9 [!0&!1] 2 [0&!1] 4 State: +4 [0&!1] 3 [!0&!1] 6 {0 1 2} State: 5 [!0&!1] 7 {0} [0&!1] 4 [0&!1] 1 +[0&!1] 8 {0} State: 6 [!0&!1] 5 {2} [0&!1] 4 {3} State: 7 [!0&1] 5 [0&!1] +2 {2} [!0&1] 4 State: 8 [0&!1] 1 {1} [!0&!1] 6 {0} State: 9 [0&1] 0 {1} +[0&1] 3 {2} [0&1] 7 {1} [0&!1] 8 {2 3 4} --END--""") + +a6 = spot.automaton(""" +HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" Acceptance: 5 (Inf(1) | (Fin(0) +& Inf(4)) | Fin(2)) & Fin(3) properties: trans-labels explicit-labels +trans-acc --BODY-- State: 0 [0&1] 9 {3} [!0&!1] 0 [0&!1] 5 {0 1} State: +1 [0&!1] 9 {4} [0&1] 8 {3} State: 2 [!0&!1] 8 {0} [!0&1] 6 {2 4} [0&1] +2 [!0&1] 7 State: 3 [0&!1] 2 {0 4} [!0&!1] 3 {1} [!0&1] 4 {0} State: 4 +[0&!1] 5 {2} [0&1] 0 [!0&1] 1 {0} State: 5 [!0&!1] 0 [!0&!1] 6 State: 6 +[0&1] 3 {2} [!0&1] 1 [0&1] 2 {0 1 3 4} State: 7 [0&1] 1 [!0&1] 7 {0 2} +State: 8 [!0&1] 7 [!0&!1] 9 {0} State: 9 [0&1] 8 {0} [0&!1] 5 [0&!1] +1 --END--""") + +a7 = spot.automaton(""" +HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" acc-name: Rabin 3 Acceptance: +6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)) properties: +trans-labels explicit-labels trans-acc --BODY-- State: 0 [0&!1] 8 {0} +[!0&!1] 6 {0 1} State: 1 [!0&1] 4 {2} [0&1] 8 {2} State: 2 [0&1] 6 {1 4} +[!0&!1] 3 {1 4} State: 3 [!0&!1] 8 {2 4} [0&1] 4 State: 4 [!0&!1] 8 {4} +[!0&!1] 7 State: 5 [!0&!1] 2 {0 5} [!0&!1] 8 {0 4} [!0&!1] 9 {4} State: +6 [!0&1] 1 {2 3 4} State: 7 [0&!1] 5 {0} [0&!1] 7 State: 8 [!0&1] 4 {0 2} +State: 9 [0&1] 3 {4} [!0&1] 5 {4} --END--""") + +a8 = spot.automaton(''' +HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" Acceptance: 6 Fin(5) & +((Fin(1) & (Inf(3) | Inf(4))) | Fin(0) | Fin(2)) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&1] 8 {0} [0&!1] 6 {2} +State: 1 [!0&1] 9 {0 4 5} State: 2 [!0&1] 1 State: 3 [0&!1] 3 {2} +[0&1] 4 {3 5} State: 4 [0&1] 7 {5} [0&!1] 9 {2} [!0&1] 0 {0 2} State: +5 [!0&1] 1 [!0&1] 3 {2 3} State: 6 [0&!1] 8 {1 2 5} [!0&1] 7 {3} State: +7 [0&1] 2 {0} [!0&1] 5 State: 8 [0&!1] 3 {4 5} State: 9 [!0&1] 3 {1 2} +[0&1] 1 {4} [0&!1] 5 {2} --END--''') + +a9 = spot.automaton(""" +HOA: v1 States: 10 Start: 0 AP: 2 "a" "b" acc-name: Streett 3 Acceptance: +6 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) properties: +trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 +[0&1] 1 [0&!1] 9 {0 5} State: 1 [0&!1] 5 State: 2 [!0&!1] 4 {1} State: 3 +[!0&!1] 8 {0} State: 4 [0&1] 6 {0 3} State: 5 [!0&!1] 7 State: 6 [!0&1] +4 State: 7 [!0&!1] 3 {2 5} State: 8 [0&!1] 1 {2} [!0&!1] 2 {2} State: +9 [!0&1] 6 {2 4} --END--""") + +a10 = spot.automaton(""" +HOA: v1 States: 2 Acceptance: 4 (Fin(0)|Fin(1))&(Fin(2)|Fin(3)) Start: 0 +AP: 0 --BODY-- State: 0 [t] 0 {0 2 3} [t] 1 {1} State: 1 [t] 0 {2} +[t] 1 {3 0 1} --END--""") + +a11 = spot.automaton(""" +HOA: v1 States: 2 Acceptance: 6 (Fin(0)|Fin(1))&(Fin(2)|Fin(3))& +(Fin(4)|Fin(5)) Start: 0 AP: 0 --BODY-- State: 0 [t] 0 {0 2 3} [t] +1 {1 4} State: 1 [t] 0 {2 5} [t] 1 {3 0 1} --END--""") + + +def generic_emptiness2_rec(aut): + spot.cleanup_acceptance_here(aut, False) + # Catching 'false' acceptance here is an optimization that could be removed. + if aut.acc().is_f(): + return True + # Catching Fin-less acceptance here to use a regular emptiness check is an + # optimization. This "if" block could be removed without breaking the + # algorithm. + if not aut.acc().uses_fin_acceptance(): + return aut.is_empty() + si = spot.scc_info(aut, True) + acc_scc = si.one_accepting_scc() + if acc_scc >= 0: + return False + nscc = si.scc_count() + # Now recurse in all non-rejecting SCC + for scc in range(nscc): + if not si.is_rejecting_scc(scc): + acc = aut.acc() + sets = si.acc_sets_of(scc) + acc = acc.restrict_to(sets) + # Do we have any unit Fin? + fu = acc.fin_unit() + if fu: + for part in si.split_on_sets(scc, fu): + if not generic_emptiness2(part): + return False + else: + # Find some Fin set, we necessarily have one, otherwise the SCC + # would have been found to be either rejecting or accepting. + fo = acc.fin_one() + assert fo >= 0, acc + for part in si.split_on_sets(scc, [fo]): + if not generic_emptiness2(part): + return False + whole = si.split_on_sets(scc, [])[0] + whole.set_acceptance(acc.remove([fo], False)) + if not generic_emptiness2(whole): + return False + return True + +# The python version of spot.generic_emptiness_check() +def generic_emptiness2(aut): + old_a = spot.acc_cond(aut.acc()) + res = generic_emptiness2_rec(aut) + # Restore the original acceptance condition + aut.set_acceptance(old_a) + return res + +def run_bench(automata): + for aut in automata: + # Make sure our three implementation behave identically + res3 = spot.generic_emptiness_check(aut) + res2 = spot.remove_fin(aut).is_empty() + res1 = generic_emptiness2(aut) + res = str(res1)[0] + str(res2)[0] + str(res3)[0] + print(res) + assert res in ('TTT', 'FFF') + +run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11])