21 Nov
2019
21 Nov
'19
12:22 p.m.
On Wed, Nov 20, 2019 at 12:54 PM Victor Khomenko
<victor.khomenko(a)newcastle.ac.uk> wrote:
Hi Alexandre,
Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be
possible to print a warning with diagnostics, like the online tool does? Something like:
Warning: The property is stutter-sensitive - the following words are a proof, as they
differ only by some stuttering:
Accepted word: a & b; a & b; cycle{!a & !b}
Rejected word: a & b; cycle{!a & !b}
Motivation:
* by passing the option --check=stutter-invariant the user tells the tool that
stutter-invariance is important for them, hence a warning/diagnostics is desirable if the
check fails (this warning does not have to be printed if this option is not passed)
* it's not easy to get these traces from the final automaton - my understanding is
that some potentially costly operations are required, which are performed during the check
anyway
* the current way of getting this diagnostics (python + libraries; maybe there is a
better way I don't know about?) creates many dependencies, thus making it difficult to
integrate this functionality into toolchains - ideally one would want just a single
executable ltl2tgba
* my (perhaps naive) understanding is that this is not difficult to implement and does
not incur much extra run-time as the check has to be performed anyway
Hi Victor,
A couple of issues:
1. The stutter-invariance check does not need to compute those two
words, getting them requires extra work.
2. The stutter-invariance check currently obey the SPOT_STUTTER_CHECK
environment variable (see the spot-x(7) man page) to select the
algorithm to use, but getting those words cannot be done with any of
the offered algorithms.
3. The --check=stutter-invariant option just asks Spot to label any
automaton it produces with the "stutter-invariant" or
"stutter-sensitive" properties (or "!stutter-invariant" with -H1.1),
it does not imply that you expect the output to be stutter-invariant:
you may just want that information to turn on or off some options
automatically. So I'm quite reluctant to implement such a warning,
especially since that does not play well when the tools are used in
pipelines.
4. If you want to integrate this into a toolchain, scanning the output
for warning is probably not very robust.
So because of #1-#2 I'd like the user to request those sample words
explicitly, and because of #3-#4 I'd like to find a way to provide
those words in a way that fit better with the tool suite. Currently
the only warnings we have are for timeouts when running other tools,
everything else is an error.
So maybe we can turn this warning into an error with an option like
--check=expect-stutter-invariant, and in this case I'm fine with an
error and a diagnostic (and #4 is your problem). That's the simplest
option to implement, but it's not very "toolable"
Another possibility is to add an option
--check=stutter-invariant-counterexample that would insert lines like
spot.accepted-word: "a & b; a & b; cycle{!a & !b}"
spot.rejected-word: "a & b; cycle{!a & !b}"
in the -H1.1 output [*]. Would that work for you?
Or maybe it should be --check=sample-words, which would add those
lines even if stutter-invariance checks are not run, with the
convention, like in the online tool, that when
--check=stutter-invariant,sample-words is used and the automaton
stutter-sensitive, the sample words will be stutter-equivalent.
Another possibility, not incompatible with the previous suggestions,
is to teach the --format=%w option about how to display rejecting
words and how to inherit those words from the stutter invariance
checks if any. That way one could choose how those words are
presented, even in a context where -H1.1 cannot be used [*]. E.g.,
with
ltl2tgba formula --check=stutter-invariant --format='/*
accepting word: %w
rejecting word: %[r]w
*/
%h'
and get those two words and the formula at once. (Currently %[r]w
works like %w a display any accepting word.)
[*] FWIW, option -H1.1 is supposed to enable version v1.1 of the HOA
format, but that version has never been published, exists only on a
branch of the github repository for the format, and it will probably
be renamed v2. The implementation in Spot is not correct with respect
to the redefinition of the Streett acceptance condition. So it's fine
to use -H1.1 to pass automata between tools based on Spot, but it's
probably not a good idea to use that with third-party tools yet.
What do you think?
None of that should be very difficult to implement, but I will not
have the time to do it before December, and it's unlikely that it will
be released before next year.
BTW, if you prefer, you can also replace the Python dependency by a
web dependency :-) Just URLencode your LTL formula and do
% curl -s --request GET
https://spot.lrde.epita.fr/api/study/X%21a%26GF%28a%7Cb%29 | json_pp
{
"acc_word" : "a & !b; !a & !b; cycle{!a & b}",
"mp_class" : "R",
"mp_class_text" : "a recurrence property",
"mp_hierarchy_svg" : "[...]",
"safety_liveness" : "none",
"stutter_invariant" : false
}
probably only good as a short-term hack,