On Wed, Nov 20, 2019 at 12:54 PM Victor Khomenko victor.khomenko@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,