Potential bug in counterexample handling
Closed this issue · 3 comments
In class de.learnlib.counterexamples.LocalSuffixFinders
line 204:
int low = asTransformer.isAccessSequence(prefix) ? prefixLen : prefixLen-1;
Why do you use prefixLen-1? Shouldn't this rather be 0?
This line was not intended as a default mechanism (if the prefix of the counterexample is not an access sequence or a one-letter-extension of an access sequence, the result is not catastrophic anyway - the worst thing to happen is that a CE is not recognized as such).
The rationale behind this was the following: queries are separated into a prefix and a suffix. The prefix can be regarded as a word that leads to some point of interested (state in the SUL/hypothesis), and the suffix as the part which exposes interesting (i.e., differing) behavior. From the perspective of classical automata learning, using ua (where u is an access sequence and a an alphabet symbol) as a prefix does make sense, since the output corresponding to a can never be wrong in the hypothesis (assuming that for all states in the hypothesis all outputs are inferred correctly). This might be an invalid assumption in certain cases (think, e.g., of AAR), but not in the classical case.
The check was hence introduced to deal with an input which is in fact correct, but where the characteristics of the counterexample handling mechanism come with the need to start with a real access sequence anyway. I can however change this if this is confusing or a more robust behavior is desired.
We could make this of counterexamples split into prefix and suffix of a convention (one can always set only set suffix). The downside would be that it would probably hard to discover if somebody violates it. Can we introduce a helper method that generates such counterexamples using an access sequence transformer without using queries?
A second aspect is the naming. I think we should think about this in general. If we name something Rivest it should do exactly what is described by Rivest. I like the optimization. But we should give it a name, evaluate it, and report its effect in some form.
Well, this is a rather old issue and the line in question seems to be already gone from the source code. So I think it is finally time to close this issue.