13166566074

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

Build # 13166566074

Build Type

push

github

Committed by

mtf90

Commit Message

test api conformance

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

Run Details

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

19 existing lines in 4 files now uncovered.

12484 of 13229 relevant lines covered (94.37%)

1.72 hits per line

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

96.74

/algorithms/active/adt/src/main/java/de/learnlib/algorithm/adt/ads/DefensiveADS.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of LearnLib <https://learnlib.de>.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package de.learnlib.algorithm.adt.ads;

import java.util.ArrayDeque;
import java.util.BitSet;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;

import de.learnlib.algorithm.adt.adt.ADTLeafNode;
import de.learnlib.algorithm.adt.adt.ADTNode;
import de.learnlib.algorithm.adt.api.PartialTransitionAnalyzer;
import de.learnlib.algorithm.adt.util.ADTUtil;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.concept.StateIDs;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.smartcollection.ReflexiveMapView;
import net.automatalib.common.util.HashUtil;
import net.automatalib.common.util.Pair;
import net.automatalib.util.automaton.ads.ADS;
import net.automatalib.util.automaton.ads.ADSUtil;
import net.automatalib.util.automaton.ads.BacktrackingSearch;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A variant of the backtracking ADS search (see {@link ADS}, {@link BacktrackingSearch}), that works on partially
 * defined automata. It tries to find an ADS based on defined transitions and successively closes transitions if no ADS
 * has been found.
 *
 * @param <S>
 *         (hypothesis) state type
 * @param <I>
 *         input alphabet type
 * @param <O>
 *         output alphabet type
 */
public final class DefensiveADS<S, I, O> {

    private final MealyMachine<S, I, ?, O> automaton;
    private final Alphabet<I> alphabet;
    private final Set<S> states;
    private final PartialTransitionAnalyzer<S, I> partialTransitionAnalyzer;
    /**
     * The states, whose outgoing {@link #refinementInput}-transitions need to be closed.
     */
    private @Nullable Set<S> refinementStates;
    /**
     * The output for which the outgoing transitions of {@link #refinementStates} are undefined.
     */
    private @Nullable I refinementInput;

    private DefensiveADS(MealyMachine<S, I, ?, O> automaton,
                         Alphabet<I> alphabet,
                         Set<S> states,
                         PartialTransitionAnalyzer<S, I> partialTransitionAnalyzer) {
        this.automaton = automaton;
        this.alphabet = alphabet;
        this.states = states;
        this.partialTransitionAnalyzer = partialTransitionAnalyzer;
    }

    /**
     * Compute an adaptive distinguishing sequence (as an ADT) for the given automaton and the given set of states.
     *
     * @param automaton
     *         the automaton for which an ADS should be computed
     * @param alphabet
     *         the input alphabet of the automaton
     * @param states
     *         the set of states which should be distinguished by the computed ADS
     * @param pta
     *         the analyzer to inspect and close partial transitions
     * @param <S>
     *         (hypothesis) state type
     * @param <I>
     *         input alphabet type
     * @param <O>
     *         output alphabet type
     *
     * @return {@code Optional.empty()} if there exists no ADS that distinguishes the given states, a valid ADS
     * otherwise.
     */
    public static <S, I, O> Optional<ADTNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
                                                               Alphabet<I> alphabet,
                                                               Set<S> states,
                                                               PartialTransitionAnalyzer<S, I> pta) {

        return new DefensiveADS<>(automaton, alphabet, states, pta).compute();
    }

    private Optional<ADTNode<S, I, O>> compute() {

        final Map<S, S> initialMapping = new ReflexiveMapView<>(states);
        Optional<ADTNode<S, I, O>> interMediateResult = compute(initialMapping);

        while (!interMediateResult.isPresent()) {

            // we encountered open transitions that can be closed
            if (refinementStates != null && refinementInput != null) {
                for (S s : refinementStates) {
                    this.partialTransitionAnalyzer.closeTransition(s, this.refinementInput);
                }
                this.refinementStates = null;
                this.refinementInput = null;
            } else { // no ADS found
                break;
            }

            // retry with updated hypothesis
            interMediateResult = compute(initialMapping);
        }

        return interMediateResult;
    }

    private Optional<ADTNode<S, I, O>> compute(Map<S, S> mapping) {

        final long maximumSplittingWordLength =
                ADSUtil.computeMaximumSplittingWordLength(automaton.size(), mapping.size(), this.states.size());
        final Queue<Word<I>> splittingWordCandidates = new ArrayDeque<>();
        final StateIDs<S> stateIds = automaton.stateIDs();
        final Set<BitSet> cache = new HashSet<>();

        splittingWordCandidates.add(Word.epsilon());

        while (!splittingWordCandidates.isEmpty()) {

            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            final @NonNull Word<I> prefix = splittingWordCandidates.poll();
            final Map<S, S> currentToInitialMapping = new LinkedHashMap<>(HashUtil.capacity(mapping.size()));

            for (Entry<S, S> e : mapping.entrySet()) {
                currentToInitialMapping.put(automaton.getSuccessor(e.getKey(), prefix), e.getValue());
            }

            final BitSet currentSetAsBitSet = new BitSet();
            for (S s : currentToInitialMapping.keySet()) {
                currentSetAsBitSet.set(stateIds.getStateId(s));
            }

            if (cache.contains(currentSetAsBitSet)) {
                continue;
            }

            oneSymbolFuture:
            for (I i : this.alphabet) {

                //check for missing transitions
                final Set<S> statesWithMissingTransitions = new LinkedHashSet<>();
                for (S s : currentToInitialMapping.keySet()) {
                    if (!this.partialTransitionAnalyzer.isTransitionDefined(s, i)) {
                        statesWithMissingTransitions.add(s);
                    }
                }

                // if we encountered undefined transitions, stop further search
                if (!statesWithMissingTransitions.isEmpty()) {

                    // override existing refinement candidate, if we can assure progress with fewer transitions to refine
                    if (refinementStates == null || statesWithMissingTransitions.size() < refinementStates.size()) {
                        refinementStates = statesWithMissingTransitions;
                        refinementInput = i;
                    }

                    continue;
                }

                // compute successors
                final Map<O, Map<S, S>> successors = new HashMap<>();

                for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {
                    final S current = entry.getKey();
                    final S nextState = automaton.getSuccessor(current, i);
                    final O nextOutput = automaton.getOutput(current, i);

                    final Map<S, S> nextMapping;
                    if (successors.containsKey(nextOutput)) {
                        nextMapping = successors.get(nextOutput);
                    } else {
                        nextMapping = new HashMap<>();
                        successors.put(nextOutput, nextMapping);
                    }

                    // invalid input
                    if (nextMapping.put(nextState, entry.getValue()) != null) {
                        continue oneSymbolFuture;
                    }
                }

                //splitting word
                if (successors.size() > 1) {
                    final Map<O, ADTNode<S, I, O>> results = new HashMap<>();

                    for (Map.Entry<O, Map<S, S>> entry : successors.entrySet()) {

                        final Map<S, S> currentMapping = entry.getValue();

                        final BitSet currentNodeAsBitSet = new BitSet();
                        for (S s : currentMapping.keySet()) {
                            currentNodeAsBitSet.set(stateIds.getStateId(s));
                        }

                        if (cache.contains(currentNodeAsBitSet)) {
                            continue oneSymbolFuture;
                        }

                        final Optional<ADTNode<S, I, O>> succ;
                        if (currentMapping.size() > 1) {
                            succ = compute(currentMapping);
                        } else {
                            final S s = currentMapping.values().iterator().next();
                            succ = Optional.of(new ADTLeafNode<>(null, s));
                        }

                        if (!succ.isPresent()) {
                            cache.add(currentNodeAsBitSet);
                            continue oneSymbolFuture;
                        }

                        results.put(entry.getKey(), succ.get());
                    }

                    // create ADS (if we haven't continued until here)
                    final Pair<ADTNode<S, I, O>, ADTNode<S, I, O>> ads =
                            ADTUtil.buildADSFromTrace(automaton, prefix.append(i), mapping.keySet().iterator().next());
                    final ADTNode<S, I, O> head = ads.getFirst();
                    final ADTNode<S, I, O> tail = ads.getSecond();

                    for (Map.Entry<O, ADTNode<S, I, O>> entry : results.entrySet()) {
                        entry.getValue().setParent(tail);
                        tail.getChildren().put(entry.getKey(), entry.getValue());
                    }

                    return Optional.of(head);
                } else if (prefix.length() < maximumSplittingWordLength) { // no splitting word
                    splittingWordCandidates.add(prefix.append(i));
                }
            }

            cache.add(currentSetAsBitSet);
        }

        return Optional.empty();
    }
}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of LearnLib <https://learnlib.de>.
3	*
4	* Licensed under the Apache License, Version 2.0 (the "License");
5	* you may not use this file except in compliance with the License.
6	* You may obtain a copy of the License at
7	*
8	* http://www.apache.org/licenses/LICENSE-2.0
9	*
10	* Unless required by applicable law or agreed to in writing, software
11	* distributed under the License is distributed on an "AS IS" BASIS,
12	* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13	* See the License for the specific language governing permissions and
14	* limitations under the License.
15	*/
16	package de.learnlib.algorithm.adt.ads;
17
18	import java.util.ArrayDeque;
19	import java.util.BitSet;
20	import java.util.HashMap;
21	import java.util.HashSet;
22	import java.util.LinkedHashMap;
23	import java.util.LinkedHashSet;
24	import java.util.Map;
25	import java.util.Map.Entry;
26	import java.util.Optional;
27	import java.util.Queue;
28	import java.util.Set;
29
30	import de.learnlib.algorithm.adt.adt.ADTLeafNode;
31	import de.learnlib.algorithm.adt.adt.ADTNode;
32	import de.learnlib.algorithm.adt.api.PartialTransitionAnalyzer;
33	import de.learnlib.algorithm.adt.util.ADTUtil;
34	import net.automatalib.alphabet.Alphabet;
35	import net.automatalib.automaton.concept.StateIDs;
36	import net.automatalib.automaton.transducer.MealyMachine;
37	import net.automatalib.common.smartcollection.ReflexiveMapView;
38	import net.automatalib.common.util.HashUtil;
39	import net.automatalib.common.util.Pair;
40	import net.automatalib.util.automaton.ads.ADS;
41	import net.automatalib.util.automaton.ads.ADSUtil;
42	import net.automatalib.util.automaton.ads.BacktrackingSearch;
43	import net.automatalib.word.Word;
44	import org.checkerframework.checker.nullness.qual.NonNull;
45	import org.checkerframework.checker.nullness.qual.Nullable;
46
47	/**
48	* A variant of the backtracking ADS search (see {@link ADS}, {@link BacktrackingSearch}), that works on partially
49	* defined automata. It tries to find an ADS based on defined transitions and successively closes transitions if no ADS
50	* has been found.
51	*
52	* @param <S>
53	* (hypothesis) state type
54	* @param <I>
55	* input alphabet type
56	* @param <O>
57	* output alphabet type
58	*/
59	public final class DefensiveADS<S, I, O> {
60
61	private final MealyMachine<S, I, ?, O> automaton;
62	private final Alphabet<I> alphabet;
63	private final Set<S> states;
64	private final PartialTransitionAnalyzer<S, I> partialTransitionAnalyzer;
65	/**
66	* The states, whose outgoing {@link #refinementInput}-transitions need to be closed.
67	*/
68	private @Nullable Set<S> refinementStates;
69	/**
70	* The output for which the outgoing transitions of {@link #refinementStates} are undefined.
71	*/
72	private @Nullable I refinementInput;
73
74	private DefensiveADS(MealyMachine<S, I, ?, O> automaton,
75	Alphabet<I> alphabet,
76	Set<S> states,
77	PartialTransitionAnalyzer<S, I> partialTransitionAnalyzer) {	2✔
78	this.automaton = automaton;	2✔
79	this.alphabet = alphabet;	2✔
80	this.states = states;	2✔
81	this.partialTransitionAnalyzer = partialTransitionAnalyzer;	2✔
82	}	2✔
83
84	/**
85	* Compute an adaptive distinguishing sequence (as an ADT) for the given automaton and the given set of states.
86	*
87	* @param automaton
88	* the automaton for which an ADS should be computed
89	* @param alphabet
90	* the input alphabet of the automaton
91	* @param states
92	* the set of states which should be distinguished by the computed ADS
93	* @param pta
94	* the analyzer to inspect and close partial transitions
95	* @param <S>
96	* (hypothesis) state type
97	* @param <I>
98	* input alphabet type
99	* @param <O>
100	* output alphabet type
101	*
102	* @return {@code Optional.empty()} if there exists no ADS that distinguishes the given states, a valid ADS
103	* otherwise.
104	*/
105	public static <S, I, O> Optional<ADTNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
106	Alphabet<I> alphabet,
107	Set<S> states,
108	PartialTransitionAnalyzer<S, I> pta) {
109
110	return new DefensiveADS<>(automaton, alphabet, states, pta).compute();	2✔
111	}
112
113	private Optional<ADTNode<S, I, O>> compute() {
114
115	final Map<S, S> initialMapping = new ReflexiveMapView<>(states);	2✔
116	Optional<ADTNode<S, I, O>> interMediateResult = compute(initialMapping);	2✔
117
118	while (!interMediateResult.isPresent()) {	2✔
119
120	// we encountered open transitions that can be closed
121	if (refinementStates != null && refinementInput != null) {	2✔
122	for (S s : refinementStates) {	2✔
123	this.partialTransitionAnalyzer.closeTransition(s, this.refinementInput);	2✔
124	}	2✔
125	this.refinementStates = null;	2✔
126	this.refinementInput = null;	2✔
127	} else { // no ADS found
128	break;
129	}
130
131	// retry with updated hypothesis
132	interMediateResult = compute(initialMapping);	2✔
133	}
134
135	return interMediateResult;	2✔
136	}
137
138	private Optional<ADTNode<S, I, O>> compute(Map<S, S> mapping) {
139
140	final long maximumSplittingWordLength =	2✔
141	ADSUtil.computeMaximumSplittingWordLength(automaton.size(), mapping.size(), this.states.size());	2✔
142	final Queue<Word<I>> splittingWordCandidates = new ArrayDeque<>();	2✔
143	final StateIDs<S> stateIds = automaton.stateIDs();	2✔
144	final Set<BitSet> cache = new HashSet<>();	2✔
145
146	splittingWordCandidates.add(Word.epsilon());	2✔
147
148	while (!splittingWordCandidates.isEmpty()) {	2✔
149
150	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
151	final @NonNull Word<I> prefix = splittingWordCandidates.poll();	2✔
152	final Map<S, S> currentToInitialMapping = new LinkedHashMap<>(HashUtil.capacity(mapping.size()));	2✔
153
154	for (Entry<S, S> e : mapping.entrySet()) {	2✔
155	currentToInitialMapping.put(automaton.getSuccessor(e.getKey(), prefix), e.getValue());	2✔
156	}	2✔
157
158	final BitSet currentSetAsBitSet = new BitSet();	2✔
159	for (S s : currentToInitialMapping.keySet()) {	2✔
160	currentSetAsBitSet.set(stateIds.getStateId(s));	2✔
161	}	2✔
162
163	if (cache.contains(currentSetAsBitSet)) {	2✔
164	continue;	2✔
165	}
166
167	oneSymbolFuture:
168	for (I i : this.alphabet) {	2✔
169
170	//check for missing transitions
171	final Set<S> statesWithMissingTransitions = new LinkedHashSet<>();	2✔
172	for (S s : currentToInitialMapping.keySet()) {	2✔
173	if (!this.partialTransitionAnalyzer.isTransitionDefined(s, i)) {	2✔
174	statesWithMissingTransitions.add(s);	2✔
175	}
176	}	2✔
177
178	// if we encountered undefined transitions, stop further search
179	if (!statesWithMissingTransitions.isEmpty()) {	2✔
180
181	// override existing refinement candidate, if we can assure progress with fewer transitions to refine
182	if (refinementStates == null \|\| statesWithMissingTransitions.size() < refinementStates.size()) {	2✔
183	refinementStates = statesWithMissingTransitions;	2✔
184	refinementInput = i;	2✔
185	}
186
187	continue;
188	}
189
190	// compute successors
191	final Map<O, Map<S, S>> successors = new HashMap<>();	2✔
192
193	for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {	2✔
194	final S current = entry.getKey();	2✔
195	final S nextState = automaton.getSuccessor(current, i);	2✔
196	final O nextOutput = automaton.getOutput(current, i);	2✔
197
198	final Map<S, S> nextMapping;
199	if (successors.containsKey(nextOutput)) {	2✔
200	nextMapping = successors.get(nextOutput);	2✔
201	} else {
202	nextMapping = new HashMap<>();	2✔
203	successors.put(nextOutput, nextMapping);	2✔
204	}
205
206	// invalid input
207	if (nextMapping.put(nextState, entry.getValue()) != null) {	2✔
208	continue oneSymbolFuture;	2✔
209	}
210	}	2✔
211
212	//splitting word
213	if (successors.size() > 1) {	2✔
214	final Map<O, ADTNode<S, I, O>> results = new HashMap<>();	2✔
215
216	for (Map.Entry<O, Map<S, S>> entry : successors.entrySet()) {	2✔
217
218	final Map<S, S> currentMapping = entry.getValue();	2✔
219
220	final BitSet currentNodeAsBitSet = new BitSet();	2✔
221	for (S s : currentMapping.keySet()) {	2✔
222	currentNodeAsBitSet.set(stateIds.getStateId(s));	2✔
223	}	2✔
224
225	if (cache.contains(currentNodeAsBitSet)) {	2✔
UNCOV 226	continue oneSymbolFuture;	×
227	}
228
229	final Optional<ADTNode<S, I, O>> succ;
230	if (currentMapping.size() > 1) {	2✔
231	succ = compute(currentMapping);	2✔
232	} else {
233	final S s = currentMapping.values().iterator().next();	2✔
234	succ = Optional.of(new ADTLeafNode<>(null, s));	2✔
235	}
236
237	if (!succ.isPresent()) {	2✔
UNCOV 238	cache.add(currentNodeAsBitSet);	×
UNCOV 239	continue oneSymbolFuture;	×
240	}
241
242	results.put(entry.getKey(), succ.get());	2✔
243	}	2✔
244
245	// create ADS (if we haven't continued until here)
246	final Pair<ADTNode<S, I, O>, ADTNode<S, I, O>> ads =	2✔
247	ADTUtil.buildADSFromTrace(automaton, prefix.append(i), mapping.keySet().iterator().next());	2✔
248	final ADTNode<S, I, O> head = ads.getFirst();	2✔
249	final ADTNode<S, I, O> tail = ads.getSecond();	2✔
250
251	for (Map.Entry<O, ADTNode<S, I, O>> entry : results.entrySet()) {	2✔
252	entry.getValue().setParent(tail);	2✔
253	tail.getChildren().put(entry.getKey(), entry.getValue());	2✔
254	}	2✔
255
256	return Optional.of(head);	2✔
257	} else if (prefix.length() < maximumSplittingWordLength) { // no splitting word	2✔
258	splittingWordCandidates.add(prefix.append(i));	2✔
259	}
260	}	2✔
261
262	cache.add(currentSetAsBitSet);	2✔
263	}	2✔
264
265	return Optional.empty();	2✔
266	}
267	}

LearnLib / learnlib / 13166566074

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

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