6412002873

Committed 04 Oct 2023 10:05PM UTC coverage: 92.303% (+0.02%) from 92.282%

Build # 6412002873

Build Type

push

github

Committed by

mtf90

Commit Message

further tweak versions

* downgrade maven-javadoc-plugin version because it (for whatever reason) doesn't work on Java 11+
* update previously missed doc skin version

Run Details

11573 of 12538 relevant lines covered (92.3%)

1.67 hits per line

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

95.6

/algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/ads/DefensiveADS.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.adt.ads;

import java.util.BitSet;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Optional;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;

import de.learnlib.algorithms.adt.adt.ADTLeafNode;
import de.learnlib.algorithms.adt.adt.ADTNode;
import de.learnlib.algorithms.adt.api.PartialTransitionAnalyzer;
import de.learnlib.algorithms.adt.util.ADTUtil;
import net.automatalib.automata.concepts.StateIDs;
import net.automatalib.automata.transducers.MealyMachine;
import net.automatalib.commons.smartcollections.ReflexiveMapView;
import net.automatalib.commons.util.Pair;
import net.automatalib.util.automata.ads.ADSUtil;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A variant of the backtracking ADS search (see {@link net.automatalib.util.automata.ads.ADS}, {@link
 * net.automatalib.util.automata.ads.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
 *
 * @author frohme
 */
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 LinkedList<>();
        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 = mapping.keySet()
                                                             .stream()
                                                             .collect(Collectors.toMap(x -> automaton.getSuccessor(x,
                                                                                                                   prefix),
                                                                                       mapping::get));
            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 HashSet<>();
                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 = new HashMap<>();
                        successors.put(nextOutput, nextMapping);
                    } else {
                        nextMapping = successors.get(nextOutput);
                    }

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

LearnLib / learnlib / 6412002873

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