Question about EQ

[Teck Ping Khoo]

Hi everyone

Consider the following code:

DFAEquivalenceOracle<Character> eqOracle = new DFAWpMethodEQOracle<>(mqOracle, 5);

My understanding is that we are creating an EQ oracle using the Wp method. The Wp method is from test case generation theory. When applied here, it means that our active automata learning algorithm have a hypothesis automata, and we are trying to check it for equivalence with an ideal SUL automata (which does not exist). The Wp method will try to find a trace which is in our hypothesis but not in the SUL automata, up to a threshold of 5. If it cannot be found, Wp will conclude that the two automata are equivalent. 

Is my understanding correct? Exactly what does the threshold of 5 mean? I used the code above in my project and got a rather large model with 26 states. 

Regards

Teck Ping

[Markus Frohme]

The W(p)MethodEQOracles use the current hypothesis to compute test cases (based on the W(p)Method) and compare the outputs of the hypothesis and the SUL for these tests. If the output differs, it returns the current testword as a counterexample, if all tests match, it signals equivalence.

The problem is, that in early phases of learning your hypothesis is relatively small so the test cases will not be very exhaustive and likely miss paths in your SUL. This is where the parameter comes in. The classic W(p)Method generates tests from the cartesian product of <transition cover> x <state characterization> sets. The oracles generate tests from the cartesian product of <transition cover> x <middle part> x <state characterization>, where the "middle part" set contains all possible words up to the length of your provided parameter. You can think of it as an upper bound for a lookahead if you suspect the SUL to have additional states (I think this approach is even discussed in the original WpMethod paper).

So you don't want to set this value too low, to not miss any paths in your SUL, but also not too high, as the number of test cases grow exponentially in this parameter.

The next release (or current development version, if you feel comfortable with them) changes this to two parameters (expectedSize and lookahead) to allow for dynamically adapting the lookahead based on an expected size of the hypothesis. See [0] for details.


[0] - https://github.com/LearnLib/automatalib/issues/32

On Fri, Sep 20, 2019 at 02:41:15AM -0700, Teck Ping Khoo wrote:
> Hi everyone
>
> Consider the following code:
>
> DFAEquivalenceOracle<Character> eqOracle = new
> DFAWpMethodEQOracle<>(mqOracle, 5);
>
> My understanding is that we are creating an EQ oracle using the Wp method.
> The Wp method is from test case generation theory. When applied here, it
> means that our active automata learning algorithm have a hypothesis

> automata, and we are trying to check it for equivalence with an *ideal *SUL