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

81.82

/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/AbstractLStar.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.lstar;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.Objects;

import de.learnlib.AccessSequenceTransformer;
import de.learnlib.LearnerStateTracker;
import de.learnlib.algorithm.GlobalSuffixLearner;
import de.learnlib.algorithm.lstar.ce.ObservationTableCEXHandlers;
import de.learnlib.datastructure.observationtable.GenericObservationTable;
import de.learnlib.datastructure.observationtable.Inconsistency;
import de.learnlib.datastructure.observationtable.OTLearner;
import de.learnlib.datastructure.observationtable.ObservationTable;
import de.learnlib.datastructure.observationtable.Row;
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.SuffixOutput;
import net.automatalib.word.Word;

/**
 * An abstract base class for L*-style algorithms.
 * <p>
 * This class implements basic management features (table, alphabet, oracle) and the main loop of alternating
 * completeness and consistency checks. It does not take care of choosing how to initialize the table and hypothesis
 * construction.
 *
 * @param <A>
 *         automaton type
 * @param <I>
 *         input symbol type
 * @param <D>
 *         output domain type
 */
public abstract class AbstractLStar<A, I, D> implements OTLearner<A, I, D>,
                                                        GlobalSuffixLearner<A, I, D>,
                                                        AccessSequenceTransformer<I>,
                                                        SupportsGrowingAlphabet<I>,
                                                        LearnerStateTracker {

    protected final Alphabet<I> alphabet;
    protected final MembershipOracle<I, D> oracle;
    protected GenericObservationTable<I, D> table;

    /**
     * Constructor.
     *
     * @param alphabet
     *         the learning alphabet.
     * @param oracle
     *         the membership oracle.
     */
    protected AbstractLStar(Alphabet<I> alphabet, MembershipOracle<I, D> oracle) {
        this.alphabet = alphabet;
        this.oracle = oracle;
        this.table = new GenericObservationTable<>(alphabet);
    }

    @Override
    public void startLearning() {
        requireLearningProcessNotStarted();
        List<Word<I>> prefixes = initialPrefixes();
        List<Word<I>> suffixes = initialSuffixes();
        List<List<Row<I>>> initialUnclosed = table.initialize(prefixes, suffixes, oracle);

        completeConsistentTable(initialUnclosed, table.isInitialConsistencyCheckRequired());
    }

    @Override
    public final boolean refineHypothesis(DefaultQuery<I, D> ceQuery) {
        requireLearningProcessStarted();
        if (!MQUtil.isCounterexample(ceQuery, hypothesisOutput())) {
            return false;
        }
        int oldDistinctRows = table.numberOfDistinctRows();
        doRefineHypothesis(ceQuery);
        assert table.numberOfDistinctRows() > oldDistinctRows;
        return true;
    }

    protected abstract SuffixOutput<I, D> hypothesisOutput();

    protected void doRefineHypothesis(DefaultQuery<I, D> ceQuery) {
        List<List<Row<I>>> unclosed = incorporateCounterExample(ceQuery);
        completeConsistentTable(unclosed, true);
    }

    /**
     * Incorporates the information provided by a counterexample into the observation data structure.
     *
     * @param ce
     *         the query which contradicts the hypothesis
     *
     * @return the rows (equivalence classes) which became unclosed by adding the information.
     */
    protected List<List<Row<I>>> incorporateCounterExample(DefaultQuery<I, D> ce) {
        return ObservationTableCEXHandlers.handleClassicLStar(ce, table, oracle);
    }

    protected List<Word<I>> initialPrefixes() {
        return Collections.singletonList(Word.epsilon());
    }

    /**
     * Returns the list of initial suffixes which are used to initialize the table.
     *
     * @return the list of initial suffixes.
     */
    protected abstract List<Word<I>> initialSuffixes();

    /**
     * Iteratively checks for unclosedness and inconsistencies in the table, and fixes any occurrences thereof. This
     * process is repeated until the observation table is both closed and consistent.
     *
     * @param unclosed
     *         the unclosed rows (equivalence classes) to start with.
     * @param checkConsistency
     *         a flag indicating whether consistency should be checked as well. If {@code false}, only closedness is
     *         ensured.
     *
     * @return {@code true} if unclosed rows have been closed, {@code false} otherwise
     */
    protected boolean completeConsistentTable(List<List<Row<I>>> unclosed, boolean checkConsistency) {
        boolean refined = false;
        List<List<Row<I>>> unclosedIter = unclosed;
        do {
            while (!unclosedIter.isEmpty()) {
                List<Row<I>> closingRows = selectClosingRows(unclosedIter);
                unclosedIter = table.toShortPrefixes(closingRows, oracle);
                refined = true;
            }

            if (checkConsistency) {
                Inconsistency<I> incons;

                do {
                    incons = table.findInconsistency();
                    if (incons != null) {
                        Word<I> newSuffix = analyzeInconsistency(incons);
                        unclosedIter = table.addSuffix(newSuffix, oracle);
                    }
                } while (unclosedIter.isEmpty() && incons != null);
            }
        } while (!unclosedIter.isEmpty());

        return refined;
    }

    /**
     * This method selects a set of rows to use for closing the table. It receives as input a list of row lists, such
     * that each (inner) list contains long prefix rows with (currently) identical contents, which have no matching
     * short prefix row. The outer list is the list of all those equivalence classes.
     *
     * @param unclosed
     *         a list of equivalence classes of unclosed rows.
     *
     * @return a list containing a representative row from each class to move to the short prefix part.
     */
    protected List<Row<I>> selectClosingRows(List<List<Row<I>>> unclosed) {
        List<Row<I>> closingRows = new ArrayList<>(unclosed.size());

        for (List<Row<I>> rowList : unclosed) {
            closingRows.add(rowList.get(0));
        }

        return closingRows;
    }

    /**
     * Analyzes an inconsistency. This analysis consists in determining the column in which the two successor rows
     * differ.
     *
     * @param incons
     *         the inconsistency description
     *
     * @return the suffix to add in order to fix the inconsistency
     */
    protected Word<I> analyzeInconsistency(Inconsistency<I> incons) {
        int inputIdx = alphabet.getSymbolIndex(incons.getSymbol());

        Row<I> succRow1 = incons.getFirstRow().getSuccessor(inputIdx);
        Row<I> succRow2 = incons.getSecondRow().getSuccessor(inputIdx);

        int numSuffixes = table.getSuffixes().size();

        for (int i = 0; i < numSuffixes; i++) {
            D val1 = table.cellContents(succRow1, i), val2 = table.cellContents(succRow2, i);
            if (!Objects.equals(val1, val2)) {
                I sym = alphabet.getSymbol(inputIdx);
                Word<I> suffix = table.getSuffixes().get(i);
                return suffix.prepend(sym);
            }
        }

        throw new IllegalArgumentException("Bogus inconsistency");
    }

    @Override
    public Collection<Word<I>> getGlobalSuffixes() {
        return Collections.unmodifiableCollection(table.getSuffixes());
    }

    @Override
    public boolean addGlobalSuffixes(Collection<? extends Word<I>> newGlobalSuffixes) {
        List<List<Row<I>>> unclosed = table.addSuffixes(newGlobalSuffixes, oracle);
        return !unclosed.isEmpty() && completeConsistentTable(unclosed, false);
    }

    @Override
    public ObservationTable<I, D> getObservationTable() {
        return table;
    }

    @Override
    public boolean hasLearningProcessStarted() {
        return this.table.isInitialized();
    }

    @Override
    public void addAlphabetSymbol(I symbol) {

        if (!this.alphabet.containsSymbol(symbol)) {
            this.alphabet.asGrowingAlphabetOrThrowException().addSymbol(symbol);
        }

        final List<List<Row<I>>> unclosed = this.table.addAlphabetSymbol(symbol, oracle);
        completeConsistentTable(unclosed, true);
    }

    @Override
    public Word<I> transformAccessSequence(Word<I> word) {
        return this.table.transformAccessSequence(word);
    }
}

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.lstar;
17
18	import java.util.ArrayList;
19	import java.util.Collection;
20	import java.util.Collections;
21	import java.util.List;
22	import java.util.Objects;
23
24	import de.learnlib.AccessSequenceTransformer;
25	import de.learnlib.LearnerStateTracker;
26	import de.learnlib.algorithm.GlobalSuffixLearner;
27	import de.learnlib.algorithm.lstar.ce.ObservationTableCEXHandlers;
28	import de.learnlib.datastructure.observationtable.GenericObservationTable;
29	import de.learnlib.datastructure.observationtable.Inconsistency;
30	import de.learnlib.datastructure.observationtable.OTLearner;
31	import de.learnlib.datastructure.observationtable.ObservationTable;
32	import de.learnlib.datastructure.observationtable.Row;
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.SuffixOutput;
39	import net.automatalib.word.Word;
40
41	/**
42	* An abstract base class for L*-style algorithms.
43	* <p>
44	* This class implements basic management features (table, alphabet, oracle) and the main loop of alternating
45	* completeness and consistency checks. It does not take care of choosing how to initialize the table and hypothesis
46	* construction.
47	*
48	* @param <A>
49	* automaton type
50	* @param <I>
51	* input symbol type
52	* @param <D>
53	* output domain type
54	*/
55	public abstract class AbstractLStar<A, I, D> implements OTLearner<A, I, D>,	2✔
56	GlobalSuffixLearner<A, I, D>,
57	AccessSequenceTransformer<I>,
58	SupportsGrowingAlphabet<I>,
59	LearnerStateTracker {
60
61	protected final Alphabet<I> alphabet;
62	protected final MembershipOracle<I, D> oracle;
63	protected GenericObservationTable<I, D> table;
64
65	/**
66	* Constructor.
67	*
68	* @param alphabet
69	* the learning alphabet.
70	* @param oracle
71	* the membership oracle.
72	*/
73	protected AbstractLStar(Alphabet<I> alphabet, MembershipOracle<I, D> oracle) {	2✔
74	this.alphabet = alphabet;	2✔
75	this.oracle = oracle;	2✔
76	this.table = new GenericObservationTable<>(alphabet);	2✔
77	}	2✔
78
79	@Override
80	public void startLearning() {
81	requireLearningProcessNotStarted();	2✔
82	List<Word<I>> prefixes = initialPrefixes();	2✔
83	List<Word<I>> suffixes = initialSuffixes();	2✔
84	List<List<Row<I>>> initialUnclosed = table.initialize(prefixes, suffixes, oracle);	2✔
85
86	completeConsistentTable(initialUnclosed, table.isInitialConsistencyCheckRequired());	2✔
87	}	2✔
88
89	@Override
90	public final boolean refineHypothesis(DefaultQuery<I, D> ceQuery) {
91	requireLearningProcessStarted();	2✔
92	if (!MQUtil.isCounterexample(ceQuery, hypothesisOutput())) {	2✔
93	return false;	2✔
94	}
95	int oldDistinctRows = table.numberOfDistinctRows();	2✔
96	doRefineHypothesis(ceQuery);	2✔
97	assert table.numberOfDistinctRows() > oldDistinctRows;	2✔
98	return true;	2✔
99	}
100
101	protected abstract SuffixOutput<I, D> hypothesisOutput();
102
103	protected void doRefineHypothesis(DefaultQuery<I, D> ceQuery) {
104	List<List<Row<I>>> unclosed = incorporateCounterExample(ceQuery);	×
105	completeConsistentTable(unclosed, true);	×
106	}	×
107
108	/**
109	* Incorporates the information provided by a counterexample into the observation data structure.
110	*
111	* @param ce
112	* the query which contradicts the hypothesis
113	*
114	* @return the rows (equivalence classes) which became unclosed by adding the information.
115	*/
116	protected List<List<Row<I>>> incorporateCounterExample(DefaultQuery<I, D> ce) {
117	return ObservationTableCEXHandlers.handleClassicLStar(ce, table, oracle);	×
118	}
119
120	protected List<Word<I>> initialPrefixes() {
121	return Collections.singletonList(Word.epsilon());	×
122	}
123
124	/**
125	* Returns the list of initial suffixes which are used to initialize the table.
126	*
127	* @return the list of initial suffixes.
128	*/
129	protected abstract List<Word<I>> initialSuffixes();
130
131	/**
132	* Iteratively checks for unclosedness and inconsistencies in the table, and fixes any occurrences thereof. This
133	* process is repeated until the observation table is both closed and consistent.
134	*
135	* @param unclosed
136	* the unclosed rows (equivalence classes) to start with.
137	* @param checkConsistency
138	* a flag indicating whether consistency should be checked as well. If {@code false}, only closedness is
139	* ensured.
140	*
141	* @return {@code true} if unclosed rows have been closed, {@code false} otherwise
142	*/
143	protected boolean completeConsistentTable(List<List<Row<I>>> unclosed, boolean checkConsistency) {
144	boolean refined = false;	2✔
145	List<List<Row<I>>> unclosedIter = unclosed;	2✔
146	do {
147	while (!unclosedIter.isEmpty()) {	2✔
148	List<Row<I>> closingRows = selectClosingRows(unclosedIter);	2✔
149	unclosedIter = table.toShortPrefixes(closingRows, oracle);	2✔
150	refined = true;	2✔
151	}	2✔
152
153	if (checkConsistency) {	2✔
154	Inconsistency<I> incons;
155
156	do {
157	incons = table.findInconsistency();	2✔
158	if (incons != null) {	2✔
159	Word<I> newSuffix = analyzeInconsistency(incons);	2✔
160	unclosedIter = table.addSuffix(newSuffix, oracle);	2✔
161	}
162	} while (unclosedIter.isEmpty() && incons != null);	2✔
163	}
164	} while (!unclosedIter.isEmpty());	2✔
165
166	return refined;	2✔
167	}
168
169	/**
170	* This method selects a set of rows to use for closing the table. It receives as input a list of row lists, such
171	* that each (inner) list contains long prefix rows with (currently) identical contents, which have no matching
172	* short prefix row. The outer list is the list of all those equivalence classes.
173	*
174	* @param unclosed
175	* a list of equivalence classes of unclosed rows.
176	*
177	* @return a list containing a representative row from each class to move to the short prefix part.
178	*/
179	protected List<Row<I>> selectClosingRows(List<List<Row<I>>> unclosed) {
180	List<Row<I>> closingRows = new ArrayList<>(unclosed.size());	×
181
182	for (List<Row<I>> rowList : unclosed) {	×
183	closingRows.add(rowList.get(0));	×
184	}	×
185
186	return closingRows;	×
187	}
188
189	/**
190	* Analyzes an inconsistency. This analysis consists in determining the column in which the two successor rows
191	* differ.
192	*
193	* @param incons
194	* the inconsistency description
195	*
196	* @return the suffix to add in order to fix the inconsistency
197	*/
198	protected Word<I> analyzeInconsistency(Inconsistency<I> incons) {
199	int inputIdx = alphabet.getSymbolIndex(incons.getSymbol());	2✔
200
201	Row<I> succRow1 = incons.getFirstRow().getSuccessor(inputIdx);	2✔
202	Row<I> succRow2 = incons.getSecondRow().getSuccessor(inputIdx);	2✔
203
204	int numSuffixes = table.getSuffixes().size();	2✔
205
206	for (int i = 0; i < numSuffixes; i++) {	2✔
207	D val1 = table.cellContents(succRow1, i), val2 = table.cellContents(succRow2, i);	2✔
208	if (!Objects.equals(val1, val2)) {	2✔
209	I sym = alphabet.getSymbol(inputIdx);	2✔
210	Word<I> suffix = table.getSuffixes().get(i);	2✔
211	return suffix.prepend(sym);	2✔
212	}
213	}
214
215	throw new IllegalArgumentException("Bogus inconsistency");	×
216	}
217
218	@Override
219	public Collection<Word<I>> getGlobalSuffixes() {
220	return Collections.unmodifiableCollection(table.getSuffixes());	×
221	}
222
223	@Override
224	public boolean addGlobalSuffixes(Collection<? extends Word<I>> newGlobalSuffixes) {
225	List<List<Row<I>>> unclosed = table.addSuffixes(newGlobalSuffixes, oracle);	2✔
226	return !unclosed.isEmpty() && completeConsistentTable(unclosed, false);	2✔
227	}
228
229	@Override
230	public ObservationTable<I, D> getObservationTable() {
231	return table;	2✔
232	}
233
234	@Override
235	public boolean hasLearningProcessStarted() {
236	return this.table.isInitialized();	2✔
237	}
238
239	@Override
240	public void addAlphabetSymbol(I symbol) {
241
242	if (!this.alphabet.containsSymbol(symbol)) {	2✔
243	this.alphabet.asGrowingAlphabetOrThrowException().addSymbol(symbol);	2✔
244	}
245
246	final List<List<Row<I>>> unclosed = this.table.addAlphabetSymbol(symbol, oracle);	2✔
247	completeConsistentTable(unclosed, true);	2✔
248	}	2✔
249
250	@Override
251	public Word<I> transformAccessSequence(Word<I> word) {
252	return this.table.transformAccessSequence(word);	2✔
253	}
254	}

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