Skip to content

Commit 110ed62

Browse files
mtf90mtf90
authored
Add Resumable support for remaining Lambda learners (#159)
* initial work on resumable TTTLambda * add test cases * do not store refernce to oracle in datastructures * warn on mismatching alphabets * add changelog
1 parent 8bc2787 commit 110ed62

20 files changed

Lines changed: 304 additions & 84 deletions

‎CHANGELOG.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
1111
* Added a new (L*-based) learning algorithm for *Mealy machines with local timers* (MMLTs), including support for parallel queries, caching, and conformance testing (thanks to [Paul Kogel](https://github.com/pdev55)).
1212
* Added the L<sup>s</sup> active learning algorithm for Mealy machines (thanks to [Wolffhardt Schwabe](https://github.com/stateMachinist)).
1313
* Added an `EarlyExitEQOracle` which for a given `AdaptiveMembershipOracle` and `TestWordGenerator` stops the evaluation of (potentially long) Mealy-based equivalence tests as soon as a mismatch with the hypothesis is detected, potentially improving the symbol performance of the given equivalence oracle.
14+
* Both lambda learners (`LLambda{DFA,Mealy}` and `TTTLambda{DFA,Mealy}`) now support the `Resumable` interface.
1415

1516
### Changed
1617

‎algorithms/active/lambda/pom.xml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,10 @@ limitations under the License.
6363
<groupId>org.checkerframework</groupId>
6464
<artifactId>checker-qual</artifactId>
6565
</dependency>
66+
<dependency>
67+
<groupId>org.slf4j</groupId>
68+
<artifactId>slf4j-api</artifactId>
69+
</dependency>
6670

6771
<!-- test -->
6872
<dependency>

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/lstar/AbstractLLambda.java‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@
2929

3030
import de.learnlib.Resumable;
3131
import de.learnlib.algorithm.LearningAlgorithm;
32+
import de.learnlib.logging.Category;
3233
import de.learnlib.oracle.MembershipOracle;
3334
import de.learnlib.query.DefaultQuery;
3435
import de.learnlib.util.MQUtil;
@@ -37,12 +38,16 @@
3738
import net.automatalib.automaton.concept.FiniteRepresentation;
3839
import net.automatalib.automaton.concept.SuffixOutput;
3940
import net.automatalib.word.Word;
41+
import org.slf4j.Logger;
42+
import org.slf4j.LoggerFactory;
4043

4144
abstract class AbstractLLambda<M extends SuffixOutput<I, D>, I, D> implements LearningAlgorithm<M, I, D>,
4245
SupportsGrowingAlphabet<I>,
4346
Resumable<LLambdaState<I, D>>,
4447
FiniteRepresentation {
4548

49+
private static final Logger LOGGER = LoggerFactory.getLogger(AbstractLLambda.class);
50+
4651
final Alphabet<I> alphabet;
4752
final MembershipOracle<I, D> mqs;
4853
final MembershipOracle<I, D> ceqs;
@@ -305,7 +310,7 @@ public void addAlphabetSymbol(I symbol) {
305310

306311
@Override
307312
public LLambdaState<I, D> suspend() {
308-
return new LLambdaState<>(shortPrefixes, rows, suffixes);
313+
return new LLambdaState<>(alphabet, shortPrefixes, rows, suffixes);
309314
}
310315

311316
@Override
@@ -314,6 +319,14 @@ public void resume(LLambdaState<I, D> state) {
314319
this.rows.clear();
315320
this.suffixes.clear();
316321

322+
final Alphabet<I> oldAlphabet = state.getAlphabet();
323+
if (!this.alphabet.equals(oldAlphabet)) {
324+
LOGGER.warn(Category.DATASTRUCTURE,
325+
"The current alphabet '{}' differs from the resumed alphabet '{}'. Future behavior may be inconsistent",
326+
this.alphabet,
327+
oldAlphabet);
328+
}
329+
317330
this.shortPrefixes.addAll(state.getShortPrefixes());
318331
this.rows.putAll(state.getRows());
319332
this.suffixes.addAll(state.getSuffixes());

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/lstar/LLambdaState.java‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
import java.util.Set;
2121

2222
import de.learnlib.Resumable;
23+
import net.automatalib.alphabet.Alphabet;
2324
import net.automatalib.word.Word;
2425

2526
/**
@@ -32,16 +33,22 @@
3233
*/
3334
public class LLambdaState<I, D> {
3435

36+
private final Alphabet<I> alphabet;
3537
private final Set<Word<I>> shortPrefixes;
3638
private final Map<Word<I>, List<D>> rows;
3739
private final List<Word<I>> suffixes;
3840

39-
LLambdaState(Set<Word<I>> shortPrefixes, Map<Word<I>, List<D>> rows, List<Word<I>> suffixes) {
41+
LLambdaState(Alphabet<I> alphabet, Set<Word<I>> shortPrefixes, Map<Word<I>, List<D>> rows, List<Word<I>> suffixes) {
42+
this.alphabet = alphabet;
4043
this.shortPrefixes = shortPrefixes;
4144
this.rows = rows;
4245
this.suffixes = suffixes;
4346
}
4447

48+
Alphabet<I> getAlphabet() {
49+
return alphabet;
50+
}
51+
4552
Set<Word<I>> getShortPrefixes() {
4653
return shortPrefixes;
4754
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/AbstractTTTLambda.java‎

Lines changed: 42 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,14 @@
2020
import java.util.List;
2121
import java.util.Objects;
2222

23+
import de.learnlib.Resumable;
2324
import de.learnlib.algorithm.LearningAlgorithm;
2425
import de.learnlib.algorithm.lambda.ttt.dt.AbstractDecisionTree;
2526
import de.learnlib.algorithm.lambda.ttt.dt.DTLeaf;
2627
import de.learnlib.algorithm.lambda.ttt.pt.PTNode;
2728
import de.learnlib.algorithm.lambda.ttt.pt.PrefixTree;
2829
import de.learnlib.algorithm.lambda.ttt.st.SuffixTrie;
30+
import de.learnlib.logging.Category;
2931
import de.learnlib.oracle.MembershipOracle;
3032
import de.learnlib.query.DefaultQuery;
3133
import de.learnlib.util.MQUtil;
@@ -35,17 +37,25 @@
3537
import net.automatalib.automaton.concept.SuffixOutput;
3638
import net.automatalib.word.Word;
3739
import org.checkerframework.checker.nullness.qual.Nullable;
40+
import org.slf4j.Logger;
41+
import org.slf4j.LoggerFactory;
3842

39-
public abstract class AbstractTTTLambda<M extends SuffixOutput<I, D>, I, D>
40-
implements LearningAlgorithm<M, I, D>, SupportsGrowingAlphabet<I>, FiniteRepresentation {
43+
public abstract class AbstractTTTLambda<M extends SuffixOutput<I, D>, I, D> implements LearningAlgorithm<M, I, D>,
44+
SupportsGrowingAlphabet<I>,
45+
Resumable<TTTLambdaState<I, D>>,
46+
FiniteRepresentation {
4147

48+
private static final Logger LOGGER = LoggerFactory.getLogger(AbstractTTTLambda.class);
49+
50+
private final MembershipOracle<I, D> mqs;
4251
private final MembershipOracle<I, D> ceqs;
4352
protected final Alphabet<I> alphabet;
44-
protected final SuffixTrie<I> strie;
45-
protected final PrefixTree<I, D> ptree;
53+
protected SuffixTrie<I> strie;
54+
protected PrefixTree<I, D> ptree;
4655

47-
protected AbstractTTTLambda(Alphabet<I> alphabet, MembershipOracle<I, D> ceqs) {
56+
protected AbstractTTTLambda(Alphabet<I> alphabet, MembershipOracle<I, D> mqs, MembershipOracle<I, D> ceqs) {
4857
this.alphabet = alphabet;
58+
this.mqs = mqs;
4959
this.ceqs = ceqs;
5060

5161
this.strie = new SuffixTrie<>();
@@ -61,8 +71,8 @@ protected AbstractTTTLambda(Alphabet<I> alphabet, MembershipOracle<I, D> ceqs) {
6171
@Override
6272
public void startLearning() {
6373
assert dtree() != null && getHypothesisModel() != null;
64-
dtree().sift(ptree.root());
65-
makeConsistent();
74+
dtree().sift(mqs, ptree.root());
75+
makeConsistent(mqs);
6676
}
6777

6878
@Override
@@ -82,7 +92,7 @@ public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
8292

8393
if (valid) {
8494
analyzeCounterexample(witness, witnesses);
85-
makeConsistent();
95+
makeConsistent(mqs);
8696
refined = true;
8797
} else {
8898
witnesses.pop();
@@ -109,15 +119,15 @@ public void addAlphabetSymbol(I symbol) {
109119
assert u != null;
110120
PTNode<I, D> ua = u.append(symbol);
111121
assert ua != null;
112-
dtree().sift(ua);
122+
dtree().sift(mqs, ua);
113123
}
114124

115-
makeConsistent();
125+
makeConsistent(mqs);
116126
}
117127
}
118128

119-
protected void makeConsistent() {
120-
while (dtree().makeConsistent()) {
129+
protected void makeConsistent(MembershipOracle<I, D> oracle) {
130+
while (dtree().makeConsistent(oracle)) {
121131
// do nothing ...
122132
}
123133
}
@@ -181,6 +191,25 @@ private void analyzeCounterexample(DefaultQuery<I, D> counterexample, Deque<Defa
181191
}
182192
witnesses.push(new DefaultQuery<>(ua.word(), sprime));
183193

184-
ua.makeShortPrefix();
194+
ua.makeShortPrefix(mqs);
195+
}
196+
197+
@Override
198+
public TTTLambdaState<I, D> suspend() {
199+
return new TTTLambdaState<>(strie, ptree, dtree());
200+
}
201+
202+
@Override
203+
public void resume(TTTLambdaState<I, D> state) {
204+
this.strie = state.strie;
205+
this.ptree = state.ptree;
206+
207+
final Alphabet<I> oldAlphabet = state.dtree.getAlphabet();
208+
if (!this.alphabet.equals(oldAlphabet)) {
209+
LOGGER.warn(Category.DATASTRUCTURE,
210+
"The current alphabet '{}' differs from the resumed alphabet '{}'. Future behavior may be inconsistent",
211+
this.alphabet,
212+
oldAlphabet);
213+
}
185214
}
186215
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/TTTLambdaState.java‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/* Copyright (C) 2013-2026 TU Dortmund University
2+
* This file is part of LearnLib <https://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.lambda.ttt;
17+
18+
import de.learnlib.algorithm.lambda.ttt.dt.AbstractDecisionTree;
19+
import de.learnlib.algorithm.lambda.ttt.pt.PrefixTree;
20+
import de.learnlib.algorithm.lambda.ttt.st.SuffixTrie;
21+
22+
public class TTTLambdaState<I, D> {
23+
24+
public final SuffixTrie<I> strie;
25+
public final PrefixTree<I, D> ptree;
26+
public final AbstractDecisionTree<I, D> dtree;
27+
28+
public TTTLambdaState(SuffixTrie<I> strie, PrefixTree<I, D> ptree, AbstractDecisionTree<I, D> dtree) {
29+
this.strie = strie;
30+
this.ptree = ptree;
31+
this.dtree = dtree;
32+
}
33+
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/dfa/DecisionTreeDFA.java‎

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,15 +20,13 @@
2020
import de.learnlib.algorithm.lambda.ttt.dt.Children;
2121
import de.learnlib.algorithm.lambda.ttt.dt.DTInnerNode;
2222
import de.learnlib.algorithm.lambda.ttt.dt.DTLeaf;
23-
import de.learnlib.algorithm.lambda.ttt.pt.PTNode;
2423
import de.learnlib.algorithm.lambda.ttt.st.STNode;
25-
import de.learnlib.oracle.MembershipOracle;
2624
import net.automatalib.alphabet.Alphabet;
2725

2826
class DecisionTreeDFA<I> extends AbstractDecisionTree<I, Boolean> {
2927

30-
DecisionTreeDFA(MembershipOracle<I, Boolean> mqOracle, Alphabet<I> sigma, STNode<I> stRoot) {
31-
super(sigma, mqOracle, stRoot);
28+
DecisionTreeDFA(Alphabet<I> sigma, STNode<I> stRoot) {
29+
super(sigma, stRoot);
3230
}
3331

3432
boolean isAccepting(DTLeaf<I, Boolean> s) {
@@ -41,11 +39,6 @@ protected Children<I, Boolean> newChildren() {
4139
return new ChildrenDFA<>();
4240
}
4341

44-
@Override
45-
protected Boolean query(PTNode<I, Boolean> prefix, STNode<I> suffix) {
46-
return mqOracle.answerQuery(prefix.word(), suffix.word());
47-
}
48-
4942
private DTInnerNode<I, Boolean> localRoot() {
5043
return (DTInnerNode<I, Boolean>) root;
5144
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/dfa/TTTLambdaDFA.java‎

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717

1818
import de.learnlib.algorithm.LearningAlgorithm.DFALearner;
1919
import de.learnlib.algorithm.lambda.ttt.AbstractTTTLambda;
20+
import de.learnlib.algorithm.lambda.ttt.TTTLambdaState;
2021
import de.learnlib.algorithm.lambda.ttt.dt.AbstractDecisionTree;
2122
import de.learnlib.algorithm.lambda.ttt.dt.DTInnerNode;
2223
import de.learnlib.algorithm.lambda.ttt.dt.DTLeaf;
@@ -28,16 +29,16 @@
2829

2930
public class TTTLambdaDFA<I> extends AbstractTTTLambda<DFA<?, I>, I, Boolean> implements DFALearner<I> {
3031

31-
private final HypothesisDFA<I> hypothesis;
32-
private final DecisionTreeDFA<I> dtree;
32+
private HypothesisDFA<I> hypothesis;
33+
private DecisionTreeDFA<I> dtree;
3334

3435
public TTTLambdaDFA(Alphabet<I> alphabet, MembershipOracle<I, Boolean> mqo) {
3536
this(alphabet, mqo, mqo);
3637
}
3738

3839
public TTTLambdaDFA(Alphabet<I> alphabet, MembershipOracle<I, Boolean> mqs, MembershipOracle<I, Boolean> ceqs) {
39-
super(alphabet, ceqs);
40-
dtree = new DecisionTreeDFA<>(mqs, alphabet, strie.root());
40+
super(alphabet, mqs, ceqs);
41+
dtree = new DecisionTreeDFA<>(alphabet, strie.root());
4142
DTInnerNode<I, Boolean> dtRoot = new DTInnerNode<>(null, dtree, new ChildrenDFA<>(), strie.root());
4243
dtree.setRoot(dtRoot);
4344
hypothesis = new HypothesisDFA<>(ptree, dtree);
@@ -67,4 +68,15 @@ protected AbstractDecisionTree<I, Boolean> dtree() {
6768
public int size() {
6869
return hypothesis.size();
6970
}
71+
72+
@Override
73+
public void resume(TTTLambdaState<I, Boolean> state) {
74+
super.resume(state);
75+
if (state.dtree instanceof DecisionTreeDFA<I> d) {
76+
this.dtree = d;
77+
this.hypothesis = new HypothesisDFA<>(ptree, dtree);
78+
} else {
79+
throw new IllegalArgumentException("provided state does not match expected structure");
80+
}
81+
}
7082
}

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/dt/AbstractDTNode.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import java.util.List;
2020

2121
import de.learnlib.algorithm.lambda.ttt.pt.PTNode;
22+
import de.learnlib.oracle.MembershipOracle;
2223
import org.checkerframework.checker.nullness.qual.Nullable;
2324

2425
public abstract class AbstractDTNode<I, D> {
@@ -44,7 +45,7 @@ void path(List<AbstractDTNode<I, D>> path) {
4445
}
4546
}
4647

47-
abstract void sift(PTNode<I, D> prefix);
48+
abstract void sift(MembershipOracle<I, D> oracle, PTNode<I, D> prefix);
4849

4950
abstract void leaves(List<DTLeaf<I, D>> list);
5051

‎algorithms/active/lambda/src/main/java/de/learnlib/algorithm/lambda/ttt/dt/AbstractDecisionTree.java‎

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -26,23 +26,19 @@
2626
public abstract class AbstractDecisionTree<I, D> {
2727

2828
private final STNode<I> stRoot;
29-
protected final MembershipOracle<I, D> mqOracle;
30-
protected final Alphabet<I> alphabet;
29+
private final Alphabet<I> alphabet;
3130

3231
protected AbstractDTNode<I, D> root;
3332

34-
protected AbstractDecisionTree(Alphabet<I> alphabet, MembershipOracle<I, D> mqOracle, STNode<I> stRoot) {
35-
this.mqOracle = mqOracle;
33+
protected AbstractDecisionTree(Alphabet<I> alphabet, STNode<I> stRoot) {
3634
this.alphabet = alphabet;
3735
this.stRoot = stRoot;
3836
}
3937

4038
protected abstract Children<I, D> newChildren();
4139

42-
protected abstract D query(PTNode<I, D> prefix, STNode<I> suffix);
43-
44-
public void sift(PTNode<I, D> prefix) {
45-
root.sift(prefix);
40+
public void sift(MembershipOracle<I, D> oracle, PTNode<I, D> prefix) {
41+
root.sift(oracle, prefix);
4642
}
4743

4844
public void setRoot(AbstractDTNode<I, D> newRoot) {
@@ -55,11 +51,11 @@ public List<DTLeaf<I, D>> leaves() {
5551
return list;
5652
}
5753

58-
public boolean makeConsistent() {
54+
public boolean makeConsistent(MembershipOracle<I, D> oracle) {
5955
List<DTLeaf<I, D>> leaves = new ArrayList<>();
6056
root.leaves(leaves);
6157
for (DTLeaf<I, D> n : leaves) {
62-
if (n.refineIfPossible()) {
58+
if (n.refineIfPossible(oracle)) {
6359
return true;
6460
}
6561
}
@@ -70,7 +66,7 @@ AbstractDTNode<I, D> root() {
7066
return root;
7167
}
7268

73-
Alphabet<I> getAlphabet() {
69+
public Alphabet<I> getAlphabet() {
7470
return alphabet;
7571
}
7672

0 commit comments

Comments
 (0)