diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6508f5bceb..5a6d521523 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/algorithms/active/adt/pom.xml b/algorithms/active/adt/pom.xml
index 2b8000b280..f8e97deb25 100644
--- a/algorithms/active/adt/pom.xml
+++ b/algorithms/active/adt/pom.xml
@@ -40,6 +40,10 @@ limitations under the License.
de.learnlib
learnlib-api
+
+ de.learnlib
+ learnlib-cache
+
de.learnlib
learnlib-counterexamples
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADT.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADT.java
index 4a9e202ec9..f2e36ce6a6 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADT.java
+++ b/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 oldNode, ADTNode 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 sift(SymbolQueryOracle oracle, Word word, ADTNode subtree) {
-
- ADTNode 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.
*
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTLeafNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTLeafNode.java
index b855da8978..efc20275c7 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTLeafNode.java
+++ b/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 parent, @Nullable S hypothesisStat
super(parent, hypothesisState);
}
- @Override
- public ADTNode sift(SymbolQueryOracle oracle, Word prefix) {
- throw new UnsupportedOperationException("Final nodes cannot sift words");
- }
-
@Override
public NodeType getNodeType() {
return NodeType.LEAF_NODE;
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTNode.java
index 9d7b133604..f2373d53f2 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTNode.java
+++ b/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 extends RecursiveADSNode> {
/**
- * Utility method, that sifts a given word through {@code this} ADTNode. If {@code this} node is a - 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
- reset
- * node, the system under learning is reset and the provided prefix is reapplied to the system
- leaf node,
- * an exception is thrown
+ * 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 sift(SymbolQueryOracle oracle, Word prefix);
+ default ADTNode getChild(O output) {
+ return getChildren().get(output);
+ }
// default methods for graph interface
@Override
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java
index c0de4b6eb6..c4c2c9ec2f 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java
+++ b/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 sift(SymbolQueryOracle oracle, Word prefix) {
- oracle.reset();
-
- for (I i : prefix) {
- oracle.query(i);
- }
-
- return successor;
- }
-
@Override
public NodeType getNodeType() {
return NodeType.RESET_NODE;
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTSymbolNode.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTSymbolNode.java
index ba89a47cee..7f648fea07 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTSymbolNode.java
+++ b/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 parent, I symbol) {
super(parent, symbol);
}
- @Override
- public ADTNode sift(SymbolQueryOracle oracle, Word prefix) {
- final O o = oracle.query(super.getSymbol());
-
- final ADTNode successor = super.getChildren().get(o);
-
- if (successor == null) {
- final ADTNode result = new ADTLeafNode<>(this, null);
- super.getChildren().put(o, result);
- return result;
- }
-
- return successor;
- }
-
@Override
public NodeType getNodeType() {
return NodeType.SYMBOL_NODE;
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java
index 4be1ac0f83..7e75269a2d 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java
@@ -159,7 +159,7 @@ public static ADTNode splitParent(ADTNode nodeToSpli
newIter.next();
newSuffixOutput = oldIter.next();
- adsIter = adsIter.getChildren().get(newSuffixOutput);
+ adsIter = adsIter.getChild(newSuffixOutput);
}
final ADTNode continuedADS = new ADTSymbolNode<>(adsIter.getParent(), suffixIter.next());
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADSAmbiguityQuery.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADSAmbiguityQuery.java
new file mode 100644
index 0000000000..e6304b6457
--- /dev/null
+++ b/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
+ * input symbol type
+ * @param
+ * output symbol type
+ */
+class ADSAmbiguityQuery extends AbstractAdaptiveQuery {
+
+ private final Word accessSequence;
+ private final Deque oneShotPrefix;
+
+ private int asIndex;
+ private boolean inOneShot;
+
+ ADSAmbiguityQuery(Word accessSequence, Word oneShotPrefix, ADTNode, 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;
+ }
+}
+
+
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADSVerificationQuery.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADSVerificationQuery.java
new file mode 100644
index 0000000000..c722bf7bf2
--- /dev/null
+++ b/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
+ * input symbol type
+ * @param
+ * output symbol type
+ */
+class ADSVerificationQuery implements AdaptiveQuery {
+
+ private final Word prefix;
+ private final Word suffix;
+ private final Word expectedOutput;
+ private final WordBuilder outputBuilder;
+ private final ADTState state;
+
+ private final int prefixLength;
+ private final int suffixLength;
+ private int idx;
+ private @Nullable DefaultQuery> counterexample;
+
+ ADSVerificationQuery(Word prefix, Word suffix, Word expectedSuffixOutput, ADTState 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> getCounterexample() {
+ return counterexample;
+ }
+
+ ADTState getState() {
+ return state;
+ }
+
+ Word getSuffix() {
+ return suffix;
+ }
+
+ Word getExpectedOutput() {
+ return expectedOutput;
+ }
+}
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTAdaptiveQuery.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTAdaptiveQuery.java
new file mode 100644
index 0000000000..ee120fc3e3
--- /dev/null
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTAdaptiveQuery.java
@@ -0,0 +1,94 @@
+/* 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 de.learnlib.algorithm.adt.adt.ADTNode;
+import de.learnlib.algorithm.adt.automaton.ADTState;
+import de.learnlib.algorithm.adt.automaton.ADTTransition;
+import de.learnlib.algorithm.adt.util.ADTUtil;
+import net.automatalib.word.Word;
+
+/**
+ * Utility class to close transitions. This query simply tracks the current ADT node for the access sequence of the
+ * given transition and sets its output if the respective input symbol is traversed.
+ *
+ * @param
+ * input symbol type
+ * @param
+ * output symbol type
+ */
+class ADTAdaptiveQuery extends AbstractAdaptiveQuery {
+
+ private final ADTTransition transition;
+ private final Word accessSequence;
+
+ private int asIndex;
+
+ ADTAdaptiveQuery(ADTTransition transition, ADTNode, I, O> root) {
+ super(root);
+ this.transition = transition;
+ this.accessSequence = transition.getSource().getAccessSequence();
+ this.asIndex = 0;
+ }
+
+ @Override
+ public I getInput() {
+ if (this.asIndex <= this.accessSequence.length()) {
+
+ if (asIndex == this.accessSequence.length()) {
+ return transition.getInput();
+ }
+
+ return this.accessSequence.getSymbol(this.asIndex);
+ } else {
+ return super.currentADTNode.getSymbol();
+ }
+ }
+
+ @Override
+ public Response processOutput(O out) {
+ if (this.asIndex <= this.accessSequence.length()) {
+ if (this.asIndex == this.accessSequence.length()) {
+ this.transition.setOutput(out);
+ }
+
+ // if the ADT only consists of a leaf, we just set the transition output
+ if (ADTUtil.isLeafNode(super.currentADTNode)) {
+ return Response.FINISHED;
+ }
+
+ asIndex++;
+ return Response.SYMBOL;
+ } else {
+ return super.processOutput(out);
+ }
+ }
+
+ @Override
+ protected void resetProgress() {
+ this.asIndex = 0;
+ }
+
+ ADTTransition getTransition() {
+ return transition;
+ }
+
+ Word getAccessSequence() {
+ return this.accessSequence;
+ }
+}
+
+
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java
index ad4262044e..178378c723 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java
@@ -17,12 +17,13 @@
import java.util.ArrayDeque;
import java.util.ArrayList;
+import java.util.Collection;
import java.util.Collections;
-import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
+import java.util.Map.Entry;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;
@@ -49,10 +50,10 @@
import de.learnlib.algorithm.adt.model.ObservationTree;
import de.learnlib.algorithm.adt.model.ReplacementResult;
import de.learnlib.algorithm.adt.util.ADTUtil;
-import de.learnlib.algorithm.adt.util.SQOOTBridge;
import de.learnlib.counterexample.LocalSuffixFinders;
import de.learnlib.logging.Category;
-import de.learnlib.oracle.SymbolQueryOracle;
+import de.learnlib.oracle.AdaptiveMembershipOracle;
+import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
import de.learnlib.util.MQUtil;
@@ -61,7 +62,6 @@
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.util.Pair;
import net.automatalib.word.Word;
-import net.automatalib.word.WordBuilder;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
@@ -81,7 +81,8 @@ public class ADTLearner implements LearningAlgorithm.MealyLearner,
private static final Logger LOGGER = LoggerFactory.getLogger(ADTLearner.class);
private final Alphabet alphabet;
- private final SQOOTBridge oracle;
+ private final AdaptiveMembershipOracle oracle;
+ private final MealyMembershipOracle mqo;
private final LeafSplitter leafSplitter;
private final ADTExtender adtExtender;
private final SubtreeReplacer subtreeReplacer;
@@ -93,7 +94,7 @@ public class ADTLearner implements LearningAlgorithm.MealyLearner,
private ADT, I, O> adt;
public ADTLearner(Alphabet alphabet,
- SymbolQueryOracle oracle,
+ AdaptiveMembershipOracle oracle,
LeafSplitter leafSplitter,
ADTExtender adtExtender,
SubtreeReplacer subtreeReplacer) {
@@ -102,15 +103,16 @@ public ADTLearner(Alphabet alphabet,
@GenerateBuilder(defaults = BuilderDefaults.class)
public ADTLearner(Alphabet alphabet,
- SymbolQueryOracle oracle,
+ AdaptiveMembershipOracle oracle,
LeafSplitter leafSplitter,
ADTExtender adtExtender,
SubtreeReplacer subtreeReplacer,
boolean useObservationTree) {
this.alphabet = alphabet;
- this.observationTree = new ObservationTree<>(this.alphabet);
- this.oracle = new SQOOTBridge<>(this.observationTree, oracle, useObservationTree);
+ this.observationTree = new ObservationTree<>(this.alphabet, oracle, useObservationTree);
+ this.oracle = this.observationTree;
+ this.mqo = new Adaptive2MembershipWrapper<>(oracle);
this.leafSplitter = leafSplitter;
this.adtExtender = adtExtender;
@@ -129,7 +131,6 @@ public void startLearning() {
final ADTState initialState = this.hypothesis.addInitialState();
initialState.setAccessSequence(Word.epsilon());
this.observationTree.initialize(initialState);
- this.oracle.initialize();
this.adt.initialize(initialState);
for (I i : this.alphabet) {
@@ -163,7 +164,7 @@ public boolean refineHypothesis(DefaultQuery> ce) {
// subtree replacements may reactivate old CEs
for (DefaultQuery> oldCE : this.allCounterExamples) {
- if (!this.hypothesis.computeOutput(oldCE.getInput()).equals(oldCE.getOutput())) {
+ if (MQUtil.isCounterexample(oldCE, this.hypothesis)) {
this.openCounterExamples.add(oldCE);
}
}
@@ -181,10 +182,8 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) {
}
// Determine a counterexample decomposition (u, a, v)
- final int suffixIdx = LocalSuffixFinders.RIVEST_SCHAPIRE.findSuffixIndex(ceQuery,
- this.hypothesis,
- this.hypothesis,
- this.oracle);
+ final int suffixIdx =
+ LocalSuffixFinders.RIVEST_SCHAPIRE.findSuffixIndex(ceQuery, this.hypothesis, this.hypothesis, this.mqo);
if (suffixIdx == -1) {
throw new IllegalStateException();
@@ -238,8 +237,8 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) {
newNode = this.adt.extendLeaf(nodeToSplit, completeSplitter, oldOutput, newOutput, this.leafSplitter);
} else {
// directly insert into observation tree, because we use it for finding a splitter
- this.observationTree.addTrace(uaState, v, this.oracle.answerQuery(uaAccessSequence, v));
- this.observationTree.addTrace(newState, v, this.oracle.answerQuery(uAccessSequenceWithA, v));
+ this.observationTree.addTrace(uaState, v, this.mqo.answerQuery(uaAccessSequence, v));
+ this.observationTree.addTrace(newState, v, this.mqo.answerQuery(uAccessSequenceWithA, v));
// in doubt, we will always find v
final Word otSepWord = this.observationTree.findSeparatingWord(uaState, newState);
@@ -297,58 +296,23 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) {
*/
private void closeTransitions() {
while (!this.openTransitions.isEmpty()) {
- this.closeTransition(this.openTransitions.poll());
- }
- }
-
- /**
- * Close the given transitions by means of sifting the associated long prefix through the ADT.
- *
- * @param transition
- * the transition to close
- */
- private void closeTransition(ADTTransition transition) {
-
- if (!transition.needsSifting()) {
- return;
- }
-
- final Word accessSequence = transition.getSource().getAccessSequence();
- final I symbol = transition.getInput();
-
- this.oracle.reset();
- for (I i : accessSequence) {
- this.oracle.query(i);
- }
- transition.setOutput(this.oracle.query(symbol));
+ final Collection> queries = new ArrayList<>(this.openTransitions.size());
- final Word longPrefix = accessSequence.append(symbol);
- final ADTNode, I, O> finalNode =
- this.adt.sift(this.oracle, longPrefix, transition.getSiftNode());
-
- assert ADTUtil.isLeafNode(finalNode);
-
- final ADTState targetState;
-
- // new state discovered while sifting
- if (finalNode.getHypothesisState() == null) {
- targetState = this.hypothesis.addState();
- targetState.setAccessSequence(longPrefix);
-
- finalNode.setHypothesisState(targetState);
- transition.setIsSpanningTreeEdge(true);
+ //create a query object for every transition
+ for (ADTTransition transition : this.openTransitions) {
+ if (transition.needsSifting()) {
+ queries.add(new ADTAdaptiveQuery<>(transition, transition.getSiftNode()));
+ }
+ }
- this.observationTree.addState(targetState, longPrefix, transition.getOutput());
+ this.openTransitions.clear();
+ this.oracle.processQueries(queries);
- for (I i : this.alphabet) {
- this.openTransitions.add(this.hypothesis.createOpenTransition(targetState, i, this.adt.getRoot()));
+ for (ADTAdaptiveQuery query : queries) {
+ processAnsweredQuery(query);
}
- } else {
- targetState = finalNode.getHypothesisState();
}
-
- transition.setTarget(targetState);
}
@Override
@@ -361,7 +325,9 @@ public void closeTransition(ADTState state, I input) {
final ADTNode, I, O> ads = transition.getSiftNode();
final int oldNumberOfFinalStates = ADTUtil.collectLeaves(ads).size();
- this.closeTransition(transition);
+ final ADTAdaptiveQuery query = new ADTAdaptiveQuery<>(transition, transition.getSiftNode());
+ this.oracle.processQueries(Collections.singleton(query));
+ processAnsweredQuery(query);
final int newNumberOfFinalStates = ADTUtil.collectLeaves(ads).size();
@@ -371,6 +337,50 @@ public void closeTransition(ADTState state, I input) {
}
}
+ private void processAnsweredQuery(ADTAdaptiveQuery query) {
+ if (query.needsPostProcessing()) {
+ final ADTNode, I, O> parent = query.getCurrentADTNode();
+ final O out = query.getTempOut();
+ final ADTNode, I, O> succ = parent.getChild(out);
+
+ // first time we process the successor
+ if (succ == null) {
+ // add new state to the hypothesis and set the accessSequence
+ final ADTState newState = this.hypothesis.addState();
+ final Word longPrefix = query.getAccessSequence().append(query.getTransition().getInput());
+ newState.setAccessSequence(longPrefix);
+
+ // configure the transition
+ final ADTTransition transition = query.getTransition();
+ transition.setTarget(newState);
+ transition.setIsSpanningTreeEdge(true);
+
+ // add new leaf node to ADT
+ final ADTNode, I, O> result = new ADTLeafNode<>(parent, newState);
+ parent.getChildren().put(out, result);
+
+ // add the observations to the observation tree
+ O transitionOutput = query.getTransition().getOutput();
+ this.observationTree.addState(newState, longPrefix, transitionOutput);
+
+ // query successors
+ for (I i : this.alphabet) {
+ this.openTransitions.add(this.hypothesis.createOpenTransition(newState, i, this.adt.getRoot()));
+ }
+ } else {
+ assert ADTUtil.isLeafNode(succ);
+ // state has been created before, just update target
+ query.getTransition().setTarget(succ.getHypothesisState());
+ }
+ } else {
+ // update target
+ final ADTTransition transition = query.getTransition();
+ final ADTNode, I, O> adtNode = query.getCurrentADTNode();
+ assert ADTUtil.isLeafNode(adtNode);
+ transition.setTarget(adtNode.getHypothesisState());
+ }
+ }
+
@Override
public boolean isTransitionDefined(ADTState state, I input) {
final ADTTransition transition = this.hypothesis.getTransition(state, input);
@@ -386,7 +396,7 @@ public void addAlphabetSymbol(I symbol) {
}
this.hypothesis.addAlphabetSymbol(symbol);
- this.observationTree.getObservationTree().addAlphabetSymbol(symbol);
+ this.observationTree.addAlphabetSymbol(symbol);
// check if we already have information about the symbol (then the transition is defined) so we don't post
// redundant queries
@@ -423,7 +433,6 @@ public void resume(ADTLearnerState, I, O> state) {
this.observationTree.initialize(this.hypothesis.getStates(),
ADTState::getAccessSequence,
this.hypothesis::computeOutput);
- this.oracle.initialize();
}
}
@@ -648,59 +657,38 @@ private ADTNode, I, O> verifyADS(ADTNode, I, O> no
.forEach(x -> traces.put(x.getHypothesisState(), ADTUtil.buildTraceForNode(x)));
final Pair, Word> parentTrace = ADTUtil.buildTraceForNode(nodeToReplace);
- final Word parentInput = parentTrace.getFirst();
- final Word parentOutput = parentTrace.getSecond();
ADTNode, I, O> result = null;
- // validate
- for (Map.Entry, Pair, Word>> entry : traces.entrySet()) {
- final ADTState state = entry.getKey();
- final Word accessSequence = state.getAccessSequence();
-
- this.oracle.reset();
- accessSequence.forEach(this.oracle::query);
- parentInput.forEach(this.oracle::query);
+ final List> queries = new ArrayList<>(traces.size());
- final Word adsInput = entry.getValue().getFirst();
- final Word adsOutput = entry.getValue().getSecond();
-
- final WordBuilder inputWb = new WordBuilder<>(adsInput.size());
- final WordBuilder outputWb = new WordBuilder<>(adsInput.size());
-
- final Iterator inputIter = adsInput.iterator();
- final Iterator outputIter = adsOutput.iterator();
-
- boolean equal = true;
- while (equal && inputIter.hasNext()) {
- final I in = inputIter.next();
- final O realOut = this.oracle.query(in);
- final O expectedOut = outputIter.next();
+ for (Entry, Pair, Word>> e : traces.entrySet()) {
+ final ADTState state = e.getKey();
+ final Pair, Word> ads = e.getValue();
+ queries.add(new ADSVerificationQuery<>(state.getAccessSequence().concat(parentTrace.getFirst()),
+ ads.getFirst(),
+ ads.getSecond(),
+ state));
+ }
- inputWb.append(in);
- outputWb.append(realOut);
+ this.oracle.processQueries(queries);
- if (!expectedOut.equals(realOut)) {
- equal = false;
- }
- }
+ for (ADSVerificationQuery query : queries) {
+ final ADTNode, I, O> trace;
+ final DefaultQuery> ce = query.getCounterexample();
- final Word traceInput = inputWb.toWord();
- final Word traceOutput = outputWb.toWord();
-
- if (!equal) {
- this.openCounterExamples.add(new DefaultQuery<>(accessSequence.concat(parentInput, traceInput),
- this.hypothesis.computeOutput(state.getAccessSequence())
- .concat(parentOutput, traceOutput)));
+ if (ce != null) {
+ this.openCounterExamples.add(ce);
+ trace = ADTUtil.buildADSFromObservation(ce.getSuffix(), ce.getOutput(), query.getState());
+ } else {
+ trace = ADTUtil.buildADSFromObservation(query.getSuffix(), query.getExpectedOutput(), query.getState());
}
- final ADTNode, I, O> trace = ADTUtil.buildADSFromObservation(traceInput, traceOutput, state);
-
if (result == null) {
result = trace;
} else {
if (!ADTUtil.mergeADS(result, trace)) {
- this.resolveAmbiguities(nodeToReplace, result, state, cachedLeaves);
+ this.resolveAmbiguities(nodeToReplace, result, query.getState(), cachedLeaves);
}
}
}
@@ -732,39 +720,26 @@ private void resolveAmbiguities(ADTNode, I, O> nodeToReplace,
Set, I, O>> cachedLeaves) {
final Pair, Word> parentTrace = ADTUtil.buildTraceForNode(nodeToReplace);
- final Word parentInput = parentTrace.getFirst();
- final Word effectiveAccessSequence = state.getAccessSequence().concat(parentInput);
+ final ADSAmbiguityQuery query =
+ new ADSAmbiguityQuery<>(state.getAccessSequence(), parentTrace.getFirst(), newADS);
- this.oracle.reset();
- effectiveAccessSequence.forEach(this.oracle::query);
-
- ADTNode, I, O> iter = newADS;
- while (!ADTUtil.isLeafNode(iter)) {
-
- if (ADTUtil.isResetNode(iter)) {
- this.oracle.reset();
- state.getAccessSequence().forEach(this.oracle::query);
- iter = iter.getChildren().values().iterator().next();
- } else {
- final O output = this.oracle.query(iter.getSymbol());
- final ADTNode, I, O> succ = iter.getChildren().get(output);
+ this.oracle.processQuery(query);
- if (succ == null) {
- final ADTNode, I, O> newFinal = new ADTLeafNode<>(iter, state);
- iter.getChildren().put(output, newFinal);
- return;
- }
-
- iter = succ;
- }
+ if (query.needsPostProcessing()) {
+ final ADTNode, I, O> prev = query.getCurrentADTNode();
+ final ADTNode, I, O> newFinal = new ADTLeafNode<>(prev, state);
+ prev.getChildren().put(query.getTempOut(), newFinal);
+ return;
}
+ final ADTNode, I, O> finalNode = query.getCurrentADTNode();
ADTNode, I, O> oldReference = null, newReference = null;
+
for (ADTNode, I, O> leaf : cachedLeaves) {
final ADTState hypState = leaf.getHypothesisState();
assert hypState != null;
- if (hypState.equals(iter.getHypothesisState())) {
+ if (hypState.equals(finalNode.getHypothesisState())) {
oldReference = leaf;
} else if (hypState.equals(state)) {
newReference = leaf;
@@ -784,7 +759,7 @@ private void resolveAmbiguities(ADTNode, I, O> nodeToReplace,
final Word newOutputTrace = lcaTrace.getSecond().append(lcaResult.secondOutput);
final ADTNode, I, O> oldTrace =
- ADTUtil.buildADSFromObservation(sepWord, oldOutputTrace, iter.getHypothesisState());
+ ADTUtil.buildADSFromObservation(sepWord, oldOutputTrace, finalNode.getHypothesisState());
final ADTNode, I, O> newTrace = ADTUtil.buildADSFromObservation(sepWord, newOutputTrace, state);
if (!ADTUtil.mergeADS(oldTrace, newTrace)) {
@@ -792,9 +767,9 @@ private void resolveAmbiguities(ADTNode, I, O> nodeToReplace,
}
final ADTNode, I, O> reset = new ADTResetNode<>(oldTrace);
- final ADTNode, I, O> parent = iter.getParent();
+ final ADTNode, I, O> parent = finalNode.getParent();
assert parent != null;
- final O parentOutput = ADTUtil.getOutputForSuccessor(parent, iter);
+ final O parentOutput = ADTUtil.getOutputForSuccessor(parent, finalNode);
parent.getChildren().put(parentOutput, reset);
reset.setParent(parent);
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/AbstractAdaptiveQuery.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/AbstractAdaptiveQuery.java
new file mode 100644
index 0000000000..b3c440cbc3
--- /dev/null
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/AbstractAdaptiveQuery.java
@@ -0,0 +1,74 @@
+/* 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 de.learnlib.algorithm.adt.adt.ADTNode;
+import de.learnlib.algorithm.adt.automaton.ADTState;
+import de.learnlib.algorithm.adt.util.ADTUtil;
+import de.learnlib.query.AdaptiveQuery;
+
+/**
+ * Utility class to share common implementations.
+ *
+ * @param
+ * input symbol type
+ * @param
+ * output symbol type
+ */
+abstract class AbstractAdaptiveQuery implements AdaptiveQuery {
+
+ protected ADTNode, I, O> currentADTNode;
+ private O tempOut;
+
+ AbstractAdaptiveQuery(ADTNode, I, O> currentADTNode) {
+ this.currentADTNode = currentADTNode;
+ }
+
+ @Override
+ public Response processOutput(O out) {
+
+ final ADTNode, I, O> succ = currentADTNode.getChild(out);
+
+ if (succ == null) {
+ this.tempOut = out;
+ return Response.FINISHED;
+ } else if (ADTUtil.isResetNode(succ)) {
+ this.currentADTNode = succ.getChild(null);
+ resetProgress();
+ return Response.RESET;
+ } else if (ADTUtil.isSymbolNode(succ)) {
+ this.currentADTNode = succ;
+ return Response.SYMBOL;
+ } else {
+ this.currentADTNode = succ;
+ return Response.FINISHED;
+ }
+ }
+
+ protected abstract void resetProgress();
+
+ boolean needsPostProcessing() {
+ return this.tempOut != null;
+ }
+
+ ADTNode, I, O> getCurrentADTNode() {
+ return currentADTNode;
+ }
+
+ O getTempOut() {
+ return tempOut;
+ }
+}
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/Adaptive2MembershipWrapper.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/Adaptive2MembershipWrapper.java
new file mode 100644
index 0000000000..d9367385d6
--- /dev/null
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/Adaptive2MembershipWrapper.java
@@ -0,0 +1,59 @@
+/* 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.ArrayList;
+import java.util.Collection;
+
+import de.learnlib.oracle.AdaptiveMembershipOracle;
+import de.learnlib.oracle.MembershipOracle.MealyMembershipOracle;
+import de.learnlib.query.AdaptiveQuery;
+import de.learnlib.query.Query;
+import de.learnlib.util.mealy.PresetAdaptiveQuery;
+import net.automatalib.word.Word;
+
+/**
+ * Utility class to answer regular {@link Query queries} with an {@link AdaptiveMembershipOracle}.
+ *
+ * @param
+ * input symbol type
+ * @param
+ * output symbol type
+ */
+class Adaptive2MembershipWrapper implements MealyMembershipOracle {
+
+ private final AdaptiveMembershipOracle oracle;
+
+ Adaptive2MembershipWrapper(AdaptiveMembershipOracle oracle) {
+ this.oracle = oracle;
+ }
+
+ @Override
+ public void processQueries(Collection extends Query>> queries) {
+
+ Collection> adaptiveQueries = new ArrayList<>();
+
+ for (Query> query : queries) {
+ if (query.getSuffix().isEmpty()) {
+ query.answer(Word.epsilon());
+ } else {
+ adaptiveQueries.add(new PresetAdaptiveQuery<>(query));
+ }
+ }
+
+ this.oracle.processQueries(adaptiveQueries);
+ }
+}
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/model/ObservationTree.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/model/ObservationTree.java
index 1005672e1e..c9b5566f29 100644
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/model/ObservationTree.java
+++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/model/ObservationTree.java
@@ -17,18 +17,19 @@
import java.util.Collection;
import java.util.HashMap;
-import java.util.Iterator;
import java.util.Map;
-import java.util.Objects;
import java.util.Optional;
import java.util.function.Function;
import de.learnlib.algorithm.LearningAlgorithm;
import de.learnlib.algorithm.adt.adt.ADTNode;
import de.learnlib.algorithm.adt.util.ADTUtil;
+import de.learnlib.filter.cache.mealy.AdaptiveQueryCache;
+import de.learnlib.oracle.AdaptiveMembershipOracle;
+import de.learnlib.query.AdaptiveQuery;
import net.automatalib.alphabet.Alphabet;
-import net.automatalib.automaton.transducer.impl.FastMealy;
-import net.automatalib.automaton.transducer.impl.FastMealyState;
+import net.automatalib.alphabet.SupportsGrowingAlphabet;
+import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.util.Pair;
import net.automatalib.util.automaton.equivalence.NearLinearEquivalenceTest;
import net.automatalib.word.Word;
@@ -46,24 +47,29 @@
* @param
* output alphabet type
*/
-public class ObservationTree {
+public class ObservationTree implements AdaptiveMembershipOracle, SupportsGrowingAlphabet {
private final Alphabet alphabet;
- private final FastMealy observationTree;
+ private final AdaptiveMembershipOracle delegate;
- private final Map> nodeToObservationMap;
+ private final AdaptiveQueryCache cache;
+
+ private final Map nodeToObservationMap;
+
+ public ObservationTree(Alphabet alphabet, AdaptiveMembershipOracle delegate, boolean useCache) {
+ this.cache = new AdaptiveQueryCache<>(delegate, alphabet);
+
+ if (useCache) {
+ this.delegate = this.cache;
+ } else {
+ this.delegate = delegate;
+ }
- public ObservationTree(Alphabet alphabet) {
this.alphabet = alphabet;
- this.observationTree = new FastMealy<>(alphabet);
this.nodeToObservationMap = new HashMap<>();
}
- public FastMealy getObservationTree() {
- return observationTree;
- }
-
/**
* Initialize the observation tree with initial hypothesis state. Usually used during {@link
* LearningAlgorithm#startLearning()}
@@ -72,7 +78,7 @@ public FastMealy getObservationTree() {
* the initial state of the hypothesis
*/
public void initialize(S state) {
- final FastMealyState init = this.observationTree.addInitialState();
+ final Integer init = this.cache.getCache().getInitialState();
this.nodeToObservationMap.put(state, init);
}
@@ -89,11 +95,11 @@ public void initialize(S state) {
public void initialize(Collection states,
Function> asFunction,
Function, Word> outputFunction) {
- final FastMealyState init = this.observationTree.addInitialState();
+ final Integer init = this.cache.getCache().getInitialState();
for (S s : states) {
final Word as = asFunction.apply(s);
- final FastMealyState treeNode = this.addTrace(init, as, outputFunction.apply(as));
+ final Integer treeNode = this.addTrace(init, as, outputFunction.apply(as));
this.nodeToObservationMap.put(s, treeNode);
}
}
@@ -112,32 +118,8 @@ public void addTrace(S state, Word input, Word output) {
this.addTrace(this.nodeToObservationMap.get(state), input, output);
}
- private FastMealyState addTrace(FastMealyState state, Word input, Word output) {
-
- assert input.length() == output.length() : "Traces differ in length";
-
- final Iterator inputIter = input.iterator();
- final Iterator outputIter = output.iterator();
- FastMealyState iter = state;
-
- while (inputIter.hasNext()) {
-
- final I nextInput = inputIter.next();
- final O nextOuput = outputIter.next();
- final FastMealyState nextState;
-
- if (this.observationTree.getTransition(iter, nextInput) == null) {
- nextState = this.observationTree.addState();
- this.observationTree.addTransition(iter, nextInput, nextState, nextOuput);
- } else {
- assert Objects.equals(nextOuput, this.observationTree.getOutput(iter, nextInput)) : "Inconsistent observations";
- nextState = this.observationTree.getSuccessor(iter, nextInput);
- }
-
- iter = nextState;
- }
-
- return iter;
+ private Integer addTrace(Integer state, Word input, Word output) {
+ return this.cache.insert(state, input, output);
}
/**
@@ -151,7 +133,7 @@ private FastMealyState addTrace(FastMealyState state, Word input, Word<
*/
public void addTrace(S state, ADTNode adtNode) {
- final FastMealyState internalState = this.nodeToObservationMap.get(state);
+ final Integer internalState = this.nodeToObservationMap.get(state);
ADTNode adsIter = adtNode;
@@ -179,17 +161,8 @@ public void addState(S newState, Word accessSequence, O output) {
final Word prefix = accessSequence.prefix(accessSequence.length() - 1);
final I sym = accessSequence.lastSymbol();
- final FastMealyState pred =
- this.observationTree.getSuccessor(this.observationTree.getInitialState(), prefix);
- final FastMealyState target;
-
- assert pred != null;
- if (pred.getTransitionObject(alphabet.getSymbolIndex(sym)) == null) {
- target = this.observationTree.addState();
- this.observationTree.addTransition(pred, sym, target, output);
- } else {
- target = this.observationTree.getSuccessor(pred, sym);
- }
+ final Integer pred = this.cache.getCache().getState(prefix);
+ final Integer target = this.cache.insert(pred, Word.fromLetter(sym), Word.fromLetter(output));
this.nodeToObservationMap.put(newState, target);
}
@@ -209,15 +182,16 @@ public void addState(S newState, Word accessSequence, O output) {
*/
public Optional> findSeparatingWord(S s1, S s2, Word prefix) {
- final FastMealyState n1 = this.nodeToObservationMap.get(s1);
- final FastMealyState n2 = this.nodeToObservationMap.get(s2);
+ final MealyMachine cache = this.cache.getCache();
+
+ final Integer n1 = this.nodeToObservationMap.get(s1);
+ final Integer n2 = this.nodeToObservationMap.get(s2);
- final FastMealyState s1Succ = this.observationTree.getSuccessor(n1, prefix);
- final FastMealyState s2Succ = this.observationTree.getSuccessor(n2, prefix);
+ final Integer s1Succ = cache.getSuccessor(n1, prefix);
+ final Integer s2Succ = cache.getSuccessor(n2, prefix);
if (s1Succ != null && s2Succ != null) {
- final Word sepWord =
- NearLinearEquivalenceTest.findSeparatingWord(this.observationTree, s1Succ, s2Succ, alphabet, true);
+ final Word sepWord = NearLinearEquivalenceTest.findSeparatingWord(cache, s1Succ, s2Succ, alphabet, true);
if (sepWord != null) {
return Optional.of(sepWord);
@@ -239,10 +213,10 @@ public Optional> findSeparatingWord(S s1, S s2, Word prefix) {
*/
public Word findSeparatingWord(S s1, S s2) {
- final FastMealyState n1 = this.nodeToObservationMap.get(s1);
- final FastMealyState n2 = this.nodeToObservationMap.get(s2);
+ final Integer n1 = this.nodeToObservationMap.get(s1);
+ final Integer n2 = this.nodeToObservationMap.get(s2);
- return NearLinearEquivalenceTest.findSeparatingWord(this.observationTree, n1, n2, this.alphabet, true);
+ return NearLinearEquivalenceTest.findSeparatingWord(this.cache.getCache(), n1, n2, this.alphabet, true);
}
/**
@@ -257,8 +231,18 @@ public Word findSeparatingWord(S s1, S s2) {
* @return the previously stored output behavior of the system under learning
*/
public Word trace(S s, Word input) {
- final FastMealyState q = this.nodeToObservationMap.get(s);
- return this.observationTree.computeStateOutput(q, input);
+ final Integer q = this.nodeToObservationMap.get(s);
+ return this.cache.getCache().computeStateOutput(q, input);
}
+ @Override
+ public void processQueries(Collection extends AdaptiveQuery> queries) {
+ this.delegate.processQueries(queries);
+ }
+
+ @Override
+ public void addAlphabetSymbol(I i) {
+ this.alphabet.asGrowingAlphabetOrThrowException().add(i);
+ this.cache.addAlphabetSymbol(i);
+ }
}
diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/SQOOTBridge.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/SQOOTBridge.java
deleted file mode 100644
index bfbe2a3488..0000000000
--- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/SQOOTBridge.java
+++ /dev/null
@@ -1,120 +0,0 @@
-/* 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.util;
-
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.List;
-import java.util.Objects;
-
-import de.learnlib.algorithm.adt.model.ObservationTree;
-import de.learnlib.oracle.SymbolQueryOracle;
-import net.automatalib.automaton.transducer.impl.FastMealy;
-import net.automatalib.automaton.transducer.impl.FastMealyState;
-
-/**
- * A utility class that links an observation tree with a symbol query oracle, meaning that all queries to the symbol
- * query oracle will be stored in the observation tree. Additionally, if a query can be answered by the observation tree
- * (and caching is enabled) the delegated symbol query oracle will not be queried.
- *
- * @param
- * input alphabet type
- * @param