31619759710

Committed 12 Aug 2026 04:27PM UTC coverage: 95.488% (+1.1%) from 94.368%

Build # 31619759710

Build Type

push

github

Committed by

mtf90

Commit Message

use new version scheme

Coverage Stats

15533 of 16267 relevant lines covered (95.49%)

1.72 hits per line

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

99.07

/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.AccessSequenceTransformer;
import de.learnlib.LearnerStateTracker;
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>,
                                                                                       AccessSequenceTransformer<I>,
                                                                                       SupportsGrowingAlphabet<I>,
                                                                                       Resumable<TTTLambdaState<I, D>>,
                                                                                       FiniteRepresentation,
                                                                                       LearnerStateTracker {

    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;
    private boolean started;

    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<>();

        this.started = false;
    }

    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() {
        requireLearningProcessNotStarted();
        dtree().sift(mqs, ptree.root());
        makeConsistent(mqs);
        started = true;
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
        requireLearningProcessStarted();

        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 boolean hasLearningProcessStarted() {
        return started;
    }

    @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);
        }
    }

    @Override
    public Word<I> transformAccessSequence(Word<I> word) {
        requireLearningProcessStarted();

        DTLeaf<I, D> state = getState(word);
        assert state != null;
        List<PTNode<I, D>> shortPrefixes = state.getShortPrefixes();

        assert shortPrefixes.size() == 1;

        return shortPrefixes.get(0).word();
    }

    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(), started);
    }

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

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

LearnLib / learnlib / 31619759710

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