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

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

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