Execution of TTT results in ConflictException on deterministic models

[emuskardin]

Hi :)

Describe the bug
Learning of Mealy Machines with TTT results in a cache ConflictException. When caching is removed, the algorithm learns the correct model.

Learning is done on randomly generated models, therefore there should be no non-deterministic behavior. In addition, if the learning algorithm is replaced, lets say with KV, the learning finishes as expected. So it seems that there might be some bug in TTT's handling of caching.

To Reproduce
I put a test script below that contains two seeds that reproduce the behavior and have included a screenshot of the output for one failing seed.

Desktop (please complete the following information):

• OS: Windows,
• Java version: 11
• LearnLib version: 0.17.0

Additional context
This happens relatively rarely, I encountered it while benchmarking random automata.

** Files **
Output:

Code to reproduce:

import de.learnlib.algorithm.LearningAlgorithm;
import de.learnlib.algorithm.ttt.mealy.TTTLearnerMealy;
import de.learnlib.driver.simulator.MealySimulatorSUL;
import de.learnlib.filter.cache.sul.SULCaches;
import de.learnlib.filter.statistic.Counter;
import de.learnlib.filter.statistic.sul.ResetCounterSUL;
import de.learnlib.filter.statistic.sul.SymbolCounterSUL;
import de.learnlib.oracle.EquivalenceOracle;
import de.learnlib.oracle.equivalence.MealyRandomWordsEQOracle;
import de.learnlib.oracle.membership.MealySimulatorOracle;
import de.learnlib.oracle.membership.SULOracle;
import de.learnlib.statistic.StatisticSUL;
import de.learnlib.sul.SUL;
import de.learnlib.util.Experiment;
import de.learnlib.util.statistic.SimpleProfiler;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.ListAlphabet;
import net.automatalib.automaton.transducer.CompactMealy;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.util.automaton.random.RandomAutomata;
import net.automatalib.word.Word;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Random;

import static de.learnlib.acex.AcexAnalyzers.BINARY_SEARCH_BWD;

public class TTTCacheError {
    public static void findFailing() throws IOException {

        int numStates = 1000;

        List<Integer> inputs = new ArrayList<>(Arrays.asList(0, 1, 2, 3, 4));
        List<Integer> outputs = new ArrayList<>(Arrays.asList(0, 1, 2, 3, 4));

        Alphabet<Integer> alphabet = new ListAlphabet<>(inputs);
        Alphabet<Integer> outputAlphabet =  new ListAlphabet<>(outputs);

        // Failing seeds 584,789
        int[] failingSeeds = {584,789};

        // can be used to find more failing
        // for (int k = 1000; k < 2000; k++) {

        for (int seedNum : failingSeeds){
            System.out.println("Failing seed " + seedNum);
            Random seed = new Random(seedNum);

            CompactMealy<Integer, Integer> target = RandomAutomata.randomMealy(seed, numStates, alphabet, outputAlphabet, true);
            
            MealySimulatorSUL<Integer, Integer> driver = new MealySimulatorSUL<>(target);

            StatisticSUL<Integer, Integer> queryStatisticSul = new ResetCounterSUL<>("membership queries", driver);
            StatisticSUL<Integer, Integer> stepStatisticSul = new SymbolCounterSUL<>("steps", queryStatisticSul);

            SUL<Integer, Integer> effectiveSul = stepStatisticSul;
            effectiveSul = SULCaches.createCache(alphabet, effectiveSul);

            SULOracle<Integer, Integer> mqOracle = new SULOracle<>(effectiveSul);
            LearningAlgorithm<? extends MealyMachine<?, Integer, ?, Integer>, Integer, Word<Integer>> learningAlg = null;

            learningAlg = new TTTLearnerMealy<>(alphabet, mqOracle, BINARY_SEARCH_BWD);
            // Seems to work for KV
            // learningAlg = new KearnsVaziraniMealy<>(alphabet, mqOracle, true, BINARY_SEARCH_BWD);


            EquivalenceOracle.MealyEquivalenceOracle<Integer, Integer> eqOracle = new MealyRandomWordsEQOracle<>(
                    new MealySimulatorOracle<>(target),
                    10,
                    50,
                    30000,
                    seed // make results reproducible
            );

            Experiment.MealyExperiment<Integer, Integer> experiment = new Experiment.MealyExperiment<>(learningAlg, eqOracle, alphabet);
            experiment.setProfile(true);
            experiment.setLogModels(false);
            SimpleProfiler.reset();

            experiment.run();

            Counter e = SimpleProfiler.cumulated("Learning");

            assert e != null;

            SimpleProfiler.logResults();

            MealyMachine<?, Integer, ?, Integer> result = experiment.getFinalHypothesis();
            // model statistics
            if (result.size() != target.size()) {
                System.out.println("Learning failed." + result.size() + " vs " + numStates);
            }
        }
    }

    public static void main(String[] args) throws IOException, InterruptedException, NoSuchMethodException {
        findFailing();
    }

}

[mtf90]

Dear @emuskardin,

thanks for the report. I can reproduce the error on the current development version and it seems to be related to the DAG cache implementation (which had similar issues in the past). If you don't care about memory consumption, you may use SULCaches.createTreeCache instead for your benchmarks. I'll try to extract a test-case from your example and open a ticket in AutomataLib.

[emuskardin]

Thank you @mtf90 :)

I don't know if this is useful information, but it seems that if you change cex. processing to BINARY_SEARCH_FWD at least for these 2 failing seeds it works (and for the other 1000 random models). However, it might simply be due to different learning processes, if BINARY_SEARCH_FWD and BINARY_SEARCH_BWD do not necessarily return the same splitting point.

I just tested FWD on 1000 random automata and no crashes, while 1000 tests were enough to find these 2 failing seeds for BWD.
Just saying this as while the bug might be in the cache, it is weird that in my experiments this bug is only triggered on TTT, and not on L*, KV, and OP.

[mtf90]

I think this mainly depends on the order in which words are inserted into the cache since the DAG cache tries to merge dangling ends that do not conflict. It appears that TTT + BINARY_SEARCH_BWD hits that sweet spot which performs an illegal merge that later causes conflicts.

[mtf90]

Closing in favor of LearnLib/automatalib#79.

This is actually a very good catch because it requires a specific structure and order of traces to trigger the issue. I should have a fix ready fairly quickly. Does this affect you in any critical production environment or can you live with it being included in the next regular release? In the meantime you could either use the nightly builds of LearnLib or fall-back to the tree cache.

[emuskardin]

Great :)
No, it was a minor inconvenience while playing with different algorithms, and as mentioned, it was hard to find :)