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

99.41

/algorithms/active/procedural/src/main/java/de/learnlib/algorithm/procedural/spmm/SPMMLearner.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.procedural.spmm;

import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;
import java.util.Set;

import de.learnlib.AccessSequenceTransformer;
import de.learnlib.LearnerStateTracker;
import de.learnlib.algorithm.LearnerConstructor;
import de.learnlib.algorithm.LearningAlgorithm;
import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
import de.learnlib.algorithm.procedural.SymbolWrapper;
import de.learnlib.algorithm.procedural.spmm.manager.OptimizingATManager;
import de.learnlib.oracle.MembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.util.MQUtil;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.ProceduralInputAlphabet;
import net.automatalib.alphabet.SupportsGrowingAlphabet;
import net.automatalib.alphabet.impl.DefaultProceduralInputAlphabet;
import net.automatalib.alphabet.impl.GrowingMapAlphabet;
import net.automatalib.automaton.procedural.SPMM;
import net.automatalib.automaton.procedural.impl.EmptySPMM;
import net.automatalib.automaton.procedural.impl.StackSPMM;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.util.HashUtil;
import net.automatalib.common.util.Pair;
import net.automatalib.common.util.mapping.Mapping;
import net.automatalib.util.automaton.Automata;
import net.automatalib.util.automaton.procedural.SPMMs;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;

/**
 * A learning algorithm for {@link SPMM}s.
 *
 * @param <I>
 *         input symbol type
 * @param <O>
 *         output symbol type
 * @param <L>
 *         sub-learner type
 */
public class SPMMLearner<I, O, L extends MealyLearner<SymbolWrapper<I>, O> & SupportsGrowingAlphabet<SymbolWrapper<I>> & AccessSequenceTransformer<SymbolWrapper<I>>>
        implements LearningAlgorithm<SPMM<?, I, ?, O>, I, Word<O>>, LearnerStateTracker {

    private final ProceduralInputAlphabet<I> alphabet;
    private final O errorOutput;
    private final MembershipOracle<I, Word<O>> oracle;
    private final Mapping<I, LearnerConstructor<L, SymbolWrapper<I>, Word<O>>> learnerConstructors;
    private final ATManager<I, O> atManager;

    private final Map<I, L> learners;
    private I initialCallSymbol;
    private O initialOutputSymbol;
    private boolean learningStarted;

    private final Map<I, SymbolWrapper<I>> mapping;

    public SPMMLearner(ProceduralInputAlphabet<I> alphabet,
                       O errorOutput,
                       MembershipOracle<I, Word<O>> oracle,
                       LearnerConstructor<L, SymbolWrapper<I>, Word<O>> learnerConstructor) {
        this(alphabet,
             errorOutput,
             oracle,
             i -> learnerConstructor,
             new OptimizingATManager<>(alphabet, errorOutput));
    }

    public SPMMLearner(ProceduralInputAlphabet<I> alphabet,
                       O errorOutput,
                       MembershipOracle<I, Word<O>> oracle,
                       Mapping<I, LearnerConstructor<L, SymbolWrapper<I>, Word<O>>> learnerConstructors,
                       ATManager<I, O> atManager) {
        this.alphabet = alphabet;
        this.errorOutput = errorOutput;
        this.oracle = oracle;
        this.learnerConstructors = learnerConstructors;
        this.atManager = atManager;

        this.learners = new HashMap<>(HashUtil.capacity(this.alphabet.getNumCalls()));
        this.learningStarted = false;
        this.mapping = new HashMap<>(HashUtil.capacity(this.alphabet.size()));

        for (I i : this.alphabet.getInternalAlphabet()) {
            final SymbolWrapper<I> wrapper = new SymbolWrapper<>(i, true);
            this.mapping.put(i, wrapper);
        }

        final SymbolWrapper<I> wrapper = new SymbolWrapper<>(this.alphabet.getReturnSymbol(), false);
        this.mapping.put(this.alphabet.getReturnSymbol(), wrapper);
    }

    @Override
    public void startLearning() {
        requireLearningProcessNotStarted();
        this.learningStarted = true;
        // do nothing, as we have to wait for evidence that the potential main procedure actually terminates
    }

    @Override
    public boolean refineHypothesis(DefaultQuery<I, Word<O>> defaultQuery) {
        requireLearningProcessStarted();

        if (!MQUtil.isCounterexample(defaultQuery, getHypothesisModel())) {
            return false;
        }

        assert defaultQuery.getPrefix().isEmpty() : "Counterexamples need to provide full trace information";
        assert this.alphabet.isReturnMatched(defaultQuery.getInput()) : "Counterexample has unmatched return symbols";

        boolean changed = extractUsefulInformationFromCounterExample(defaultQuery);

        while (refineHypothesisInternal(defaultQuery)) {
            changed = true;
        }

        ensureReturnClosure();

        assert SPMMs.isValid(getHypothesisModel());

        return changed;
    }

    private boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> defaultQuery) {

        final SPMM<?, I, ?, O> hypothesis = this.getHypothesisModel();

        if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) {
            return false;
        }

        final Word<I> input = defaultQuery.getInput();
        final Word<O> output = defaultQuery.getOutput();

        final int mismatchIdx = detectMismatchingIdx(hypothesis, input, output);

        // extract local ce
        final int callIdx = alphabet.findCallIndex(input, mismatchIdx);
        final I procedure = input.getSymbol(callIdx);

        final Pair<Word<I>, Word<O>> localTraces = alphabet.project(input.subWord(callIdx + 1, mismatchIdx + 1),
                                                                    output.subWord(callIdx + 1, mismatchIdx + 1),
                                                                    0);
        final DefaultQuery<SymbolWrapper<I>, Word<O>> localCE =
                constructLocalCE(localTraces.getFirst(), localTraces.getSecond());
        final boolean localRefinement = this.learners.get(procedure).refineHypothesis(localCE);
        assert localRefinement;

        return true;
    }

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

    @Override
    public SPMM<?, I, ?, O> getHypothesisModel() {
        requireLearningProcessStarted();

        if (this.learners.isEmpty()) {
            return new EmptySPMM<>(this.alphabet, errorOutput);
        }

        final Alphabet<SymbolWrapper<I>> internalAlphabet = new GrowingMapAlphabet<>();
        final Alphabet<SymbolWrapper<I>> callAlphabet = new GrowingMapAlphabet<>();
        final SymbolWrapper<I> returnSymbol;

        final Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> procedures = getSubModels();
        final Map<SymbolWrapper<I>, MealyMachine<?, SymbolWrapper<I>, ?, O>> mappedProcedures =
                new HashMap<>(HashUtil.capacity(procedures.size()));

        for (Entry<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> e : procedures.entrySet()) {
            final SymbolWrapper<I> w = this.mapping.get(e.getKey());
            assert w != null;
            mappedProcedures.put(w, e.getValue());
            callAlphabet.add(w);
        }

        for (I i : this.alphabet.getInternalAlphabet()) {
            final SymbolWrapper<I> w = this.mapping.get(i);
            assert w != null;
            internalAlphabet.add(w);
        }

        returnSymbol = this.mapping.get(alphabet.getReturnSymbol());
        assert returnSymbol != null;

        final ProceduralInputAlphabet<SymbolWrapper<I>> mappedAlphabet =
                new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol);

        final StackSPMM<?, SymbolWrapper<I>, ?, O> delegate = new StackSPMM<>(mappedAlphabet,
                                                                              this.mapping.get(initialCallSymbol),
                                                                              initialOutputSymbol,
                                                                              errorOutput,
                                                                              mappedProcedures);

        return new MappingSPMM<>(alphabet, errorOutput, mapping, delegate);
    }

    private boolean extractUsefulInformationFromCounterExample(DefaultQuery<I, Word<O>> defaultQuery) {

        final Word<I> input = defaultQuery.getInput();
        final Word<O> output = defaultQuery.getOutput();

        // CEs should always be rooted at the main procedure
        this.initialCallSymbol = input.firstSymbol();
        this.initialOutputSymbol = output.firstSymbol();

        final Pair<Set<I>, Set<I>> newSeqs = atManager.scanCounterexample(defaultQuery);
        final Set<I> newCalls = newSeqs.getFirst();
        final Set<I> newTerms = newSeqs.getSecond();

        boolean update = false;

        for (I call : newTerms) {
            final SymbolWrapper<I> sym = new SymbolWrapper<>(call, true);
            this.mapping.put(call, sym);
            for (L learner : this.learners.values()) {
                learner.addAlphabetSymbol(sym);
                update = true;
            }
        }

        for (I sym : newCalls) {
            update = true;
            final L newLearner = learnerConstructors.get(sym)
                                                    .constructLearner(new GrowingMapAlphabet<>(this.mapping.values()),
                                                                      new ProceduralMembershipOracle<>(alphabet,
                                                                                                       oracle,
                                                                                                       sym,
                                                                                                       errorOutput,
                                                                                                       atManager));

            newLearner.startLearning();

            // add new learner here, so that we have an AccessSequenceTransformer available when scanning for shorter ts
            this.learners.put(sym, newLearner);

            // try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses
            final Set<I> newTS =
                    this.atManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()),
                                                  learners,
                                                  mapping.values());

            for (I call : newTS) {
                final SymbolWrapper<I> wrapper = new SymbolWrapper<>(call, true);
                this.mapping.put(call, wrapper);
                for (L learner : this.learners.values()) {
                    learner.addAlphabetSymbol(wrapper);
                }
            }

            // add non-terminating version for new call
            if (!this.mapping.containsKey(sym)) {
                final SymbolWrapper<I> wrapper = new SymbolWrapper<>(sym, false);
                this.mapping.put(sym, wrapper);
                for (L learner : this.learners.values()) {
                    learner.addAlphabetSymbol(wrapper);
                }
            }
        }

        return update;
    }

    private Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> getSubModels() {
        final Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> subModels =
                new HashMap<>(HashUtil.capacity(this.learners.size()));

        for (Map.Entry<I, L> entry : this.learners.entrySet()) {
            subModels.put(entry.getKey(), entry.getValue().getHypothesisModel());
        }

        return subModels;
    }

    private DefaultQuery<SymbolWrapper<I>, Word<O>> constructLocalCE(Word<I> input, Word<O> output) {

        final WordBuilder<SymbolWrapper<I>> wb = new WordBuilder<>(input.length());
        for (I i : input) {
            wb.append(mapping.get(i));
        }

        return new DefaultQuery<>(wb.toWord(), output);
    }

    private void ensureReturnClosure() {
        for (L learner : this.learners.values()) {
            boolean stable = false;

            while (!stable) {
                stable = ensureReturnClosure(learner.getHypothesisModel(), mapping.values(), learner);
            }
        }
    }

    private <S, T> boolean ensureReturnClosure(MealyMachine<S, SymbolWrapper<I>, T, O> hyp,
                                               Collection<SymbolWrapper<I>> inputs,
                                               L learner) {

        final Set<Word<SymbolWrapper<I>>> cover = new HashSet<>();
        for (Word<SymbolWrapper<I>> sc : Automata.stateCover(hyp, inputs)) {
            cover.add(learner.transformAccessSequence(sc));
        }

        for (Word<SymbolWrapper<I>> cov : cover) {
            final S state = hyp.getState(cov);

            for (SymbolWrapper<I> i : inputs) {
                if (Objects.equals(i.getDelegate(), alphabet.getReturnSymbol())) {

                    final S succ = hyp.getSuccessor(state, i);

                    for (SymbolWrapper<I> next : inputs) {
                        final O succOut = hyp.getOutput(succ, next);

                        if (!Objects.equals(errorOutput, succOut)) { // error closure is violated
                            // TODO split prefix/suffix? Issue with learners?
                            final Word<SymbolWrapper<I>> lp = cov.append(i);
                            final DefaultQuery<SymbolWrapper<I>, Word<O>> ce = new DefaultQuery<>(Word.epsilon(),
                                                                                                  lp.append(next),
                                                                                                  hyp.computeOutput(lp)
                                                                                                     .append(errorOutput));
                            final boolean refined = learner.refineHypothesis(ce);
                            assert refined;
                            return false;
                        }
                    }
                }
            }
        }

        return true;
    }

    private <S, T> int detectMismatchingIdx(SPMM<S, I, T, O> spmm, Word<I> input, Word<O> output) {

        final Iterator<I> inIter = input.iterator();
        final Iterator<O> outIter = output.iterator();

        S stateIter = spmm.getInitialState();
        int idx = 0;

        while (inIter.hasNext() && outIter.hasNext()) {
            final I i = inIter.next();
            final O o = outIter.next();

            T t = spmm.getTransition(stateIter, i);

            if (t == null || !Objects.equals(o, spmm.getTransitionOutput(t))) {
                return idx;
            }
            stateIter = spmm.getSuccessor(t);
            idx++;
        }

        throw new IllegalArgumentException("Non-counterexamples shouldn't be scanned for a mis-match");
    }
}

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.procedural.spmm;
17
18	import java.util.Collection;
19	import java.util.Collections;
20	import java.util.HashMap;
21	import java.util.HashSet;
22	import java.util.Iterator;
23	import java.util.Map;
24	import java.util.Map.Entry;
25	import java.util.Objects;
26	import java.util.Set;
27
28	import de.learnlib.AccessSequenceTransformer;
29	import de.learnlib.LearnerStateTracker;
30	import de.learnlib.algorithm.LearnerConstructor;
31	import de.learnlib.algorithm.LearningAlgorithm;
32	import de.learnlib.algorithm.LearningAlgorithm.MealyLearner;
33	import de.learnlib.algorithm.procedural.SymbolWrapper;
34	import de.learnlib.algorithm.procedural.spmm.manager.OptimizingATManager;
35	import de.learnlib.oracle.MembershipOracle;
36	import de.learnlib.query.DefaultQuery;
37	import de.learnlib.util.MQUtil;
38	import net.automatalib.alphabet.Alphabet;
39	import net.automatalib.alphabet.ProceduralInputAlphabet;
40	import net.automatalib.alphabet.SupportsGrowingAlphabet;
41	import net.automatalib.alphabet.impl.DefaultProceduralInputAlphabet;
42	import net.automatalib.alphabet.impl.GrowingMapAlphabet;
43	import net.automatalib.automaton.procedural.SPMM;
44	import net.automatalib.automaton.procedural.impl.EmptySPMM;
45	import net.automatalib.automaton.procedural.impl.StackSPMM;
46	import net.automatalib.automaton.transducer.MealyMachine;
47	import net.automatalib.common.util.HashUtil;
48	import net.automatalib.common.util.Pair;
49	import net.automatalib.common.util.mapping.Mapping;
50	import net.automatalib.util.automaton.Automata;
51	import net.automatalib.util.automaton.procedural.SPMMs;
52	import net.automatalib.word.Word;
53	import net.automatalib.word.WordBuilder;
54
55	/**
56	* A learning algorithm for {@link SPMM}s.
57	*
58	* @param <I>
59	* input symbol type
60	* @param <O>
61	* output symbol type
62	* @param <L>
63	* sub-learner type
64	*/
65	public class SPMMLearner<I, O, L extends MealyLearner<SymbolWrapper<I>, O> & SupportsGrowingAlphabet<SymbolWrapper<I>> & AccessSequenceTransformer<SymbolWrapper<I>>>	2✔
66	implements LearningAlgorithm<SPMM<?, I, ?, O>, I, Word<O>>, LearnerStateTracker {
67
68	private final ProceduralInputAlphabet<I> alphabet;
69	private final O errorOutput;
70	private final MembershipOracle<I, Word<O>> oracle;
71	private final Mapping<I, LearnerConstructor<L, SymbolWrapper<I>, Word<O>>> learnerConstructors;
72	private final ATManager<I, O> atManager;
73
74	private final Map<I, L> learners;
75	private I initialCallSymbol;
76	private O initialOutputSymbol;
77	private boolean learningStarted;
78
79	private final Map<I, SymbolWrapper<I>> mapping;
80
81	public SPMMLearner(ProceduralInputAlphabet<I> alphabet,
82	O errorOutput,
83	MembershipOracle<I, Word<O>> oracle,
84	LearnerConstructor<L, SymbolWrapper<I>, Word<O>> learnerConstructor) {
85	this(alphabet,	2✔
86	errorOutput,
87	oracle,
88	i -> learnerConstructor,	2✔
89	new OptimizingATManager<>(alphabet, errorOutput));
90	}	2✔
91
92	public SPMMLearner(ProceduralInputAlphabet<I> alphabet,
93	O errorOutput,
94	MembershipOracle<I, Word<O>> oracle,
95	Mapping<I, LearnerConstructor<L, SymbolWrapper<I>, Word<O>>> learnerConstructors,
96	ATManager<I, O> atManager) {	2✔
97	this.alphabet = alphabet;	2✔
98	this.errorOutput = errorOutput;	2✔
99	this.oracle = oracle;	2✔
100	this.learnerConstructors = learnerConstructors;	2✔
101	this.atManager = atManager;	2✔
102
103	this.learners = new HashMap<>(HashUtil.capacity(this.alphabet.getNumCalls()));	2✔
104	this.learningStarted = false;	2✔
105	this.mapping = new HashMap<>(HashUtil.capacity(this.alphabet.size()));	2✔
106
107	for (I i : this.alphabet.getInternalAlphabet()) {	2✔
108	final SymbolWrapper<I> wrapper = new SymbolWrapper<>(i, true);	2✔
109	this.mapping.put(i, wrapper);	2✔
110	}	2✔
111
112	final SymbolWrapper<I> wrapper = new SymbolWrapper<>(this.alphabet.getReturnSymbol(), false);	2✔
113	this.mapping.put(this.alphabet.getReturnSymbol(), wrapper);	2✔
114	}	2✔
115
116	@Override
117	public void startLearning() {
118	requireLearningProcessNotStarted();	2✔
119	this.learningStarted = true;	2✔
120	// do nothing, as we have to wait for evidence that the potential main procedure actually terminates
121	}	2✔
122
123	@Override
124	public boolean refineHypothesis(DefaultQuery<I, Word<O>> defaultQuery) {
125	requireLearningProcessStarted();	2✔
126
127	if (!MQUtil.isCounterexample(defaultQuery, getHypothesisModel())) {	2✔
128	return false;	2✔
129	}
130
131	assert defaultQuery.getPrefix().isEmpty() : "Counterexamples need to provide full trace information";	2✔
132	assert this.alphabet.isReturnMatched(defaultQuery.getInput()) : "Counterexample has unmatched return symbols";	2✔
133
134	boolean changed = extractUsefulInformationFromCounterExample(defaultQuery);	2✔
135
136	while (refineHypothesisInternal(defaultQuery)) {	2✔
137	changed = true;	2✔
138	}
139
140	ensureReturnClosure();	2✔
141
142	assert SPMMs.isValid(getHypothesisModel());	2✔
143
144	return changed;	2✔
145	}
146
147	private boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> defaultQuery) {
148
149	final SPMM<?, I, ?, O> hypothesis = this.getHypothesisModel();	2✔
150
151	if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) {	2✔
152	return false;	2✔
153	}
154
155	final Word<I> input = defaultQuery.getInput();	2✔
156	final Word<O> output = defaultQuery.getOutput();	2✔
157
158	final int mismatchIdx = detectMismatchingIdx(hypothesis, input, output);	2✔
159
160	// extract local ce
161	final int callIdx = alphabet.findCallIndex(input, mismatchIdx);	2✔
162	final I procedure = input.getSymbol(callIdx);	2✔
163
164	final Pair<Word<I>, Word<O>> localTraces = alphabet.project(input.subWord(callIdx + 1, mismatchIdx + 1),	2✔
165	output.subWord(callIdx + 1, mismatchIdx + 1),	2✔
166	0);
167	final DefaultQuery<SymbolWrapper<I>, Word<O>> localCE =	2✔
168	constructLocalCE(localTraces.getFirst(), localTraces.getSecond());	2✔
169	final boolean localRefinement = this.learners.get(procedure).refineHypothesis(localCE);	2✔
170	assert localRefinement;	2✔
171
172	return true;	2✔
173	}
174
175	@Override
176	public boolean hasLearningProcessStarted() {
177	return this.learningStarted;	2✔
178	}
179
180	@Override
181	public SPMM<?, I, ?, O> getHypothesisModel() {
182	requireLearningProcessStarted();	2✔
183
184	if (this.learners.isEmpty()) {	2✔
185	return new EmptySPMM<>(this.alphabet, errorOutput);	2✔
186	}
187
188	final Alphabet<SymbolWrapper<I>> internalAlphabet = new GrowingMapAlphabet<>();	2✔
189	final Alphabet<SymbolWrapper<I>> callAlphabet = new GrowingMapAlphabet<>();	2✔
190	final SymbolWrapper<I> returnSymbol;
191
192	final Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> procedures = getSubModels();	2✔
193	final Map<SymbolWrapper<I>, MealyMachine<?, SymbolWrapper<I>, ?, O>> mappedProcedures =	2✔
194	new HashMap<>(HashUtil.capacity(procedures.size()));	2✔
195
196	for (Entry<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> e : procedures.entrySet()) {	2✔
197	final SymbolWrapper<I> w = this.mapping.get(e.getKey());	2✔
198	assert w != null;	2✔
199	mappedProcedures.put(w, e.getValue());	2✔
200	callAlphabet.add(w);	2✔
201	}	2✔
202
203	for (I i : this.alphabet.getInternalAlphabet()) {	2✔
204	final SymbolWrapper<I> w = this.mapping.get(i);	2✔
205	assert w != null;	2✔
206	internalAlphabet.add(w);	2✔
207	}	2✔
208
209	returnSymbol = this.mapping.get(alphabet.getReturnSymbol());	2✔
210	assert returnSymbol != null;	2✔
211
212	final ProceduralInputAlphabet<SymbolWrapper<I>> mappedAlphabet =	2✔
213	new DefaultProceduralInputAlphabet<>(internalAlphabet, callAlphabet, returnSymbol);
214
215	final StackSPMM<?, SymbolWrapper<I>, ?, O> delegate = new StackSPMM<>(mappedAlphabet,	2✔
216	this.mapping.get(initialCallSymbol),	2✔
217	initialOutputSymbol,
218	errorOutput,
219	mappedProcedures);
220
221	return new MappingSPMM<>(alphabet, errorOutput, mapping, delegate);	2✔
222	}
223
224	private boolean extractUsefulInformationFromCounterExample(DefaultQuery<I, Word<O>> defaultQuery) {
225
226	final Word<I> input = defaultQuery.getInput();	2✔
227	final Word<O> output = defaultQuery.getOutput();	2✔
228
229	// CEs should always be rooted at the main procedure
230	this.initialCallSymbol = input.firstSymbol();	2✔
231	this.initialOutputSymbol = output.firstSymbol();	2✔
232
233	final Pair<Set<I>, Set<I>> newSeqs = atManager.scanCounterexample(defaultQuery);	2✔
234	final Set<I> newCalls = newSeqs.getFirst();	2✔
235	final Set<I> newTerms = newSeqs.getSecond();	2✔
236
237	boolean update = false;	2✔
238
239	for (I call : newTerms) {	2✔
240	final SymbolWrapper<I> sym = new SymbolWrapper<>(call, true);	2✔
241	this.mapping.put(call, sym);	2✔
242	for (L learner : this.learners.values()) {	2✔
243	learner.addAlphabetSymbol(sym);	2✔
244	update = true;	2✔
245	}	2✔
246	}	2✔
247
248	for (I sym : newCalls) {	2✔
249	update = true;	2✔
250	final L newLearner = learnerConstructors.get(sym)	2✔
251	.constructLearner(new GrowingMapAlphabet<>(this.mapping.values()),	2✔
252	new ProceduralMembershipOracle<>(alphabet,
253	oracle,
254	sym,
255	errorOutput,
256	atManager));
257
258	newLearner.startLearning();	2✔
259
260	// add new learner here, so that we have an AccessSequenceTransformer available when scanning for shorter ts
261	this.learners.put(sym, newLearner);	2✔
262
263	// try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses
264	final Set<I> newTS =	2✔
265	this.atManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()),	2✔
266	learners,
267	mapping.values());	2✔
268
269	for (I call : newTS) {	2✔
270	final SymbolWrapper<I> wrapper = new SymbolWrapper<>(call, true);	2✔
271	this.mapping.put(call, wrapper);	2✔
272	for (L learner : this.learners.values()) {	2✔
273	learner.addAlphabetSymbol(wrapper);	2✔
274	}	2✔
275	}	2✔
276
277	// add non-terminating version for new call
278	if (!this.mapping.containsKey(sym)) {	2✔
279	final SymbolWrapper<I> wrapper = new SymbolWrapper<>(sym, false);	2✔
280	this.mapping.put(sym, wrapper);	2✔
281	for (L learner : this.learners.values()) {	2✔
282	learner.addAlphabetSymbol(wrapper);	2✔
283	}	2✔
284	}
285	}	2✔
286
287	return update;	2✔
288	}
289
290	private Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> getSubModels() {
291	final Map<I, MealyMachine<?, SymbolWrapper<I>, ?, O>> subModels =	2✔
292	new HashMap<>(HashUtil.capacity(this.learners.size()));	2✔
293
294	for (Map.Entry<I, L> entry : this.learners.entrySet()) {	2✔
295	subModels.put(entry.getKey(), entry.getValue().getHypothesisModel());	2✔
296	}	2✔
297
298	return subModels;	2✔
299	}
300
301	private DefaultQuery<SymbolWrapper<I>, Word<O>> constructLocalCE(Word<I> input, Word<O> output) {
302
303	final WordBuilder<SymbolWrapper<I>> wb = new WordBuilder<>(input.length());	2✔
304	for (I i : input) {	2✔
305	wb.append(mapping.get(i));	2✔
306	}	2✔
307
308	return new DefaultQuery<>(wb.toWord(), output);	2✔
309	}
310
311	private void ensureReturnClosure() {
312	for (L learner : this.learners.values()) {	2✔
313	boolean stable = false;	2✔
314
315	while (!stable) {	2✔
316	stable = ensureReturnClosure(learner.getHypothesisModel(), mapping.values(), learner);	2✔
317	}
318	}	2✔
319	}	2✔
320
321	private <S, T> boolean ensureReturnClosure(MealyMachine<S, SymbolWrapper<I>, T, O> hyp,
322	Collection<SymbolWrapper<I>> inputs,
323	L learner) {
324
325	final Set<Word<SymbolWrapper<I>>> cover = new HashSet<>();	2✔
326	for (Word<SymbolWrapper<I>> sc : Automata.stateCover(hyp, inputs)) {	2✔
327	cover.add(learner.transformAccessSequence(sc));	2✔
328	}	2✔
329
330	for (Word<SymbolWrapper<I>> cov : cover) {	2✔
331	final S state = hyp.getState(cov);	2✔
332
333	for (SymbolWrapper<I> i : inputs) {	2✔
334	if (Objects.equals(i.getDelegate(), alphabet.getReturnSymbol())) {	2✔
335
336	final S succ = hyp.getSuccessor(state, i);	2✔
337
338	for (SymbolWrapper<I> next : inputs) {	2✔
339	final O succOut = hyp.getOutput(succ, next);	2✔
340
341	if (!Objects.equals(errorOutput, succOut)) { // error closure is violated	2✔
342	// TODO split prefix/suffix? Issue with learners?
343	final Word<SymbolWrapper<I>> lp = cov.append(i);	2✔
344	final DefaultQuery<SymbolWrapper<I>, Word<O>> ce = new DefaultQuery<>(Word.epsilon(),	2✔
345	lp.append(next),	2✔
346	hyp.computeOutput(lp)	2✔
347	.append(errorOutput));	2✔
348	final boolean refined = learner.refineHypothesis(ce);	2✔
349	assert refined;	2✔
350	return false;	2✔
351	}
352	}	2✔
353	}
354	}	2✔
355	}	2✔
356
357	return true;	2✔
358	}
359
360	private <S, T> int detectMismatchingIdx(SPMM<S, I, T, O> spmm, Word<I> input, Word<O> output) {
361
362	final Iterator<I> inIter = input.iterator();	2✔
363	final Iterator<O> outIter = output.iterator();	2✔
364
365	S stateIter = spmm.getInitialState();	2✔
366	int idx = 0;	2✔
367
368	while (inIter.hasNext() && outIter.hasNext()) {	2✔
369	final I i = inIter.next();	2✔
370	final O o = outIter.next();	2✔
371
372	T t = spmm.getTransition(stateIter, i);	2✔
373
374	if (t == null \|\| !Objects.equals(o, spmm.getTransitionOutput(t))) {	2✔
375	return idx;	2✔
376	}
377	stateIter = spmm.getSuccessor(t);	2✔
378	idx++;	2✔
379	}	2✔
380
381	throw new IllegalArgumentException("Non-counterexamples shouldn't be scanned for a mis-match");	×
382	}
383	}

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