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

98.1

/algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/LSharpMealy.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.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.AccessSequenceTransformer;
import de.learnlib.LearnerStateTracker;
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).
 * <p>
 * <b>Implementation note:</b> this learner uses the {@link AccessSequenceTransformer} interface to provide access to
 * the representatives of the states of the current hypothesis model.
 *
 * @param <I>
 *         input symbol type
 * @param <O>
 *         output symbol type
 */
public class LSharpMealy<I, O> implements MealyLearner<I, O>, AccessSequenceTransformer<I>, LearnerStateTracker {

    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;

    public LSharpMealy(Alphabet<I> alphabet, AdaptiveMembershipOracle<I, O> oracle) {
        this(alphabet,
             oracle,
             BuilderDefaults.rule2(),
             BuilderDefaults.rule3(),
             BuilderDefaults.sinkState(),
             BuilderDefaults.sinkOutput(),
             BuilderDefaults.random());
    }

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

    ArrayStorage<Word<I>> getAccessMap() {
        return new ArrayStorage<>(accessMap);
    }

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

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

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

    @Override
    public boolean hasLearningProcessStarted() {
        return !basisMap.isEmpty();
    }

    @Override
    public Word<I> transformAccessSequence(Word<I> word) {
        requireLearningProcessStarted();
        final CompactMealy<I, O> hyp = constructHypothesis();
        final Integer bs = hyp.getState(word);
        assert bs != null;
        return accessMap.get(bs);
    }

    static final class BuilderDefaults {

        private BuilderDefaults() {
            // prevent instantiation
        }

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

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

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

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

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

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

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