From 61a188b76d430a3e0a33bb34cb76d5182068236c Mon Sep 17 00:00:00 2001 From: Markus Frohme Date: Mon, 13 Jan 2025 21:13:17 +0100 Subject: [PATCH] cleanup some ADT code --- .../de/learnlib/algorithm/adt/adt/ADT.java | 26 ++- .../algorithm/adt/adt/ADTResetNode.java | 10 +- .../algorithm/adt/config/LeafSplitters.java | 6 +- .../model/replacer/ExhaustiveReplacer.java | 3 +- .../model/replacer/LevelOrderReplacer.java | 4 +- .../config/model/replacer/SingleReplacer.java | 14 +- .../algorithm/adt/learner/ADTLearner.java | 77 +++++---- .../algorithm/adt/model/ObservationTree.java | 31 ++-- .../learnlib/algorithm/adt/util/ADTUtil.java | 161 ++++++------------ .../cache/mealy/AdaptiveQueryCache.java | 11 ++ 10 files changed, 160 insertions(+), 183 deletions(-) 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 ac481f96d..9890e31f5 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 @@ -73,6 +73,7 @@ public void replaceNode(ADTNode oldNode, ADTNode newNode) { this.root = newNode; } else if (ADTUtil.isResetNode(oldNode)) { final ADTNode endOfPreviousADS = oldNode.getParent(); + assert endOfPreviousADS != null; final O outputToReset = ADTUtil.getOutputForSuccessor(endOfPreviousADS, oldNode); newNode.setParent(endOfPreviousADS); @@ -83,6 +84,8 @@ public void replaceNode(ADTNode oldNode, ADTNode newNode) { assert ADTUtil.isResetNode(oldNodeParent); final ADTNode endOfPreviousADS = oldNodeParent.getParent(); + assert endOfPreviousADS != null; + final O outputToReset = ADTUtil.getOutputForSuccessor(endOfPreviousADS, oldNodeParent); final ADTNode newResetNode = new ADTResetNode<>(newNode); @@ -191,30 +194,35 @@ public LCAInfo findLCA(ADTNode s1, ADTNode s2) { final Map, ADTNode> s1ParentsToS1 = new HashMap<>(); ADTNode s1Iter = s1; - ADTNode s2Iter = s2; + ADTNode s1ParentIter = s1.getParent(); - while (s1Iter.getParent() != null) { - s1ParentsToS1.put(s1Iter.getParent(), s1Iter); - s1Iter = s1Iter.getParent(); + while (s1ParentIter != null) { + s1ParentsToS1.put(s1ParentIter, s1Iter); + s1Iter = s1ParentIter; + s1ParentIter = s1ParentIter.getParent(); } final Set> s1Parents = s1ParentsToS1.keySet(); - while (s2Iter.getParent() != null) { + ADTNode s2Iter = s2; + ADTNode s2ParentIter = s2.getParent(); + + while (s2ParentIter != null) { - if (s1Parents.contains(s2Iter.getParent())) { - if (!ADTUtil.isSymbolNode(s2Iter.getParent())) { + if (s1Parents.contains(s2ParentIter)) { + if (!ADTUtil.isSymbolNode(s2ParentIter)) { throw new IllegalStateException("Only Symbol Nodes should be LCAs"); } - final ADTNode lca = s2Iter.getParent(); + final ADTNode lca = s2ParentIter; final O s1Out = ADTUtil.getOutputForSuccessor(lca, s1ParentsToS1.get(lca)); final O s2Out = ADTUtil.getOutputForSuccessor(lca, s2Iter); return new LCAInfo<>(lca, s1Out, s2Out); } - s2Iter = s2Iter.getParent(); + s2Iter = s2ParentIter; + s2ParentIter = s2ParentIter.getParent(); } throw new IllegalStateException("Nodes do not share a parent node"); 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 faf44ef37..496b35d21 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 org.checkerframework.checker.nullness.qual.Nullable; - /** * Reset node implementation. * @@ -40,8 +38,8 @@ public ADTResetNode(ADTNode successor) { } @Override - public @Nullable I getSymbol() { - return null; + public I getSymbol() { + throw new UnsupportedOperationException("Reset nodes do not have a symbol"); } @Override @@ -65,8 +63,8 @@ public Map> getChildren() { } @Override - public @Nullable S getState() { - return null; + public S getState() { + throw new UnsupportedOperationException("Reset nodes cannot reference a hypothesis state"); } @Override 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 c49fa92a6..b0d71b73f 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 @@ -162,9 +162,11 @@ public static ADTNode splitParent(ADTNode nodeToSpli adsIter = adsIter.getChild(newSuffixOutput); } - final ADTNode continuedADS = new ADTSymbolNode<>(adsIter.getParent(), suffixIter.next()); + final ADTNode parent = adsIter.getParent(); + final ADTNode continuedADS = new ADTSymbolNode<>(parent, suffixIter.next()); - adsIter.getParent().getChildren().put(newSuffixOutput, continuedADS); + assert parent != null; + parent.getChildren().put(newSuffixOutput, continuedADS); return finalizeSplit(nodeToSplit, continuedADS, suffixIter, oldIter, newIter); } diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/ExhaustiveReplacer.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/ExhaustiveReplacer.java index 89ba53459..cc37baf79 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/ExhaustiveReplacer.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/ExhaustiveReplacer.java @@ -57,8 +57,7 @@ public Set> computeReplacements(MealyMachin return Collections.singleton(new ReplacementResult<>(adt.getRoot(), potentialResult.get())); } - final Set> candidates = ADTUtil.collectADSNodes(adt.getRoot()); - candidates.remove(adt.getRoot()); + final Set> candidates = ADTUtil.collectADSNodes(adt.getRoot(), false); final PriorityQueue> queue = new PriorityQueue<>(candidates.size(), Comparator.comparingInt(Set::size)); for (ADTNode node : candidates) { diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/LevelOrderReplacer.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/LevelOrderReplacer.java index d1b7ea7fe..1dcaccd90 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/LevelOrderReplacer.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/LevelOrderReplacer.java @@ -30,6 +30,7 @@ import de.learnlib.algorithm.adt.util.ADTUtil; import net.automatalib.alphabet.Alphabet; import net.automatalib.automaton.transducer.MealyMachine; +import org.checkerframework.checker.nullness.qual.NonNull; public class LevelOrderReplacer implements SubtreeReplacer { @@ -55,7 +56,8 @@ public Set> computeReplacements(MealyMachin queue.add(adt.getRoot()); while (!queue.isEmpty()) { - final ADTNode node = queue.poll(); + @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399 + final @NonNull ADTNode node = queue.poll(); final Set targetStates = ADTUtil.collectHypothesisStates(node); // try to extendLeaf the parent ADS diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/SingleReplacer.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/SingleReplacer.java index 64cde63ca..4f685f471 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/SingleReplacer.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/SingleReplacer.java @@ -50,8 +50,7 @@ public Set> computeReplacements(MealyMachin Alphabet inputs, ADT adt) { - final Set> candidates = ADTUtil.collectADSNodes(adt.getRoot()); - candidates.remove(adt.getRoot()); + final Set> candidates = ADTUtil.collectADSNodes(adt.getRoot(), false); // cache scores to prevent expensive recalculations during sorting final List, Double>> sortedCandidates = new ArrayList<>(candidates.size()); @@ -111,12 +110,11 @@ public Set> computeReplacements(MealyMachin * * @return a ReplacementResult for the parent (reset) node, if a valid replacement is found. {@code null} otherwise. */ - @Nullable - static ReplacementResult computeParentExtension(MealyMachine hypothesis, - Alphabet inputs, - ADTNode node, - Set targetStates, - ADSCalculator adsCalculator) { + static @Nullable ReplacementResult computeParentExtension(MealyMachine hypothesis, + Alphabet inputs, + ADTNode node, + Set targetStates, + ADSCalculator adsCalculator) { final ADTNode parentReset = node.getParent(); assert ADTUtil.isResetNode(parentReset) : "should not happen"; 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 f88f0a0d8..d5cfd2892 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 @@ -26,10 +26,8 @@ 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; -import java.util.stream.Collectors; import de.learnlib.Resumable; import de.learnlib.algorithm.LearningAlgorithm; @@ -65,6 +63,7 @@ import net.automatalib.common.util.HashUtil; import net.automatalib.common.util.Pair; import net.automatalib.word.Word; +import org.checkerframework.checker.nullness.qual.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -159,7 +158,9 @@ public boolean refineHypothesis(DefaultQuery> ce) { // normal refinement step while (!this.openCounterExamples.isEmpty()) { - final DefaultQuery> currentCE = this.openCounterExamples.poll(); + @SuppressWarnings("nullness") + // false positive https://github.com/typetools/checker-framework/issues/399 + final @NonNull DefaultQuery> currentCE = this.openCounterExamples.poll(); this.allCounterExamples.add(currentCE); while (this.refineHypothesisInternal(currentCE)) { @@ -219,12 +220,7 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { oldTrans.setTarget(newState); oldTrans.setIsSpanningTreeEdge(true); - final Set, I, O>> finalNodes = ADTUtil.collectLeaves(this.adt.getRoot()); - final ADTNode, I, O> nodeToSplit = finalNodes.stream() - .filter(n -> uaState.equals(n.getState())) - .findFirst() - .orElseThrow(IllegalStateException::new); - + final ADTNode, I, O> nodeToSplit = findNodeForState(uaState); final ADTNode, I, O> newNode; // directly insert into observation tree, because we use it for finding a splitter @@ -232,15 +228,9 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { this.observationTree.addTrace(newState, nodeToSplit); final Word previousTrace = ADTUtil.buildTraceForNode(nodeToSplit).getFirst(); - final Optional> extension = this.observationTree.findSeparatingWord(uaState, newState, previousTrace); - - if (extension.isPresent()) { - final Word completeSplitter = previousTrace.concat(extension.get()); - final Word oldOutput = this.observationTree.trace(uaState, completeSplitter); - final Word newOutput = this.observationTree.trace(newState, completeSplitter); + final Word extension = this.observationTree.findSeparatingWord(uaState, newState, previousTrace); - newNode = this.adt.extendLeaf(nodeToSplit, completeSplitter, oldOutput, newOutput, this.leafSplitter); - } else { + if (extension == null) { // directly insert into observation tree, because we use it for finding a splitter this.observationTree.addTrace(uaState, v, this.mqo.answerQuery(uaAccessSequence, v)); this.observationTree.addTrace(newState, v, this.mqo.answerQuery(uAccessSequenceWithA, v)); @@ -248,6 +238,7 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { // in doubt, we will always find v final Word otSepWord = this.observationTree.findSeparatingWord(uaState, newState); final Word splitter; + assert otSepWord != null; if (otSepWord.length() < v.length()) { splitter = otSepWord; @@ -259,6 +250,12 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { final Word newOutput = this.observationTree.trace(newState, splitter); newNode = this.adt.splitLeaf(nodeToSplit, splitter, oldOutput, newOutput, this.leafSplitter); + } else { + final Word completeSplitter = previousTrace.concat(extension); + final Word oldOutput = this.observationTree.trace(uaState, completeSplitter); + final Word newOutput = this.observationTree.trace(newState, completeSplitter); + + newNode = this.adt.extendLeaf(nodeToSplit, completeSplitter, oldOutput, newOutput, this.leafSplitter); } newNode.setState(newState); @@ -269,11 +266,7 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { newTransitions.add(this.hypothesis.createOpenTransition(newState, i, this.adt.getRoot())); } - final List> transitionsToRefine = nodeToSplit.getState() - .getIncomingTransitions() - .stream() - .filter(x -> !x.isSpanningTreeEdge()) - .collect(Collectors.toList()); + final List> transitionsToRefine = getIncomingNonSpanningTreeTransitions(uaState); for (ADTTransition x : transitionsToRefine) { x.setTarget(null); @@ -299,6 +292,18 @@ public boolean refineHypothesisInternal(DefaultQuery> ceQuery) { return true; } + private ADTNode, I, O> findNodeForState(ADTState state) { + + for (ADTNode, I, O> leaf : ADTUtil.collectLeaves(this.adt.getRoot())) { + if (leaf.getState().equals(state)) { + return leaf; + } + } + + throw new IllegalStateException("Cannot find leaf for state " + state); + + } + @Override public MealyMachine getHypothesisModel() { return this.hypothesis; @@ -503,7 +508,8 @@ private ADTNode, I, O> evaluateAdtExtension(ADTNode, I, O> extension = potentialExtension.getReplacement(); final ADTNode, I, O> nodeToReplace = ads.getParent(); // reset node - assert this.validateADS(nodeToReplace, extension, Collections.emptySet()); + assert extension != null && nodeToReplace != null && + this.validateADS(nodeToReplace, extension, Collections.emptySet()); final ADTNode, I, O> replacement = this.verifyADS(nodeToReplace, extension, @@ -602,7 +608,7 @@ private boolean validateADS(ADTNode, I, O> oldADS, if (ADTUtil.isResetNode(oldADS)) { oldNodes = ADTUtil.collectResetNodes(this.adt.getRoot()); } else { - oldNodes = ADTUtil.collectADSNodes(this.adt.getRoot()); + oldNodes = ADTUtil.collectADSNodes(this.adt.getRoot(), true); } if (!oldNodes.contains(oldADS)) { @@ -755,7 +761,6 @@ private void resolveAmbiguities(ADTNode, I, O> nodeToReplace, for (ADTNode, I, O> leaf : cachedLeaves) { final ADTState hypState = leaf.getState(); - assert hypState != null; if (hypState.equals(finalNode.getState())) { oldReference = leaf; @@ -768,6 +773,7 @@ private void resolveAmbiguities(ADTNode, I, O> nodeToReplace, } } + assert oldReference != null && newReference != null; final LCAInfo, I, O> lcaResult = this.adt.findLCA(oldReference, newReference); final ADTNode, I, O> lca = lcaResult.adtNode; final Pair, Word> lcaTrace = ADTUtil.buildTraceForNode(lca); @@ -807,13 +813,7 @@ private void resiftAffectedTransitions(Set, I, O>> states for (ADTNode, I, O> state : states) { - final List> transitionsToRefine = state.getState() - .getIncomingTransitions() - .stream() - .filter(x -> !x.isSpanningTreeEdge()) - .collect(Collectors.toList()); - - for (ADTTransition trans : transitionsToRefine) { + for (ADTTransition trans : getIncomingNonSpanningTreeTransitions(state.getState())) { trans.setTarget(null); trans.setSiftNode(finalizedADS); this.openTransitions.add(trans); @@ -821,6 +821,19 @@ private void resiftAffectedTransitions(Set, I, O>> states } } + private List> getIncomingNonSpanningTreeTransitions(ADTState state) { + final Set> transitions = state.getIncomingTransitions(); + final List> result = new ArrayList<>(transitions.size()); + + for (ADTTransition t : transitions) { + if (!t.isSpanningTreeEdge()) { + result.add(t); + } + } + + return result; + } + public ADT, I, O> getADT() { return adt; } 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 8a02dd498..7caf149a3 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 @@ -18,7 +18,6 @@ import java.util.Collection; import java.util.HashMap; import java.util.Map; -import java.util.Optional; import java.util.function.Function; import de.learnlib.algorithm.LearningAlgorithm; @@ -33,6 +32,7 @@ import net.automatalib.common.util.Pair; import net.automatalib.util.automaton.equivalence.NearLinearEquivalenceTest; import net.automatalib.word.Word; +import org.checkerframework.checker.nullness.qual.Nullable; /** * A class, that stores observations of the system under learning in a tree-like structure. Can be used to
  • @@ -54,11 +54,13 @@ public class ObservationTree implements AdaptiveMembershipOracle, private final AdaptiveMembershipOracle delegate; private final AdaptiveQueryCache cache; + private final Integer init; private final Map nodeToObservationMap; public ObservationTree(Alphabet alphabet, AdaptiveMembershipOracle delegate, boolean useCache) { this.cache = new AdaptiveQueryCache<>(delegate, alphabet); + this.init = this.cache.getInit(); if (useCache) { this.delegate = this.cache; @@ -71,15 +73,14 @@ public ObservationTree(Alphabet alphabet, AdaptiveMembershipOracle dele } /** - * Initialize the observation tree with initial hypothesis state. Usually used during {@link - * LearningAlgorithm#startLearning()} + * Initialize the observation tree with initial hypothesis state. Usually used during + * {@link LearningAlgorithm#startLearning()} * * @param state * the initial state of the hypothesis */ public void initialize(S state) { - final Integer init = this.cache.getCache().getInitialState(); - this.nodeToObservationMap.put(state, init); + this.nodeToObservationMap.put(state, this.init); } /** @@ -95,11 +96,9 @@ public void initialize(S state) { public void initialize(Collection states, Function> asFunction, Function, Word> outputFunction) { - final Integer init = this.cache.getCache().getInitialState(); - for (S s : states) { final Word as = asFunction.apply(s); - final Integer treeNode = this.addTrace(init, as, outputFunction.apply(as)); + final Integer treeNode = this.addTrace(this.init, as, outputFunction.apply(as)); this.nodeToObservationMap.put(s, treeNode); } } @@ -177,10 +176,10 @@ public void addState(S newState, Word accessSequence, O output) { * @param prefix * input sequence * - * @return A {@link Word} separating the two states reached after applying the prefix to s1 and s2. {@code - * Optional.empty()} if not separating word exists. + * @return A {@link Word} separating the two states reached after applying the prefix to s1 and s2, or {@code null} + * if no separating word exists. */ - public Optional> findSeparatingWord(S s1, S s2, Word prefix) { + public @Nullable Word findSeparatingWord(S s1, S s2, Word prefix) { final MealyMachine cache = this.cache.getCache(); @@ -191,14 +190,10 @@ public Optional> findSeparatingWord(S s1, S s2, Word prefix) { final Integer s2Succ = cache.getSuccessor(n2, prefix); if (s1Succ != null && s2Succ != null) { - final Word sepWord = NearLinearEquivalenceTest.findSeparatingWord(cache, s1Succ, s2Succ, alphabet, true); - - if (sepWord != null) { - return Optional.of(sepWord); - } + return NearLinearEquivalenceTest.findSeparatingWord(cache, s1Succ, s2Succ, alphabet, true); } - return Optional.empty(); + return null; } /** @@ -211,7 +206,7 @@ public Optional> findSeparatingWord(S s1, S s2, Word prefix) { * * @return A {@link Word} separating the two words. {@code null} if no such word is found. */ - public Word findSeparatingWord(S s1, S s2) { + public @Nullable Word findSeparatingWord(S s1, S s2) { final Integer n1 = this.nodeToObservationMap.get(s1); final Integer n2 = this.nodeToObservationMap.get(s2); diff --git a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/ADTUtil.java b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/ADTUtil.java index 20c8e6801..d3d51b12f 100644 --- a/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/ADTUtil.java +++ b/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/util/ADTUtil.java @@ -20,16 +20,18 @@ import java.util.Map; import java.util.Objects; import java.util.Set; -import java.util.function.Function; +import java.util.function.Predicate; import de.learnlib.algorithm.adt.adt.ADTLeafNode; import de.learnlib.algorithm.adt.adt.ADTNode; +import de.learnlib.algorithm.adt.adt.ADTNode.NodeType; import de.learnlib.algorithm.adt.adt.ADTSymbolNode; import net.automatalib.automaton.transducer.MealyMachine; import net.automatalib.common.util.Pair; import net.automatalib.graph.ads.ADSNode; +import net.automatalib.util.automaton.ads.ADSUtil; import net.automatalib.word.Word; -import net.automatalib.word.WordBuilder; +import org.checkerframework.checker.nullness.qual.Nullable; /** * Utility class, that offers some operations revolving around adaptive distinguishing sequences. @@ -40,84 +42,92 @@ private ADTUtil() { // prevent instantiation } - public static boolean isSymbolNode(ADTNode node) { + public static boolean isLeafNode(@Nullable ADTNode node) { + return checkNodeType(node, ADTNode.NodeType.LEAF_NODE); + } + + public static boolean isResetNode(@Nullable ADTNode node) { + return checkNodeType(node, ADTNode.NodeType.RESET_NODE); + } + + public static boolean isSymbolNode(@Nullable ADTNode node) { return checkNodeType(node, ADTNode.NodeType.SYMBOL_NODE); } - private static boolean checkNodeType(ADTNode node, ADTNode.NodeType type) { + private static boolean checkNodeType(@Nullable ADTNode node, ADTNode.NodeType type) { return node != null && node.getNodeType() == type; } public static ADTNode getStartOfADS(ADTNode node) { - ADTNode iter = node; + ADTNode result = node; + ADTNode iter = node.getParent(); - while (iter.getParent() != null && !ADTUtil.isResetNode(iter.getParent())) { + while (iter != null && !ADTUtil.isResetNode(iter)) { + result = iter; iter = iter.getParent(); } - return iter; - } - - public static boolean isResetNode(ADTNode node) { - return checkNodeType(node, ADTNode.NodeType.RESET_NODE); - } - - public static Set collectHypothesisStates(ADTNode root) { - final Set result = new LinkedHashSet<>(); - collectTransformedLeavesRecursively(result, root, ADTNode::getState); return result; } - public static Set> collectLeaves(ADTNode root) { - final Set> result = new LinkedHashSet<>(); - collectTransformedLeavesRecursively(result, root, Function.identity()); + public static Set collectHypothesisStates(ADTNode root) { + final Set result = new LinkedHashSet<>(); + collectHypothesisStatesRecursively(result, root); return result; } - private static void collectTransformedLeavesRecursively(Set nodes, - ADTNode current, - Function, T> transformer) { + private static void collectHypothesisStatesRecursively(Set nodes, ADTNode current) { if (ADTUtil.isLeafNode(current)) { - nodes.add(transformer.apply(current)); + nodes.add(current.getState()); } else { - for (ADTNode n : current.getChildren().values()) { - collectTransformedLeavesRecursively(nodes, n, transformer); + for (ADTNode n : current.getChildren().values()) { + collectHypothesisStatesRecursively(nodes, n); } } } - public static Set> collectADSNodes(ADTNode root) { + public static Set> collectLeaves(ADTNode root) { final Set> result = new LinkedHashSet<>(); - result.add(root); - collectADSNodesRecursively(result, root); + collectNodesRecursively(result, root, NodeType.LEAF_NODE); return result; } - private static void collectADSNodesRecursively(Set> nodes, - ADTNode current) { - if (ADTUtil.isResetNode(current)) { - nodes.addAll(current.getChildren().values()); + public static Set> collectResetNodes(ADTNode root) { + final Set> result = new LinkedHashSet<>(); + collectNodesRecursively(result, root, NodeType.RESET_NODE); + return result; + } + + private static void collectNodesRecursively(Set> nodes, + ADTNode current, + NodeType type) { + if (current.getNodeType() == type) { + nodes.add(current); } for (ADTNode n : current.getChildren().values()) { - collectADSNodesRecursively(nodes, n); + collectNodesRecursively(nodes, n, type); } } - public static Set> collectResetNodes(ADTNode root) { + public static Set> collectADSNodes(ADTNode root, boolean includeRoot) { final Set> result = new LinkedHashSet<>(); - collectResetNodesRecursively(result, root); + if (includeRoot) { + result.add(root); + } + collectADSNodesRecursively(result, root); return result; } - private static void collectResetNodesRecursively(Set> nodes, ADTNode current) { + private static void collectADSNodesRecursively(Set> nodes, + ADTNode current) { if (ADTUtil.isResetNode(current)) { - nodes.add(current); + nodes.addAll(current.getChildren().values()); } for (ADTNode n : current.getChildren().values()) { - collectResetNodesRecursively(nodes, n); + collectADSNodesRecursively(nodes, n); } } @@ -125,7 +135,6 @@ public static Set> collectDirectSubADSs(ADTNode> result = new LinkedHashSet<>(); collectDirectSubTreesRecursively(result, node); return result; - } private static void collectDirectSubTreesRecursively(Set> nodes, @@ -140,36 +149,12 @@ private static void collectDirectSubTreesRecursively(Set Pair, Word> buildTraceForNode(ADTNode node) { - - ADTNode parentIter = node.getParent(); - ADTNode nodeIter = node; - final WordBuilder inputBuilder = new WordBuilder<>(); - final WordBuilder outputBuilder = new WordBuilder<>(); - - while (parentIter != null && !ADTUtil.isResetNode(parentIter)) { - inputBuilder.append(parentIter.getSymbol()); - outputBuilder.append(ADTUtil.getOutputForSuccessor(parentIter, nodeIter)); - - nodeIter = parentIter; - parentIter = parentIter.getParent(); - } - - return Pair.of(inputBuilder.reverse().toWord(), outputBuilder.reverse().toWord()); + final Predicate> predicate = ADTUtil::isResetNode; + return ADSUtil.buildTraceForNode(node, predicate.negate()); } public static O getOutputForSuccessor(ADTNode node, ADTNode successor) { - - if (!node.equals(successor.getParent())) { - throw new IllegalArgumentException("No parent relationship"); - } - - for (Map.Entry> entry : node.getChildren().entrySet()) { - if (entry.getValue().equals(successor)) { - return entry.getKey(); - } - } - - throw new IllegalArgumentException("No child relationship"); + return ADSUtil.getOutputForSuccessor(node, successor); } /** @@ -212,20 +197,14 @@ public static ADTNode buildFromADS(ADSNode node) { * * @param adt * the node whose subtree should be analyzed - * @param - * (hypothesis) state type - * @param - * input alphabet type - * @param - * output alphabet type * * @return the number of encountered reset nodes */ - public static int computeEffectiveResets(ADTNode adt) { + public static int computeEffectiveResets(ADTNode adt) { return computeEffectiveResetsInternal(adt, 0); } - private static int computeEffectiveResetsInternal(ADTNode ads, int accumulatedResets) { + private static int computeEffectiveResetsInternal(ADTNode ads, int accumulatedResets) { if (ADTUtil.isLeafNode(ads)) { return accumulatedResets; } @@ -234,7 +213,7 @@ private static int computeEffectiveResetsInternal(ADTNode ads int resets = 0; - for (ADTNode value : ads.getChildren().values()) { + for (ADTNode value : ads.getChildren().values()) { resets += computeEffectiveResetsInternal(value, nextCosts); } @@ -244,29 +223,7 @@ private static int computeEffectiveResetsInternal(ADTNode ads public static Pair, ADTNode> buildADSFromTrace(MealyMachine automaton, Word trace, S state) { - - final Iterator sequenceIter = trace.iterator(); - final I input = sequenceIter.next(); - final ADTNode head = new ADTSymbolNode<>(null, input); - - ADTNode tempADS = head; - I tempInput = input; - S tempState = state; - - while (sequenceIter.hasNext()) { - final I nextInput = sequenceIter.next(); - final ADTNode nextNode = new ADTSymbolNode<>(tempADS, nextInput); - - final O oldOutput = automaton.getOutput(tempState, tempInput); - - tempADS.getChildren().put(oldOutput, nextNode); - - tempADS = nextNode; - tempState = automaton.getSuccessor(tempState, tempInput); - tempInput = nextInput; - } - - return Pair.of(head, tempADS); + return ADSUtil.buildFromTrace(automaton, trace, state, ADTSymbolNode::new); } /** @@ -287,9 +244,7 @@ public static Pair, ADTNode> buildADSFromTra * * @return the root node of the constructed ADS */ - public static ADTNode buildADSFromObservation(Word input, - Word output, - S finalState) { + public static ADTNode buildADSFromObservation(Word input, Word output, S finalState) { if (input.size() != output.size()) { throw new IllegalArgumentException("Arguments differ in length"); @@ -365,8 +320,4 @@ public static boolean mergeADS(ADTNode parent, ADTNode boolean isLeafNode(ADTNode node) { - return checkNodeType(node, ADTNode.NodeType.LEAF_NODE); - } } diff --git a/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java b/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java index e956e6c0a..1c1c94490 100644 --- a/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java +++ b/filters/cache/src/main/java/de/learnlib/filter/cache/mealy/AdaptiveQueryCache.java @@ -172,6 +172,17 @@ public void addAlphabetSymbol(I symbol) { return this.cache; } + /** + * Returns the initial state of the structural view of the cache. + * + * @return the initial state of the cache + * + * @see #getCache() + */ + public Integer getInit() { + return this.init; + } + /** * Inserts the given trace of input symbols and associates the trace of given output symbols with it. *