Commit 77f3ba94 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

translate: fix stutter-invariant flag on leading Xs

Issue discovered by Mikuláš Klokočka and reported by František
Blahoudek.

* spot/twaalgos/translate.cc: Reset the stutter-invariant flag
when adding extra transitions for leading Xs.
* tests/core/stutter-tgba.test: New test case.
* NEWS: Mention the bug.
parent 560c6f2d
Pipeline #5062 passed with stages
in 451 minutes and 42 seconds
......@@ -90,6 +90,10 @@ New in spot 2.6.3.dev (not yet released)
Bugs fixed:
- translate() would incorrectly mark as stutter-invariant
some automata produced from formulas of the form X(f...)
where f... is syntactically stutter-invariant.
- acc_cond::is_generalized_rabin() and
acc_cond::is_generalized_streett() did not recognize the cases
were a single generalized pair is used.
......
......@@ -313,6 +313,10 @@ namespace spot
}
while (--leading_x);
aut->set_init_state(init);
// Adding initial edges is very likely to kill stutter
// invariance (and it certainly cannot fix it).
if (aut->prop_stutter_invariant().is_true())
aut->prop_stutter_invariant(trival::maybe());
}
}
else
......
......@@ -103,6 +103,16 @@ test `autfilt -c --is-stutter-invariant input` = 0
grep '!deterministic' input.2
grep '!stutter-invariant' input.2
# From an email by František Blahoudek and Mikuláš Klokočka
ltl2tgba 'X(a & GF(a | Gb))' > input
grep stutter input && exit 1
grep deterministic input && exit 1
# This will involve a complementation
run 0 autfilt -H1.1 --check=stutter input > input.2
test `autfilt -c --is-stutter-invariant input` = 0
grep '!deterministic' input.2
grep '!stutter-invariant' input.2
# From an email by Anton Pirogov
cat >pirogov <<EOF
......
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