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

96.77

/util/src/main/java/net/automatalib/util/automaton/ads/BacktrackingSearch.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.ads;

import java.util.BitSet;
import java.util.Collections;
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.function.BiFunction;
import java.util.function.Function;
import java.util.stream.Collectors;

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.graph.ads.ADSNode;
import net.automatalib.graph.ads.impl.ADSLeafNode;
import net.automatalib.graph.ads.impl.ADSSymbolNode;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.NonNull;

/**
 * A class containing methods for computing adaptive distinguishing sequences (for arbitrary sets of states) by means of
 * a backtracking approach.
 */
public final class BacktrackingSearch {

    private BacktrackingSearch() {}

    /**
     * Computes an ADS by constructing (growing) splitting words for the current set of states and recursively computing
     * sub-ADSs for the induced partitions. May yield non-optimal ADSs.
     *
     * @param automaton
     *         The automaton for which an ADS should be computed
     * @param input
     *         the input alphabet of the automaton
     * @param states
     *         the set of states which should be distinguished by the computed ADS
     * @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<ADSNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
                                                               Alphabet<I> input,
                                                               Set<S> states) {

        if (states.size() == 1) {
            return ADS.compute(automaton, input, states);
        }

        final SplitTree<S, I, O> node = new SplitTree<>(states, new ReflexiveMapView<>(states));

        return compute(automaton, input, node);
    }

    /**
     * See {@link #compute(MealyMachine, Alphabet, Set)}. Internal version, that uses the {@link SplitTree}
     * representation.
     */
    static <S, I, O> Optional<ADSNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
                                                        Alphabet<I> input,
                                                        SplitTree<S, I, O> node) {
        return compute(automaton, input, node, node.getPartition().size());
    }

    private static <S, I, T, O> Optional<ADSNode<S, I, O>> compute(MealyMachine<S, I, T, O> automaton,
                                                                   Alphabet<I> input,
                                                                   SplitTree<S, I, O> node,
                                                                   int originalPartitionSize) {

        final long maximumSplittingWordLength = ADSUtil.computeMaximumSplittingWordLength(automaton.size(),
                                                                                          node.getPartition().size(),
                                                                                          originalPartitionSize);
        final Queue<Word<I>> splittingWordCandidates = new LinkedList<>();
        final StateIDs<S> stateIds = automaton.stateIDs();
        final Set<BitSet> cache = new HashSet<>();

        splittingWordCandidates.add(Word.epsilon());

        candidateLoop:
        while (!splittingWordCandidates.isEmpty()) {

            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            final @NonNull Word<I> prefix = splittingWordCandidates.poll();
            @SuppressWarnings("nullness") // the initial prefix (epsilon) guarantees non-nullness.
            final Map<S, S> currentToInitialMapping = node.getPartition()
                                                          .stream()
                                                          .collect(Collectors.toMap(x -> automaton.getSuccessor(x,
                                                                                                                prefix),
                                                                                    Function.identity()));
            final BitSet currentSetAsBitSet = new BitSet();
            for (S s : currentToInitialMapping.keySet()) {
                currentSetAsBitSet.set(stateIds.getStateId(s));
            }

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

            oneSymbolFuture:
            for (I i : input) {
                // compute successors
                final Map<O, SplitTree<S, I, O>> successors = new HashMap<>();

                for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {
                    final S current = entry.getKey();
                    final T trans = automaton.getTransition(current, i);

                    if (trans == null) {
                        throw new IllegalArgumentException("Partial automata are not supported");
                    }

                    final S nextState = automaton.getSuccessor(trans);
                    final O nextOutput = automaton.getTransitionOutput(trans);

                    final SplitTree<S, I, O> child;
                    if (successors.containsKey(nextOutput)) {
                        child = successors.get(nextOutput);
                    } else {
                        child = new SplitTree<>(new HashSet<>());
                        successors.put(nextOutput, child);
                    }

                    // invalid input
                    if (!child.getPartition().add(nextState)) {
                        continue oneSymbolFuture;
                    }
                    child.getMapping().put(nextState, node.getMapping().get(entry.getValue()));
                }

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

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

                        final SplitTree<S, I, O> currentNode = entry.getValue();

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

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

                        final Optional<ADSNode<S, I, O>> succ;
                        if (currentNode.getPartition().size() > 2) {
                            succ = BacktrackingSearch.compute(automaton, input, currentNode, originalPartitionSize);
                        } else {
                            succ = ADS.compute(automaton, input, currentNode);
                        }

                        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<ADSNode<S, I, O>, ADSNode<S, I, O>> ads =
                            ADSUtil.buildFromTrace(automaton, prefix.append(i), node.getPartition().iterator().next());
                    final ADSNode<S, I, O> head = ads.getFirst();
                    final ADSNode<S, I, O> tail = ads.getSecond();

                    for (Map.Entry<O, ADSNode<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();
    }

    /**
     * Computes an ADS by iterating over the successor tree in a breadth-first manner, yielding an optimal (dependent on
     * the passed optimization function) ADS.
     *
     * @param automaton
     *         The automaton for which an ADS should be computed
     * @param input
     *         the input alphabet of the automaton
     * @param states
     *         the set of states which should be distinguished by the computed ADS
     * @param costAggregator
     *         the optimization function by which solutions should be pruned
     * @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<ADSNode<S, I, O>> computeOptimal(MealyMachine<S, I, ?, O> automaton,
                                                                      Alphabet<I> input,
                                                                      Set<S> states,
                                                                      CostAggregator costAggregator) {

        if (states.size() == 1) {
            return ADS.compute(automaton, input, states);
        }

        final Optional<SearchState<S, I, O>> searchState = exploreSearchSpace(automaton,
                                                                              input,
                                                                              states,
                                                                              costAggregator,
                                                                              new HashMap<>(),
                                                                              new HashSet<>(),
                                                                              Integer.MAX_VALUE);

        return searchState.map(s -> constructADS(automaton, new ReflexiveMapView<>(states), s));
    }

    private static <S, I, T, O> Optional<SearchState<S, I, O>> exploreSearchSpace(MealyMachine<S, I, T, O> automaton,
                                                                                  Alphabet<I> alphabet,
                                                                                  Set<S> targets,
                                                                                  CostAggregator costAggregator,
                                                                                  Map<Set<S>, Optional<SearchState<S, I, O>>> stateCache,
                                                                                  Set<Set<S>> currentTraceCache,
                                                                                  int costsBound) {

        final Optional<SearchState<S, I, O>> cachedValue = stateCache.get(targets);

        if (cachedValue != null) {
            return cachedValue;
        }

        if (currentTraceCache.contains(targets)) {
            return Optional.empty();
        }

        if (targets.size() == 1) {
            final SearchState<S, I, O> resultSS = new SearchState<>();
            final Optional<SearchState<S, I, O>> result = Optional.of(resultSS);
            stateCache.put(targets, result);
            return result;
        }

        // any further expansion would lead to a worse result, hence stop here.
        if (costsBound == 0) {
            return Optional.empty();
        }

        boolean foundValidSuccessor = false;
        boolean convergingStates = true;
        int bestCosts = costsBound;
        Map<O, SearchState<S, I, O>> bestSuccessor = null;
        I bestInputSymbol = null;

        alphabetLoop:
        for (I i : alphabet) {

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

            for (S s : targets) {
                final T trans = automaton.getTransition(s, i);

                if (trans == null) {
                    throw new IllegalArgumentException("Partial automata are not supported");
                }

                final S nextState = automaton.getSuccessor(trans);
                final O nextOutput = automaton.getTransitionOutput(trans);

                final Set<S> child;
                if (successors.containsKey(nextOutput)) {
                    child = successors.get(nextOutput);
                } else {
                    child = new HashSet<>();
                    successors.put(nextOutput, child);
                }

                // invalid input
                if (!child.add(nextState)) {
                    continue alphabetLoop;
                }
            }

            convergingStates = false;

            final int costsForInputSymbol;
            final Map<O, SearchState<S, I, O>> successorsForInputSymbol;

            if (successors.size() > 1) {

                successorsForInputSymbol = new HashMap<>(HashUtil.capacity(successors.size()));
                int partitionCosts = 0;

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

                    final Optional<SearchState<S, I, O>> potentialResult = exploreSearchSpace(automaton,
                                                                                              alphabet,
                                                                                              entry.getValue(),
                                                                                              costAggregator,
                                                                                              stateCache,
                                                                                              new HashSet<>(),
                                                                                              bestCosts);

                    if (!potentialResult.isPresent()) {
                        continue alphabetLoop;
                    }

                    final SearchState<S, I, O> subResult = potentialResult.get();
                    successorsForInputSymbol.put(entry.getKey(), subResult);

                    partitionCosts = costAggregator.apply(partitionCosts, subResult.costs);

                    if (partitionCosts >= bestCosts) {
                        continue alphabetLoop;
                    }
                }

                costsForInputSymbol = partitionCosts;
            } else {
                final Map.Entry<O, Set<S>> entry = successors.entrySet().iterator().next();
                final Set<S> nextTargets = entry.getValue();

                final Set<Set<S>> nextTraceCache = new HashSet<>(currentTraceCache);
                nextTraceCache.add(targets);

                final Optional<SearchState<S, I, O>> potentialResult = exploreSearchSpace(automaton,
                                                                                          alphabet,
                                                                                          nextTargets,
                                                                                          costAggregator,
                                                                                          stateCache,
                                                                                          nextTraceCache,
                                                                                          bestCosts);

                if (!potentialResult.isPresent()) {
                    continue alphabetLoop;
                }

                final SearchState<S, I, O> subResult = potentialResult.get();

                costsForInputSymbol = subResult.costs;
                successorsForInputSymbol = Collections.singletonMap(entry.getKey(), subResult);
            }

            // update result
            if (costsForInputSymbol < bestCosts) {
                foundValidSuccessor = true;
                bestCosts = costsForInputSymbol;
                bestSuccessor = successorsForInputSymbol;
                bestInputSymbol = i;
            }
        }

        if (convergingStates) {
            stateCache.put(targets, Optional.empty());
            return Optional.empty();
        }

        if (!foundValidSuccessor) {
            return Optional.empty();
        }

        final SearchState<S, I, O> resultSS = new SearchState<>();
        resultSS.costs = bestCosts + 1;
        resultSS.successors = bestSuccessor;
        resultSS.symbol = bestInputSymbol;

        final Optional<SearchState<S, I, O>> result = Optional.of(resultSS);
        stateCache.put(targets, result);
        return result;
    }

    private static <S, I, T, O> ADSNode<S, I, O> constructADS(MealyMachine<S, I, T, O> automaton,
                                                              Map<S, S> currentToInitialMapping,
                                                              SearchState<S, I, O> searchState) {

        if (currentToInitialMapping.size() == 1) {
            return new ADSLeafNode<>(null, currentToInitialMapping.values().iterator().next());
        }

        final I i = searchState.symbol;
        final Map<O, Map<S, S>> successors = new HashMap<>();

        for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {
            final S current = entry.getKey();
            final T trans = automaton.getTransition(current, i);
            assert trans != null;
            final S nextState = automaton.getSuccessor(trans);
            final O nextOutput = automaton.getTransitionOutput(trans);

            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) {
                throw new IllegalStateException();
            }
        }

        final ADSNode<S, I, O> result = new ADSSymbolNode<>(null, i);

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

            final O output = entry.getKey();
            final Map<S, S> nextMapping = entry.getValue();

            final ADSNode<S, I, O> successor = constructADS(automaton, nextMapping, searchState.successors.get(output));

            result.getChildren().put(output, successor);
            successor.setParent(result);
        }

        return result;
    }

    /**
     * Utility enum, that allows to specify the optimization criterion when performing and optimal ADS search. See
     * {@link BacktrackingSearch#computeOptimal(MealyMachine, Alphabet, Set, CostAggregator)}.
     */
    public enum CostAggregator implements BiFunction<Integer, Integer, Integer> {
        MIN_LENGTH() {
            @Override
            public Integer apply(Integer oldValue, Integer newValue) {
                return Math.max(oldValue, newValue);
            }
        },

        MIN_SIZE() {
            @Override
            public Integer apply(Integer oldValue, Integer newValue) {
                return oldValue + newValue;
            }
        }
    }

    /**
     * Internal utility class that encapsulates information of a node in a successor tree.
     *
     * @param <S>
     *         (hypothesis) state type
     * @param <I>
     *         input alphabet type
     * @param <O>
     *         output alphabet type
     */
    private static final class SearchState<S, I, O> {

        private I symbol;

        private Map<O, SearchState<S, I, O>> successors;

        private int costs;
    }
}

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.ads;
17
18	import java.util.BitSet;
19	import java.util.Collections;
20	import java.util.HashMap;
21	import java.util.HashSet;
22	import java.util.LinkedList;
23	import java.util.Map;
24	import java.util.Optional;
25	import java.util.Queue;
26	import java.util.Set;
27	import java.util.function.BiFunction;
28	import java.util.function.Function;
29	import java.util.stream.Collectors;
30
31	import net.automatalib.alphabet.Alphabet;
32	import net.automatalib.automaton.concept.StateIDs;
33	import net.automatalib.automaton.transducer.MealyMachine;
34	import net.automatalib.common.smartcollection.ReflexiveMapView;
35	import net.automatalib.common.util.HashUtil;
36	import net.automatalib.common.util.Pair;
37	import net.automatalib.graph.ads.ADSNode;
38	import net.automatalib.graph.ads.impl.ADSLeafNode;
39	import net.automatalib.graph.ads.impl.ADSSymbolNode;
40	import net.automatalib.word.Word;
41	import org.checkerframework.checker.nullness.qual.NonNull;
42
43	/**
44	* A class containing methods for computing adaptive distinguishing sequences (for arbitrary sets of states) by means of
45	* a backtracking approach.
46	*/
47	public final class BacktrackingSearch {	2✔
48
49	private BacktrackingSearch() {}
50
51	/**
52	* Computes an ADS by constructing (growing) splitting words for the current set of states and recursively computing
53	* sub-ADSs for the induced partitions. May yield non-optimal ADSs.
54	*
55	* @param automaton
56	* The automaton for which an ADS should be computed
57	* @param input
58	* the input alphabet of the automaton
59	* @param states
60	* the set of states which should be distinguished by the computed ADS
61	* @param <S>
62	* (hypothesis) state type
63	* @param <I>
64	* input alphabet type
65	* @param <O>
66	* output alphabet type
67	*
68	* @return {@code Optional.empty()} if there exists no ADS that distinguishes the given states, a valid ADS
69	* otherwise.
70	*/
71	public static <S, I, O> Optional<ADSNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
72	Alphabet<I> input,
73	Set<S> states) {
74
75	if (states.size() == 1) {	2✔
76	return ADS.compute(automaton, input, states);	2✔
77	}
78
79	final SplitTree<S, I, O> node = new SplitTree<>(states, new ReflexiveMapView<>(states));	2✔
80
81	return compute(automaton, input, node);	2✔
82	}
83
84	/**
85	* See {@link #compute(MealyMachine, Alphabet, Set)}. Internal version, that uses the {@link SplitTree}
86	* representation.
87	*/
88	static <S, I, O> Optional<ADSNode<S, I, O>> compute(MealyMachine<S, I, ?, O> automaton,
89	Alphabet<I> input,
90	SplitTree<S, I, O> node) {
91	return compute(automaton, input, node, node.getPartition().size());	2✔
92	}
93
94	private static <S, I, T, O> Optional<ADSNode<S, I, O>> compute(MealyMachine<S, I, T, O> automaton,
95	Alphabet<I> input,
96	SplitTree<S, I, O> node,
97	int originalPartitionSize) {
98
99	final long maximumSplittingWordLength = ADSUtil.computeMaximumSplittingWordLength(automaton.size(),	2✔
100	node.getPartition().size(),	2✔
101	originalPartitionSize);
102	final Queue<Word<I>> splittingWordCandidates = new LinkedList<>();	2✔
103	final StateIDs<S> stateIds = automaton.stateIDs();	2✔
104	final Set<BitSet> cache = new HashSet<>();	2✔
105
106	splittingWordCandidates.add(Word.epsilon());	2✔
107
108	candidateLoop:
109	while (!splittingWordCandidates.isEmpty()) {	2✔
110
111	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
112	final @NonNull Word<I> prefix = splittingWordCandidates.poll();	2✔
113	@SuppressWarnings("nullness") // the initial prefix (epsilon) guarantees non-nullness.
114	final Map<S, S> currentToInitialMapping = node.getPartition()	2✔
115	.stream()	2✔
116	.collect(Collectors.toMap(x -> automaton.getSuccessor(x,	2✔
117	prefix),
118	Function.identity()));	2✔
119	final BitSet currentSetAsBitSet = new BitSet();	2✔
120	for (S s : currentToInitialMapping.keySet()) {	2✔
121	currentSetAsBitSet.set(stateIds.getStateId(s));	2✔
122	}	2✔
123
124	if (cache.contains(currentSetAsBitSet)) {	2✔
125	continue candidateLoop;	2✔
126	}
127
128	oneSymbolFuture:
129	for (I i : input) {	2✔
130	// compute successors
131	final Map<O, SplitTree<S, I, O>> successors = new HashMap<>();	2✔
132
133	for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {	2✔
134	final S current = entry.getKey();	2✔
135	final T trans = automaton.getTransition(current, i);	2✔
136
137	if (trans == null) {	2✔
138	throw new IllegalArgumentException("Partial automata are not supported");	×
139	}
140
141	final S nextState = automaton.getSuccessor(trans);	2✔
142	final O nextOutput = automaton.getTransitionOutput(trans);	2✔
143
144	final SplitTree<S, I, O> child;
145	if (successors.containsKey(nextOutput)) {	2✔
146	child = successors.get(nextOutput);	2✔
147	} else {
148	child = new SplitTree<>(new HashSet<>());	2✔
149	successors.put(nextOutput, child);	2✔
150	}
151
152	// invalid input
153	if (!child.getPartition().add(nextState)) {	2✔
154	continue oneSymbolFuture;	2✔
155	}
156	child.getMapping().put(nextState, node.getMapping().get(entry.getValue()));	2✔
157	}	2✔
158
159	//splitting word
160	if (successors.size() > 1) {	2✔
161	final Map<O, ADSNode<S, I, O>> results = new HashMap<>();	2✔
162
163	for (Map.Entry<O, SplitTree<S, I, O>> entry : successors.entrySet()) {	2✔
164
165	final SplitTree<S, I, O> currentNode = entry.getValue();	2✔
166
167	final BitSet currentNodeAsBitSet = new BitSet();	2✔
168	for (S s : currentNode.getPartition()) {	2✔
169	currentNodeAsBitSet.set(stateIds.getStateId(s));	2✔
170	}	2✔
171
172	if (cache.contains(currentNodeAsBitSet)) {	2✔
173	continue oneSymbolFuture;	×
174	}
175
176	final Optional<ADSNode<S, I, O>> succ;
177	if (currentNode.getPartition().size() > 2) {	2✔
178	succ = BacktrackingSearch.compute(automaton, input, currentNode, originalPartitionSize);	2✔
179	} else {
180	succ = ADS.compute(automaton, input, currentNode);	2✔
181	}
182
183	if (!succ.isPresent()) {	2✔
184	cache.add(currentNodeAsBitSet);	×
185	continue oneSymbolFuture;	×
186	}
187
188	results.put(entry.getKey(), succ.get());	2✔
189	}	2✔
190
191	// create ADS (if we haven't continued until here)
192	final Pair<ADSNode<S, I, O>, ADSNode<S, I, O>> ads =	2✔
193	ADSUtil.buildFromTrace(automaton, prefix.append(i), node.getPartition().iterator().next());	2✔
194	final ADSNode<S, I, O> head = ads.getFirst();	2✔
195	final ADSNode<S, I, O> tail = ads.getSecond();	2✔
196
197	for (Map.Entry<O, ADSNode<S, I, O>> entry : results.entrySet()) {	2✔
198	entry.getValue().setParent(tail);	2✔
199	tail.getChildren().put(entry.getKey(), entry.getValue());	2✔
200	}	2✔
201
202	return Optional.of(head);	2✔
203	} else if (prefix.length() < maximumSplittingWordLength) { // no splitting word	2✔
204	splittingWordCandidates.add(prefix.append(i));	2✔
205	}
206	}	2✔
207
208	cache.add(currentSetAsBitSet);	2✔
209	}	2✔
210
211	return Optional.empty();	2✔
212	}
213
214	/**
215	* Computes an ADS by iterating over the successor tree in a breadth-first manner, yielding an optimal (dependent on
216	* the passed optimization function) ADS.
217	*
218	* @param automaton
219	* The automaton for which an ADS should be computed
220	* @param input
221	* the input alphabet of the automaton
222	* @param states
223	* the set of states which should be distinguished by the computed ADS
224	* @param costAggregator
225	* the optimization function by which solutions should be pruned
226	* @param <S>
227	* (hypothesis) state type
228	* @param <I>
229	* input alphabet type
230	* @param <O>
231	* output alphabet type
232	*
233	* @return {@code Optional.empty()} if there exists no ADS that distinguishes the given states, a valid ADS
234	* otherwise.
235	*/
236	public static <S, I, O> Optional<ADSNode<S, I, O>> computeOptimal(MealyMachine<S, I, ?, O> automaton,
237	Alphabet<I> input,
238	Set<S> states,
239	CostAggregator costAggregator) {
240
241	if (states.size() == 1) {	2✔
242	return ADS.compute(automaton, input, states);	2✔
243	}
244
245	final Optional<SearchState<S, I, O>> searchState = exploreSearchSpace(automaton,	2✔
246	input,
247	states,
248	costAggregator,
249	new HashMap<>(),
250	new HashSet<>(),
251	Integer.MAX_VALUE);
252
253	return searchState.map(s -> constructADS(automaton, new ReflexiveMapView<>(states), s));	2✔
254	}
255
256	private static <S, I, T, O> Optional<SearchState<S, I, O>> exploreSearchSpace(MealyMachine<S, I, T, O> automaton,
257	Alphabet<I> alphabet,
258	Set<S> targets,
259	CostAggregator costAggregator,
260	Map<Set<S>, Optional<SearchState<S, I, O>>> stateCache,
261	Set<Set<S>> currentTraceCache,
262	int costsBound) {
263
264	final Optional<SearchState<S, I, O>> cachedValue = stateCache.get(targets);	2✔
265
266	if (cachedValue != null) {	2✔
267	return cachedValue;	2✔
268	}
269
270	if (currentTraceCache.contains(targets)) {	2✔
271	return Optional.empty();	2✔
272	}
273
274	if (targets.size() == 1) {	2✔
275	final SearchState<S, I, O> resultSS = new SearchState<>();	2✔
276	final Optional<SearchState<S, I, O>> result = Optional.of(resultSS);	2✔
277	stateCache.put(targets, result);	2✔
278	return result;	2✔
279	}
280
281	// any further expansion would lead to a worse result, hence stop here.
282	if (costsBound == 0) {	2✔
283	return Optional.empty();	2✔
284	}
285
286	boolean foundValidSuccessor = false;	2✔
287	boolean convergingStates = true;	2✔
288	int bestCosts = costsBound;	2✔
289	Map<O, SearchState<S, I, O>> bestSuccessor = null;	2✔
290	I bestInputSymbol = null;	2✔
291
292	alphabetLoop:
293	for (I i : alphabet) {	2✔
294
295	// compute successors
296	final Map<O, Set<S>> successors = new HashMap<>();	2✔
297
298	for (S s : targets) {	2✔
299	final T trans = automaton.getTransition(s, i);	2✔
300
301	if (trans == null) {	2✔
302	throw new IllegalArgumentException("Partial automata are not supported");	×
303	}
304
305	final S nextState = automaton.getSuccessor(trans);	2✔
306	final O nextOutput = automaton.getTransitionOutput(trans);	2✔
307
308	final Set<S> child;
309	if (successors.containsKey(nextOutput)) {	2✔
310	child = successors.get(nextOutput);	2✔
311	} else {
312	child = new HashSet<>();	2✔
313	successors.put(nextOutput, child);	2✔
314	}
315
316	// invalid input
317	if (!child.add(nextState)) {	2✔
318	continue alphabetLoop;	2✔
319	}
320	}	2✔
321
322	convergingStates = false;	2✔
323
324	final int costsForInputSymbol;
325	final Map<O, SearchState<S, I, O>> successorsForInputSymbol;
326
327	if (successors.size() > 1) {	2✔
328
329	successorsForInputSymbol = new HashMap<>(HashUtil.capacity(successors.size()));	2✔
330	int partitionCosts = 0;	2✔
331
332	for (Map.Entry<O, Set<S>> entry : successors.entrySet()) {	2✔
333
334	final Optional<SearchState<S, I, O>> potentialResult = exploreSearchSpace(automaton,	2✔
335	alphabet,
336	entry.getValue(),	2✔
337	costAggregator,
338	stateCache,
339	new HashSet<>(),
340	bestCosts);
341
342	if (!potentialResult.isPresent()) {	2✔
343	continue alphabetLoop;	2✔
344	}
345
346	final SearchState<S, I, O> subResult = potentialResult.get();	2✔
347	successorsForInputSymbol.put(entry.getKey(), subResult);	2✔
348
349	partitionCosts = costAggregator.apply(partitionCosts, subResult.costs);	2✔
350
351	if (partitionCosts >= bestCosts) {	2✔
352	continue alphabetLoop;	2✔
353	}
354	}	2✔
355
356	costsForInputSymbol = partitionCosts;	2✔
357	} else {	2✔
358	final Map.Entry<O, Set<S>> entry = successors.entrySet().iterator().next();	2✔
359	final Set<S> nextTargets = entry.getValue();	2✔
360
361	final Set<Set<S>> nextTraceCache = new HashSet<>(currentTraceCache);	2✔
362	nextTraceCache.add(targets);	2✔
363
364	final Optional<SearchState<S, I, O>> potentialResult = exploreSearchSpace(automaton,	2✔
365	alphabet,
366	nextTargets,
367	costAggregator,
368	stateCache,
369	nextTraceCache,
370	bestCosts);
371
372	if (!potentialResult.isPresent()) {	2✔
373	continue alphabetLoop;	2✔
374	}
375
376	final SearchState<S, I, O> subResult = potentialResult.get();	2✔
377
378	costsForInputSymbol = subResult.costs;	2✔
379	successorsForInputSymbol = Collections.singletonMap(entry.getKey(), subResult);	2✔
380	}
381
382	// update result
383	if (costsForInputSymbol < bestCosts) {	2✔
384	foundValidSuccessor = true;	2✔
385	bestCosts = costsForInputSymbol;	2✔
386	bestSuccessor = successorsForInputSymbol;	2✔
387	bestInputSymbol = i;	2✔
388	}
389	}	2✔
390
391	if (convergingStates) {	2✔
392	stateCache.put(targets, Optional.empty());	2✔
393	return Optional.empty();	2✔
394	}
395
396	if (!foundValidSuccessor) {	2✔
397	return Optional.empty();	2✔
398	}
399
400	final SearchState<S, I, O> resultSS = new SearchState<>();	2✔
401	resultSS.costs = bestCosts + 1;	2✔
402	resultSS.successors = bestSuccessor;	2✔
403	resultSS.symbol = bestInputSymbol;	2✔
404
405	final Optional<SearchState<S, I, O>> result = Optional.of(resultSS);	2✔
406	stateCache.put(targets, result);	2✔
407	return result;	2✔
408	}
409
410	private static <S, I, T, O> ADSNode<S, I, O> constructADS(MealyMachine<S, I, T, O> automaton,
411	Map<S, S> currentToInitialMapping,
412	SearchState<S, I, O> searchState) {
413
414	if (currentToInitialMapping.size() == 1) {	2✔
415	return new ADSLeafNode<>(null, currentToInitialMapping.values().iterator().next());	2✔
416	}
417
418	final I i = searchState.symbol;	2✔
419	final Map<O, Map<S, S>> successors = new HashMap<>();	2✔
420
421	for (Map.Entry<S, S> entry : currentToInitialMapping.entrySet()) {	2✔
422	final S current = entry.getKey();	2✔
423	final T trans = automaton.getTransition(current, i);	2✔
424	assert trans != null;	2✔
425	final S nextState = automaton.getSuccessor(trans);	2✔
426	final O nextOutput = automaton.getTransitionOutput(trans);	2✔
427
428	final Map<S, S> nextMapping;
429	if (successors.containsKey(nextOutput)) {	2✔
430	nextMapping = successors.get(nextOutput);	2✔
431	} else {
432	nextMapping = new HashMap<>();	2✔
433	successors.put(nextOutput, nextMapping);	2✔
434	}
435
436	// invalid input
437	if (nextMapping.put(nextState, entry.getValue()) != null) {	2✔
438	throw new IllegalStateException();	×
439	}
440	}	2✔
441
442	final ADSNode<S, I, O> result = new ADSSymbolNode<>(null, i);	2✔
443
444	for (Map.Entry<O, Map<S, S>> entry : successors.entrySet()) {	2✔
445
446	final O output = entry.getKey();	2✔
447	final Map<S, S> nextMapping = entry.getValue();	2✔
448
449	final ADSNode<S, I, O> successor = constructADS(automaton, nextMapping, searchState.successors.get(output));	2✔
450
451	result.getChildren().put(output, successor);	2✔
452	successor.setParent(result);	2✔
453	}	2✔
454
455	return result;	2✔
456	}
457
458	/**
459	* Utility enum, that allows to specify the optimization criterion when performing and optimal ADS search. See
460	* {@link BacktrackingSearch#computeOptimal(MealyMachine, Alphabet, Set, CostAggregator)}.
461	*/
462	public enum CostAggregator implements BiFunction<Integer, Integer, Integer> {	2✔
463	MIN_LENGTH() {	2✔
464	@Override
465	public Integer apply(Integer oldValue, Integer newValue) {
466	return Math.max(oldValue, newValue);	2✔
467	}
468	},
469
470	MIN_SIZE() {	2✔
471	@Override
472	public Integer apply(Integer oldValue, Integer newValue) {
473	return oldValue + newValue;	2✔
474	}
475	}
476	}
477
478	/**
479	* Internal utility class that encapsulates information of a node in a successor tree.
480	*
481	* @param <S>
482	* (hypothesis) state type
483	* @param <I>
484	* input alphabet type
485	* @param <O>
486	* output alphabet type
487	*/
488	private static final class SearchState<S, I, O> {
489
490	private I symbol;
491
492	private Map<O, SearchState<S, I, O>> successors;
493
494	private int costs;
495	}
496	}

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