Commit 1f90e1cf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

fix ltl2tgba -B not always returning Inf(0)

Reported by František Blahoudek.

* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.
parent 67b9bfda
New in spot 2.8.4.dev (not yet released)
Nothing yet.
Bugs fixed:
- ltl2tgba -B could return automata with "t" acceptance, instead
of the expected Inf(0).
New in spot 2.8.4 (2019-12-08)
......
......@@ -163,6 +163,15 @@ namespace spot
degen_lowinit_, degen_remscc_);
}
static void
force_buchi(twa_graph_ptr& a)
{
assert(a->acc().is_t());
acc_cond::mark_t m = a->set_buchi();
for (auto& e: a->edges())
e.acc = m;
}
twa_graph_ptr
postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const
{
......@@ -196,6 +205,8 @@ namespace spot
tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp);
if (SBACC_)
tmp = sbacc(tmp);
if (type_ == BA && tmp->acc().is_t())
force_buchi(tmp);
if (want_parity)
{
reduce_parity_here(tmp, COLORED_);
......
......@@ -292,3 +292,6 @@ test 2 = `ltl2tgba -f "$f" --low -x tls-impl=3 --stats=%s`
# This is not optimal, the smallest DBA for this formula has 2 states.
test 3 = `ltl2tgba -BD -f 'GF((p0 & GF!p0) | (!p0 & FGp0))' --stats=%s`
# Some versions of Spot incorrectly returned "t" automata with -B
test "Inf(0)" = "`ltl2tgba -B 'Xb | G!b' --stats=%g`"
Supports Markdown
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