6433387082

Committed 06 Oct 2023 03:10PM UTC coverage: 92.296% (-0.007%) from 92.303%

Build # 6433387082

Build Type

push

github

Committed by

mtf90

Commit Message

update Falk's developer id

Run Details

11573 of 12539 relevant lines covered (92.3%)

1.67 hits per line

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

81.25

/algorithms/active/lstar/src/main/java/de/learnlib/algorithms/lstar/AbstractLStar.java

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of LearnLib, http://www.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.algorithms.lstar;

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

import de.learnlib.algorithms.lstar.ce.ObservationTableCEXHandlers;
import de.learnlib.api.algorithm.feature.GlobalSuffixLearner;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
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.util.MQUtil;
import net.automatalib.SupportsGrowingAlphabet;
import net.automatalib.automata.concepts.SuffixOutput;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;

/**
 * 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>, SupportsGrowingAlphabet<I> {

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

    /**
     * Iteratedly 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.
     */
    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);
        if (unclosed.isEmpty()) {
            return false;
        }
        return completeConsistentTable(unclosed, false);
    }

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

    @Override
    public void addAlphabetSymbol(I symbol) {

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

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

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

LearnLib / learnlib / 6433387082

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