add initial checkerframework integration

* cleanup annotations and dependency definitions
* add initial checker configuration

Author: mtf90

algorithms/active/adt/pom.xml

@@ -34,7 +34,7 @@ limitations under the License.
     </description>
 
     <dependencies>
-        <!-- LearnLib dependencies -->
+        <!-- internal -->
         <dependency>
             <groupId>de.learnlib</groupId>
             <artifactId>learnlib-api</artifactId>
@@ -48,7 +48,7 @@ limitations under the License.
             <artifactId>learnlib-util</artifactId>
         </dependency>
 
-        <!-- AutomataLib dependencies -->
+        <!-- external -->
         <dependency>
             <groupId>net.automatalib</groupId>
             <artifactId>automata-api</artifactId>
@@ -66,49 +66,46 @@ limitations under the License.
             <artifactId>automata-commons-util</artifactId>
         </dependency>
 
-        <dependency>
-            <groupId>com.github.misberner.buildergen</groupId>
-            <artifactId>buildergen</artifactId>
-        </dependency>
         <dependency>
             <groupId>org.checkerframework</groupId>
             <artifactId>checker-qual</artifactId>
         </dependency>
 
-        <!--
-        Test dependencies
-        -->
-
-        <!-- TestNG -->
+        <!-- build -->
         <dependency>
-            <groupId>org.testng</groupId>
-            <artifactId>testng</artifactId>
+            <groupId>com.github.misberner.buildergen</groupId>
+            <artifactId>buildergen</artifactId>
         </dependency>
 
+        <!-- test -->
         <dependency>
-            <groupId>de.learnlib.testsupport</groupId>
-            <artifactId>learnlib-learning-examples</artifactId>
+            <groupId>de.learnlib</groupId>
+            <artifactId>learnlib-drivers-simulator</artifactId>
+            <scope>test</scope>
         </dependency>
-
         <dependency>
             <groupId>de.learnlib.testsupport</groupId>
             <artifactId>learnlib-learner-it-support</artifactId>
         </dependency>
-
         <dependency>
-            <groupId>de.learnlib</groupId>
-            <artifactId>learnlib-drivers-simulator</artifactId>
-            <scope>test</scope>
+            <groupId>de.learnlib.testsupport</groupId>
+            <artifactId>learnlib-learning-examples</artifactId>
         </dependency>
         <dependency>
             <groupId>de.learnlib</groupId>
             <artifactId>learnlib-membership-oracles</artifactId>
             <scope>test</scope>
         </dependency>
+
         <dependency>
             <groupId>net.automatalib</groupId>
             <artifactId>automata-serialization-dot</artifactId>
             <scope>test</scope>
         </dependency>
+
+        <dependency>
+            <groupId>org.testng</groupId>
+            <artifactId>testng</artifactId>
+        </dependency>
     </dependencies>
 </project>

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/ads/DefensiveADS.java

@@ -36,6 +36,8 @@
 import net.automatalib.util.automata.ads.ADSUtil;
 import net.automatalib.words.Alphabet;
 import net.automatalib.words.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * A variant of the backtracking ADS search (see {@link net.automatalib.util.automata.ads.ADS}, {@link
@@ -60,11 +62,11 @@ public final class DefensiveADS<S, I, O> {
     /**
      * The states, whose outgoing {@link #refinementInput}-transitions need to be closed.
      */
-    private Set<S> refinementStates;
+    private @Nullable Set<S> refinementStates;
     /**
      * The output for which the outgoing transitions of {@link #refinementStates} are undefined.
      */
-    private I refinementInput;
+    private @Nullable I refinementInput;
 
     private DefensiveADS(final MealyMachine<S, I, ?, O> automaton,
                          final Alphabet<I> alphabet,
@@ -145,7 +147,8 @@ private Optional<ADTNode<S, I, O>> compute(final Map<S, S> mapping) {
         candidateLoop:
         while (!splittingWordCandidates.isEmpty()) {
 
-            final Word<I> prefix = splittingWordCandidates.poll();
+            @SuppressWarnings("nullness") // false positive https://github.com/typetools/checker-framework/issues/399
+            final @NonNull Word<I> prefix = splittingWordCandidates.poll();
             final Map<S, S> currentToInitialMapping = mapping.keySet()
                                                              .stream()
                                                              .collect(Collectors.toMap(x -> automaton.getSuccessor(x,

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/adt/ADTResetNode.java

@@ -21,6 +21,7 @@
 
 import de.learnlib.api.oracle.SymbolQueryOracle;
 import net.automatalib.words.Word;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * Reset node implementation.
@@ -36,15 +37,15 @@
  */
 public class ADTResetNode<S, I, O> implements ADTNode<S, I, O>, Serializable {
 
-    final ADTNode<S, I, O> successor;
-    ADTNode<S, I, O> parent;
+    private final ADTNode<S, I, O> successor;
+    private ADTNode<S, I, O> parent;
 
     public ADTResetNode(final ADTNode<S, I, O> successor) {
         this.successor = successor;
     }
 
     @Override
-    public I getSymbol() {
+    public @Nullable I getSymbol() {
         return null;
     }
 
@@ -69,7 +70,7 @@ public Map<O, ADTNode<S, I, O>> getChildren() {
     }
 
     @Override
-    public S getHypothesisState() {
+    public @Nullable S getHypothesisState() {
         return null;
     }
 

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/adt/ADTSymbolNode.java

@@ -61,7 +61,7 @@ public NodeType getNodeType() {
 
     @Override
     public String toString() {
-        return super.getSymbol().toString();
+        return String.valueOf(super.getSymbol());
     }
 
 }

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/automaton/ADTHypothesis.java

@@ -21,8 +21,6 @@
 import net.automatalib.automata.transducers.MutableMealyMachine;
 import net.automatalib.words.Alphabet;
 import net.automatalib.words.Word;
-import org.checkerframework.checker.nullness.qual.NonNull;
-import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * Hypothesis model.
@@ -41,13 +39,11 @@ public ADTHypothesis(final Alphabet<I> alphabet) {
         super(alphabet);
     }
 
-    @NonNull
     @Override
     public ADTState<I, O> getSuccessor(final ADTTransition<I, O> transition) {
         return transition.getTarget();
     }
 
-    @NonNull
     public ADTTransition<I, O> createOpenTransition(final ADTState<I, O> source,
                                                     final I input,
                                                     final ADTNode<ADTState<I, O>, I, O> siftTarget) {
@@ -82,31 +78,31 @@ protected ADTState<I, O> createState(final Void property) {
         return new ADTState<>(inputAlphabet.size());
     }
 
-    @NonNull
     @Override
-    public ADTTransition<I, O> createTransition(final ADTState<I, O> successor, @Nullable final O properties) {
+    public ADTTransition<I, O> createTransition(final ADTState<I, O> successor, final O properties) {
         ADTTransition<I, O> result = new ADTTransition<>();
         result.setTarget(successor);
         result.setOutput(properties);
         return result;
     }
 
     @Override
-    public void setTransitionOutput(final ADTTransition<I, O> transition, @Nullable final O output) {
+    public void setTransitionOutput(final ADTTransition<I, O> transition, final O output) {
         transition.setOutput(output);
     }
 
-    @Nullable
     @Override
     public O getTransitionOutput(final ADTTransition<I, O> transition) {
         return transition.getOutput();
     }
 
+    @SuppressWarnings("nullness") // hypothesis is always complete
     @Override
     public Word<I> transformAccessSequence(final Word<I> word) {
         return this.getState(word).getAccessSequence();
     }
 
+    @SuppressWarnings("nullness") // hypothesis is always complete
     @Override
     public boolean isAccessSequence(final Word<I> word) {
         return this.getState(word).getAccessSequence().equals(word);

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/config/LeafSplitters.java

@@ -17,6 +17,7 @@
 
 import java.util.Iterator;
 import java.util.Map;
+import java.util.Objects;
 
 import de.learnlib.algorithms.adt.adt.ADTLeafNode;
 import de.learnlib.algorithms.adt.adt.ADTNode;
@@ -118,7 +119,7 @@ private static <S, I, O> ADTNode<S, I, O> finalizeSplit(final ADTNode<S, I, O> n
         O oldOut = oldIter.next();
         O newOut = newIter.next();
 
-        while (oldOut.equals(newOut)) {
+        while (Objects.equals(oldOut, newOut)) {
             final ADTNode<S, I, O> next = new ADTSymbolNode<>(previous, suffixIter.next());
 
             previous.getChildren().put(oldOut, next);

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/config/model/extender/DefaultExtender.java

@@ -17,6 +17,7 @@
 
 import java.util.HashMap;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Optional;
 import java.util.Set;
 import java.util.function.Function;
@@ -88,7 +89,7 @@ public <I, O> ExtensionResult<ADTState<I, O>, I, O> computeExtension(final ADTHy
                             partialTransitionAnalyzer.closeTransition(s, input);
                         }
 
-                        if (!hypothesis.getOutput(s, input).equals(output)) {
+                        if (!Objects.equals(hypothesis.getOutput(s, input), output)) {
                             final ADTState<I, O> initial = entry.getValue();
                             final Word<I> as = initial.getAccessSequence();
                             final Word<O> asOut = hypothesis.computeOutput(as);

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/learner/ADTLearner.java

@@ -62,7 +62,6 @@
 import net.automatalib.words.Word;
 import net.automatalib.words.WordBuilder;
 import net.automatalib.words.impl.Alphabets;
-import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * The main learning algorithm.
@@ -280,7 +279,6 @@ public boolean refineHypothesisInternal(DefaultQuery<I, Word<O>> ceQuery) {
         return true;
     }
 
-    @NonNull
     @Override
     public MealyMachine<?, I, ?, O> getHypothesisModel() {
         return this.hypothesis;

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/model/ExtensionResult.java

@@ -19,6 +19,7 @@
 import de.learnlib.algorithms.adt.api.ADTExtender;
 import de.learnlib.api.query.DefaultQuery;
 import net.automatalib.words.Word;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * A class that describes the possible result a {@link ADTExtender} can return. Extending a parent trace can either <ul>
@@ -39,9 +40,8 @@ public class ExtensionResult<S, I, O> {
 
     private static final ExtensionResult<?, ?, ?> EMPTY = new ExtensionResult();
 
-    private final DefaultQuery<I, Word<O>> counterExample;
-
-    private final ADTNode<S, I, O> replacement;
+    private final @Nullable DefaultQuery<I, Word<O>> counterExample;
+    private final @Nullable ADTNode<S, I, O> replacement;
 
     private ExtensionResult() {
         this.replacement = null;
@@ -89,7 +89,7 @@ public boolean isCounterExample() {
      *
      * @return the counterexample
      */
-    public DefaultQuery<I, Word<O>> getCounterExample() {
+    public @Nullable DefaultQuery<I, Word<O>> getCounterExample() {
         return counterExample;
     }
 
@@ -107,7 +107,7 @@ public boolean isReplacement() {
      *
      * @return the replacement
      */
-    public ADTNode<S, I, O> getReplacement() {
+    public @Nullable ADTNode<S, I, O> getReplacement() {
         return replacement;
     }
 }

algorithms/active/adt/src/main/java/de/learnlib/algorithms/adt/model/ObservationTree.java

@@ -19,6 +19,7 @@
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Optional;
 import java.util.function.Function;
 
@@ -130,7 +131,7 @@ private FastMealyState<O> addTrace(final FastMealyState<O> state, final Word<I>
                 nextState = this.observationTree.addState();
                 this.observationTree.addTransition(iter, nextInput, nextState, nextOuput);
             } else {
-                assert this.observationTree.getOutput(iter, nextInput).equals(nextOuput) : "Inconsistent observations";
+                assert Objects.equals(nextOuput, this.observationTree.getOutput(iter, nextInput)) : "Inconsistent observations";
                 nextState = this.observationTree.getSuccessor(iter, nextInput);
             }