From 566a43dd17631b23a4835739c2e85cb4277d6b1a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Oct 2019 15:18:48 +0200 Subject: [PATCH] improve readability of parity(false, true, 5) * spot/twa/acc.hh: Introduce parity_min_odd(n) and friends. * spot/twaalgos/determinize.cc, spot/twaalgos/rabin2parity.cc, spot/twaalgos/toparity.cc: Use them. * tests/python/parity.py: Call each function exhaustively. * NEWS: Mention the new functions. --- NEWS | 10 ++++++++++ spot/twa/acc.hh | 32 +++++++++++++++++++++++++++++--- spot/twaalgos/determinize.cc | 2 +- spot/twaalgos/rabin2parity.cc | 28 ++++++++++++++-------------- spot/twaalgos/toparity.cc | 13 ++++++------- tests/python/parity.py | 14 ++++++++++++++ 6 files changed, 74 insertions(+), 25 deletions(-) diff --git a/NEWS b/NEWS index 2f359d168..31f3a96ec 100644 --- a/NEWS +++ b/NEWS @@ -30,6 +30,16 @@ New in spot 2.8.2.dev (not yet released) variants of F[n:m] and G[n:m], but those four are only implemented as syntactic sugar. + - acc_cond::acc_code::parity(bool, bool, int) was not very readable, + as it was unclear to the reader what the boolean argument meant. + The following sister functions can now improve readability: + parity_max(is_odd, n) = parity(true, is_odd, n) + parity_max_odd(n) = parity_max(true, n) + parity_max_even(n) = parity_max(false, n) + parity_min(is_odd, n) = parity(false, is_odd, n) + parity_min_odd(n) = parity_min(true, n) + parity_min_even(n) = parity_min(false, n) + Python: - Doing "import spot.foo" will now load any spot-extra/foo.py on diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index cad84f7da..6ddde3ef8 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -816,11 +816,37 @@ namespace spot /// \brief Build a parity acceptance condition /// - /// In parity acceptance a word is accepting if the maximum (or + /// In parity acceptance a run is accepting if the maximum (or /// minimum) set number that is seen infinitely often is odd (or - /// even). This function will build a formula for that, as + /// even). These functions will build a formula for that, as /// specified in the HOA format. - static acc_code parity(bool max, bool odd, unsigned sets); + /// @{ + static acc_code parity(bool is_max, bool is_odd, unsigned sets); + static acc_code parity_max(bool is_odd, unsigned sets) + { + return parity(true, is_odd, sets); + } + static acc_code parity_max_odd(unsigned sets) + { + return parity_max(true, sets); + } + static acc_code parity_max_even(unsigned sets) + { + return parity_max(false, sets); + } + static acc_code parity_min(bool is_odd, unsigned sets) + { + return parity(false, is_odd, sets); + } + static acc_code parity_min_odd(unsigned sets) + { + return parity_min(true, sets); + } + static acc_code parity_min_even(unsigned sets) + { + return parity_min(false, sets); + } + /// @} /// \brief Build a random acceptance condition /// diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 20f4a54ba..307f07613 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -965,7 +965,7 @@ namespace spot if (sets % 2 == 1) sets += 1; // Acceptance is now min(odd) since we can emit Red on paths 0 with new opti - res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets)); + res->set_acceptance(sets, acc_cond::acc_code::parity_min_odd(sets)); res->prop_universal(true); res->prop_state_acc(false); diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc index c307b08bb..2fb31d2ac 100644 --- a/spot/twaalgos/rabin2parity.cc +++ b/spot/twaalgos/rabin2parity.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -77,19 +77,19 @@ namespace spot build_iar_scc(scc_.initial()); - // resulting automaton has acceptance condition: parity max odd - // with priorities ranging from 0 to 2*(nb pairs) - // /!\ priorities are shifted by -1 compared to the original paper - if (is_rabin) - res_->set_acceptance(2*pairs_.size() + 1, - acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1)); - else - res_->set_acceptance(2*pairs_.size() + 1, - acc_cond::acc_code::parity(true, false, 2*pairs_.size() + 1)); - - // set initial state - res_->set_init_state( - iar2num.at(state2iar.at(aut_->get_init_state_number()))); + { + // resulting automaton has acceptance condition: parity max odd + // for Rabin-like input and parity max even for Streett-like input. + // with priorities ranging from 0 to 2*(nb pairs) + // /!\ priorities are shifted by -1 compared to the original paper + unsigned sets = 2 * pairs_.size() + 1; + res_->set_acceptance(sets, acc_cond::acc_code::parity_max(is_rabin, + sets)); + } + { + unsigned s = iar2num.at(state2iar.at(aut_->get_init_state_number())); + res_->set_init_state(s); + } // there could be quite a number of unreachable states, prune them res_->purge_unreachable_states(); diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index f612e4ca1..51046fadd 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -128,18 +128,17 @@ namespace spot lar_state dst{e.dst, new_perm}; unsigned dst_num = get_state(dst); - // do the h last elements satisfy the acceptance condition? + // Do the h last elements satisfy the acceptance condition? + // If they do, emit 2h, if they don't emit 2h+1. acc_cond::mark_t m(new_perm.end() - h, new_perm.end()); - if (aut_->acc().accepting(m)) - res_->new_edge(src_num, dst_num, e.cond, {2*h}); - else - res_->new_edge(src_num, dst_num, e.cond, {2*h+1}); + bool rej = !aut_->acc().accepting(m); + res_->new_edge(src_num, dst_num, e.cond, {2*h + rej}); } } // parity max even - res_->set_acceptance(2*aut_->num_sets() + 2, - acc_cond::acc_code::parity(true, false, 2*aut_->num_sets() + 2)); + unsigned sets = 2*aut_->num_sets() + 2; + res_->set_acceptance(sets, acc_cond::acc_code::parity_max_even(sets)); if (pretty_print) { diff --git a/tests/python/parity.py b/tests/python/parity.py index 738fb18d8..84a3437aa 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -20,6 +20,20 @@ import spot +max_even_5 = spot.acc_code.parity(True, False, 5) +assert max_even_5 == spot.acc_code.parity_max_even(5) +assert max_even_5 == spot.acc_code.parity_max(False, 5) +min_even_5 = spot.acc_code.parity(False, False, 5) +assert min_even_5 == spot.acc_code.parity_min_even(5) +assert min_even_5 == spot.acc_code.parity_min(False, 5) + +max_odd_5 = spot.acc_code.parity(True, True, 5) +assert max_odd_5 == spot.acc_code.parity_max_odd(5) +assert max_odd_5 == spot.acc_code.parity_max(True, 5) +min_odd_5 = spot.acc_code.parity(False, True, 5) +assert min_odd_5 == spot.acc_code.parity_min_odd(5) +assert min_odd_5 == spot.acc_code.parity_min(True, 5) + for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'): a1 = spot.translate(f, 'parity')