6654683895

Committed 26 Oct 2023 01:15PM UTC coverage: 89.683% (+0.3%) from 89.4%

Build # 6654683895

Build Type

push

github

Committed by

mtf90

Commit Message

util: handle some more corner-cases in equivalence checks

Run Details

8 of 8 new or added lines in 1 file covered. (100.0%)

15830 of 17651 relevant lines covered (89.68%)

1.66 hits per line

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

98.17

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

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.Deque;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import com.google.common.collect.Iterators;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.incremental.ConflictException;
import net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder;
import net.automatalib.incremental.dfa.Acceptance;
import net.automatalib.util.graph.traversal.GraphTraversal;
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.visualization.helper.DelegateVisualizationHelper;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Incrementally builds a tree, from a set of positive and negative words. Using {@link #insert(Word, boolean)}, either
 * the set of words definitely in the target language or definitely <i>not</i> in the target language is augmented. The
 * {@link #lookup(Word)} method then returns, for a given word, whether this word is in the set of definitely accepted
 * words ({@link Acceptance#TRUE}), definitely rejected words ({@link Acceptance#FALSE}), or neither ({@link
 * Acceptance#DONT_KNOW}).
 *
 * @param <I>
 *         input symbol class
 */
public class IncrementalDFATreeBuilder<I> extends AbstractIncrementalDFABuilder<I> {

    protected final Node root;

    public IncrementalDFATreeBuilder(Alphabet<I> inputAlphabet) {
        super(inputAlphabet);
        this.root = new Node();
    }

    @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) {
            ensureInputCapacity(root, alphabetSize, newAlphabetSize);
            alphabetSize = newAlphabetSize;
        }
    }

    private void ensureInputCapacity(Node node, int oldAlphabetSize, int newAlphabetSize) {
        node.ensureInputCapacity(newAlphabetSize);
        for (int i = 0; i < oldAlphabetSize; i++) {
            final Node child = node.getChild(i);
            if (child != null) {
                ensureInputCapacity(child, oldAlphabetSize, newAlphabetSize);
            }
        }
    }

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

    protected <S> @Nullable Word<I> doFindSeparatingWord(DFA<S, I> target,
                                                         Collection<? extends I> inputs,
                                                         boolean omitUndefined) {
        S automatonInit = target.getInitialState();

        if (automatonInit == null) {
            return omitUndefined ? null : Word.epsilon();
        }

        if (root.getAcceptance().conflicts(target.isAccepting(automatonInit))) {
            return Word.epsilon();
        }

        // incomingInput can be null here, because we will always skip the bottom stack element below
        @SuppressWarnings("nullness")
        Record<@Nullable S, I> init = new Record<>(automatonInit, root, null, inputs.iterator());

        Deque<Record<@Nullable S, I>> dfsStack = new ArrayDeque<>();
        dfsStack.push(init);

        while (!dfsStack.isEmpty()) {
            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
            @NonNull Record<@Nullable S, I> rec = dfsStack.peek();
            if (!rec.inputIt.hasNext()) {
                dfsStack.pop();
                continue;
            }
            I input = rec.inputIt.next();
            int inputIdx = inputAlphabet.getSymbolIndex(input);

            Node succ = rec.treeNode.getChild(inputIdx);
            if (succ == null) {
                continue;
            }

            @Nullable S state = rec.automatonState;
            @Nullable S automatonSucc = state == null ? null : target.getTransition(state, input);
            if (automatonSucc == null && omitUndefined) {
                continue;
            }

            boolean succAcc = automatonSucc != null && target.isAccepting(automatonSucc);

            if (succ.getAcceptance().conflicts(succAcc)) {
                WordBuilder<I> wb = new WordBuilder<>(dfsStack.size());
                wb.append(input);

                dfsStack.pop();
                while (!dfsStack.isEmpty()) {
                    wb.append(rec.incomingInput);
                    rec = dfsStack.pop();
                }
                return wb.reverse().toWord();
            }

            dfsStack.push(new Record<>(automatonSucc, succ, input, inputs.iterator()));
        }

        return null;
    }

    @Override
    public Acceptance lookup(Word<? extends I> inputWord) {
        Node curr = root;

        for (I sym : inputWord) {
            int symIdx = inputAlphabet.getSymbolIndex(sym);
            Node succ = curr.getChild(symIdx);
            if (succ == null) {
                return Acceptance.DONT_KNOW;
            }
            curr = succ;
        }
        return curr.getAcceptance();
    }

    @Override
    public void insert(Word<? extends I> word, boolean acceptance) {
        Node curr = root;

        for (I sym : word) {
            int inputIdx = inputAlphabet.getSymbolIndex(sym);
            Node succ = curr.getChild(inputIdx);
            if (succ == null) {
                succ = new Node();
                curr.setChild(inputIdx, alphabetSize, succ);
            }
            curr = succ;
        }

        Acceptance acc = curr.getAcceptance();
        Acceptance newWordAcc = Acceptance.fromBoolean(acceptance);
        if (acc == Acceptance.DONT_KNOW) {
            curr.setAcceptance(newWordAcc);
        } else if (acc != newWordAcc) {
            throw new ConflictException(
                    "Conflicting acceptance values for word " + word + ": " + acc + " vs " + newWordAcc);
        }
    }

    @Override
    public GraphView asGraph() {
        return new GraphView();
    }

    @Override
    public TransitionSystemView asTransitionSystem() {
        return new TransitionSystemView();
    }

    protected static final class Record<S, I> {

        public final S automatonState;
        public final Node treeNode;
        public final I incomingInput;
        public final Iterator<? extends I> inputIt;

        public Record(S automatonState, Node treeNode, I incomingInput, Iterator<? extends I> inputIt) {
            this.automatonState = automatonState;
            this.treeNode = treeNode;
            this.incomingInput = incomingInput;
            this.inputIt = inputIt;
        }
    }

    public class GraphView extends AbstractGraphView<I, Node, Edge<I>> {

        @Override
        public Collection<Node> getNodes() {
            List<Node> result = new ArrayList<>();
            Iterators.addAll(result, GraphTraversal.depthFirstIterator(this, Collections.singleton(root)));
            return result;
        }

        @Override
        public Collection<Edge<I>> getOutgoingEdges(Node node) {
            List<Edge<I>> result = new ArrayList<>(alphabetSize);
            for (int i = 0; i < alphabetSize; i++) {
                Node succ = node.getChild(i);
                if (succ != null) {
                    result.add(new Edge<>(succ, inputAlphabet.getSymbol(i)));
                }
            }
            return result;
        }

        @Override
        public Node getTarget(Edge<I> edge) {
            return edge.getNode();
        }

        @Override
        public I getInputSymbol(Edge<I> edge) {
            return edge.getInput();
        }

        @Override
        public Acceptance getAcceptance(Node node) {
            return node.getAcceptance();
        }

        @Override
        public Node getInitialNode() {
            return root;
        }

        @Override
        public VisualizationHelper<Node, Edge<I>> getVisualizationHelper() {
            return new DelegateVisualizationHelper<Node, Edge<I>>(super.getVisualizationHelper()) {

                private int id;

                @Override
                public boolean getNodeProperties(Node node, Map<String, String> properties) {
                    if (!super.getNodeProperties(node, properties)) {
                        return false;
                    }
                    properties.put(NodeAttrs.LABEL, "n" + (id++));
                    return true;
                }
            };
        }
    }

    public class TransitionSystemView extends AbstractTransitionSystemView<Node, I, Node> {

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

        @Override
        public @Nullable Node getTransition(Node state, I input) {
            int inputIdx = inputAlphabet.getSymbolIndex(input);
            return state.getChild(inputIdx);
        }

        @Override
        public Node getInitialState() {
            return root;
        }

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

}

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.tree;
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.Deque;
23	import java.util.Iterator;
24	import java.util.List;
25	import java.util.Map;
26
27	import com.google.common.collect.Iterators;
28	import net.automatalib.alphabet.Alphabet;
29	import net.automatalib.alphabet.impl.Alphabets;
30	import net.automatalib.automaton.fsa.DFA;
31	import net.automatalib.incremental.ConflictException;
32	import net.automatalib.incremental.dfa.AbstractIncrementalDFABuilder;
33	import net.automatalib.incremental.dfa.Acceptance;
34	import net.automatalib.util.graph.traversal.GraphTraversal;
35	import net.automatalib.visualization.VisualizationHelper;
36	import net.automatalib.visualization.helper.DelegateVisualizationHelper;
37	import net.automatalib.word.Word;
38	import net.automatalib.word.WordBuilder;
39	import org.checkerframework.checker.nullness.qual.NonNull;
40	import org.checkerframework.checker.nullness.qual.Nullable;
41
42	/**
43	* Incrementally builds a tree, from a set of positive and negative words. Using {@link #insert(Word, boolean)}, either
44	* the set of words definitely in the target language or definitely <i>not</i> in the target language is augmented. The
45	* {@link #lookup(Word)} method then returns, for a given word, whether this word is in the set of definitely accepted
46	* words ({@link Acceptance#TRUE}), definitely rejected words ({@link Acceptance#FALSE}), or neither ({@link
47	* Acceptance#DONT_KNOW}).
48	*
49	* @param <I>
50	* input symbol class
51	*/
52	public class IncrementalDFATreeBuilder<I> extends AbstractIncrementalDFABuilder<I> {
53
54	protected final Node root;
55
56	public IncrementalDFATreeBuilder(Alphabet<I> inputAlphabet) {
57	super(inputAlphabet);	2✔
58	this.root = new Node();	2✔
59	}	2✔
60
61	@Override
62	public void addAlphabetSymbol(I symbol) {
63	if (!this.inputAlphabet.containsSymbol(symbol)) {	2✔
64	Alphabets.toGrowingAlphabetOrThrowException(this.inputAlphabet).addSymbol(symbol);	2✔
65	}
66
67	final int newAlphabetSize = this.inputAlphabet.size();	2✔
68	// even if the symbol was already in the alphabet, we need to make sure to be able to store the new symbol
69	if (alphabetSize < newAlphabetSize) {	2✔
70	ensureInputCapacity(root, alphabetSize, newAlphabetSize);	2✔
71	alphabetSize = newAlphabetSize;	2✔
72	}
73	}	2✔
74
75	private void ensureInputCapacity(Node node, int oldAlphabetSize, int newAlphabetSize) {
76	node.ensureInputCapacity(newAlphabetSize);	2✔
77	for (int i = 0; i < oldAlphabetSize; i++) {	2✔
78	final Node child = node.getChild(i);	2✔
79	if (child != null) {	2✔
80	ensureInputCapacity(child, oldAlphabetSize, newAlphabetSize);	2✔
81	}
82	}
83	}	2✔
84
85	@Override
86	public @Nullable Word<I> findSeparatingWord(DFA<?, I> target,
87	Collection<? extends I> inputs,
88	boolean omitUndefined) {
89	return doFindSeparatingWord(target, inputs, omitUndefined);	2✔
90	}
91
92	protected <S> @Nullable Word<I> doFindSeparatingWord(DFA<S, I> target,
93	Collection<? extends I> inputs,
94	boolean omitUndefined) {
95	S automatonInit = target.getInitialState();	2✔
96
97	if (automatonInit == null) {	2✔
98	return omitUndefined ? null : Word.epsilon();	2✔
99	}
100
101	if (root.getAcceptance().conflicts(target.isAccepting(automatonInit))) {	2✔
102	return Word.epsilon();	×
103	}
104
105	// incomingInput can be null here, because we will always skip the bottom stack element below
106	@SuppressWarnings("nullness")
107	Record<@Nullable S, I> init = new Record<>(automatonInit, root, null, inputs.iterator());	2✔
108
109	Deque<Record<@Nullable S, I>> dfsStack = new ArrayDeque<>();	2✔
110	dfsStack.push(init);	2✔
111
112	while (!dfsStack.isEmpty()) {	2✔
113	@SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
114	@NonNull Record<@Nullable S, I> rec = dfsStack.peek();	2✔
115	if (!rec.inputIt.hasNext()) {	2✔
116	dfsStack.pop();	2✔
117	continue;	2✔
118	}
119	I input = rec.inputIt.next();	2✔
120	int inputIdx = inputAlphabet.getSymbolIndex(input);	2✔
121
122	Node succ = rec.treeNode.getChild(inputIdx);	2✔
123	if (succ == null) {	2✔
124	continue;	2✔
125	}
126
127	@Nullable S state = rec.automatonState;	2✔
128	@Nullable S automatonSucc = state == null ? null : target.getTransition(state, input);	2✔
129	if (automatonSucc == null && omitUndefined) {	2✔
130	continue;	2✔
131	}
132
133	boolean succAcc = automatonSucc != null && target.isAccepting(automatonSucc);	2✔
134
135	if (succ.getAcceptance().conflicts(succAcc)) {	2✔
136	WordBuilder<I> wb = new WordBuilder<>(dfsStack.size());	2✔
137	wb.append(input);	2✔
138
139	dfsStack.pop();	2✔
140	while (!dfsStack.isEmpty()) {	2✔
141	wb.append(rec.incomingInput);	2✔
142	rec = dfsStack.pop();	2✔
143	}
144	return wb.reverse().toWord();	2✔
145	}
146
147	dfsStack.push(new Record<>(automatonSucc, succ, input, inputs.iterator()));	2✔
148	}	2✔
149
150	return null;	2✔
151	}
152
153	@Override
154	public Acceptance lookup(Word<? extends I> inputWord) {
155	Node curr = root;	2✔
156
157	for (I sym : inputWord) {	2✔
158	int symIdx = inputAlphabet.getSymbolIndex(sym);	2✔
159	Node succ = curr.getChild(symIdx);	2✔
160	if (succ == null) {	2✔
161	return Acceptance.DONT_KNOW;	2✔
162	}
163	curr = succ;	2✔
164	}	2✔
165	return curr.getAcceptance();	2✔
166	}
167
168	@Override
169	public void insert(Word<? extends I> word, boolean acceptance) {
170	Node curr = root;	2✔
171
172	for (I sym : word) {	2✔
173	int inputIdx = inputAlphabet.getSymbolIndex(sym);	2✔
174	Node succ = curr.getChild(inputIdx);	2✔
175	if (succ == null) {	2✔
176	succ = new Node();	2✔
177	curr.setChild(inputIdx, alphabetSize, succ);	2✔
178	}
179	curr = succ;	2✔
180	}	2✔
181
182	Acceptance acc = curr.getAcceptance();	2✔
183	Acceptance newWordAcc = Acceptance.fromBoolean(acceptance);	2✔
184	if (acc == Acceptance.DONT_KNOW) {	2✔
185	curr.setAcceptance(newWordAcc);	2✔
186	} else if (acc != newWordAcc) {	2✔
187	throw new ConflictException(	2✔
188	"Conflicting acceptance values for word " + word + ": " + acc + " vs " + newWordAcc);
189	}
190	}	2✔
191
192	@Override
193	public GraphView asGraph() {
194	return new GraphView();	2✔
195	}
196
197	@Override
198	public TransitionSystemView asTransitionSystem() {
199	return new TransitionSystemView();	2✔
200	}
201
202	protected static final class Record<S, I> {
203
204	public final S automatonState;
205	public final Node treeNode;
206	public final I incomingInput;
207	public final Iterator<? extends I> inputIt;
208
209	public Record(S automatonState, Node treeNode, I incomingInput, Iterator<? extends I> inputIt) {	2✔
210	this.automatonState = automatonState;	2✔
211	this.treeNode = treeNode;	2✔
212	this.incomingInput = incomingInput;	2✔
213	this.inputIt = inputIt;	2✔
214	}	2✔
215	}
216
217	public class GraphView extends AbstractGraphView<I, Node, Edge<I>> {	2✔
218
219	@Override
220	public Collection<Node> getNodes() {
221	List<Node> result = new ArrayList<>();	2✔
222	Iterators.addAll(result, GraphTraversal.depthFirstIterator(this, Collections.singleton(root)));	2✔
223	return result;	2✔
224	}
225
226	@Override
227	public Collection<Edge<I>> getOutgoingEdges(Node node) {
228	List<Edge<I>> result = new ArrayList<>(alphabetSize);	2✔
229	for (int i = 0; i < alphabetSize; i++) {	2✔
230	Node succ = node.getChild(i);	2✔
231	if (succ != null) {	2✔
232	result.add(new Edge<>(succ, inputAlphabet.getSymbol(i)));	2✔
233	}
234	}
235	return result;	2✔
236	}
237
238	@Override
239	public Node getTarget(Edge<I> edge) {
240	return edge.getNode();	2✔
241	}
242
243	@Override
244	public I getInputSymbol(Edge<I> edge) {
245	return edge.getInput();	2✔
246	}
247
248	@Override
249	public Acceptance getAcceptance(Node node) {
250	return node.getAcceptance();	2✔
251	}
252
253	@Override
254	public Node getInitialNode() {
255	return root;	2✔
256	}
257
258	@Override
259	public VisualizationHelper<Node, Edge<I>> getVisualizationHelper() {
260	return new DelegateVisualizationHelper<Node, Edge<I>>(super.getVisualizationHelper()) {	2✔
261
262	private int id;
263
264	@Override
265	public boolean getNodeProperties(Node node, Map<String, String> properties) {
266	if (!super.getNodeProperties(node, properties)) {	2✔
267	return false;	×
268	}
269	properties.put(NodeAttrs.LABEL, "n" + (id++));	2✔
270	return true;	2✔
271	}
272	};
273	}
274	}
275
276	public class TransitionSystemView extends AbstractTransitionSystemView<Node, I, Node> {	2✔
277
278	@Override
279	public Node getSuccessor(Node transition) {
280	return transition;	2✔
281	}
282
283	@Override
284	public @Nullable Node getTransition(Node state, I input) {
285	int inputIdx = inputAlphabet.getSymbolIndex(input);	2✔
286	return state.getChild(inputIdx);	2✔
287	}
288
289	@Override
290	public Node getInitialState() {
291	return root;	2✔
292	}
293
294	@Override
295	public Acceptance getStateProperty(Node state) {
296	return state.getAcceptance();	2✔
297	}
298	}
299
300	}

LearnLib / automatalib / 6654683895

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