Skip to content

Commit

Permalink
cleanup some ADT code
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtf90
mtf90 committed Jan 13, 2025
1 parent 2fa3fd0 commit 61a188b
Show file tree
Hide file tree
Showing 10 changed files with 160 additions and 183 deletions.
26 changes: 17 additions & 9 deletions algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADT.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ public void replaceNode(ADTNode<S, I, O> oldNode, ADTNode<S, I, O> newNode) {
this.root = newNode;
} else if (ADTUtil.isResetNode(oldNode)) {
final ADTNode<S, I, O> endOfPreviousADS = oldNode.getParent();
assert endOfPreviousADS != null;
final O outputToReset = ADTUtil.getOutputForSuccessor(endOfPreviousADS, oldNode);

newNode.setParent(endOfPreviousADS);
Expand All @@ -83,6 +84,8 @@ public void replaceNode(ADTNode<S, I, O> oldNode, ADTNode<S, I, O> newNode) {
assert ADTUtil.isResetNode(oldNodeParent);

final ADTNode<S, I, O> endOfPreviousADS = oldNodeParent.getParent();
assert endOfPreviousADS != null;

final O outputToReset = ADTUtil.getOutputForSuccessor(endOfPreviousADS, oldNodeParent);
final ADTNode<S, I, O> newResetNode = new ADTResetNode<>(newNode);

Expand Down Expand Up @@ -191,30 +194,35 @@ public LCAInfo<S, I, O> findLCA(ADTNode<S, I, O> s1, ADTNode<S, I, O> s2) {
final Map<ADTNode<S, I, O>, ADTNode<S, I, O>> s1ParentsToS1 = new HashMap<>();

ADTNode<S, I, O> s1Iter = s1;
ADTNode<S, I, O> s2Iter = s2;
ADTNode<S, I, O> 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<ADTNode<S, I, O>> s1Parents = s1ParentsToS1.keySet();

while (s2Iter.getParent() != null) {
ADTNode<S, I, O> s2Iter = s2;
ADTNode<S, I, O> 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<S, I, O> lca = s2Iter.getParent();
final ADTNode<S, I, O> 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");
Expand Down
10 changes: 4 additions & 6 deletions algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/adt/ADTResetNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,6 @@
import java.util.Collections;
import java.util.Map;

import org.checkerframework.checker.nullness.qual.Nullable;

/**
* Reset node implementation.
*
Expand All @@ -40,8 +38,8 @@ public ADTResetNode(ADTNode<S, I, O> successor) {
}

@Override
public @Nullable I getSymbol() {
return null;
public I getSymbol() {
throw new UnsupportedOperationException("Reset nodes do not have a symbol");
}

@Override
Expand All @@ -65,8 +63,8 @@ public Map<O, ADTNode<S, I, O>> getChildren() {
}

@Override
public @Nullable S getState() {
return null;
public S getState() {
throw new UnsupportedOperationException("Reset nodes cannot reference a hypothesis state");
}

@Override
Expand Down
6 changes: 4 additions & 2 deletions algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/config/LeafSplitters.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,9 +162,11 @@ public static <S, I, O> ADTNode<S, I, O> splitParent(ADTNode<S, I, O> nodeToSpli
adsIter = adsIter.getChild(newSuffixOutput);
}

final ADTNode<S, I, O> continuedADS = new ADTSymbolNode<>(adsIter.getParent(), suffixIter.next());
final ADTNode<S, I, O> parent = adsIter.getParent();
final ADTNode<S, I, O> 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);
}
Expand Down
3 changes: 1 addition & 2 deletions ...adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/ExhaustiveReplacer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,7 @@ public <S, I, O> Set<ReplacementResult<S, I, O>> computeReplacements(MealyMachin
return Collections.singleton(new ReplacementResult<>(adt.getRoot(), potentialResult.get()));
}

final Set<ADTNode<S, I, O>> candidates = ADTUtil.collectADSNodes(adt.getRoot());
candidates.remove(adt.getRoot());
final Set<ADTNode<S, I, O>> candidates = ADTUtil.collectADSNodes(adt.getRoot(), false);

final PriorityQueue<Set<S>> queue = new PriorityQueue<>(candidates.size(), Comparator.comparingInt(Set::size));
for (ADTNode<S, I, O> node : candidates) {
Expand Down
4 changes: 3 additions & 1 deletion ...adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/LevelOrderReplacer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand All @@ -55,7 +56,8 @@ public <S, I, O> Set<ReplacementResult<S, I, O>> computeReplacements(MealyMachin
queue.add(adt.getRoot());

while (!queue.isEmpty()) {
final ADTNode<S, I, O> node = queue.poll();
@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
final @NonNull ADTNode<S, I, O> node = queue.poll();
final Set<S> targetStates = ADTUtil.collectHypothesisStates(node);

// try to extendLeaf the parent ADS
Expand Down
14 changes: 6 additions & 8 deletions ...ive/adt/src/main/java/de/learnlib/algorithm/adt/config/model/replacer/SingleReplacer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,7 @@ public <S, I, O> Set<ReplacementResult<S, I, O>> computeReplacements(MealyMachin
Alphabet<I> inputs,
ADT<S, I, O> adt) {

final Set<ADTNode<S, I, O>> candidates = ADTUtil.collectADSNodes(adt.getRoot());
candidates.remove(adt.getRoot());
final Set<ADTNode<S, I, O>> candidates = ADTUtil.collectADSNodes(adt.getRoot(), false);

// cache scores to prevent expensive recalculations during sorting
final List<Pair<ADTNode<S, I, O>, Double>> sortedCandidates = new ArrayList<>(candidates.size());
Expand Down Expand Up @@ -111,12 +110,11 @@ public <S, I, O> Set<ReplacementResult<S, I, O>> computeReplacements(MealyMachin
*
* @return a ReplacementResult for the parent (reset) node, if a valid replacement is found. {@code null} otherwise.
*/
@Nullable
static <S, I, O> ReplacementResult<S, I, O> computeParentExtension(MealyMachine<S, I, ?, O> hypothesis,
Alphabet<I> inputs,
ADTNode<S, I, O> node,
Set<S> targetStates,
ADSCalculator adsCalculator) {
static <S, I, O> @Nullable ReplacementResult<S, I, O> computeParentExtension(MealyMachine<S, I, ?, O> hypothesis,
Alphabet<I> inputs,
ADTNode<S, I, O> node,
Set<S> targetStates,
ADSCalculator adsCalculator) {
final ADTNode<S, I, O> parentReset = node.getParent();
assert ADTUtil.isResetNode(parentReset) : "should not happen";

Expand Down
77 changes: 45 additions & 32 deletions algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/learner/ADTLearner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -159,7 +158,9 @@ public boolean refineHypothesis(DefaultQuery<I, Word<O>> ce) {
// normal refinement step
while (!this.openCounterExamples.isEmpty()) {

final DefaultQuery<I, Word<O>> currentCE = this.openCounterExamples.poll();
@SuppressWarnings("nullness")
// false positive https://github.com/typetools/checker-framework/issues/399
final @NonNull DefaultQuery<I, Word<O>> currentCE = this.openCounterExamples.poll();
this.allCounterExamples.add(currentCE);

while (this.refineHypothesisInternal(currentCE)) {
Expand Down Expand Up @@ -219,35 +220,25 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
oldTrans.setTarget(newState);
oldTrans.setIsSpanningTreeEdge(true);

final Set<ADTNode<ADTState<I, O>, I, O>> finalNodes = ADTUtil.collectLeaves(this.adt.getRoot());
final ADTNode<ADTState<I, O>, I, O> nodeToSplit = finalNodes.stream()
.filter(n -> uaState.equals(n.getState()))
.findFirst()
.orElseThrow(IllegalStateException::new);

final ADTNode<ADTState<I, O>, I, O> nodeToSplit = findNodeForState(uaState);
final ADTNode<ADTState<I, O>, I, O> newNode;

// directly insert into observation tree, because we use it for finding a splitter
this.observationTree.addState(newState, newState.getAccessSequence(), oldTrans.getOutput());
this.observationTree.addTrace(newState, nodeToSplit);

final Word<I> previousTrace = ADTUtil.buildTraceForNode(nodeToSplit).getFirst();
final Optional<Word<I>> extension = this.observationTree.findSeparatingWord(uaState, newState, previousTrace);

if (extension.isPresent()) {
final Word<I> completeSplitter = previousTrace.concat(extension.get());
final Word<O> oldOutput = this.observationTree.trace(uaState, completeSplitter);
final Word<O> newOutput = this.observationTree.trace(newState, completeSplitter);
final Word<I> 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));

// in doubt, we will always find v
final Word<I> otSepWord = this.observationTree.findSeparatingWord(uaState, newState);
final Word<I> splitter;
assert otSepWord != null;

if (otSepWord.length() < v.length()) {
splitter = otSepWord;
Expand All @@ -259,6 +250,12 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
final Word<O> newOutput = this.observationTree.trace(newState, splitter);

newNode = this.adt.splitLeaf(nodeToSplit, splitter, oldOutput, newOutput, this.leafSplitter);
} else {
final Word<I> completeSplitter = previousTrace.concat(extension);
final Word<O> oldOutput = this.observationTree.trace(uaState, completeSplitter);
final Word<O> newOutput = this.observationTree.trace(newState, completeSplitter);

newNode = this.adt.extendLeaf(nodeToSplit, completeSplitter, oldOutput, newOutput, this.leafSplitter);
}
newNode.setState(newState);

Expand All @@ -269,11 +266,7 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
newTransitions.add(this.hypothesis.createOpenTransition(newState, i, this.adt.getRoot()));
}

final List<ADTTransition<I, O>> transitionsToRefine = nodeToSplit.getState()
.getIncomingTransitions()
.stream()
.filter(x -> !x.isSpanningTreeEdge())
.collect(Collectors.toList());
final List<ADTTransition<I, O>> transitionsToRefine = getIncomingNonSpanningTreeTransitions(uaState);

for (ADTTransition<I, O> x : transitionsToRefine) {
x.setTarget(null);
Expand All @@ -299,6 +292,18 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
return true;
}

private ADTNode<ADTState<I, O>, I, O> findNodeForState(ADTState<I, O> state) {

for (ADTNode<ADTState<I, O>, 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<?, I, ?, O> getHypothesisModel() {
return this.hypothesis;
Expand Down Expand Up @@ -503,7 +508,8 @@ private ADTNode<ADTState<I, O>, I, O> evaluateAdtExtension(ADTNode<ADTState<I, O
final ADTNode<ADTState<I, O>, I, O> extension = potentialExtension.getReplacement();
final ADTNode<ADTState<I, O>, 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<ADTState<I, O>, I, O> replacement = this.verifyADS(nodeToReplace,
extension,
Expand Down Expand Up @@ -602,7 +608,7 @@ private boolean validateADS(ADTNode<ADTState<I, O>, 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)) {
Expand Down Expand Up @@ -755,7 +761,6 @@ private void resolveAmbiguities(ADTNode<ADTState<I, O>, I, O> nodeToReplace,

for (ADTNode<ADTState<I, O>, I, O> leaf : cachedLeaves) {
final ADTState<I, O> hypState = leaf.getState();
assert hypState != null;

if (hypState.equals(finalNode.getState())) {
oldReference = leaf;
Expand All @@ -768,6 +773,7 @@ private void resolveAmbiguities(ADTNode<ADTState<I, O>, I, O> nodeToReplace,
}
}

assert oldReference != null && newReference != null;
final LCAInfo<ADTState<I, O>, I, O> lcaResult = this.adt.findLCA(oldReference, newReference);
final ADTNode<ADTState<I, O>, I, O> lca = lcaResult.adtNode;
final Pair<Word<I>, Word<O>> lcaTrace = ADTUtil.buildTraceForNode(lca);
Expand Down Expand Up @@ -807,20 +813,27 @@ private void resiftAffectedTransitions(Set<ADTNode<ADTState<I, O>, I, O>> states

for (ADTNode<ADTState<I, O>, I, O> state : states) {

final List<ADTTransition<I, O>> transitionsToRefine = state.getState()
.getIncomingTransitions()
.stream()
.filter(x -> !x.isSpanningTreeEdge())
.collect(Collectors.toList());

for (ADTTransition<I, O> trans : transitionsToRefine) {
for (ADTTransition<I, O> trans : getIncomingNonSpanningTreeTransitions(state.getState())) {
trans.setTarget(null);
trans.setSiftNode(finalizedADS);
this.openTransitions.add(trans);
}
}
}

private List<ADTTransition<I, O>> getIncomingNonSpanningTreeTransitions(ADTState<I, O> state) {
final Set<ADTTransition<I, O>> transitions = state.getIncomingTransitions();
final List<ADTTransition<I, O>> result = new ArrayList<>(transitions.size());

for (ADTTransition<I, O> t : transitions) {
if (!t.isSpanningTreeEdge()) {
result.add(t);
}
}

return result;
}

public ADT<ADTState<I, O>, I, O> getADT() {
return adt;
}
Expand Down
Loading

0 comments on commit 61a188b

Please sign in to comment.