From 9cc1bdf10f17ce69563290398fbb2157d00456b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 6 Oct 2020 17:46:34 +0200 Subject: [PATCH] =?UTF-8?q?postprocess,=20translate:=20add=20support=20for?= =?UTF-8?q?=20B=C3=BCchi=20(not=20state-based)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit spot/twaalgos/postproc.hh: Introduce options Buchi and GeneralizedBuchi. The latter is similar to TGBA but the former differs from BA in that it does not imply state-based acceptance, since that can be specified separately. Also all other acceptance types are not abbreviated, so those new names make more sense. * NEWS: Mention that. * spot/twaalgos/postproc.cc, spot/twaalgos/translate.cc: Adjust to support Buchi and GeneralizedBuchi without breaking BA and TGBA. * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_post.cc, bin/ltl2tgta.cc, doc/org/tut10.org, doc/org/tut12.org, doc/org/tut30.org, python/spot/__init__.py, tests/python/automata.ipynb, tests/python/langmap.py, tests/python/misc-ec.py, tests/python/satmin.ipynb, tests/python/satmin.py, tests/python/toweak.py: Use the new names. * tests/Makefile.am: Add missing langmap.py. --- NEWS | 26 +++++++++++ bin/autfilt.cc | 8 ++-- bin/common_aoutput.cc | 3 +- bin/common_post.cc | 8 ++-- bin/ltl2tgta.cc | 11 +++-- doc/org/tut10.org | 40 ++++++++-------- doc/org/tut12.org | 58 ++++++++++++----------- doc/org/tut30.org | 23 +++++----- python/spot/__init__.py | 43 +++++++++++------ spot/twaalgos/postproc.cc | 92 +++++++++++++++++++------------------ spot/twaalgos/postproc.hh | 47 +++++++++++-------- spot/twaalgos/translate.cc | 33 +++++++++---- tests/Makefile.am | 1 + tests/python/automata.ipynb | 52 ++++++++++----------- tests/python/langmap.py | 16 +++---- tests/python/misc-ec.py | 4 +- tests/python/satmin.ipynb | 2 +- tests/python/satmin.py | 4 +- tests/python/toweak.py | 4 +- 19 files changed, 274 insertions(+), 201 deletions(-) diff --git a/NEWS b/NEWS index c405dca2f..6e76efd67 100644 --- a/NEWS +++ b/NEWS @@ -55,6 +55,32 @@ New in spot 2.9.4.dev (not yet released) file. With this refactoring, we can retrieve both a kripke or a kripkecube from a PINS file. + - The postprocessor::set_type() method can now accept + options postprocessor::Buchi and postprocessor::GeneralizedBuchi. + + These syntaxes is more homogeneous with the rest of the supported + types. Note that postprocessor::BA and postprocessor::TGBA, while + still supported and not yet marked as deprecated, are best avoided + in new code. + + postprocessor::set_type(postprocessor::TGBA) + + can be replaced by + + postprocessor::set_type(postprocessor::BA) + + and + + postprocessor::set_type(postprocessor::Buchi) + postprocessor::set_pref(postprocessor::Small + | postprocessor::SBAcc) + + Note that the old postprocessor::BA option implied state-based + acceptance (and was unique in that way), but the new + postprocessor::Buchi specifies Büchi acceptance without requiring + state-based acceptance (something that postprocessor did not + permit before). + - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which used to take ages are now instantaneous. (Issue #412.) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5cc3bda7e..38015004e 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -686,17 +686,17 @@ ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut) { spot::postprocessor p; - p.set_type(spot::postprocessor::TGBA); + p.set_type(spot::postprocessor::Buchi); p.set_pref(spot::postprocessor::Any); p.set_level(spot::postprocessor::Low); - return spot::degeneralize_tba(p.run(aut)); + return p.run(aut); } static spot::twa_graph_ptr product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { - if ((type == spot::postprocessor::BA) + if ((type == spot::postprocessor::Buchi) && (left->num_sets() + right->num_sets() > spot::acc_cond::mark_t::max_accsets())) { @@ -709,7 +709,7 @@ product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) static spot::twa_graph_ptr product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { - if ((type == spot::postprocessor::BA) + if ((type == spot::postprocessor::Buchi) && (left->num_sets() + right->num_sets() > spot::acc_cond::mark_t::max_accsets())) { diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index f19326889..3d1802dbb 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -340,7 +340,8 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) case 's': automaton_format = Spin; if (type != spot::postprocessor::Monitor) - type = spot::postprocessor::BA; + type = spot::postprocessor::Buchi; + sbacc = spot::postprocessor::SBAcc; automaton_format_opt = arg; break; case OPT_CHECK: diff --git a/bin/common_post.cc b/bin/common_post.cc index e6ebfd29b..6998eeb4f 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,7 +24,7 @@ #include "error.h" #include "argmatch.h" -spot::postprocessor::output_type type = spot::postprocessor::TGBA; +spot::postprocessor::output_type type = spot::postprocessor::GeneralizedBuchi; spot::postprocessor::output_pref pref = spot::postprocessor::Small; spot::postprocessor::output_pref comp = spot::postprocessor::Any; spot::postprocessor::output_pref sbacc = spot::postprocessor::Any; @@ -165,7 +165,7 @@ parse_opt_post(int key, char* arg, struct argp_state*) pref_set = true; break; case 'B': - type = spot::postprocessor::BA; + type = spot::postprocessor::Buchi; colored = spot::postprocessor::Any; sbacc = spot::postprocessor::SBAcc; break; @@ -250,7 +250,7 @@ parse_opt_post(int key, char* arg, struct argp_state*) case OPT_TGBA: if (automaton_format == Spin) error(2, 0, "--spin and --tgba are incompatible"); - type = spot::postprocessor::TGBA; + type = spot::postprocessor::GeneralizedBuchi; colored = spot::postprocessor::Any; break; default: diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 8663f5513..ad3a64299 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -126,15 +126,16 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_TGTA: ta_type = TGTA; - type = spot::postprocessor::TGBA; + type = spot::postprocessor::GeneralizedBuchi; break; case OPT_GTA: ta_type = GTA; - type = spot::postprocessor::TGBA; + type = spot::postprocessor::GeneralizedBuchi; break; case OPT_TA: ta_type = TA; - type = spot::postprocessor::BA; + type = spot::postprocessor::Buchi; + sbacc = spot::postprocessor::SBAcc; break; case OPT_INIT: opt_with_artificial_initial_state = false; @@ -196,7 +197,7 @@ namespace if (ta_type != TGTA) { auto testing_automaton = - tgba_to_ta(aut, ap_set, type == spot::postprocessor::BA, + tgba_to_ta(aut, ap_set, type == spot::postprocessor::Buchi, opt_with_artificial_initial_state, opt_single_pass_emptiness_check, opt_with_artificial_livelock); diff --git a/doc/org/tut10.org b/doc/org/tut10.org index 85cf5b73d..419a33197 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -88,7 +88,7 @@ that takes a formula (possibly as a string) as first argument: #+BEGIN_SRC python import spot -print(spot.translate('GFa -> GFb', 'BA').to_str('spin')) +print(spot.translate('GFa -> GFb', 'buchi', 'sbacc').to_str('spin')) #+END_SRC #+RESULTS: @@ -120,15 +120,16 @@ T0_S3: * C++ -All the translation pipeline (this include simplifying the formula, +All the translation pipeline (this includes simplifying the formula, translating the simplified formula into an automaton, and simplifying the resulting automaton) is handled by the =spot::translator= class. An instance of this class can configured by calling =set_type()= to chose the type of automaton to output, =set_level()= to set the level of optimization (it's high by default), and =set_pref()= to set various preferences (like small or deterministic) or characteristic -(complete, unambiguous) for the resulting automaton. Finally, the -output as a never claim is done via the =print_never_claim= function. +(complete, unambiguous, state-based acceptance) for the resulting +automaton. Finally, the output as a never claim is done via the +=print_never_claim= function. #+BEGIN_SRC C++ #include @@ -138,11 +139,13 @@ output as a never claim is done via the =print_never_claim= function. int main() { - spot::parsed_formula pf = spot::parse_infix_psl("[]<>p0 || <>[]p1"); + spot::parsed_formula pf = spot::parse_infix_psl("[]<>a || <>[]b"); if (pf.format_errors(std::cerr)) return 1; spot::translator trans; - trans.set_type(spot::postprocessor::BA); + trans.set_type(spot::postprocessor::Buchi); + trans.set_pref(spot::postprocessor::SBAcc + | spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(pf.f); print_never_claim(std::cout, aut) << '\n'; return 0; @@ -155,24 +158,25 @@ never { T0_init: if :: (true) -> goto T0_init - :: (p0) -> goto accept_S1 - :: (p1) -> goto accept_S2 + :: (a) -> goto accept_S1 + :: (b) -> goto accept_S2 fi; accept_S1: if - :: (p0) -> goto accept_S1 - :: (!(p0)) -> goto T0_S3 + :: (a) -> goto accept_S1 + :: (!(a)) -> goto T0_S3 fi; accept_S2: if - :: (p1) -> goto accept_S2 + :: (b) -> goto accept_S2 fi; T0_S3: if - :: (p0) -> goto accept_S1 - :: (!(p0)) -> goto T0_S3 + :: (a) -> goto accept_S1 + :: (!(a)) -> goto T0_S3 fi; } + #+end_example * Additional comments @@ -188,17 +192,17 @@ help(spot.translate) #+begin_example Help on function translate in module spot: -translate(formula, *args, dict= *' at 0x7f1f9541c090> >, xargs=None) +translate(formula, *args, dict= *' at 0x7f42f4cea030> >, xargs=None) Translate a formula into an automaton. Keep in mind that 'Deterministic' expresses just a preference that may not be satisfied. The optional arguments should be strings among the following: - - 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), 'coBuchi' + - at most one in 'GeneralizedBuchi', 'Buchi', or 'Monitor', + 'generic', 'parity', 'parity min odd', 'parity min even', + 'parity max odd', 'parity max even', 'coBuchi' + (type of acceptance condition to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' diff --git a/doc/org/tut12.org b/doc/org/tut12.org index 253c7bb43..fbe01e53e 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -121,7 +121,7 @@ more simplification opportunities.) #+begin_src python import spot # Translate LTLf to Büchi. -aut = spot.from_ltlf('(a U b) & Fc').translate('ba') +aut = spot.from_ltlf('(a U b) & Fc').translate('small', 'buchi', 'sbacc') # Remove "alive" atomic proposition rem = spot.remove_ap() rem.add_ap('alive') @@ -141,7 +141,7 @@ AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic -properties: very-weak +properties: terminal --BODY-- State: 0 [!2] 0 @@ -171,36 +171,38 @@ wrappers around the =spot::translator= and =spot::postprocessor= objects that we need to use here. #+begin_src C++ -#include -#include -#include -#include -#include -#include + #include + #include + #include + #include + #include + #include -int main() -{ - spot::parsed_formula pf = spot::parse_infix_psl("(a U b) & Fc"); - if (pf.format_errors(std::cerr)) - return 1; + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("(a U b) & Fc"); + if (pf.format_errors(std::cerr)) + return 1; - spot::translator trans; - trans.set_type(spot::postprocessor::BA); - trans.set_pref(spot::postprocessor::Small); - spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); + spot::translator trans; + trans.set_type(spot::postprocessor::Buchi); + trans.set_pref(spot::postprocessor::SBAcc + | spot::postprocessor::Small); + spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); - spot::remove_ap rem; - rem.add_ap("alive"); - aut = rem.strip(aut); + spot::remove_ap rem; + rem.add_ap("alive"); + aut = rem.strip(aut); - spot::postprocessor post; - post.set_type(spot::postprocessor::BA); - post.set_pref(spot::postprocessor::Small); // or ::Deterministic - aut = post.run(aut); + spot::postprocessor post; + post.set_type(spot::postprocessor::Buchi); + post.set_pref(spot::postprocessor::SBAcc + | spot::postprocessor::Small); // or ::Deterministic + aut = post.run(aut); - print_hoa(std::cout, aut) << '\n'; - return 0; -} + print_hoa(std::cout, aut) << '\n'; + return 0; + } #+end_src #+RESULTS: @@ -212,7 +214,7 @@ AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic -properties: very-weak +properties: terminal --BODY-- State: 0 [!2] 0 diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 819b147b7..6fc0bd7f3 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -94,11 +94,11 @@ The Python version uses the =postprocess()= routine: #+BEGIN_SRC python :wrap SRC hoa import spot -aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic') +aut = spot.automaton('tut30.hoa').postprocess('buchi', 'sbacc', 'deterministic') print(aut.to_str('hoa')) #+END_SRC #+RESULTS: -#+BEGIN_SRC hoa +#+begin_SRC hoa HOA: v1 States: 5 Start: 1 @@ -106,7 +106,7 @@ AP: 1 "p1" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic weak +properties: deterministic terminal --BODY-- State: 0 {0} [t] 0 @@ -122,7 +122,7 @@ State: 4 [!0] 0 [0] 4 --END-- -#+END_SRC +#+end_SRC The =postprocess()= function has an interface similar to [[file:tut10.org][the =translate()= function discussed previously]]: @@ -145,10 +145,10 @@ postprocess(automaton, *args, formula=None, xargs=None) not already 'Deterministic'. The optional arguments should be strings among the following: - - 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), 'coBuchi' + - at most one in 'Generic', 'GeneralizedBuchi', 'Buchi', or + 'Monitor', 'parity', 'parity min odd', 'parity min even', + 'parity max odd', 'parity max even', 'coBuchi' + (type of acceptance condition to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' @@ -195,8 +195,9 @@ automaton to process. return 1; } spot::postprocessor post; - post.set_type(spot::postprocessor::BA); - post.set_pref(spot::postprocessor::Deterministic); + post.set_type(spot::postprocessor::Buchi); + post.set_pref(spot::postprocessor::SBAcc + | spot::postprocessor::Deterministic); post.set_level(spot::postprocessor::High); auto aut = post.run(pa->aut); spot::print_hoa(std::cout, aut) << '\n'; @@ -213,7 +214,7 @@ AP: 1 "p1" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic very-weak +properties: deterministic terminal --BODY-- State: 0 {0} [t] 0 diff --git a/python/spot/__init__.py b/python/spot/__init__.py index faa50d30e..f5beecee1 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -584,12 +584,17 @@ def _postproc_translate_options(obj, default_type, *args): if type_ is not None and type_name_ != val: raise ValueError("type cannot be both {} and {}" .format(type_name_, val)) - elif val == 'generic': + elif val == 'generic' or val == 'gen' or val == 'g': type_ = postprocessor.Generic - elif val == 'tgba': - type_ = postprocessor.TGBA - elif val == 'ba': - type_ = postprocessor.BA + elif val == 'tgba': # historical + type_ = postprocessor.GeneralizedBuchi + elif val == 'generalizedbuchi': + type_ = postprocessor.GeneralizedBuchi + elif val == 'ba': # historical + type_ = postprocessor.Buchi + sbac_ = postprocessor.SBAcc + elif val == 'buchi': + type_ = postprocessor.Buchi elif val == 'cobuchi' or val == 'nca': type_ = postprocessor.CoBuchi elif val == 'dca': @@ -652,7 +657,8 @@ def _postproc_translate_options(obj, default_type, *args): colo_ = postprocessor.Colored elif val == 'complete': comp_ = postprocessor.Complete - elif val == 'sbacc' or val == 'state-based-acceptance': + elif (val == 'sbacc' or val == 'statebasedacceptance' + or val == 'state-based-acceptance'): sbac_ = postprocessor.SBAcc else: assert(val == 'unambiguous') @@ -661,12 +667,16 @@ def _postproc_translate_options(obj, default_type, *args): options = { 'any': pref_set, 'ba': type_set, + 'buchi': type_set, 'cobuchi': type_set, 'colored': misc_set, 'complete': misc_set, 'dca': type_set, 'deterministic': pref_set, + 'g': type_set, + 'gen': type_set, 'generic': type_set, + 'generalizedbuchi': type_set, 'high': optm_set, 'low': optm_set, 'medium': optm_set, @@ -684,6 +694,7 @@ def _postproc_translate_options(obj, default_type, *args): 'sbacc': misc_set, 'small': pref_set, 'statebasedacceptance': misc_set, + 'state-based-acceptance': misc_set, 'tgba': type_set, 'unambiguous': misc_set, } @@ -730,10 +741,10 @@ def translate(formula, *args, dict=_bdd_dict, xargs=None): may not be satisfied. The optional arguments should be strings among the following: - - 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), 'coBuchi' + - at most one in 'GeneralizedBuchi', 'Buchi', or 'Monitor', + 'generic', 'parity', 'parity min odd', 'parity min even', + 'parity max odd', 'parity max even', 'coBuchi' + (type of acceptance condition to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' @@ -748,6 +759,7 @@ def translate(formula, *args, dict=_bdd_dict, xargs=None): string (that will be converted to `spot.option_map`), as the `xargs` argument. This is similar to the `-x` option of command-line tools; so check out the spot-x(7) man page for details. + """ if type(xargs) is str: xargs = option_map(xargs) @@ -786,10 +798,10 @@ def postprocess(automaton, *args, formula=None, xargs=None): not already 'Deterministic'. The optional arguments should be strings among the following: - - 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), 'coBuchi' + - at most one in 'Generic', 'GeneralizedBuchi', 'Buchi', or + 'Monitor', 'parity', 'parity min odd', 'parity min even', + 'parity max odd', 'parity max even', 'coBuchi' + (type of acceptance condition to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' @@ -808,7 +820,8 @@ def postprocess(automaton, *args, formula=None, xargs=None): string (that will be converted to `spot.option_map`), as the `xargs` argument. This is similar to the `-x` option of command-line tools; so check out the spot-x(7) man page for details. -""" + + """ if type(xargs) is str: xargs = option_map(xargs) p = postprocessor(xargs) diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 36c6af003..1142220d7 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -48,7 +48,7 @@ namespace spot static twa_graph_ptr ensure_ba(twa_graph_ptr& a) { - if (a->num_sets() == 0) + if (a->acc().is_t()) { auto m = a->set_buchi(); for (auto& t: a->edges()) @@ -154,6 +154,15 @@ namespace spot } } + twa_graph_ptr + postprocessor::choose_degen(const twa_graph_ptr& a) const + { + if (state_based_) + return do_degen(a); + else + return do_degen_tba(a); + } + twa_graph_ptr postprocessor::do_degen(const twa_graph_ptr& a) const { @@ -173,15 +182,6 @@ namespace spot degen_lowinit_, degen_remscc_); } - static void - force_buchi(twa_graph_ptr& a) - { - assert(a->acc().is_t()); - acc_cond::mark_t m = a->set_buchi(); - for (auto& e: a->edges()) - e.acc = m; - } - twa_graph_ptr postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const { @@ -212,11 +212,12 @@ namespace spot 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 = choose_degen(tmp); + assert(!!SBACC_ == state_based_); + if (state_based_) tmp = sbacc(tmp); - if (type_ == BA && tmp->acc().is_t()) - force_buchi(tmp); + if (type_ == Buchi) + tmp = ensure_ba(tmp); if (want_parity) { reduce_parity_here(tmp, COLORED_); @@ -244,10 +245,18 @@ namespace spot ba_simul_ = (level_ == High) ? 3 : 0; if (scc_filter_ < 0) scc_filter_ = 1; - if (type_ == BA || SBACC_) + if (type_ == BA) + { + pref_ |= SBAcc; + type_ = Buchi; + } + if (SBACC_) state_based_ = true; + else if (state_based_) + pref_ |= SBAcc; - bool via_gba = (type_ == BA) || (type_ == TGBA) || (type_ == Monitor); + bool via_gba = + (type_ == Buchi) || (type_ == GeneralizedBuchi) || (type_ == Monitor); bool want_parity = type_ & Parity; if (COLORED_ && !want_parity) throw std::runtime_error("postprocessor: the Colored setting only works " @@ -317,8 +326,8 @@ namespace spot if (PREF_ == Any && level_ == Low && (type_ == Generic - || type_ == TGBA - || (type_ == BA && a->is_sba()) + || type_ == GeneralizedBuchi + || (type_ == Buchi && a->acc().is_buchi()) || (type_ == Monitor && a->num_sets() == 0) || (want_parity && a->acc().is_parity()) || (type_ == CoBuchi && a->acc().is_co_buchi()))) @@ -362,8 +371,8 @@ namespace spot if (PREF_ == Any) { - if (type_ == BA) - a = do_degen(a); + if (type_ == Buchi) + a = choose_degen(a); else if (type_ == CoBuchi) a = to_nca(a); return finalize(a); @@ -402,8 +411,6 @@ namespace spot if (!ab && PREF_ != Deterministic) ab = &wdba_aborter; dba = minimize_obligation(a, f, nullptr, reject_bigger, ab); - if (!dba) - std::cerr << "DBA aborted\n"; if (dba && dba->prop_inherently_weak().is_true() @@ -412,7 +419,7 @@ namespace spot // The WDBA is a BA, so no degeneralization is required. // We just need to add an acceptance set if there is none. dba_is_minimal = dba_is_wdba = true; - if (type_ == BA) + if (type_ == Buchi) ensure_ba(dba); } else @@ -426,9 +433,9 @@ namespace spot // at hard levels if we want a small output. if (!dba || (level_ == High && PREF_ == Small)) { - if (((SBACC_ && a->prop_state_acc().is_true()) - || (type_ == BA && a->is_sba())) - && !tba_determinisation_) + if ((state_based_ && a->prop_state_acc().is_true()) + && !tba_determinisation_ + && (type_ != Buchi || a->acc().is_buchi())) { sim = do_sba_simul(a, ba_simul_); } @@ -437,11 +444,11 @@ namespace spot sim = do_simul(a, simul_); // Degeneralize the result of the simulation if needed. // No need to do that if tba_determinisation_ will be used. - if (type_ == BA && !tba_determinisation_) - sim = do_degen(sim); + if (type_ == Buchi && !tba_determinisation_) + sim = choose_degen(sim); else if (want_parity && !sim->acc().is_parity()) sim = do_degen_tba(sim); - else if (SBACC_ && !tba_determinisation_) + else if (state_based_ && !tba_determinisation_) sim = sbacc(sim); } } @@ -452,21 +459,16 @@ namespace spot if (!dba && is_deterministic(sim)) { std::swap(sim, dba); - // We postponed degeneralization above i case we would need + // We postponed degeneralization above in case we would need // to perform TBA-determinisation, but now it is clear // that we won't perform it. So do degeneralize. if (tba_determinisation_) { - if (type_ == BA) - { - dba = do_degen(dba); - assert(is_deterministic(dba)); - } - else if (SBACC_) - { - dba = sbacc(dba); - assert(is_deterministic(dba)); - } + if (type_ == Buchi) + dba = choose_degen(dba); + else if (state_based_) + dba = sbacc(dba); + assert(is_deterministic(dba)); } } @@ -513,8 +515,8 @@ namespace spot else { // degeneralize sim, because we did not do it earlier - if (type_ == BA) - sim = do_degen(sim); + if (type_ == Buchi) + sim = choose_degen(sim); } } @@ -552,7 +554,7 @@ namespace spot throw std::runtime_error ("postproc() not yet updated to mix sat-minimize and Generic"); unsigned target_acc; - if (type_ == BA) + if (type_ == Buchi) target_acc = 1; else if (sat_acc_ != -1) target_acc = sat_acc_; @@ -634,8 +636,8 @@ namespace spot // Degeneralize the dba resulting from tba-determinization or // sat-minimization (which is a TBA) if requested and needed. - if (dba && !dba_is_wdba && type_ == BA - && !(dba_is_minimal && state_based_ && dba->num_sets() == 1)) + if (dba && !dba_is_wdba && type_ == Buchi && state_based_ + && !(dba_is_minimal && dba->num_sets() == 1)) dba = degeneralize(dba); if (dba && sim) diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index c084078fa..375bf43b4 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -72,26 +72,29 @@ namespace spot /// options used for debugging or benchmarking. postprocessor(const option_map* opt = nullptr); - 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, - ParityMin = Parity | 8, - ParityMax = Parity | 16, - ParityOdd = Parity | 32, - ParityEven = Parity | 64, - ParityMinOdd = ParityMin | ParityOdd, - ParityMaxOdd = ParityMax | ParityOdd, - ParityMinEven = ParityMin | ParityEven, - ParityMaxEven = ParityMax | ParityEven, - CoBuchi = 128, + enum output_type { + TGBA = 0, // Historical. Use GeneralizedBuchi instead + GeneralizedBuchi = 0, // Introduced in Spot 2.10 to replace TGBA + BA = 1, // Historical. Implies Buchi and SBAcc. + Monitor = 2, + Generic = 3, + Parity = 4, + ParityMin = Parity | 8, + ParityMax = Parity | 16, + ParityOdd = Parity | 32, + ParityEven = Parity | 64, + ParityMinOdd = ParityMin | ParityOdd, + ParityMaxOdd = ParityMax | ParityOdd, + ParityMinEven = ParityMin | ParityEven, + ParityMaxEven = ParityMax | ParityEven, + CoBuchi = 128, + Buchi = 256, // introduced in Spot 2.10, does not imply SBAcc }; /// \brief Select the desired output type. /// - /// \c TGBA requires transition-based generalized Büchi acceptance - /// while \c BA requests state-based Büchi acceptance. In both + /// \c GeneralizedBuchi requires generalized Büchi acceptance + /// while \c Buchi requests Büchi acceptance. In both /// cases, automata with more complex acceptance conditions will /// be converted into these simpler acceptance. For references /// about the algorithms used behind these options, see section 5 @@ -116,17 +119,22 @@ namespace spot /// not all TGBA can be degeneralized, using \c Generic will allow /// parity acceptance to be used instead). /// - /// \a Parity and its variants request the acceptance condition to + /// \c Parity and its variants request the acceptance condition to /// be of some parity type. Note that the determinization /// algorithm used by Spot produces "parity min odd" acceptance, /// but other parity types can be obtained from there by minor /// adjustments. /// - /// \a CoBuchi requests a Co-Büchi automaton equivalent to + /// \c 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. + /// \c BA is a historical type that means Buchi and additionally + /// set state-based acceptance (this should normally be set + /// with `set_pref(SBAcc)`). + /// + /// If set_type() is not called, the default \c output_type is \c + /// GeneralizedBuchi. void set_type(output_type type) { @@ -221,6 +229,7 @@ namespace spot protected: 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 choose_degen(const twa_graph_ptr& input) 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; diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index dcdcb8175..6a39b37f6 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -142,7 +142,7 @@ namespace spot r2 = r2[0]; ++leading_x; } - if (type_ == Generic || type_ == TGBA) + if (type_ == Generic || type_ == GeneralizedBuchi) { // F(q|u|f) = q|F(u)|F(f) only for generic acceptance // G(q&e&f) = q&G(e)&G(f) @@ -174,7 +174,7 @@ namespace spot // with disjunction, but it seems to generate larger automata // in many cases and it needs to be further investigated. Maybe // this could be relaxed in the case of deterministic output. - (!r2.is(op::And) && (type_ == TGBA || type_ == BA))) + (!r2.is(op::And) && (type_ == GeneralizedBuchi || type_ == Buchi))) goto nosplit; op topop = r2.kind(); @@ -182,7 +182,7 @@ namespace spot std::vector oblg; std::vector susp; std::vector rest; - bool want_g = type_ == TGBA || type_ == BA; + bool want_g = type_ == GeneralizedBuchi || type_ == Buchi; for (formula child: r2) { if (child.is_syntactic_obligation()) @@ -213,7 +213,8 @@ namespace spot { // The only cases where we accept susp and rest to be both // non-empty is when doing Generic acceptance or TGBA. - if (!rest.empty() && !(type_ == Generic || type_ == TGBA)) + if (!rest.empty() + && !(type_ == Generic || type_ == GeneralizedBuchi)) { rest.insert(rest.end(), susp.begin(), susp.end()); susp.clear(); @@ -225,7 +226,7 @@ namespace spot } // For TGBA and BA, we only split if there is something to // suspend. - if (susp.empty() && (type_ == TGBA || type_ == BA)) + if (susp.empty() && (type_ == GeneralizedBuchi || type_ == Buchi)) goto nosplit; option_map om_wos; @@ -375,17 +376,19 @@ namespace spot if (gf_guarantee_ && PREF_ != Any) { bool det = unambiguous || (PREF_ == Deterministic); - bool sba = type_ == BA || (pref_ & SBAcc); - if ((type_ & (BA | Parity | Generic)) || type_ == TGBA) + if ((type_ & (Buchi | Parity)) + || type_ == Generic + || type_ == GeneralizedBuchi) aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), - det, sba); - if (aut2 && ((type_ == BA) || (type_ & Parity)) + det, state_based_); + if (aut2 && (type_ & (Buchi | Parity)) && (pref_ & Deterministic)) return finalize(aut2); if (!aut2 && (type_ == Generic || type_ & (Parity | CoBuchi))) { - aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); + aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), + state_based_); if (aut2 && (type_ & (CoBuchi | Parity)) && (pref_ & Deterministic)) @@ -418,6 +421,16 @@ namespace spot twa_graph_ptr translator::run(formula* f) { + if (type_ == BA) + { + pref_ |= SBAcc; + type_ = Buchi; + } + if (pref_ & SBAcc) + state_based_ = true; + else if (state_based_) + pref_ |= SBAcc; + if (simpl_owned_) { // Modify the options according to set_pref() and set_type(). diff --git a/tests/Makefile.am b/tests/Makefile.am index 94e4ac645..52c7be9b0 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -400,6 +400,7 @@ TESTS_python = \ python/interdep.py \ python/intrun.py \ python/kripke.py \ + python/langmap.py \ python/ltl2tgba.test \ python/ltlf.py \ python/ltlparse.py \ diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 6a20b5685..6b62441fa 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f419a180> >" + " *' at 0x7fc69c0f16c0> >" ] }, "execution_count": 2, @@ -187,7 +187,7 @@ } ], "source": [ - "a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a" + "a = spot.translate('(a U b) & GFc & GFd', 'Buchi', 'state-based', 'complete'); a" ] }, { @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f419adb0> >" + " *' at 0x7fc68d909240> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f41614b0> >" + " *' at 0x7fc68d9099c0> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f41613f0> >" + " *' at 0x7fc69e19d9c0> >" ] }, "execution_count": 8, @@ -966,7 +966,7 @@ } ], "source": [ - "f.translate('ba', 'small').show('.v')" + "f.translate('buchi', 'state-based', 'small').show('.v')" ] }, { @@ -1190,7 +1190,7 @@ } ], "source": [ - "f.translate('ba', 'det').show('v.')" + "f.translate('buchi', 'state-based', 'det').show('v.')" ] }, { @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4161ba0> >" + " *' at 0x7fc68d916150> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c300> >" + " *' at 0x7fc68d916450> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c5d0> >" + " *' at 0x7fc68d916a20> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f41747b0> >" + " *' at 0x7fc68d91ca20> >" ] }, "metadata": {}, @@ -1974,7 +1974,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4174720> >" + " *' at 0x7fc68d91c9c0> >" ] }, "metadata": {}, @@ -2132,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4174c30> >" + " *' at 0x7fc68d91cd80> >" ] }, "metadata": {}, @@ -2280,7 +2280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4174b10> >" + " *' at 0x7fc68d91ccc0> >" ] }, "metadata": {}, @@ -2291,8 +2291,8 @@ "a = spot.automaton('example1.aut')\n", "display(a)\n", "display(spot.remove_fin(a))\n", - "display(a.postprocess('TGBA', 'complete'))\n", - "display(a.postprocess('BA'))" + "display(a.postprocess('GeneralizedBuchi', 'complete'))\n", + "display(a.postprocess('Buchi', \"SBAcc\"))" ] }, { @@ -2469,7 +2469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f41748a0> >" + " *' at 0x7fc68d91cb40> >" ] }, "execution_count": 19, @@ -2545,7 +2545,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4179450> >" + " *' at 0x7fc68d925690> >" ] }, "execution_count": 20, @@ -3095,7 +3095,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c9f0> >" + " *' at 0x7fc68d91c480> >" ] }, "metadata": {}, @@ -3195,7 +3195,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f4174300> >" + " *' at 0x7fc68d91c510> >" ] }, "execution_count": 24, @@ -3268,7 +3268,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c510> >" + " *' at 0x7fc68d91c2d0> >" ] }, "execution_count": 25, @@ -3439,7 +3439,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416ccf0> >" + " *' at 0x7fc68d9164e0> >" ] }, "execution_count": 27, @@ -3522,7 +3522,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c9f0> >" + " *' at 0x7fc68d91c480> >" ] }, "metadata": {}, @@ -3587,7 +3587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c9f0> >" + " *' at 0x7fc68d91c480> >" ] }, "metadata": {}, @@ -3674,7 +3674,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f33f416c9f0> >" + " *' at 0x7fc68d91c480> >" ] }, "execution_count": 29, @@ -3707,7 +3707,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.5" + "version": "3.8.6" } }, "nbformat": 4, diff --git a/tests/python/langmap.py b/tests/python/langmap.py index 5d4ce3cd5..6fd860986 100644 --- a/tests/python/langmap.py +++ b/tests/python/langmap.py @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2017, 2020 Laboratoire de Recherche et Développement # de l'Epita (LRDE) # # This file is part of Spot, a model checking library. @@ -29,7 +29,7 @@ def hstates(txt): def test(f, opt, expected): - aut = spot.translate(f, opt, 'deterministic') + aut = spot.translate(f, *opt, 'deterministic') v = spot.language_map(aut) assert len(v) == aut.num_states() spot.highlight_languages(aut) @@ -40,15 +40,15 @@ def test(f, opt, expected): exit(1) -test('GF(a) & GFb & c', 'BA', '1 0 2 0 3 0') -test('GF(a) & c & X!a', 'BA', '2 0 3 0') -test('(a U b) & GF(c & Xd)', 'generic', '1 0 2 0') -test('GF(a <-> Xb) & Fb', 'generic', '0 0 1 1 2 0 3 1 4 1') -test('Xa', 'BA', '') +test('GF(a) & GFb & c', ['Buchi', 'SBAcc'], '1 0 2 0 3 0') +test('GF(a) & c & X!a', ['Buchi', 'SBAcc'], '2 0 3 0') +test('(a U b) & GF(c & Xd)', ['generic'], '1 0 2 0') +test('GF(a <-> Xb) & Fb', ['generic', 'low'], '1 0 2 0 3 0') +test('Xa', ['Buchi', 'SBAcc'], '') # Non-deterministic automata are not supported try: - test('FGa', 'BA', '') + test('FGa', ['Buchi'], '') except RuntimeError as e: assert 'language_map only works with deterministic automata'in str(e) else: diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py index 4c01e345f..d1234bd69 100644 --- a/tests/python/misc-ec.py +++ b/tests/python/misc-ec.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, 2020 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -18,7 +18,7 @@ # along with this program. If not, see . import spot -aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA') +aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'Buchi', 'SBAcc') ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut) n = 0 while True: diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 7b41f1ac2..3e9c7c8b1 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -265,7 +265,7 @@ } ], "source": [ - "aut = f.translate('det', 'BA'); aut" + "aut = f.translate('det', 'Buchi', 'SBAcc'); aut" ] }, { diff --git a/tests/python/satmin.py b/tests/python/satmin.py index caf639463..156b27ea8 100644 --- a/tests/python/satmin.py +++ b/tests/python/satmin.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2020 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -20,7 +20,7 @@ import spot -aut = spot.translate('GFa & GFb', 'BA') +aut = spot.translate('GFa & GFb', 'Buchi', 'SBAcc') assert aut.num_sets() == 1 assert aut.num_states() == 3 assert aut.is_deterministic() diff --git a/tests/python/toweak.py b/tests/python/toweak.py index 550ab6408..b2d908037 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -31,7 +31,7 @@ b | (a & XF(b R a)) | (!a & XG(!b U !a))""" def test_phi(phi): - a = spot.translate(phi, 'TGBA', 'SBAcc') + a = spot.translate(phi, 'GeneralizedBuchi', 'SBAcc') res = spot.to_weak_alternating(spot.dualize(a)) assert res.equivalent_to(spot.formula.Not(spot.formula(phi)))