13166566074

Committed 05 Feb 2025 09:05PM UTC coverage: 94.368% (+0.04%) from 94.324%

Build # 13166566074

Build Type

push

github

Committed by

mtf90

Commit Message

test api conformance

when provided with a non-counterexample, refineHypothesis should return false and not throw an exception.

Run Details

12 of 12 new or added lines in 4 files covered. (100.0%)

19 existing lines in 4 files now uncovered.

12484 of 13229 relevant lines covered (94.37%)

1.72 hits per line

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

97.93

/algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/LSharpMealy.java

/* Copyright (C) 2013-2025 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.lsharp;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Random;
import java.util.Set;

import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
import de.learnlib.oracle.AdaptiveMembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.tooling.annotation.builder.GenerateBuilder;
import de.learnlib.util.mealy.MealyUtil;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.automaton.transducer.impl.CompactMealy;
import net.automatalib.common.util.Pair;
import net.automatalib.common.util.array.ArrayStorage;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Implementation of the L<sup>#</sup> algorithm for {@link MealyMachine}s. The implementation is based on the
 * <a href="https://gitlab.science.ru.nl/sws/lsharp/-/tree/8526fc3a88fa18b0c408d867385bcc9a29a302a1">original
 * implementation</a> of the authors. However, it does not support all features (such as compressed ADSs or some of the
 * more intricate equivalence checks on observation trees).
 *
 * @param <I>
 *         input symbol type
 * @param <O>
 *         output symbol type
 */
public class LSharpMealy<I, O> implements MealyLearner<I, O> {

    private final LSOracle<I, O> oqOracle;
    private final Alphabet<I> inputAlphabet;
    private final Set<Word<I>> basis;
    private final Map<Word<I>, List<Word<I>>> frontierToBasisMap;
    private final Map<Word<I>, Integer> basisMap;
    private final ArrayStorage<Word<I>> accessMap;

    @GenerateBuilder(defaults = BuilderDefaults.class)
    public LSharpMealy(Alphabet<I> alphabet,
                       AdaptiveMembershipOracle<I, O> oracle,
                       Rule2 rule2,
                       Rule3 rule3,
                       @Nullable Word<I> sinkState,
                       O sinkOutput,
                       Random random) {
        this.oqOracle = new LSOracle<>(oracle,
                                       new NormalObservationTree<>(alphabet),
                                       rule2,
                                       rule3,
                                       sinkState,
                                       sinkOutput,
                                       random);
        this.inputAlphabet = alphabet;
        this.basis = new LinkedHashSet<>();
        basis.add(Word.epsilon());
        this.frontierToBasisMap = new HashMap<>();
        this.basisMap = new HashMap<>();
        this.accessMap = new ArrayStorage<>();
    }

    public boolean processCex(DefaultQuery<I, Word<O>> cex, MealyMachine<Integer, I, ?, O> mealy) {
        assert cex != null;
        Word<I> ceInput = cex.getInput();
        Word<O> ceOutput = cex.getOutput();
        oqOracle.addObservation(ceInput, ceOutput);
        int prefixIndex = MealyUtil.findMismatch(mealy, ceInput, ceOutput);
        if (prefixIndex == MealyUtil.NO_MISMATCH) {
            return false;
        }
        this.processBinarySearch(ceInput.prefix(prefixIndex), ceOutput.prefix(prefixIndex), mealy);
        return true;
    }

    public void processBinarySearch(Word<I> ceInput, Word<O> ceOutput, MealyMachine<Integer, I, ?, O> mealy) {
        Integer r = oqOracle.getTree().getSucc(oqOracle.getTree().defaultState(), ceInput);
        assert r != null;
        this.updateFrontierAndBasis();
        Integer init = mealy.getInitialState();
        if (this.frontierToBasisMap.containsKey(ceInput) || basis.contains(ceInput) || init == null) {
            return;
        }

        Integer q = mealy.getSuccessor(init, ceInput);
        assert q != null;
        Word<I> accQT = accessMap.get(q);
        assert accQT != null;

        NormalObservationTree<I, O> oTree = oqOracle.getTree();
        Integer qt = oTree.getSucc(oTree.defaultState(), accQT);
        assert qt != null;

        int x = 0;
        for (Word<I> prefix : ceInput.prefixes(false)) {
            if (!prefix.isEmpty() && frontierToBasisMap.containsKey(prefix)) {
                x = prefix.length();
                break;
            }
        }

        assert x > 0;
        int y = ceInput.size();
        int h = Math.floorDiv(x + y, 2);

        Word<I> sigma1 = ceInput.prefix(h);
        Word<I> sigma2 = ceInput.suffix(ceInput.size() - h);
        Integer qp = mealy.getSuccessor(init, sigma1);
        assert qp != null;
        Word<I> accQPt = accessMap.get(qp);
        assert accQPt != null;

        Word<I> eta = ApartnessUtil.computeWitness(oTree, r, qt);
        assert eta != null;

        Word<I> outputQuery = accQPt.concat(sigma2).concat(eta);
        Word<O> sulResponse = oqOracle.outputQuery(outputQuery);
        Integer qpt = oTree.getSucc(oTree.defaultState(), accQPt);
        assert qpt != null;

        Integer rp = oTree.getSucc(oTree.defaultState(), sigma1);
        assert rp != null;

        Word<I> wit = ApartnessUtil.computeWitness(oTree, qpt, rp);
        if (wit != null) {
            processBinarySearch(sigma1, ceOutput.prefix(sigma1.length()), mealy);
        } else {
            Word<I> newInputs = accQPt.concat(sigma2);
            processBinarySearch(newInputs, sulResponse.prefix(newInputs.length()), mealy);
        }
    }

    public void makeObsTreeAdequate() {
        do {
            List<Pair<Word<I>, List<Word<I>>>> newFrontier = oqOracle.exploreFrontier(basis);
            for (Pair<Word<I>, List<Word<I>>> pair : newFrontier) {
                frontierToBasisMap.put(pair.getFirst(), pair.getSecond());
            }

            for (Entry<Word<I>, List<Word<I>>> entry : frontierToBasisMap.entrySet()) {
                if (entry.getValue().size() > 1) {
                    List<Word<I>> newCands = oqOracle.identifyFrontier(entry.getKey(), entry.getValue());
                    frontierToBasisMap.put(entry.getKey(), newCands);
                }
            }

            this.promoteFrontierState();
        } while (!this.treeIsAdequate());
    }

    public void promoteFrontierState() {
        Word<I> newBS = null;
        for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {
            if (e.getValue().isEmpty()) {
                newBS = e.getKey();
                break;
            }
        }
        if (newBS == null) {
            return;
        }

        Word<I> bs = Word.fromWords(newBS);
        basis.add(bs);
        frontierToBasisMap.remove(bs);
        NormalObservationTree<I, O> oTree = oqOracle.getTree();

        for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {
            if (!ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs)) {
                e.getValue().add(bs);
            }
        }
    }

    public boolean treeIsAdequate() {
        this.checkFrontierConsistency();

        for (List<Word<I>> value : frontierToBasisMap.values()) {
            if (value.size() != 1) {
                return false;
            }
        }

        NormalObservationTree<I, O> oTree = oqOracle.getTree();
        for (Word<I> b : basis) {
            for (I i : inputAlphabet) {
                Integer q = oTree.getSucc(oTree.defaultState(), b);
                if (q == null || oTree.getOut(q, i) == null) {
                    return false;
                }
            }
        }

        return true;
    }

    public void updateFrontierAndBasis() {
        NormalObservationTree<I, O> oTree = oqOracle.getTree();

        for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {
            e.getValue().removeIf(bs -> ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs));
        }

        this.promoteFrontierState();
        this.checkFrontierConsistency();

        for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {
            e.getValue().removeIf(bs -> ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs));
        }
    }

    public CompactMealy<I, O> buildHypothesis() {
        while (true) {
            this.makeObsTreeAdequate();
            CompactMealy<I, O> hyp = this.constructHypothesis();

            DefaultQuery<I, Word<O>> ce = this.checkConsistency(hyp);
            if (ce != null) {
                this.processCex(ce, hyp);
            } else {
                return hyp;
            }
        }
    }

    public CompactMealy<I, O> constructHypothesis() {

        CompactMealy<I, O> result = new CompactMealy<>(inputAlphabet, basis.size());
        basisMap.clear();
        accessMap.ensureCapacity(basis.size());

        for (Word<I> bAcc : basis) {
            Integer state = result.addState();
            basisMap.put(bAcc, state);
            accessMap.set(state, bAcc);
        }

        NormalObservationTree<I, O> oTree = oqOracle.getTree();
        for (Word<I> q : basis) {
            for (I i : inputAlphabet) {
                Integer bs = oTree.getSucc(oTree.defaultState(), q);
                assert bs != null;
                O output = oTree.getOut(bs, i);
                assert output != null;
                Word<I> fAcc = q.append(i);

                Pair<Word<I>, Boolean> pair = this.identifyFrontierOrBasis(fAcc);
                Word<I> dest = pair.getFirst();

                Integer hypBS = basisMap.get(q);
                assert hypBS != null;
                Integer hypDest = basisMap.get(dest);
                assert hypDest != null;
                result.addTransition(hypBS, i, hypDest, output);
            }
        }

        result.setInitialState(0);
        return result;
    }

    public Pair<Word<I>, Boolean> identifyFrontierOrBasis(Word<I> seq) {
        if (basis.contains(seq)) {
            return Pair.of(seq, false);
        }

        List<Word<I>> frontier = frontierToBasisMap.get(seq);
        assert frontier != null;
        return Pair.of(frontier.get(0), true);
    }

    public void initObsTree(@Nullable List<Pair<Word<I>, Word<O>>> logs) {
        if (logs != null) {
            for (Pair<Word<I>, Word<O>> pair : logs) {
                oqOracle.addObservation(pair.getFirst(), pair.getSecond());
            }
        }
    }

    public void checkFrontierConsistency() {
        List<Word<I>> basisSet = new ArrayList<>(basis);
        NormalObservationTree<I, O> oTree = oqOracle.getTree();

        for (Word<I> bs : basisSet) {
            for (I i : inputAlphabet) {
                Word<I> fsAcc = bs.append(i);
                if (oTree.getSucc(oTree.defaultState(), fsAcc) != null && !basis.contains(fsAcc) &&
                    !frontierToBasisMap.containsKey(fsAcc)) {
                    List<Word<I>> candidates = new ArrayList<>(basis.size());
                    for (Word<I> b : basis) {
                        if (!ApartnessUtil.accStatesAreApart(oTree, fsAcc, b)) {
                            candidates.add(b);
                        }
                    }
                    frontierToBasisMap.put(fsAcc, candidates);
                }
            }
        }
    }

    public @Nullable DefaultQuery<I, Word<O>> checkConsistency(MealyMachine<Integer, I, ?, O> mealy) {
        NormalObservationTree<I, O> oTree = oqOracle.getTree();
        Word<I> wit = ApartnessUtil.treeAndHypComputeWitness(oTree, oTree.defaultState(), mealy, 0);
        if (wit == null) {
            return null;
        }

        Word<O> os = oTree.getObservation(null, wit);
        assert os != null;
        return new DefaultQuery<>(wit, os);
    }

    @Override
    public void startLearning() {
        this.initObsTree(null);
        buildHypothesis();
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, Word<O>> ceQuery) {
        boolean result = processCex(ceQuery, constructHypothesis());
        buildHypothesis();
        return result;
    }

    @Override
    public MealyMachine<?, I, ?, O> getHypothesisModel() {
        return constructHypothesis();
    }

    static final class BuilderDefaults {

        private BuilderDefaults() {
            // prevent instantiation
        }

        public static Rule2 rule2() {
            return Rule2.ADS;
        }

        public static Rule3 rule3() {
            return Rule3.ADS;
        }

        public static <I> @Nullable Word<I> sinkState() {
            return null;
        }

        public static <O> @Nullable O sinkOutput() {
            return null;
        }

        public static Random random() {
            return new Random();
        }
    }
}

1	/* Copyright (C) 2013-2025 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.lsharp;
17
18	import java.util.ArrayList;
19	import java.util.HashMap;
20	import java.util.LinkedHashSet;
21	import java.util.List;
22	import java.util.Map;
23	import java.util.Map.Entry;
24	import java.util.Random;
25	import java.util.Set;
26
27	import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
28	import de.learnlib.oracle.AdaptiveMembershipOracle;
29	import de.learnlib.query.DefaultQuery;
30	import de.learnlib.tooling.annotation.builder.GenerateBuilder;
31	import de.learnlib.util.mealy.MealyUtil;
32	import net.automatalib.alphabet.Alphabet;
33	import net.automatalib.automaton.transducer.MealyMachine;
34	import net.automatalib.automaton.transducer.impl.CompactMealy;
35	import net.automatalib.common.util.Pair;
36	import net.automatalib.common.util.array.ArrayStorage;
37	import net.automatalib.word.Word;
38	import org.checkerframework.checker.nullness.qual.Nullable;
39
40	/**
41	* Implementation of the L<sup>#</sup> algorithm for {@link MealyMachine}s. The implementation is based on the
42	* <a href="https://gitlab.science.ru.nl/sws/lsharp/-/tree/8526fc3a88fa18b0c408d867385bcc9a29a302a1">original
43	* implementation</a> of the authors. However, it does not support all features (such as compressed ADSs or some of the
44	* more intricate equivalence checks on observation trees).
45	*
46	* @param <I>
47	* input symbol type
48	* @param <O>
49	* output symbol type
50	*/
51	public class LSharpMealy<I, O> implements MealyLearner<I, O> {	2✔
52
53	private final LSOracle<I, O> oqOracle;
54	private final Alphabet<I> inputAlphabet;
55	private final Set<Word<I>> basis;
56	private final Map<Word<I>, List<Word<I>>> frontierToBasisMap;
57	private final Map<Word<I>, Integer> basisMap;
58	private final ArrayStorage<Word<I>> accessMap;
59
60	@GenerateBuilder(defaults = BuilderDefaults.class)
61	public LSharpMealy(Alphabet<I> alphabet,
62	AdaptiveMembershipOracle<I, O> oracle,
63	Rule2 rule2,
64	Rule3 rule3,
65	@Nullable Word<I> sinkState,
66	O sinkOutput,
67	Random random) {	2✔
68	this.oqOracle = new LSOracle<>(oracle,	2✔
69	new NormalObservationTree<>(alphabet),
70	rule2,
71	rule3,
72	sinkState,
73	sinkOutput,
74	random);
75	this.inputAlphabet = alphabet;	2✔
76	this.basis = new LinkedHashSet<>();	2✔
77	basis.add(Word.epsilon());	2✔
78	this.frontierToBasisMap = new HashMap<>();	2✔
79	this.basisMap = new HashMap<>();	2✔
80	this.accessMap = new ArrayStorage<>();	2✔
81	}	2✔
82
83	public boolean processCex(DefaultQuery<I, Word<O>> cex, MealyMachine<Integer, I, ?, O> mealy) {
84	assert cex != null;	2✔
85	Word<I> ceInput = cex.getInput();	2✔
86	Word<O> ceOutput = cex.getOutput();	2✔
87	oqOracle.addObservation(ceInput, ceOutput);	2✔
88	int prefixIndex = MealyUtil.findMismatch(mealy, ceInput, ceOutput);	2✔
89	if (prefixIndex == MealyUtil.NO_MISMATCH) {	2✔
90	return false;	2✔
91	}
92	this.processBinarySearch(ceInput.prefix(prefixIndex), ceOutput.prefix(prefixIndex), mealy);	2✔
93	return true;	2✔
94	}
95
96	public void processBinarySearch(Word<I> ceInput, Word<O> ceOutput, MealyMachine<Integer, I, ?, O> mealy) {
97	Integer r = oqOracle.getTree().getSucc(oqOracle.getTree().defaultState(), ceInput);	2✔
98	assert r != null;	2✔
99	this.updateFrontierAndBasis();	2✔
100	Integer init = mealy.getInitialState();	2✔
101	if (this.frontierToBasisMap.containsKey(ceInput) \|\| basis.contains(ceInput) \|\| init == null) {	2✔
102	return;	2✔
103	}
104
105	Integer q = mealy.getSuccessor(init, ceInput);	2✔
106	assert q != null;	2✔
107	Word<I> accQT = accessMap.get(q);	2✔
108	assert accQT != null;	2✔
109
110	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
111	Integer qt = oTree.getSucc(oTree.defaultState(), accQT);	2✔
112	assert qt != null;	2✔
113
114	int x = 0;	2✔
115	for (Word<I> prefix : ceInput.prefixes(false)) {	2✔
116	if (!prefix.isEmpty() && frontierToBasisMap.containsKey(prefix)) {	2✔
117	x = prefix.length();	2✔
118	break;	2✔
119	}
120	}	2✔
121
122	assert x > 0;	2✔
123	int y = ceInput.size();	2✔
124	int h = Math.floorDiv(x + y, 2);	2✔
125
126	Word<I> sigma1 = ceInput.prefix(h);	2✔
127	Word<I> sigma2 = ceInput.suffix(ceInput.size() - h);	2✔
128	Integer qp = mealy.getSuccessor(init, sigma1);	2✔
129	assert qp != null;	2✔
130	Word<I> accQPt = accessMap.get(qp);	2✔
131	assert accQPt != null;	2✔
132
133	Word<I> eta = ApartnessUtil.computeWitness(oTree, r, qt);	2✔
134	assert eta != null;	2✔
135
136	Word<I> outputQuery = accQPt.concat(sigma2).concat(eta);	2✔
137	Word<O> sulResponse = oqOracle.outputQuery(outputQuery);	2✔
138	Integer qpt = oTree.getSucc(oTree.defaultState(), accQPt);	2✔
139	assert qpt != null;	2✔
140
141	Integer rp = oTree.getSucc(oTree.defaultState(), sigma1);	2✔
142	assert rp != null;	2✔
143
144	Word<I> wit = ApartnessUtil.computeWitness(oTree, qpt, rp);	2✔
145	if (wit != null) {	2✔
146	processBinarySearch(sigma1, ceOutput.prefix(sigma1.length()), mealy);	2✔
147	} else {
148	Word<I> newInputs = accQPt.concat(sigma2);	2✔
149	processBinarySearch(newInputs, sulResponse.prefix(newInputs.length()), mealy);	2✔
150	}
151	}	2✔
152
153	public void makeObsTreeAdequate() {
154	do {
155	List<Pair<Word<I>, List<Word<I>>>> newFrontier = oqOracle.exploreFrontier(basis);	2✔
156	for (Pair<Word<I>, List<Word<I>>> pair : newFrontier) {	2✔
157	frontierToBasisMap.put(pair.getFirst(), pair.getSecond());	2✔
158	}	2✔
159
160	for (Entry<Word<I>, List<Word<I>>> entry : frontierToBasisMap.entrySet()) {	2✔
161	if (entry.getValue().size() > 1) {	2✔
162	List<Word<I>> newCands = oqOracle.identifyFrontier(entry.getKey(), entry.getValue());	2✔
163	frontierToBasisMap.put(entry.getKey(), newCands);	2✔
164	}
165	}	2✔
166
167	this.promoteFrontierState();	2✔
168	} while (!this.treeIsAdequate());	2✔
169	}	2✔
170
171	public void promoteFrontierState() {
172	Word<I> newBS = null;	2✔
173	for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {	2✔
174	if (e.getValue().isEmpty()) {	2✔
175	newBS = e.getKey();	2✔
176	break;	2✔
177	}
178	}	2✔
179	if (newBS == null) {	2✔
180	return;	2✔
181	}
182
183	Word<I> bs = Word.fromWords(newBS);	2✔
184	basis.add(bs);	2✔
185	frontierToBasisMap.remove(bs);	2✔
186	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
187
188	for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {	2✔
189	if (!ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs)) {	2✔
190	e.getValue().add(bs);	2✔
191	}
192	}	2✔
193	}	2✔
194
195	public boolean treeIsAdequate() {
196	this.checkFrontierConsistency();	2✔
197
198	for (List<Word<I>> value : frontierToBasisMap.values()) {	2✔
199	if (value.size() != 1) {	2✔
200	return false;	2✔
201	}
202	}	2✔
203
204	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
205	for (Word<I> b : basis) {	2✔
206	for (I i : inputAlphabet) {	2✔
207	Integer q = oTree.getSucc(oTree.defaultState(), b);	2✔
208	if (q == null \|\| oTree.getOut(q, i) == null) {	2✔
209	return false;	×
210	}
211	}	2✔
212	}	2✔
213
214	return true;	2✔
215	}
216
217	public void updateFrontierAndBasis() {
218	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
219
220	for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {	2✔
221	e.getValue().removeIf(bs -> ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs));	2✔
222	}	2✔
223
224	this.promoteFrontierState();	2✔
225	this.checkFrontierConsistency();	2✔
226
227	for (Entry<Word<I>, List<Word<I>>> e : frontierToBasisMap.entrySet()) {	2✔
228	e.getValue().removeIf(bs -> ApartnessUtil.accStatesAreApart(oTree, e.getKey(), bs));	2✔
229	}	2✔
230	}	2✔
231
232	public CompactMealy<I, O> buildHypothesis() {
233	while (true) {
234	this.makeObsTreeAdequate();	2✔
235	CompactMealy<I, O> hyp = this.constructHypothesis();	2✔
236
237	DefaultQuery<I, Word<O>> ce = this.checkConsistency(hyp);	2✔
238	if (ce != null) {	2✔
239	this.processCex(ce, hyp);	2✔
240	} else {
241	return hyp;	2✔
242	}
243	}	2✔
244	}
245
246	public CompactMealy<I, O> constructHypothesis() {
247
248	CompactMealy<I, O> result = new CompactMealy<>(inputAlphabet, basis.size());	2✔
249	basisMap.clear();	2✔
250	accessMap.ensureCapacity(basis.size());	2✔
251
252	for (Word<I> bAcc : basis) {	2✔
253	Integer state = result.addState();	2✔
254	basisMap.put(bAcc, state);	2✔
255	accessMap.set(state, bAcc);	2✔
256	}	2✔
257
258	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
259	for (Word<I> q : basis) {	2✔
260	for (I i : inputAlphabet) {	2✔
261	Integer bs = oTree.getSucc(oTree.defaultState(), q);	2✔
262	assert bs != null;	2✔
263	O output = oTree.getOut(bs, i);	2✔
264	assert output != null;	2✔
265	Word<I> fAcc = q.append(i);	2✔
266
267	Pair<Word<I>, Boolean> pair = this.identifyFrontierOrBasis(fAcc);	2✔
268	Word<I> dest = pair.getFirst();	2✔
269
270	Integer hypBS = basisMap.get(q);	2✔
271	assert hypBS != null;	2✔
272	Integer hypDest = basisMap.get(dest);	2✔
273	assert hypDest != null;	2✔
274	result.addTransition(hypBS, i, hypDest, output);	2✔
275	}	2✔
276	}	2✔
277
278	result.setInitialState(0);	2✔
279	return result;	2✔
280	}
281
282	public Pair<Word<I>, Boolean> identifyFrontierOrBasis(Word<I> seq) {
283	if (basis.contains(seq)) {	2✔
284	return Pair.of(seq, false);	2✔
285	}
286
287	List<Word<I>> frontier = frontierToBasisMap.get(seq);	2✔
288	assert frontier != null;	2✔
289	return Pair.of(frontier.get(0), true);	2✔
290	}
291
292	public void initObsTree(@Nullable List<Pair<Word<I>, Word<O>>> logs) {
293	if (logs != null) {	2✔
UNCOV 294	for (Pair<Word<I>, Word<O>> pair : logs) {	×
UNCOV 295	oqOracle.addObservation(pair.getFirst(), pair.getSecond());	×
UNCOV 296	}	×
297	}
298	}	2✔
299
300	public void checkFrontierConsistency() {
301	List<Word<I>> basisSet = new ArrayList<>(basis);	2✔
302	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
303
304	for (Word<I> bs : basisSet) {	2✔
305	for (I i : inputAlphabet) {	2✔
306	Word<I> fsAcc = bs.append(i);	2✔
307	if (oTree.getSucc(oTree.defaultState(), fsAcc) != null && !basis.contains(fsAcc) &&	2✔
308	!frontierToBasisMap.containsKey(fsAcc)) {	2✔
309	List<Word<I>> candidates = new ArrayList<>(basis.size());	2✔
310	for (Word<I> b : basis) {	2✔
311	if (!ApartnessUtil.accStatesAreApart(oTree, fsAcc, b)) {	2✔
312	candidates.add(b);	2✔
313	}
314	}	2✔
315	frontierToBasisMap.put(fsAcc, candidates);	2✔
316	}
317	}	2✔
318	}	2✔
319	}	2✔
320
321	public @Nullable DefaultQuery<I, Word<O>> checkConsistency(MealyMachine<Integer, I, ?, O> mealy) {
322	NormalObservationTree<I, O> oTree = oqOracle.getTree();	2✔
323	Word<I> wit = ApartnessUtil.treeAndHypComputeWitness(oTree, oTree.defaultState(), mealy, 0);	2✔
324	if (wit == null) {	2✔
325	return null;	2✔
326	}
327
328	Word<O> os = oTree.getObservation(null, wit);	2✔
329	assert os != null;	2✔
330	return new DefaultQuery<>(wit, os);	2✔
331	}
332
333	@Override
334	public void startLearning() {
335	this.initObsTree(null);	2✔
336	buildHypothesis();	2✔
337	}	2✔
338
339	@Override
340	public boolean refineHypothesis(DefaultQuery<I, Word<O>> ceQuery) {
341	boolean result = processCex(ceQuery, constructHypothesis());	2✔
342	buildHypothesis();	2✔
343	return result;	2✔
344	}
345
346	@Override
347	public MealyMachine<?, I, ?, O> getHypothesisModel() {
348	return constructHypothesis();	2✔
349	}
350
351	static final class BuilderDefaults {
352
353	private BuilderDefaults() {
354	// prevent instantiation
355	}
356
357	public static Rule2 rule2() {
358	return Rule2.ADS;	2✔
359	}
360
361	public static Rule3 rule3() {
362	return Rule3.ADS;	2✔
363	}
364
365	public static <I> @Nullable Word<I> sinkState() {
366	return null;	2✔
367	}
368
369	public static <O> @Nullable O sinkOutput() {
370	return null;	2✔
371	}
372
373	public static Random random() {
374	return new Random();	2✔
375	}
376	}
377	}

LearnLib / learnlib / 13166566074

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