diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 8b2439252..90c6eec3d 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,6 +117,15 @@ the determinization algorithm.") }, the determinization algorithm.") }, { DOC("det-stutter", "Set to 0 to disable optimizations based on \ the stutter-invariance in the determinization algorithm.") }, + { DOC("gen-reduce-parity", "When the postprocessor routines are \ +configured to output automata with any kind of acceptance condition, \ +but they happen to process an automaton with parity acceptance, they \ +call a function to minimize the number of colors needed. This option \ +controls what happen when this reduction does not reduce the number of \ +colors: when set (the default) the output of the reduction is returned, \ +this means the colors in the automaton may have changed slightly, and in \ +particular, there is no transition with more than one color; when unset, \ +the original automaton is returned.") }, { DOC("gf-guarantee", "Set to 0 to disable alternate constructions \ for GF(guarantee)->[D]BA and FG(safety)->DCA. Those constructions \ are from an LICS'18 paper by J. Esparza, J. Křentínský, and S. Sickert. \ diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 698f31371..3d9df7e1f 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -84,6 +84,7 @@ namespace spot sat_states_ = opt->get("sat-states", 0); state_based_ = opt->get("state-based", 0); wdba_minimize_ = opt->get("wdba-minimize", 1); + gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); if (sat_acc_ && sat_minimize_ == 0) sat_minimize_ = 1; // Dicho. @@ -254,15 +255,25 @@ namespace spot bool isparity = in->acc().is_parity(); if (isparity && in->is_existential() && (type_ == Generic || want_parity)) - return reduce_parity(in); - if (!(want_parity && isparity)) { - if (level_ == High) - return simplify_acceptance(in); - else - return cleanup_acceptance(in); + auto res = reduce_parity(in); + if (want_parity || gen_reduce_parity_) + return res; + // In case type_ == Generic and gen_reduce_parity_ == 0, + // we only return the result of reduce_parity() if it can + // lower the number of colors. Otherwise, + // simplify_acceptance() will not do better and we return + // the input unchanged. The reason for not always using + // the output of reduce_parity() is that is may hide + // symmetries between automata, as in issue #402. + return (res->num_sets() < in->num_sets()) ? res : in; } - return cleanup_parity(in); + if (want_parity && isparity) + return cleanup_parity(in); + if (level_ == High) + return simplify_acceptance(in); + else + return cleanup_acceptance(in); }; a = simplify_acc(a); diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 8a75dfe32..5b739e5b7 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -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. @@ -251,6 +251,7 @@ namespace spot bool sat_langmap_ = false; int sat_acc_ = 0; int sat_states_ = 0; + int gen_reduce_parity_ = 1; bool state_based_ = false; bool wdba_minimize_ = true; }; diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 325c87c36..7ef799662 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -226,22 +226,32 @@ namespace spot if (susp.empty() && (type_ == TGBA || type_ == BA)) goto nosplit; - option_map om; + option_map om_wos; + option_map om_ws; if (opt_) - om = *opt_; - om.set("ltl-split", 0); - translator translate_without_split(simpl_, &om); + om_ws = *opt_; + // Don't blindingly apply reduce_parity() in the + // generic case, for issue #402. + om_ws.set("gen-reduce-parity", 0); + om_wos = om_ws; + om_wos.set("ltl-split", 0); + translator translate_without_split(simpl_, &om_wos); // Never force colored automata at intermediate steps. // This is best added at the very end. translate_without_split.set_pref(pref_ & ~Colored); translate_without_split.set_level(level_); translate_without_split.set_type(type_); + translator translate_with_split(simpl_, &om_ws); + translate_with_split.set_pref(pref_ & ~Colored); + translate_with_split.set_level(level_); + translate_with_split.set_type(type_); + auto transrun = [&](formula f) { if (f == r2) return translate_without_split.run(f); else - return run(f); + return translate_with_split.run(f); }; // std::cerr << "splitting\n"; diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index e83d4d1ac..22c005146 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -419,7 +419,6 @@ f=$f'& (!b | X(b | (a R !b))) & (!d | X(d | (c R !d))) & F(a | !b) & F(c | !d))' test '8,1' = `ltl2tgba "$f" --stats=%s,%d` test '8,1' = `ltl2tgba -GD "$f" --stats=%s,%d` - # Two formulas for which ltl2tgba 2.7.3 was raising an error with -GDS # Reported by David Müller. cat >in <expected < c) W d))' | grep '\[f\]' && exit 1 # Reported by Jens Kreber @@ -448,4 +446,9 @@ ltl2tgba 'X!c & X(b & c & d & a U e)' --stats=%w | grep 0 && exit 1 # would in turn cause the HOA printer to choke. ltlcross -f 'G(F(Gb ^ Fa) & FG!a)' 'ltl2tgba -G -D' +# Issue #402, reported by Juraj Major. +f='(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)' +test 1,8,3 = `ltl2tgba -G -D "$f" --stats=%s,%e,%a` +test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a` + :