Parallelize ADT Learner

CHANGELOG.md

@@ -10,6 +10,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 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).
+* The `ADTLearner` has been refactored to 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)).
 
 ### Changed
 
@@ -30,6 +31,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 * The `de.learnlib.tooling:learnlib-annotation-processor` artifact has been dropped. The functionality has been moved to a [standalone project](https://github.com/LearnLib/build-tools).
 * The `de.learnlib:learnlib-rpni-edsm` and `de.learnlib:learnlib-rpni-mdl` artifacts have been dropped. The code has been merged with the `de.learnlib:learnlib-rpni` artifact.
 * `PropertyOracle`s can no longer set a property. This value is now immutable and must be provided during instantiation. Previously, the internal state wasn't updated accordingly if a property was overridden.
+* `SymbolQueryOracle`s (and related code such as the respective caches, counters, etc.) have been removed without replacement. Equivalent functionality on the basis of the new `AdaptiveMembershipOracle`s is available instead.
 
 
 ## [0.17.0] - 2023-11-15

algorithms/active/adt/pom.xml

@@ -40,6 +40,10 @@ limitations under the License.
             <groupId>de.learnlib</groupId>
             <artifactId>learnlib-api</artifactId>
         </dependency>
+        <dependency>
+            <groupId>de.learnlib</groupId>
+            <artifactId>learnlib-cache</artifactId>
+        </dependency>
         <dependency>
             <groupId>de.learnlib</groupId>
             <artifactId>learnlib-counterexamples</artifactId>

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADT.java

@@ -22,7 +22,6 @@
 import de.learnlib.algorithm.adt.api.LeafSplitter;
 import de.learnlib.algorithm.adt.config.LeafSplitters;
 import de.learnlib.algorithm.adt.util.ADTUtil;
-import de.learnlib.oracle.SymbolQueryOracle;
 import net.automatalib.word.Word;
 
 /**
@@ -93,29 +92,6 @@ public void replaceNode(ADTNode<S, I, O> oldNode, ADTNode<S, I, O> newNode) {
         }
     }
 
-    /**
-     * Successively sifts a word through the ADT induced by the given node. Stops when reaching a leaf.
-     *
-     * @param oracle
-     *         the oracle to query with inner node symbols
-     * @param word
-     *         the word to sift
-     * @param subtree
-     *         the node whose subtree is considered
-     *
-     * @return the leaf (see {@link ADTNode#sift(SymbolQueryOracle, Word)})
-     */
-    public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> word, ADTNode<S, I, O> subtree) {
-
-        ADTNode<S, I, O> current = subtree;
-
-        while (!ADTUtil.isLeafNode(current)) {
-            current = current.sift(oracle, word);
-        }
-
-        return current;
-    }
-
     /**
      * Splitting a leaf node by extending the trace leading into the node to split.
      *

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTLeafNode.java

@@ -15,9 +15,7 @@
  */
 package de.learnlib.algorithm.adt.adt;
 
-import de.learnlib.oracle.SymbolQueryOracle;
 import net.automatalib.graph.ads.impl.AbstractRecursiveADSLeafNode;
-import net.automatalib.word.Word;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -37,11 +35,6 @@ public ADTLeafNode(@Nullable ADTNode<S, I, O> parent, @Nullable S hypothesisStat
         super(parent, hypothesisState);
     }
 
-    @Override
-    public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
-        throw new UnsupportedOperationException("Final nodes cannot sift words");
-    }
-
     @Override
     public NodeType getNodeType() {
         return NodeType.LEAF_NODE;

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTNode.java

@@ -19,10 +19,8 @@
 import java.util.Map;
 
 import de.learnlib.algorithm.adt.util.ADTUtil;
-import de.learnlib.oracle.SymbolQueryOracle;
 import net.automatalib.graph.ads.RecursiveADSNode;
 import net.automatalib.visualization.VisualizationHelper;
-import net.automatalib.word.Word;
 
 /**
  * The ADT equivalent of {@link net.automatalib.graph.ads.ADSNode}. In contrast to regular adaptive distinguishing
@@ -38,23 +36,16 @@
 public interface ADTNode<S, I, O> extends RecursiveADSNode<S, I, O, ADTNode<S, I, O>> {
 
     /**
-     * Utility method, that sifts a given word through {@code this} ADTNode. If {@code this} node is a <ul> <li>symbol
-     * node, the symbol is applied to the system under learning and the corresponding child node (based on the observed
-     * output) is returned. If no matching child node is found, a new leaf node is returned instead </li> <li> reset
-     * node, the system under learning is reset and the provided prefix is reapplied to the system </li> <li> leaf node,
-     * an exception is thrown </li> </ul>
+     * Convenience method for directly accessing this node's {@link #getChildren() children}.
      *
-     * @param oracle
-     *         the oracle used to query the system under learning
-     * @param prefix
-     *         the prefix to be re-applied after encountering a reset node
+     * @param output
+     *         the output symbol to determine the child to returned
      *
-     * @return the corresponding child node
-     *
-     * @throws UnsupportedOperationException
-     *         when invoked on a leaf node (see {@link #getNodeType()}).
+     * @return the child node that is mapped to given output. May be {@code null},
      */
-    ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix);
+    default ADTNode<S, I, O> getChild(O output) {
+        return getChildren().get(output);
+    }
 
     // default methods for graph interface
     @Override

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java

@@ -18,8 +18,6 @@
 import java.util.Collections;
 import java.util.Map;
 
-import de.learnlib.oracle.SymbolQueryOracle;
-import net.automatalib.word.Word;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -76,17 +74,6 @@ public void setHypothesisState(S state) {
         throw new UnsupportedOperationException("Reset nodes cannot reference a hypothesis state");
     }
 
-    @Override
-    public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
-        oracle.reset();
-
-        for (I i : prefix) {
-            oracle.query(i);
-        }
-
-        return successor;
-    }
-
     @Override
     public NodeType getNodeType() {
         return NodeType.RESET_NODE;

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTSymbolNode.java

@@ -15,9 +15,7 @@
  */
 package de.learnlib.algorithm.adt.adt;
 
-import de.learnlib.oracle.SymbolQueryOracle;
 import net.automatalib.graph.ads.impl.AbstractRecursiveADSSymbolNode;
-import net.automatalib.word.Word;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -37,21 +35,6 @@ public ADTSymbolNode(@Nullable ADTNode<S, I, O> parent, I symbol) {
         super(parent, symbol);
     }
 
-    @Override
-    public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
-        final O o = oracle.query(super.getSymbol());
-
-        final ADTNode<S, I, O> successor = super.getChildren().get(o);
-
-        if (successor == null) {
-            final ADTNode<S, I, O> result = new ADTLeafNode<>(this, null);
-            super.getChildren().put(o, result);
-            return result;
-        }
-
-        return successor;
-    }
-
     @Override
     public NodeType getNodeType() {
         return NodeType.SYMBOL_NODE;

algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java

@@ -159,7 +159,7 @@ public static <S, I, O> ADTNode<S, I, O> splitParent(ADTNode<S, I, O> nodeToSpli
             newIter.next();
             newSuffixOutput = oldIter.next();
 
-            adsIter = adsIter.getChildren().get(newSuffixOutput);
+            adsIter = adsIter.getChild(newSuffixOutput);
         }
 
         final ADTNode<S, I, O> continuedADS = new ADTSymbolNode<>(adsIter.getParent(), suffixIter.next());

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

@@ -0,0 +1,81 @@
+/* Copyright (C) 2013-2024 TU Dortmund University
+ * This file is part of LearnLib, http://www.learnlib.de/.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package de.learnlib.algorithm.adt.learner;
+
+import java.util.ArrayDeque;
+import java.util.Deque;
+
+import de.learnlib.algorithm.adt.adt.ADTNode;
+import de.learnlib.algorithm.adt.automaton.ADTState;
+import net.automatalib.word.Word;
+
+/**
+ * Utility class to resolve ADS ambiguities. This query simply tracks the current ADT node for the given inputs.
+ *
+ * @param <I>
+ *         input symbol type
+ * @param <O>
+ *         output symbol type
+ */
+class ADSAmbiguityQuery<I, O> extends AbstractAdaptiveQuery<I, O> {
+
+    private final Word<I> accessSequence;
+    private final Deque<I> oneShotPrefix;
+
+    private int asIndex;
+    private boolean inOneShot;
+
+    ADSAmbiguityQuery(Word<I> accessSequence, Word<I> oneShotPrefix, ADTNode<ADTState<I, O>, I, O> root) {
+        super(root);
+        this.accessSequence = accessSequence;
+        this.oneShotPrefix = new ArrayDeque<>(oneShotPrefix.asList());
+        this.asIndex = 0;
+        this.inOneShot = false;
+    }
+
+    @Override
+    public I getInput() {
+        if (this.asIndex < this.accessSequence.length()) {
+            return this.accessSequence.getSymbol(this.asIndex);
+        } else {
+            this.inOneShot = !this.oneShotPrefix.isEmpty();
+            if (this.inOneShot) {
+                return oneShotPrefix.poll();
+            } else {
+                return this.currentADTNode.getSymbol();
+            }
+        }
+    }
+
+    @Override
+    public Response processOutput(O out) {
+        if (this.asIndex < this.accessSequence.length()) {
+            asIndex++;
+            return Response.SYMBOL;
+        } else if (this.inOneShot) {
+            return Response.SYMBOL;
+        } else {
+            return super.processOutput(out);
+        }
+    }
+
+    @Override
+    protected void resetProgress() {
+        this.asIndex = 0;
+    }
+}
+
+

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

@@ -0,0 +1,107 @@
+/* Copyright (C) 2013-2024 TU Dortmund University
+ * This file is part of LearnLib, http://www.learnlib.de/.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package de.learnlib.algorithm.adt.learner;
+
+import java.util.Objects;
+
+import de.learnlib.algorithm.adt.automaton.ADTState;
+import de.learnlib.query.AdaptiveQuery;
+import de.learnlib.query.DefaultQuery;
+import net.automatalib.word.Word;
+import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+/**
+ * Utility class to verify ADSs. This query tracks the current ADT node for the given inputs and compares it with an
+ * expected output, potentially constructing a counterexample from the observed data.
+ *
+ * @param <I>
+ *         input symbol type
+ * @param <O>
+ *         output symbol type
+ */
+class ADSVerificationQuery<I, O> implements AdaptiveQuery<I, O> {
+
+    private final Word<I> prefix;
+    private final Word<I> suffix;
+    private final Word<O> expectedOutput;
+    private final WordBuilder<O> outputBuilder;
+    private final ADTState<I, O> state;
+
+    private final int prefixLength;
+    private final int suffixLength;
+    private int idx;
+    private @Nullable DefaultQuery<I, Word<O>> counterexample;
+
+    ADSVerificationQuery(Word<I> prefix, Word<I> suffix, Word<O> expectedSuffixOutput, ADTState<I, O> state) {
+        this.prefix = prefix;
+        this.suffix = suffix;
+        this.expectedOutput = expectedSuffixOutput;
+        this.outputBuilder = new WordBuilder<>(suffix.size());
+        this.state = state;
+
+        this.prefixLength = prefix.length();
+        this.suffixLength = suffix.length();
+        this.idx = 0;
+    }
+
+    @Override
+    public I getInput() {
+        if (idx < prefixLength) {
+            return prefix.getSymbol(idx);
+        } else {
+            return suffix.getSymbol(idx - prefixLength);
+        }
+    }
+
+    @Override
+    public Response processOutput(O out) {
+        if (idx < prefixLength) {
+            idx++;
+            return Response.SYMBOL;
+        } else {
+            outputBuilder.append(out);
+
+            if (!Objects.equals(out, expectedOutput.getSymbol(idx - prefixLength))) {
+                counterexample =
+                        new DefaultQuery<>(prefix, suffix.prefix(outputBuilder.size()), outputBuilder.toWord());
+                return Response.FINISHED;
+            } else if (outputBuilder.size() < suffixLength) {
+                idx++;
+                return Response.SYMBOL;
+            } else {
+                return Response.FINISHED;
+            }
+        }
+    }
+
+    @Nullable
+    DefaultQuery<I, Word<O>> getCounterexample() {
+        return counterexample;
+    }
+
+    ADTState<I, O> getState() {
+        return state;
+    }
+
+    Word<I> getSuffix() {
+        return suffix;
+    }
+
+    Word<O> getExpectedOutput() {
+        return expectedOutput;
+    }
+}