Skip to content

Commit bd602cb

Browse files
leonthaleevitomtf90
authored
Parallelize ADT Learner (#132)
* short: - new AdaptiveQuery abstract class with adt and default query extensions - new adaptiveADTOracle classes with parallel interfaces and static implementation - adaptive membership oracle for preset adaptive queries - sleepySUL - changes in ADTLearner class for new Adaptive classes verbose: - added abstract class Adaptive Query in "de.learnlib.query" - added Adaptive_ADT_Query class in "de.learnlib.algorithm.adt.Adaptive" - (added ADTNode<S, I, O> getSuccessor() in ADTResetNode ( in "de.learnlib.algorithm.adt.adt" ) for Adaptive_ADT_Query to work ) - added AdaptiveMembershipOracle interface in "de.learnlib.oracle" - added package Adaptive in "de/learnlib/algorithm/adt/Adaptive" - added Sul_Adaptive_Oracle class in "de.learnlib.algorithm.adt.Adaptive" - added Adaptive_DEF_Query class in "de.learnlib.algorithm.adt.Adaptive" - added A2M_Oracle class in "de.learnlib.algorithm.adt.Adaptive" - added ParallelAdaptiveOracle interface in "de.learnlib.oracle" - added StaticParallelAdaptiveOracle in "de.learnlib.oracle.parallelism" - added SleepySUL class in "de.learnlib.algorithm.adt.Adaptive" - modified ADTLearner class: - added constructor for adaptive membership oracle - added AdaptiveMembershipOracle attribute. - modified startLearning() to choose between oracles - added closeTransitionsLeon() method to use appropriate oracles * added contact info to the parent pom.xml * initial refacotring ideas known issues: * adaptive parallel oracle testing still missing * AQOOTBridge non-functional * A2S_Oracle non-functional * add parallelism tests * some experimentation with adaptive caches * may replace SQOOTBridge * testing of counter currently broken * some progress * some progress * tests now pass * fix code-analysis remarks * remove old SymbolQuery code * some cleanups * share some functionality * add documentation + small cleanups * update CHANGELOG * remove obsolete method --------- Co-authored-by: vito <vito@vito> Co-authored-by: Markus Frohme <[email protected]> Co-authored-by: Markus Frohme <[email protected]>
1 parent 3e5c33d commit bd602cb

File tree

56 files changed

+2642
-995
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+2642
-995
lines changed

‎CHANGELOG.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
1010

1111
* 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.
1212
* 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).
13+
* 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)).
1314

1415
### Changed
1516

@@ -30,6 +31,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
3031
* 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).
3132
* 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.
3233
* `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.
34+
* `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.
3335

3436

3537
## [0.17.0] - 2023-11-15

‎algorithms/active/adt/pom.xml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,10 @@ limitations under the License.
4040
<groupId>de.learnlib</groupId>
4141
<artifactId>learnlib-api</artifactId>
4242
</dependency>
43+
<dependency>
44+
<groupId>de.learnlib</groupId>
45+
<artifactId>learnlib-cache</artifactId>
46+
</dependency>
4347
<dependency>
4448
<groupId>de.learnlib</groupId>
4549
<artifactId>learnlib-counterexamples</artifactId>

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

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@
2222
import de.learnlib.algorithm.adt.api.LeafSplitter;
2323
import de.learnlib.algorithm.adt.config.LeafSplitters;
2424
import de.learnlib.algorithm.adt.util.ADTUtil;
25-
import de.learnlib.oracle.SymbolQueryOracle;
2625
import net.automatalib.word.Word;
2726

2827
/**
@@ -93,29 +92,6 @@ public void replaceNode(ADTNode<S, I, O> oldNode, ADTNode<S, I, O> newNode) {
9392
}
9493
}
9594

96-
/**
97-
* Successively sifts a word through the ADT induced by the given node. Stops when reaching a leaf.
98-
*
99-
* @param oracle
100-
* the oracle to query with inner node symbols
101-
* @param word
102-
* the word to sift
103-
* @param subtree
104-
* the node whose subtree is considered
105-
*
106-
* @return the leaf (see {@link ADTNode#sift(SymbolQueryOracle, Word)})
107-
*/
108-
public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> word, ADTNode<S, I, O> subtree) {
109-
110-
ADTNode<S, I, O> current = subtree;
111-
112-
while (!ADTUtil.isLeafNode(current)) {
113-
current = current.sift(oracle, word);
114-
}
115-
116-
return current;
117-
}
118-
11995
/**
12096
* Splitting a leaf node by extending the trace leading into the node to split.
12197
*

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

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,7 @@
1515
*/
1616
package de.learnlib.algorithm.adt.adt;
1717

18-
import de.learnlib.oracle.SymbolQueryOracle;
1918
import net.automatalib.graph.ads.impl.AbstractRecursiveADSLeafNode;
20-
import net.automatalib.word.Word;
2119
import org.checkerframework.checker.nullness.qual.Nullable;
2220

2321
/**
@@ -37,11 +35,6 @@ public ADTLeafNode(@Nullable ADTNode<S, I, O> parent, @Nullable S hypothesisStat
3735
super(parent, hypothesisState);
3836
}
3937

40-
@Override
41-
public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
42-
throw new UnsupportedOperationException("Final nodes cannot sift words");
43-
}
44-
4538
@Override
4639
public NodeType getNodeType() {
4740
return NodeType.LEAF_NODE;

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

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,8 @@
1919
import java.util.Map;
2020

2121
import de.learnlib.algorithm.adt.util.ADTUtil;
22-
import de.learnlib.oracle.SymbolQueryOracle;
2322
import net.automatalib.graph.ads.RecursiveADSNode;
2423
import net.automatalib.visualization.VisualizationHelper;
25-
import net.automatalib.word.Word;
2624

2725
/**
2826
* The ADT equivalent of {@link net.automatalib.graph.ads.ADSNode}. In contrast to regular adaptive distinguishing
@@ -38,23 +36,16 @@
3836
public interface ADTNode<S, I, O> extends RecursiveADSNode<S, I, O, ADTNode<S, I, O>> {
3937

4038
/**
41-
* Utility method, that sifts a given word through {@code this} ADTNode. If {@code this} node is a <ul> <li>symbol
42-
* node, the symbol is applied to the system under learning and the corresponding child node (based on the observed
43-
* output) is returned. If no matching child node is found, a new leaf node is returned instead </li> <li> reset
44-
* node, the system under learning is reset and the provided prefix is reapplied to the system </li> <li> leaf node,
45-
* an exception is thrown </li> </ul>
39+
* Convenience method for directly accessing this node's {@link #getChildren() children}.
4640
*
47-
* @param oracle
48-
* the oracle used to query the system under learning
49-
* @param prefix
50-
* the prefix to be re-applied after encountering a reset node
41+
* @param output
42+
* the output symbol to determine the child to returned
5143
*
52-
* @return the corresponding child node
53-
*
54-
* @throws UnsupportedOperationException
55-
* when invoked on a leaf node (see {@link #getNodeType()}).
44+
* @return the child node that is mapped to given output. May be {@code null},
5645
*/
57-
ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix);
46+
default ADTNode<S, I, O> getChild(O output) {
47+
return getChildren().get(output);
48+
}
5849

5950
// default methods for graph interface
6051
@Override

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

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,6 @@
1818
import java.util.Collections;
1919
import java.util.Map;
2020

21-
import de.learnlib.oracle.SymbolQueryOracle;
22-
import net.automatalib.word.Word;
2321
import org.checkerframework.checker.nullness.qual.Nullable;
2422

2523
/**
@@ -76,17 +74,6 @@ public void setHypothesisState(S state) {
7674
throw new UnsupportedOperationException("Reset nodes cannot reference a hypothesis state");
7775
}
7876

79-
@Override
80-
public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
81-
oracle.reset();
82-
83-
for (I i : prefix) {
84-
oracle.query(i);
85-
}
86-
87-
return successor;
88-
}
89-
9077
@Override
9178
public NodeType getNodeType() {
9279
return NodeType.RESET_NODE;

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

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,7 @@
1515
*/
1616
package de.learnlib.algorithm.adt.adt;
1717

18-
import de.learnlib.oracle.SymbolQueryOracle;
1918
import net.automatalib.graph.ads.impl.AbstractRecursiveADSSymbolNode;
20-
import net.automatalib.word.Word;
2119
import org.checkerframework.checker.nullness.qual.Nullable;
2220

2321
/**
@@ -37,21 +35,6 @@ public ADTSymbolNode(@Nullable ADTNode<S, I, O> parent, I symbol) {
3735
super(parent, symbol);
3836
}
3937

40-
@Override
41-
public ADTNode<S, I, O> sift(SymbolQueryOracle<I, O> oracle, Word<I> prefix) {
42-
final O o = oracle.query(super.getSymbol());
43-
44-
final ADTNode<S, I, O> successor = super.getChildren().get(o);
45-
46-
if (successor == null) {
47-
final ADTNode<S, I, O> result = new ADTLeafNode<>(this, null);
48-
super.getChildren().put(o, result);
49-
return result;
50-
}
51-
52-
return successor;
53-
}
54-
5538
@Override
5639
public NodeType getNodeType() {
5740
return NodeType.SYMBOL_NODE;

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ public static <S, I, O> ADTNode<S, I, O> splitParent(ADTNode<S, I, O> nodeToSpli
159159
newIter.next();
160160
newSuffixOutput = oldIter.next();
161161

162-
adsIter = adsIter.getChildren().get(newSuffixOutput);
162+
adsIter = adsIter.getChild(newSuffixOutput);
163163
}
164164

165165
final ADTNode<S, I, O> continuedADS = new ADTSymbolNode<>(adsIter.getParent(), suffixIter.next());

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

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/* Copyright (C) 2013-2024 TU Dortmund University
2+
* This file is part of LearnLib, http://www.learnlib.de/.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.algorithm.adt.learner;
17+
18+
import java.util.ArrayDeque;
19+
import java.util.Deque;
20+
21+
import de.learnlib.algorithm.adt.adt.ADTNode;
22+
import de.learnlib.algorithm.adt.automaton.ADTState;
23+
import net.automatalib.word.Word;
24+
25+
/**
26+
* Utility class to resolve ADS ambiguities. This query simply tracks the current ADT node for the given inputs.
27+
*
28+
* @param <I>
29+
* input symbol type
30+
* @param <O>
31+
* output symbol type
32+
*/
33+
class ADSAmbiguityQuery<I, O> extends AbstractAdaptiveQuery<I, O> {
34+
35+
private final Word<I> accessSequence;
36+
private final Deque<I> oneShotPrefix;
37+
38+
private int asIndex;
39+
private boolean inOneShot;
40+
41+
ADSAmbiguityQuery(Word<I> accessSequence, Word<I> oneShotPrefix, ADTNode<ADTState<I, O>, I, O> root) {
42+
super(root);
43+
this.accessSequence = accessSequence;
44+
this.oneShotPrefix = new ArrayDeque<>(oneShotPrefix.asList());
45+
this.asIndex = 0;
46+
this.inOneShot = false;
47+
}
48+
49+
@Override
50+
public I getInput() {
51+
if (this.asIndex < this.accessSequence.length()) {
52+
return this.accessSequence.getSymbol(this.asIndex);
53+
} else {
54+
this.inOneShot = !this.oneShotPrefix.isEmpty();
55+
if (this.inOneShot) {
56+
return oneShotPrefix.poll();
57+
} else {
58+
return this.currentADTNode.getSymbol();
59+
}
60+
}
61+
}
62+
63+
@Override
64+
public Response processOutput(O out) {
65+
if (this.asIndex < this.accessSequence.length()) {
66+
asIndex++;
67+
return Response.SYMBOL;
68+
} else if (this.inOneShot) {
69+
return Response.SYMBOL;
70+
} else {
71+
return super.processOutput(out);
72+
}
73+
}
74+
75+
@Override
76+
protected void resetProgress() {
77+
this.asIndex = 0;
78+
}
79+
}
80+
81+

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

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
/* Copyright (C) 2013-2024 TU Dortmund University
2+
* This file is part of LearnLib, http://www.learnlib.de/.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.algorithm.adt.learner;
17+
18+
import java.util.Objects;
19+
20+
import de.learnlib.algorithm.adt.automaton.ADTState;
21+
import de.learnlib.query.AdaptiveQuery;
22+
import de.learnlib.query.DefaultQuery;
23+
import net.automatalib.word.Word;
24+
import net.automatalib.word.WordBuilder;
25+
import org.checkerframework.checker.nullness.qual.Nullable;
26+
27+
/**
28+
* Utility class to verify ADSs. This query tracks the current ADT node for the given inputs and compares it with an
29+
* expected output, potentially constructing a counterexample from the observed data.
30+
*
31+
* @param <I>
32+
* input symbol type
33+
* @param <O>
34+
* output symbol type
35+
*/
36+
class ADSVerificationQuery<I, O> implements AdaptiveQuery<I, O> {
37+
38+
private final Word<I> prefix;
39+
private final Word<I> suffix;
40+
private final Word<O> expectedOutput;
41+
private final WordBuilder<O> outputBuilder;
42+
private final ADTState<I, O> state;
43+
44+
private final int prefixLength;
45+
private final int suffixLength;
46+
private int idx;
47+
private @Nullable DefaultQuery<I, Word<O>> counterexample;
48+
49+
ADSVerificationQuery(Word<I> prefix, Word<I> suffix, Word<O> expectedSuffixOutput, ADTState<I, O> state) {
50+
this.prefix = prefix;
51+
this.suffix = suffix;
52+
this.expectedOutput = expectedSuffixOutput;
53+
this.outputBuilder = new WordBuilder<>(suffix.size());
54+
this.state = state;
55+
56+
this.prefixLength = prefix.length();
57+
this.suffixLength = suffix.length();
58+
this.idx = 0;
59+
}
60+
61+
@Override
62+
public I getInput() {
63+
if (idx < prefixLength) {
64+
return prefix.getSymbol(idx);
65+
} else {
66+
return suffix.getSymbol(idx - prefixLength);
67+
}
68+
}
69+
70+
@Override
71+
public Response processOutput(O out) {
72+
if (idx < prefixLength) {
73+
idx++;
74+
return Response.SYMBOL;
75+
} else {
76+
outputBuilder.append(out);
77+
78+
if (!Objects.equals(out, expectedOutput.getSymbol(idx - prefixLength))) {
79+
counterexample =
80+
new DefaultQuery<>(prefix, suffix.prefix(outputBuilder.size()), outputBuilder.toWord());
81+
return Response.FINISHED;
82+
} else if (outputBuilder.size() < suffixLength) {
83+
idx++;
84+
return Response.SYMBOL;
85+
} else {
86+
return Response.FINISHED;
87+
}
88+
}
89+
}
90+
91+
@Nullable
92+
DefaultQuery<I, Word<O>> getCounterexample() {
93+
return counterexample;
94+
}
95+
96+
ADTState<I, O> getState() {
97+
return state;
98+
}
99+
100+
Word<I> getSuffix() {
101+
return suffix;
102+
}
103+
104+
Word<O> getExpectedOutput() {
105+
return expectedOutput;
106+
}
107+
}

0 commit comments

Comments
 (0)