6763327895

Committed 05 Nov 2023 07:29PM UTC coverage: 89.726% (-0.1%) from 89.868%

Build # 6763327895

Build Type

push

github

Committed by

mtf90

Commit Message

fix typo

Run Details

4 of 4 new or added lines in 4 files covered. (100.0%)

99 existing lines in 18 files now uncovered.

15677 of 17472 relevant lines covered (89.73%)

1.66 hits per line

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

96.7

/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of AutomataLib, http://www.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.incremental.moore.dag;

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

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.Alphabets;
import net.automatalib.automaton.concept.InputAlphabetHolder;
import net.automatalib.automaton.concept.StateIDs;
import net.automatalib.automaton.graph.TransitionEdge;
import net.automatalib.automaton.transducer.MooreMachine;
import net.automatalib.automaton.transducer.MooreMachine.MooreGraphView;
import net.automatalib.automaton.visualization.MooreVisualizationHelper;
import net.automatalib.common.util.IntDisjointSets;
import net.automatalib.common.util.UnionFind;
import net.automatalib.graph.Graph;
import net.automatalib.incremental.ConflictException;
import net.automatalib.incremental.moore.IncrementalMooreBuilder;
import net.automatalib.ts.output.MooreTransitionSystem;
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Incrementally builds an (acyclic) Moore machine from a set of input and corresponding output words.
 *
 * @param <I>
 *         input symbol class
 * @param <O>
 *         output symbol class
 */
public class IncrementalMooreDAGBuilder<I, O> implements IncrementalMooreBuilder<I, O>, InputAlphabetHolder<I> {

    private final Map<@Nullable StateSignature<O>, State<O>> register;
    private final Alphabet<I> inputAlphabet;
    private int alphabetSize;
    private @MonotonicNonNull State<O> init;

    /**
     * Constructor.
     *
     * @param inputAlphabet
     *         the input alphabet to use
     */
    public IncrementalMooreDAGBuilder(Alphabet<I> inputAlphabet) {
        this.register = new LinkedHashMap<>();
        this.inputAlphabet = inputAlphabet;
        this.alphabetSize = inputAlphabet.size();
    }

    @Override
    public void addAlphabetSymbol(I symbol) {
        if (!this.inputAlphabet.containsSymbol(symbol)) {
            Alphabets.toGrowingAlphabetOrThrowException(this.inputAlphabet).addSymbol(symbol);
        }

        final int newAlphabetSize = this.inputAlphabet.size();
        // even if the symbol was already in the alphabet, we need to make sure to be able to store the new symbol
        if (alphabetSize < newAlphabetSize) {
            register.values().forEach(n -> n.ensureInputCapacity(newAlphabetSize));
            alphabetSize = newAlphabetSize;
        }
    }

    @Override
    public boolean hasDefinitiveInformation(Word<? extends I> word) {
        return getState(word) != null;
    }

    /**
     * Retrieves the (internal) state reached by the given input word, or {@code null} if no information about the input
     * word is present.
     *
     * @param word
     *         the input word
     *
     * @return the corresponding state
     */
    private @Nullable State<O> getState(Word<? extends I> word) {
        State<O> s = init;

        if (s == null) {
            return null;
        }

        for (I sym : word) {
            int idx = inputAlphabet.getSymbolIndex(sym);
            s = s.getSuccessor(idx);
            if (s == null) {
                break;
            }
        }
        return s;
    }

    @Override
    public boolean lookup(Word<? extends I> word, List<? super O> output) {
        State<O> curr = init;

        if (curr == null) {
            return false;
        }

        output.add(curr.getOutput());

        for (I sym : word) {
            int idx = inputAlphabet.getSymbolIndex(sym);
            State<O> succ = curr.getSuccessor(idx);
            if (succ == null) {
                return false;
            }
            output.add(succ.getOutput());
            curr = succ;
        }

        return true;
    }

    @Override
    public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
        assert word.size() + 1 == outputWord.size();

        Iterator<? extends O> outWordIterator = outputWord.iterator();
        final O rootOut = outWordIterator.next();

        if (init == null) {
            StateSignature<O> initSig = new StateSignature<>(alphabetSize, rootOut);
            this.init = new State<>(initSig);
            register.put(null, init);
        }

        State<O> curr = init;
        State<O> conf = null;

        Deque<Transition<O>> path = new ArrayDeque<>();

        // Find the internal state in the automaton that can be reached by a
        // maximal prefix of the word (i.e., a path of secured information)
        for (I sym : word) {
            // During this, store the *first* confluence state (i.e., state with multiple incoming edges).
            if (conf == null && curr.isConfluence()) {
                conf = curr;
            }

            int idx = inputAlphabet.getSymbolIndex(sym);
            State<O> succ = curr.getSuccessor(idx);
            if (succ == null) {
                break;
            }

            // If a transition exists for the input symbol, it also has an output symbol.
            // Check if this matches the provided one, otherwise there is a conflict
            O outSym = outWordIterator.next();
            if (!Objects.equals(outSym, succ.getOutput())) {
                throw new ConflictException(
                        "Error inserting " + word.prefix(path.size() + 1) + " / " + outputWord.prefix(path.size() + 1) +
                        ": Incompatible output symbols: " + outSym + " vs " + curr.getOutput());
            }
            path.push(new Transition<>(curr, idx));
            curr = succ;
        }

        int len = word.length();
        int prefixLen = path.size();

        // The information was already present - we do not need to continue
        if (prefixLen == len) {
            return;
        }

        State<O> last = curr;

        if (conf != null) {
            if (conf == last) {
                conf = null;
            }
            last = hiddenClone(last);
            if (conf == null) {
                Transition<O> peek = path.peek();
                assert peek != null;
                State<O> prev = peek.state;
                if (prev != init) {
                    updateSignature(prev, peek.transIdx, last);
                } else {
                    updateInitSignature(peek.transIdx, last);
                }
            }
        } else if (last != init) {
            hide(last);
        }

        // We then create a suffix path, i.e., a linear sequence of states corresponding to
        // the suffix (more precisely: the suffix minus the first symbol, since this is the
        // transition which is used for gluing the suffix path to the existing automaton).
        Word<? extends I> suffix = word.subWord(prefixLen);
        Word<? extends O> suffixOut = outputWord.subWord(prefixLen);

        // Here we prepare the "gluing" transition
        I sym = suffix.firstSymbol();
        int suffTransIdx = inputAlphabet.getSymbolIndex(sym);
        O suffTransOut = suffixOut.firstSymbol();

        State<O> suffixState = createSuffix(suffix.subWord(1), suffixOut.subWord(1));

        if (last != init) {
            last = unhide(last, suffTransIdx, suffixState);

            // the suffixState may be part of our current path and become confluent due to un-hiding
            if (suffixState.isConfluence()) {
                // update the reference with whatever state comes first
                final Iterator<Transition<O>> iter = path.descendingIterator();
                while (iter.hasNext()) {
                    final State<O> s = iter.next().state;
                    if (s == conf || s == suffixState) {
                        conf = s;
                        break;
                    }
                }
            }
        } else {
            updateInitSignature(suffTransIdx, suffixState, suffTransOut);
        }

        if (path.isEmpty()) {
            return;
        }

        if (conf != null) {
            // If there was a confluence state, we have to clone all nodes on
            // the prefix path up to this state, in order to separate it from other
            // prefixes reaching the confluence state (we do not know anything about them plus the suffix).
            Transition<O> next;
            do {
                next = path.pop();
                State<O> state = next.state;
                int idx = next.transIdx;
                state = clone(state, idx, last);
                last = state;
            } while (next.state != conf);
        }

        // Finally, we have to refresh all the signatures, iterating backwards until the updating becomes stable.
        while (path.size() > 1) {
            Transition<O> next = path.pop();
            State<O> state = next.state;
            int idx = next.transIdx;

            // when extending the path we previously traversed (i.e. expanding the suffix), it may happen that we end up
            // adding a cyclic transition. If this is the case, simply clone the current state and update the parent in
            // the next iteration
            if (state == last) {
                last = clone(state, idx, last);
                continue;
            }

            State<O> updated = updateSignature(state, idx, last);
            if (state == updated) {
                return;
            }
            last = updated;
        }

        int finalIdx = path.pop().transIdx;

        updateInitSignature(finalIdx, last);
    }

    private State<O> hiddenClone(State<O> other) {
        StateSignature<O> sig = other.getSignature().duplicate();

        for (int i = 0; i < alphabetSize; i++) {
            State<O> succ = sig.successors.array[i];
            if (succ != null) {
                succ.increaseIncoming();
            }
        }
        return new State<>(sig);
    }

    /**
     * Update the signature of a state, changing only the successor state of a single transition index.
     *
     * @param state
     *         the state which's signature to update
     * @param idx
     *         the transition index to modify
     * @param succ
     *         the new successor state
     *
     * @return the resulting state, which can either be the same as the input state (if the new signature is unique), or
     * the result of merging with another state.
     */
    private State<O> updateSignature(State<O> state, int idx, State<O> succ) {
        StateSignature<O> sig = state.getSignature();
        if (sig.successors.array[idx] == succ) {
            return state;
        }

        register.remove(sig);
        if (sig.successors.array[idx] != null) {
            sig.successors.array[idx].decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        succ.increaseIncoming();
        sig.updateHashCode();
        return replaceOrRegister(state);
    }

    /**
     * Update the signature of the initial state. This requires special handling, as the initial state is not stored in
     * the register (since it can never legally act as a predecessor).
     *
     * @param idx
     *         the transition index being changed
     * @param succ
     *         the new successor state
     */
    private void updateInitSignature(int idx, State<O> succ) {
        assert init != null;
        StateSignature<O> sig = init.getSignature();
        State<O> oldSucc = sig.successors.array[idx];
        if (oldSucc == succ) {
            return;
        }
        if (oldSucc != null) {
            oldSucc.decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        succ.increaseIncoming();
    }

    /**
     * Updates the signature of the initial state, changing both the successor state and the output symbol.
     *
     * @param idx
     *         the transition index to change
     * @param succ
     *         the new successor state
     * @param out
     *         the output symbol
     */
    private void updateInitSignature(int idx, State<O> succ, O out) {
        assert init != null;
        StateSignature<O> sig = init.getSignature();
        State<O> oldSucc = sig.successors.array[idx];
        if (oldSucc == succ && Objects.equals(out, succ.getOutput())) {
            return;
        }
        if (oldSucc != null) {
            oldSucc.decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        succ.increaseIncoming();
    }

    private void hide(State<O> state) {
        assert state != init;
        StateSignature<O> sig = state.getSignature();

        register.remove(sig);
    }

    private State<O> createSuffix(Word<? extends I> suffix, Word<? extends O> suffixOut) {
        StateSignature<O> sig = new StateSignature<>(alphabetSize, suffixOut.lastSymbol());
        sig.updateHashCode();
        State<O> last = replaceOrRegister(sig);

        int len = suffix.length();
        for (int i = len - 1; i >= 0; i--) {
            sig = new StateSignature<>(alphabetSize, suffixOut.getSymbol(i));
            I sym = suffix.getSymbol(i);
            int idx = inputAlphabet.getSymbolIndex(sym);
            sig.successors.array[idx] = last;
            sig.updateHashCode();
            last = replaceOrRegister(sig);
        }

        return last;
    }

    private State<O> unhide(State<O> state, int idx, State<O> succ) {
        StateSignature<O> sig = state.getSignature();
        State<O> prevSucc = sig.successors.array[idx];
        if (prevSucc != null) {
            prevSucc.decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        if (succ != null) {
            succ.increaseIncoming();
        }
        sig.updateHashCode();
        return replaceOrRegister(state);
    }

    private State<O> clone(State<O> other, int idx, State<O> succ) {
        StateSignature<O> sig = other.getSignature();
        if (sig.successors.array[idx] == succ) {
            return other;
        }
        sig = sig.duplicate();
        sig.successors.array[idx] = succ;
        sig.updateHashCode();
        return replaceOrRegister(sig);
    }

    private State<O> replaceOrRegister(State<O> state) {
        StateSignature<O> sig = state.getSignature();
        State<O> other = register.get(sig);
        if (other != null) {
            if (state != other) {
                for (int i = 0; i < sig.successors.array.length; i++) {
                    State<O> succ = sig.successors.array[i];
                    if (succ != null) {
                        succ.decreaseIncoming();
                    }
                }
            }
            return other;
        }

        register.put(sig, state);
        return state;
    }

    private State<O> replaceOrRegister(StateSignature<O> sig) {
        State<O> state = register.get(sig);
        if (state != null) {
            return state;
        }

        state = new State<>(sig);
        register.put(sig, state);
        for (int i = 0; i < sig.successors.array.length; i++) {
            State<O> succ = sig.successors.array[i];
            if (succ != null) {
                succ.increaseIncoming();
            }
        }
        return state;
    }

    @Override
    public @Nullable Word<I> findSeparatingWord(MooreMachine<?, I, ?, O> target,
                                                Collection<? extends I> inputs,
                                                boolean omitUndefined) {
        return doFindSeparatingWord(target, inputs, omitUndefined);
    }

    private <S, T> @Nullable Word<I> doFindSeparatingWord(MooreMachine<S, I, T, O> moore,
                                                          Collection<? extends I> inputs,
                                                          boolean omitUndefined) {
        State<O> init1 = init;
        S init2 = moore.getInitialState();

        if (init1 == null && init2 == null) {
            return null;
        } else if (init1 == null || init2 == null) {
            return omitUndefined ? null : Word.epsilon();
        }

        if (!Objects.equals(init1.getOutput(), moore.getStateOutput(init2))) {
            return Word.epsilon();
        }

        Map<State<O>, Integer> ids = new HashMap<>();
        StateIDs<S> mooreIds = moore.stateIDs();

        int thisStates = register.size();
        int id1 = getStateId(init1, ids), id2 = mooreIds.getStateId(init2) + thisStates;

        IntDisjointSets uf = new UnionFind(thisStates + moore.size());
        uf.link(id1, id2);

        Queue<Record<S, I, O>> queue = new ArrayDeque<>();

        queue.offer(new Record<>(init1, init2));

        I lastSym = null;

        Record<S, I, O> current;

        explore:
        while ((current = queue.poll()) != null) {
            State<O> state1 = current.state1;
            S state2 = current.state2;

            for (I sym : inputs) {
                int idx = inputAlphabet.getSymbolIndex(sym);
                State<O> succ1 = state1.getSuccessor(idx);
                if (succ1 == null) {
                    continue;
                }

                S succ2 = moore.getSuccessor(state2, sym);
                if (succ2 == null) {
                    if (omitUndefined) {
                        continue;
                    }
                    lastSym = sym;
                    break explore;
                }

                O out1 = succ1.getOutput();
                O out2 = moore.getStateOutput(succ2);
                if (!Objects.equals(out1, out2)) {
                    lastSym = sym;
                    break explore;
                }

                id1 = getStateId(succ1, ids);
                id2 = mooreIds.getStateId(succ2) + thisStates;

                int r1 = uf.find(id1), r2 = uf.find(id2);

                if (r1 == r2) {
                    continue;
                }

                uf.link(r1, r2);

                queue.offer(new Record<>(succ1, succ2, current, sym));
            }
        }

        if (current == null) {
            return null;
        }

        int ceLength = current.depth;
        if (lastSym != null) {
            ceLength++;
        }

        @SuppressWarnings("nullness") // we make sure to set each index to a value of type I
        WordBuilder<I> wb = new WordBuilder<>(null, ceLength);

        int index = ceLength;

        if (lastSym != null) {
            wb.setSymbol(--index, lastSym);
        }

        while (current.reachedFrom != null) {
            final I reachedVia = current.reachedVia;
            wb.setSymbol(--index, reachedVia);
            current = current.reachedFrom;
        }

        return wb.toWord();
    }

    private static <O> int getStateId(State<O> state, Map<State<O>, Integer> ids) {
        return ids.computeIfAbsent(state, k -> ids.size());
    }

    @Override
    public Alphabet<I> getInputAlphabet() {
        return inputAlphabet;
    }

    @Override
    public MooreTransitionSystem<?, I, ?, O> asTransitionSystem() {
        return new AutomatonView();
    }

    @Override
    public Graph<?, ?> asGraph() {
        return new MooreGraphView<State<O>, I, State<O>, O, AutomatonView>(new AutomatonView(), inputAlphabet) {

            @Override
            public VisualizationHelper<State<O>, TransitionEdge<I, State<O>>> getVisualizationHelper() {
                return new MooreVisualizationHelper<State<O>, I, State<O>, O>(automaton) {

                    @Override
                    public boolean getNodeProperties(State<O> node, Map<String, String> properties) {
                        super.getNodeProperties(node, properties);

                        properties.put(NodeAttrs.LABEL, String.valueOf(node.getOutput()));
                        if (node.isConfluence()) {
                            properties.put(NodeAttrs.SHAPE, NodeShapes.OCTAGON);
                        }

                        return true;
                    }
                };
            }
        };
    }

    // /////////////////////////////////////////////////////////////////////
    // Equivalence test //
    // /////////////////////////////////////////////////////////////////////

    private static final class Record<S, I, O> {

        private final State<O> state1;
        private final S state2;
        private final I reachedVia;
        private final @Nullable Record<S, I, O> reachedFrom;
        private final int depth;

        @SuppressWarnings("nullness") // we will only access reachedVia after checking reachedFrom for null
        Record(State<O> state1, S state2) {
            this.state1 = state1;
            this.state2 = state2;
            this.reachedFrom = null;
            this.reachedVia = null;
            this.depth = 0;
        }

        Record(State<O> state1, S state2, Record<S, I, O> reachedFrom, I reachedVia) {
            this.state1 = state1;
            this.state2 = state2;
            this.reachedFrom = reachedFrom;
            this.reachedVia = reachedVia;
            this.depth = reachedFrom.depth + 1;
        }
    }

    private class AutomatonView implements MooreMachine<State<O>, I, State<O>, O> {

        @Override
        public O getStateOutput(State<O> state) {
            return state.getOutput();
        }

        @Override
        public @Nullable State<O> getTransition(State<O> state, I input) {
            return state.getSuccessor(inputAlphabet.getSymbolIndex(input));
        }

        @Override
        public State<O> getSuccessor(State<O> transition) {
            return transition;
        }

        @Override
        public @Nullable State<O> getInitialState() {
            return init;
        }

        @Override
        public Collection<State<O>> getStates() {
            return Collections.unmodifiableCollection(register.values());
        }
    }
}

1	/* Copyright (C) 2013-2023 TU Dortmund
2	* This file is part of AutomataLib, http://www.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.incremental.moore.dag;
17
18	import java.util.ArrayDeque;
19	import java.util.Collection;
20	import java.util.Collections;
21	import java.util.Deque;
22	import java.util.HashMap;
23	import java.util.Iterator;
24	import java.util.LinkedHashMap;
25	import java.util.List;
26	import java.util.Map;
27	import java.util.Objects;
28	import java.util.Queue;
29
30	import net.automatalib.alphabet.Alphabet;
31	import net.automatalib.alphabet.Alphabets;
32	import net.automatalib.automaton.concept.InputAlphabetHolder;
33	import net.automatalib.automaton.concept.StateIDs;
34	import net.automatalib.automaton.graph.TransitionEdge;
35	import net.automatalib.automaton.transducer.MooreMachine;
36	import net.automatalib.automaton.transducer.MooreMachine.MooreGraphView;
37	import net.automatalib.automaton.visualization.MooreVisualizationHelper;
38	import net.automatalib.common.util.IntDisjointSets;
39	import net.automatalib.common.util.UnionFind;
40	import net.automatalib.graph.Graph;
41	import net.automatalib.incremental.ConflictException;
42	import net.automatalib.incremental.moore.IncrementalMooreBuilder;
43	import net.automatalib.ts.output.MooreTransitionSystem;
44	import net.automatalib.visualization.VisualizationHelper;
45	import net.automatalib.word.Word;
46	import net.automatalib.word.WordBuilder;
47	import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
48	import org.checkerframework.checker.nullness.qual.Nullable;
49
50	/**
51	* Incrementally builds an (acyclic) Moore machine from a set of input and corresponding output words.
52	*
53	* @param <I>
54	* input symbol class
55	* @param <O>
56	* output symbol class
57	*/
58	public class IncrementalMooreDAGBuilder<I, O> implements IncrementalMooreBuilder<I, O>, InputAlphabetHolder<I> {	2✔
59
60	private final Map<@Nullable StateSignature<O>, State<O>> register;
61	private final Alphabet<I> inputAlphabet;
62	private int alphabetSize;
63	private @MonotonicNonNull State<O> init;
64
65	/**
66	* Constructor.
67	*
68	* @param inputAlphabet
69	* the input alphabet to use
70	*/
71	public IncrementalMooreDAGBuilder(Alphabet<I> inputAlphabet) {	2✔
72	this.register = new LinkedHashMap<>();	2✔
73	this.inputAlphabet = inputAlphabet;	2✔
74	this.alphabetSize = inputAlphabet.size();	2✔
75	}	2✔
76
77	@Override
78	public void addAlphabetSymbol(I symbol) {
79	if (!this.inputAlphabet.containsSymbol(symbol)) {	2✔
80	Alphabets.toGrowingAlphabetOrThrowException(this.inputAlphabet).addSymbol(symbol);	2✔
81	}
82
83	final int newAlphabetSize = this.inputAlphabet.size();	2✔
84	// even if the symbol was already in the alphabet, we need to make sure to be able to store the new symbol
85	if (alphabetSize < newAlphabetSize) {	2✔
86	register.values().forEach(n -> n.ensureInputCapacity(newAlphabetSize));	2✔
87	alphabetSize = newAlphabetSize;	2✔
88	}
89	}	2✔
90
91	@Override
92	public boolean hasDefinitiveInformation(Word<? extends I> word) {
93	return getState(word) != null;	2✔
94	}
95
96	/**
97	* Retrieves the (internal) state reached by the given input word, or {@code null} if no information about the input
98	* word is present.
99	*
100	* @param word
101	* the input word
102	*
103	* @return the corresponding state
104	*/
105	private @Nullable State<O> getState(Word<? extends I> word) {
106	State<O> s = init;	2✔
107
108	if (s == null) {	2✔
109	return null;	2✔
110	}
111
112	for (I sym : word) {	2✔
113	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
114	s = s.getSuccessor(idx);	2✔
115	if (s == null) {	2✔
116	break;	2✔
117	}
118	}	2✔
119	return s;	2✔
120	}
121
122	@Override
123	public boolean lookup(Word<? extends I> word, List<? super O> output) {
124	State<O> curr = init;	2✔
125
126	if (curr == null) {	2✔
UNCOV 127	return false;	×
128	}
129
130	output.add(curr.getOutput());	2✔
131
132	for (I sym : word) {	2✔
133	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
134	State<O> succ = curr.getSuccessor(idx);	2✔
135	if (succ == null) {	2✔
136	return false;	2✔
137	}
138	output.add(succ.getOutput());	2✔
139	curr = succ;	2✔
140	}	2✔
141
142	return true;	2✔
143	}
144
145	@Override
146	public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
147	assert word.size() + 1 == outputWord.size();	2✔
148
149	Iterator<? extends O> outWordIterator = outputWord.iterator();	2✔
150	final O rootOut = outWordIterator.next();	2✔
151
152	if (init == null) {	2✔
153	StateSignature<O> initSig = new StateSignature<>(alphabetSize, rootOut);	2✔
154	this.init = new State<>(initSig);	2✔
155	register.put(null, init);	2✔
156	}
157
158	State<O> curr = init;	2✔
159	State<O> conf = null;	2✔
160
161	Deque<Transition<O>> path = new ArrayDeque<>();	2✔
162
163	// Find the internal state in the automaton that can be reached by a
164	// maximal prefix of the word (i.e., a path of secured information)
165	for (I sym : word) {	2✔
166	// During this, store the first confluence state (i.e., state with multiple incoming edges).
167	if (conf == null && curr.isConfluence()) {	2✔
168	conf = curr;	2✔
169	}
170
171	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
172	State<O> succ = curr.getSuccessor(idx);	2✔
173	if (succ == null) {	2✔
174	break;	2✔
175	}
176
177	// If a transition exists for the input symbol, it also has an output symbol.
178	// Check if this matches the provided one, otherwise there is a conflict
179	O outSym = outWordIterator.next();	2✔
180	if (!Objects.equals(outSym, succ.getOutput())) {	2✔
181	throw new ConflictException(	2✔
182	"Error inserting " + word.prefix(path.size() + 1) + " / " + outputWord.prefix(path.size() + 1) +	2✔
183	": Incompatible output symbols: " + outSym + " vs " + curr.getOutput());	2✔
184	}
185	path.push(new Transition<>(curr, idx));	2✔
186	curr = succ;	2✔
187	}	2✔
188
189	int len = word.length();	2✔
190	int prefixLen = path.size();	2✔
191
192	// The information was already present - we do not need to continue
193	if (prefixLen == len) {	2✔
194	return;	2✔
195	}
196
197	State<O> last = curr;	2✔
198
199	if (conf != null) {	2✔
200	if (conf == last) {	2✔
201	conf = null;	2✔
202	}
203	last = hiddenClone(last);	2✔
204	if (conf == null) {	2✔
205	Transition<O> peek = path.peek();	2✔
206	assert peek != null;	2✔
207	State<O> prev = peek.state;	2✔
208	if (prev != init) {	2✔
209	updateSignature(prev, peek.transIdx, last);	2✔
210	} else {
211	updateInitSignature(peek.transIdx, last);	2✔
212	}
213	}	2✔
214	} else if (last != init) {	2✔
215	hide(last);	2✔
216	}
217
218	// We then create a suffix path, i.e., a linear sequence of states corresponding to
219	// the suffix (more precisely: the suffix minus the first symbol, since this is the
220	// transition which is used for gluing the suffix path to the existing automaton).
221	Word<? extends I> suffix = word.subWord(prefixLen);	2✔
222	Word<? extends O> suffixOut = outputWord.subWord(prefixLen);	2✔
223
224	// Here we prepare the "gluing" transition
225	I sym = suffix.firstSymbol();	2✔
226	int suffTransIdx = inputAlphabet.getSymbolIndex(sym);	2✔
227	O suffTransOut = suffixOut.firstSymbol();	2✔
228
229	State<O> suffixState = createSuffix(suffix.subWord(1), suffixOut.subWord(1));	2✔
230
231	if (last != init) {	2✔
232	last = unhide(last, suffTransIdx, suffixState);	2✔
233
234	// the suffixState may be part of our current path and become confluent due to un-hiding
235	if (suffixState.isConfluence()) {	2✔
236	// update the reference with whatever state comes first
237	final Iterator<Transition<O>> iter = path.descendingIterator();	2✔
238	while (iter.hasNext()) {	2✔
239	final State<O> s = iter.next().state;	2✔
240	if (s == conf \|\| s == suffixState) {	2✔
241	conf = s;	2✔
242	break;	2✔
243	}
244	}	2✔
245	}	2✔
246	} else {
247	updateInitSignature(suffTransIdx, suffixState, suffTransOut);	2✔
248	}
249
250	if (path.isEmpty()) {	2✔
251	return;	2✔
252	}
253
254	if (conf != null) {	2✔
255	// If there was a confluence state, we have to clone all nodes on
256	// the prefix path up to this state, in order to separate it from other
257	// prefixes reaching the confluence state (we do not know anything about them plus the suffix).
258	Transition<O> next;
259	do {
260	next = path.pop();	2✔
261	State<O> state = next.state;	2✔
262	int idx = next.transIdx;	2✔
263	state = clone(state, idx, last);	2✔
264	last = state;	2✔
265	} while (next.state != conf);	2✔
266	}
267
268	// Finally, we have to refresh all the signatures, iterating backwards until the updating becomes stable.
269	while (path.size() > 1) {	2✔
270	Transition<O> next = path.pop();	2✔
271	State<O> state = next.state;	2✔
272	int idx = next.transIdx;	2✔
273
274	// when extending the path we previously traversed (i.e. expanding the suffix), it may happen that we end up
275	// adding a cyclic transition. If this is the case, simply clone the current state and update the parent in
276	// the next iteration
277	if (state == last) {	2✔
278	last = clone(state, idx, last);	2✔
279	continue;	2✔
280	}
281
282	State<O> updated = updateSignature(state, idx, last);	2✔
283	if (state == updated) {	2✔
284	return;	2✔
285	}
286	last = updated;	2✔
287	}	2✔
288
289	int finalIdx = path.pop().transIdx;	2✔
290
291	updateInitSignature(finalIdx, last);	2✔
292	}	2✔
293
294	private State<O> hiddenClone(State<O> other) {
295	StateSignature<O> sig = other.getSignature().duplicate();	2✔
296
297	for (int i = 0; i < alphabetSize; i++) {	2✔
298	State<O> succ = sig.successors.array[i];	2✔
299	if (succ != null) {	2✔
300	succ.increaseIncoming();	2✔
301	}
302	}
303	return new State<>(sig);	2✔
304	}
305
306	/**
307	* Update the signature of a state, changing only the successor state of a single transition index.
308	*
309	* @param state
310	* the state which's signature to update
311	* @param idx
312	* the transition index to modify
313	* @param succ
314	* the new successor state
315	*
316	* @return the resulting state, which can either be the same as the input state (if the new signature is unique), or
317	* the result of merging with another state.
318	*/
319	private State<O> updateSignature(State<O> state, int idx, State<O> succ) {
320	StateSignature<O> sig = state.getSignature();	2✔
321	if (sig.successors.array[idx] == succ) {	2✔
322	return state;	2✔
323	}
324
325	register.remove(sig);	2✔
326	if (sig.successors.array[idx] != null) {	2✔
327	sig.successors.array[idx].decreaseIncoming();	2✔
328	}
329	sig.successors.array[idx] = succ;	2✔
330	succ.increaseIncoming();	2✔
331	sig.updateHashCode();	2✔
332	return replaceOrRegister(state);	2✔
333	}
334
335	/**
336	* Update the signature of the initial state. This requires special handling, as the initial state is not stored in
337	* the register (since it can never legally act as a predecessor).
338	*
339	* @param idx
340	* the transition index being changed
341	* @param succ
342	* the new successor state
343	*/
344	private void updateInitSignature(int idx, State<O> succ) {
345	assert init != null;	2✔
346	StateSignature<O> sig = init.getSignature();	2✔
347	State<O> oldSucc = sig.successors.array[idx];	2✔
348	if (oldSucc == succ) {	2✔
349	return;	2✔
350	}
351	if (oldSucc != null) {	2✔
352	oldSucc.decreaseIncoming();	2✔
353	}
354	sig.successors.array[idx] = succ;	2✔
355	succ.increaseIncoming();	2✔
356	}	2✔
357
358	/**
359	* Updates the signature of the initial state, changing both the successor state and the output symbol.
360	*
361	* @param idx
362	* the transition index to change
363	* @param succ
364	* the new successor state
365	* @param out
366	* the output symbol
367	*/
368	private void updateInitSignature(int idx, State<O> succ, O out) {
369	assert init != null;	2✔
370	StateSignature<O> sig = init.getSignature();	2✔
371	State<O> oldSucc = sig.successors.array[idx];	2✔
372	if (oldSucc == succ && Objects.equals(out, succ.getOutput())) {	2✔
UNCOV 373	return;	×
374	}
375	if (oldSucc != null) {	2✔
UNCOV 376	oldSucc.decreaseIncoming();	×
377	}
378	sig.successors.array[idx] = succ;	2✔
379	succ.increaseIncoming();	2✔
380	}	2✔
381
382	private void hide(State<O> state) {
383	assert state != init;	2✔
384	StateSignature<O> sig = state.getSignature();	2✔
385
386	register.remove(sig);	2✔
387	}	2✔
388
389	private State<O> createSuffix(Word<? extends I> suffix, Word<? extends O> suffixOut) {
390	StateSignature<O> sig = new StateSignature<>(alphabetSize, suffixOut.lastSymbol());	2✔
391	sig.updateHashCode();	2✔
392	State<O> last = replaceOrRegister(sig);	2✔
393
394	int len = suffix.length();	2✔
395	for (int i = len - 1; i >= 0; i--) {	2✔
396	sig = new StateSignature<>(alphabetSize, suffixOut.getSymbol(i));	2✔
397	I sym = suffix.getSymbol(i);	2✔
398	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
399	sig.successors.array[idx] = last;	2✔
400	sig.updateHashCode();	2✔
401	last = replaceOrRegister(sig);	2✔
402	}
403
404	return last;	2✔
405	}
406
407	private State<O> unhide(State<O> state, int idx, State<O> succ) {
408	StateSignature<O> sig = state.getSignature();	2✔
409	State<O> prevSucc = sig.successors.array[idx];	2✔
410	if (prevSucc != null) {	2✔
UNCOV 411	prevSucc.decreaseIncoming();	×
412	}
413	sig.successors.array[idx] = succ;	2✔
414	if (succ != null) {	2✔
415	succ.increaseIncoming();	2✔
416	}
417	sig.updateHashCode();	2✔
418	return replaceOrRegister(state);	2✔
419	}
420
421	private State<O> clone(State<O> other, int idx, State<O> succ) {
422	StateSignature<O> sig = other.getSignature();	2✔
423	if (sig.successors.array[idx] == succ) {	2✔
UNCOV 424	return other;	×
425	}
426	sig = sig.duplicate();	2✔
427	sig.successors.array[idx] = succ;	2✔
428	sig.updateHashCode();	2✔
429	return replaceOrRegister(sig);	2✔
430	}
431
432	private State<O> replaceOrRegister(State<O> state) {
433	StateSignature<O> sig = state.getSignature();	2✔
434	State<O> other = register.get(sig);	2✔
435	if (other != null) {	2✔
436	if (state != other) {	2✔
437	for (int i = 0; i < sig.successors.array.length; i++) {	2✔
438	State<O> succ = sig.successors.array[i];	2✔
439	if (succ != null) {	2✔
440	succ.decreaseIncoming();	2✔
441	}
442	}
443	}
444	return other;	2✔
445	}
446
447	register.put(sig, state);	2✔
448	return state;	2✔
449	}
450
451	private State<O> replaceOrRegister(StateSignature<O> sig) {
452	State<O> state = register.get(sig);	2✔
453	if (state != null) {	2✔
454	return state;	2✔
455	}
456
457	state = new State<>(sig);	2✔
458	register.put(sig, state);	2✔
459	for (int i = 0; i < sig.successors.array.length; i++) {	2✔
460	State<O> succ = sig.successors.array[i];	2✔
461	if (succ != null) {	2✔
462	succ.increaseIncoming();	2✔
463	}
464	}
465	return state;	2✔
466	}
467
468	@Override
469	public @Nullable Word<I> findSeparatingWord(MooreMachine<?, I, ?, O> target,
470	Collection<? extends I> inputs,
471	boolean omitUndefined) {
472	return doFindSeparatingWord(target, inputs, omitUndefined);	2✔
473	}
474
475	private <S, T> @Nullable Word<I> doFindSeparatingWord(MooreMachine<S, I, T, O> moore,
476	Collection<? extends I> inputs,
477	boolean omitUndefined) {
478	State<O> init1 = init;	2✔
479	S init2 = moore.getInitialState();	2✔
480
481	if (init1 == null && init2 == null) {	2✔
UNCOV 482	return null;	×
483	} else if (init1 == null \|\| init2 == null) {	2✔
484	return omitUndefined ? null : Word.epsilon();	2✔
485	}
486
487	if (!Objects.equals(init1.getOutput(), moore.getStateOutput(init2))) {	2✔
UNCOV 488	return Word.epsilon();	×
489	}
490
491	Map<State<O>, Integer> ids = new HashMap<>();	2✔
492	StateIDs<S> mooreIds = moore.stateIDs();	2✔
493
494	int thisStates = register.size();	2✔
495	int id1 = getStateId(init1, ids), id2 = mooreIds.getStateId(init2) + thisStates;	2✔
496
497	IntDisjointSets uf = new UnionFind(thisStates + moore.size());	2✔
498	uf.link(id1, id2);	2✔
499
500	Queue<Record<S, I, O>> queue = new ArrayDeque<>();	2✔
501
502	queue.offer(new Record<>(init1, init2));	2✔
503
504	I lastSym = null;	2✔
505
506	Record<S, I, O> current;
507
508	explore:
509	while ((current = queue.poll()) != null) {	2✔
510	State<O> state1 = current.state1;	2✔
511	S state2 = current.state2;	2✔
512
513	for (I sym : inputs) {	2✔
514	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
515	State<O> succ1 = state1.getSuccessor(idx);	2✔
516	if (succ1 == null) {	2✔
517	continue;	2✔
518	}
519
520	S succ2 = moore.getSuccessor(state2, sym);	2✔
521	if (succ2 == null) {	2✔
522	if (omitUndefined) {	2✔
523	continue;	2✔
524	}
525	lastSym = sym;	2✔
526	break explore;	2✔
527	}
528
529	O out1 = succ1.getOutput();	2✔
530	O out2 = moore.getStateOutput(succ2);	2✔
531	if (!Objects.equals(out1, out2)) {	2✔
532	lastSym = sym;	2✔
533	break explore;	2✔
534	}
535
536	id1 = getStateId(succ1, ids);	2✔
537	id2 = mooreIds.getStateId(succ2) + thisStates;	2✔
538
539	int r1 = uf.find(id1), r2 = uf.find(id2);	2✔
540
541	if (r1 == r2) {	2✔
UNCOV 542	continue;	×
543	}
544
545	uf.link(r1, r2);	2✔
546
547	queue.offer(new Record<>(succ1, succ2, current, sym));	2✔
548	}	2✔
549	}	2✔
550
551	if (current == null) {	2✔
552	return null;	2✔
553	}
554
555	int ceLength = current.depth;	2✔
556	if (lastSym != null) {	2✔
557	ceLength++;	2✔
558	}
559
560	@SuppressWarnings("nullness") // we make sure to set each index to a value of type I
561	WordBuilder<I> wb = new WordBuilder<>(null, ceLength);	2✔
562
563	int index = ceLength;	2✔
564
565	if (lastSym != null) {	2✔
566	wb.setSymbol(--index, lastSym);	2✔
567	}
568
569	while (current.reachedFrom != null) {	2✔
570	final I reachedVia = current.reachedVia;	2✔
571	wb.setSymbol(--index, reachedVia);	2✔
572	current = current.reachedFrom;	2✔
573	}	2✔
574
575	return wb.toWord();	2✔
576	}
577
578	private static <O> int getStateId(State<O> state, Map<State<O>, Integer> ids) {
579	return ids.computeIfAbsent(state, k -> ids.size());	2✔
580	}
581
582	@Override
583	public Alphabet<I> getInputAlphabet() {
UNCOV 584	return inputAlphabet;	×
585	}
586
587	@Override
588	public MooreTransitionSystem<?, I, ?, O> asTransitionSystem() {
589	return new AutomatonView();	2✔
590	}
591
592	@Override
593	public Graph<?, ?> asGraph() {
594	return new MooreGraphView<State<O>, I, State<O>, O, AutomatonView>(new AutomatonView(), inputAlphabet) {	2✔
595
596	@Override
597	public VisualizationHelper<State<O>, TransitionEdge<I, State<O>>> getVisualizationHelper() {
598	return new MooreVisualizationHelper<State<O>, I, State<O>, O>(automaton) {	2✔
599
600	@Override
601	public boolean getNodeProperties(State<O> node, Map<String, String> properties) {
602	super.getNodeProperties(node, properties);	2✔
603
604	properties.put(NodeAttrs.LABEL, String.valueOf(node.getOutput()));	2✔
605	if (node.isConfluence()) {	2✔
UNCOV 606	properties.put(NodeAttrs.SHAPE, NodeShapes.OCTAGON);	×
607	}
608
609	return true;	2✔
610	}
611	};
612	}
613	};
614	}
615
616	// /////////////////////////////////////////////////////////////////////
617	// Equivalence test //
618	// /////////////////////////////////////////////////////////////////////
619
620	private static final class Record<S, I, O> {
621
622	private final State<O> state1;
623	private final S state2;
624	private final I reachedVia;
625	private final @Nullable Record<S, I, O> reachedFrom;
626	private final int depth;
627
628	@SuppressWarnings("nullness") // we will only access reachedVia after checking reachedFrom for null
629	Record(State<O> state1, S state2) {	2✔
630	this.state1 = state1;	2✔
631	this.state2 = state2;	2✔
632	this.reachedFrom = null;	2✔
633	this.reachedVia = null;	2✔
634	this.depth = 0;	2✔
635	}	2✔
636
637	Record(State<O> state1, S state2, Record<S, I, O> reachedFrom, I reachedVia) {	2✔
638	this.state1 = state1;	2✔
639	this.state2 = state2;	2✔
640	this.reachedFrom = reachedFrom;	2✔
641	this.reachedVia = reachedVia;	2✔
642	this.depth = reachedFrom.depth + 1;	2✔
643	}	2✔
644	}
645
646	private class AutomatonView implements MooreMachine<State<O>, I, State<O>, O> {	2✔
647
648	@Override
649	public O getStateOutput(State<O> state) {
650	return state.getOutput();	2✔
651	}
652
653	@Override
654	public @Nullable State<O> getTransition(State<O> state, I input) {
655	return state.getSuccessor(inputAlphabet.getSymbolIndex(input));	2✔
656	}
657
658	@Override
659	public State<O> getSuccessor(State<O> transition) {
660	return transition;	2✔
661	}
662
663	@Override
664	public @Nullable State<O> getInitialState() {
665	return init;	2✔
666	}
667
668	@Override
669	public Collection<State<O>> getStates() {
670	return Collections.unmodifiableCollection(register.values());	2✔
671	}
672	}
673	}

LearnLib / automatalib / 6763327895

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