Problem with using Ralib to extract the behavioral model with inequality theory

[Alim9100]

Hello, I hope you are doing well.

I recently attempted to use the main branch of the Ralib for extracting the behavioral model of a binary search tree data structure, treating it as a System Under Learning (SUL). Unfortunately, I encountered an unresolved error during the process.
The error manifested while the tool was calculating the initial branching for a prefix and a suffix symbol. Specifically, an exception of type "IllegalStateException" was thrown at line 290 in the class "MultiTheoryTreeOracle".
The error message indicated: "Guard instantiated using a dvi that was already used to instantiate a prior guard," suggesting that the teacher may be generating duplicate fresh values.

I have attached the source code of the SUL, the configuration file, the execution log file,
and the stack trace for the error. Could you please assist me in understanding what went
wrong and how to resolve it?

Thank for your attention.
MethodConfig.txt
Config.txt
Driver.txt
BinaryTree.txt.txt
log.txt

[fhowar]

@pfg666 @FredrikTaquist could you take a look? It is a problem with initial branching.

[pfg666]

Hi Alim,

Thanks for reporting. I checked your code and was able to reproduce the problem. Based on my initial investigation, I suspect the cause is a bug in the inequality theory implementation ( de.learnlib.ralib.theory.inequality.InequalityTheoryWithEq ).

@FredrikTaquist , here is a print-out of an SDT the implementation produces::

[[r1, r2]-+
        []-(s1!=r1)
         |    [Leaf-]
         +-(s1!=r2)
         |    [Leaf-]
         +-(s1=r2)
         |    [Leaf+]
         +-(s1=r1)
              [Leaf+]
]

I would have expected four branches, one of which with guard (s1!=r1 && s1!=r2).

[pfg666]

A follow-up, I discussed with @FredrikTaquist . Our plan is to refactor the theories and with that, fix issues including the one you reported. Unfortunately, this may take time (late April/May). If you need to proceed with this project, what you may consider is checking the succ-stable branch. This contains a prototype version of RALib that was adapted for learning TCP stacks. Since the tree oracle implementations were altered significantly in that version, I think there is a good chance this bug is not present.