Commit 67060420 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

postproc: fix issue #402

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/translate.cc: Introduce a gen-reduce-parity option and
use it on sub-automata built by ltl-split.
* bin/spot-x.cc: Document it.
* tests/core/ltl2tgba2.test: Add test case reported by Juraj Major.
parent fe340ae8
Pipeline #18360 passed with stages
in 185 minutes and 10 seconds
// -*- 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. \
......
......@@ -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);
......
// -*- 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;
};
......
// -*- 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";
......
......@@ -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 <<EOF
......@@ -432,8 +431,7 @@ cat >expected <<EOF
8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2))
EOF
# This formulas used to produce translation with false label.
# These formulas used to produce translation with false label.
# Reported by Florian Renkin
ltl2tgba -D -G 'F(G(a | !a) & ((b <-> 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`
:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment