From 42ebf8b18c4b93bb65050591741d907c8a00ec70 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Jan 2018 12:06:03 +0100 Subject: [PATCH] postproc: introduce --parity output * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add parity options. * bin/common_post.cc: Add support for --parity. * NEWS: Mention it. * tests/core/parity2.test: New file. * tests/Makefile.am: Add it. --- NEWS | 10 ++ bin/common_post.cc | 49 +++++++- spot/twaalgos/postproc.cc | 75 ++++++++---- spot/twaalgos/postproc.hh | 34 +++-- tests/Makefile.am | 11 +- tests/core/parity2.test | 252 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 390 insertions(+), 41 deletions(-) create mode 100755 tests/core/parity2.test diff --git a/NEWS b/NEWS index 24f3b3ec2..c50079e42 100644 --- a/NEWS +++ b/NEWS @@ -47,6 +47,11 @@ New in spot 2.4.4.dev (net yet released) - ltlsynt is a new tool for synthesizing a controller from LTL/PSL specifications. + - ltl2tgba, autfilt, and dstar2tgba have a new '--parity' option to + force parity acceptance on the output. Different styles can be + requested using for instance --parity='min odd' or --parity='max + even'. + - ltldo learned to limit the number of automata it outputs using -n. - autcross, ltlcross, and ltldo learned --fail-on-timeout. @@ -176,6 +181,11 @@ New in spot 2.4.4.dev (net yet released) optimization for stutter-invariant automata that may produce slightly smaller automata. + - spot::postprocessor::set_type() can now request different forms of + parity acceptance as output. However currently the conversions + are not very smart: if the input does not already have parity + acceptance, it will simply be degeneralized or determinized. + - acc_cond::name(fmt) is a new method that name well-known acceptance conditions. The fmt parameter specify the format to use for that name (e.g. to the style used in HOA, or that used by print_dot()). diff --git a/bin/common_post.cc b/bin/common_post.cc index b6796f1b8..5b1766f33 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,6 +21,7 @@ #include "common_r.hh" #include "common_aoutput.hh" #include "error.h" +#include "argmatch.h" spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_pref pref = spot::postprocessor::Small; @@ -55,6 +56,10 @@ static constexpr const argp_option options[] = { "state-based-acceptance", 'S', nullptr, 0, "define the acceptance using states", 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "parity", 'P', + "any|min|max|odd|even|min odd|min even|max odd|max even", + OPTION_ARG_OPTIONAL, + "automaton with parity acceptance", 0, }, /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, @@ -105,6 +110,10 @@ static const argp_option options_disabled[] = { "state-based-acceptance", 'S', nullptr, 0, "define the acceptance using states", 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "parity", 'P', + "[any|min|max|odd|even|min odd|min even|max odd|max even]", + OPTION_ARG_OPTIONAL, + "automaton with parity acceptance", 0, }, /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, @@ -123,7 +132,7 @@ static const argp_option options_disabled[] = }; static int -parse_opt_post(int key, char*, struct argp_state*) +parse_opt_post(int key, char* arg, struct argp_state*) { // This switch is alphabetically-ordered. switch (key) @@ -148,6 +157,40 @@ parse_opt_post(int key, char*, struct argp_state*) case 'M': type = spot::postprocessor::Monitor; break; + case 'P': + { + static char const *const parity_args[] = + { + "any", "min", "max", "odd", "even", + "min odd", "odd min", + "min even", "even min", + "max odd", "odd max", + "max even", "even max", + nullptr + }; + static spot::postprocessor::output_type const parity_types[] = + { + spot::postprocessor::Parity, + spot::postprocessor::ParityMin, + spot::postprocessor::ParityMax, + spot::postprocessor::ParityOdd, + spot::postprocessor::ParityEven, + spot::postprocessor::ParityMinOdd, + spot::postprocessor::ParityMinOdd, + spot::postprocessor::ParityMinEven, + spot::postprocessor::ParityMinEven, + spot::postprocessor::ParityMaxOdd, + spot::postprocessor::ParityMaxOdd, + spot::postprocessor::ParityMaxEven, + spot::postprocessor::ParityMaxEven, + }; + ARGMATCH_VERIFY(parity_args, parity_types); + if (arg) + type = XARGMATCH("--parity", arg, parity_args, parity_types); + else + type = spot::postprocessor::Parity; + } + break; case 'S': sbacc = spot::postprocessor::SBAcc; break; diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 375f3224e..d931c67b4 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -35,6 +35,7 @@ #include #include #include +#include namespace spot { @@ -147,6 +148,15 @@ namespace spot return do_sba_simul(d, ba_simul_); } + twa_graph_ptr + postprocessor::do_degen_tba(const twa_graph_ptr& a) + { + return degeneralize_tba(a, + degen_reset_, degen_order_, + degen_cache_, degen_lskip_, + degen_lowinit_, degen_remscc_); + } + twa_graph_ptr postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) { @@ -183,6 +193,33 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; + bool want_parity = (type_ & Parity) == Parity; + + auto finalize = [&](twa_graph_ptr tmp) + { + if (COMP_) + tmp = complete(tmp); + if (want_parity && tmp->acc().is_generalized_buchi()) + tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp); + if (SBACC_) + tmp = sbacc(tmp); + if (want_parity) + { + parity_kind kind = parity_kind_any; + parity_style style = parity_style_any; + if ((type_ & ParityMin) == ParityMin) + kind = parity_kind_min; + else if ((type_ & ParityMax) == ParityMax) + kind = parity_kind_max; + if ((type_ & ParityOdd) == ParityOdd) + style = parity_style_odd; + else if ((type_ & ParityEven) == ParityEven) + style = parity_style_even; + change_parity_here(tmp, kind, style); + } + return tmp; + }; + if (!a->is_existential() && // We will probably have to revisit this condition later. // Currently, the intent is that postprocessor should never @@ -191,7 +228,8 @@ namespace spot !(type_ == Generic && PREF_ == Any && level_ == Low)) a = remove_alternation(a); - if (type_ != Generic && !a->acc().is_generalized_buchi()) + if ((type_ != Generic && !a->acc().is_generalized_buchi()) + || (want_parity && !a->acc().is_parity())) { a = to_generalized_buchi(a); if (PREF_ == Any && level_ == Low) @@ -202,14 +240,9 @@ namespace spot && (type_ == Generic || type_ == TGBA || (type_ == BA && a->is_sba()) - || (type_ == Monitor && a->num_sets() == 0))) - { - if (COMP_) - a = complete(a); - if (SBACC_) - a = sbacc(a); - return a; - } + || (type_ == Monitor && a->num_sets() == 0) + || (want_parity && a->acc().is_parity()))) + return finalize(a); int original_acc = a->num_sets(); @@ -244,20 +277,14 @@ namespace spot } a->remove_unused_ap(); } - if (COMP_) - a = complete(a); - return a; + return finalize(a); } if (PREF_ == Any) { if (type_ == BA) a = do_degen(a); - if (COMP_) - a = complete(a); - if (SBACC_) - a = sbacc(a); - return a; + return finalize(a); } bool dba_is_wdba = false; @@ -305,6 +332,8 @@ namespace spot // No need to do that if tba_determinisation_ will be used. if (type_ == BA && !tba_determinisation_) sim = do_degen(sim); + else if (want_parity && !sim->acc().is_parity()) + sim = do_degen_tba(sim); else if (SBACC_ && !tba_determinisation_) sim = sbacc(sim); } @@ -382,7 +411,7 @@ namespace spot } } - if (PREF_ == Deterministic && type_ == Generic && !dba) + if ((PREF_ == Deterministic && (type_ == Generic || want_parity)) && !dba) { dba = tgba_determinize(to_generalized_buchi(sim), false, det_scc_, det_simul_, det_stutter_); @@ -517,12 +546,6 @@ namespace spot sim = dba ? dba : sim; sim->remove_unused_ap(); - - if (COMP_) - sim = complete(sim); - if (SBACC_) - sim = sbacc(sim); - - return sim; + return finalize(sim); } } diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index f2b0fa635..072e5d2a7 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -72,7 +72,20 @@ namespace spot /// options used for debugging or benchmarking. postprocessor(const option_map* opt = nullptr); - enum output_type { TGBA, BA, Monitor, Generic }; + enum output_type { TGBA = 0, + BA = 1, + 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, + }; /// \brief Select the desired output type. /// @@ -96,11 +109,17 @@ namespace spot /// SystemC" (Deian Tabakov and Moshe Y. Vardi, Proceedings of /// RV’10, LNCS 6418). /// - /// Finally \c Generic remove all constraints about the acceptance - /// condition. Using \c Generic can be needed to force the - /// determinization of some automata (e.g., not all TGBA can be - /// degeneralized, using \c Generic will allow parity acceptance - /// to be used instead). + /// \c Generic removes all constraints about the acceptance + /// condition. Using \c Generic (or \c Parity below) can be + /// needed to force the determinization of some automata (e.g., + /// 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 + /// 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. /// /// If set_type() is not called, the default \c output_type is \c TGBA. void @@ -195,6 +214,7 @@ namespace spot twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_degen(const twa_graph_ptr& input); + twa_graph_ptr do_degen_tba(const twa_graph_ptr& input); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); diff --git a/tests/Makefile.am b/tests/Makefile.am index 1d3521eb2..bca0a8a57 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,10 +1,10 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 -## Laboratoire de Recherche et Développement de l'Epita (LRDE). -## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -## Université Pierre et Marie Curie. +## Copyright (C) 2009-2018 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). +## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 +## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +## Pierre et Marie Curie. ## ## This file is part of Spot, a model checking library. ## @@ -310,6 +310,7 @@ TESTS_twa = \ core/dca.test \ core/dnfstreett.test \ core/parity.test \ + core/parity2.test \ core/ltlsynt.test ############################## PYTHON ############################## diff --git a/tests/core/parity2.test b/tests/core/parity2.test new file mode 100755 index 000000000..ddbfd401a --- /dev/null +++ b/tests/core/parity2.test @@ -0,0 +1,252 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +rm -rf res res2 + +for x in P 'Pmin odd' 'Pmax even'; do + ltl2tgba "-$x" FGa 'GFa & GFb' >>res + ltl2tgba FGa 'GFa & GFb' | autfilt --name=%M --high "-$x" >>res2 + ltl2tgba -D "-$x" FGa 'GFa & GFb' >>res3 + ltl2tgba FGa 'GFa & GFb' | autfilt -D --name=%M --high "-$x" >>res4 +done + +cat >expected<expected2< XXXb)'