Bug in WMethod Oracle Implementation

[icezyclon]

Problem: The WMethodOracle is not implemented correctly. It produces too few test sequences and does not find a counterexample even though its maxmimum state variable is high enough.
Please see and try the tests included in this PR.

Context: The WMethodOracle uses combinations from itertools for extending the middle of its testing set. However, these sequences are much too short to actually cover the entire state space given by the maximum state variable.
I believe that the author though the second argument of combinations is the length of the resulting sequences, when in reality it is the number of buckets to split the alphabet into. See https://docs.python.org/3/library/itertools.html#itertools.combinations

Problem 2: Also, on an unrelated note, I saw that the calculation for the characterization set does not work for Moore Machines in general. Calling compute_characterization_set on the Moore Machine generated by generate_hypothesis in the newly added test will result in the algorithm claiming that the machine is non-canonical, even though it isn't.

[mtappler]

@problem 2:
When working with Moore machines, the characterization set currently needs to be initialized such that it includes the empty sequence; see the documentation of the parameter char_set_init (which contains a typo that I just noticed).
If have not done so, could you please try initializing the characterization set like that to check whether this is the reason for the computation failing? I.e., please try calling the compute_characterization_set with char_set_init = [()].

The find_cex method of WMethodEqOracle should do that too, which currently is not the case, so this should be fixed.

[icezyclon]

@problem 2: When working with Moore machines, the characterization set currently needs to be initialized such that it includes the empty sequence; see the documentation of the parameter char_set_init (which contains a typo that I just noticed). If have not done so, could you please try initializing the characterization set like that to check whether this is the reason for the computation failing? I.e., please try calling the compute_characterization_set with char_set_init = [()].

The find_cex method of WMethodEqOracle should do that too, which currently is not the case, so this should be fixed.

I tried this already and calling mm.compute_characterization_set([tuple()]) does not work with the example generated by generate_hypothesis, same as when adding the input alphabet in addition to the empty sequence. That is why I mentioned this issue again.

[emuskardin]

I will try to solve the issue tomorrow.
I left this bug here on purpose, just to check if you are being careful with your implementation 😹
Thanks for the addition of the test file :)

(I merged the test-case and will update you once it is solved)