TTT: Index 1 out of bounds in first counter example #140
Comments
|
Hi,
Yes. Queries consist of a prefix (e.g., an access sequence to a state) and a suffix (e.g., the future behavior of a reached state). Queries should be answered with the system's response to the suffix only. In your transformation, you construct lists with the full instead. Your actual oracle needs to be adjusted accordingly.
It depends on what the learner is currently doing. For TTT, there is a distinct counterexample analysis phase where, for example, binary search is used to pinpoint a violating transition. This search is inherently sequential, so you often see query batches of size 1. Once the hypothesis is refined, the open transitions need to be closed. This typically results in multiple simultaneous queries and the discrimination tree-based learners should batch them as well (if they consistently don't, feel free to raise another issue). However, this scales with the number of input symbols, so in your example ( In contrast, the vanilla L* algorithm just adds all prefixes of the counterexample as rows to the observation table. Together with potentially multiple columns, this often results in batches of some quadratic size. |
|
Hello, thank you for the quick reply and the clarification! Applying the proposed snippet indeed fixes the issue, I ran into. I was not aware about the requirement to provide the suffix only instead of the entire word. Regarding the batching, I tried to modify the alphabet to get more queries, by adding all letters from A to Z. - final static String[] INPUT_ALPHABET = { "A" };
+ final static String[] INPUT_ALPHABET = { "A", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o",
+ "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z" };
However, it seems that one query per batch is executed nonetheless: The result is consistent with my actual oracle. Thank you again for the help! |
|
Oh wow, this is actually an "issue" with the existing implementation. Specifically for the Mealy learner, creating new transitions results in an extra query to determine the transition output. This is called in a simple Furthermore, finalizing splitters also involves posing singleton queries. It seems like only the sifting of transitions properly utilizes batching. (You'll see it with discrimination trees with height > 1, e.g., if your hypothesis has more states). From the looks of it, it should be possible to batch these operations as they have no sequential data-dependencies between them. I'll try to look into it in the upcoming days. |
Describe the bug
Hello,
I am trying to run the TTT algorithm on
learnlib 0.17and run into some issues when setting it up with a "TraceLevelOracle", i.e. I have no SUL as such, but only the Oracle that provides an Output Trace for a corresponding input trace.My example is fairly short, and oriented at the examples that were given in
examples/. Regarding the "TraceLevelOracle", I followed the advice from #130.To Reproduce
I have the following
main:And my TraceLevelOracle looks as follows:
The
processQueriesperforms a transformation to nestedArrayLists, as they are usually passed to another program, where the batch is performed and retrieved. To simplify, I used a simple loop and anifto abstract this behavior.The output I get is the following:
Oddly enough, using the
ExtensibleLStarMealyLearner yields an execution which runs in an infinite loop.Is there some detail I overlooked with the abstraction? I would expect both algorithms to provide as output the two state mealy machine
[0] - (Sigma) -> [1] (Loop (Sigma)).Finally I have one question about the implementation of batching for TTT and for LStarMealy: When executing
ExtensibleLStarMealywith a larger alphabet, I get batch sizes, that are greater then 1, while with TTT I don't. Is it correct, that TTT always performs sequential queries to the oracle and does not batch them?Thank you for the great project and the work you put into it!
The text was updated successfully, but these errors were encountered: