21987934897

Committed 13 Feb 2026 01:06PM UTC coverage: 95.047% (-0.004%) from 95.051%

Build # 21987934897

Build Type

push

github

Committed by

web-flow

Commit Message

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

Coverage Stats

72 of 74 new or added lines in 13 files covered. (97.3%)

14584 of 15344 relevant lines covered (95.05%)

1.74 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

98.96

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

/* Copyright (C) 2013-2026 TU Dortmund University
 * This file is part of LearnLib <https://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.lambda.ttt;

import java.util.ArrayDeque;
import java.util.Deque;
import java.util.List;
import java.util.Objects;

import de.learnlib.Resumable;
import de.learnlib.algorithm.LearningAlgorithm;
import de.learnlib.algorithm.lambda.ttt.dt.AbstractDecisionTree;
import de.learnlib.algorithm.lambda.ttt.dt.DTLeaf;
import de.learnlib.algorithm.lambda.ttt.pt.PTNode;
import de.learnlib.algorithm.lambda.ttt.pt.PrefixTree;
import de.learnlib.algorithm.lambda.ttt.st.SuffixTrie;
import de.learnlib.logging.Category;
import de.learnlib.oracle.MembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.util.MQUtil;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.SupportsGrowingAlphabet;
import net.automatalib.automaton.concept.FiniteRepresentation;
import net.automatalib.automaton.concept.SuffixOutput;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

public abstract class AbstractTTTLambda<M extends SuffixOutput<I, D>, I, D> implements LearningAlgorithm<M, I, D>,
                                                                                       SupportsGrowingAlphabet<I>,
                                                                                       Resumable<TTTLambdaState<I, D>>,
                                                                                       FiniteRepresentation {

    private static final Logger LOGGER = LoggerFactory.getLogger(AbstractTTTLambda.class);

    private final MembershipOracle<I, D> mqs;
    private final MembershipOracle<I, D> ceqs;
    protected final Alphabet<I> alphabet;
    protected SuffixTrie<I> strie;
    protected PrefixTree<I, D> ptree;

    protected AbstractTTTLambda(Alphabet<I> alphabet, MembershipOracle<I, D> mqs, MembershipOracle<I, D> ceqs) {
        this.alphabet = alphabet;
        this.mqs = mqs;
        this.ceqs = ceqs;

        this.strie = new SuffixTrie<>();
        this.ptree = new PrefixTree<>();
    }

    protected abstract int maxSearchIndex(int ceLength);

    protected abstract @Nullable DTLeaf<I, D> getState(Word<I> prefix);

    protected abstract AbstractDecisionTree<I, D> dtree();

    @Override
    public void startLearning() {
        assert dtree() != null && getHypothesisModel() != null;
        dtree().sift(mqs, ptree.root());
        makeConsistent(mqs);
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
        final Deque<DefaultQuery<I, D>> witnesses = new ArrayDeque<>();
        witnesses.add(counterexample);
        boolean refined = false;

        while (MQUtil.isCounterexample(counterexample, getHypothesisModel())) {
            final DefaultQuery<I, D> witness = witnesses.getFirst();

            if (witness.getOutput() == null) {
                witness.answer(ceqs.answerQuery(witness.getPrefix(), witness.getSuffix()));
            }

            final boolean valid = MQUtil.isCounterexample(witness, getHypothesisModel());

            if (valid) {
                analyzeCounterexample(witness, witnesses);
                makeConsistent(mqs);
                refined = true;
            } else {
                witnesses.pop();
            }
        }

        assert size() == dtree().leaves().size();
        return refined;
    }

    @Override
    public void addAlphabetSymbol(I symbol) {
        if (!this.alphabet.containsSymbol(symbol)) {
            this.alphabet.asGrowingAlphabetOrThrowException().addSymbol(symbol);
        }

        // check if symbol is already part of ptree/hypothesis
        if (ptree.root().succ(symbol) == null) {

            List<DTLeaf<I, D>> leaves = dtree().leaves();

            for (DTLeaf<I, D> leaf : leaves) {
                PTNode<I, D> u = leaf.getShortPrefixes().get(0);
                assert u != null;
                PTNode<I, D> ua = u.append(symbol);
                assert ua != null;
                dtree().sift(mqs, ua);
            }

            makeConsistent(mqs);
        }
    }

    protected void makeConsistent(MembershipOracle<I, D> oracle) {
        while (dtree().makeConsistent(oracle)) {
            // do nothing ...
        }
    }

    private PTNode<I, D> longestShortPrefixOf(Word<I> ce) {
        PTNode<I, D> cur = ptree.root();
        int i = 0;
        do {
            cur = cur.succ(ce.getSymbol(i++));
            assert cur != null;
        } while (cur.state().getShortPrefixes().contains(cur) && i < ce.length());

        assert !cur.state().getShortPrefixes().contains(cur);
        return cur;
    }

    private void analyzeCounterexample(DefaultQuery<I, D> counterexample, Deque<DefaultQuery<I, D>> witnesses) {
        M hyp = getHypothesisModel();
        Word<I> ce = counterexample.getInput();
        PTNode<I, D> ua = null;
        PTNode<I, D> lsp = longestShortPrefixOf(ce);
        int upper = maxSearchIndex(ce.length());
        int lower = lsp.word().length() - 1;
        while (upper - lower > 1) {
            int mid = (upper + lower) / 2;
            Word<I> prefix = ce.prefix(mid);
            Word<I> suffix = ce.suffix(ce.length() - mid);

            DTLeaf<I, D> q = getState(prefix);
            assert q != null;

            boolean stillCe = false;
            for (PTNode<I, D> u : q.getShortPrefixes()) {
                D sysOut = ceqs.answerQuery(u.word(), suffix);
                D hypOut = hyp.computeSuffixOutput(u.word(), suffix);
                if (!Objects.equals(sysOut, hypOut)) {
                    ua = u.succ(suffix.firstSymbol());
                    lower = mid;
                    stillCe = true;
                    break;
                }
            }
            if (stillCe) {
                continue;
            }
            upper = mid;
        }

        if (ua == null) {
            assert lower == lsp.word().length() - 1;
            ua = lsp;
        }

        // add witnesses
        int mid = (upper + lower) / 2;
        Word<I> sprime = ce.suffix(ce.length() - (mid + 1));
        DTLeaf<I, D> qnext = getState(ua.word());
        assert qnext != null;
        for (PTNode<I, D> uprime : qnext.getShortPrefixes()) {
            witnesses.push(new DefaultQuery<>(uprime.word(), sprime));
        }
        witnesses.push(new DefaultQuery<>(ua.word(), sprime));

        ua.makeShortPrefix(mqs);
    }

    @Override
    public TTTLambdaState<I, D> suspend() {
        return new TTTLambdaState<>(strie, ptree, dtree());
    }

    @Override
    public void resume(TTTLambdaState<I, D> state) {
        this.strie = state.strie;
        this.ptree = state.ptree;

        final Alphabet<I> oldAlphabet = state.dtree.getAlphabet();
        if (!this.alphabet.equals(oldAlphabet)) {
            LOGGER.warn(Category.DATASTRUCTURE,
                        "The current alphabet '{}' differs from the resumed alphabet '{}'. Future behavior may be inconsistent",
                        this.alphabet,
                        oldAlphabet);
        }
    }
}

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 java.util.ArrayDeque;
19	import java.util.Deque;
20	import java.util.List;
21	import java.util.Objects;
22
23	import de.learnlib.Resumable;
24	import de.learnlib.algorithm.LearningAlgorithm;
25	import de.learnlib.algorithm.lambda.ttt.dt.AbstractDecisionTree;
26	import de.learnlib.algorithm.lambda.ttt.dt.DTLeaf;
27	import de.learnlib.algorithm.lambda.ttt.pt.PTNode;
28	import de.learnlib.algorithm.lambda.ttt.pt.PrefixTree;
29	import de.learnlib.algorithm.lambda.ttt.st.SuffixTrie;
30	import de.learnlib.logging.Category;
31	import de.learnlib.oracle.MembershipOracle;
32	import de.learnlib.query.DefaultQuery;
33	import de.learnlib.util.MQUtil;
34	import net.automatalib.alphabet.Alphabet;
35	import net.automatalib.alphabet.SupportsGrowingAlphabet;
36	import net.automatalib.automaton.concept.FiniteRepresentation;
37	import net.automatalib.automaton.concept.SuffixOutput;
38	import net.automatalib.word.Word;
39	import org.checkerframework.checker.nullness.qual.Nullable;
40	import org.slf4j.Logger;
41	import org.slf4j.LoggerFactory;
42
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 {
47
48	private static final Logger LOGGER = LoggerFactory.getLogger(AbstractTTTLambda.class);	2 ✔
49
50	private final MembershipOracle<I, D> mqs;
51	private final MembershipOracle<I, D> ceqs;
52	protected final Alphabet<I> alphabet;
53	protected SuffixTrie<I> strie;
54	protected PrefixTree<I, D> ptree;
55
56	protected AbstractTTTLambda(Alphabet<I> alphabet, MembershipOracle<I, D> mqs, MembershipOracle<I, D> ceqs) {	2 ✔
57	this.alphabet = alphabet;	2 ✔
58	this.mqs = mqs;	2 ✔
59	this.ceqs = ceqs;	2 ✔
60
61	this.strie = new SuffixTrie<>();	2 ✔
62	this.ptree = new PrefixTree<>();	2 ✔
63	}	2 ✔
64
65	protected abstract int maxSearchIndex(int ceLength);
66
67	protected abstract @Nullable DTLeaf<I, D> getState(Word<I> prefix);
68
69	protected abstract AbstractDecisionTree<I, D> dtree();
70
71	@Override
72	public void startLearning() {
73	assert dtree() != null && getHypothesisModel() != null;	2 ✔
74	dtree().sift(mqs, ptree.root());	2 ✔
75	makeConsistent(mqs);	2 ✔
76	}	2 ✔
77
78	@Override
79	public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
80	final Deque<DefaultQuery<I, D>> witnesses = new ArrayDeque<>();	2 ✔
81	witnesses.add(counterexample);	2 ✔
82	boolean refined = false;	2 ✔
83
84	while (MQUtil.isCounterexample(counterexample, getHypothesisModel())) {	2 ✔
85	final DefaultQuery<I, D> witness = witnesses.getFirst();	2 ✔
86
87	if (witness.getOutput() == null) {	2 ✔
88	witness.answer(ceqs.answerQuery(witness.getPrefix(), witness.getSuffix()));	2 ✔
89	}
90
91	final boolean valid = MQUtil.isCounterexample(witness, getHypothesisModel());	2 ✔
92
93	if (valid) {	2 ✔
94	analyzeCounterexample(witness, witnesses);	2 ✔
95	makeConsistent(mqs);	2 ✔
96	refined = true;	2 ✔
97	} else {
98	witnesses.pop();	2 ✔
99	}
100	}	2 ✔
101
102	assert size() == dtree().leaves().size();	2 ✔
103	return refined;	2 ✔
104	}
105
106	@Override
107	public void addAlphabetSymbol(I symbol) {
108	if (!this.alphabet.containsSymbol(symbol)) {	2 ✔
109	this.alphabet.asGrowingAlphabetOrThrowException().addSymbol(symbol);	2 ✔
110	}
111
112	// check if symbol is already part of ptree/hypothesis
113	if (ptree.root().succ(symbol) == null) {	2 ✔
114
115	List<DTLeaf<I, D>> leaves = dtree().leaves();	2 ✔
116
117	for (DTLeaf<I, D> leaf : leaves) {	2 ✔
118	PTNode<I, D> u = leaf.getShortPrefixes().get(0);	2 ✔
119	assert u != null;	2 ✔
120	PTNode<I, D> ua = u.append(symbol);	2 ✔
121	assert ua != null;	2 ✔
122	dtree().sift(mqs, ua);	2 ✔
123	}	2 ✔
124
125	makeConsistent(mqs);	2 ✔
126	}
127	}	2 ✔
128
129	protected void makeConsistent(MembershipOracle<I, D> oracle) {
130	while (dtree().makeConsistent(oracle)) {	2 ✔
131	// do nothing ...
132	}
133	}	2 ✔
134
135	private PTNode<I, D> longestShortPrefixOf(Word<I> ce) {
136	PTNode<I, D> cur = ptree.root();	2 ✔
137	int i = 0;	2 ✔
138	do {
139	cur = cur.succ(ce.getSymbol(i++));	2 ✔
140	assert cur != null;	2 ✔
141	} while (cur.state().getShortPrefixes().contains(cur) && i < ce.length());	2 ✔
142
143	assert !cur.state().getShortPrefixes().contains(cur);	2 ✔
144	return cur;	2 ✔
145	}
146
147	private void analyzeCounterexample(DefaultQuery<I, D> counterexample, Deque<DefaultQuery<I, D>> witnesses) {
148	M hyp = getHypothesisModel();	2 ✔
149	Word<I> ce = counterexample.getInput();	2 ✔
150	PTNode<I, D> ua = null;	2 ✔
151	PTNode<I, D> lsp = longestShortPrefixOf(ce);	2 ✔
152	int upper = maxSearchIndex(ce.length());	2 ✔
153	int lower = lsp.word().length() - 1;	2 ✔
154	while (upper - lower > 1) {	2 ✔
155	int mid = (upper + lower) / 2;	2 ✔
156	Word<I> prefix = ce.prefix(mid);	2 ✔
157	Word<I> suffix = ce.suffix(ce.length() - mid);	2 ✔
158
159	DTLeaf<I, D> q = getState(prefix);	2 ✔
160	assert q != null;	2 ✔
161
162	boolean stillCe = false;	2 ✔
163	for (PTNode<I, D> u : q.getShortPrefixes()) {	2 ✔
164	D sysOut = ceqs.answerQuery(u.word(), suffix);	2 ✔
165	D hypOut = hyp.computeSuffixOutput(u.word(), suffix);	2 ✔
166	if (!Objects.equals(sysOut, hypOut)) {	2 ✔
167	ua = u.succ(suffix.firstSymbol());	2 ✔
168	lower = mid;	2 ✔
169	stillCe = true;	2 ✔
170	break;	2 ✔
171	}
172	}	2 ✔
173	if (stillCe) {	2 ✔
174	continue;	2 ✔
175	}
176	upper = mid;	2 ✔
177	}	2 ✔
178
179	if (ua == null) {	2 ✔
180	assert lower == lsp.word().length() - 1;	2 ✔
181	ua = lsp;	2 ✔
182	}
183
184	// add witnesses
185	int mid = (upper + lower) / 2;	2 ✔
186	Word<I> sprime = ce.suffix(ce.length() - (mid + 1));	2 ✔
187	DTLeaf<I, D> qnext = getState(ua.word());	2 ✔
188	assert qnext != null;	2 ✔
189	for (PTNode<I, D> uprime : qnext.getShortPrefixes()) {	2 ✔
190	witnesses.push(new DefaultQuery<>(uprime.word(), sprime));	2 ✔
191	}	2 ✔
192	witnesses.push(new DefaultQuery<>(ua.word(), sprime));	2 ✔
193
194	ua.makeShortPrefix(mqs);	2 ✔
195	}	2 ✔
196
197	@Override
198	public TTTLambdaState<I, D> suspend() {
199	return new TTTLambdaState<>(strie, ptree, dtree());	2 ✔
200	}
201
202	@Override
203	public void resume(TTTLambdaState<I, D> state) {
204	this.strie = state.strie;	2 ✔
205	this.ptree = state.ptree;	2 ✔
206
207	final Alphabet<I> oldAlphabet = state.dtree.getAlphabet();	2 ✔
208	if (!this.alphabet.equals(oldAlphabet)) {	2 ✔
NEW 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	}
214	}	2 ✔
215	}

LearnLib / learnlib / 21987934897

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous