Add error prone support and perform code cleanups

.mvn/jvm.config

@@ -0,0 +1,10 @@
+--add-exports jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED
+--add-exports jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED
+--add-opens jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED
+--add-opens jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED

pom.xml

@@ -110,6 +110,7 @@
         <checker-qual.version>3.53.1</checker-qual.version>
         <commons-lang.version>3.20.0</commons-lang.version>
         <gson.version>2.13.2</gson.version>
+        <error-prone.version>2.48.0</error-prone.version>
         <guava.version>33.5.0-jre</guava.version>
         <jakarta-xml.version>4.0.5</jakarta-xml.version>
         <jaxb-runtime.version>4.0.6</jaxb-runtime.version>
@@ -250,8 +251,19 @@
                 <configuration>
                     <showWarnings>true</showWarnings>
                     <compilerArgs>
-                         <arg>-Xlint:deprecation</arg>
+                        <arg>-Xlint:deprecation</arg>
+                        <arg>-XDcompilePolicy=simple</arg>
+                        <arg>--should-stop=ifError=FLOW</arg>
+                        <arg>-XDaddTypeAnnotationsToSymbol=true</arg>
+                        <arg>-Xplugin:ErrorProne -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:StringConcatToTextBlock:OFF</arg>
                     </compilerArgs>
+                    <annotationProcessorPaths>
+                        <path>
+                            <groupId>com.google.errorprone</groupId>
+                            <artifactId>error_prone_core</artifactId>
+                            <version>${error-prone.version}</version>
+                        </path>
+                    </annotationProcessorPaths>
                 </configuration>
             </plugin>
 

src/main/java/de/learnlib/ralib/automata/Assignment.java

@@ -43,6 +43,12 @@ public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment)
         this.assignment = assignment;
     }
 
+    /**
+     * Updates the register valuation {@code registers} based on register assignment.
+     * Any registers in {@code registers} which are not assigned to a new register will be dropped.
+     *
+     * @return the new valuation
+     */
     public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
     	RegisterValuation val = new RegisterValuation();
     	for (Map.Entry<Register, ? extends SymbolicDataValue> e : assignment.entrySet()) {
@@ -60,8 +66,8 @@ public RegisterValuation valuation(RegisterValuation registers, ParameterValuati
     	return val;
     }
 
-    /*
-     * @deprecated method is unsafe, use {@link #valuation()} instead
+    /**
+     * Deprecated and unsafe method; use {@link de.learnlib.ralib.automata.Assignment#valuation(RegisterValuation, ParameterValuation, Constants) Valuation} instead.
      * Method is unsafe because it keeps registers that are not given a new assignment, which can cause
      * a discrepancy in the number of registers a location has, depending on the path to the location.
      * Method is deprecated rather than removed because the functionality is used by XML automata models.
@@ -82,12 +88,6 @@ public RegisterValuation compute(RegisterValuation registers, ParameterValuation
                 val.put(e.getKey(), registers.get((Register) valp));
             }
             else if (valp.isParameter()) {
-            	DataValue dv = parameters.get((Parameter) valp);
-            	for (Map.Entry<Parameter, DataValue> ep : parameters.entrySet()) {
-            		if (ep.getKey().equals(valp)) {
-            			dv = ep.getValue();
-            		}
-            	}
                 val.put(e.getKey(), parameters.get((Parameter) valp));
             }
             //TODO: check if we want to copy constant values into vars

src/main/java/de/learnlib/ralib/automata/RARun.java

@@ -72,8 +72,8 @@ public Expression<Boolean> getGuard(int i) {
 		if (transition == null) {
 			return null;
 		}
-		return transition instanceof OutputTransition ?
-				outputGuard((OutputTransition) transition) :
+		return transition instanceof OutputTransition outputTransition ?
+				outputGuard(outputTransition) :
 					transition.getGuard();
 	}
 

src/main/java/de/learnlib/ralib/automata/Transition.java

@@ -53,12 +53,15 @@ public boolean isEnabled(RegisterValuation registers, ParameterValuation paramet
         return guard.evaluateSMT(SMTUtil.compose(registers, parameters, consts));
     }
 
+    /**
+     * @return the valuation
+     */
     public RegisterValuation valuation(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
     	return this.getAssignment().valuation(registers, parameters, consts);
     }
 
-    /*
-     * @deprecated method is unsafe, use {@link #valuation()} instead
+    /**
+     * Deprecated and unsafe method; use {@link de.learnlib.ralib.automata.Transition#valuation(RegisterValuation, ParameterValuation, Constants) Valuation} instead.
      * Method is unsafe because it keeps registers that are not given a new assignment, which can cause
      * a discrepancy in the number of registers a location has, depending on the path to the location.
      * Method is deprecated rather than removed because the functionality is used by XML automata models.

src/main/java/de/learnlib/ralib/automata/util/RAToDot.java

@@ -77,7 +77,7 @@ private void printLocations(RegisterAutomaton ra) {
             if (!acceptingOnly || loc.isAccepting()) {
                 printLocation(loc);
                 stringRA.append(" [shape=");
-                stringRA.append( (loc.isAccepting()) ? "doublecircle" : "circle");
+                stringRA.append(loc.isAccepting() ? "doublecircle" : "circle");
                 stringRA.append("]");
                 stringRA.append(NEWLINE);
             }
@@ -106,8 +106,8 @@ private void printTransitions(RegisterAutomaton ra) {
                 printLocation(t.getDestination());
                 stringRA.append(" [label=<");
 
-                if (t instanceof OutputTransition) {
-                    printOutputLabel( (OutputTransition)t );
+                if (t instanceof OutputTransition outputTransition) {
+                    printOutputLabel( outputTransition );
                 } else {
                     printInputLabel( t );
                 }

src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java

@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014-2015 The LearnLib Contributors
+ * Copyright (C) 2014-2025 The LearnLib Contributors
  * This file is part of LearnLib, http://www.learnlib.de/.
  *
  * Licensed under the Apache License, Version 2.0 (the "License");
@@ -87,11 +87,11 @@ private static RegisterAutomaton.Alphabet.Inputs exportInputs(Collection<InputSy
         for (InputSymbol input : is) {
             RegisterAutomaton.Alphabet.Inputs.Symbol s = factory.createRegisterAutomatonAlphabetInputsSymbol();
             s.setName(input.getName());
-            int idx=1;
+            int idx = 1;
             for (DataType t : input.getPtypes()) {
                 RegisterAutomaton.Alphabet.Inputs.Symbol.Param param =
                         factory.createRegisterAutomatonAlphabetInputsSymbolParam();
-                param.setName("p" + (idx++));
+                param.setName("p" + idx++);
                 param.setType(t.getName());
                 s.getParam().add(param);
             }
@@ -105,11 +105,11 @@ private static RegisterAutomaton.Alphabet.Outputs exportOutputs(Collection<Outpu
         for (OutputSymbol output : os) {
             RegisterAutomaton.Alphabet.Outputs.Symbol s = factory.createRegisterAutomatonAlphabetOutputsSymbol();
             s.setName(output.getName());
-            int idx=1;
+            int idx = 1;
             for (DataType t : output.getPtypes()) {
                 RegisterAutomaton.Alphabet.Outputs.Symbol.Param param =
                         factory.createRegisterAutomatonAlphabetOutputsSymbolParam();
-                param.setName("p" + (idx++));
+                param.setName("p" + idx++);
                 param.setType(t.getName());
                 s.getParam().add(param);
             }
@@ -130,7 +130,7 @@ private static RegisterAutomaton.Locations exportLocations(
             if (ra.getInitialState().equals(loc)) {
                 l.setInitial("true");
             }
-            ret.getLocation()   .add(l);
+            ret.getLocation().add(l);
         }
         return ret;
     }
@@ -140,11 +140,11 @@ private static RegisterAutomaton.Transitions exportTransitions(Collection<Transi
                 factory.createRegisterAutomatonTransitions();
 
         for (Transition t : trans) {
-            if (t instanceof OutputTransition) {
-                ret.getTransition().add( exportOutputTransition( (OutputTransition)t, tmp ));
+            if (t instanceof OutputTransition outputTransition) {
+                ret.getTransition().add( exportOutputTransition(outputTransition, tmp));
             }
             else {
-                ret.getTransition().add( exportInputTransition( t ));
+                ret.getTransition().add(exportInputTransition(t));
             }
         }
         return ret;
@@ -272,10 +272,9 @@ public static void write(de.learnlib.ralib.automata.RegisterAutomaton ra, Consta
         Set<OutputSymbol> outputs = new HashSet<>();
         for (Transition t : ra.getTransitions()) {
             ParameterizedSymbol ps = t.getLabel();
-            if (ps instanceof InputSymbol) {
-                inputs.add((InputSymbol)ps);
-            }
-            else {
+            if (ps instanceof InputSymbol inputSymbol) {
+                inputs.add(inputSymbol);
+            } else {
                 outputs.add((OutputSymbol) ps);
             }
         }

src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java

@@ -18,11 +18,11 @@
 
 import java.io.InputStream;
 import java.math.BigDecimal;
+import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashSet;
 import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
-import java.util.LinkedList;
 import java.util.List;
 import java.util.ListIterator;
 import java.util.Map;
@@ -118,7 +118,7 @@ private void loadModel(InputStream is) {
         }
 
         // determine input/output locations
-        List<RegisterAutomaton.Transitions.Transition> transitions = new LinkedList<>(a.getTransitions().getTransition());
+        List<RegisterAutomaton.Transitions.Transition> transitions = new ArrayList<>(a.getTransitions().getTransition());
         while(!transitions.isEmpty()) {
             ListIterator<Transition> iter = transitions.listIterator();
             while (iter.hasNext()) {
@@ -185,7 +185,7 @@ else if (constMap.containsKey(ass.value)) {
             Assignment assign = new Assignment(assignments);
 
             // output
-            if (ps instanceof OutputSymbol) {
+            if (ps instanceof OutputSymbol outputSymbol) {
 
                 Parameter[] pList = paramList(ps);
                 int idx = 0;
@@ -223,7 +223,7 @@ else if (constMap.containsKey(ass.value)) {
                 OutputMapping outMap = new OutputMapping(fresh, outputs);
 
                 OutputTransition tOut = new OutputTransition(p, outMap,
-                        (OutputSymbol) ps, from, to, assign);
+                        outputSymbol, from, to, assign);
                 iora.addTransition(from, ps, tOut);
                 LOGGER.trace(Category.EVENT, "Loading: {}", tOut);
             } // input
@@ -321,10 +321,6 @@ private DataType getOrCreateType(String name) {
         return t;
     }
 
-    private boolean isDoubleTempCheck(String name) {
-        return name.equals("DOUBLE") || name.equals("double");
-    }
-
     private Map<String, SymbolicDataValue> buildValueMap(
             Map<String, ? extends SymbolicDataValue> ... maps) {
         Map<String, SymbolicDataValue> ret = new LinkedHashMap<>();

src/main/java/de/learnlib/ralib/ceanalysis/Essentializer.java

@@ -16,8 +16,10 @@
  */
 package de.learnlib.ralib.ceanalysis;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.LinkedList;
+import java.util.List;
 
 import de.learnlib.ralib.data.DataValue;
 import de.learnlib.ralib.oracles.DataWordOracle;
@@ -46,7 +48,7 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
         final Word<ParameterizedSymbol> acts = DataWords.actsOf(in);
         DataValue[] vals = DataWords.valsOf(in);
 
-        IDX: for (int index=vals.length-1; index>=0; index--) {
+        IDX: for (int index = vals.length-1; index >= 0; index--) {
             final DataValue v = vals[index];
             final LinkedList<Integer> indices = indexesOf(vals, v);
             // is index unique or first?
@@ -67,8 +69,8 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
                 Integer[] sublist = subListFrom(indices, index);
                 // TODO: special case implementation for equalities
                 // TODO: use theory / sdt construction instead
-                for (int c=0; c<(1<<sublist.length)-1; c++) {
-                    for (int i=0; i<sublist.length; i++) {
+                for (int c = 0; c < (1<<sublist.length)-1; c++) {
+                    for (int i = 0; i < sublist.length; i++) {
                         vals[sublist[i]] = (c & (1<<i)) == 0 ? fresh : v;
                     }
                     instantiated = DataWords.instantiate(acts, vals);
@@ -77,7 +79,7 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
                         continue IDX;
                     }
                 }
-                for (int i=0; i<sublist.length; i++) {
+                for (int i = 0; i < sublist.length; i++) {
                     vals[sublist[i]] = v;
                 }
             }
@@ -86,8 +88,9 @@ public Word<PSymbolInstance> essentialEq(Word<PSymbolInstance> in) {
         return DataWords.instantiate(acts, vals);
     }
 
+    @SuppressWarnings("NonApiType")
     private Integer[] subListFrom(LinkedList<Integer> list, Integer i) {
-        LinkedList<Integer> sublist = new LinkedList<>();
+        List<Integer> sublist = new ArrayList<>();
         for (Integer index : list) {
             if (index > i) {
                 sublist.add(index);
@@ -96,9 +99,10 @@ private Integer[] subListFrom(LinkedList<Integer> list, Integer i) {
         return sublist.toArray(new Integer[] {});
     }
 
+    @SuppressWarnings({"NonApiType", "JdkObsolete"})
     private LinkedList<Integer> indexesOf(DataValue[] vals, DataValue v) {
         LinkedList<Integer> list = new LinkedList<>();
-        for (int i=0; i< vals.length; i++) {
+        for (int i = 0; i < vals.length; i++) {
             if (vals[i].equals(v)) {
                 list.add(i);
             }

src/main/java/de/learnlib/ralib/ceanalysis/PrefixFinder.java

@@ -3,6 +3,7 @@
 import java.util.ArrayList;
 import java.util.Iterator;
 import java.util.LinkedHashSet;
+import java.util.List;
 import java.util.Map;
 import java.util.Optional;
 import java.util.Set;
@@ -187,7 +188,7 @@ private Set<Mapping<DataValue, DataValue>> extendedValuationRenamings(SDT uSDT,
 		DataValue[] sdtValsArr = sdtVals.toArray(new DataValue[sdtVals.size()]);
 
 		// gather data values from prefix of run at index id
-		ArrayList<DataValue> runVals = new ArrayList<>();
+		List<DataValue> runVals = new ArrayList<>();
 		for (int i = 1; i <= id-1; i++) {
 			for (DataValue d : run.getTransitionSymbol(i).getParameterValues()) {
 				runVals.add(d);
@@ -230,7 +231,7 @@ private Set<Mapping<DataValue, DataValue>> extendedValuationRenamings(SDT uSDT,
 	 * @param d
 	 * @return array containing data values of {@code list}, with one occurrence of {@code d} removed
 	 */
-	private ArrayList<DataValue> removeFirst(ArrayList<DataValue> list, DataValue d) {
+	private List<DataValue> removeFirst(List<DataValue> list, DataValue d) {
 		ArrayList<DataValue> ret = new ArrayList<>();
 		ret.addAll(list);
 		for (int i = 0; i < list.size(); i++) {

src/main/java/de/learnlib/ralib/ct/CTAutomatonBuilder.java

@@ -203,7 +203,7 @@ private Transition createTransition(ParameterizedSymbol action, Expression<Boole
 			return null;
 		}
 
-		if (!ioMode || !(action instanceof OutputSymbol)) {
+		if (!ioMode || !(action instanceof OutputSymbol outputSymbol)) {
 			// create input transition
 			return new Transition(action, guard, src_loc, dest_loc, assignment);
 		}
@@ -227,7 +227,7 @@ private Transition createTransition(ParameterizedSymbol action, Expression<Boole
         OutputMapping outMap = new OutputMapping(fresh, outmap);
 
         return new OutputTransition(ExpressionUtil.TRUE,
-                outMap, (OutputSymbol) action, src_loc, dest_loc, assignment);
+                outMap, outputSymbol, src_loc, dest_loc, assignment);
 	}
 
 
@@ -247,12 +247,12 @@ else if (expr instanceof NumericBooleanExpression nbe) {
                 Parameter p = null;
                 SymbolicDataValue sv = null;
 
-                if (left instanceof Parameter) {
+                if (left instanceof Parameter pleft) {
                     if (right instanceof Parameter) {
                         throw new UnsupportedOperationException("not implemented yet.");
                     }
                     else {
-                        p = (Parameter) left;
+                        p = pleft;
                         sv = right;
                     }
                 }