Which branch is usable and error free?

[Alim9100]

Hi, I want to use this tool. in the previous one in bitbucket, I had problem with generating models. The random walk equivalence oracle could not generate counterexample correctly. For example when I learned the model of queue with the capacity of 12, it only generated a model for queue with 2 capacity. Is this bug fixed in this version?

In addition, the inequality oracle throws exception while it tries to generate fresh value. the Z3 can not generate value for inequality theory and throws exception.

[fhowar]

The main branch is the current development version, which should be stable and correct.

To your other questions:

A random walk may not find a counterexample. In a black-box scenario, this is expected. Can you provide more details on the configuration you used?

For the Z3 bug: please try the main branch of this repository. If the bug still occurs, please provide more information (experiment setup, stack trace, etc.)

[Alim9100]

model.txt Thank you for your response. I tried to learn the model of a queue with capacity of8: package de.learnlib.ralib.TestSul;

import java.util.LinkedList; import java.util.Queue;

public class Queue8 { private Queue list;

public Queue8() {
    list = new LinkedList<>();
}

public void push(int x) {

    if (list.size() < 8) {
        list.add(x);
    }
}

public boolean pop(int y) {
    if(list.peek()==y) {
        list.poll();
        return true;
    }
    return false;
}

}

And with the following configurations:

!bash

target=de.learnlib.ralib.TestSul.Queue8 methods=push(int:int)void+\ pop(int:int)boolean:boolean

project.name=Queue8 logging.level=FINEST use.ceopt=true use.suffixopt=false use.fresh=false use.rwalk=true export.model=true rwalk.prob.fresh=0.8 rwalk.prob.reset=0.1 rwalk.max.depth=40 rwalk.max.runs=2000 rwalk.reset.count=false rwalk.draw.uniform=false

solver=z3

teachers=int:de.learnlib.ralib.tools.theories.IntegerEqualityTheory

I have attached the final learned model:

This is not equivalent with the SUL. Can I make any changes to extract an accurate model?

I have two additional questions. 1)The method that you used for analyzing counterexample is not same with the proposed method that you introduced in your paper "Active learning for extended finite state machines". Are these two methods the same in terms of performance? 2) Is there any method to visualize the extracted model?(for instance to dot,...)

Thank you for your attention. I am looking forward to hearing from you.

[Alim9100]

Have you developed other equivalence oracle except RandomWalk?

[fhowar]

Have you developed other equivalence oracle except RandomWalk?

RaLib currently only implements RandomWalk for black-box testing. Recently the configuration option rwalk.seed.transitions was added that will start RandomWalk not from the initial location but after one of the transitions in the current hypothesis model. In many cases, this is more effective for finding counterexamples.

https://github.com/LearnLib/ralib/commit/50fb172b049c782a8ef201dcf55b1131d03ea47d

More elaborate algorithms for finding counterexamples in RA learning will need some research or thesis projects.

[fhowar]

This is not equivalent with the SUL. Can I make any changes to extract an accurate model?

The number of RandomWalks you use seems low and you almost always use new data values while in your target pop() will only accept data values that were pushed before

rwalk.prob.fresh=0.5
rwalk.max.runs=10000

I would try to play with the above two options and see if the final model changes. Also, as mentioned in the other answer, try to set rwalk.seed.transitions=true

I have two additional questions. 1)The method that you used for analyzing counterexample is not same with the proposed method that you introduced in your paper "Active learning for extended finite state machines". Are these two methods the same in terms of performance?

Yes, you are right. The only real difference between the SL* default configuration in RaLib and the paper should be that the implementation uses a binary search for finding the relevant index of the counterexample. The worst case complexity of the default implementation should thus be better than reported in the paper, i.e., O(trlog(m)) instead of O(trm). The linear backwards search can be enabled in the code instead, yielding the complexity reported in the paper.

In practice, there should not be much of a difference if you use short counterexamples (e.g., by shortening with the ce optimisers that you enabled with use.ceopt=true).

https://github.com/LearnLib/ralib/blob/main/src/main/java/de/learnlib/ralib/learning/CounterexampleAnalysis.java#L41

2) Is there any method to visualize the extracted model?(for instance to dot,...)

You should be able to use the RaToDot class to produce dot models that can be rendered with the Graphviz tool

https://github.com/LearnLib/ralib/blob/main/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java https://graphviz.org

Thank you for your attention. I am looking forward to hearing from you.