13138848026

Committed 04 Feb 2025 02:53PM UTC coverage: 92.108% (+2.2%) from 89.877%

Build # 13138848026

Build Type

push

github

Committed by

mtf90

Commit Message

[maven-release-plugin] prepare release automatalib-0.12.0

Run Details

16609 of 18032 relevant lines covered (92.11%)

1.7 hits per line

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

97.06

/util/src/main/java/net/automatalib/util/automaton/equivalence/CharacterizingSets.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://automatalib.net>.
 *
 * 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 net.automatalib.util.automaton.equivalence;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Queue;

import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.automaton.fsa.FiniteStateAcceptor;
import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
import net.automatalib.common.util.collection.CollectionUtil;
import net.automatalib.util.automaton.Automata;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Operations for calculating <i>characterizing sets</i>.
 * <p>
 * A characterizing set for a whole automaton is a set <i>W</i> of words such that for every two states
 * <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i>, there exists a word <i>w &isin; W</i> such that <i>w</i> exposes a
 * difference between <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i> (i.e., either covers a transition with differing
 * property (or not defined in only one case), or reaching a successor state with differing properties), or there exists
 * no such word at all.
 * <p>
 * A characterizing set for a single state <i>s</i> is a set <i>W</i> of words such that for every state <i>t</i>, there
 * exists a word <i>w &isin; W</i> such that <i>w</i> exposes a difference between <i>s</i> and <i>t</i>, or there
 * exists no such word at all.
 */
public final class CharacterizingSets {

    private CharacterizingSets() {}

    /**
     * Computes a characterizing set for the given automaton.
     *
     * @param automaton
     *         the automaton for which to determine the characterizing set.
     * @param inputs
     *         the input alphabets to consider
     * @param result
     *         the collection in which to store the characterizing words
     * @param <I>
     *         input symbol type
     */
    public static <I> void findCharacterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
                                                 Collection<? extends I> inputs,
                                                 Collection<? super Word<I>> result) {
        findIncrementalCharacterizingSet(automaton, inputs, Collections.emptyList(), result);
    }

    /**
     * Computes a characterizing set for a specified state in the given automaton.
     *
     * @param automaton
     *         the automaton containing the state
     * @param inputs
     *         the input alphabets to consider
     * @param state
     *         the state for which to determine the characterizing set
     * @param result
     *         the collection in which to store the characterizing words
     * @param <S>
     *         state type
     * @param <I>
     *         input symbol type
     */
    public static <S, I> void findCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                    Collection<? extends I> inputs,
                                                    S state,
                                                    Collection<? super Word<I>> result) {

        Object prop = automaton.getStateProperty(state);

        List<S> currentBlock = new ArrayList<>();

        boolean multipleStateProps = false;

        for (S s : automaton) {
            if (Objects.equals(s, state)) {
                continue;
            }

            Object sProp = automaton.getStateProperty(s);
            if (Objects.equals(sProp, prop)) {
                currentBlock.add(s);
            } else {
                multipleStateProps = true;
            }
        }

        if (multipleStateProps) {
            result.add(Word.epsilon());
        }

        while (!currentBlock.isEmpty()) {
            Iterator<S> it = currentBlock.iterator();

            Word<I> suffix = null;
            while (it.hasNext() && suffix == null) {
                S s = it.next();
                suffix = Automata.findSeparatingWord(automaton, state, s, inputs);
            }

            if (suffix == null) {
                return;
            }

            result.add(suffix);

            List<?> trace = buildTrace(automaton, state, suffix);

            List<S> nextBlock = new ArrayList<>();
            while (it.hasNext()) {
                S s = it.next();
                if (checkTrace(automaton, s, suffix, trace)) {
                    nextBlock.add(s);
                }
            }

            currentBlock = nextBlock;
        }
    }

    public static <I> Iterator<Word<I>> characterizingSetIterator(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
                                                                  Collection<? extends I> inputs) {
        return new IncrementalCharacterizingSetIterator<>(automaton, inputs, Collections.emptyList());
    }

    private static <S, I, T, SP, TP> List<?> buildTrace(UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
                                                        S state,
                                                        Word<I> suffix) {
        if (suffix.isEmpty()) {
            SP prop = automaton.getStateProperty(state);
            return Collections.singletonList(prop);
        }
        List<@Nullable Object> trace = new ArrayList<>(2 * suffix.length());

        S curr = state;

        for (I sym : suffix) {
            T trans = automaton.getTransition(curr, sym);

            if (trans == null) {
                return trace;
            }

            TP transitionProperty = automaton.getTransitionProperty(trans);
            trace.add(transitionProperty);

            curr = automaton.getSuccessor(trans);
            SP stateProperty = automaton.getStateProperty(curr);
            trace.add(stateProperty);
        }

        // acceptors are evaluated on the reached state, therefore no prefixes discriminate
        if (automaton instanceof FiniteStateAcceptor) {
            return trace.subList(trace.size() - 2, trace.size());
        }

        return trace;
    }

    private static <S, I, T, SP, TP, P> boolean checkTrace(UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
                                                           S state,
                                                           Word<I> suffix,
                                                           List<P> trace) {

        Iterator<P> it = trace.iterator();
        S curr = state;

        for (I sym : suffix) {
            T trans = automaton.getTransition(curr, sym);

            if (!it.hasNext()) {
                return trans == null;
            } else if (trans == null) {
                return false;
            }

            TP transitionProperty = automaton.getTransitionProperty(trans);

            if (!Objects.equals(transitionProperty, it.next())) {
                return false;
            }

            curr = automaton.getSuccessor(trans);
            SP stateProperty = automaton.getStateProperty(curr);

            if (!Objects.equals(stateProperty, it.next())) {
                return false;
            }
        }

        return true;
    }

    public static <S, I> boolean findIncrementalCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                                  Collection<? extends I> inputs,
                                                                  Collection<? extends Word<I>> oldSuffixes,
                                                                  Collection<? super Word<I>> newSuffixes) {

        boolean refined = false;

        // We need a list to ensure a stable iteration order
        List<? extends Word<I>> oldSuffixList = CollectionUtil.randomAccessList(oldSuffixes);

        Queue<List<S>> blocks = buildInitialBlocks(automaton, oldSuffixList);

        if (!oldSuffixes.contains(Word.epsilon()) && epsilonRefine(automaton, blocks)) {
            newSuffixes.add(Word.epsilon());
            refined = true;
        }

        Word<I> suffix;

        while ((suffix = refine(automaton, inputs, blocks)) != null) {
            newSuffixes.add(suffix);
            refined = true;
        }

        return refined;
    }

    public static <I> Iterator<Word<I>> incrementalCharacterizingSetIterator(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
                                                                             Collection<? extends I> inputs,
                                                                             Collection<? extends Word<I>> oldSuffixes) {
        return new IncrementalCharacterizingSetIterator<>(automaton, inputs, oldSuffixes);
    }

    private static <S, I> Queue<List<S>> buildInitialBlocks(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                            List<? extends Word<I>> oldSuffixes) {
        Map<List<List<?>>, List<S>> initialPartitioning = new HashMap<>();
        Queue<List<S>> blocks = new ArrayDeque<>();
        for (S state : automaton) {
            List<List<?>> sig = buildSignature(automaton, oldSuffixes, state);
            List<S> block = initialPartitioning.get(sig);
            if (block == null) {
                block = new ArrayList<>();
                blocks.add(block);
                initialPartitioning.put(sig, block);
            }
            block.add(state);
        }

        return blocks;
    }

    private static <S, I> List<List<?>> buildSignature(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                       List<? extends Word<I>> suffixes,
                                                       S state) {
        List<List<?>> signature = new ArrayList<>(suffixes.size());

        for (Word<I> suffix : suffixes) {
            List<?> trace = buildTrace(automaton, state, suffix);
            signature.add(trace);
        }

        return signature;
    }

    private static <S, I> boolean epsilonRefine(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                Queue<List<S>> blockQueue) {

        int initialSize = blockQueue.size();

        boolean refined = false;

        for (int i = 0; i < initialSize; i++) {
            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            @NonNull List<S> block = blockQueue.poll();
            if (block.size() <= 1) {
                continue;
            }
            Map<?, List<S>> propCluster = clusterByProperty(automaton, block);
            if (propCluster.size() > 1) {
                refined = true;
            }
            blockQueue.addAll(propCluster.values());
        }

        return refined;
    }

    private static <S, I> @Nullable Word<I> refine(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                                   Collection<? extends I> inputs,
                                                   Queue<List<S>> blockQueue) {

        List<S> currBlock;
        while ((currBlock = blockQueue.poll()) != null) {
            if (currBlock.size() <= 1) {
                continue; // we cannot split further
            }

            Iterator<S> it = currBlock.iterator();

            S ref = it.next();

            Word<I> suffix = null;
            S state = null;
            while (it.hasNext() && suffix == null) {
                state = it.next();
                suffix = Automata.findSeparatingWord(automaton, ref, state, inputs);
            }

            if (state != null && suffix != null) {
                int otherBlocks = blockQueue.size();

                Map<List<?>, List<S>> buckets = new HashMap<>();

                List<S> firstBucket = new ArrayList<>();
                List<S> secondBucket = new ArrayList<>();
                firstBucket.add(ref);
                buckets.put(buildTrace(automaton, ref, suffix), firstBucket);
                secondBucket.add(state);
                buckets.put(buildTrace(automaton, state, suffix), secondBucket);

                cluster(automaton, suffix, it, buckets);

                blockQueue.addAll(buckets.values());

                // Split all other blocks that were in the queue
                for (int i = 0; i < otherBlocks; i++) {
                    @SuppressWarnings("nullness") // we know that there are at least 'otherBlocks' items in the queue
                    @NonNull List<S> otherBlock = blockQueue.poll();
                    if (otherBlock.size() > 1) {
                        buckets.clear();
                        cluster(automaton, suffix, otherBlock.iterator(), buckets);
                        blockQueue.addAll(buckets.values());
                    }
                }

                return suffix;
            }
        }
        return null;
    }

    private static <S, I, SP> Map<?, List<S>> clusterByProperty(UniversalDeterministicAutomaton<S, I, ?, SP, ?> automaton,
                                                                List<S> states) {
        Map<SP, List<S>> result = new HashMap<>();

        for (S state : states) {
            SP prop = automaton.getStateProperty(state);
            List<S> block = result.computeIfAbsent(prop, k -> new ArrayList<>());
            block.add(state);
        }

        return result;
    }

    private static <S, I> void cluster(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                       Word<I> suffix,
                                       Iterator<S> stateIt,
                                       Map<List<?>, List<S>> bucketMap) {

        while (stateIt.hasNext()) {
            S state = stateIt.next();
            List<?> trace = buildTrace(automaton, state, suffix);
            List<S> bucket = bucketMap.computeIfAbsent(trace, k -> new ArrayList<>());
            bucket.add(state);
        }
    }

    private static class IncrementalCharacterizingSetIterator<S, I> extends AbstractSimplifiedIterator<Word<I>> {

        private final UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton;
        private final Collection<? extends I> inputs;
        private final List<? extends Word<I>> oldSuffixes;
        private Queue<List<S>> blocks;

        IncrementalCharacterizingSetIterator(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
                                             Collection<? extends I> inputs,
                                             Collection<? extends Word<I>> oldSuffixes) {
            this.automaton = automaton;
            this.inputs = inputs;
            this.oldSuffixes = CollectionUtil.randomAccessList(oldSuffixes);
        }

        @Override
        protected boolean calculateNext() {
            // first call
            if (blocks == null) {
                blocks = buildInitialBlocks(automaton, oldSuffixes);
                if (!oldSuffixes.contains(Word.epsilon()) && epsilonRefine(automaton, blocks)) {
                    super.nextValue = Word.epsilon();
                    return true;
                }
            }

            final Word<I> suffix = refine(automaton, inputs, blocks);

            if (suffix != null) {
                super.nextValue = suffix;
                return true;
            }
            return false;
        }
    }
}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://automatalib.net>.
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 net.automatalib.util.automaton.equivalence;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collection;
21	import java.util.Collections;
22	import java.util.HashMap;
23	import java.util.Iterator;
24	import java.util.List;
25	import java.util.Map;
26	import java.util.Objects;
27	import java.util.Queue;
28
29	import net.automatalib.automaton.UniversalDeterministicAutomaton;
30	import net.automatalib.automaton.fsa.FiniteStateAcceptor;
31	import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
32	import net.automatalib.common.util.collection.CollectionUtil;
33	import net.automatalib.util.automaton.Automata;
34	import net.automatalib.word.Word;
35	import org.checkerframework.checker.nullness.qual.NonNull;
36	import org.checkerframework.checker.nullness.qual.Nullable;
37
38	/**
39	* Operations for calculating <i>characterizing sets</i>.
40	* <p>
41	* A characterizing set for a whole automaton is a set <i>W</i> of words such that for every two states
42	* <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i>, there exists a word <i>w ∈ W</i> such that <i>w</i> exposes a
43	* difference between <i>s<sub>1</sub></i> and <i>s<sub>2</sub></i> (i.e., either covers a transition with differing
44	* property (or not defined in only one case), or reaching a successor state with differing properties), or there exists
45	* no such word at all.
46	* <p>
47	* A characterizing set for a single state <i>s</i> is a set <i>W</i> of words such that for every state <i>t</i>, there
48	* exists a word <i>w ∈ W</i> such that <i>w</i> exposes a difference between <i>s</i> and <i>t</i>, or there
49	* exists no such word at all.
50	*/
51	public final class CharacterizingSets {
52
53	private CharacterizingSets() {}
54
55	/**
56	* Computes a characterizing set for the given automaton.
57	*
58	* @param automaton
59	* the automaton for which to determine the characterizing set.
60	* @param inputs
61	* the input alphabets to consider
62	* @param result
63	* the collection in which to store the characterizing words
64	* @param <I>
65	* input symbol type
66	*/
67	public static <I> void findCharacterizingSet(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
68	Collection<? extends I> inputs,
69	Collection<? super Word<I>> result) {
70	findIncrementalCharacterizingSet(automaton, inputs, Collections.emptyList(), result);	2✔
71	}	2✔
72
73	/**
74	* Computes a characterizing set for a specified state in the given automaton.
75	*
76	* @param automaton
77	* the automaton containing the state
78	* @param inputs
79	* the input alphabets to consider
80	* @param state
81	* the state for which to determine the characterizing set
82	* @param result
83	* the collection in which to store the characterizing words
84	* @param <S>
85	* state type
86	* @param <I>
87	* input symbol type
88	*/
89	public static <S, I> void findCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
90	Collection<? extends I> inputs,
91	S state,
92	Collection<? super Word<I>> result) {
93
94	Object prop = automaton.getStateProperty(state);	2✔
95
96	List<S> currentBlock = new ArrayList<>();	2✔
97
98	boolean multipleStateProps = false;	2✔
99
100	for (S s : automaton) {	2✔
101	if (Objects.equals(s, state)) {	2✔
102	continue;	2✔
103	}
104
105	Object sProp = automaton.getStateProperty(s);	2✔
106	if (Objects.equals(sProp, prop)) {	2✔
107	currentBlock.add(s);	2✔
108	} else {
109	multipleStateProps = true;	2✔
110	}
111	}	2✔
112
113	if (multipleStateProps) {	2✔
114	result.add(Word.epsilon());	2✔
115	}
116
117	while (!currentBlock.isEmpty()) {	2✔
118	Iterator<S> it = currentBlock.iterator();	2✔
119
120	Word<I> suffix = null;	2✔
121	while (it.hasNext() && suffix == null) {	2✔
122	S s = it.next();	2✔
123	suffix = Automata.findSeparatingWord(automaton, state, s, inputs);	2✔
124	}	2✔
125
126	if (suffix == null) {	2✔
127	return;	×
128	}
129
130	result.add(suffix);	2✔
131
132	List<?> trace = buildTrace(automaton, state, suffix);	2✔
133
134	List<S> nextBlock = new ArrayList<>();	2✔
135	while (it.hasNext()) {	2✔
136	S s = it.next();	2✔
137	if (checkTrace(automaton, s, suffix, trace)) {	2✔
138	nextBlock.add(s);	2✔
139	}
140	}	2✔
141
142	currentBlock = nextBlock;	2✔
143	}	2✔
144	}	2✔
145
146	public static <I> Iterator<Word<I>> characterizingSetIterator(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
147	Collection<? extends I> inputs) {
148	return new IncrementalCharacterizingSetIterator<>(automaton, inputs, Collections.emptyList());	2✔
149	}
150
151	private static <S, I, T, SP, TP> List<?> buildTrace(UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
152	S state,
153	Word<I> suffix) {
154	if (suffix.isEmpty()) {	2✔
155	SP prop = automaton.getStateProperty(state);	×
156	return Collections.singletonList(prop);	×
157	}
158	List<@Nullable Object> trace = new ArrayList<>(2 * suffix.length());	2✔
159
160	S curr = state;	2✔
161
162	for (I sym : suffix) {	2✔
163	T trans = automaton.getTransition(curr, sym);	2✔
164
165	if (trans == null) {	2✔
166	return trace;	2✔
167	}
168
169	TP transitionProperty = automaton.getTransitionProperty(trans);	2✔
170	trace.add(transitionProperty);	2✔
171
172	curr = automaton.getSuccessor(trans);	2✔
173	SP stateProperty = automaton.getStateProperty(curr);	2✔
174	trace.add(stateProperty);	2✔
175	}	2✔
176
177	// acceptors are evaluated on the reached state, therefore no prefixes discriminate
178	if (automaton instanceof FiniteStateAcceptor) {	2✔
179	return trace.subList(trace.size() - 2, trace.size());	2✔
180	}
181
182	return trace;	2✔
183	}
184
185	private static <S, I, T, SP, TP, P> boolean checkTrace(UniversalDeterministicAutomaton<S, I, T, SP, TP> automaton,
186	S state,
187	Word<I> suffix,
188	List<P> trace) {
189
190	Iterator<P> it = trace.iterator();	2✔
191	S curr = state;	2✔
192
193	for (I sym : suffix) {	2✔
194	T trans = automaton.getTransition(curr, sym);	2✔
195
196	if (!it.hasNext()) {	2✔
197	return trans == null;	2✔
198	} else if (trans == null) {	2✔
199	return false;	×
200	}
201
202	TP transitionProperty = automaton.getTransitionProperty(trans);	2✔
203
204	if (!Objects.equals(transitionProperty, it.next())) {	2✔
205	return false;	2✔
206	}
207
208	curr = automaton.getSuccessor(trans);	2✔
209	SP stateProperty = automaton.getStateProperty(curr);	2✔
210
211	if (!Objects.equals(stateProperty, it.next())) {	2✔
212	return false;	2✔
213	}
214	}	2✔
215
216	return true;	2✔
217	}
218
219	public static <S, I> boolean findIncrementalCharacterizingSet(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
220	Collection<? extends I> inputs,
221	Collection<? extends Word<I>> oldSuffixes,
222	Collection<? super Word<I>> newSuffixes) {
223
224	boolean refined = false;	2✔
225
226	// We need a list to ensure a stable iteration order
227	List<? extends Word<I>> oldSuffixList = CollectionUtil.randomAccessList(oldSuffixes);	2✔
228
229	Queue<List<S>> blocks = buildInitialBlocks(automaton, oldSuffixList);	2✔
230
231	if (!oldSuffixes.contains(Word.epsilon()) && epsilonRefine(automaton, blocks)) {	2✔
232	newSuffixes.add(Word.epsilon());	2✔
233	refined = true;	2✔
234	}
235
236	Word<I> suffix;
237
238	while ((suffix = refine(automaton, inputs, blocks)) != null) {	2✔
239	newSuffixes.add(suffix);	2✔
240	refined = true;	2✔
241	}
242
243	return refined;	2✔
244	}
245
246	public static <I> Iterator<Word<I>> incrementalCharacterizingSetIterator(UniversalDeterministicAutomaton<?, I, ?, ?, ?> automaton,
247	Collection<? extends I> inputs,
248	Collection<? extends Word<I>> oldSuffixes) {
249	return new IncrementalCharacterizingSetIterator<>(automaton, inputs, oldSuffixes);	2✔
250	}
251
252	private static <S, I> Queue<List<S>> buildInitialBlocks(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
253	List<? extends Word<I>> oldSuffixes) {
254	Map<List<List<?>>, List<S>> initialPartitioning = new HashMap<>();	2✔
255	Queue<List<S>> blocks = new ArrayDeque<>();	2✔
256	for (S state : automaton) {	2✔
257	List<List<?>> sig = buildSignature(automaton, oldSuffixes, state);	2✔
258	List<S> block = initialPartitioning.get(sig);	2✔
259	if (block == null) {	2✔
260	block = new ArrayList<>();	2✔
261	blocks.add(block);	2✔
262	initialPartitioning.put(sig, block);	2✔
263	}
264	block.add(state);	2✔
265	}	2✔
266
267	return blocks;	2✔
268	}
269
270	private static <S, I> List<List<?>> buildSignature(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
271	List<? extends Word<I>> suffixes,
272	S state) {
273	List<List<?>> signature = new ArrayList<>(suffixes.size());	2✔
274
275	for (Word<I> suffix : suffixes) {	2✔
276	List<?> trace = buildTrace(automaton, state, suffix);	2✔
277	signature.add(trace);	2✔
278	}	2✔
279
280	return signature;	2✔
281	}
282
283	private static <S, I> boolean epsilonRefine(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
284	Queue<List<S>> blockQueue) {
285
286	int initialSize = blockQueue.size();	2✔
287
288	boolean refined = false;	2✔
289
290	for (int i = 0; i < initialSize; i++) {	2✔
291	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
292	@NonNull List<S> block = blockQueue.poll();	2✔
293	if (block.size() <= 1) {	2✔
294	continue;	2✔
295	}
296	Map<?, List<S>> propCluster = clusterByProperty(automaton, block);	2✔
297	if (propCluster.size() > 1) {	2✔
298	refined = true;	2✔
299	}
300	blockQueue.addAll(propCluster.values());	2✔
301	}
302
303	return refined;	2✔
304	}
305
306	private static <S, I> @Nullable Word<I> refine(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
307	Collection<? extends I> inputs,
308	Queue<List<S>> blockQueue) {
309
310	List<S> currBlock;
311	while ((currBlock = blockQueue.poll()) != null) {	2✔
312	if (currBlock.size() <= 1) {	2✔
313	continue; // we cannot split further	2✔
314	}
315
316	Iterator<S> it = currBlock.iterator();	2✔
317
318	S ref = it.next();	2✔
319
320	Word<I> suffix = null;	2✔
321	S state = null;	2✔
322	while (it.hasNext() && suffix == null) {	2✔
323	state = it.next();	2✔
324	suffix = Automata.findSeparatingWord(automaton, ref, state, inputs);	2✔
325	}
326
327	if (state != null && suffix != null) {	2✔
328	int otherBlocks = blockQueue.size();	2✔
329
330	Map<List<?>, List<S>> buckets = new HashMap<>();	2✔
331
332	List<S> firstBucket = new ArrayList<>();	2✔
333	List<S> secondBucket = new ArrayList<>();	2✔
334	firstBucket.add(ref);	2✔
335	buckets.put(buildTrace(automaton, ref, suffix), firstBucket);	2✔
336	secondBucket.add(state);	2✔
337	buckets.put(buildTrace(automaton, state, suffix), secondBucket);	2✔
338
339	cluster(automaton, suffix, it, buckets);	2✔
340
341	blockQueue.addAll(buckets.values());	2✔
342
343	// Split all other blocks that were in the queue
344	for (int i = 0; i < otherBlocks; i++) {	2✔
345	@SuppressWarnings("nullness") // we know that there are at least 'otherBlocks' items in the queue
346	@NonNull List<S> otherBlock = blockQueue.poll();	2✔
347	if (otherBlock.size() > 1) {	2✔
348	buckets.clear();	2✔
349	cluster(automaton, suffix, otherBlock.iterator(), buckets);	2✔
350	blockQueue.addAll(buckets.values());	2✔
351	}
352	}
353
354	return suffix;	2✔
355	}
356	}	×
357	return null;	2✔
358	}
359
360	private static <S, I, SP> Map<?, List<S>> clusterByProperty(UniversalDeterministicAutomaton<S, I, ?, SP, ?> automaton,
361	List<S> states) {
362	Map<SP, List<S>> result = new HashMap<>();	2✔
363
364	for (S state : states) {	2✔
365	SP prop = automaton.getStateProperty(state);	2✔
366	List<S> block = result.computeIfAbsent(prop, k -> new ArrayList<>());	2✔
367	block.add(state);	2✔
368	}	2✔
369
370	return result;	2✔
371	}
372
373	private static <S, I> void cluster(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
374	Word<I> suffix,
375	Iterator<S> stateIt,
376	Map<List<?>, List<S>> bucketMap) {
377
378	while (stateIt.hasNext()) {	2✔
379	S state = stateIt.next();	2✔
380	List<?> trace = buildTrace(automaton, state, suffix);	2✔
381	List<S> bucket = bucketMap.computeIfAbsent(trace, k -> new ArrayList<>());	2✔
382	bucket.add(state);	2✔
383	}	2✔
384	}	2✔
385
386	private static class IncrementalCharacterizingSetIterator<S, I> extends AbstractSimplifiedIterator<Word<I>> {
387
388	private final UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton;
389	private final Collection<? extends I> inputs;
390	private final List<? extends Word<I>> oldSuffixes;
391	private Queue<List<S>> blocks;
392
393	IncrementalCharacterizingSetIterator(UniversalDeterministicAutomaton<S, I, ?, ?, ?> automaton,
394	Collection<? extends I> inputs,
395	Collection<? extends Word<I>> oldSuffixes) {	2✔
396	this.automaton = automaton;	2✔
397	this.inputs = inputs;	2✔
398	this.oldSuffixes = CollectionUtil.randomAccessList(oldSuffixes);	2✔
399	}	2✔
400
401	@Override
402	protected boolean calculateNext() {
403	// first call
404	if (blocks == null) {	2✔
405	blocks = buildInitialBlocks(automaton, oldSuffixes);	2✔
406	if (!oldSuffixes.contains(Word.epsilon()) && epsilonRefine(automaton, blocks)) {	2✔
407	super.nextValue = Word.epsilon();	2✔
408	return true;	2✔
409	}
410	}
411
412	final Word<I> suffix = refine(automaton, inputs, blocks);	2✔
413
414	if (suffix != null) {	2✔
415	super.nextValue = suffix;	2✔
416	return true;	2✔
417	}
418	return false;	2✔
419	}
420	}
421	}

LearnLib / automatalib / 13138848026

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