confusing diagnostic

On Tue, May 21, 2019 at 5:47 PM Victor Khomenko wrote:

Hi Alexandre,

I tried the formula {(a:b) | (a;b)}|->Gc in the online tool, and it correctly tells that it's stutter-sensitive, with

    Accepted word:  a & !b & c; a & !b & c; cycle{b & !c}
    Rejected word:  a & !b; cycle{b & !c}

Then it claims that the words differ only by some stuttering, which is not quite true. I think one should add & c to the first letter of the rejected word.

Regards, Victor.

This is really an issue for spot/spot-web-app> but we should fix it in the explain_stut() function of stutter-inv.ipynb as well. We just need to make sure that each letter of word uses all atomic propositions (the missing ones can be set to positive or negative, it does not matter).