From 44df3c0837ff8e15177879c2f79e9788b7b35982 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 3 Dec 2019 17:42:32 +0100 Subject: [PATCH] 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 | 14 ++++++++ bin/common_aoutput.cc | 21 +++++++++--- bin/man/spot-x.x | 3 ++ doc/org/concepts.org | 13 +++++--- doc/org/hoa.org | 64 ++++++++++++++++++++++++++++++++++++ spot/twaalgos/hoa.cc | 10 ++++++ spot/twaalgos/stutter.cc | 46 ++++++++++++++++++++++++-- spot/twaalgos/stutter.hh | 9 ++++- tests/core/stutter-tgba.test | 22 ++++++++++++- 9 files changed, 187 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index 0255459a9..432525b7d 100644 --- a/NEWS +++ b/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 diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 8ec651fbc..8b02c0477 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -49,16 +49,22 @@ enum check_type { check_unambiguous = (1 << 0), check_stutter = (1 << 1), - check_strength = (1 << 2), - check_semi_determinism = (1 << 3), + check_stutter_example = check_stutter | (1 << 2), + 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 " - "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.", + "in the HOA format (implies -H). PROP may be some prefix of " + "'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) diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index a243b34b1..69d8e35d9 100644 --- a/bin/man/spot-x.x +++ b/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 diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 05cc91863..3578d90f4 100644 --- a/doc/org/concepts.org +++ b/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 | -| ~original-states~ | ~std::vector~ | original state number before transformation (used by some algorithms like =degeneralize()=) | -| ~original-clauses~ | ~std::vector~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= | -| ~state-names~ | ~std::vector~ | vector naming each state of the automaton, for display purpose | +| ~degen-levels~ | ~std::vector~ | level associated to each state by the degeneralization algorithm | | ~highlight-edges~ | ~std::map~ | map of (edge number, color number) for highlighting the output | | ~highlight-states~ | ~std::map~ | map of (state number, color number) for highlighting the output | | ~incomplete-states~ | ~std::set~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) | -| ~degen-levels~ | ~std::vector~ | level associated to each state by the degeneralization algorithm | +| ~original-clauses~ | ~std::vector~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= | +| ~original-states~ | ~std::vector~ | 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~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | +| ~state-names~ | ~std::vector~ | 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()=. diff --git a/doc/org/hoa.org b/doc/org/hoa.org index ed09fa990..fcee71c10 100644 --- a/doc/org/hoa.org +++ b/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 diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 32a0eb019..320053eb5 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -599,6 +599,16 @@ namespace spot os << nl; } } + if (auto word = aut->get_named_prop("accepted-word")) + { + os << (v1_1 ? "spot." : "spot-") << "accepted-word: \""; + escape_str(os, *word) << '"' << nl; + } + if (auto word = aut->get_named_prop("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. diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 0a58294c3..b0625d2d7 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -31,6 +31,7 @@ #include #include #include +#include #include #include #include @@ -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("accepted-word", + new std::string(os.str())); + os.str(""); + os << *rword; + aut->set_named_prop("rejected-word", + new std::string(os.str())); + aut->prop_stutter_invariant(false); + return false; } std::vector diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index 47faceafb..908f47e3c 100644 --- a/spot/twaalgos/stutter.hh +++ b/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); ///@{ diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test index fd3d26f1a..ecc11b56d 100755 --- a/tests/core/stutter-tgba.test +++ b/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 + +: