diff --git a/src/tests/stutter-tgba.test b/src/tests/stutter-tgba.test index dd3f69d03..63430890c 100755 --- a/src/tests/stutter-tgba.test +++ b/src/tests/stutter-tgba.test @@ -70,6 +70,8 @@ State: 2 --END-- EOF +diff output expected + run 0 $ltl2tgba -H 'F(a & X(!a & b))' > input grep stutter-invariant input && exit 1 run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2 @@ -77,4 +79,9 @@ grep stutter-invariant input.2 run 0 $autfilt --check=stutter input > input.2 grep stutter-invariant input.2 -diff output expected +run 0 $ltl2tgba -H 'F(a & X(a & b))' > input +grep stutter-invariant input && exit 1 +run 0 $ltl2tgba --check=stutter 'F(a & X(a & b))' > input.2 +grep stutter-sensitive input.2 +run 0 $autfilt --check=stutter input > input.2 +grep stutter-sensitive input.2 diff --git a/src/twa/twa.hh b/src/twa/twa.hh index 54d752fd6..bb50212ec 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -715,7 +715,8 @@ namespace spot bool state_based_acc:1; // State-based acceptance. bool inherently_weak:1; // Weak automaton. bool deterministic:1; // Deterministic automaton. - bool stutter_inv:1; // Stutter invariant + bool stutter_invariant:1; // Stutter invariant language. + bool stutter_sensitive:1; // Stutter sensitive language. }; union { @@ -798,12 +799,22 @@ namespace spot bool is_stutter_invariant() const { - return is.stutter_inv; + return is.stutter_invariant; + } + + bool is_stutter_sensitive() const + { + return is.stutter_sensitive; } void prop_stutter_invariant(bool val = true) { - is.stutter_inv = val; + is.stutter_invariant = val; + } + + void prop_stutter_sensitive(bool val = true) + { + is.stutter_sensitive = val; } struct prop_set @@ -830,7 +841,10 @@ namespace spot if (p.deterministic) prop_deterministic(other->is_deterministic()); if (p.stutter_inv) - prop_stutter_invariant(other->is_stutter_invariant()); + { + prop_stutter_invariant(other->is_stutter_invariant()); + prop_stutter_sensitive(other->is_stutter_sensitive()); + } } void prop_keep(prop_set p) @@ -841,6 +855,11 @@ namespace spot prop_inherently_weak(false); if (!p.deterministic) prop_deterministic(false); + if (!p.stutter_inv) + { + prop_stutter_invariant(false); + prop_stutter_sensitive(false); + } } }; diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 1c9c11dd7..7068d0804 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -327,8 +327,11 @@ namespace spot prop(" complete"); if (md.is_deterministic) prop(" deterministic"); + assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive())); if (aut->is_stutter_invariant()) prop(" stutter-invariant"); + if (aut->is_stutter_sensitive()) + prop(" stutter-sensitive"); if (aut->is_inherently_weak()) prop(" inherently-weak"); os << nl; diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 098108538..985f55196 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -667,8 +667,8 @@ namespace spot is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), std::move(neg), get_all_ap(aut)); - if (is_stut) - aut->prop_stutter_invariant(is_stut); + aut->prop_stutter_invariant(is_stut); + aut->prop_stutter_sensitive(!is_stut); return is_stut; } }