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

99.09

/util/src/main/java/net/automatalib/util/automaton/ads/LeeYannakakis.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.Collections;
import java.util.EnumMap;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;

import net.automatalib.alphabet.Alphabet;
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.base.CompactEdge;
import net.automatalib.graph.impl.CompactUniversalGraph;
import net.automatalib.util.graph.Path;
import net.automatalib.util.graph.ShortestPaths;
import net.automatalib.util.graph.traversal.GraphTraversal;
import net.automatalib.word.Word;

/**
 * Algorithm of Lee and Yannakakis for computing adaptive distinguishing sequences (of length at most n^2) in O(n^2)
 * time (where n denotes the number of states of the automaton).
 * <p>
 * See: D. Lee and M. Yannakakis - "Testing Finite-State Machines: State Identification and Verification", IEEE
 * Transactions on Computers 43.3 (1994)
 */
@SuppressWarnings("nullness")
public final class LeeYannakakis {

    private LeeYannakakis() {}

    /**
     * Computes an ADS using the algorithm of Lee and Yannakakis.
     *
     * @param automaton
     *         The automaton for which an ADS should be computed
     * @param input
     *         the input alphabet of the automaton
     * @param <S>
     *         (hypothesis) state type
     * @param <I>
     *         input alphabet type
     * @param <O>
     *         output alphabet type
     *
     * @return A {@link LYResult} containing an adaptive distinguishing sequence (if existent) and a possible set of
     * indistinguishable states.
     */
    public static <S, I, O> LYResult<S, I, O> compute(MealyMachine<S, I, ?, O> automaton, Alphabet<I> input) {

        final SplitTreeResult<S, I, O> str = computeSplitTree(automaton, input);

        if (str.isPresent()) {
            final Set<S> states = new HashSet<>(automaton.getStates());
            return new LYResult<>(extractADS(automaton, str.get(), states, new ReflexiveMapView<>(states), null));
        }

        return new LYResult<>(str.getIndistinguishableStates());
    }

    private static <S, I, O> SplitTreeResult<S, I, O> computeSplitTree(MealyMachine<S, I, ?, O> automaton,
                                                                       Alphabet<I> input) {

        final SplitTree<S, I, O> st = new SplitTree<>(new HashSet<>(automaton.getStates()));
        final Set<SplitTree<S, I, O>> leaves = new HashSet<>(HashUtil.capacity(automaton.size()));
        leaves.add(st);

        while (leaves.stream().anyMatch(LeeYannakakis::needsRefinement)) {

            final int maxCardinality = leaves.stream()
                                             .mapToInt(x -> x.getPartition().size())
                                             .max()
                                             .orElseThrow(IllegalStateException::new);
            final Set<SplitTree<S, I, O>> r =
                    leaves.stream().filter(x -> x.getPartition().size() == maxCardinality).collect(Collectors.toSet());

            final Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> validitySetMap =
                    computeValidities(automaton, input, r, leaves);

            if (!validitySetMap.get(Validity.INVALID).isEmpty()) {
                final Set<Pair<Word<I>, SplitTree<S, I, O>>> set = validitySetMap.get(Validity.INVALID);

                final Set<S> indistinguishableStates = new HashSet<>();

                for (Pair<Word<I>, SplitTree<S, I, O>> pair : set) {
                    indistinguishableStates.addAll(pair.getSecond().getPartition());
                }

                return new SplitTreeResult<>(indistinguishableStates);
            }

            // a-valid partitions
            for (Pair<Word<I>, SplitTree<S, I, O>> aPartition : validitySetMap.get(Validity.A_VALID)) {

                assert aPartition.getFirst().size() == 1 : "a-valid inputs should always contain exactly 1 symbol";

                final I aValidInput = aPartition.getFirst().firstSymbol();
                final SplitTree<S, I, O> nodeToRefine = aPartition.getSecond();
                final Map<O, Set<S>> successorMap = nodeToRefine.getPartition()
                                                                .stream()
                                                                .collect(Collectors.groupingBy(s -> automaton.getOutput(
                                                                        s,
                                                                        aValidInput), Collectors.toSet()));

                nodeToRefine.setSequence(Word.fromSymbols(aValidInput));
                leaves.remove(nodeToRefine);

                for (Map.Entry<O, Set<S>> entry : successorMap.entrySet()) {
                    final SplitTree<S, I, O> child = new SplitTree<>(entry.getValue());
                    nodeToRefine.getSuccessors().put(entry.getKey(), child);
                    leaves.add(child);
                }
                for (S s : nodeToRefine.getPartition()) {
                    nodeToRefine.getMapping().put(s, automaton.getSuccessor(s, aValidInput));
                }
            }

            // b-valid partitions
            for (Pair<Word<I>, SplitTree<S, I, O>> bPartition : validitySetMap.get(Validity.B_VALID)) {

                assert bPartition.getFirst().size() == 1 : "b-valid inputs should always contain exactly 1 symbol";

                final I bValidInput = bPartition.getFirst().firstSymbol();
                final SplitTree<S, I, O> nodeToRefine = bPartition.getSecond();
                final Map<S, S> successorsToNodes = nodeToRefine.getPartition()
                                                                .stream()
                                                                .collect(Collectors.toMap(x -> automaton.getSuccessor(x,
                                                                                                                      bValidInput),
                                                                                          Function.identity()));
                final SplitTree<S, I, O> v =
                        st.findLowestSubsetNode(successorsToNodes.keySet()).orElseThrow(IllegalStateException::new);

                nodeToRefine.setSequence(v.getSequence().prepend(bValidInput));
                leaves.remove(nodeToRefine);

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

                    final Set<S> wSet = entry.getValue().getPartition();
                    final Set<S> intersection = new HashSet<>(successorsToNodes.keySet());
                    intersection.retainAll(wSet);

                    if (!intersection.isEmpty()) {
                        final Set<S> indistinguishableNodes =
                                intersection.stream().map(successorsToNodes::get).collect(Collectors.toSet());
                        final SplitTree<S, I, O> newChild = new SplitTree<>(indistinguishableNodes);
                        nodeToRefine.getSuccessors().put(entry.getKey(), newChild);
                        leaves.add(newChild);
                    }
                }
                for (S s : nodeToRefine.getPartition()) {
                    nodeToRefine.getMapping().put(s, v.getMapping().get(automaton.getSuccessor(s, bValidInput)));
                }
            }

            // c-valid partitions
            for (Pair<Word<I>, SplitTree<S, I, O>> cPartition : validitySetMap.get(Validity.C_VALID)) {
                final Word<I> cValidInput = cPartition.getFirst();
                final SplitTree<S, I, O> nodeToRefine = cPartition.getSecond();
                final Map<S, S> successorsToNodes = nodeToRefine.getPartition()
                                                                .stream()
                                                                .collect(Collectors.toMap(x -> automaton.getSuccessor(x,
                                                                                                                      cValidInput),
                                                                                          Function.identity()));
                final SplitTree<S, I, O> c =
                        st.findLowestSubsetNode(successorsToNodes.keySet()).orElseThrow(IllegalStateException::new);

                nodeToRefine.setSequence(cValidInput.concat(c.getSequence()));
                leaves.remove(nodeToRefine);

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

                    final Set<S> wSet = entry.getValue().getPartition();
                    final Set<S> intersection = new HashSet<>(successorsToNodes.keySet());
                    intersection.retainAll(wSet);

                    if (!intersection.isEmpty()) {
                        final Set<S> indistinguishableNodes =
                                intersection.stream().map(successorsToNodes::get).collect(Collectors.toSet());
                        final SplitTree<S, I, O> newChild = new SplitTree<>(indistinguishableNodes);
                        nodeToRefine.getSuccessors().put(entry.getKey(), newChild);
                        leaves.add(newChild);
                    }
                }
                for (S s : nodeToRefine.getPartition()) {
                    nodeToRefine.getMapping().put(s, c.getMapping().get(automaton.getSuccessor(s, cValidInput)));
                }
            }
        }

        return new SplitTreeResult<>(st);
    }

    private static <S, I, O> ADSNode<S, I, O> extractADS(MealyMachine<S, I, ?, O> automaton,
                                                         SplitTree<S, I, O> st,
                                                         Set<S> currentSet,
                                                         Map<S, S> currentToInitialMapping,
                                                         ADSNode<S, I, O> predecessor) {

        if (currentSet.size() == 1) {
            final S currentNode = currentSet.iterator().next();

            assert currentToInitialMapping.containsKey(currentNode);

            return new ADSLeafNode<>(predecessor, currentToInitialMapping.get(currentNode));
        }

        final SplitTree<S, I, O> u = st.findLowestSubsetNode(currentSet).orElseThrow(IllegalStateException::new);
        final Pair<ADSNode<S, I, O>, ADSNode<S, I, O>> ads =
                ADSUtil.buildFromTrace(automaton, u.getSequence(), currentSet.iterator().next());
        final ADSNode<S, I, O> head = ads.getFirst();
        final ADSNode<S, I, O> tail = ads.getSecond();

        head.setParent(predecessor);

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

            final O output = entry.getKey();
            final SplitTree<S, I, O> tree = entry.getValue();
            final Set<S> intersection = new HashSet<>(tree.getPartition());
            intersection.retainAll(currentSet);

            if (!intersection.isEmpty()) {
                final Map<S, S> nextCurrentToInitialMapping = intersection.stream()
                                                                          .collect(Collectors.toMap(key -> u.getMapping()
                                                                                                            .get(key),
                                                                                                    currentToInitialMapping::get));

                final Set<S> nextCurrent =
                        intersection.stream().map(x -> u.getMapping().get(x)).collect(Collectors.toSet());
                tail.getChildren()
                    .put(output, extractADS(automaton, st, nextCurrent, nextCurrentToInitialMapping, tail));
            }
        }

        return head;
    }

    private static <S, I, O> boolean needsRefinement(SplitTree<S, I, O> node) {
        return node.getPartition().size() > 1;
    }

    private static <S, I, O> boolean isValidInput(MealyMachine<S, I, ?, O> automaton, I input, Set<S> states) {

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

        for (S s : states) {
            final O output = automaton.getOutput(s, input);
            final S successor = automaton.getSuccessor(s, input);

            if (!successors.containsKey(output)) {
                successors.put(output, new HashSet<>());
            }

            if (!successors.get(output).add(successor)) {
                return false;
            }
        }

        return true;
    }

    private static <S, I, O> Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> computeValidities(MealyMachine<S, I, ?, O> automaton,
                                                                                                     Alphabet<I> inputs,
                                                                                                     Set<SplitTree<S, I, O>> r,
                                                                                                     Set<SplitTree<S, I, O>> pi) {

        final Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> result = new EnumMap<>(Validity.class);
        final Map<S, Integer> stateToPartitionMap = new HashMap<>();
        final Map<SplitTree<S, I, O>, Integer> nodeToPartitionMap = new HashMap<>(HashUtil.capacity(pi.size()));

        int counter = 0;
        for (SplitTree<S, I, O> partition : pi) {
            for (S s : partition.getPartition()) {
                final Integer previousValue = stateToPartitionMap.put(s, counter);
                assert previousValue == null : "Not a true partition";
            }
            nodeToPartitionMap.put(partition, counter++);
        }

        for (Validity v : Validity.values()) {
            result.put(v, new HashSet<>());
        }

        final Set<SplitTree<S, I, O>> pendingCs = new HashSet<>();
        final Map<Integer, Validity> partitionToClassificationMap = new HashMap<>();

        final CompactUniversalGraph<Void, I> implicationGraph = new CompactUniversalGraph<>(nodeToPartitionMap.size());

        for (int i = 0; i < nodeToPartitionMap.size(); i++) {
            implicationGraph.addIntNode();
        }

        partitionLoop:
        for (SplitTree<S, I, O> b : r) {

            // general validity
            final Map<I, Boolean> validInputMap = new HashMap<>(HashUtil.capacity(inputs.size()));
            for (I i : inputs) {
                validInputMap.put(i, isValidInput(automaton, i, b.getPartition()));
            }

            // a valid
            for (I i : inputs) {

                if (!validInputMap.get(i)) {
                    continue;
                }

                final Set<O> outputs =
                        b.getPartition().stream().map(s -> automaton.getOutput(s, i)).collect(Collectors.toSet());

                if (outputs.size() > 1) {
                    result.get(Validity.A_VALID).add(Pair.of(Word.fromSymbols(i), b));
                    partitionToClassificationMap.put(stateToPartitionMap.get(b.getPartition().iterator().next()),
                                                     Validity.A_VALID);
                    continue partitionLoop;
                }
            }

            // b valid
            for (I i : inputs) {

                if (!validInputMap.get(i)) {
                    continue;
                }

                final Set<Integer> successors = b.getPartition()
                                                 .stream()
                                                 .map(s -> stateToPartitionMap.get(automaton.getSuccessor(s, i)))
                                                 .collect(Collectors.toSet());

                if (successors.size() > 1) {
                    result.get(Validity.B_VALID).add(Pair.of(Word.fromSymbols(i), b));
                    partitionToClassificationMap.put(stateToPartitionMap.get(b.getPartition().iterator().next()),
                                                     Validity.B_VALID);
                    continue partitionLoop;
                }
            }

            // c valid
            // we defer evaluation to later point in time, because we need to check if the target partitions are a- or b-valid
            for (I i : inputs) {

                if (!validInputMap.get(i)) {
                    continue;
                }

                final S nodeInPartition = b.getPartition().iterator().next();
                final S successor = automaton.getSuccessor(nodeInPartition, i);

                final Integer partition = stateToPartitionMap.get(nodeInPartition);
                final Integer successorPartition = stateToPartitionMap.get(successor);

                if (!partition.equals(successorPartition)) {
                    implicationGraph.connect(partition, successorPartition, i);
                    pendingCs.add(b);
                }
            }

            if (pendingCs.contains(b)) {
                continue partitionLoop;
            }

            //if we haven't continued the loop up until here, there is no valid input
            result.get(Validity.INVALID).add(Pair.of(null, b));
        }

        //check remaining potential Cs
        pendingCLoop:
        for (SplitTree<S, I, O> pendingC : pendingCs) {

            final Integer pendingPartition = nodeToPartitionMap.get(pendingC);
            final Iterator<Integer> iter =
                    GraphTraversal.breadthFirstIterator(implicationGraph, Collections.singleton(pendingPartition));

            while (iter.hasNext()) {

                final Integer successor = iter.next();
                final Validity successorValidity = partitionToClassificationMap.get(successor);
                if (successorValidity == Validity.A_VALID || successorValidity == Validity.B_VALID) {
                    final Path<Integer, CompactEdge<I>> path = ShortestPaths.shortestPath(implicationGraph,
                                                                                          pendingPartition,
                                                                                          implicationGraph.size(),
                                                                                          successor);
                    assert path != null; // by construction should never be null
                    final Word<I> word = path.stream().map(CompactEdge::getProperty).collect(Word.collector());

                    result.get(Validity.C_VALID).add(Pair.of(word, pendingC));
                    continue pendingCLoop;
                }
            }

            result.get(Validity.INVALID).add(Pair.of(null, pendingC));
        }

        return result;
    }

    private enum Validity {
        A_VALID,
        B_VALID,
        C_VALID,
        INVALID
    }
}

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.Collections;
19	import java.util.EnumMap;
20	import java.util.HashMap;
21	import java.util.HashSet;
22	import java.util.Iterator;
23	import java.util.Map;
24	import java.util.Set;
25	import java.util.function.Function;
26	import java.util.stream.Collectors;
27
28	import net.automatalib.alphabet.Alphabet;
29	import net.automatalib.automaton.transducer.MealyMachine;
30	import net.automatalib.common.smartcollection.ReflexiveMapView;
31	import net.automatalib.common.util.HashUtil;
32	import net.automatalib.common.util.Pair;
33	import net.automatalib.graph.ads.ADSNode;
34	import net.automatalib.graph.ads.impl.ADSLeafNode;
35	import net.automatalib.graph.base.CompactEdge;
36	import net.automatalib.graph.impl.CompactUniversalGraph;
37	import net.automatalib.util.graph.Path;
38	import net.automatalib.util.graph.ShortestPaths;
39	import net.automatalib.util.graph.traversal.GraphTraversal;
40	import net.automatalib.word.Word;
41
42	/**
43	* Algorithm of Lee and Yannakakis for computing adaptive distinguishing sequences (of length at most n^2) in O(n^2)
44	* time (where n denotes the number of states of the automaton).
45	* <p>
46	* See: D. Lee and M. Yannakakis - "Testing Finite-State Machines: State Identification and Verification", IEEE
47	* Transactions on Computers 43.3 (1994)
48	*/
49	@SuppressWarnings("nullness")	2✔
50	public final class LeeYannakakis {
51
52	private LeeYannakakis() {}
53
54	/**
55	* Computes an ADS using the algorithm of Lee and Yannakakis.
56	*
57	* @param automaton
58	* The automaton for which an ADS should be computed
59	* @param input
60	* the input alphabet of the automaton
61	* @param <S>
62	* (hypothesis) state type
63	* @param <I>
64	* input alphabet type
65	* @param <O>
66	* output alphabet type
67	*
68	* @return A {@link LYResult} containing an adaptive distinguishing sequence (if existent) and a possible set of
69	* indistinguishable states.
70	*/
71	public static <S, I, O> LYResult<S, I, O> compute(MealyMachine<S, I, ?, O> automaton, Alphabet<I> input) {
72
73	final SplitTreeResult<S, I, O> str = computeSplitTree(automaton, input);	2✔
74
75	if (str.isPresent()) {	2✔
76	final Set<S> states = new HashSet<>(automaton.getStates());	2✔
77	return new LYResult<>(extractADS(automaton, str.get(), states, new ReflexiveMapView<>(states), null));	2✔
78	}
79
80	return new LYResult<>(str.getIndistinguishableStates());	2✔
81	}
82
83	private static <S, I, O> SplitTreeResult<S, I, O> computeSplitTree(MealyMachine<S, I, ?, O> automaton,
84	Alphabet<I> input) {
85
86	final SplitTree<S, I, O> st = new SplitTree<>(new HashSet<>(automaton.getStates()));	2✔
87	final Set<SplitTree<S, I, O>> leaves = new HashSet<>(HashUtil.capacity(automaton.size()));	2✔
88	leaves.add(st);	2✔
89
90	while (leaves.stream().anyMatch(LeeYannakakis::needsRefinement)) {	2✔
91
92	final int maxCardinality = leaves.stream()	2✔
93	.mapToInt(x -> x.getPartition().size())	2✔
94	.max()	2✔
95	.orElseThrow(IllegalStateException::new);	2✔
96	final Set<SplitTree<S, I, O>> r =	2✔
97	leaves.stream().filter(x -> x.getPartition().size() == maxCardinality).collect(Collectors.toSet());	2✔
98
99	final Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> validitySetMap =	2✔
100	computeValidities(automaton, input, r, leaves);	2✔
101
102	if (!validitySetMap.get(Validity.INVALID).isEmpty()) {	2✔
103	final Set<Pair<Word<I>, SplitTree<S, I, O>>> set = validitySetMap.get(Validity.INVALID);	2✔
104
105	final Set<S> indistinguishableStates = new HashSet<>();	2✔
106
107	for (Pair<Word<I>, SplitTree<S, I, O>> pair : set) {	2✔
108	indistinguishableStates.addAll(pair.getSecond().getPartition());	2✔
109	}	2✔
110
111	return new SplitTreeResult<>(indistinguishableStates);	2✔
112	}
113
114	// a-valid partitions
115	for (Pair<Word<I>, SplitTree<S, I, O>> aPartition : validitySetMap.get(Validity.A_VALID)) {	2✔
116
117	assert aPartition.getFirst().size() == 1 : "a-valid inputs should always contain exactly 1 symbol";	2✔
118
119	final I aValidInput = aPartition.getFirst().firstSymbol();	2✔
120	final SplitTree<S, I, O> nodeToRefine = aPartition.getSecond();	2✔
121	final Map<O, Set<S>> successorMap = nodeToRefine.getPartition()	2✔
122	.stream()	2✔
123	.collect(Collectors.groupingBy(s -> automaton.getOutput(	2✔
124	s,
125	aValidInput), Collectors.toSet()));	2✔
126
127	nodeToRefine.setSequence(Word.fromSymbols(aValidInput));	2✔
128	leaves.remove(nodeToRefine);	2✔
129
130	for (Map.Entry<O, Set<S>> entry : successorMap.entrySet()) {	2✔
131	final SplitTree<S, I, O> child = new SplitTree<>(entry.getValue());	2✔
132	nodeToRefine.getSuccessors().put(entry.getKey(), child);	2✔
133	leaves.add(child);	2✔
134	}	2✔
135	for (S s : nodeToRefine.getPartition()) {	2✔
136	nodeToRefine.getMapping().put(s, automaton.getSuccessor(s, aValidInput));	2✔
137	}	2✔
138	}	2✔
139
140	// b-valid partitions
141	for (Pair<Word<I>, SplitTree<S, I, O>> bPartition : validitySetMap.get(Validity.B_VALID)) {	2✔
142
143	assert bPartition.getFirst().size() == 1 : "b-valid inputs should always contain exactly 1 symbol";	2✔
144
145	final I bValidInput = bPartition.getFirst().firstSymbol();	2✔
146	final SplitTree<S, I, O> nodeToRefine = bPartition.getSecond();	2✔
147	final Map<S, S> successorsToNodes = nodeToRefine.getPartition()	2✔
148	.stream()	2✔
149	.collect(Collectors.toMap(x -> automaton.getSuccessor(x,	2✔
150	bValidInput),
151	Function.identity()));	2✔
152	final SplitTree<S, I, O> v =	2✔
153	st.findLowestSubsetNode(successorsToNodes.keySet()).orElseThrow(IllegalStateException::new);	2✔
154
155	nodeToRefine.setSequence(v.getSequence().prepend(bValidInput));	2✔
156	leaves.remove(nodeToRefine);	2✔
157
158	for (Map.Entry<O, SplitTree<S, I, O>> entry : v.getSuccessors().entrySet()) {	2✔
159
160	final Set<S> wSet = entry.getValue().getPartition();	2✔
161	final Set<S> intersection = new HashSet<>(successorsToNodes.keySet());	2✔
162	intersection.retainAll(wSet);	2✔
163
164	if (!intersection.isEmpty()) {	2✔
165	final Set<S> indistinguishableNodes =	2✔
166	intersection.stream().map(successorsToNodes::get).collect(Collectors.toSet());	2✔
167	final SplitTree<S, I, O> newChild = new SplitTree<>(indistinguishableNodes);	2✔
168	nodeToRefine.getSuccessors().put(entry.getKey(), newChild);	2✔
169	leaves.add(newChild);	2✔
170	}
171	}	2✔
172	for (S s : nodeToRefine.getPartition()) {	2✔
173	nodeToRefine.getMapping().put(s, v.getMapping().get(automaton.getSuccessor(s, bValidInput)));	2✔
174	}	2✔
175	}	2✔
176
177	// c-valid partitions
178	for (Pair<Word<I>, SplitTree<S, I, O>> cPartition : validitySetMap.get(Validity.C_VALID)) {	2✔
179	final Word<I> cValidInput = cPartition.getFirst();	2✔
180	final SplitTree<S, I, O> nodeToRefine = cPartition.getSecond();	2✔
181	final Map<S, S> successorsToNodes = nodeToRefine.getPartition()	2✔
182	.stream()	2✔
183	.collect(Collectors.toMap(x -> automaton.getSuccessor(x,	2✔
184	cValidInput),
185	Function.identity()));	2✔
186	final SplitTree<S, I, O> c =	2✔
187	st.findLowestSubsetNode(successorsToNodes.keySet()).orElseThrow(IllegalStateException::new);	2✔
188
189	nodeToRefine.setSequence(cValidInput.concat(c.getSequence()));	2✔
190	leaves.remove(nodeToRefine);	2✔
191
192	for (Map.Entry<O, SplitTree<S, I, O>> entry : c.getSuccessors().entrySet()) {	2✔
193
194	final Set<S> wSet = entry.getValue().getPartition();	2✔
195	final Set<S> intersection = new HashSet<>(successorsToNodes.keySet());	2✔
196	intersection.retainAll(wSet);	2✔
197
198	if (!intersection.isEmpty()) {	2✔
199	final Set<S> indistinguishableNodes =	2✔
200	intersection.stream().map(successorsToNodes::get).collect(Collectors.toSet());	2✔
201	final SplitTree<S, I, O> newChild = new SplitTree<>(indistinguishableNodes);	2✔
202	nodeToRefine.getSuccessors().put(entry.getKey(), newChild);	2✔
203	leaves.add(newChild);	2✔
204	}
205	}	2✔
206	for (S s : nodeToRefine.getPartition()) {	2✔
207	nodeToRefine.getMapping().put(s, c.getMapping().get(automaton.getSuccessor(s, cValidInput)));	2✔
208	}	2✔
209	}	2✔
210	}	2✔
211
212	return new SplitTreeResult<>(st);	2✔
213	}
214
215	private static <S, I, O> ADSNode<S, I, O> extractADS(MealyMachine<S, I, ?, O> automaton,
216	SplitTree<S, I, O> st,
217	Set<S> currentSet,
218	Map<S, S> currentToInitialMapping,
219	ADSNode<S, I, O> predecessor) {
220
221	if (currentSet.size() == 1) {	2✔
222	final S currentNode = currentSet.iterator().next();	2✔
223
224	assert currentToInitialMapping.containsKey(currentNode);	2✔
225
226	return new ADSLeafNode<>(predecessor, currentToInitialMapping.get(currentNode));	2✔
227	}
228
229	final SplitTree<S, I, O> u = st.findLowestSubsetNode(currentSet).orElseThrow(IllegalStateException::new);	2✔
230	final Pair<ADSNode<S, I, O>, ADSNode<S, I, O>> ads =	2✔
231	ADSUtil.buildFromTrace(automaton, u.getSequence(), currentSet.iterator().next());	2✔
232	final ADSNode<S, I, O> head = ads.getFirst();	2✔
233	final ADSNode<S, I, O> tail = ads.getSecond();	2✔
234
235	head.setParent(predecessor);	2✔
236
237	for (Map.Entry<O, SplitTree<S, I, O>> entry : u.getSuccessors().entrySet()) {	2✔
238
239	final O output = entry.getKey();	2✔
240	final SplitTree<S, I, O> tree = entry.getValue();	2✔
241	final Set<S> intersection = new HashSet<>(tree.getPartition());	2✔
242	intersection.retainAll(currentSet);	2✔
243
244	if (!intersection.isEmpty()) {	2✔
245	final Map<S, S> nextCurrentToInitialMapping = intersection.stream()	2✔
246	.collect(Collectors.toMap(key -> u.getMapping()	2✔
247	.get(key),	2✔
248	currentToInitialMapping::get));	2✔
249
250	final Set<S> nextCurrent =	2✔
251	intersection.stream().map(x -> u.getMapping().get(x)).collect(Collectors.toSet());	2✔
252	tail.getChildren()	2✔
253	.put(output, extractADS(automaton, st, nextCurrent, nextCurrentToInitialMapping, tail));	2✔
254	}
255	}	2✔
256
257	return head;	2✔
258	}
259
260	private static <S, I, O> boolean needsRefinement(SplitTree<S, I, O> node) {
261	return node.getPartition().size() > 1;	2✔
262	}
263
264	private static <S, I, O> boolean isValidInput(MealyMachine<S, I, ?, O> automaton, I input, Set<S> states) {
265
266	final Map<O, Set<S>> successors = new HashMap<>();	2✔
267
268	for (S s : states) {	2✔
269	final O output = automaton.getOutput(s, input);	2✔
270	final S successor = automaton.getSuccessor(s, input);	2✔
271
272	if (!successors.containsKey(output)) {	2✔
273	successors.put(output, new HashSet<>());	2✔
274	}
275
276	if (!successors.get(output).add(successor)) {	2✔
277	return false;	2✔
278	}
279	}	2✔
280
281	return true;	2✔
282	}
283
284	private static <S, I, O> Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> computeValidities(MealyMachine<S, I, ?, O> automaton,
285	Alphabet<I> inputs,
286	Set<SplitTree<S, I, O>> r,
287	Set<SplitTree<S, I, O>> pi) {
288
289	final Map<Validity, Set<Pair<Word<I>, SplitTree<S, I, O>>>> result = new EnumMap<>(Validity.class);	2✔
290	final Map<S, Integer> stateToPartitionMap = new HashMap<>();	2✔
291	final Map<SplitTree<S, I, O>, Integer> nodeToPartitionMap = new HashMap<>(HashUtil.capacity(pi.size()));	2✔
292
293	int counter = 0;	2✔
294	for (SplitTree<S, I, O> partition : pi) {	2✔
295	for (S s : partition.getPartition()) {	2✔
296	final Integer previousValue = stateToPartitionMap.put(s, counter);	2✔
297	assert previousValue == null : "Not a true partition";	2✔
298	}	2✔
299	nodeToPartitionMap.put(partition, counter++);	2✔
300	}	2✔
301
302	for (Validity v : Validity.values()) {	2✔
303	result.put(v, new HashSet<>());	2✔
304	}
305
306	final Set<SplitTree<S, I, O>> pendingCs = new HashSet<>();	2✔
307	final Map<Integer, Validity> partitionToClassificationMap = new HashMap<>();	2✔
308
309	final CompactUniversalGraph<Void, I> implicationGraph = new CompactUniversalGraph<>(nodeToPartitionMap.size());	2✔
310
311	for (int i = 0; i < nodeToPartitionMap.size(); i++) {	2✔
312	implicationGraph.addIntNode();	2✔
313	}
314
315	partitionLoop:
316	for (SplitTree<S, I, O> b : r) {	2✔
317
318	// general validity
319	final Map<I, Boolean> validInputMap = new HashMap<>(HashUtil.capacity(inputs.size()));	2✔
320	for (I i : inputs) {	2✔
321	validInputMap.put(i, isValidInput(automaton, i, b.getPartition()));	2✔
322	}	2✔
323
324	// a valid
325	for (I i : inputs) {	2✔
326
327	if (!validInputMap.get(i)) {	2✔
328	continue;	2✔
329	}
330
331	final Set<O> outputs =	2✔
332	b.getPartition().stream().map(s -> automaton.getOutput(s, i)).collect(Collectors.toSet());	2✔
333
334	if (outputs.size() > 1) {	2✔
335	result.get(Validity.A_VALID).add(Pair.of(Word.fromSymbols(i), b));	2✔
336	partitionToClassificationMap.put(stateToPartitionMap.get(b.getPartition().iterator().next()),	2✔
337	Validity.A_VALID);
338	continue partitionLoop;	2✔
339	}
340	}	2✔
341
342	// b valid
343	for (I i : inputs) {	2✔
344
345	if (!validInputMap.get(i)) {	2✔
346	continue;	2✔
347	}
348
349	final Set<Integer> successors = b.getPartition()	2✔
350	.stream()	2✔
351	.map(s -> stateToPartitionMap.get(automaton.getSuccessor(s, i)))	2✔
352	.collect(Collectors.toSet());	2✔
353
354	if (successors.size() > 1) {	2✔
355	result.get(Validity.B_VALID).add(Pair.of(Word.fromSymbols(i), b));	2✔
356	partitionToClassificationMap.put(stateToPartitionMap.get(b.getPartition().iterator().next()),	2✔
357	Validity.B_VALID);
358	continue partitionLoop;	2✔
359	}
360	}	2✔
361
362	// c valid
363	// we defer evaluation to later point in time, because we need to check if the target partitions are a- or b-valid
364	for (I i : inputs) {	2✔
365
366	if (!validInputMap.get(i)) {	2✔
367	continue;	2✔
368	}
369
370	final S nodeInPartition = b.getPartition().iterator().next();	2✔
371	final S successor = automaton.getSuccessor(nodeInPartition, i);	2✔
372
373	final Integer partition = stateToPartitionMap.get(nodeInPartition);	2✔
374	final Integer successorPartition = stateToPartitionMap.get(successor);	2✔
375
376	if (!partition.equals(successorPartition)) {	2✔
377	implicationGraph.connect(partition, successorPartition, i);	2✔
378	pendingCs.add(b);	2✔
379	}
380	}	2✔
381
382	if (pendingCs.contains(b)) {	2✔
383	continue partitionLoop;	2✔
384	}
385
386	//if we haven't continued the loop up until here, there is no valid input
387	result.get(Validity.INVALID).add(Pair.of(null, b));	2✔
388	}	2✔
389
390	//check remaining potential Cs
391	pendingCLoop:
392	for (SplitTree<S, I, O> pendingC : pendingCs) {	2✔
393
394	final Integer pendingPartition = nodeToPartitionMap.get(pendingC);	2✔
395	final Iterator<Integer> iter =	2✔
396	GraphTraversal.breadthFirstIterator(implicationGraph, Collections.singleton(pendingPartition));	2✔
397
398	while (iter.hasNext()) {	2✔
399
400	final Integer successor = iter.next();	2✔
401	final Validity successorValidity = partitionToClassificationMap.get(successor);	2✔
402	if (successorValidity == Validity.A_VALID \|\| successorValidity == Validity.B_VALID) {	2✔
403	final Path<Integer, CompactEdge<I>> path = ShortestPaths.shortestPath(implicationGraph,	2✔
404	pendingPartition,
405	implicationGraph.size(),	2✔
406	successor);
407	assert path != null; // by construction should never be null	2✔
408	final Word<I> word = path.stream().map(CompactEdge::getProperty).collect(Word.collector());	2✔
409
410	result.get(Validity.C_VALID).add(Pair.of(word, pendingC));	2✔
411	continue pendingCLoop;	2✔
412	}
413	}	2✔
414
415	result.get(Validity.INVALID).add(Pair.of(null, pendingC));	×
416	}	×
417
418	return result;	2✔
419	}
420
421	private enum Validity {	2✔
422	A_VALID,	2✔
423	B_VALID,	2✔
424	C_VALID,	2✔
425	INVALID	2✔
426	}
427	}

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