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

97.6

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

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Set;
import java.util.function.Predicate;

import com.google.common.collect.Maps;
import com.google.common.collect.Sets;
import de.learnlib.acex.AcexAnalyzer;
import de.learnlib.acex.analyzers.AcexAnalyzers;
import de.learnlib.acex.impl.AbstractBaseCounterexample;
import de.learnlib.algorithms.procedural.spa.manager.OptimizingATRManager;
import de.learnlib.api.AccessSequenceTransformer;
import de.learnlib.api.algorithm.LearnerConstructor;
import de.learnlib.api.algorithm.LearningAlgorithm;
import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
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.fsa.DFA;
import net.automatalib.automata.procedural.EmptySPA;
import net.automatalib.automata.procedural.SPA;
import net.automatalib.automata.procedural.StackSPA;
import net.automatalib.commons.util.mappings.Mapping;
import net.automatalib.words.ProceduralInputAlphabet;
import net.automatalib.words.Word;
import net.automatalib.words.WordBuilder;
import net.automatalib.words.impl.GrowingMapAlphabet;
import org.checkerframework.checker.nullness.qual.NonNull;

/**
 * A learning algorithm for {@link SPA}s.
 *
 * @param <I>
 *         input symbol type
 * @param <L>
 *         sub-learner type
 */
public class SPALearner<I, L extends DFALearner<I> & SupportsGrowingAlphabet<I> & AccessSequenceTransformer<I>>
        implements LearningAlgorithm<SPA<?, I>, I, Boolean> {

    private final ProceduralInputAlphabet<I> alphabet;
    private final MembershipOracle<I, Boolean> oracle;
    private final Mapping<I, LearnerConstructor<L, I, Boolean>> learnerConstructors;
    private final AcexAnalyzer analyzer;
    private final ATRManager<I> atrManager;

    private final Map<I, L> subLearners;
    private final Set<I> activeAlphabet;
    private I initialCallSymbol;

    public SPALearner(ProceduralInputAlphabet<I> alphabet,
                      MembershipOracle<I, Boolean> oracle,
                      LearnerConstructor<L, I, Boolean> learnerConstructor) {
        this(alphabet,
             oracle,
             (i) -> learnerConstructor,
             AcexAnalyzers.BINARY_SEARCH_FWD,
             new OptimizingATRManager<>(alphabet));
    }

    public SPALearner(ProceduralInputAlphabet<I> alphabet,
                      MembershipOracle<I, Boolean> oracle,
                      Mapping<I, LearnerConstructor<L, I, Boolean>> learnerConstructors,
                      AcexAnalyzer analyzer,
                      ATRManager<I> atrManager) {
        this.alphabet = alphabet;
        this.oracle = oracle;
        this.learnerConstructors = learnerConstructors;
        this.analyzer = analyzer;
        this.atrManager = atrManager;

        this.subLearners = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls());
        this.activeAlphabet = Sets.newHashSetWithExpectedSize(alphabet.getNumCalls() + alphabet.getNumInternals());
        this.activeAlphabet.addAll(alphabet.getInternalAlphabet());
    }

    @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, Boolean> defaultQuery) {

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

        boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery);

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

        return changed;
    }

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

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

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

        // look for better sequences and ensure TS conformance prior to CE analysis
        boolean localRefinement = updateATRAndCheckTSConformance(hypothesis);

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

        final Word<I> input = defaultQuery.getInput();
        final List<Integer> returnIndices = determineReturnIndices(input);
        final int idx = analyzer.analyzeAbstractCounterexample(new Acex(input,
                                                                        defaultQuery.getOutput() ?
                                                                                hypothesis::accepts :
                                                                                this.oracle::answerQuery,
                                                                        returnIndices));
        final int returnIdx = returnIndices.get(idx);

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

        final Word<I> localTrace = this.alphabet.project(input.subWord(callIdx + 1, returnIdx), 0);
        final DefaultQuery<I, Boolean> localCE = new DefaultQuery<>(localTrace, defaultQuery.getOutput());

        localRefinement |= this.subLearners.get(procedure).refineHypothesis(localCE);
        assert localRefinement;

        return true;
    }

    @Override
    public SPA<?, I> getHypothesisModel() {

        if (this.subLearners.isEmpty()) {
            return new EmptySPA<>(this.alphabet);
        }

        return new StackSPA<>(alphabet, initialCallSymbol, getSubModels());
    }

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

        if (!defaultQuery.getOutput()) {
            return false;
        }

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

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

        final Set<I> newProcedures = atrManager.scanPositiveCounterexample(input);

        for (I sym : newProcedures) {
            final L newLearner = learnerConstructors.get(sym)
                                                    .constructLearner(new GrowingMapAlphabet<>(alphabet.getInternalAlphabet()),
                                                                      new ProceduralMembershipOracle<>(alphabet,
                                                                                                       oracle,
                                                                                                       sym,
                                                                                                       atrManager));
            // add existing procedures (without itself) to new learner
            for (I call : this.subLearners.keySet()) {
                newLearner.addAlphabetSymbol(call);
            }

            newLearner.startLearning();

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

            // try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses
            this.atrManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()),
                                           subLearners,
                                           activeAlphabet);
            this.activeAlphabet.add(sym);

            // add the new procedure (with a possibly shorter ts) to all learners (including the new one)
            for (L learner : this.subLearners.values()) {
                learner.addAlphabetSymbol(sym);
            }
        }

        if (!newProcedures.isEmpty()) {
            this.atrManager.scanProcedures(getSubModels(), subLearners, activeAlphabet);
            return true;
        } else {
            return false;
        }
    }

    private Map<I, DFA<?, I>> getSubModels() {
        final Map<I, DFA<?, I>> subModels = Maps.newHashMapWithExpectedSize(this.subLearners.size());

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

        return subModels;
    }

    private boolean updateATRAndCheckTSConformance(SPA<?, I> hypothesis) {
        boolean refinement = false;
        Map<I, DFA<?, I>> subModels = hypothesis.getProcedures();

        while (checkAndEnsureTSConformance(subModels)) {
            refinement = true;
            subModels = getSubModels();
            this.atrManager.scanProcedures(subModels, subLearners, activeAlphabet);
        }

        return refinement;
    }

    private List<Integer> determineReturnIndices(Word<I> input) {

        final List<Integer> returnIndices = new ArrayList<>();

        for (int i = 0; i < input.length(); i++) {
            if (this.alphabet.isReturnSymbol(input.getSymbol(i))) {
                returnIndices.add(i);
            }
        }

        return returnIndices;
    }

    private boolean checkAndEnsureTSConformance(Map<I, DFA<?, I>> subModels) {
        boolean refinement = false;

        for (I procedure : this.subLearners.keySet()) {
            final Word<I> terminatingSequence = this.atrManager.getTerminatingSequence(procedure);
            final WordBuilder<I> embeddedTS = new WordBuilder<>(terminatingSequence.size() + 2);
            embeddedTS.append(procedure);
            embeddedTS.append(terminatingSequence);
            embeddedTS.append(alphabet.getReturnSymbol());
            refinement |= checkSingleTerminatingSequence(embeddedTS.toWord(), subModels);
        }

        return refinement;
    }

    private boolean checkSingleTerminatingSequence(Word<I> input, Map<I, DFA<?, I>> hypotheses) {
        boolean refinement = false;

        for (int i = 0; i < input.size(); i++) {
            final I sym = input.getSymbol(i);

            if (this.alphabet.isCallSymbol(sym)) {
                final int returnIdx = this.alphabet.findReturnIndex(input, i + 1);
                final Word<I> projectedRun = this.alphabet.project(input.subWord(i + 1, returnIdx), 0);
                // whenever we extract a terminating sequence, we can also instantiate a learner.
                // Therefore, the existence of the hypothesis is guaranteed.
                @SuppressWarnings("assignment.type.incompatible")
                final @NonNull DFA<?, I> hyp = hypotheses.get(sym);

                if (!hyp.accepts(projectedRun)) {
                    refinement = true;
                    subLearners.get(sym).refineHypothesis(new DefaultQuery<>(projectedRun, true));
                }
            }
        }

        return refinement;
    }

    private class Acex extends AbstractBaseCounterexample<Boolean> {

        private final Word<I> input;
        private final Predicate<? super Word<I>> oracle;
        private final List<Integer> returnIndices;

        Acex(Word<I> input, Predicate<? super Word<I>> oracle, List<Integer> returnIndices) {
            super(returnIndices.size() + 1);
            this.input = input;
            this.oracle = oracle;
            this.returnIndices = returnIndices;

            setEffect(returnIndices.size(), true);
            setEffect(0, false);
        }

        @Override
        protected Boolean computeEffect(int index) {
            final Deque<Word<I>> wordStack = new ArrayDeque<>();
            int idx = this.returnIndices.get(index);

            while (idx > 0) {
                final int callIdx = alphabet.findCallIndex(input, idx);
                final I callSymbol = input.getSymbol(callIdx);
                final Word<I> normalized = alphabet.project(input.subWord(callIdx + 1, idx), 0);
                final Word<I> expanded = alphabet.expand(normalized, atrManager::getTerminatingSequence);

                wordStack.push(expanded.prepend(callSymbol));

                idx = callIdx;
            }

            final WordBuilder<I> builder = new WordBuilder<>();
            wordStack.forEach(builder::append);
            builder.append(input.subWord(this.returnIndices.get(index)));

            return oracle.test(builder.toWord());
        }

        @Override
        public boolean checkEffects(Boolean eff1, Boolean eff2) {
            return Objects.equals(eff1, eff2);
        }
    }
}

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.spa;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collections;
21	import java.util.Deque;
22	import java.util.List;
23	import java.util.Map;
24	import java.util.Objects;
25	import java.util.Set;
26	import java.util.function.Predicate;
27
28	import com.google.common.collect.Maps;
29	import com.google.common.collect.Sets;
30	import de.learnlib.acex.AcexAnalyzer;
31	import de.learnlib.acex.analyzers.AcexAnalyzers;
32	import de.learnlib.acex.impl.AbstractBaseCounterexample;
33	import de.learnlib.algorithms.procedural.spa.manager.OptimizingATRManager;
34	import de.learnlib.api.AccessSequenceTransformer;
35	import de.learnlib.api.algorithm.LearnerConstructor;
36	import de.learnlib.api.algorithm.LearningAlgorithm;
37	import de.learnlib.api.algorithm.LearningAlgorithm.DFALearner;
38	import de.learnlib.api.oracle.MembershipOracle;
39	import de.learnlib.api.query.DefaultQuery;
40	import de.learnlib.util.MQUtil;
41	import net.automatalib.SupportsGrowingAlphabet;
42	import net.automatalib.automata.fsa.DFA;
43	import net.automatalib.automata.procedural.EmptySPA;
44	import net.automatalib.automata.procedural.SPA;
45	import net.automatalib.automata.procedural.StackSPA;
46	import net.automatalib.commons.util.mappings.Mapping;
47	import net.automatalib.words.ProceduralInputAlphabet;
48	import net.automatalib.words.Word;
49	import net.automatalib.words.WordBuilder;
50	import net.automatalib.words.impl.GrowingMapAlphabet;
51	import org.checkerframework.checker.nullness.qual.NonNull;
52
53	/**
54	* A learning algorithm for {@link SPA}s.
55	*
56	* @param <I>
57	* input symbol type
58	* @param <L>
59	* sub-learner type
60	*/
61	public class SPALearner<I, L extends DFALearner<I> & SupportsGrowingAlphabet<I> & AccessSequenceTransformer<I>>	2✔
62	implements LearningAlgorithm<SPA<?, I>, I, Boolean> {
63
64	private final ProceduralInputAlphabet<I> alphabet;
65	private final MembershipOracle<I, Boolean> oracle;
66	private final Mapping<I, LearnerConstructor<L, I, Boolean>> learnerConstructors;
67	private final AcexAnalyzer analyzer;
68	private final ATRManager<I> atrManager;
69
70	private final Map<I, L> subLearners;
71	private final Set<I> activeAlphabet;
72	private I initialCallSymbol;
73
74	public SPALearner(ProceduralInputAlphabet<I> alphabet,
75	MembershipOracle<I, Boolean> oracle,
76	LearnerConstructor<L, I, Boolean> learnerConstructor) {
77	this(alphabet,	×
78	oracle,
79	(i) -> learnerConstructor,	×
80	AcexAnalyzers.BINARY_SEARCH_FWD,
81	new OptimizingATRManager<>(alphabet));
82	}	×
83
84	public SPALearner(ProceduralInputAlphabet<I> alphabet,
85	MembershipOracle<I, Boolean> oracle,
86	Mapping<I, LearnerConstructor<L, I, Boolean>> learnerConstructors,
87	AcexAnalyzer analyzer,
88	ATRManager<I> atrManager) {	2✔
89	this.alphabet = alphabet;	2✔
90	this.oracle = oracle;	2✔
91	this.learnerConstructors = learnerConstructors;	2✔
92	this.analyzer = analyzer;	2✔
93	this.atrManager = atrManager;	2✔
94
95	this.subLearners = Maps.newHashMapWithExpectedSize(this.alphabet.getNumCalls());	2✔
96	this.activeAlphabet = Sets.newHashSetWithExpectedSize(alphabet.getNumCalls() + alphabet.getNumInternals());	2✔
97	this.activeAlphabet.addAll(alphabet.getInternalAlphabet());	2✔
98	}	2✔
99
100	@Override
101	public void startLearning() {
102	// do nothing, as we have to wait for evidence that the potential main procedure actually terminates
103	}	2✔
104
105	@Override
106	public boolean refineHypothesis(DefaultQuery<I, Boolean> defaultQuery) {
107
108	assert this.alphabet.isWellMatched(defaultQuery.getInput());	2✔
109
110	boolean changed = this.extractUsefulInformationFromCounterExample(defaultQuery);	2✔
111
112	while (refineHypothesisInternal(defaultQuery)) {	2✔
113	changed = true;	2✔
114	}
115
116	return changed;	2✔
117	}
118
119	private boolean refineHypothesisInternal(DefaultQuery<I, Boolean> defaultQuery) {
120
121	final SPA<?, I> hypothesis = this.getHypothesisModel();	2✔
122
123	if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) {	2✔
124	return false;	2✔
125	}
126
127	// look for better sequences and ensure TS conformance prior to CE analysis
128	boolean localRefinement = updateATRAndCheckTSConformance(hypothesis);	2✔
129
130	if (!MQUtil.isCounterexample(defaultQuery, hypothesis)) {	2✔
131	return localRefinement;	2✔
132	}
133
134	final Word<I> input = defaultQuery.getInput();	2✔
135	final List<Integer> returnIndices = determineReturnIndices(input);	2✔
136	final int idx = analyzer.analyzeAbstractCounterexample(new Acex(input,	2✔
137	defaultQuery.getOutput() ?	2✔
138	hypothesis::accepts :
139	this.oracle::answerQuery,
140	returnIndices));
141	final int returnIdx = returnIndices.get(idx);	2✔
142
143	// extract local ce
144	final int callIdx = this.alphabet.findCallIndex(input, returnIdx);	2✔
145	final I procedure = input.getSymbol(callIdx);	2✔
146
147	final Word<I> localTrace = this.alphabet.project(input.subWord(callIdx + 1, returnIdx), 0);	2✔
148	final DefaultQuery<I, Boolean> localCE = new DefaultQuery<>(localTrace, defaultQuery.getOutput());	2✔
149
150	localRefinement \|= this.subLearners.get(procedure).refineHypothesis(localCE);	2✔
151	assert localRefinement;	2✔
152
153	return true;	2✔
154	}
155
156	@Override
157	public SPA<?, I> getHypothesisModel() {
158
159	if (this.subLearners.isEmpty()) {	2✔
160	return new EmptySPA<>(this.alphabet);	2✔
161	}
162
163	return new StackSPA<>(alphabet, initialCallSymbol, getSubModels());	2✔
164	}
165
166	private boolean extractUsefulInformationFromCounterExample(DefaultQuery<I, Boolean> defaultQuery) {
167
168	if (!defaultQuery.getOutput()) {	2✔
169	return false;	2✔
170	}
171
172	final Word<I> input = defaultQuery.getInput();	2✔
173
174	// positive CEs should always be rooted at the main procedure
175	this.initialCallSymbol = input.firstSymbol();	2✔
176
177	final Set<I> newProcedures = atrManager.scanPositiveCounterexample(input);	2✔
178
179	for (I sym : newProcedures) {	2✔
180	final L newLearner = learnerConstructors.get(sym)	2✔
181	.constructLearner(new GrowingMapAlphabet<>(alphabet.getInternalAlphabet()),	2✔
182	new ProceduralMembershipOracle<>(alphabet,
183	oracle,
184	sym,
185	atrManager));
186	// add existing procedures (without itself) to new learner
187	for (I call : this.subLearners.keySet()) {	2✔
188	newLearner.addAlphabetSymbol(call);	2✔
189	}	2✔
190
191	newLearner.startLearning();	2✔
192
193	// add new learner here, so that we have an AccessSequenceTransformer available when scanning for shorter ts
194	this.subLearners.put(sym, newLearner);	2✔
195
196	// try to find a shorter terminating sequence for 'sym' before procedure is added to other hypotheses
197	this.atrManager.scanProcedures(Collections.singletonMap(sym, newLearner.getHypothesisModel()),	2✔
198	subLearners,
199	activeAlphabet);
200	this.activeAlphabet.add(sym);	2✔
201
202	// add the new procedure (with a possibly shorter ts) to all learners (including the new one)
203	for (L learner : this.subLearners.values()) {	2✔
204	learner.addAlphabetSymbol(sym);	2✔
205	}	2✔
206	}	2✔
207
208	if (!newProcedures.isEmpty()) {	2✔
209	this.atrManager.scanProcedures(getSubModels(), subLearners, activeAlphabet);	2✔
210	return true;	2✔
211	} else {
212	return false;	2✔
213	}
214	}
215
216	private Map<I, DFA<?, I>> getSubModels() {
217	final Map<I, DFA<?, I>> subModels = Maps.newHashMapWithExpectedSize(this.subLearners.size());	2✔
218
219	for (Map.Entry<I, L> entry : this.subLearners.entrySet()) {	2✔
220	subModels.put(entry.getKey(), entry.getValue().getHypothesisModel());	2✔
221	}	2✔
222
223	return subModels;	2✔
224	}
225
226	private boolean updateATRAndCheckTSConformance(SPA<?, I> hypothesis) {
227	boolean refinement = false;	2✔
228	Map<I, DFA<?, I>> subModels = hypothesis.getProcedures();	2✔
229
230	while (checkAndEnsureTSConformance(subModels)) {	2✔
231	refinement = true;	2✔
232	subModels = getSubModels();	2✔
233	this.atrManager.scanProcedures(subModels, subLearners, activeAlphabet);	2✔
234	}
235
236	return refinement;	2✔
237	}
238
239	private List<Integer> determineReturnIndices(Word<I> input) {
240
241	final List<Integer> returnIndices = new ArrayList<>();	2✔
242
243	for (int i = 0; i < input.length(); i++) {	2✔
244	if (this.alphabet.isReturnSymbol(input.getSymbol(i))) {	2✔
245	returnIndices.add(i);	2✔
246	}
247	}
248
249	return returnIndices;	2✔
250	}
251
252	private boolean checkAndEnsureTSConformance(Map<I, DFA<?, I>> subModels) {
253	boolean refinement = false;	2✔
254
255	for (I procedure : this.subLearners.keySet()) {	2✔
256	final Word<I> terminatingSequence = this.atrManager.getTerminatingSequence(procedure);	2✔
257	final WordBuilder<I> embeddedTS = new WordBuilder<>(terminatingSequence.size() + 2);	2✔
258	embeddedTS.append(procedure);	2✔
259	embeddedTS.append(terminatingSequence);	2✔
260	embeddedTS.append(alphabet.getReturnSymbol());	2✔
261	refinement \|= checkSingleTerminatingSequence(embeddedTS.toWord(), subModels);	2✔
262	}	2✔
263
264	return refinement;	2✔
265	}
266
267	private boolean checkSingleTerminatingSequence(Word<I> input, Map<I, DFA<?, I>> hypotheses) {
268	boolean refinement = false;	2✔
269
270	for (int i = 0; i < input.size(); i++) {	2✔
271	final I sym = input.getSymbol(i);	2✔
272
273	if (this.alphabet.isCallSymbol(sym)) {	2✔
274	final int returnIdx = this.alphabet.findReturnIndex(input, i + 1);	2✔
275	final Word<I> projectedRun = this.alphabet.project(input.subWord(i + 1, returnIdx), 0);	2✔
276	// whenever we extract a terminating sequence, we can also instantiate a learner.
277	// Therefore, the existence of the hypothesis is guaranteed.
278	@SuppressWarnings("assignment.type.incompatible")
279	final @NonNull DFA<?, I> hyp = hypotheses.get(sym);	2✔
280
281	if (!hyp.accepts(projectedRun)) {	2✔
282	refinement = true;	2✔
283	subLearners.get(sym).refineHypothesis(new DefaultQuery<>(projectedRun, true));	2✔
284	}
285	}
286	}
287
288	return refinement;	2✔
289	}
290
291	private class Acex extends AbstractBaseCounterexample<Boolean> {
292
293	private final Word<I> input;
294	private final Predicate<? super Word<I>> oracle;
295	private final List<Integer> returnIndices;
296
297	Acex(Word<I> input, Predicate<? super Word<I>> oracle, List<Integer> returnIndices) {	2✔
298	super(returnIndices.size() + 1);	2✔
299	this.input = input;	2✔
300	this.oracle = oracle;	2✔
301	this.returnIndices = returnIndices;	2✔
302
303	setEffect(returnIndices.size(), true);	2✔
304	setEffect(0, false);	2✔
305	}	2✔
306
307	@Override
308	protected Boolean computeEffect(int index) {
309	final Deque<Word<I>> wordStack = new ArrayDeque<>();	2✔
310	int idx = this.returnIndices.get(index);	2✔
311
312	while (idx > 0) {	2✔
313	final int callIdx = alphabet.findCallIndex(input, idx);	2✔
314	final I callSymbol = input.getSymbol(callIdx);	2✔
315	final Word<I> normalized = alphabet.project(input.subWord(callIdx + 1, idx), 0);	2✔
316	final Word<I> expanded = alphabet.expand(normalized, atrManager::getTerminatingSequence);	2✔
317
318	wordStack.push(expanded.prepend(callSymbol));	2✔
319
320	idx = callIdx;	2✔
321	}	2✔
322
323	final WordBuilder<I> builder = new WordBuilder<>();	2✔
324	wordStack.forEach(builder::append);	2✔
325	builder.append(input.subWord(this.returnIndices.get(index)));	2✔
326
327	return oracle.test(builder.toWord());	2✔
328	}
329
330	@Override
331	public boolean checkEffects(Boolean eff1, Boolean eff2) {
332	return Objects.equals(eff1, eff2);	2✔
333	}
334	}
335	}

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