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

99.38

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

import java.util.Collection;
import java.util.Collections;
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 com.google.common.collect.Maps;
import de.learnlib.algorithms.procedural.SymbolWrapper;
import de.learnlib.algorithms.procedural.spmm.manager.OptimizingATManager;
import de.learnlib.api.AccessSequenceTransformer;
import de.learnlib.api.algorithm.LearnerConstructor;
import de.learnlib.api.algorithm.LearningAlgorithm;
import de.learnlib.api.algorithm.LearningAlgorithm.MealyLearner;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.util.MQUtil;
import net.automatalib.SupportsGrowingAlphabet;
import net.automatalib.automata.procedural.EmptySPMM;
import net.automatalib.automata.procedural.SPMM;
import net.automatalib.automata.procedural.StackSPMM;
import net.automatalib.automata.transducers.MealyMachine;
import net.automatalib.commons.util.Pair;
import net.automatalib.commons.util.mappings.Mapping;
import net.automatalib.util.automata.Automata;
import net.automatalib.util.automata.procedural.SPMMUtil;
import net.automatalib.words.Alphabet;
import net.automatalib.words.ProceduralInputAlphabet;
import net.automatalib.words.Word;
import net.automatalib.words.WordBuilder;
import net.automatalib.words.impl.DefaultProceduralInputAlphabet;
import net.automatalib.words.impl.GrowingMapAlphabet;

/**
 * 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>> {

    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 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 = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls());
        this.mapping = Maps.newHashMapWithExpectedSize(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() {
        // 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) {

        assert this.alphabet.isReturnMatched(defaultQuery.getInput());

        boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery);

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

        ensureReturnClosure();

        assert SPMMUtil.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 SPMM<?, I, ?, O> getHypothesisModel() {

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

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