Clean up CF definitions (#101)

* initial refactoring

* some more cleanups

* cleanups

Author: mtf90

api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java

@@ -65,8 +65,9 @@ protected Collection<Pair<I, S>> initialNodes() {
 
         for (Entry<I, UniversalDeterministicAutomaton<S, I, ?, ?, ?>> e : subModels.entrySet()) {
             final S init = e.getValue().getInitialState();
-            assert init != null;
-            initialNodes.add(Pair.of(e.getKey(), init));
+            if (init != null) {
+                initialNodes.add(Pair.of(e.getKey(), init));
+            }
         }
 
         return initialNodes;

build-config/src/main/resources/automatalib-spotbugs-exclusions.xml

@@ -35,14 +35,21 @@ limitations under the License.
     </Match>
     <Match>
         <Bug pattern="NP_NULL_ON_SOME_PATH_FROM_RETURN_VALUE"/>
-        <And>
-            <!-- Fine according to JavaDoc -->
-            <Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
-            <Or>
-                <Method name="popBack" returns="java.lang.Object"/>
-                <Method name="popFront" returns="java.lang.Object"/>
-            </Or>
-        </And>
+        <Or>
+            <And>
+                <!-- Fine according to data-flow -->
+                <Class name="net.automatalib.util.automaton.ads.LeeYannakakis"/>
+                <Method name="computeValidities"/>
+            </And>
+            <And>
+                <!-- Fine according to JavaDoc -->
+                <Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
+                <Or>
+                    <Method name="popBack" returns="java.lang.Object"/>
+                    <Method name="popFront" returns="java.lang.Object"/>
+                </Or>
+            </And>
+        </Or>
     </Match>
     <Match>
         <!-- Passing references is mostly fine for performance reasons. Since we do not deal with security-related code,

build-parent/pom.xml

@@ -240,7 +240,6 @@ limitations under the License.
                                     <goal>compile</goal>
                                 </goals>
                                 <configuration>
-                                    <failOnWarning>true</failOnWarning>
                                     <fork>true</fork>
                                     <outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
                                     <annotationProcessorPaths combine.children="append">
@@ -273,7 +272,6 @@ limitations under the License.
                                         </arg>
                                         <arg>-AskipUses=^java.(awt.*|util.(Arrays|Map|ArrayDeque)|io.StreamTokenizer)|^javax.swing.*</arg>
                                         <arg>-AsuppressWarnings=uninitialized</arg>
-                                        <arg>-AassumeAssertionsAreEnabled</arg>
                                         <arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
                                     </compilerArgs>
                                 </configuration>
@@ -285,7 +283,6 @@ limitations under the License.
                                     <goal>testCompile</goal>
                                 </goals>
                                 <configuration>
-                                    <failOnWarning>true</failOnWarning>
                                     <fork>true</fork>
                                     <outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
                                     <annotationProcessorPaths combine.children="append">
@@ -311,7 +308,6 @@ limitations under the License.
                                         <arg>-AonlyDefs=^net\.automatalib</arg>
                                         <arg>-AskipUses=.*</arg>
                                         <arg>-AsuppressWarnings=uninitialized</arg>
-                                        <arg>-AassumeAssertionsAreEnabled</arg>
                                         <arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
                                     </compilerArgs>
                                 </configuration>

commons/smartcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java

@@ -36,6 +36,7 @@ public class ReflexiveMapView<T> extends AbstractMap<T, T> {
 
     private final Set<@KeyFor("this") T> domain;
 
+    @SuppressWarnings("type") // the provided items become keys for this map view
     public ReflexiveMapView(Set<T> domain) {
         this.domain = Collections.unmodifiableSet(domain);
     }
@@ -68,6 +69,7 @@ public boolean containsKey(@Nullable Object key) {
     }
 
     @Override
+    @SuppressWarnings("return") // it is okay that values are also keys for this map
     public Set<T> values() {
         return this.domain;
     }

core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java

@@ -32,6 +32,7 @@
 import net.automatalib.symbol.time.TimedInput;
 import net.automatalib.symbol.time.TimedOutput;
 import net.automatalib.symbol.time.TimeoutSymbol;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -132,8 +133,9 @@ public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> so
                 }
             }
 
-            assert lastOutput != null;
-            return new MealyTransition<>(currentConfig, new TimedOutput<>(lastOutput));
+            @SuppressWarnings("nullness") // since remainingTime must be > 0, the while loop iterates at least once
+            final @NonNull O output = lastOutput;
+            return new MealyTransition<>(currentConfig, new TimedOutput<>(output));
         } else {
             throw new IllegalArgumentException("Unknown input symbol type");
         }

core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java

@@ -50,7 +50,7 @@ public StackSPA(ProceduralInputAlphabet<I> alphabet,
     }
 
     @Override
-    public StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
+    public @Nullable StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
         if (state.isTerm()) {
             return null;
         } else if (alphabet.isInternalSymbol(input)) {

core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java

@@ -15,7 +15,6 @@
  */
 package net.automatalib.automaton.procedural.impl;
 
-import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -54,21 +53,25 @@ StackState<S, I, P> push(P newProcedure, S newState) {
         return new StackState<>(this, newProcedure, newState);
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     StackState<S, I, P> pop() {
         assert !isStatic() : "This method should never be called on static states";
         return prev;
     }
 
+    @SuppressWarnings("type") // since this method is package-private, we are happy to only assert nullability
     StackState<S, I, P> updateState(S state) {
         assert !isStatic() : "This method should never be called on static states";
         return new StackState<>(prev, procedure, state);
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     P getProcedure() {
         assert !isStatic() : "This method should never be called on static states";
         return procedure;
     }
 
+    @SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
     S getCurrentState() {
         assert !isStatic() : "This method should never be called on static states";
         return procedureState;
@@ -92,9 +95,6 @@ boolean isTerm() {
         return this == TERM;
     }
 
-    // contract is satisfied by definition of constructors
-    @SuppressWarnings("contracts.conditional.postcondition")
-    @EnsuresNonNullIf(expression = {"this.prev", "this.procedure", "this.procedureState"}, result = false)
     private boolean isStatic() {
         return isInit() || isTerm();
     }

examples/src/main/java/net/automatalib/example/graph/DFSExample.java

@@ -30,6 +30,7 @@
 import net.automatalib.visualization.Visualization;
 import net.automatalib.visualization.VisualizationHelper;
 import net.automatalib.visualization.VisualizationHelper.EdgeStyles;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * A small example of a {@link GraphTraversal graph traversal} that uses a custom {@link GraphTraversalVisitor} to
@@ -168,16 +169,16 @@ static class DFSResultDOTHelper<N, E> implements VisualizationHelper<N, E> {
         @Override
         public boolean getNodeProperties(N node, Map<String, String> properties) {
             String lbl = properties.get(NodeAttrs.LABEL);
-            DFSData record = records.get(node);
-            assert record != null;
+            @SuppressWarnings("nullness") // we have traversed all nodes before
+            @NonNull DFSData record = records.get(node);
             properties.put(NodeAttrs.LABEL, lbl + " [#" + record.dfsNumber + "]");
             return true;
         }
 
         @Override
         public boolean getEdgeProperties(N src, E edge, N tgt, Map<String, String> properties) {
-            EdgeType et = edgeTypes.get(edge);
-            assert et != null;
+            @SuppressWarnings("nullness") // we have traversed all nodes before
+            @NonNull EdgeType et = edgeTypes.get(edge);
             properties.put(EdgeAttrs.STYLE, et.getStyle());
             properties.remove(EdgeAttrs.LABEL);
             return true;

incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java

@@ -23,6 +23,7 @@
 import net.automatalib.incremental.ConflictException;
 import net.automatalib.incremental.dfa.Acceptance;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
@@ -74,7 +75,6 @@ public Acceptance lookup(Word<? extends I> word) {
      */
     @Override
     public void insert(Word<? extends I> word, boolean accepting) {
-        int len = word.length();
         Acceptance acc = Acceptance.fromBoolean(accepting);
 
         State curr = init;
@@ -99,6 +99,7 @@ public void insert(Word<? extends I> word, boolean accepting) {
             curr = succ;
         }
 
+        int len = word.length();
         int prefixLen = path.size();
 
         State last = curr;
@@ -139,8 +140,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
                 // confluence always requires cloning, to separate this path from other paths
                 last = hiddenClone(last);
                 if (conf == null) {
-                    Transition peek = path.peek();
-                    assert peek != null;
+                    // the root node is never confluent so in this context, the path always contains at least one node
+                    @SuppressWarnings("nullness")
+                    @NonNull Transition peek = path.peek();
                     State prev = peek.state;
                     if (prev == init) {
                         updateInitSignature(peek.transIdx, last);

incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java

@@ -23,6 +23,7 @@
 import net.automatalib.incremental.ConflictException;
 import net.automatalib.incremental.dfa.Acceptance;
 import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * The prefix-closed version of {@link IncrementalDFADAGBuilder}. Contrary to the regular lookup semantics, where an
@@ -145,8 +146,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
                 }
                 last = hiddenClone(last);
                 if (conf == null) {
-                    Transition peek = path.peek();
-                    assert peek != null;
+                    // the root node is never confluent so in this context, the path always contains at least one node
+                    @SuppressWarnings("nullness")
+                    @NonNull Transition peek = path.peek();
                     State prev = peek.state;
                     if (prev == init) {
                         updateInitSignature(peek.transIdx, last);