some more cleanups

* Simplified the VPDA State class
* Streamlined generics on CanonicalWordComparator
* CheckerFramework cleanups

CHANGELOG.md

@@ -15,6 +15,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 * We overhauled the handling of input and output streams for all (de-)serializers. Input and output streams are no longer closed automatically. This is to prevent asymmetric code where we would close a stream that we haven't opened. This is problematic in cases where e.g. `System.out` is passed as an output stream to simply print a serialized automaton and the `System.out` stream would be closed afterwards. Since input and output streams are usually opened in client-code, they should be closed in client-code as well. We suggest to simply wrap calls to the serializers in a try-with-resource block.
 * Due to the DOT parsers rewrite (see **Fixed**), the attribute parsers now receive a `Map<String, String>` instead of a `Map<String, Object>`.
+* The `State` class (used by the `OneSEVPA` automaton) not longer supports the notion of a sink state. The `AbstractOneSEVPA` class now conforms with the default semantics of a `DeterministicTransitionSystem` that undefined transitions simply return `null`.
 
 
 ### Removed

api/src/main/java/net/automatalib/automata/vpda/State.java

@@ -15,9 +15,7 @@
  */
 package net.automatalib.automata.vpda;
 
-import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.qual.Pure;
 
 /**
  * Utility class to combine an entity (e.g. a location) with stack information.
@@ -29,39 +27,19 @@
  */
 public final class State<L> {
 
-    private static final State<?> SINK = new State<>();
-    private final @Nullable L loc;
+    private final L loc;
     private final @Nullable StackContents stack;
 
-    private State() {
-        this.loc = null;
-        this.stack = null;
-    }
-
     public State(final L loc, final @Nullable StackContents stack) {
         this.loc = loc;
         this.stack = stack;
     }
 
-    @SuppressWarnings("unchecked")
-    @Pure
-    public static <L> State<L> getSink() {
-        return (State<L>) SINK;
-    }
-
-    @Pure
-    public @Nullable L getLocation() {
+    public L getLocation() {
         return loc;
     }
 
-    @Pure
     public @Nullable StackContents getStackContents() {
         return stack;
     }
-
-    @EnsuresNonNullIf(expression = {"getLocation()"}, result = false)
-    @Pure
-    public boolean isSink() {
-        return getLocation() == null;
-    }
 }

api/src/main/java/net/automatalib/words/CanonicalWordComparator.java

@@ -19,7 +19,7 @@
 
 import net.automatalib.commons.util.comparison.CmpUtil;
 
-class CanonicalWordComparator<I> implements Comparator<Word<? extends I>> {
+class CanonicalWordComparator<I> implements Comparator<Word<I>> {
 
     private final Comparator<? super I> symComparator;
 
@@ -28,7 +28,7 @@ class CanonicalWordComparator<I> implements Comparator<Word<? extends I>> {
     }
 
     @Override
-    public int compare(Word<? extends I> o1, Word<? extends I> o2) {
+    public int compare(Word<I> o1, Word<I> o2) {
         int ldiff = o1.length() - o2.length();
         if (ldiff != 0) {
             return ldiff;

api/src/main/java/net/automatalib/words/Word.java

@@ -84,7 +84,7 @@ public abstract class Word<I> extends AbstractPrintable implements ArrayWritable
         WORD_SYMBOL_DELIM_RIGHT = settings.getProperty(AutomataLibProperty.WORD_SYMBOL_DELIM_RIGHT, "");
     }
 
-    public static <I> Comparator<Word<? extends I>> canonicalComparator(Comparator<? super I> symComparator) {
+    public static <I> Comparator<Word<I>> canonicalComparator(Comparator<? super I> symComparator) {
         return new CanonicalWordComparator<>(symComparator);
     }
 

build-parent/pom.xml

@@ -249,8 +249,14 @@ limitations under the License.
                                     </annotationProcessors>
                                     <compilerArgs>
                                         <arg>-J-Xbootclasspath/p:${com.google.errorprone:javac:jar}</arg>
-                                        <arg>-AskipDefs=net\.automatalib\.(serialization\.taf\.parser|serialization\.dot|modelcheckers\.ltsmin)\.(Internal.*|Token.*|SimpleCharStream)</arg> <!-- generated classes -->
-                                        <arg>-AskipUses=^com\.google|^java\.(awt|util\.Arrays|io\.StreamTokenizer)|^javax\.swing</arg>
+                                        <arg>-AskipDefs=^net.automatalib.serialization.taf.parser.(Internal.*|Token.*|SimpleCharStream)|\
+                                                        ^net.automatalib.serialization.dot.(Internal.*|Token.*|SimpleCharStream)|\
+                                                        ^net.automatalib.modelcheckers.ltsmin.(Internal.*|Token.*|SimpleCharStream)|\
+                                        </arg>
+                                        <arg>-AskipUses=^com.google.*|\
+                                                        ^java.(awt.*|util.Arrays|io.StreamTokenizer)|\
+                                                        ^javax.swing.*|\
+                                        </arg>
                                         <arg>-AsuppressWarnings=uninitialized</arg>
                                         <arg>-AassumeAssertionsAreEnabled</arg>
                                         <arg>-Astubs=jdk8.astub:collection-object-parameters-may-be-null.astub</arg>

core/src/main/java/net/automatalib/automata/vpda/AbstractOneSEVPA.java

@@ -25,6 +25,7 @@
 import net.automatalib.visualization.DefaultVisualizationHelper;
 import net.automatalib.visualization.VisualizationHelper;
 import net.automatalib.words.VPDAlphabet;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * Abstract class for 1-SEVPAs that implements functionality shared across different subtypes.
@@ -49,11 +50,7 @@ public VPDAlphabet<I> getAlphabet() {
     }
 
     @Override
-    public State<L> getTransition(final State<L> state, final I input) {
-        if (state.isSink()) {
-            return State.getSink();
-        }
-
+    public @Nullable State<L> getTransition(final State<L> state, final I input) {
         final L loc = state.getLocation();
         final VPDAlphabet.SymbolType type = alphabet.getSymbolType(input);
         switch (type) {
@@ -63,19 +60,19 @@ public State<L> getTransition(final State<L> state, final I input) {
             case RETURN: {
                 final StackContents contents = state.getStackContents();
                 if (contents == null) {
-                    return State.getSink();
+                    return null;
                 }
                 final int stackElem = contents.peek();
                 final L succ = getReturnSuccessor(loc, input, stackElem);
                 if (succ == null) {
-                    return State.getSink();
+                    return null;
                 }
                 return new State<>(succ, contents.pop());
             }
             case INTERNAL: {
                 final L succ = getInternalSuccessor(loc, input);
                 if (succ == null) {
-                    return State.getSink();
+                    return null;
                 }
                 return new State<>(succ, state.getStackContents());
             }

serialization/taf/src/main/java/net/automatalib/serialization/taf/writer/TAFWriter.java

@@ -192,7 +192,6 @@ private void writeStringCollection(Collection<?> symbols) throws IOException {
         if (symbols.isEmpty()) {
             out.append("{}");
         } else if (symbols.size() == 1) {
-            @SuppressWarnings("nullness") // the above 'if' guarantees the existence of the element
             Object sym = symbols.iterator().next();
             StringUtil.enquoteIfNecessary(String.valueOf(sym), out, ID_PATTERN);
         } else {

util/src/main/java/net/automatalib/util/automata/conformance/IncrementalWMethodTestsIterator.java

@@ -162,16 +162,16 @@ public Item<I> merge(Item<I> oldObject, Item<I> newObject) {
 
     }
 
-    private static final class ItemComparator<I> implements Comparator<Item<? extends I>> {
+    private static final class ItemComparator<I> implements Comparator<Item<I>> {
 
-        private final Comparator<? super Word<? extends I>> canonicalCmp;
+        private final Comparator<Word<I>> canonicalCmp;
 
         ItemComparator(Comparator<? super I> symComparator) {
             this.canonicalCmp = Word.canonicalComparator(symComparator);
         }
 
         @Override
-        public int compare(Item<? extends I> o1, Item<? extends I> o2) {
+        public int compare(Item<I> o1, Item<I> o2) {
             int cmp = canonicalCmp.compare(o1.middle, o2.middle);
             if (cmp != 0) {
                 return cmp;

visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTFrame.java

@@ -52,8 +52,9 @@ public void actionPerformed(ActionEvent e) {
                 DOTFrame.this.dispatchEvent(new WindowEvent(DOTFrame.this, WindowEvent.WINDOW_CLOSING));
             }
         });
-        setJMenuBar(new JMenuBar());
-        getJMenuBar().add(menu);
+        JMenuBar jMenuBar = new JMenuBar();
+        jMenuBar.add(menu);
+        setJMenuBar(jMenuBar);
 
         setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
         pack();

visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTPanel.java

@@ -35,6 +35,8 @@
 import javax.swing.JPanel;
 import javax.swing.JScrollPane;
 
+import org.checkerframework.checker.initialization.qual.UnknownInitialization;
+import org.checkerframework.checker.nullness.qual.RequiresNonNull;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -46,34 +48,11 @@ public class DOTPanel extends JPanel {
     private final ImageComponent imgComponent;
     private final JList<PlottedGraph> listBox;
     private final DefaultListModel<PlottedGraph> graphs;
-    private final Action saveDotAction = new AbstractDisabledAction("Save DOT") {
 
-        @Override
-        public void actionPerformed(ActionEvent e) {
-            saveDOT();
-        }
-    };
-    private final Action savePngAction = new AbstractDisabledAction("Save PNG") {
-
-        @Override
-        public void actionPerformed(ActionEvent e) {
-            savePNG();
-        }
-    };
-    private final Action renameAction = new AbstractDisabledAction("Rename") {
-
-        @Override
-        public void actionPerformed(ActionEvent e) {
-            rename();
-        }
-    };
-    private final Action clearAction = new AbstractAction("Clear") {
-
-        @Override
-        public void actionPerformed(ActionEvent e) {
-            clear();
-        }
-    };
+    private final Action saveDotAction;
+    private final Action savePngAction;
+    private final Action renameAction;
+    private final Action clearAction;
 
     public DOTPanel() {
         setLayout(new GridBagLayout());
@@ -95,6 +74,36 @@ public DOTPanel() {
         c.gridheight = 1;
         this.graphs = new DefaultListModel<>();
         listBox = new JList<>(graphs);
+
+        saveDotAction = new AbstractDisabledAction("Save DOT") {
+
+            @Override
+            public void actionPerformed(ActionEvent e) {
+                saveDOT();
+            }
+        };
+        savePngAction = new AbstractDisabledAction("Save PNG") {
+
+            @Override
+            public void actionPerformed(ActionEvent e) {
+                savePNG();
+            }
+        };
+        renameAction = new AbstractDisabledAction("Rename") {
+
+            @Override
+            public void actionPerformed(ActionEvent e) {
+                rename();
+            }
+        };
+        clearAction = new AbstractAction("Clear") {
+
+            @Override
+            public void actionPerformed(ActionEvent e) {
+                clear();
+            }
+        };
+
         listBox.addListSelectionListener(e -> {
             int idx = listBox.getSelectedIndex();
             boolean activeSelection = (idx != -1);
@@ -137,7 +146,8 @@ public Action getClearAction() {
         return clearAction;
     }
 
-    public void saveDOT() {
+    @RequiresNonNull("listBox")
+    public void saveDOT(@UnknownInitialization(JPanel.class) DOTPanel this) {
         PlottedGraph pg = listBox.getSelectedValue();
         if (pg == null) {
             JOptionPane.showMessageDialog(this,
@@ -162,7 +172,8 @@ public void saveDOT() {
         }
     }
 
-    public void savePNG() {
+    @RequiresNonNull("listBox")
+    public void savePNG(@UnknownInitialization(JPanel.class) DOTPanel this) {
         PlottedGraph pg = listBox.getSelectedValue();
         if (pg == null) {
             JOptionPane.showMessageDialog(this,
@@ -203,11 +214,13 @@ public void addGraph(String name, Reader dotText) throws IOException {
         graphs.addElement(pg);
     }
 
-    public void clear() {
+    @RequiresNonNull("graphs")
+    public void clear(@UnknownInitialization(JPanel.class) DOTPanel this) {
         graphs.clear();
     }
 
-    public void rename() {
+    @RequiresNonNull("listBox")
+    public void rename(@UnknownInitialization(JPanel.class) DOTPanel this) {
         PlottedGraph pg = listBox.getSelectedValue();
         if (pg == null) {
             JOptionPane.showMessageDialog(this,

visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/ImageComponent.java

@@ -59,10 +59,13 @@ public void actionPerformed(ActionEvent e) {
                 return;
             }
             File f = chooser.getSelectedFile();
+            if (img == null) {
+                throw new IllegalStateException("No image has been set");
+            }
+            if (f == null) {
+                throw new IllegalStateException("No file has been selected");
+            }
             try {
-                if (img == null) {
-                    throw new IllegalStateException("No image has been set");
-                }
                 ImageIO.write(img, "png", f);
             } catch (IOException ex) {
                 JOptionPane.showMessageDialog(ImageComponent.this,