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.7

/incremental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.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.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.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)) {
            this.inputAlphabet.asGrowingAlphabetOrThrowException().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) {
                    updateInitSignature(peek.transIdx, last);
                } else {
                    updateSignature(prev, 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) {
            updateInitSignature(suffTransIdx, suffixState, suffTransOut);
        } else {
            last = unhide(last, suffTransIdx, suffixState);

            if (conf != null) {
                // in case of a cyclic structure, the suffix may make predecessors of 'conf' confluent due to un-hiding
                // update the reference with whatever confluent state comes first
                final Iterator<Transition<O>> iter = path.descendingIterator();
                while (iter.hasNext()) {
                    final State<O> s = iter.next().state;
                    if (s.isConfluence()) {
                        conf = s;
                        break;
                    }
                }
            }
        }

        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.get(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();
        State<O> oldSucc = sig.successors.get(idx);
        if (oldSucc == succ) {
            return state;
        }

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

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