diff --git a/NEWS b/NEWS index 2c1732adb..051aa9f4a 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 4f50117a0..9fee4e847 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -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 diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test index 2d81b7778..fd3d26f1a 100755 --- a/tests/core/stutter-tgba.test +++ b/tests/core/stutter-tgba.test @@ -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 <