From fd0d752bc3d4a8427655c6f5e2aefebcce18f430 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Apr 2020 15:20:53 +0200 Subject: [PATCH] to_parity: only call reduce_parity() when prefix_parity is enabled Calling reduce_parity() in to_parity() is confusing, because then running to_parity() on one SCC does not necessarily produce the same output as running to_parity() on the entire automaton. However it is necessary for the implementation of parity_prefix. As a compromise, disable reduce_parity() when parity_prefix is disabled, this way we can use that to demonstrate how the algorithm works. * spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not call reduce_parity() when parity_prefix is disabled. * tests/python/toparity.py: Adjust. --- spot/twaalgos/toparity.cc | 20 ++++++++++++++++---- spot/twaalgos/toparity.hh | 36 +++++++++++++++++++++++------------- tests/python/toparity.py | 10 +++++++--- 3 files changed, 46 insertions(+), 20 deletions(-) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 09fa6a5c1..df707f865 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1679,13 +1679,25 @@ run() res_->set_init_state(initial_state_res->second); else res_->new_state(); - res_->set_acceptance( - acc_cond::acc_code::parity_max(is_odd, SPOT_MAX_ACCSETS)); if (options.pretty_print) res_->set_named_prop("state-names", names); - reduce_parity_here(res_); + res_->purge_unreachable_states(); - // res_->merge_states(); + // If parity_prefix is used, we use all available colors by + // default: The IAR/CAR are using lower indices, and the prefix is + // using the upper indices. So we use reduce_parity() to clear + // the mess. If parity_prefix is not used, + unsigned max_color = SPOT_MAX_ACCSETS; + if (!options.parity_prefix) + { + acc_cond::mark_t all = {}; + for (auto& e: res_->edges()) + all |= e.acc; + max_color = all.max_set(); + } + res_->set_acceptance(acc_cond::acc_code::parity_max(is_odd, max_color)); + if (options.parity_prefix) + reduce_parity_here(res_); return res_; } diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index a8e631baa..a97fda0e6 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -31,16 +31,16 @@ namespace spot /// several elements in a record, it tries to find an order such /// that the new permutation already exists. bool search_ex = true; - /// If \a use_last is true and \a search_ex are true, we use the + /// If \c use_last is true and \a search_ex are true, we use the /// most recent state when we find multiple existing state /// compatible with the current move. - bool use_last = true; - /// If \a force_order is true, we force to use an order when CAR or IAR is + bool use_last = true; + /// If \c force_order is true, we force to use an order when CAR or IAR is /// applied. Given a state s and a set E ({0}, {0 1}, {2} for example) we /// construct an order on colors. With the given example, we ask to have /// a permutation that start with [0 …], [0 1 …] or [2 …] in /// that order of preference. - bool force_order = true; + bool force_order = true; /// If \c partial_degen is true, apply a partial /// degeneralization to remove occurrences of acceptance /// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`. @@ -51,15 +51,25 @@ namespace spot /// If \c scc_acc_clean is true, to_parity() will ignore colors /// no occoring in an SCC while processing this SCC. bool acc_clean = true; - /// If \a parity_equiv is true, to_parity() will check if there + /// If \c parity_equiv is true, to_parity() will check if there /// exists a permutations of colors such that the acceptance /// condition is a parity condition. - bool parity_equiv = true; - /// If \a parity_prefix is true, to_parity() will remove the prefix of - /// the acceptance condition that correspond to parity, works on the - // remaining and adds marks to process the prefix. - bool parity_prefix = true; - /// If \a rabin_to_buchi is true, to_parity() tries to convert a Rabin or + bool parity_equiv = true; + /// If \c parity_prefix is true, to_parity() will use a special + /// handling for acceptance conditions of the form `Inf(m0) | + /// (Fin(m1) & (Inf(m2) | (… β)))` that start as a parity + /// condition (modulo a renumbering of `m0`, `m1`, `m2`, ...) but where + /// `β` can be an arbitrary formula. In this case, the paritization + /// algorithm is really applied only to `β`, and the marks of the + /// prefix are appended after a suitable renumbering. + /// + /// For technical reasons, activating this option (and this is the + /// default) causes reduce_parity() to be called at the end to + /// minimize the number of colors used. It is therefore + /// recommended to disable this option when one wants to follow + /// the output CAR/IAR constructions. + bool parity_prefix = true; + /// If \c rabin_to_buchi is true, to_parity() tries to convert a Rabin or /// Streett condition to Büchi or co-Büchi with /// rabin_to_buchi_if_realizable(). bool rabin_to_buchi = true; @@ -69,8 +79,8 @@ namespace spot /// Use propagate_marks_here to increase the number of marks on transition /// in order to move more colors (and increase the number of /// compatible states) when we apply LAR. - bool propagate_col = true; - /// If \a pretty_print is true, states of the output automaton are + bool propagate_col = true; + /// If \c pretty_print is true, states of the output automaton are /// named to help debugging. bool pretty_print = false; }; diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 9ebaabc14..c3b193be8 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -106,6 +106,10 @@ def test(aut, expected_num_states=[], full=True): propagate_col = opt.propagate_col, pretty_print = opt.pretty_print, ) + p1st, p1ed, p1se = p1.num_states(), p1.num_edges(), p1.num_sets() + if opt.parity_prefix is False: + # Reduce the number of colors to help are_equivalent + spot.reduce_parity_here(p1) assert spot.are_equivalent(aut, p1) if expected_num is not None: assert p1.num_states() == expected_num @@ -113,9 +117,9 @@ def test(aut, expected_num_states=[], full=True): # Make sure passing opt is the same as setting # each argument individually p2 = spot.to_parity(aut, opt) - assert p2.num_states() == p1.num_states() - assert p2.num_edges() == p1.num_edges() - assert p2.num_sets() == p1.num_sets() + assert p2.num_states() == p1st + assert p2.num_edges() == p1ed + assert p2.num_sets() == p1se test(spot.automaton("""HOA: v1 name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &