make ADT configurable in its suffix finder

Author: mtf90

CHANGELOG.md

@@ -11,6 +11,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 * LearnLib now supports JPMS modules. All artifacts now provide a `module-info` descriptor except of the distribution artifacts (for Maven-less environments) which only provide an `Automatic-Module-Name` due to non-modular dependencies. Note that while this is a Java 9+ feature, LearnLib still supports Java 8 byte code for the remaining class files.
 * Added the L# active learning algorithm (thanks to [Tiago Ferreira](https://github.com/tiferrei)).
 * The `ADTLearner` has been refactored to no longer use the (now-removed) `SymbolQueryOracle` but a new `AdaptiveMembershipOracle` instead which supports answering queries in parallel (thanks to [Leon Vitorovic](https://github.com/leonthalee)).
+* The `ADTLearner` can now be parameterized in its counterexample analysis method.
 * Added an `InterningMembershipOracle` (including refinements) to the `learnlib-cache` artifact that interns query responses to reduce memory consumption of large data structures. This exports the internal concepts of the DHC learner (which no longer interns query responses automatically).
 * `StaticParallelOracleBuilder` now supports custom executor services.
 

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java

@@ -50,6 +50,7 @@
 import de.learnlib.algorithm.adt.model.ObservationTree;
 import de.learnlib.algorithm.adt.model.ReplacementResult;
 import de.learnlib.algorithm.adt.util.ADTUtil;
+import de.learnlib.counterexample.LocalSuffixFinder;
 import de.learnlib.counterexample.LocalSuffixFinders;
 import de.learnlib.logging.Category;
 import de.learnlib.oracle.AdaptiveMembershipOracle;
@@ -92,6 +93,7 @@ public class ADTLearner<I, O> implements LearningAlgorithm.MealyLearner<I, O>,
     private final Queue<DefaultQuery<I, Word<O>>> openCounterExamples;
     private final Set<DefaultQuery<I, Word<O>>> allCounterExamples;
     private final ObservationTree<ADTState<I, O>, I, O> observationTree;
+    private final LocalSuffixFinder<? super I, ? super Word<O>> suffixFinder;
     private ADTHypothesis<I, O> hypothesis;
     private ADT<ADTState<I, O>, I, O> adt;
 
@@ -100,7 +102,7 @@ public ADTLearner(Alphabet<I> alphabet,
                       LeafSplitter leafSplitter,
                       ADTExtender adtExtender,
                       SubtreeReplacer subtreeReplacer) {
-        this(alphabet, oracle, leafSplitter, adtExtender, subtreeReplacer, true);
+        this(alphabet, oracle, leafSplitter, adtExtender, subtreeReplacer, true, LocalSuffixFinders.RIVEST_SCHAPIRE);
     }
 
     @GenerateBuilder(defaults = BuilderDefaults.class)
@@ -109,7 +111,8 @@ public ADTLearner(Alphabet<I> alphabet,
                       LeafSplitter leafSplitter,
                       ADTExtender adtExtender,
                       SubtreeReplacer subtreeReplacer,
-                      boolean useObservationTree) {
+                      boolean useObservationTree,
+                      LocalSuffixFinder<? super I, ? super Word<O>> suffixFinder) {
 
         this.alphabet = alphabet;
         this.observationTree = new ObservationTree<>(this.alphabet, oracle, useObservationTree);
@@ -119,6 +122,7 @@ public ADTLearner(Alphabet<I> alphabet,
         this.leafSplitter = leafSplitter;
         this.adtExtender = adtExtender;
         this.subtreeReplacer = subtreeReplacer;
+        this.suffixFinder = suffixFinder;
 
         this.hypothesis = new ADTHypothesis<>(this.alphabet);
         this.openTransitions = new ArrayDeque<>();
@@ -188,8 +192,7 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
         }
 
         // Determine a counterexample decomposition (u, a, v)
-        final int suffixIdx =
-                LocalSuffixFinders.RIVEST_SCHAPIRE.findSuffixIndex(ceQuery, this.hypothesis, this.hypothesis, this.mqo);
+        final int suffixIdx = suffixFinder.findSuffixIndex(ceQuery, this.hypothesis, this.hypothesis, this.mqo);
 
         if (suffixIdx == -1) {
             throw new IllegalStateException();
@@ -859,5 +862,10 @@ public static SubtreeReplacer subtreeReplacer() {
         public static boolean useObservationTree() {
             return true;
         }
+
+        @SuppressWarnings("unchecked")
+        public static <I, D> LocalSuffixFinder<I, D> suffixFinder() {
+            return (LocalSuffixFinder<I, D>) LocalSuffixFinders.RIVEST_SCHAPIRE;
+        }
     }
 }

algorithms/active/adt/src/test/java/de/learnlib/algorithm/adt/it/ADTIT.java

@@ -31,6 +31,8 @@
 import de.learnlib.algorithm.adt.config.SubtreeReplacers;
 import de.learnlib.algorithm.adt.learner.ADTLearner;
 import de.learnlib.algorithm.adt.learner.ADTLearnerBuilder;
+import de.learnlib.counterexample.LocalSuffixFinder;
+import de.learnlib.counterexample.LocalSuffixFinders;
 import de.learnlib.driver.simulator.MealySimulatorSUL;
 import de.learnlib.filter.statistic.oracle.CounterAdaptiveQueryOracle;
 import de.learnlib.oracle.AdaptiveMembershipOracle;
@@ -49,6 +51,7 @@
 import net.automatalib.automaton.transducer.impl.CompactMealy;
 import net.automatalib.exception.FormatException;
 import net.automatalib.serialization.dot.DOTParsers;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.testng.Assert;
 import org.testng.annotations.Test;
 
@@ -88,9 +91,14 @@ protected <I, O> void addLearnerVariants(Alphabet<I> alphabet,
                 for (int k = 0; k < SUBTREE_REPLACERS.size(); k++) {
                     final SubtreeReplacer subtreeReplacer = SUBTREE_REPLACERS.get(k);
                     builder.setSubtreeReplacer(subtreeReplacer);
-                    builder.setUseObservationTree(useCacheGenerator.nextBoolean());
 
-                    variants.addLearnerVariant(i + "," + j + "," + k, builder.create());
+                    for (LocalSuffixFinder<@Nullable Object, @Nullable Object> suffixFinder : LocalSuffixFinders.values()) {
+                        builder.setSuffixFinder(suffixFinder);
+                        builder.setUseObservationTree(useCacheGenerator.nextBoolean());
+
+                        variants.addLearnerVariant(i + "," + j + "," + k, builder.create());
+                    }
+
                 }
             }
         }