add a --check=stutter-sensitive-example option

* spot/twaalgos/stutter.cc,
spot/twaalgos/stutter.hh (check_stutter_invariance): Add a
find_counterexamples argument.
* spot/twaalgos/hoa.cc: Output accepted-word and rejected-word examples.
* bin/common_aoutput.cc: Handle --check=stutter-sensitive-example.
* NEWS: Mention it.
* tests/core/stutter-tgba.test: Test it.
* doc/org/concepts.org, doc/org/hoa.org: Document accepted-word and
rejected-word named properties.
* bin/man/spot-x.x: Mention that --check=stutter-sensitive-example
ignores SPOT_STUTTER_CHECK.

NEWS

@@ -1,5 +1,19 @@
 New in spot 2.8.3.dev  (not yet released)
 
+  Command-line tools:
+
+  - When the --check=stutter-sensitive-example option is passed to
+    tools like ltl2tgba, autfilt, genaut, or ltldo, the produced
+    automata are checked for stutter-invariance (as in the
+    --check=stutter-invariant case), additionally a proof of
+    stutter-sensitiveness is provided as two stutter-equivalent words:
+    one accepted, and one rejected.  These sample words are printed in
+    the HOA output.
+
+    % ltl2tgba --check=stutter-sensitive-example Xa | grep word:
+    spot-accepted-word: "!a; cycle{a}"
+    spot-rejected-word: "!a; !a; cycle{a}"
+
   Library:
 
   - Historically, Spot only supports LTL with infinite semantics

bin/common_aoutput.cc

@@ -49,16 +49,22 @@ enum check_type
   {
     check_unambiguous = (1 << 0),
     check_stutter = (1 << 1),
-    check_strength = (1 << 2),
+    check_stutter_example = check_stutter | (1 << 2),
-    check_semi_determinism = (1 << 3),
+    check_strength = (1 << 3),
+    check_semi_determinism = (1 << 4),
     check_all = -1U,
   };
 static char const *const check_args[] =
   {
     "unambiguous",
+    /* Before we added --check=stutter-sensitive-example,
+       --check=stutter used to unambiguously refer to
+       stutter-invariant. */
+    "stutter",
     "stutter-invariant", "stuttering-invariant",
     "stutter-insensitive", "stuttering-insensitive",
     "stutter-sensitive", "stuttering-sensitive",
+    "stutter-sensitive-example", "stuttering-sensitive-example",
     "strength", "weak", "terminal",
     "semi-determinism", "semi-deterministic",
     "all",
@@ -67,9 +73,11 @@ static char const *const check_args[] =
 static check_type const check_types[] =
   {
     check_unambiguous,
+    check_stutter,
     check_stutter, check_stutter,
     check_stutter, check_stutter,
     check_stutter, check_stutter,
+    check_stutter_example, check_stutter_example,
     check_strength, check_strength, check_strength,
     check_semi_determinism, check_semi_determinism,
     check_all
@@ -149,8 +157,9 @@ static const argp_option options[] =
     { "format", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
     { "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL,
       "test for the additional property PROP and output the result "
-      "in the HOA format (implies -H).  PROP may be any prefix of "
+      "in the HOA format (implies -H).  PROP may be some prefix of "
-      "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
+      "'all' (default), 'unambiguous', 'stutter-invariant', "
+      "'stutter-sensitive-example', 'semi-determinism', or 'strength'.",
       0 },
     { nullptr, 0, nullptr, 0, nullptr, 0 }
   };
@@ -585,7 +594,9 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
   if (opt_check)
     {
       if (opt_check & check_stutter)
-        spot::check_stutter_invariance(aut, f);
+        spot::check_stutter_invariance(aut, f, false,
+                                       (opt_check & check_stutter_example)
+                                       == check_stutter_example);
       if (opt_check & check_unambiguous)
         spot::check_unambiguous(aut);
       if (opt_check & check_strength)

bin/man/spot-x.x

@@ -230,6 +230,9 @@ sl(a) x sl(!a), performed on-the-fly
 cl(a) x cl(!a)
 .RE
 .RE
+This variable is used by the \fB--check=stutter-invariance\fR and
+\fB--stutter-invariant\fR options, but it is ignored by
+\fB--check=stutter-sensitive-example\fR.
 
 .TP
 \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR

doc/org/concepts.org

@@ -1132,17 +1132,20 @@ Here is a list of named properties currently used inside Spot:
 
 | key name            | (pointed) value type           | description                                                                                                                                           |
 |---------------------+--------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------|
+| ~accepted-word~     | ~std::string~                  | a word accepted by the automaton                                                                                                                      |
 | ~automaton-name~    | ~std::string~                  | name for the automaton, for instance to display in the HOA format                                                                                     |
-| ~product-states~    | ~const spot::product_states~   | vector of pairs of states giving the left and right operands of each state in a product automaton                                                     |
+| ~degen-levels~      | ~std::vector<unsigned>~        | level associated to each state by the degeneralization algorithm                                                                                      |
-| ~original-states~   | ~std::vector<unsigned>~        | original state number before transformation (used by some algorithms like =degeneralize()=)                                                           |
-| ~original-clauses~  | ~std::vector<unsigned>~        | original DNF clause associated to each state in automata created by =dnf_to_streett()=                                                                |
-| ~state-names~       | ~std::vector<std::string>~     | vector naming each state of the automaton, for display purpose                                                                                        |
 | ~highlight-edges~   | ~std::map<unsigned, unsigned>~ | map of (edge number, color number) for highlighting the output                                                                                        |
 | ~highlight-states~  | ~std::map<unsigned, unsigned>~ | map of (state number, color number) for highlighting the output                                                                                       |
 | ~incomplete-states~ | ~std::set<unsigned>~           | set of states numbers that should be displayed as incomplete  (used internally by ~print_dot()~ when truncating large automata)                       |
-| ~degen-levels~      | ~std::vector<unsigned>~        | level associated to each state by the degeneralization algorithm                                                                                      |
+| ~original-clauses~  | ~std::vector<unsigned>~        | original DNF clause associated to each state in automata created by =dnf_to_streett()=                                                                |
+| ~original-states~   | ~std::vector<unsigned>~        | original state number before transformation (used by some algorithms like =degeneralize()=)                                                           |
+| ~product-states~    | ~const spot::product_states~   | vector of pairs of states giving the left and right operands of each state in a product automaton                                                     |
+| ~rejected-word~     | ~std::string~                  | a word rejected by the automaton                                                                                                                      |
 | ~simulated-states~  | ~std::vector<unsigned>~        | map states of the original automaton to states if the current automaton in the result of simulation-based reductions                                  |
+| ~state-names~       | ~std::vector<std::string>~     | vector naming each state of the automaton, for display purpose                                                                                        |
 | ~synthesis-outputs~ | ~bdd~                          | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) |
+
 Objects referenced via named properties are automatically destroyed
 when the automaton is destroyed, but this can be altered by passing a
 custom destructor as a third parameter to =twa::set_named_prop()=.

doc/org/hoa.org

@@ -967,6 +967,8 @@ terminal.
    :CUSTOM_ID: extensions
    :END:
 
+** Highlighting states and edges
+
 Spot supports two additional headers that are not part of the standard
 HOA format.  These are =spot.highlight.states= and
 =spot.highlight.edges=.  These are used to [[file:autfilt.org::#decoration][decorate states and edges]]
@@ -1105,6 +1107,68 @@ State: 2
 --END--
 #+END_SRC
 
+** Sample words
+
+When the =--check=stutter-sensitive-example= option is used, and when
+a stutter-sensitive automaton is output, two sample words are added to
+the HOA output as a proof that the automaton is stutter-sensitive.
+One of these words is accepted, the other is rejected, and the two are
+stutter-equivalent (i.e., they differ only by some stuttering).
+
+The headers are called =spot.accepted-word= and =spot.rejected-word=
+if HOA v1.1 is selected.  However since these are also useful to
+third-party tools, we also output them as =spot-accepted-word= and
+=spot-rejected-word= in HOA v1.
+
+#+BEGIN_SRC sh :wrap SRC hoa
+ltl2tgba --check=stutter-sensitive-example -H1 Xa; echo
+ltl2tgba --check=stutter-sensitive-example -H1.1 Xa
+#+END_SRC
+
+#+RESULTS:
+#+begin_SRC hoa
+HOA: v1
+name: "Xa"
+States: 3
+Start: 1
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-sensitive terminal
+spot-accepted-word: "!a; cycle{a}"
+spot-rejected-word: "!a; !a; cycle{a}"
+--BODY--
+State: 0
+[0] 2
+State: 1
+[t] 0
+State: 2 {0}
+[t] 2
+--END--
+
+HOA: v1.1
+name: "Xa"
+States: 3
+Start: 1
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: deterministic !stutter-invariant terminal
+spot.accepted-word: "!a; cycle{a}"
+spot.rejected-word: "!a; !a; cycle{a}"
+--BODY--
+State: 0
+[0] 2
+State: 1
+[t] 0
+State: 2 {0}
+[t] 2
+--END--
+#+end_SRC
+
+
 #+BEGIN_SRC sh :results silent :exports results
 rm -f stvstracc.hoa sba.hoa stvstrlab.hoa decorate.hoa
 #+END_SRC

spot/twaalgos/hoa.cc

@@ -599,6 +599,16 @@ namespace spot
             os << nl;
           }
       }
+    if (auto word = aut->get_named_prop<std::string>("accepted-word"))
+      {
+        os << (v1_1 ? "spot." : "spot-") << "accepted-word: \"";
+        escape_str(os, *word) << '"' << nl;
+      }
+    if (auto word = aut->get_named_prop<std::string>("rejected-word"))
+      {
+        os << (v1_1 ? "spot." : "spot-") << "rejected-word: \"";
+        escape_str(os, *word) << '"' << nl;
+      }
 
     // If we want to output implicit labels, we have to
     // fill a vector with all destinations in order.

spot/twaalgos/stutter.cc

@@ -31,6 +31,7 @@
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/word.hh>
 #include <spot/twa/twaproduct.hh>
 #include <spot/twa/bddprint.hh>
 #include <deque>
@@ -664,10 +665,11 @@ namespace spot
 
   trival
   check_stutter_invariance(twa_graph_ptr aut, formula f,
-                           bool do_not_determinize)
+                           bool do_not_determinize,
+                           bool find_counterexamples)
   {
     trival is_stut = aut->prop_stutter_invariant();
-    if (is_stut.is_known())
+    if (!find_counterexamples && is_stut.is_known())
       return is_stut.is_true();
 
     twa_graph_ptr neg = nullptr;
@@ -676,7 +678,45 @@ namespace spot
     else if (!is_deterministic(aut) && do_not_determinize)
       return trival::maybe();
 
-    return is_stutter_invariant(aut, std::move(neg));
+    if (!find_counterexamples)
+      return is_stutter_invariant(aut, std::move(neg));
+
+    // Procedure that may find a counterexample.
+
+    if (!neg)
+      neg = complement(aut);
+
+    auto aword = product(closure(aut), closure(neg))->accepting_word();
+    if (!aword)
+      {
+        aut->prop_stutter_invariant(true);
+        return true;
+      }
+    aword->simplify();
+    aword->use_all_aps(aut->ap_vars());
+    auto aaut = aword->as_automaton();
+    twa_word_ptr rword;
+    if (aaut->intersects(aut))
+      {
+        rword = sl2(aaut)->intersecting_word(neg);
+        rword->simplify();
+      }
+    else
+      {
+        rword = aword;
+        aword = sl2(aaut)->intersecting_word(neg);
+        aword->simplify();
+      }
+    std::ostringstream os;
+    os << *aword;
+    aut->set_named_prop<std::string>("accepted-word",
+                                     new std::string(os.str()));
+    os.str("");
+    os << *rword;
+    aut->set_named_prop<std::string>("rejected-word",
+                                     new std::string(os.str()));
+    aut->prop_stutter_invariant(false);
+    return false;
   }
 
   std::vector<bool>

spot/twaalgos/stutter.hh

@@ -122,12 +122,19 @@ namespace spot
   /// If no complemented automaton could be constructed, the
   /// the result will be returned as trival::maybe().
   ///
+  /// If \a find_counterexamples is set and the automaton is found to
+  /// be stutter-sensitive, then two named properties named
+  /// "accepted-word" and "rejected-word" will be added to the
+  /// automaton.  Those sample words will be stutter-equivalent, and
+  /// serve as a proof that the property is stutter-sensitive.
+  ///
   /// This variant of is_stutter_invariant() is used for the
   /// --check=stutter option of command-line tools.
   SPOT_API trival
   check_stutter_invariance(twa_graph_ptr aut_f,
                            formula f = nullptr,
-                           bool do_not_determinize = false);
+                           bool do_not_determinize = false,
+                           bool find_counterexamples = false);
 
 
   ///@{

tests/core/stutter-tgba.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014-2018 Laboratoire de Recherche et
+# Copyright (C) 2014-2019 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -137,3 +137,23 @@ for i in 1 2 3 4 5 6 7 8; do
     test 0 = `SPOT_STUTTER_CHECK=$i \
               autfilt pirogov --is-stutter-invariant -c` || exit 1
 done
+
+
+ltl2tgba Xa --check=stutter-sensitive-example > out
+grep ' stutter-sensitive' out
+grep '^spot-accepted-word: "' out
+grep '^spot-rejected-word: "' out
+
+ltl2tgba 'X"a b"' --check=stutter-sensitive-example -H1.1 > out
+grep ' !stutter-invariant' out
+grep '^spot\.accepted-word: ".*\\\"' out
+grep '^spot\.rejected-word: ".*\\\"' out
+# Make sur we can parse it ok.
+autfilt -q out
+
+ltl2tgba Ga --check=stutter-sensitive-example > out
+grep ' stutter-invariant' out
+grep -q '^spot.accepted-word: "' out && exit 1
+grep -q '^spot.rejected-word: "' out && exit 1
+
+: