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

/incremental/src/main/java/net/automatalib/incremental/dfa/dag/AbstractIncrementalDFADAGBuilder.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.dfa.dag;

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

import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.UniversalAutomaton;
import net.automatalib.automaton.concept.StateIDs;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.graph.TransitionEdge;
import net.automatalib.automaton.graph.UniversalAutomatonGraphView;
import net.automatalib.common.util.IntDisjointSets;
import net.automatalib.common.util.UnionFind;
import net.automatalib.graph.Graph;
import net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder;
import net.automatalib.incremental.dfa.AbstractVisualizationHelper;
import net.automatalib.incremental.dfa.Acceptance;
import net.automatalib.ts.UniversalDTS;
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;

abstract class AbstractIncrementalDFADAGBuilder<I> extends AbstractIncrementalDFABuilder<I> {

    final Map<StateSignature, State> register;
    final State init;
    State sink;

    AbstractIncrementalDFADAGBuilder(Alphabet<I> inputAlphabet) {
        super(inputAlphabet);
        this.register = new LinkedHashMap<>();
        StateSignature sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW);
        this.init = new State(sig);
        register.put(sig, init);
    }

    @Override
    public void addAlphabetSymbol(I symbol) {
        final int oldSize = alphabetSize;
        super.addAlphabetSymbol(symbol);
        final int newSize = alphabetSize;

        if (oldSize < newSize) {
            register.values().forEach(n -> n.ensureInputCapacity(newSize));
        }
    }

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

    private <S> @Nullable Word<I> doFindSeparatingWord(DFA<S, I> target,
                                                       Collection<? extends I> inputs,
                                                       boolean omitUndefined) {
        int thisStates = register.size();
        Map<State, Integer> stateIds = new HashMap<>();
        if (sink != null) {
            stateIds.put(sink, 0);
            thisStates++;
        }
        int targetStates = target.size();
        if (!omitUndefined) {
            targetStates++;
        }

        S init2 = target.getInitialState();

        if (init2 == null && omitUndefined) {
            return null;
        }

        State init1 = init;

        boolean acc = init2 != null && target.isAccepting(init2);
        if (init1.getAcceptance().conflicts(acc)) {
            return Word.epsilon();
        }

        IntDisjointSets uf = new UnionFind(thisStates + targetStates);
        StateIDs<S> tgtIds = target.stateIDs();
        int id1 = getStateId(init1, stateIds);
        int id2 = (init2 != null ? tgtIds.getStateId(init2) : targetStates - 1) + thisStates;

        uf.link(id1, id2);

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

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

        I lastSym = null;

        Record<@Nullable S, I> current;

        explore:
        while ((current = queue.poll()) != null) {
            State state1 = current.state1;
            @Nullable S state2 = current.state2;

            for (I sym : inputs) {
                @Nullable S succ2 = (state2 != null) ? target.getSuccessor(state2, sym) : null;
                if (succ2 == null && omitUndefined) {
                    continue;
                }

                int idx = inputAlphabet.getSymbolIndex(sym);
                State succ1 = state1 != sink ? state1.getSuccessor(idx) : sink;

                if (succ1 == null) {
                    continue;
                }

                id1 = getStateId(succ1, stateIds);
                id2 = (succ2 != null ? tgtIds.getStateId(succ2) : targetStates - 1) + thisStates;

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

                if (r1 == r2) {
                    continue;
                }

                if (succ1 == sink) {
                    if (succ2 == null) {
                        continue;
                    }
                    if (target.isAccepting(succ2)) {
                        lastSym = sym;
                        break explore;
                    }
                } else {
                    boolean succ2acc = succ2 != null && target.isAccepting(succ2);
                    if (succ1.getAcceptance().conflicts(succ2acc)) {
                        lastSym = sym;
                        break explore;
                    }
                }

                uf.link(r1, r2);

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

        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 int getStateId(State s, Map<State, Integer> idMap) {
        Integer id = idMap.get(s);
        if (id != null) {
            return id;
        }
        id = idMap.size();
        idMap.put(s, id);
        return id;
    }

    abstract @Nullable State getState(Word<? extends I> word);

    void updateInitSignature(Acceptance acc) {
        StateSignature sig = init.getSignature();
        sig.acceptance = acc;
    }

    void updateInitSignature(int idx, State succ) {
        StateSignature sig = init.getSignature();
        State oldSucc = sig.successors.array[idx];
        if (oldSucc == succ) {
            return;
        }
        if (oldSucc != null) {
            oldSucc.decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        succ.increaseIncoming();
    }

    void updateInitSignature(Acceptance acc, int idx, State succ) {
        StateSignature sig = init.getSignature();
        State oldSucc = sig.successors.array[idx];
        Acceptance oldAcc = sig.acceptance;
        if (oldSucc == succ && oldAcc == acc) {
            return;
        }
        if (oldSucc != null) {
            oldSucc.decreaseIncoming();
        }
        sig.successors.array[idx] = succ;
        succ.increaseIncoming();
        sig.acceptance = acc;
    }

    /**
     * Updates the signature for a given state.
     *
     * @param state
     *         the state
     * @param acc
     *         the new acceptance value
     *
     * @return the canonical state for the updated signature
     */
    State updateSignature(State state, Acceptance acc) {
        assert state != init;
        StateSignature sig = state.getSignature();
        if (sig.acceptance == acc) {
            return state;
        }
        register.remove(sig);
        sig.acceptance = acc;
        sig.updateHashCode();
        return replaceOrRegister(state);
    }

    /**
     * Updates the signature for a given state.
     *
     * @param state
     *         the state
     * @param idx
     *         the index of the transition to change
     * @param succ
     *         the new successor for the above index
     *
     * @return the canonical state for the updated signature
     */
    State updateSignature(State state, int idx, State succ) {
        assert state != init;

        StateSignature 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);
    }

    State updateSignature(State state, Acceptance acc, int idx, State succ) {
        assert state != init;

        StateSignature sig = state.getSignature();
        if (sig.successors.array[idx] == succ && sig.acceptance == acc) {
            return state;
        }
        register.remove(sig);
        sig.successors.array[idx] = succ;
        sig.acceptance = acc;
        succ.increaseIncoming();
        sig.updateHashCode();
        return replaceOrRegister(state);
    }

    /**
     * Returns the canonical state for the given state's signature, or registers the state as canonical if no state with
     * that signature exists.
     *
     * @param state
     *         the state
     *
     * @return the canonical state for the given state's signature
     */
    State replaceOrRegister(State state) {
        StateSignature sig = state.getSignature();
        State other = register.get(sig);
        if (other != null) {
            if (state != other) {
                for (int i = 0; i < sig.successors.array.length; i++) {
                    State succ = sig.successors.array[i];
                    if (succ != null) {
                        succ.decreaseIncoming();
                    }
                }
            }
            return other;
        }

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

    /**
     * Returns (and possibly creates) the canonical state for the given signature.
     *
     * @param sig
     *         the signature
     *
     * @return the canonical state for the given signature
     */
    State replaceOrRegister(StateSignature sig) {
        State 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 succ = sig.successors.array[i];
            if (succ != null) {
                succ.increaseIncoming();
            }
        }
        return state;
    }

    State hiddenClone(State other) {
        assert other != init;

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

    void hide(State state) {
        assert state != init;

        StateSignature sig = state.getSignature();
        register.remove(sig);
    }

    State unhide(State state, Acceptance acc, int idx, State succ) {
        assert state != init;

        StateSignature sig = state.getSignature();
        sig.acceptance = acc;
        State 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);
    }

    State unhide(State state, int idx, State succ) {
        assert state != init;

        StateSignature sig = state.getSignature();
        State 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);
    }

    /**
     * Clones a state, changing the signature.
     *
     * @param other
     *         the state to clone
     * @param acc
     *         the new acceptance value
     *
     * @return the canonical state for the derived signature
     */
    State clone(State other, Acceptance acc) {
        assert other != init;

        StateSignature sig = other.getSignature();
        if (sig.acceptance == acc) {
            return other;
        }
        sig = sig.duplicate();
        sig.acceptance = acc;
        sig.updateHashCode();
        return replaceOrRegister(sig);
    }

    /**
     * Clones a state, changing the signature.
     *
     * @param other
     *         the state to clone
     * @param idx
     *         the index of the transition to change
     * @param succ
     *         the new successor state
     *
     * @return the canonical state for the derived signature
     */
    State clone(State other, int idx, State succ) {
        assert other != init;

        StateSignature sig = other.getSignature();
        if (sig.successors.array[idx] == succ) {
            return other;
        }
        sig = sig.duplicate();
        sig.successors.array[idx] = succ;
        sig.updateHashCode();
        return replaceOrRegister(sig);
    }

    State clone(State other, Acceptance acc, int idx, State succ) {
        assert other != init;

        StateSignature sig = other.getSignature();
        if (sig.successors.array[idx] == succ && sig.acceptance == acc) {
            return other;
        }
        sig = sig.duplicate();
        sig.successors.array[idx] = succ;
        sig.acceptance = acc;
        return replaceOrRegister(sig);
    }

    @Override
    public UniversalDTS<?, I, ?, Acceptance, Void> asTransitionSystem() {
        return new TransitionSystemView();
    }

    @Override
    public Graph<?, ?> asGraph() {
        return new UniversalAutomatonGraphView<State, I, State, Acceptance, Void, TransitionSystemView>(new TransitionSystemView(),
                                                                                                        inputAlphabet) {

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

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

                        if (node.isConfluence()) {
                            String shape = (node.getAcceptance() == Acceptance.TRUE) ?
                                    NodeShapes.DOUBLEOCTAGON :
                                    NodeShapes.OCTAGON;
                            properties.put(NodeAttrs.SHAPE, shape);
                        }
                        return true;
                    }

                    @Override
                    public Acceptance getAcceptance(State state) {
                        return state.getAcceptance();
                    }
                };
            }
        };
    }

    private static final class Record<S, I> {

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

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

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

    private class TransitionSystemView implements UniversalDTS<State, I, State, Acceptance, Void>,
                                                  UniversalAutomaton<State, I, State, Acceptance, Void> {

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

        @Override
        public State getTransition(State state, I input) {
            if (state == sink) {
                return state;
            }
            int idx = inputAlphabet.getSymbolIndex(input);
            return state.getSuccessor(idx);
        }

        @Override
        public State getInitialState() {
            return init;
        }

        @Override
        public Acceptance getStateProperty(State state) {
            return state.getAcceptance();
        }

        @Override
        public Void getTransitionProperty(State transition) {
            return null;
        }

        @Override
        public Collection<State> getStates() {
            if (sink == null) {
                return Collections.unmodifiableCollection(register.values());
            }
            List<State> result = new ArrayList<>(register.size() + 1);
            result.addAll(register.values());
            result.add(sink);
            return result;
        }
    }

}

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.dfa.dag;
17
18	import java.util.ArrayDeque;
19	import java.util.ArrayList;
20	import java.util.Collection;
21	import java.util.Collections;
22	import java.util.HashMap;
23	import java.util.LinkedHashMap;
24	import java.util.List;
25	import java.util.Map;
26	import java.util.Queue;
27
28	import net.automatalib.alphabet.Alphabet;
29	import net.automatalib.automaton.UniversalAutomaton;
30	import net.automatalib.automaton.concept.StateIDs;
31	import net.automatalib.automaton.fsa.DFA;
32	import net.automatalib.automaton.graph.TransitionEdge;
33	import net.automatalib.automaton.graph.UniversalAutomatonGraphView;
34	import net.automatalib.common.util.IntDisjointSets;
35	import net.automatalib.common.util.UnionFind;
36	import net.automatalib.graph.Graph;
37	import net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder;
38	import net.automatalib.incremental.dfa.AbstractVisualizationHelper;
39	import net.automatalib.incremental.dfa.Acceptance;
40	import net.automatalib.ts.UniversalDTS;
41	import net.automatalib.visualization.VisualizationHelper;
42	import net.automatalib.word.Word;
43	import net.automatalib.word.WordBuilder;
44	import org.checkerframework.checker.nullness.qual.Nullable;
45
46	abstract class AbstractIncrementalDFADAGBuilder<I> extends AbstractIncrementalDFABuilder<I> {	2✔
47
48	final Map<StateSignature, State> register;
49	final State init;
50	State sink;
51
52	AbstractIncrementalDFADAGBuilder(Alphabet<I> inputAlphabet) {
53	super(inputAlphabet);	2✔
54	this.register = new LinkedHashMap<>();	2✔
55	StateSignature sig = new StateSignature(alphabetSize, Acceptance.DONT_KNOW);	2✔
56	this.init = new State(sig);	2✔
57	register.put(sig, init);	2✔
58	}	2✔
59
60	@Override
61	public void addAlphabetSymbol(I symbol) {
62	final int oldSize = alphabetSize;	2✔
63	super.addAlphabetSymbol(symbol);	2✔
64	final int newSize = alphabetSize;	2✔
65
66	if (oldSize < newSize) {	2✔
67	register.values().forEach(n -> n.ensureInputCapacity(newSize));	2✔
68	}
69	}	2✔
70
71	@Override
72	public @Nullable Word<I> findSeparatingWord(DFA<?, I> target,
73	Collection<? extends I> inputs,
74	boolean omitUndefined) {
75	return doFindSeparatingWord(target, inputs, omitUndefined);	2✔
76	}
77
78	private <S> @Nullable Word<I> doFindSeparatingWord(DFA<S, I> target,
79	Collection<? extends I> inputs,
80	boolean omitUndefined) {
81	int thisStates = register.size();	2✔
82	Map<State, Integer> stateIds = new HashMap<>();	2✔
83	if (sink != null) {	2✔
84	stateIds.put(sink, 0);	2✔
85	thisStates++;	2✔
86	}
87	int targetStates = target.size();	2✔
88	if (!omitUndefined) {	2✔
89	targetStates++;	2✔
90	}
91
92	S init2 = target.getInitialState();	2✔
93
94	if (init2 == null && omitUndefined) {	2✔
95	return null;	2✔
96	}
97
98	State init1 = init;	2✔
99
100	boolean acc = init2 != null && target.isAccepting(init2);	2✔
101	if (init1.getAcceptance().conflicts(acc)) {	2✔
102	return Word.epsilon();	2✔
103	}
104
105	IntDisjointSets uf = new UnionFind(thisStates + targetStates);	2✔
106	StateIDs<S> tgtIds = target.stateIDs();	2✔
107	int id1 = getStateId(init1, stateIds);	2✔
108	int id2 = (init2 != null ? tgtIds.getStateId(init2) : targetStates - 1) + thisStates;	2✔
109
110	uf.link(id1, id2);	2✔
111
112	Queue<Record<@Nullable S, I>> queue = new ArrayDeque<>();	2✔
113
114	queue.add(new Record<>(init1, init2));	2✔
115
116	I lastSym = null;	2✔
117
118	Record<@Nullable S, I> current;
119
120	explore:
121	while ((current = queue.poll()) != null) {	2✔
122	State state1 = current.state1;	2✔
123	@Nullable S state2 = current.state2;	2✔
124
125	for (I sym : inputs) {	2✔
126	@Nullable S succ2 = (state2 != null) ? target.getSuccessor(state2, sym) : null;	2✔
127	if (succ2 == null && omitUndefined) {	2✔
128	continue;	2✔
129	}
130
131	int idx = inputAlphabet.getSymbolIndex(sym);	2✔
132	State succ1 = state1 != sink ? state1.getSuccessor(idx) : sink;	2✔
133
134	if (succ1 == null) {	2✔
135	continue;	2✔
136	}
137
138	id1 = getStateId(succ1, stateIds);	2✔
139	id2 = (succ2 != null ? tgtIds.getStateId(succ2) : targetStates - 1) + thisStates;	2✔
140
141	int r1 = uf.find(id1), r2 = uf.find(id2);	2✔
142
143	if (r1 == r2) {	2✔
UNCOV 144	continue;	×
145	}
146
147	if (succ1 == sink) {	2✔
148	if (succ2 == null) {	2✔
149	continue;	2✔
150	}
151	if (target.isAccepting(succ2)) {	2✔
152	lastSym = sym;	2✔
153	break explore;	2✔
154	}
155	} else {
156	boolean succ2acc = succ2 != null && target.isAccepting(succ2);	2✔
157	if (succ1.getAcceptance().conflicts(succ2acc)) {	2✔
158	lastSym = sym;	2✔
159	break explore;	2✔
160	}
161	}
162
163	uf.link(r1, r2);	2✔
164
165	queue.add(new Record<>(succ1, succ2, sym, current));	2✔
166	}	2✔
167	}	2✔
168
169	if (current == null) {	2✔
170	return null;	2✔
171	}
172
173	int ceLength = current.depth;	2✔
174	if (lastSym != null) {	2✔
175	ceLength++;	2✔
176	}
177
178	@SuppressWarnings("nullness") // we make sure to set each index to a value of type I
179	WordBuilder<I> wb = new WordBuilder<>(null, ceLength);	2✔
180
181	int index = ceLength;	2✔
182
183	if (lastSym != null) {	2✔
184	wb.setSymbol(--index, lastSym);	2✔
185	}
186
187	while (current.reachedFrom != null) {	2✔
188	final I reachedVia = current.reachedVia;	2✔
189	wb.setSymbol(--index, reachedVia);	2✔
190	current = current.reachedFrom;	2✔
191	}	2✔
192
193	return wb.toWord();	2✔
194	}
195
196	private static int getStateId(State s, Map<State, Integer> idMap) {
197	Integer id = idMap.get(s);	2✔
198	if (id != null) {	2✔
199	return id;	2✔
200	}
201	id = idMap.size();	2✔
202	idMap.put(s, id);	2✔
203	return id;	2✔
204	}
205
206	abstract @Nullable State getState(Word<? extends I> word);
207
208	void updateInitSignature(Acceptance acc) {
209	StateSignature sig = init.getSignature();	2✔
210	sig.acceptance = acc;	2✔
211	}	2✔
212
213	void updateInitSignature(int idx, State succ) {
214	StateSignature sig = init.getSignature();	2✔
215	State oldSucc = sig.successors.array[idx];	2✔
216	if (oldSucc == succ) {	2✔
217	return;	2✔
218	}
219	if (oldSucc != null) {	2✔
220	oldSucc.decreaseIncoming();	2✔
221	}
222	sig.successors.array[idx] = succ;	2✔
223	succ.increaseIncoming();	2✔
224	}	2✔
225
226	void updateInitSignature(Acceptance acc, int idx, State succ) {
227	StateSignature sig = init.getSignature();	2✔
228	State oldSucc = sig.successors.array[idx];	2✔
229	Acceptance oldAcc = sig.acceptance;	2✔
230	if (oldSucc == succ && oldAcc == acc) {	2✔
231	return;	2✔
232	}
233	if (oldSucc != null) {	2✔
234	oldSucc.decreaseIncoming();	2✔
235	}
236	sig.successors.array[idx] = succ;	2✔
237	succ.increaseIncoming();	2✔
238	sig.acceptance = acc;	2✔
239	}	2✔
240
241	/**
242	* Updates the signature for a given state.
243	*
244	* @param state
245	* the state
246	* @param acc
247	* the new acceptance value
248	*
249	* @return the canonical state for the updated signature
250	*/
251	State updateSignature(State state, Acceptance acc) {
252	assert state != init;	2✔
253	StateSignature sig = state.getSignature();	2✔
254	if (sig.acceptance == acc) {	2✔
UNCOV 255	return state;	×
256	}
257	register.remove(sig);	2✔
258	sig.acceptance = acc;	2✔
259	sig.updateHashCode();	2✔
260	return replaceOrRegister(state);	2✔
261	}
262
263	/**
264	* Updates the signature for a given state.
265	*
266	* @param state
267	* the state
268	* @param idx
269	* the index of the transition to change
270	* @param succ
271	* the new successor for the above index
272	*
273	* @return the canonical state for the updated signature
274	*/
275	State updateSignature(State state, int idx, State succ) {
276	assert state != init;	2✔
277
278	StateSignature sig = state.getSignature();	2✔
279	if (sig.successors.array[idx] == succ) {	2✔
280	return state;	2✔
281	}
282	register.remove(sig);	2✔
283	if (sig.successors.array[idx] != null) {	2✔
284	sig.successors.array[idx].decreaseIncoming();	2✔
285	}
286
287	sig.successors.array[idx] = succ;	2✔
288	succ.increaseIncoming();	2✔
289	sig.updateHashCode();	2✔
290	return replaceOrRegister(state);	2✔
291	}
292
293	State updateSignature(State state, Acceptance acc, int idx, State succ) {
294	assert state != init;	2✔
295
296	StateSignature sig = state.getSignature();	2✔
297	if (sig.successors.array[idx] == succ && sig.acceptance == acc) {	2✔
298	return state;	2✔
299	}
300	register.remove(sig);	2✔
301	sig.successors.array[idx] = succ;	2✔
302	sig.acceptance = acc;	2✔
303	succ.increaseIncoming();	2✔
304	sig.updateHashCode();	2✔
305	return replaceOrRegister(state);	2✔
306	}
307
308	/**
309	* Returns the canonical state for the given state's signature, or registers the state as canonical if no state with
310	* that signature exists.
311	*
312	* @param state
313	* the state
314	*
315	* @return the canonical state for the given state's signature
316	*/
317	State replaceOrRegister(State state) {
318	StateSignature sig = state.getSignature();	2✔
319	State other = register.get(sig);	2✔
320	if (other != null) {	2✔
321	if (state != other) {	2✔
322	for (int i = 0; i < sig.successors.array.length; i++) {	2✔
323	State succ = sig.successors.array[i];	2✔
324	if (succ != null) {	2✔
325	succ.decreaseIncoming();	2✔
326	}
327	}
328	}
329	return other;	2✔
330	}
331
332	register.put(sig, state);	2✔
333	return state;	2✔
334	}
335
336	/**
337	* Returns (and possibly creates) the canonical state for the given signature.
338	*
339	* @param sig
340	* the signature
341	*
342	* @return the canonical state for the given signature
343	*/
344	State replaceOrRegister(StateSignature sig) {
345	State state = register.get(sig);	2✔
346	if (state != null) {	2✔
347	return state;	2✔
348	}
349
350	state = new State(sig);	2✔
351	register.put(sig, state);	2✔
352	for (int i = 0; i < sig.successors.array.length; i++) {	2✔
353	State succ = sig.successors.array[i];	2✔
354	if (succ != null) {	2✔
355	succ.increaseIncoming();	2✔
356	}
357	}
358	return state;	2✔
359	}
360
361	State hiddenClone(State other) {
362	assert other != init;	2✔
363
364	StateSignature sig = other.getSignature().duplicate();	2✔
365	for (int i = 0; i < alphabetSize; i++) {	2✔
366	State succ = sig.successors.array[i];	2✔
367	if (succ != null) {	2✔
368	succ.increaseIncoming();	2✔
369	}
370	}
371	return new State(sig);	2✔
372	}
373
374	void hide(State state) {
375	assert state != init;	2✔
376
377	StateSignature sig = state.getSignature();	2✔
378	register.remove(sig);	2✔
379	}	2✔
380
381	State unhide(State state, Acceptance acc, int idx, State succ) {
382	assert state != init;	2✔
383
384	StateSignature sig = state.getSignature();	2✔
385	sig.acceptance = acc;	2✔
386	State prevSucc = sig.successors.array[idx];	2✔
387	if (prevSucc != null) {	2✔
UNCOV 388	prevSucc.decreaseIncoming();	×
389	}
390	sig.successors.array[idx] = succ;	2✔
391	if (succ != null) {	2✔
392	succ.increaseIncoming();	2✔
393	}
394	sig.updateHashCode();	2✔
395
396	return replaceOrRegister(state);	2✔
397	}
398
399	State unhide(State state, int idx, State succ) {
400	assert state != init;	2✔
401
402	StateSignature sig = state.getSignature();	2✔
403	State prevSucc = sig.successors.array[idx];	2✔
404	if (prevSucc != null) {	2✔
UNCOV 405	prevSucc.decreaseIncoming();	×
406	}
407	sig.successors.array[idx] = succ;	2✔
408	if (succ != null) {	2✔
409	succ.increaseIncoming();	2✔
410	}
411	sig.updateHashCode();	2✔
412
413	return replaceOrRegister(state);	2✔
414	}
415
416	/**
417	* Clones a state, changing the signature.
418	*
419	* @param other
420	* the state to clone
421	* @param acc
422	* the new acceptance value
423	*
424	* @return the canonical state for the derived signature
425	*/
426	State clone(State other, Acceptance acc) {
427	assert other != init;	2✔
428
429	StateSignature sig = other.getSignature();	2✔
430	if (sig.acceptance == acc) {	2✔
UNCOV 431	return other;	×
432	}
433	sig = sig.duplicate();	2✔
434	sig.acceptance = acc;	2✔
435	sig.updateHashCode();	2✔
436	return replaceOrRegister(sig);	2✔
437	}
438
439	/**
440	* Clones a state, changing the signature.
441	*
442	* @param other
443	* the state to clone
444	* @param idx
445	* the index of the transition to change
446	* @param succ
447	* the new successor state
448	*
449	* @return the canonical state for the derived signature
450	*/
451	State clone(State other, int idx, State succ) {
452	assert other != init;	2✔
453
454	StateSignature sig = other.getSignature();	2✔
455	if (sig.successors.array[idx] == succ) {	2✔
UNCOV 456	return other;	×
457	}
458	sig = sig.duplicate();	2✔
459	sig.successors.array[idx] = succ;	2✔
460	sig.updateHashCode();	2✔
461	return replaceOrRegister(sig);	2✔
462	}
463
464	State clone(State other, Acceptance acc, int idx, State succ) {
465	assert other != init;	2✔
466
467	StateSignature sig = other.getSignature();	2✔
468	if (sig.successors.array[idx] == succ && sig.acceptance == acc) {	2✔
UNCOV 469	return other;	×
470	}
471	sig = sig.duplicate();	2✔
472	sig.successors.array[idx] = succ;	2✔
473	sig.acceptance = acc;	2✔
474	return replaceOrRegister(sig);	2✔
475	}
476
477	@Override
478	public UniversalDTS<?, I, ?, Acceptance, Void> asTransitionSystem() {
479	return new TransitionSystemView();	2✔
480	}
481
482	@Override
483	public Graph<?, ?> asGraph() {
484	return new UniversalAutomatonGraphView<State, I, State, Acceptance, Void, TransitionSystemView>(new TransitionSystemView(),	2✔
485	inputAlphabet) {	2✔
486
487	@Override
488	public VisualizationHelper<State, TransitionEdge<I, State>> getVisualizationHelper() {
489	return new AbstractVisualizationHelper<State, I, State, TransitionSystemView>(automaton) {	2✔
490
491	@Override
492	public boolean getNodeProperties(State node, Map<String, String> properties) {
493	super.getNodeProperties(node, properties);	2✔
494
495	if (node.isConfluence()) {	2✔
496	String shape = (node.getAcceptance() == Acceptance.TRUE) ?	2✔
497	NodeShapes.DOUBLEOCTAGON :
498	NodeShapes.OCTAGON;
499	properties.put(NodeAttrs.SHAPE, shape);	2✔
500	}
501	return true;	2✔
502	}
503
504	@Override
505	public Acceptance getAcceptance(State state) {
506	return state.getAcceptance();	2✔
507	}
508	};
509	}
510	};
511	}
512
513	private static final class Record<S, I> {
514
515	public final State state1;
516	public final S state2;
517	public final I reachedVia;
518	public final @Nullable Record<S, I> reachedFrom;
519	public final int depth;
520
521	@SuppressWarnings("nullness") // we will only access reachedVia after checking reachedFrom for null
522	Record(State state1, S state2) {	2✔
523	this.state1 = state1;	2✔
524	this.state2 = state2;	2✔
525	this.reachedVia = null;	2✔
526	this.reachedFrom = null;	2✔
527	this.depth = 0;	2✔
528	}	2✔
529
530	Record(State state1, S state2, I reachedVia, Record<S, I> reachedFrom) {	2✔
531	this.state1 = state1;	2✔
532	this.state2 = state2;	2✔
533	this.reachedVia = reachedVia;	2✔
534	this.reachedFrom = reachedFrom;	2✔
535	this.depth = reachedFrom.depth + 1;	2✔
536	}	2✔
537	}
538
539	private class TransitionSystemView implements UniversalDTS<State, I, State, Acceptance, Void>,	2✔
540	UniversalAutomaton<State, I, State, Acceptance, Void> {
541
542	@Override
543	public State getSuccessor(State transition) {
544	return transition;	2✔
545	}
546
547	@Override
548	public State getTransition(State state, I input) {
549	if (state == sink) {	2✔
550	return state;	2✔
551	}
552	int idx = inputAlphabet.getSymbolIndex(input);	2✔
553	return state.getSuccessor(idx);	2✔
554	}
555
556	@Override
557	public State getInitialState() {
558	return init;	2✔
559	}
560
561	@Override
562	public Acceptance getStateProperty(State state) {
563	return state.getAcceptance();	2✔
564	}
565
566	@Override
567	public Void getTransitionProperty(State transition) {
UNCOV 568	return null;	×
569	}
570
571	@Override
572	public Collection<State> getStates() {
573	if (sink == null) {	2✔
574	return Collections.unmodifiableCollection(register.values());	2✔
575	}
576	List<State> result = new ArrayList<>(register.size() + 1);	2✔
577	result.addAll(register.values());	2✔
578	result.add(sink);	2✔
579	return result;	2✔
580	}
581	}
582
583	}

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