From 61b0a542f13f404380b0d34ae4a42aaa02c82c76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Jan 2018 20:53:53 +0100 Subject: [PATCH] =?UTF-8?q?postproc:=20add=20support=20for=20co-B=C3=BCchi?= =?UTF-8?q?=20output?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New function. (weak_to_cobuchi): New internal function, used in to_nca and to_dca when appropriate. * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement the CoBuchi option. * python/spot/__init__.py: Support it in Python. * bin/common_post.cc: Add support for --buchi. * bin/autfilt.cc: Remove the --dca option. * tests/core/dca.test, tests/python/automata.ipynb: Adjust and add more tests. In particular, add more complex persistence and recurrence formulas to the list of dca.test. * tests/python/dca.test: Adjust and rename to... * tests/core/dca2.test: ... this. Add more tests, to the point that this is now failing, as described in issue #317. * tests/python/dca.py: Remove. * tests/Makefile.am: Adjust. --- NEWS | 25 ++- bin/autfilt.cc | 8 - bin/common_post.cc | 16 +- python/spot/__init__.py | 14 +- spot/twaalgos/cobuchi.cc | 100 ++++++++-- spot/twaalgos/cobuchi.hh | 32 ++- spot/twaalgos/postproc.cc | 25 ++- spot/twaalgos/postproc.hh | 9 +- tests/Makefile.am | 6 +- tests/core/dca.test | 359 ++++++++++++--------------------- tests/core/dca2.test | 75 +++++++ tests/python/automata.ipynb | 381 ++++++++++++++++++++++-------------- tests/python/dca.py | 37 ---- tests/python/dca.test | 62 ------ 14 files changed, 618 insertions(+), 531 deletions(-) create mode 100755 tests/core/dca2.test delete mode 100755 tests/python/dca.py delete mode 100755 tests/python/dca.test diff --git a/NEWS b/NEWS index 57447072e..830294eba 100644 --- a/NEWS +++ b/NEWS @@ -30,6 +30,11 @@ New in spot 2.4.4.dev (net yet released) output. Different styles can be requested using for instance --parity='min odd' or --parity='max even'. + - ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option + to force co-Büchi acceptance on the output. Beware: if the input + language is not co-Büchi realizable the output automaton will + recognize a superset of the input. + - genltl learned to generate six new families of formulas, taken from the SYNTCOMP competition on reactive synthesis, and from from Müller & Sickert's GandALF'17 paper: @@ -40,11 +45,8 @@ New in spot 2.4.4.dev (net yet released) --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) - - autfilt learned a couple of acceptance transformations: - --streett-like converts automata with DNF acceptance - into automata with Streett-like acceptance. - --dca converts automata with DNF or Streett-like - acceptance into deterministic co-Büchi. + - autfilt learned --streett-like to convert automata with DNF + acceptance into automata with Streett-like acceptance. - autfilt learned --acceptance-is=ACC to filter automata by acceptance condition. ACC can be the name of some acceptance @@ -91,10 +93,11 @@ New in spot 2.4.4.dev (net yet released) - spot::nsa_to_nca(), spot::dfn_to_nca(), spot::dfn_to_dca(), and spot::nsa_to_dca(), convert automata with DNF or Streett-like acceptance into deterministic or non-deterministic co-Büchi - automata. spot::to_dca() dispatches between the last two - functions. The language of produced automata include the original - language, but may be larger if the original automaton is not - co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 paper. + automata. spot::to_dca() and spot::to_nca() dispatches between + these four functions. The language of produced automata include + the original language, but may be larger if the original automaton + is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 + paper. - spot::scc_info::states_on_acc_cycle_of() return all states visited by any accepting cycle of the specified SCC. It only @@ -182,6 +185,10 @@ New in spot 2.4.4.dev (net yet released) have parity acceptance, it will simply be degeneralized or determinized. + - spot::postprocessor::set_type() can now request co-Büchi + acceptance as output. This calls the aforementioned to_nca() or + to_dca() functions. + - spot::remove_fin() will now call simplify_acceptance(), introduced in 2.4, before attempting its different Fin-removal strategies. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5bf095076..7c2169348 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -359,12 +359,6 @@ static const argp_option options[] = "solver can be set thanks to the SPOT_SATSOLVER environment variable" "(see spot-x)." , 0 }, - { "dca", OPT_DCA, nullptr, 0, - "convert to deterministic co-Büchi. The resulting automaton will always " - "recognize at least the same language. Actually, it can recognize " - "more if the original language can not be expressed using a co-Büchi " - "acceptance condition." - , 0 }, { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 }, { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM", @@ -1440,8 +1434,6 @@ namespace aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF); if (opt_gsa) aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN); - if (opt_dca) - aut = spot::to_dca(aut, false); if (opt_streett_like) aut = spot::dnf_to_streett(aut); diff --git a/bin/common_post.cc b/bin/common_post.cc index dbe6bce6a..c54330e9b 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -34,7 +34,8 @@ bool level_set = false; bool pref_set = false; enum { - OPT_HIGH = 1, + OPT_COBUCHI = 256, + OPT_HIGH, OPT_LOW, OPT_MEDIUM, OPT_SMALL, @@ -65,6 +66,11 @@ static constexpr const argp_option options[] = "any|min|max|odd|even|min odd|min even|max odd|max even", OPTION_ARG_OPTIONAL, "colored automaton with parity acceptance", 0, }, + { "cobuchi", OPT_COBUCHI, nullptr, 0, + "automaton with co-Büchi acceptance (will recognize" + "a superset of the input language if not co-Büchi " + "realizable)", 0 }, + { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, @@ -123,6 +129,11 @@ static const argp_option options_disabled[] = "any|min|max|odd|even|min odd|min even|max odd|max even", OPTION_ARG_OPTIONAL, "colored automaton with parity acceptance", 0, }, + { "cobuchi", OPT_COBUCHI, nullptr, 0, + "automaton with co-Büchi acceptance (will recognize" + "a superset of the input language if not co-Büchi " + "realizable)", 0 }, + { "coBuchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, @@ -210,6 +221,9 @@ parse_opt_post(int key, char* arg, struct argp_state*) case 'S': sbacc = spot::postprocessor::SBAcc; break; + case OPT_COBUCHI: + type = spot::postprocessor::CoBuchi; + break; case OPT_HIGH: level = spot::postprocessor::High; simplification_level = 3; diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 9263b6878..12900ada0 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -503,6 +503,11 @@ def _postproc_translate_options(obj, default_type, *args): type_ = postprocessor.TGBA elif val == 'ba': type_ = postprocessor.BA + elif val == 'cobuchi' or val == 'nca': + type_ = postprocessor.CoBuchi + elif val == 'dca': + type_ = postprocessor.CoBuchi + pref_ = postprocessor.Deterministic elif val == 'parity min odd': type_ = postprocessor.ParityMinOdd elif val == 'parity min even': @@ -566,14 +571,17 @@ def _postproc_translate_options(obj, default_type, *args): options = { 'any': pref_set, 'ba': type_set, - 'complete': misc_set, + 'cobuchi': type_set, 'colored': misc_set, + 'complete': misc_set, + 'dca': type_set, 'deterministic': pref_set, 'generic': type_set, 'high': optm_set, 'low': optm_set, 'medium': optm_set, 'monitor': type_set, + 'nca': type_set, 'parity even': type_set, 'parity max even': type_set, 'parity max odd': type_set, @@ -635,7 +643,7 @@ def translate(formula, *args, dict=_bdd_dict): - at most one in 'TGBA', 'BA', or 'Monitor', 'generic', 'parity', 'parity min odd', 'parity min even', 'parity max odd', 'parity max even' (type of automaton to - build) + build), 'coBuchi' - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' @@ -668,7 +676,7 @@ def postprocess(automaton, *args, formula=None): - at most one in 'Generic', 'TGBA', 'BA', or 'Monitor', 'parity', 'parity min odd', 'parity min even', 'parity max odd', 'parity max even' (type of automaton to - build) + build), 'coBuchi' - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 9e9a55de9..8c1405d97 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -29,6 +29,8 @@ #include #include #include +#include +#include #include #include @@ -196,7 +198,7 @@ namespace spot bool was_rabin = false, unsigned orig_num_st = 0) : aut_(ref_prod), - state_based_((bool)aut_->prop_state_acc()), + state_based_(aut_->prop_state_acc().is_true()), pairs_(pairs), nb_pairs_(pairs.size()), named_states_(named_states), @@ -241,29 +243,30 @@ namespace spot twa_graph_ptr - nsa_to_nca(const const_twa_graph_ptr& ref, + nsa_to_nca(const_twa_graph_ptr ref, bool named_states, vect_nca_info* nca_info) { - twa_graph_ptr ref_tmp = ref->acc().is_parity() ? to_generalized_streett(ref) - : nullptr; + if (ref->acc().is_parity()) + ref = to_generalized_streett(ref); + std::vector pairs; - if (!(ref_tmp ? ref_tmp : ref)->acc().is_streett_like(pairs)) + if (!ref->acc().is_streett_like(pairs)) throw std::runtime_error("nsa_to_nca() only works with Streett-like or " "Parity acceptance condition"); - nsa_to_nca_converter nca_converter(ref_tmp ? ref_tmp : ref, - ref_tmp ? ref_tmp : ref, - pairs, - named_states, - false); + // FIXME: At the moment this algorithm does not support + // transition-based acceptance. See issue #317. Once that is + // fixed we may remove the next line. + ref = sbacc(std::const_pointer_cast(ref)); + + nsa_to_nca_converter nca_converter(ref, ref, pairs, named_states, false); return nca_converter.run(nca_info); } twa_graph_ptr - dnf_to_nca(const const_twa_graph_ptr& ref, - bool named_states, + dnf_to_nca(const_twa_graph_ptr ref, bool named_states, vect_nca_info* nca_info) { const acc_cond::acc_code& code = ref->get_acceptance(); @@ -287,6 +290,61 @@ namespace spot return nca_converter.run(nca_info); } + namespace + { + twa_graph_ptr + weak_to_cobuchi(const const_twa_graph_ptr& aut) + { + trival iw = aut->prop_inherently_weak(); + if (iw.is_false()) + return nullptr; + scc_info si(aut); + if (iw.is_maybe() && !is_weak_automaton(aut, &si)) + return nullptr; + auto res = make_twa_graph(aut->get_dict()); + res->copy_ap_of(aut); + res->prop_copy(aut, twa::prop_set::all()); + res->new_states(aut->num_states()); + si.determine_unknown_acceptance(); + unsigned ns = si.scc_count(); + for (unsigned s = 0; s < ns; ++s) + { + acc_cond::mark_t m = 0U; + if (si.is_rejecting_scc(s)) + m = acc_cond::mark_t{0}; + else + assert(si.is_accepting_scc(s)); + + for (auto& e: si.edges_of(s)) + res->new_edge(e.src, e.dst, e.cond, m); + } + res->set_co_buchi(); + res->set_init_state(aut->get_init_state_number()); + res->prop_weak(true); + res->prop_state_acc(true); + return res; + } + } + + twa_graph_ptr + to_nca(const_twa_graph_ptr aut, bool named_states) + { + if (auto weak = weak_to_cobuchi(aut)) + return weak; + + const acc_cond::acc_code& code = aut->get_acceptance(); + + std::vector pairs; + if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) + return nsa_to_nca(aut, named_states); + else if (code.is_dnf()) + return dnf_to_nca(aut, named_states); + + auto tmp = make_twa_graph(aut, twa::prop_set::all()); + tmp->set_acceptance(aut->acc().num_sets(), + aut->get_acceptance().to_dnf()); + return to_nca(tmp, named_states); + } namespace { @@ -543,7 +601,7 @@ namespace spot twa_graph_ptr - nsa_to_dca(const const_twa_graph_ptr& aut, bool named_states) + nsa_to_dca(const_twa_graph_ptr aut, bool named_states) { debug << "NSA_to_dca" << std::endl; std::vector pairs; @@ -568,7 +626,7 @@ namespace spot twa_graph_ptr - dnf_to_dca(const const_twa_graph_ptr& aut, bool named_states) + dnf_to_dca(const_twa_graph_ptr aut, bool named_states) { debug << "DNF_to_dca" << std::endl; const acc_cond::acc_code& code = aut->get_acceptance(); @@ -599,8 +657,12 @@ namespace spot twa_graph_ptr - to_dca(const const_twa_graph_ptr& aut, bool named_states) + to_dca(const_twa_graph_ptr aut, bool named_states) { + if (is_deterministic(aut)) + if (auto weak = weak_to_cobuchi(aut)) + return weak; + const acc_cond::acc_code& code = aut->get_acceptance(); std::vector pairs; @@ -608,8 +670,10 @@ namespace spot return nsa_to_dca(aut, named_states); else if (code.is_dnf()) return dnf_to_dca(aut, named_states); - else - throw std::runtime_error("to_dca() only works with Streett-like, Parity " - "or any acceptance condition in DNF"); + + auto tmp = make_twa_graph(aut, twa::prop_set::all()); + tmp->set_acceptance(aut->acc().num_sets(), + aut->get_acceptance().to_dnf()); + return to_nca(tmp, named_states); } } diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh index e54404058..166c1a530 100644 --- a/spot/twaalgos/cobuchi.hh +++ b/spot/twaalgos/cobuchi.hh @@ -78,7 +78,7 @@ namespace spot /// \a named_states name each state for easier debugging. /// \a nca_info retrieve information about state visited infinitely often. SPOT_API twa_graph_ptr - nsa_to_nca(const const_twa_graph_ptr& aut, + nsa_to_nca(const_twa_graph_ptr aut, bool named_states = false, vect_nca_info* nca_info = nullptr); @@ -103,10 +103,21 @@ namespace spot /// \a named_states name each state for easier debugging. /// \a nca_info retrieve information about state visited infinitely often. SPOT_API twa_graph_ptr - dnf_to_nca(const const_twa_graph_ptr& aut, + dnf_to_nca(const_twa_graph_ptr aut, bool named_states = false, vect_nca_info* nca_info = nullptr); + /// \brief Converts any ω-automata to non-deterministic co-buchi + /// + /// The language of the resulting automaton always include the + /// original language, and is a superset iff the original language + /// can not be expressed using a co-Büchi acceptance condition. + /// + /// The implementation dispatches between dnf_to_nca, nsa_to_nca, + /// and a trivial implementation for weak automata. + SPOT_API twa_graph_ptr + to_nca(const_twa_graph_ptr aut, bool named_states = false); + /// \brief Converts a nondet Streett-like aut. to a det. co-Büchi aut. /// /// This function calls first nsa_to_nca() in order to retrieve som @@ -127,7 +138,7 @@ namespace spot /// \a aut The automaton to convert. /// \a named_states name each state for easier debugging. SPOT_API twa_graph_ptr - nsa_to_dca(const const_twa_graph_ptr& aut, bool named_states = false); + nsa_to_dca(const_twa_graph_ptr aut, bool named_states = false); /// \brief Converts an aut. with acceptance in DNF to a det. co-Büchi aut. /// @@ -149,13 +160,16 @@ namespace spot /// \a aut The automaton to convert. /// \a named_states name each state for easier debugging. SPOT_API twa_graph_ptr - dnf_to_dca(const const_twa_graph_ptr& aut, bool named_states = false); + dnf_to_dca(const_twa_graph_ptr aut, bool named_states = false); - /// \brief Converts any ω-automata to det. co-buchi (when possible) + /// \brief Converts any ω-automata to deterministic co-buchi /// - /// The resulting automaton will always recognize at least the same language. - /// Actually, it can recognize more if the original language can not be - /// expressed using a co-Büchi acceptance condition. + /// The language of the resulting automaton always include the + /// original language, and is a superset iff the original language + /// can not be expressed using a co-Büchi acceptance condition. + /// + /// The implementation dispatches between dnf_to_dca, nsa_to_dca, + /// and a trivial implementation for deterministic weak automata. SPOT_API twa_graph_ptr - to_dca(const const_twa_graph_ptr& aut, bool named_states = false); + to_dca(const_twa_graph_ptr aut, bool named_states = false); } diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index ba62ebb25..2e23ba693 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -36,6 +36,8 @@ #include #include #include +#include +#include namespace spot { @@ -194,6 +196,7 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; + bool via_gba = (type_ == BA) || (type_ == TGBA) || (type_ == Monitor); bool want_parity = (type_ & Parity) == Parity; if (COLORED_ && !want_parity) throw std::runtime_error("postprocessor: the Colored setting only works " @@ -234,7 +237,7 @@ namespace spot !(type_ == Generic && PREF_ == Any && level_ == Low)) a = remove_alternation(a); - if ((type_ != Generic && !a->acc().is_generalized_buchi()) + if ((via_gba && !a->acc().is_generalized_buchi()) || (want_parity && !a->acc().is_parity())) { a = to_generalized_buchi(a); @@ -247,7 +250,8 @@ namespace spot || type_ == TGBA || (type_ == BA && a->is_sba()) || (type_ == Monitor && a->num_sets() == 0) - || (want_parity && a->acc().is_parity()))) + || (want_parity && a->acc().is_parity()) + || (type_ == CoBuchi && a->acc().is_co_buchi()))) return finalize(a); int original_acc = a->num_sets(); @@ -290,6 +294,8 @@ namespace spot { if (type_ == BA) a = do_degen(a); + else if (type_ == CoBuchi) + a = to_nca(a); return finalize(a); } @@ -552,6 +558,21 @@ namespace spot sim = dba ? dba : sim; sim->remove_unused_ap(); + + if (type_ == CoBuchi) + { + unsigned ns = sim->num_states(); + if (PREF_ == Deterministic) + sim = to_dca(sim); + else + sim = to_nca(sim); + + // if the input of to_dca/to_nca was weak, the number of + // states has not changed, and running simulation is useless. + if (level_ != Low && ns < sim->num_states()) + sim = do_simul(sim, simul_); + } + return finalize(sim); } } diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index c3491ba96..fd2f48a0f 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -72,8 +72,8 @@ namespace spot /// options used for debugging or benchmarking. postprocessor(const option_map* opt = nullptr); - enum output_type { TGBA = 0, - BA = 1, + enum output_type { TGBA = 0, // should be renamed GeneralizedBuchi + BA = 1, // should be renamed Buchi and not imply SBAcc Monitor = 2, Generic = 3, Parity = 4, @@ -85,6 +85,7 @@ namespace spot ParityMaxOdd = ParityMax | ParityOdd, ParityMinEven = ParityMin | ParityEven, ParityMaxEven = ParityMax | ParityEven, + CoBuchi = 128, }; /// \brief Select the desired output type. @@ -121,6 +122,10 @@ namespace spot /// but other parity types can be obtained from there by minor /// adjustments. /// + /// \a CoBuchi requests a Co-Büchi automaton equivalent to + /// the input, when possible, or a Co-Büchi automaton that + /// recognize a larger language otherwise. + /// /// If set_type() is not called, the default \c output_type is \c TGBA. void set_type(output_type type) diff --git a/tests/Makefile.am b/tests/Makefile.am index de418f193..c9e9781d2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -309,11 +309,15 @@ TESTS_twa = \ core/cycles.test \ core/acc_word.test \ core/dca.test \ + core/dca2.test \ core/dnfstreett.test \ core/parity.test \ core/parity2.test \ core/ltlsynt.test +# Issue #317. +XFAIL_TESTS = core/dca2.test + ############################## PYTHON ############################## if USE_PYTHON @@ -356,7 +360,6 @@ TESTS_python = \ python/bdditer.py \ python/bddnqueen.py \ python/bugdet.py \ - python/dca.test \ python/declenv.py \ python/decompose_scc.py \ python/dualize.py \ @@ -410,7 +413,6 @@ nb-html: $(TESTS_ipython:.ipynb=.html) EXTRA_DIST = \ $(TESTS) \ python/ltl2tgba.py \ - python/dca.py \ python/ipnbdoctest.py diff --git a/tests/core/dca.test b/tests/core/dca.test index ece9bf11f..cd9eca867 100644 --- a/tests/core/dca.test +++ b/tests/core/dca.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -118,7 +118,6 @@ Xb -> Gb (b | X!b) W a b W (!b xor (!a M FXb)) - ((b M 1) M 1) xor (a xor Ga) b <-> (a M 1) a xor F(!X!Fa xor (b U Xa)) @@ -149,6 +148,36 @@ a M (G!b R Xb) (!a R a) | (Fa xor XFb) XF(b | Gb) M ((b R a) R !a) !a xor (0 R ((b -> a) -> Gb)) +b & X(b U (F(!b | X(!b M !a)) W a)) +G(Fb & ((Gb & (a R F!a)) | (F!b & (!a U Ga)))) +G((G!b & (G(!a & b) | (F!b & Fa))) | (Fb&((F!b&G!a) | (Fa&Gb)))) +GF(a | b | (!a & XFb)) +GF((a & (!b | X(!b R XX!a))) | (!a & b & X(b U XXa))) +F!b | G(a M Fb) +G(a | (!b M (G!a | GFa))) +Ga | (!a & G(b | X(b M Fa))) +GF(Fa R (a | F!b)) +G(((b & Fa) | (!b & G!a)) M Fa) +XG!a | G(a M Fb) +G(b | X(b M Fa)) +G(b | G(((!a & FG!b) | (a & GFb)) U !a)) +G(!a | F((!a & (a W b)) | (a & (!a M !b)))) +G((Fa & ((b & Ga) | (!b & F!a))) | (G!a & ((b & F!a) | (!b & Ga)))) +G(b | G(!a & !b) | F(!a & Fa)) +(b | Ga) & G(Fa & F(!a & b)) +G(F!a & Fa) +G(b M Fa) +G(G(a & b) | (F!b & F!a)) +Ga R XF((Xa & (!a | Fb)) | (a & G!b & X!a)) +G(Fb & ((G!a & XXGb) | (Fa & XXF!b))) +G((b & G(!a | Ga)) | (!b & F(a & F!a))) +G(b & (X!a M Fa)) +G(Fa & (X((!a & G!b) | (a & Fb)) M Fb)) +G(Fa | G(!b M F!a)) +G((Ga & F(!a W b)) | (F!a & G(a M !b))) +G(Fb U a) +G(F!b & Fb) +F(b & F!b) R (!a M Fa) (Ga | Fb) M 1 !G(F(b & Fa) W b) @@ -180,248 +209,118 @@ Fa -> XXG(1 U Gb) XXFa U Ga a & F!X(a | XFa) F(a | Gb) +F((XXb&G(!a|(Gb&XG!a)|(F!b&XFa)))|(XX!b&F(a&((Gb&XFa)|(XG!a&F!b))))) +F((!a & F(a W (a R b))) | (a & G(!a M (!a U !b)))) +XFb R F((b & F!a) | (!b & Ga)) +F((G!b & XX!a) | (Fb & XXa)) W (!a | Ga) +F((a & FG(Ga M b)) | (!a & GF(F!a W !b))) +XF(!a | GF(!b W F!a)) +(b & X(b W a)) M (Xb R (Fb & Fa)) +F(b | (G!b & FGa) | G(Fb & F!a)) +FG(((a & !b) | (!a & b)) & F((F!a & Xb) | (Ga & X!b))) +X(!b | XF((a & F((F!b & G!a) | (Gb & Fa))) | (!a & G(G(!a & b) | (F!b & Fa))))) +F((a & !b & G((b | Fa) U b)) | ((!a | b) & F((!b & G!a) R !b))) +XF(b | GF((b & Fa) | (!b & G!a))) +(FGa R (!b M F!a)) R (!b | FGb) +F(!b | (FGa & F(Gb & X!a)) | G(F!a & (F!b | Xa))) +Xb R (F!b U ((b & XF!a) | (!b & XGa))) +(Fa U ((b & Ga) | (!b & F!a))) W X((a & F!b) | (!a & Gb)) +X!a R F(Fb R !a) +Ga | F((a & b & G((!a | F!b) U !a)) | ((!a | !b) & F((a & Gb) R a))) +F(a W Fb) W ((!a & G!b) | (a & Fb)) +F((b&G(F((a&b)|(!a&!b))|(G!b U!a)))|(!b&F(G((a&!b)|(!a&b))&(Fb R a)))) +F((Fa & G(a | b)) | (G!a & F(!a & !b))) W G!a +F(Fa & G(a | b)) W G!a +F(!b | GF((!b & Fa) | (b & G!a))) +Fa R XF(Xb | (!b M G!a)) +F((b & G(F!b & Fa)) | (!b & F(Gb | G!a))) +XX(FGb R (b U ((a & F!b) | (!a & Gb)))) +F((a & F(!a W G!b)) | (!a & G(a M Fb))) +Fa R (((a & F!b) | (!a & Gb)) R F(Xb W Fa)) +F((b & F(G!b | G!a)) | (!b & G(Fb & Fa))) +F((Fb & G!a) | (G!b & Fa)) W (a | Xb) EOF -cat formulas | ltlcross \ +ltlcross --grind=bugs -F formulas \ --timeout=60 \ '{1} ltl2tgba %f >%T' \ '{2} case `ltlfilt -f %f --format=%%[w]h` in *P*) ltl2tgba -B %f | autfilt\ - --dca ;; *) ltl2tgba -B %f;; esac >%O' + -D --cobuchi ;; *) ltl2tgba -B %f;; esac >%O' \ + '{3} case `ltlfilt -f %f --format=%%[w]h` in *P*) ltl2tgba --cobuchi %f;; \ + *) ltl2tgba -B %f;; esac >%O' for i in 4 5 6 7 8 9 10 do for acc in "min even" "min odd" "max even" "max odd"; do randaut -A "parity $acc $i" a b c > input.hoa - autfilt --dca input.hoa > res.hoa - autfilt input.hoa --included-in=res.hoa + autfilt -D --cobuchi input.hoa > res.hoa + autfilt -q input.hoa --included-in=res.hoa + autfilt -q --deterministic --acceptance-is=coBuchi res.hoa done done -cat formulas | ltlcross \ +ltlcross -F formulas \ --timeout=60 \ '{1} ltl2tgba %f | autfilt --gra >%T' \ - '{2} case `ltlfilt -f %f --format=%\[w]h` in *P*) ltl2tgba -B %f | autfilt\ - --gra | autfilt --dca ;; *) ltl2tgba -B %f;; esac >%O' + '{2} case `ltlfilt -f %f --format=%%[w]h` in *P*) ltl2tgba -B %f | autfilt\ + --gra | autfilt --cobuchi;; *) ltl2tgba -B %f;; esac >%O' \ + '{3} case `ltlfilt -f %f --format=%%[w]h` in *P*) ltl2tgba -B %f | autfilt\ + --gra | autfilt --cobuchi -D;; *) ltl2tgba -B %f;; esac >%O' -cat > bigtest.hoa << EOF -HOA: v1 -States: 29 -Start: 7 -AP: 3 "a" "b" "c" -Acceptance: 5 Fin(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(4)) -properties: trans-labels explicit-labels state-acc complete -properties: deterministic ---BODY-- -State: 0 {3} -[0&!1&!2] 0 -[0&1&!2] 1 -[0&!1&2] 4 -[!0&1&2] 13 -[!0&!1&2] 15 -[!0&1&!2] 20 -[!0&!1&!2] 21 -[0&1&2] 22 -State: 1 {3} -[0&!1&!2] 0 -[0&1&!2] 1 -[!0&2] 13 -[!0&1&!2] 20 -[!0&!1&!2] 21 -[0&2] 22 -State: 2 {3} -[0&!1&2] 2 -[0&!1&!2] 3 -[0&1&!2] 12 -[!0&1] 13 -[0&1&2] 14 -[!0&!1] 15 -State: 3 {3} -[0&!1&2] 2 -[0&!1&!2] 3 -[0&1&!2] 12 -[!0&1&2] 13 -[0&1&2] 14 -[!0&!1&2] 15 -[!0&!1&!2] 16 -[!0&1&!2] 20 -State: 4 {3} -[0&!1&!2] 3 -[0&!1&2] 4 -[0&1&!2] 12 -[!0&1] 13 -[!0&!1] 15 -[0&1&2] 22 -State: 5 {3} -[0&!1&2] 5 -[0&1&!2] 12 -[!0&1] 13 -[0&1&2] 14 -[!0&!1] 15 -[0&!1&!2] 17 -State: 6 {3} -[0&!1&2] 5 -[0&!1&!2] 6 -[!0&1&2] 13 -[0&1&2] 14 -[!0&!1&2] 15 -[0&1&!2] 18 -[!0&1&!2] 20 -[!0&!1&!2] 28 -State: 7 {1 3} -[!0 | 2] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -State: 8 {1 3} -[0&1&!2] 1 -[0&!1&2] 8 -[0&!1&!2] 9 -[!0&1] 13 -[0&1&2] 22 -[!0&!1] 23 -State: 9 {1 3} -[0&1&!2] 1 -[0&!1&2] 8 -[0&!1&!2] 9 -[!0&1&2] 13 -[!0&1&!2] 20 -[0&1&2] 22 -[!0&!1&2] 23 -[!0&!1&!2] 24 -State: 10 {1 3} -[0&1&!2] 10 -[0&!1&!2] 11 -[!0&2] 13 -[0&2] 22 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 11 {1 3} -[0&!1&2] 8 -[0&1&!2] 10 -[0&!1&!2] 11 -[!0&1&2] 13 -[0&1&2] 22 -[!0&!1&2] 23 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 12 {0 1 3} -[0&!1&!2] 0 -[0&1&!2] 1 -[!0&2] 13 -[!0&1&!2] 20 -[!0&!1&!2] 21 -[0&2] 22 -State: 13 {0 1 3} -[0&1&!2] 10 -[0&!1&!2] 11 -[!0 | 2] 13 -State: 14 {0 1 3} -[!0] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[0&2] 22 -State: 15 {0 1 3} -[0&!1&!2] 6 -[!0&1 | 1&2] 13 -[0&1&!2] 18 -[!0&!1 | !1&2] 23 -State: 16 {0 1 3} -[0&!1&!2] 6 -[1&2] 13 -[0&1&!2] 18 -[!0&1&!2] 20 -[!1&2] 23 -[!0&!1&!2] 24 -State: 17 {0 1 3} -[0&1&!2] 1 -[0&!1&2] 8 -[0&!1&!2] 9 -[!0&1&2] 13 -[!0&1&!2] 20 -[0&1&2] 22 -[!0&!1&2] 23 -[!0&!1&!2] 24 -State: 18 {0 1 3} -[0&1&!2] 10 -[0&!1&!2] 11 -[!0&2] 13 -[0&2] 22 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 19 {0 1 3} -[0&!1&2] 8 -[0&1&!2] 10 -[0&!1&!2] 11 -[!0&1&2] 13 -[0&1&2] 22 -[!0&!1&2] 23 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 20 {0 1 3} -[2] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 21 {0 1 3} -[1&2] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[!1&2] 23 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 22 {2 3} -[!0] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[0&2] 22 -State: 23 {2 3} -[0&!1&!2] 6 -[!0&1 | 1&2] 13 -[0&1&!2] 18 -[!0&!1 | !1&2] 23 -State: 24 {2 3} -[0&!1&!2] 6 -[1&2] 13 -[0&1&!2] 18 -[!0&1&!2] 20 -[!1&2] 23 -[!0&!1&!2] 24 -State: 25 {2 3} -[2] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 26 {2 3} -[1&2] 13 -[0&1&!2] 18 -[0&!1&!2] 19 -[!1&2] 23 -[!0&1&!2] 25 -[!0&!1&!2] 26 -State: 27 {2 3} -[0&!1&2] 5 -[0&!1&!2] 6 -[!0&1&2] 13 -[0&1&2] 14 -[!0&!1&2] 15 -[0&1&!2] 18 -[!0&1&!2] 20 -[!0&!1&!2] 28 -State: 28 {4} -[1&2] 13 -[!1&2] 15 -[0&1&!2] 18 -[!0&1&!2] 20 -[0&!1&!2] 27 -[!0&!1&!2] 28 ---END-- + +testeq() +{ + cat >test.hoa + autfilt test.hoa --coBuchi -D > res.hoa + autfilt -q res.hoa --is-det --acceptance-is=coBuchi --equivalent-to=test.hoa + autfilt test.hoa --coBuchi > res.hoa + autfilt -q res.hoa --acceptance-is=coBuchi --equivalent-to=test.hoa +} + +testeq << EOF +HOA: v1 States: 29 Start: 7 AP: 3 "a" "b" "c" Acceptance: 5 Fin(0) +& (Inf(1) | Fin(2)) & (Inf(3) | Fin(4)) properties: trans-labels +explicit-labels state-acc complete properties: deterministic --BODY-- +State: 0 {3} [0&!1&!2] 0 [0&1&!2] 1 [0&!1&2] 4 [!0&1&2] 13 [!0&!1&2] 15 +[!0&1&!2] 20 [!0&!1&!2] 21 [0&1&2] 22 State: 1 {3} [0&!1&!2] 0 [0&1&!2] +1 [!0&2] 13 [!0&1&!2] 20 [!0&!1&!2] 21 [0&2] 22 State: 2 {3} [0&!1&2] +2 [0&!1&!2] 3 [0&1&!2] 12 [!0&1] 13 [0&1&2] 14 [!0&!1] 15 State: 3 {3} +[0&!1&2] 2 [0&!1&!2] 3 [0&1&!2] 12 [!0&1&2] 13 [0&1&2] 14 [!0&!1&2] 15 +[!0&!1&!2] 16 [!0&1&!2] 20 State: 4 {3} [0&!1&!2] 3 [0&!1&2] 4 [0&1&!2] +12 [!0&1] 13 [!0&!1] 15 [0&1&2] 22 State: 5 {3} [0&!1&2] 5 [0&1&!2] 12 +[!0&1] 13 [0&1&2] 14 [!0&!1] 15 [0&!1&!2] 17 State: 6 {3} [0&!1&2] 5 +[0&!1&!2] 6 [!0&1&2] 13 [0&1&2] 14 [!0&!1&2] 15 [0&1&!2] 18 [!0&1&!2] +20 [!0&!1&!2] 28 State: 7 {1 3} [!0 | 2] 13 [0&1&!2] 18 [0&!1&!2] 19 +State: 8 {1 3} [0&1&!2] 1 [0&!1&2] 8 [0&!1&!2] 9 [!0&1] 13 [0&1&2] 22 +[!0&!1] 23 State: 9 {1 3} [0&1&!2] 1 [0&!1&2] 8 [0&!1&!2] 9 [!0&1&2] +13 [!0&1&!2] 20 [0&1&2] 22 [!0&!1&2] 23 [!0&!1&!2] 24 State: 10 {1 3} +[0&1&!2] 10 [0&!1&!2] 11 [!0&2] 13 [0&2] 22 [!0&1&!2] 25 [!0&!1&!2] 26 +State: 11 {1 3} [0&!1&2] 8 [0&1&!2] 10 [0&!1&!2] 11 [!0&1&2] 13 [0&1&2] +22 [!0&!1&2] 23 [!0&1&!2] 25 [!0&!1&!2] 26 State: 12 {0 1 3} [0&!1&!2] 0 +[0&1&!2] 1 [!0&2] 13 [!0&1&!2] 20 [!0&!1&!2] 21 [0&2] 22 State: 13 {0 1 3} +[0&1&!2] 10 [0&!1&!2] 11 [!0 | 2] 13 State: 14 {0 1 3} [!0] 13 [0&1&!2] +18 [0&!1&!2] 19 [0&2] 22 State: 15 {0 1 3} [0&!1&!2] 6 [!0&1 | 1&2] +13 [0&1&!2] 18 [!0&!1 | !1&2] 23 State: 16 {0 1 3} [0&!1&!2] 6 [1&2] +13 [0&1&!2] 18 [!0&1&!2] 20 [!1&2] 23 [!0&!1&!2] 24 State: 17 {0 1 3} +[0&1&!2] 1 [0&!1&2] 8 [0&!1&!2] 9 [!0&1&2] 13 [!0&1&!2] 20 [0&1&2] 22 +[!0&!1&2] 23 [!0&!1&!2] 24 State: 18 {0 1 3} [0&1&!2] 10 [0&!1&!2] +11 [!0&2] 13 [0&2] 22 [!0&1&!2] 25 [!0&!1&!2] 26 State: 19 {0 1 3} +[0&!1&2] 8 [0&1&!2] 10 [0&!1&!2] 11 [!0&1&2] 13 [0&1&2] 22 [!0&!1&2] 23 +[!0&1&!2] 25 [!0&!1&!2] 26 State: 20 {0 1 3} [2] 13 [0&1&!2] 18 [0&!1&!2] +19 [!0&1&!2] 25 [!0&!1&!2] 26 State: 21 {0 1 3} [1&2] 13 [0&1&!2] 18 +[0&!1&!2] 19 [!1&2] 23 [!0&1&!2] 25 [!0&!1&!2] 26 State: 22 {2 3} [!0] +13 [0&1&!2] 18 [0&!1&!2] 19 [0&2] 22 State: 23 {2 3} [0&!1&!2] 6 [!0&1 | +1&2] 13 [0&1&!2] 18 [!0&!1 | !1&2] 23 State: 24 {2 3} [0&!1&!2] 6 [1&2] +13 [0&1&!2] 18 [!0&1&!2] 20 [!1&2] 23 [!0&!1&!2] 24 State: 25 {2 3} [2] +13 [0&1&!2] 18 [0&!1&!2] 19 [!0&1&!2] 25 [!0&!1&!2] 26 State: 26 {2 3} +[1&2] 13 [0&1&!2] 18 [0&!1&!2] 19 [!1&2] 23 [!0&1&!2] 25 [!0&!1&!2] 26 +State: 27 {2 3} [0&!1&2] 5 [0&!1&!2] 6 [!0&1&2] 13 [0&1&2] 14 [!0&!1&2] +15 [0&1&!2] 18 [!0&1&!2] 20 [!0&!1&!2] 28 State: 28 {4} [1&2] 13 [!1&2] +15 [0&1&!2] 18 [!0&1&!2] 20 [0&!1&!2] 27 [!0&!1&!2] 28 --END-- EOF -autfilt bigtest.hoa --dca > res.hoa -autfilt bigtest.hoa --equivalent-to='res.hoa' -cat >empty.hoa< res.hoa -autfilt empty.hoa --equivalent-to='res.hoa' -cat >empty.hoa< res.hoa -autfilt empty.hoa --equivalent-to='res.hoa' -cat >empty.hoa< res.hoa -autfilt empty.hoa --equivalent-to='res.hoa' diff --git a/tests/core/dca2.test b/tests/core/dca2.test new file mode 100755 index 000000000..e14c87ee2 --- /dev/null +++ b/tests/core/dca2.test @@ -0,0 +1,75 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017, 2018 Laboratoire de Recherche et +# Développement de l'EPITA. +# +# 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 . + +. ./defs +set -e + +cat >l_formulas <<'EOF' +FG!b +FGc +F(a | Gb) +XF(b & Ga) +a | c | FG(!b & !c) +!a | FGb +F((!a & ((c & F!b) | (!c & Gb))) | (a & ((c & Gb) | (!c & F!b)))) +F((c & F!b) | (!c & Gb)) +F((!c R a) W G!b) +FG(((!b | (c M b)) & X(c & Xa)) | (b & (!c W !b) & X(!c | X!a))) +(Ga M c) M ((!b & Fb) M F(a | !b)) +(Gb | X(!b M X!b)) M ((b & c) | (!b & !c)) +F(c R (X!c W Fb)) +XF!c & F(Fb R a) +(!c M F(b & Ga)) W (b U a) +EOF + +cat >r_formulas <<'EOF' +GF(b | GF!c) +!b & G(G!c | XFc) +GF(b | c | (!c & XFb)) +GFc | G(!b | !c) +G(Gb | Fc) +G(c | (c R Xc) | XF(b & !c)) +Gc R XFb +G(c | (!b M (GFc | G!c))) +F(((c W Xb) & F(b R !c)) | ((!c M X!b) & G(!b U c))) +EOF + +while read l_f; do + ltl2tgba --parity='max odd' "$l_f" > l.hoa + autfilt -q --acceptance-is='Fin(0) | Inf(1)' l.hoa + while read r_f; do + # Dualizing a deterministic transition-based parity automaton + # to obtain a transition-based deterministic streett + # automaton. What we want to avoid as much as possible is + # weak automata, because l.hoa is already weak and that would + # make the sum/product weak as well. + 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 + # 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 + + autcross --language-preserved --verbose -F or.hoa -F and.hoa \ + 'autfilt %H --stats=%M | ltl2tgba >%O' \ + 'autfilt --cobuchi' 'autfilt --cobuchi -D' + done \n" ], "text/plain": [ - " *' at 0x7fb1043b73f0> >" + " *' at 0x7f9d08673930> >" ] }, "execution_count": 2, @@ -171,9 +167,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -312,9 +306,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -468,9 +460,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -493,9 +483,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -550,7 +538,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042bc900> >" + " *' at 0x7f9d0857cbd0> >" ] }, "execution_count": 6, @@ -565,9 +553,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -622,7 +608,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce7b0> >" + " *' at 0x7f9d08673960> >" ] }, "execution_count": 7, @@ -644,9 +630,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -700,7 +684,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1043b7390> >" + " *' at 0x7f9d08673b40> >" ] }, "execution_count": 8, @@ -722,9 +706,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -747,9 +729,7 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -842,9 +822,7 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1041,9 +1019,7 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1168,7 +1144,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce870> >" + " *' at 0x7f9d0858c360> >" ] }, "execution_count": 12, @@ -1190,9 +1166,7 @@ { "cell_type": "code", "execution_count": 13, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1271,7 +1245,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042bc660> >" + " *' at 0x7f9d0857c450> >" ] }, "execution_count": 13, @@ -1293,9 +1267,7 @@ { "cell_type": "code", "execution_count": 14, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1391,7 +1363,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce6c0> >" + " *' at 0x7f9d0857c420> >" ] }, "execution_count": 14, @@ -1413,9 +1385,7 @@ { "cell_type": "code", "execution_count": 15, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1492,7 +1462,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1043dd600> >" + " *' at 0x7f9d0857c480> >" ] }, "execution_count": 15, @@ -1507,9 +1477,7 @@ { "cell_type": "code", "execution_count": 16, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1964,7 +1932,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce600> >" + " *' at 0x7f9d0b183ae0> >" ] }, "execution_count": 16, @@ -1979,9 +1947,7 @@ { "cell_type": "code", "execution_count": 17, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2008,9 +1974,7 @@ { "cell_type": "code", "execution_count": 18, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -2047,9 +2011,7 @@ { "cell_type": "code", "execution_count": 19, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2588,7 +2550,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042bc8d0> >" + " *' at 0x7f9d0858c600> >" ] }, "metadata": {}, @@ -2606,9 +2568,7 @@ { "cell_type": "code", "execution_count": 20, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "!rm example1.aut" @@ -2617,9 +2577,7 @@ { "cell_type": "code", "execution_count": 21, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2749,7 +2707,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce780> >" + " *' at 0x7f9d0858c450> >" ] }, "execution_count": 21, @@ -2764,9 +2722,7 @@ { "cell_type": "code", "execution_count": 22, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2821,7 +2777,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce8a0> >" + " *' at 0x7f9d0858c390> >" ] }, "execution_count": 22, @@ -2836,9 +2792,7 @@ { "cell_type": "code", "execution_count": 23, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -3204,9 +3158,7 @@ { "cell_type": "code", "execution_count": 24, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -3261,7 +3213,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce810> >" + " *' at 0x7f9d0858c1b0> >" ] }, "metadata": {}, @@ -3286,9 +3238,7 @@ { "cell_type": "code", "execution_count": 25, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -3372,72 +3322,69 @@ { "cell_type": "code", "execution_count": 26, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a\n", + "0->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1\n", - "\n", - "1\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", - "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "⓿\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 0x7fb1042ce7e0> >" + "" ] }, "execution_count": 26, @@ -3446,7 +3393,155 @@ } ], "source": [ - "aut = spot.translate('FGa', 'generic', 'deterministic'); aut" + "aut = spot.translate('FGa', 'generic', 'deterministic'); aut.show('.ba')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Translation to co-Büchi automaton" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\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", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.translate('FGa', 'coBuchi').show('.ba')" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\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", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.translate('FGa', 'coBuchi', 'deterministic').show('.ba')" ] }, { @@ -3458,10 +3553,8 @@ }, { "cell_type": "code", - "execution_count": 27, - "metadata": { - "collapsed": false - }, + "execution_count": 29, + "metadata": {}, "outputs": [ { "data": { @@ -3524,10 +3617,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce7e0> >" + " *' at 0x7f9d0858c570> >" ] }, - "execution_count": 27, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -3549,10 +3642,8 @@ }, { "cell_type": "code", - "execution_count": 28, - "metadata": { - "collapsed": false - }, + "execution_count": 30, + "metadata": {}, "outputs": [ { "data": { @@ -3615,10 +3706,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fb1042ce7e0> >" + " *' at 0x7f9d0858c570> >" ] }, - "execution_count": 28, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } @@ -3648,7 +3739,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.3" + "version": "3.6.4" } }, "nbformat": 4, diff --git a/tests/python/dca.py b/tests/python/dca.py deleted file mode 100755 index 456b915ab..000000000 --- a/tests/python/dca.py +++ /dev/null @@ -1,37 +0,0 @@ -#!/usr/bin/python3 -# -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de -# l'EPITA. -# -# 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 . - -import sys -import spot - - -def gen_streett(formula): - aut = spot.translate(formula, 'BA') - aut.set_acceptance(2, 'Fin(0) | Inf(1)') - for e in aut.edges(): - if (e.acc): - e.acc = spot.mark_t([0,1]) - else: - e.acc = spot.mark_t([0]) - return aut - - -aut = gen_streett(sys.argv[1]) -print(aut.to_str('hoa')) diff --git a/tests/python/dca.test b/tests/python/dca.test deleted file mode 100755 index 9488aa695..000000000 --- a/tests/python/dca.test +++ /dev/null @@ -1,62 +0,0 @@ -#!/bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et -# Développement de l'EPITA. -# -# 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 . - -set -e - -# Skip this test if ltl2dstar is not installed. -(ltl2dstar --version) || exit 77 - -DIR=dca.dir -mkdir -p $DIR - -cat >$DIR/ba_formulas << 'EOF' -FG((Xc & XXa) <-> !(b xor (c M b))) -F!FGFb -XF(b & Ga) -FG(F(b R Fc) R Gc) -(!c M F(b M Ga)) W (b U a) -(c xor Gb) M 1 -X!Gc M ((Fb R a) M 1) -!a | F(b W 0) -F(!a -> Gb) -(Gb <-> X(b W Xb)) M (b xor !c) -(c R (X!c W Fb)) M 1 -!a -> (FX!(0 R F(b | c)) W c) -XF((!c R a) W !Fb) -(!a <-> !(c <-> Gb)) M 1 -((0 R a) M c) M ((b xor Fb) M F(b -> a)) -EOF -cat >$DIR/dsa_formulas <<'EOF' -(!b U b) U X(!a -> Fb) -1 U (a xor b) -X(!(!b | (a M b)) -> XXa) -!Gb -F(XF!a & (Fb U !a)) -EOF -while read ba_f; do - ../run "$srcdir/dca.py" "$ba_f" > $DIR/ba - while read dsa_f; do - ltldo -f "$dsa_f" "ltl2dstar --automata=streett\ - --ltl2nba=spin:ltl2tgba@-Ds" -H | - autfilt --product=$DIR/ba > $DIR/input.hoa - autfilt --dca $DIR/input.hoa > $DIR/res.hoa - autfilt $DIR/input.hoa --equivalent-to $DIR/res.hoa - done <$DIR/dsa_formulas -done <$DIR/ba_formulas