fix issues reported by checkerframework

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/ApartnessUtil.java

@@ -17,6 +17,7 @@
 
 import java.util.ArrayDeque;
 import java.util.Deque;
+import java.util.Objects;
 
 import net.automatalib.automaton.transducer.MealyMachine;
 import net.automatalib.common.util.Pair;
@@ -137,7 +138,7 @@ public static <S extends Comparable<S>, I, O> boolean accStatesAreApart(Observat
                     S fstD = fstOD.getSecond();
                     O sndO = sndOD.getFirst();
                     S sndD = sndOD.getSecond();
-                    if (fstO.equals(sndO)) {
+                    if (Objects.equals(fstO, sndO)) {
                         workList.push(Pair.of(fstD, sndD));
                     } else {
                         return fstD;

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/LSOracle.java

@@ -29,6 +29,7 @@
 import net.automatalib.common.util.Pair;
 import net.automatalib.word.Word;
 import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 public class LSOracle<I, O> {
@@ -37,15 +38,15 @@ public class LSOracle<I, O> {
     private final NormalObservationTree<I, O> obsTree;
     private final Rule2 rule2;
     private final Rule3 rule3;
-    private Word<I> sinkState;
+    private @MonotonicNonNull Word<I> sinkState;
     private final O sinkOutput;
     private final Random random;
 
     public LSOracle(AdaptiveMembershipOracle<I, O> sul,
                     NormalObservationTree<I, O> obsTree,
                     Rule2 rule2,
                     Rule3 rule3,
-                    Word<I> sinkState,
+                    @Nullable Word<I> sinkState,
                     O sinkOutput,
                     Random random) {
         this.sul = sul;
@@ -107,7 +108,7 @@ private Pair<Word<I>, Word<O>> rule3IO(List<Word<I>> candidates, Word<I> prefix)
             case SEPSEQ:
                 List<Integer> withS = getSuccs(randomN(candidates, 2));
                 Word<I> wit = ApartnessUtil.computeWitness(obsTree, withS.get(0), withS.get(1));
-
+                assert wit != null;
                 Word<I> inputSeq = prefix.concat(wit);
                 return Pair.of(inputSeq, this.outputQuery(inputSeq));
             default:
@@ -118,7 +119,9 @@ private Pair<Word<I>, Word<O>> rule3IO(List<Word<I>> candidates, Word<I> prefix)
     private List<Integer> getSuccs(List<Word<I>> candidates) {
         List<Integer> result = new ArrayList<>(candidates.size());
         for (Word<I> c : candidates) {
-            result.add(obsTree.getSucc(obsTree.defaultState(), c));
+            Integer succ = obsTree.getSucc(obsTree.defaultState(), c);
+            assert succ != null;
+            result.add(succ);
         }
         return result;
     }
@@ -154,12 +157,13 @@ private Pair<Word<I>, Word<O>> rule2IO(Word<I> accessQ, I i, List<Integer> bss,
                 Word<O> oSeq = this.outputQuery(prefix);
                 return Pair.of(prefix, oSeq);
             case SEPSEQ:
-                Word<I> wit = Word.epsilon();
+                Word<I> wit;
                 if (basis.size() >= 2) {
                     List<Integer> ran = getSuccs(randomN(basis, 2));
-                    assert ran.get(0) != null;
-                    assert ran.get(1) != null;
                     wit = ApartnessUtil.computeWitness(obsTree, ran.get(0), ran.get(1));
+                    assert wit != null;
+                } else {
+                     wit = Word.epsilon();
                 }
                 Word<I> inputSeq = accessQ.append(i).concat(wit);
                 Word<O> outputSeq = this.outputQuery(inputSeq);
@@ -216,15 +220,15 @@ public Word<O> outputQuery(Word<I> inputSeq) {
         sul.processQuery(query);
         out = query.getOutput();
 
-        if (sinkState == null && out.lastSymbol().equals(sinkOutput)) {
+        if (sinkState == null && Objects.equals(out.lastSymbol(), sinkOutput)) {
             sinkState = inputSeq;
         }
 
         this.addObservation(inputSeq, out);
         return out;
     }
 
-    public Pair<Word<I>, Word<O>> adaptiveOutputQuery(Word<I> prefix, I infix, ADSTree<Integer, I, O> suffix) {
+    public Pair<Word<I>, Word<O>> adaptiveOutputQuery(Word<I> prefix, @Nullable I infix, ADSTree<Integer, I, O> suffix) {
         return this.adaptiveOutputQuery(infix != null ? prefix.append(infix) : prefix, suffix);
     }
 
@@ -268,7 +272,6 @@ public Pair<Word<I>, Word<O>> adaptiveOutputQuery(Word<I> prefix, ADSTree<Intege
         while (nextInput.isPresent()) {
             I i = nextInput.get();
             inputsSent.add(i);
-            @Nullable
             Pair<O, Integer> pair = obsTree.getOutSucc(currState, i);
             if (pair == null) {
                 return null;
@@ -331,7 +334,7 @@ public Response processOutput(O out) {
             }
         }
 
-        private Response computeNext(O out) {
+        private Response computeNext(@Nullable O out) {
             final Optional<I> next = ads.nextInput(out);
             if (next.isPresent()) {
                 adsSym = next.get();

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/LSharpMealy.java

@@ -44,25 +44,12 @@ public class LSharpMealy<I, O> implements MealyLearner<I, O> {
     private final Map<Word<I>, Integer> basisMap;
     private final ArrayStorage<Word<I>> accessMap;
 
-    public LSharpMealy(Alphabet<I> alphabet, AdaptiveMembershipOracle<I, O> oracle, Rule2 rule2, Rule3 rule3) {
-        this(alphabet, oracle, rule2, rule3, null, null);
-    }
-
-    public LSharpMealy(Alphabet<I> alphabet,
-                       AdaptiveMembershipOracle<I, O> oracle,
-                       Rule2 rule2,
-                       Rule3 rule3,
-                       Word<I> sinkState,
-                       O sinkOutput) {
-        this(alphabet, oracle, rule2, rule3, sinkState, sinkOutput, new Random());
-    }
-
     @GenerateBuilder(defaults = BuilderDefaults.class)
     public LSharpMealy(Alphabet<I> alphabet,
                        AdaptiveMembershipOracle<I, O> oracle,
                        Rule2 rule2,
                        Rule3 rule3,
-                       Word<I> sinkState,
+                       @Nullable Word<I> sinkState,
                        O sinkOutput,
                        Random random) {
         this.oqOracle = new LSOracle<>(oracle,
@@ -97,11 +84,12 @@ public void processBinarySearch(Word<I> ceInput, Word<O> ceOutput, MealyMachine<
         Integer r = oqOracle.getTree().getSucc(oqOracle.getTree().defaultState(), ceInput);
         assert r != null;
         this.updateFrontierAndBasis();
-        if (this.frontierToBasisMap.containsKey(ceInput) || basis.contains(ceInput)) {
+        Integer init = mealy.getInitialState();
+        if (this.frontierToBasisMap.containsKey(ceInput) || basis.contains(ceInput) || init == null) {
             return;
         }
 
-        Integer q = mealy.getSuccessor(mealy.getInitialState(), ceInput);
+        Integer q = mealy.getSuccessor(init, ceInput);
         assert q != null;
         Word<I> accQT = accessMap.get(q);
         assert accQT != null;
@@ -124,7 +112,7 @@ public void processBinarySearch(Word<I> ceInput, Word<O> ceOutput, MealyMachine<
 
         Word<I> sigma1 = ceInput.prefix(h);
         Word<I> sigma2 = ceInput.suffix(ceInput.size() - h);
-        Integer qp = mealy.getSuccessor(mealy.getInitialState(), sigma1);
+        Integer qp = mealy.getSuccessor(init, sigma1);
         assert qp != null;
         Word<I> accQPt = accessMap.get(qp);
         assert accQPt != null;
@@ -140,7 +128,6 @@ public void processBinarySearch(Word<I> ceInput, Word<O> ceOutput, MealyMachine<
         Integer rp = oTree.getSucc(oTree.defaultState(), sigma1);
         assert rp != null;
 
-        @Nullable
         Word<I> wit = ApartnessUtil.computeWitness(oTree, qpt, rp);
         if (wit != null) {
             processBinarySearch(sigma1, ceOutput.prefix(sigma1.length()), mealy);
@@ -212,7 +199,7 @@ public boolean treeIsAdequate() {
 
         for (Pair<Word<I>, I> p : basisIpPairs) {
             Integer q = oTree.getSucc(oTree.defaultState(), p.getFirst());
-            if (oTree.getOut(q, p.getSecond()) == null) {
+            if (q == null || oTree.getOut(q, p.getSecond()) == null) {
                 return false;
             }
         }
@@ -276,8 +263,9 @@ public Pair<Word<I>, Boolean> identifyFrontierOrBasis(Word<I> seq) {
             return Pair.of(seq, false);
         }
 
-        Word<I> bs = frontierToBasisMap.get(seq).get(0);
-        return Pair.of(bs, true);
+        List<Word<I>> frontier = frontierToBasisMap.get(seq);
+        assert frontier != null;
+        return Pair.of(frontier.get(0), true);
     }
 
     public void initObsTree(@Nullable List<Pair<Word<I>, Word<O>>> logs) {
@@ -309,9 +297,8 @@ public void checkFrontierConsistency() {
         }
     }
 
-    public DefaultQuery<I, Word<O>> checkConsistency(MealyMachine<Integer, I, ?, O> mealy) {
+    public @Nullable DefaultQuery<I, Word<O>> checkConsistency(MealyMachine<Integer, I, ?, O> mealy) {
         NormalObservationTree<I, O> oTree = oqOracle.getTree();
-        @Nullable
         Word<I> wit = ApartnessUtil.treeAndHypComputeWitness(oTree, oTree.defaultState(), mealy, 0);
         if (wit == null) {
             return null;
@@ -353,11 +340,19 @@ private BuilderDefaults() {
             // prevent instantiation
         }
 
-        public static <I> Word<I> sinkState() {
+        public static Rule2 rule2() {
+            return Rule2.ADS;
+        }
+
+        public static Rule3 rule3() {
+            return Rule3.ADS;
+        }
+
+        public static <I> @Nullable Word<I> sinkState() {
             return null;
         }
 
-        public static <O> O sinkOutput() {
+        public static <O> @Nullable O sinkOutput() {
             return null;
         }
 

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/MapTransitions.java

@@ -25,7 +25,7 @@ public class MapTransitions<I, O> implements TransitionInformation<I, O> {
 
     private final Map<I, Pair<O, Integer>> trans;
 
-    public MapTransitions(Integer inSize) {
+    public MapTransitions(int inSize) {
         trans = new HashMap<>(inSize);
     }
 

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/NormalObservationTree.java

@@ -44,22 +44,21 @@ public Integer defaultState() {
         return 0;
     }
 
-    private Integer addTransitionGetDestination(Integer src, I i, O o) {
-        int srcRaw = src;
-        Pair<O, Integer> pair = this.tree.get(srcRaw).getOutSucc(i);
+    private int addTransitionGetDestination(int src, I i, O o) {
+        Pair<O, Integer> pair = this.tree.get(src).getOutSucc(i);
 
         if (pair != null) {
             return pair.getSecond();
         } else {
-            int destState = this.tree.nodeWithParent(new MapTransitions<>(this.inputAlphabet.size()), srcRaw, i);
-            this.tree.arena.get(srcRaw).value.addTrans(i, o, destState);
+            int destState = this.tree.nodeWithParent(new MapTransitions<>(this.inputAlphabet.size()), src, i);
+            this.tree.arena.get(src).value.addTrans(i, o, destState);
             return destState;
         }
     }
 
     @Override
     public Integer insertObservation(@Nullable Integer s, Word<I> input, Word<O> output) {
-        Integer curr = s == null ? defaultState() : s;
+        int curr = s == null ? defaultState() : s;
 
         int max = Math.min(input.length(), output.length());
         for (int i = 0; i < max; i++) {
@@ -85,6 +84,7 @@ public Word<I> getTransferSeq(Integer toState, Integer fromState) {
 
         while (true) {
             Pair<I, Integer> pair = this.tree.arena.get(currState).parent;
+            assert pair != null;
             I i = pair.getFirst();
             Integer parentIndex = pair.getSecond();
             accessSeq.add(i);
@@ -119,7 +119,7 @@ public Word<I> getTransferSeq(Integer toState, Integer fromState) {
         return this.tree.get(src).getOutSucc(input);
     }
 
-    Integer getSucc(Integer state, I input) {
+    private @Nullable Integer getSucc(Integer state, I input) {
         Pair<O, Integer> pair = getOutSucc(state, input);
         return pair == null ? null : pair.getSecond();
     }

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/ObservationTree.java

@@ -30,11 +30,9 @@ public interface ObservationTree<S extends Comparable<S>, I, O> {
 
     Word<I> getTransferSeq(S toState, S fromState);
 
-    @Nullable
-    Word<O> getObservation(@Nullable S start, Word<I> input);
+    @Nullable Word<O> getObservation(@Nullable S start, Word<I> input);
 
-    @Nullable
-    Pair<O, S> getOutSucc(S src, I input);
+    @Nullable Pair<O, S> getOutSucc(S src, I input);
 
     default @Nullable O getOut(S src, I input) {
         Pair<O, S> out = this.getOutSucc(src, input);
@@ -45,8 +43,7 @@ public interface ObservationTree<S extends Comparable<S>, I, O> {
         return out.getFirst();
     }
 
-    @Nullable
-    S getSucc(S src, Word<I> input);
+    @Nullable S getSucc(S src, Word<I> input);
 
     Alphabet<I> getInputAlphabet();
 

algorithms/active/lsharp/src/main/java/de/learnlib/algorithm/lsharp/ads/ADSNode.java

@@ -27,12 +27,10 @@ public class ADSNode<I, O> {
     private final int score;
 
     public ADSNode() {
-        this.input = null;
-        this.children = new HashMap<>();
-        this.score = 0;
+        this(null, new HashMap<>(), 0);
     }
 
-    public ADSNode(I input, Map<O, ADSNode<I, O>> children, int score) {
+    public ADSNode(@Nullable I input, Map<O, ADSNode<I, O>> children, int score) {
         this.input = input;
         this.children = children;
         this.score = score;