LearnLib / learnlib

A free, open-source Java library for automata learning algorithms
https://learnlib.de
Apache License 2.0
206 stars 53 forks source link

Incompatible acceptances: FALSE vs TRUE #76

Closed z11panyan closed 3 years ago

z11panyan commented 3 years ago

When I took the random DFA as the experimental object, the error "Incompatible acceptances: FALSE vs TRUE" occurred in IncrementalDFADAGBuilder.java. By debugging the class IncrementalDFADAGBuilder, the execution result of the statement , "sig.successors.array[idx] = succ" (in the function updateSignature ), puzzles me. The type of the parameter "succ" is State, and it changed after the executing of the above statement. As shown in the following figure:

捕获 捕获1

Thus, the longer word will lead to the error "Incompatible acceptances: FALSE vs TRUE".

mtf90 commented 3 years ago

Is there a way for you to provide a minimal working example so that we can reproduce the error?

Otherwise, there was a bug in the DAG-based caches that has been fixed in the current development version of AutomataLib. You could also try to use the current development version of LearnLib and see, if the error still exists. (You might want to check the AutomataLib and LearnLib changelogs before, to see if you are affected by other changes as well).

z11panyan commented 3 years ago

error3.dfa.gz This is the error dfa. The format is consistent with the example of the Paper "The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning".

mtf90 commented 3 years ago

Which equivalence and learning algorithm did you use? Alternatively, you can also post the complete .java file of your learning setup (which preferably provokes the above error when executing its main method).

z11panyan commented 3 years ago

dfa.tar.gz

This is the added files and the path is "learnlib/algorithms/active/ttt/src/test/java/de/learnlib/algorithms/ttt/dfa".

捕获2

This is the catalog of the added files. The dfa file is in "learnlib/algorithms/active/ttt/target/test-classes". In addition, the equivalence algorithm is wp-method, and the learning algorithm is LStar. What else can I offer?

mtf90 commented 3 years ago

An intermediate update: I was able to reproduce the issue and it actually looks like a bug in the DFADAGBuilder. But I need some more time to actually piece together what goes wrong here. Do you mind if I use (some of) your code to create a testcase?

For now, you can use DFACaches.createTreeCache as an alternative. This type of cache will require a little bit more system memory, but it will give you the same query performance and you should be able to successfull execute your experiments.

z11panyan commented 3 years ago

Of course not, as long as it is helpful for you. And I will try to use DFACaches.createTreeCache as an alternative.

Another issue is the queryCache. The core code of the function processQueries is as follows. ` final Collection<ProxyQuery> unanswered = queryCache(queries);

delegate.processQueries(unanswered);

updateCache(unanswered); ` I think there is an issue. If there are two identical unanswered queries in the Collection "queries", the number of unique query will be increased by 2. Could you analyse this issue?

mtf90 commented 3 years ago

Another issue is the queryCache. The core code of the function processQueries is as follows. ... I think there is an issue. If there are two identical unanswered queries in the Collection "queries", the number of unique query will be increased by 2. Could you analyse this issue?

You are correct. However, this is currently by design because in order to answer queries we need to call the answer method on every query object. Thus, we cannot "merge" duplicate queries within a single batch without copying (and aggregating) every query. But to be fair, we do exactly that (copying) in the Mealy case, because of the even greater optimization potential of prefix-closedness. It's a valid point to think about for the DFA case as well.

Do you have encountered any specific situation where this is a problem? I think mostly table-based algorithms (L* variants) may be affected by this when using prefix-closed row labels and suffix-closed discriminators (columns). Most tree-based learners use much smaller batches when classifying states and the queries withing each batch should be distinct.

z11panyan commented 3 years ago

Through experiments, table-based algorithms are affected by this issue, but it has little effect.

mtf90 commented 3 years ago

I finally managed to find the culprit and provide a fix for the issue. Looking at the diff, the devil is always in the details :D.

Are you fine with using a development version of LearnLib (respectively AutomataLib) or would you prefer a separate bugfix release?

Also, regarding you remark on handling in-batch duplicates, I created a separate issue #78.

z11panyan commented 3 years ago

Thanks for maintaining this great library! For me, a development version is fine.