Instantiating a simple learning setup

On this page the creation of a simple learning setup will be discussed. Although this concrete example will discuss an example learning a Mealy Machine, the overall structure remains the same when dealing with other types of automata, such as DFAs. For full-code examples see either the in-tree examples or other LearnLib projects such as the CAV'15 example.

For LearnLib to start learning, a target system (System Under Learning, SUL) is needed. Usually this will be an actual system for which behavioral traits are to be collected. For the sake of simplicity and reproducibility this example will consider a preexisting automaton model. The ExampleCoffeeMachine class provides a method that returns an automaton representation of a simulated coffee machine. Using this automaton model the alphabet to be considered can be retrieved and both membership oracles and equivalence oracles can be instantiated:

CompactMealy<Input, String> fm = ExampleCoffeeMachine.constructMachine();
Alphabet<Input> alphabet = fm.getInputAlphabet();

SimulatorOracle<Input, Word<String>> simoracle = new SimulatorOracle<>(fm);
SimulatorEQOracle<Input, Word<String>> eqoracle = new SimulatorEQOracle<>(fm);

MembershipOracle<Input, Word<String>> cache = MealyCaches.createCache(alphabet, simoracle);

Note: In order to use the coffee machine hypothesis (which is usually only used in tests) you need to explicitly declare the corresponding maven artifact as a compile/runtime dependency:

...
<dependency>
    <groupId>de.learnlib.testsupport</groupId>
    <artifactId>learnlib-learning-examples</artifactId>
    <version>${learnlibVersion}</version>
    <scope>runtime</scope>
</dependency>
...

The SimulatorOracle and SimulatorEQOracle classes will generate responses in accordance to the provided automaton model. The MealyCacheOracle will filter out repeated (sub-)queries to speed up the learning process.

With the alphabet known and the various oracles being instantiated, the learning algorithm itself can be created:

MealyDHC<Input, String> learner = new MealyDHC<>(alphabet, cache);

Note that MealyDHC implements the LearningAlgorithm interface and can be substituted by any other algorithm capable of creating Mealy Machines. Note that the type variables match those of the example Mealy Machine: inputs are instances of Symbol, outputs are Strings. This means that the learning algorithm will create sequences of Symbol objects as queries and will expect String data as response. Accordingly, the provided alphabet also is specified to contain Symbol objects.

Now things are set up for learning. This is an iterative process, involving following steps:

1. Initial learning of a hypothesis. This first hypothesis is not necessarily complete.
2. Searching a counterexample that proves a mismatch between the learned hypothesis and SUL behavior.
3. If no counterexample was found, the learning procedure terminates.
4. Otherwise the counterexample will be provided to the learning algorithm to resume learning, which will produce a refined hypothesis. Afterwards the overall process will resume at Step 2.

This whole procedure can be implemented as follows:

DefaultQuery<Input, Word<String>> counterexample = null;
do {
    if (counterexample == null) {
        learner.startLearning();
    } else {
        boolean refined = learner.refineHypothesis(counterexample);
        if (!refined) {
            System.err.println("No refinement effected by counterexample!");
        }
    }

    counterexample = eqoracle.findCounterExample(learner.getHypothesisModel(), alphabet);

} while (counterexample != null);

// from here on learner.getHypothesisModel() will provide an accurate model

The do-while loop will be executed as long as counterexamples are discovered by the equivalence oracle. Once the loop terminates the hypothesis model provided by the learner is guaranteed to be an exact representation of the target system if the equivalence oracle is guaranteed to find any behavioral mismatches between the hypothesis and the target system (which is the case in this example).

The whole example in one piece:

CompactMealy<Input, String> fm = ExampleCoffeeMachine.constructMachine();
Alphabet<Input> alphabet = fm.getInputAlphabet();

SimulatorOracle<Input, Word<String>> simoracle = new SimulatorOracle<>(fm);
SimulatorEQOracle<Input, Word<String>> eqoracle = new SimulatorEQOracle<>(fm);

MembershipOracle<Input, Word<String>> cache = MealyCaches.createCache(alphabet, simoracle);

MealyDHC<Input, String> learner = new MealyDHC<>(alphabet, cache);

DefaultQuery<Input, Word<String>> counterexample = null;
do {
    if (counterexample == null) {
        learner.startLearning();
    } else {
        boolean refined = learner.refineHypothesis(counterexample);
        if (!refined) {
            System.err.println("No refinement effected by counterexample!");
        }
    }

    counterexample = eqoracle.findCounterExample(learner.getHypothesisModel(), alphabet);

} while (counterexample != null);

// from here on learner.getHypothesisModel() will provide an accurate model