import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
import de.learnlib.algorithm.lambda.lstar.LLambdaMealy;
import de.learnlib.driver.simulator.MealySimulatorSUL;
import de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle;
import de.learnlib.oracle.equivalence.MealyRandomWpMethodEQOracle;
import de.learnlib.oracle.membership.SULOracle;
import de.learnlib.util.mealy.MealyUtil;
import net.automatalib.automaton.transducer.impl.CompactMealy;
import net.automatalib.exception.FormatException;
import net.automatalib.serialization.dot.DOTParsers;
import net.automatalib.util.automaton.Automata;

import java.io.IOException;
import java.util.*;

public class Main {

    public static void main(String[] args) {
        final var model = loadModel("mosquitto__two_client_will_retain.dot");
        final int eqoSeed = -1177788003;
        final var sul = new MealySimulatorSUL<>(model);
        final var mqo = new SULOracle<>(sul);
        final var learner = new LLambdaMealy<>(model.getInputAlphabet(), mqo);
        final var eqo = new MealyRandomWpMethodEQOracle<>(mqo, 0, 4, 1000000, new Random(eqoSeed), 1);
        learnToExhaustion(model, learner, eqo);
    }

    private static CompactMealy<String, String> loadModel(String name) {
        try {
            final var is = Main.class.getClassLoader().getResourceAsStream(name);
            return DOTParsers.mealy().readModel(is).model;
        } catch (IOException | FormatException e) {
            throw new RuntimeException(e.getMessage());
        }
    }

    private static void learnToExhaustion(CompactMealy<String, String> model,
                                          MealyLearner<String, String> learner,
                                          MealyEquivalenceOracle<String, String> eqo) {
        learner.startLearning();
        while (true) {
            if (Automata.findSeparatingWord(model, learner.getHypothesisModel(), model.getInputAlphabet()) == null) {
                return;
            }

            // the model is still incomplete
            final var cex = eqo.findCounterExample(learner.getHypothesisModel(), model.getInputAlphabet());
            if (cex == null) {
                throw new RuntimeException("counterexample exists, but was not found");
            }

            final var cexTrunc = MealyUtil.shortenCounterExample(learner.getHypothesisModel(), cex);
            if (!learner.refineHypothesis(cexTrunc)) {
                throw new RuntimeException("spurious counterexample from equivalence oracle");
            }
        }
    }
}

Exception in thread "main" java.lang.AssertionError
	at de.learnlib.algorithm.lambda.lstar.AbstractLLambda.refineHypothesis(AbstractLLambda.java:106)
	at de.learnlib.algorithm.lambda.lstar.LLambdaMealy.refineHypothesis(LLambdaMealy.java:32)
	at Main.learnToExhaustion(Main.java:53)
	at Main.main(Main.java:25)