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

98.65

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

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;
import java.util.Set;

import de.learnlib.api.algorithm.LearningAlgorithm;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import net.automatalib.automata.concepts.InputAlphabetHolder;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;

abstract class AbstractOptimalLStar<M, I, D>
        implements LearningAlgorithm<M, I, D>, Hypothesis<I, D>, InputAlphabetHolder<I> {

    private final Alphabet<I> alphabet;
    final MembershipOracle<I, D> mqs;
    final MembershipOracle<I, D> ceqs;

    private final Set<Word<I>> shortPrefixes;
    private final Map<Word<I>, List<D>> rows;
    final List<Word<I>> suffixes;

    AbstractOptimalLStar(Alphabet<I> alphabet,
                         MembershipOracle<I, D> mqs,
                         MembershipOracle<I, D> ceqs,
                         List<Word<I>> initialSuffixes) {
        this.alphabet = alphabet;
        this.mqs = mqs;
        this.ceqs = ceqs;

        this.suffixes = new ArrayList<>(initialSuffixes);
        this.shortPrefixes = new HashSet<>();
        this.rows = new HashMap<>();
    }

    abstract int maxSearchIndex(int ceLength);

    abstract void automatonFromTable();

    abstract D suffix(D output, int length);

    abstract boolean symbolInconsistency(Word<I> u1, Word<I> u2, I a);

    @Override
    public void startLearning() {
        initTable();
        learnLoop();
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
        Set<DefaultQuery<I, D>> witnesses = new LinkedHashSet<>();
        witnesses.add(counterexample);
        boolean refined = refineWithWitness(counterexample, witnesses);
        if (!refined) {
            return false;
        }
        do {
            for (DefaultQuery<I, D> w : witnesses) {
                refined = refineWithWitness(w, witnesses);
                if (refined) {
                    break;
                }
            }

        } while (refined);
        assert size() == shortPrefixes.size();
        return true;
    }

    @Override
    public Alphabet<I> getInputAlphabet() {
        return alphabet;
    }

    private boolean refineWithWitness(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
        boolean valid = false;
        while (counterExampleValid(counterexample)) {
            valid = true;
            analyzeCounterexample(counterexample, witnesses);
            learnLoop();
        }

        return valid;
    }

    private void initTable() {
        Word<I> epsilon = Word.epsilon();
        List<D> rowData = initRow(epsilon);
        rows.put(epsilon, rowData);
        addShortPrefix(epsilon);
    }

    private void analyzeCounterexample(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
        Word<I> ceInput = counterexample.getInput();
        Word<I> ua = null;
        int upper = maxSearchIndex(ceInput.length());
        int lower = 0;
        D hypOut = getOutput(ceInput, ceInput.length());
        while (upper - lower > 1) {
            int mid = (upper + lower) / 2;

            Word<I> prefix = ceInput.prefix(mid);
            Word<I> suffix = ceInput.suffix(ceInput.length() - mid);
            List<D> rowData = rowForState(prefix);
            boolean stillCe = false;
            for (Word<I> u : getShortPrefixes(rowData)) {
                D sysOut = suffix(ceqs.answerQuery(u, suffix), suffix.length());
                if (!Objects.equals(sysOut, suffix(hypOut, suffix.size()))) {
                    ua = u.append(suffix.firstSymbol());
                    lower = mid;
                    stillCe = true;
                    break;
                }
            }
            if (stillCe) {
                continue;
            }
            upper = mid;
        }

        if (ua == null) {
            assert upper == 1;
            ua = ceInput.prefix(1);
        }

        // add witnesses
        int mid = (upper + lower) / 2;
        Word<I> sprime = ceInput.suffix(ceInput.length() - (mid + 1));
        List<D> rnext = getRow(ua);
        for (Word<I> uprime : getShortPrefixes(rnext)) {
            witnesses.add(new DefaultQuery<>(uprime, sprime, ceqs.answerQuery(uprime, sprime)));
        }
        witnesses.add(new DefaultQuery<>(ua, sprime, ceqs.answerQuery(ua, sprime)));

        addShortPrefix(ua);
    }

    private boolean counterExampleValid(DefaultQuery<I, D> counterexample) {
        assert !counterexample.getSuffix().isEmpty();
        D hypOut = getOutput(counterexample.getInput(), counterexample.getSuffix().length());
        return !Objects.equals(hypOut, counterexample.getOutput());
    }

    private void learnLoop() {
        while (findInconsistency() || findUnclosedness()) {
            completeObservations();
        }
        automatonFromTable();
    }

    private boolean findInconsistency() {
        List<Word<I>> shortAsList = new ArrayList<>(shortPrefixes);
        for (int left = 0; left < shortAsList.size() - 1; left++) {
            for (int right = left + 1; right < shortAsList.size(); right++) {
                if (findInconsistency(shortAsList.get(left), shortAsList.get(right))) {
                    return true;
                }
            }
        }
        return false;
    }

    private boolean findInconsistency(Word<I> u1, Word<I> u2) {
        List<D> rowData1 = rows.get(u1);
        List<D> rowData2 = rows.get(u2);
        if (!Objects.equals(rowData1, rowData2)) {
            return false;
        }
        for (I a : alphabet) {
            rowData1 = rows.get(u1.append(a));
            rowData2 = rows.get(u2.append(a));
            assert rowData1 != null && rowData2 != null;
            if (!rowData1.equals(rowData2)) {
                for (int i = 0; i < rowData1.size(); i++) {
                    if (!Objects.equals(rowData1.get(i), rowData2.get(i))) {
                        Word<I> newSuffx = suffixes.get(i).prepend(a);
                        suffixes.add(newSuffx);
                        return true;
                    }
                }
            }
            if (symbolInconsistency(u1, u2, a)) {
                return true;
            }
        }
        return false;
    }

    private List<Word<I>> getShortPrefixes(Word<I> prefix) {
        List<D> rowData = rows.get(prefix);
        assert rowData != null;
        return getShortPrefixes(rowData);
    }

    List<Word<I>> getShortPrefixes(List<D> rowData) {
        List<Word<I>> shortReps = new ArrayList<>();
        for (Entry<Word<I>, List<D>> e : rows.entrySet()) {
            if (shortPrefixes.contains(e.getKey()) && rowData.equals(e.getValue())) {
                shortReps.add(e.getKey());
            }
        }
        return shortReps;
    }

    Collection<Word<I>> getShortPrefixes() {
        return shortPrefixes;
    }

    List<D> getRow(Word<I> key) {
        List<D> row = rows.get(key);
        assert row != null;
        return row;
    }

    private boolean findUnclosedness() {
        for (Word<I> prefix : rows.keySet()) {
            List<Word<I>> shortReps = getShortPrefixes(prefix);
            if (shortReps.isEmpty()) {
                addShortPrefix(prefix);
                return true;
            }
        }
        return false;
    }

    private void completeObservations() {
        for (Entry<Word<I>, List<D>> e : rows.entrySet()) {
            List<D> rowData = completeRow(e.getKey(), e.getValue());
            e.setValue(rowData);
        }
    }

    private List<D> initRow(Word<I> prefix) {
        List<D> rowData = new ArrayList<>(suffixes.size());
        for (Word<I> suffix : suffixes) {
            rowData.add(suffix(mqs.answerQuery(prefix, suffix), suffix.size()));

        }
        return rowData;
    }

    private List<D> completeRow(Word<I> prefix, List<D> oldData) {
        if (suffixes.size() == oldData.size()) {
            return oldData;
        }

        List<D> rowData = new ArrayList<>(suffixes.size());
        rowData.addAll(oldData);
        for (int i = oldData.size(); i < suffixes.size(); i++) {
            rowData.add(suffix(mqs.answerQuery(prefix, suffixes.get(i)), suffixes.get(i).size()));
        }
        return rowData;
    }

    private void addShortPrefix(Word<I> shortPrefix) {
        assert !shortPrefixes.contains(shortPrefix) && rows.containsKey(shortPrefix);

        shortPrefixes.add(shortPrefix);
        for (I a : alphabet) {
            Word<I> newPrefix = shortPrefix.append(a);
            List<D> rowData = initRow(newPrefix);
            rows.put(newPrefix, rowData);
        }
    }
}

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.oml.lstar;
17
18	import java.util.ArrayList;
19	import java.util.Collection;
20	import java.util.HashMap;
21	import java.util.HashSet;
22	import java.util.LinkedHashSet;
23	import java.util.List;
24	import java.util.Map;
25	import java.util.Map.Entry;
26	import java.util.Objects;
27	import java.util.Set;
28
29	import de.learnlib.api.algorithm.LearningAlgorithm;
30	import de.learnlib.api.oracle.MembershipOracle;
31	import de.learnlib.api.query.DefaultQuery;
32	import net.automatalib.automata.concepts.InputAlphabetHolder;
33	import net.automatalib.words.Alphabet;
34	import net.automatalib.words.Word;
35
36	abstract class AbstractOptimalLStar<M, I, D>	2✔
37	implements LearningAlgorithm<M, I, D>, Hypothesis<I, D>, InputAlphabetHolder<I> {
38
39	private final Alphabet<I> alphabet;
40	final MembershipOracle<I, D> mqs;
41	final MembershipOracle<I, D> ceqs;
42
43	private final Set<Word<I>> shortPrefixes;
44	private final Map<Word<I>, List<D>> rows;
45	final List<Word<I>> suffixes;
46
47	AbstractOptimalLStar(Alphabet<I> alphabet,
48	MembershipOracle<I, D> mqs,
49	MembershipOracle<I, D> ceqs,
50	List<Word<I>> initialSuffixes) {	2✔
51	this.alphabet = alphabet;	2✔
52	this.mqs = mqs;	2✔
53	this.ceqs = ceqs;	2✔
54
55	this.suffixes = new ArrayList<>(initialSuffixes);	2✔
56	this.shortPrefixes = new HashSet<>();	2✔
57	this.rows = new HashMap<>();	2✔
58	}	2✔
59
60	abstract int maxSearchIndex(int ceLength);
61
62	abstract void automatonFromTable();
63
64	abstract D suffix(D output, int length);
65
66	abstract boolean symbolInconsistency(Word<I> u1, Word<I> u2, I a);
67
68	@Override
69	public void startLearning() {
70	initTable();	2✔
71	learnLoop();	2✔
72	}	2✔
73
74	@Override
75	public boolean refineHypothesis(DefaultQuery<I, D> counterexample) {
76	Set<DefaultQuery<I, D>> witnesses = new LinkedHashSet<>();	2✔
77	witnesses.add(counterexample);	2✔
78	boolean refined = refineWithWitness(counterexample, witnesses);	2✔
79	if (!refined) {	2✔
80	return false;	×
81	}
82	do {
83	for (DefaultQuery<I, D> w : witnesses) {	2✔
84	refined = refineWithWitness(w, witnesses);	2✔
85	if (refined) {	2✔
86	break;	×
87	}
88	}	2✔
89
90	} while (refined);	2✔
91	assert size() == shortPrefixes.size();	2✔
92	return true;	2✔
93	}
94
95	@Override
96	public Alphabet<I> getInputAlphabet() {
97	return alphabet;	2✔
98	}
99
100	private boolean refineWithWitness(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
101	boolean valid = false;	2✔
102	while (counterExampleValid(counterexample)) {	2✔
103	valid = true;	2✔
104	analyzeCounterexample(counterexample, witnesses);	2✔
105	learnLoop();	2✔
106	}
107
108	return valid;	2✔
109	}
110
111	private void initTable() {
112	Word<I> epsilon = Word.epsilon();	2✔
113	List<D> rowData = initRow(epsilon);	2✔
114	rows.put(epsilon, rowData);	2✔
115	addShortPrefix(epsilon);	2✔
116	}	2✔
117
118	private void analyzeCounterexample(DefaultQuery<I, D> counterexample, Set<DefaultQuery<I, D>> witnesses) {
119	Word<I> ceInput = counterexample.getInput();	2✔
120	Word<I> ua = null;	2✔
121	int upper = maxSearchIndex(ceInput.length());	2✔
122	int lower = 0;	2✔
123	D hypOut = getOutput(ceInput, ceInput.length());	2✔
124	while (upper - lower > 1) {	2✔
125	int mid = (upper + lower) / 2;	2✔
126
127	Word<I> prefix = ceInput.prefix(mid);	2✔
128	Word<I> suffix = ceInput.suffix(ceInput.length() - mid);	2✔
129	List<D> rowData = rowForState(prefix);	2✔
130	boolean stillCe = false;	2✔
131	for (Word<I> u : getShortPrefixes(rowData)) {	2✔
132	D sysOut = suffix(ceqs.answerQuery(u, suffix), suffix.length());	2✔
133	if (!Objects.equals(sysOut, suffix(hypOut, suffix.size()))) {	2✔
134	ua = u.append(suffix.firstSymbol());	2✔
135	lower = mid;	2✔
136	stillCe = true;	2✔
137	break;	2✔
138	}
139	}	2✔
140	if (stillCe) {	2✔
141	continue;	2✔
142	}
143	upper = mid;	2✔
144	}	2✔
145
146	if (ua == null) {	2✔
147	assert upper == 1;	2✔
148	ua = ceInput.prefix(1);	2✔
149	}
150
151	// add witnesses
152	int mid = (upper + lower) / 2;	2✔
153	Word<I> sprime = ceInput.suffix(ceInput.length() - (mid + 1));	2✔
154	List<D> rnext = getRow(ua);	2✔
155	for (Word<I> uprime : getShortPrefixes(rnext)) {	2✔
156	witnesses.add(new DefaultQuery<>(uprime, sprime, ceqs.answerQuery(uprime, sprime)));	2✔
157	}	2✔
158	witnesses.add(new DefaultQuery<>(ua, sprime, ceqs.answerQuery(ua, sprime)));	2✔
159
160	addShortPrefix(ua);	2✔
161	}	2✔
162
163	private boolean counterExampleValid(DefaultQuery<I, D> counterexample) {
164	assert !counterexample.getSuffix().isEmpty();	2✔
165	D hypOut = getOutput(counterexample.getInput(), counterexample.getSuffix().length());	2✔
166	return !Objects.equals(hypOut, counterexample.getOutput());	2✔
167	}
168
169	private void learnLoop() {
170	while (findInconsistency() \|\| findUnclosedness()) {	2✔
171	completeObservations();	2✔
172	}
173	automatonFromTable();	2✔
174	}	2✔
175
176	private boolean findInconsistency() {
177	List<Word<I>> shortAsList = new ArrayList<>(shortPrefixes);	2✔
178	for (int left = 0; left < shortAsList.size() - 1; left++) {	2✔
179	for (int right = left + 1; right < shortAsList.size(); right++) {	2✔
180	if (findInconsistency(shortAsList.get(left), shortAsList.get(right))) {	2✔
181	return true;	2✔
182	}
183	}
184	}
185	return false;	2✔
186	}
187
188	private boolean findInconsistency(Word<I> u1, Word<I> u2) {
189	List<D> rowData1 = rows.get(u1);	2✔
190	List<D> rowData2 = rows.get(u2);	2✔
191	if (!Objects.equals(rowData1, rowData2)) {	2✔
192	return false;	2✔
193	}
194	for (I a : alphabet) {	2✔
195	rowData1 = rows.get(u1.append(a));	2✔
196	rowData2 = rows.get(u2.append(a));	2✔
197	assert rowData1 != null && rowData2 != null;	2✔
198	if (!rowData1.equals(rowData2)) {	2✔
199	for (int i = 0; i < rowData1.size(); i++) {	2✔
200	if (!Objects.equals(rowData1.get(i), rowData2.get(i))) {	2✔
201	Word<I> newSuffx = suffixes.get(i).prepend(a);	2✔
202	suffixes.add(newSuffx);	2✔
203	return true;	2✔
204	}
205	}
206	}
207	if (symbolInconsistency(u1, u2, a)) {	2✔
208	return true;	2✔
209	}
210	}	2✔
211	return false;	2✔
212	}
213
214	private List<Word<I>> getShortPrefixes(Word<I> prefix) {
215	List<D> rowData = rows.get(prefix);	2✔
216	assert rowData != null;	2✔
217	return getShortPrefixes(rowData);	2✔
218	}
219
220	List<Word<I>> getShortPrefixes(List<D> rowData) {
221	List<Word<I>> shortReps = new ArrayList<>();	2✔
222	for (Entry<Word<I>, List<D>> e : rows.entrySet()) {	2✔
223	if (shortPrefixes.contains(e.getKey()) && rowData.equals(e.getValue())) {	2✔
224	shortReps.add(e.getKey());	2✔
225	}
226	}	2✔
227	return shortReps;	2✔
228	}
229
230	Collection<Word<I>> getShortPrefixes() {
231	return shortPrefixes;	2✔
232	}
233
234	List<D> getRow(Word<I> key) {
235	List<D> row = rows.get(key);	2✔
236	assert row != null;	2✔
237	return row;	2✔
238	}
239
240	private boolean findUnclosedness() {
241	for (Word<I> prefix : rows.keySet()) {	2✔
242	List<Word<I>> shortReps = getShortPrefixes(prefix);	2✔
243	if (shortReps.isEmpty()) {	2✔
244	addShortPrefix(prefix);	2✔
245	return true;	2✔
246	}
247	}	2✔
248	return false;	2✔
249	}
250
251	private void completeObservations() {
252	for (Entry<Word<I>, List<D>> e : rows.entrySet()) {	2✔
253	List<D> rowData = completeRow(e.getKey(), e.getValue());	2✔
254	e.setValue(rowData);	2✔
255	}	2✔
256	}	2✔
257
258	private List<D> initRow(Word<I> prefix) {
259	List<D> rowData = new ArrayList<>(suffixes.size());	2✔
260	for (Word<I> suffix : suffixes) {	2✔
261	rowData.add(suffix(mqs.answerQuery(prefix, suffix), suffix.size()));	2✔
262
263	}	2✔
264	return rowData;	2✔
265	}
266
267	private List<D> completeRow(Word<I> prefix, List<D> oldData) {
268	if (suffixes.size() == oldData.size()) {	2✔
269	return oldData;	2✔
270	}
271
272	List<D> rowData = new ArrayList<>(suffixes.size());	2✔
273	rowData.addAll(oldData);	2✔
274	for (int i = oldData.size(); i < suffixes.size(); i++) {	2✔
275	rowData.add(suffix(mqs.answerQuery(prefix, suffixes.get(i)), suffixes.get(i).size()));	2✔
276	}
277	return rowData;	2✔
278	}
279
280	private void addShortPrefix(Word<I> shortPrefix) {
281	assert !shortPrefixes.contains(shortPrefix) && rows.containsKey(shortPrefix);	2✔
282
283	shortPrefixes.add(shortPrefix);	2✔
284	for (I a : alphabet) {	2✔
285	Word<I> newPrefix = shortPrefix.append(a);	2✔
286	List<D> rowData = initRow(newPrefix);	2✔
287	rows.put(newPrefix, rowData);	2✔
288	}	2✔
289	}	2✔
290	}

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