Assertion failure followed by a NullPointerException (TTT learner)

[Jaxan]

I was using a setup with the TTT learner using the EXPONENTIAL_BWD counter example analyzer (although I get the same crashes with the other analyzers). As equivalence oracle I have some randomized tester. The assertion is not triggered in all runs, so it does depend on the specific counter example.

The assertion failed is this one (AcexAnalysisAlgorithms.java:78)

Here is the stack trace:

  java.lang.Thread.State: RUNNABLE
      at de.learnlib.acex.analyzers.AcexAnalysisAlgorithms.exponentialSearchBwd(AcexAnalysisAlgorithms.java:78)
      at de.learnlib.acex.analyzers.AcexAnalyzers$5.analyzeAbstractCounterexample(AcexAnalyzers.java:83)
      at de.learnlib.acex.AcexAnalyzer.analyzeAbstractCounterexample(AcexAnalyzer.java:28)
      at de.learnlib.algorithms.ttt.base.BaseTTTLearner.splitState(BaseTTTLearner.java:215)
      at de.learnlib.algorithms.ttt.base.BaseTTTLearner.refineHypothesisSingle(BaseTTTLearner.java:198)
      at de.learnlib.algorithms.ttt.base.BaseTTTLearner.refineHypothesis(BaseTTTLearner.java:143)
      at de.learnlib.algorithms.ttt.mealy.TTTLearnerMealy.refineHypothesis(TTTLearnerMealy.java:124)
      at learnlib.LStarMain.innerMain(LStarMain.java:245)
      at learnlib.LStarMain.main(LStarMain.java:98)

A couple of notes (going deeper in the stack):

• On TTTLearnerMealy.java:124 the counter example is not shortened (so the original ce was passed along)
• It did do at least one refinement as we are at the while loop in BaseTTTLearner.java:143
• In BaseTTTLearner.java:198 we see that the same counter example is still a counter example
• In AcexAnalysisAlgorithms.java:78 the assertion failed. I did experiment a bit here. If one keeps low==0 and varies high the return value of testEffects will be first true for some time, then switch to false for some time and then go back to true again (so the assertion fails for extreme values for low and high).

If one now continues stepping though the code starting at splitState (BaseTTTLearner.java:215) it will crash, since breakpoint==0 and the asserts on lines 216, 227 also fails. Then we dive into the function splitState (BaseTTTLearner.java:875) which crashes on line 883 since dtNode is null. This NullPointerException also happens when I use different counter example analyzers.

I am not sure this project is still maintained. In that case I can try to fix it myself. But I need some more guidance. In particular I have no idea what testEffects actually means (it returns a boolean which is also not very informative).

Btw, Thanks again for the great library!

[Jaxan]

Ok. Here is my hypothesis of why there is this crash: The original counter example could not be shortened, so it is used to refine (which does not crash). Then, we repeat refinement with the same (unshortened) counter example, but note that now it might be possible to shorten it, since the hypothesis changed. And for the counter example analyzers (except the linear ones), it should be shortened to work correctly.

Do you think this could be the cause of the crash?

[fhowar]

Hi,

can you produce a minimal example and share some code so we can try to reproduce and debug locally?

Also, do you have a hunch what the source of non-determinism is?

Thanks

Falk

[Jaxan]

Sorry I read this only now.

My equivalence oracle is randomised. There is no non-determinism besides that.
I will make a nice example tomorrow, without the randomisation.

[Jaxan]

Hi Falk!

I created a gist with the java code and a dot file to reproduce the crash: here. It should be self contained (except for learnlib of course), so I hope you'll get it crashing easily. Let me know if you can't get it to work.

The current example only crashes with the specified Acex analyzer. But it does fail the assertion with other Aces analyzers as well.

All the best,
Joshua

[misberner]

Hi Joshua,

I think you have correctly described the issue - the problem is the repeated refinement using the given counterexample (the first iteration always works because all the output inconsistencies derived from the discrimination tree have the property that they mismatch on the last symbol only, if the initial counterexample was shortened).

The fix should involve only changing two lines:
In https://github.com/LearnLib/learnlib/blob/develop/algorithms/ttt/src/main/java/de/learnlib/algorithms/ttt/mealy/TTTLearnerMealy.java#L121 , rename this method to refineHypothesisSingle, and also change the super method invocation in l. 125 to refineHypothesisSingle .

Could you try this and let us know if this works (and maybe send a pull request)? I can't test it myself right now.

[Jaxan]

The fix you proposed indeed works. See #39

What is the exact precondition for the counter example analyzers? I don't want to keep that part undocumented, as it was not easy for me to figure out what was wrong.

[aschieweck]

I am closing this issue, because the Pull Request #39 was already successfully merged by @misberner.

@Jaxan: Please consider to open a new issue regarding your follow up question. We are aware that the documentation of LearnLib has to improve. Therefore any hints on the most popular questions are very welcome.