From 10ce25a7c137fb2ed3b78e7ef73a04885ee94245 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:13:55 +0100 Subject: [PATCH 01/16] WIP: Add error prone plugin support --- .mvn/jvm.config | 10 ++++++++++ pom.xml | 13 ++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) create mode 100644 .mvn/jvm.config diff --git a/.mvn/jvm.config b/.mvn/jvm.config new file mode 100644 index 00000000..32599cef --- /dev/null +++ b/.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 diff --git a/pom.xml b/pom.xml index 19ccb2de..173af346 100644 --- a/pom.xml +++ b/pom.xml @@ -110,6 +110,7 @@ 3.52.1 3.20.0 2.13.2 + 2.45.0 33.5.0-jre 4.0.4 4.0.6 @@ -250,8 +251,18 @@ true - -Xlint:deprecation + -Xlint:deprecation + -XDcompilePolicy=simple + --should-stop=ifError=FLOW + -Xplugin:ErrorProne -Xep:AlmostJavadoc:OFF -Xep:MissingOverride:OFF -Xep:RedundantControlFlow:OFF -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EffectivelyPrivate:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:UnnecessaryParentheses:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:BoxedPrimitiveEquality:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + + + com.google.errorprone + error_prone_core + ${error-prone.version} + + From 87dd367d760a8cdaf84ea0df5ad59bb75cdd6326 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:16:31 +0100 Subject: [PATCH 02/16] Fix an erroneous Javadoc comment --- .../de/learnlib/ralib/theory/equality/EqualityTheory.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java b/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java index 8c55ef5d..c5deec80 100644 --- a/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java +++ b/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.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"); @@ -390,7 +390,7 @@ private Word buildQuery(Word prefix, SymbolicS return query; } - /* + /** * Creates a "unary tree" of depth maxIndex - nextSufIndex which leads to a * rejecting Leaf. Edges are of type {@link SDTTrueGuard}. Used to shortcut * output processing. From 885625e2697d0878e12458003c05447b9922568b Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:19:21 +0100 Subject: [PATCH 03/16] Add missing Override annotations --- src/main/java/de/learnlib/ralib/data/Bijection.java | 1 + .../de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java | 1 + 2 files changed, 2 insertions(+) diff --git a/src/main/java/de/learnlib/ralib/data/Bijection.java b/src/main/java/de/learnlib/ralib/data/Bijection.java index 3c4c5d39..303c2473 100644 --- a/src/main/java/de/learnlib/ralib/data/Bijection.java +++ b/src/main/java/de/learnlib/ralib/data/Bijection.java @@ -123,6 +123,7 @@ public Mapping toVarMapping() { return vars; } + @Override public String toString() { return injection.toString(); } diff --git a/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java b/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java index 8c92883e..5aea1e21 100644 --- a/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java +++ b/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java @@ -69,6 +69,7 @@ public DoubleInequalityTheory(DataType t) { this.type = t; } + @Override public NativeZ3Solver getSolver() { return (NativeZ3Solver) solver; } From 27cc78b80b4d2af9b2175fb9628c861f8a496fbd Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:23:09 +0100 Subject: [PATCH 04/16] Remove a redundant control flow continue statement --- .../learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java b/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java index 6997f19b..d74cf0ea 100644 --- a/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java +++ b/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java @@ -225,7 +225,6 @@ protected Map mergeGuards(Map sdts, currMerged = null; prevGuard = null; prevSdt = null; - continue; } else { boolean keepMerging = true; SDTGuard nextGuard = equivClasses.get(nextDv); From c188333c6383c9d2ccec71bbebeba44003caea4f Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:26:02 +0100 Subject: [PATCH 05/16] Fix an erroneous boxed primitive equality comparison --- src/main/java/de/learnlib/ralib/theory/SDT.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/de/learnlib/ralib/theory/SDT.java b/src/main/java/de/learnlib/ralib/theory/SDT.java index f05ac7f8..388282b7 100644 --- a/src/main/java/de/learnlib/ralib/theory/SDT.java +++ b/src/main/java/de/learnlib/ralib/theory/SDT.java @@ -439,7 +439,7 @@ public boolean isEquivalentUnderCondition(SDT other, Expression conditi Expression x = entry.getKey(); Boolean outcome = entry.getValue(); for (Map.Entry, Boolean> otherEntry : otherExpressions.entrySet()) { - if (outcome != otherEntry.getValue()) { + if (!outcome.equals(otherEntry.getValue())) { Expression otherX = otherEntry.getKey(); Expression renamed = ExpressionUtil.and(otherX, condition); Expression con = ExpressionUtil.and(x, renamed); From fc2726fd31f1abd0ccf6e497944439248c341fb9 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Mon, 22 Dec 2025 22:29:14 +0100 Subject: [PATCH 06/16] Remove public from methods which are effectively private --- pom.xml | 2 +- .../ralib/equivalence/IOCounterexampleLoopRemover.java | 2 +- .../learnlib/ralib/equivalence/IOEquivalenceTest.java | 10 +++++----- .../learnlib/ralib/equivalence/RAEquivalenceTest.java | 4 ++-- .../de/learnlib/ralib/dt/RegisterConsistencyTest.java | 4 ++-- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/pom.xml b/pom.xml index 173af346..9c7351ae 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:AlmostJavadoc:OFF -Xep:MissingOverride:OFF -Xep:RedundantControlFlow:OFF -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EffectivelyPrivate:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:UnnecessaryParentheses:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:BoxedPrimitiveEquality:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:UnnecessaryParentheses:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/main/java/de/learnlib/ralib/equivalence/IOCounterexampleLoopRemover.java b/src/main/java/de/learnlib/ralib/equivalence/IOCounterexampleLoopRemover.java index 92545071..4b71f9bf 100644 --- a/src/main/java/de/learnlib/ralib/equivalence/IOCounterexampleLoopRemover.java +++ b/src/main/java/de/learnlib/ralib/equivalence/IOCounterexampleLoopRemover.java @@ -60,7 +60,7 @@ private static class Loop { private final int min; private final int max; - public Loop(int min, int max) { + Loop(int min, int max) { this.min = min; this.max = max; } diff --git a/src/main/java/de/learnlib/ralib/equivalence/IOEquivalenceTest.java b/src/main/java/de/learnlib/ralib/equivalence/IOEquivalenceTest.java index 2117a1aa..42b00376 100644 --- a/src/main/java/de/learnlib/ralib/equivalence/IOEquivalenceTest.java +++ b/src/main/java/de/learnlib/ralib/equivalence/IOEquivalenceTest.java @@ -57,16 +57,16 @@ private static class Pair { private final T1 first; private final T2 second; - public Pair(T1 first, T2 second) { + Pair(T1 first, T2 second) { this.first = first; this.second = second; } - public T1 getFirst() { + T1 getFirst() { return first; } - public T2 getSecond() { + T2 getSecond() { return second; } } @@ -83,7 +83,7 @@ private static class Tuple { RegisterValuation sys1reg; RegisterValuation sys2reg; - public Tuple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2) { + Tuple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2) { sys1loc = l1; sys2loc = l2; sys1reg = RegisterValuation.copyOf(r1); @@ -179,7 +179,7 @@ private static class Triple { Word as; Word trace; - public Triple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2, Word w, Word t) { + Triple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2, Word w, Word t) { sys1loc = l1; sys2loc = l2; sys1reg = RegisterValuation.copyOf(r1); diff --git a/src/main/java/de/learnlib/ralib/equivalence/RAEquivalenceTest.java b/src/main/java/de/learnlib/ralib/equivalence/RAEquivalenceTest.java index 301365cd..860a4139 100644 --- a/src/main/java/de/learnlib/ralib/equivalence/RAEquivalenceTest.java +++ b/src/main/java/de/learnlib/ralib/equivalence/RAEquivalenceTest.java @@ -53,7 +53,7 @@ private static class Tuple { RegisterValuation sys1reg; RegisterValuation sys2reg; - public Tuple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2) { + Tuple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2) { sys1loc = l1; sys2loc = l2; sys1reg = RegisterValuation.copyOf(r1); @@ -153,7 +153,7 @@ private static class Triple { Word as; Word trace; - public Triple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2, Word w, Word t) { + Triple(RALocation l1, RALocation l2, RegisterValuation r1, RegisterValuation r2, Word w, Word t) { sys1loc = l1; sys2loc = l2; sys1reg = RegisterValuation.copyOf(r1); diff --git a/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java b/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java index 5df076f0..9ea4215d 100644 --- a/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java +++ b/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java @@ -69,9 +69,9 @@ public SymbolicSuffixRestrictionBuilder getRestrictionBuilder() { private final DTLeaf prefixLeaf; private final DTLeaf leaf; - public SymbolicSuffix addedSuffix = null; + SymbolicSuffix addedSuffix = null; - public DummyDT(MappedPrefix word, MappedPrefix prefix) { + DummyDT(MappedPrefix word, MappedPrefix prefix) { super(new DummyOracle(), false, new Constants(), (ParameterizedSymbol[])null); leaf = new DTLeaf(word, null); prefixLeaf = new DTLeaf(prefix, null); From 947edcc0e74ba6b9572d9f966ceb3736c211ecbe Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 23 Dec 2025 16:09:19 +0100 Subject: [PATCH 07/16] Remove some unnecessary parentheses --- pom.xml | 2 +- .../learnlib/ralib/automata/util/RAToDot.java | 2 +- .../xml/RegisterAutomatonExporter.java | 10 +++++----- src/main/java/de/learnlib/ralib/dt/DT.java | 2 +- .../ralib/learning/SymbolicSuffix.java | 2 +- .../oracles/mto/MultiTheoryBranching.java | 8 ++++---- .../java/de/learnlib/ralib/smt/SMTUtil.java | 2 +- .../java/de/learnlib/ralib/theory/SDT.java | 2 +- .../ralib/theory/equality/EqualityTheory.java | 2 +- .../inequality/InequalityTheoryWithEq.java | 2 +- .../ClasssAnalyzerDataWordSUL.java | 6 +++--- .../theories/DoubleInequalityTheory.java | 20 +++++++++---------- 12 files changed, 30 insertions(+), 30 deletions(-) diff --git a/pom.xml b/pom.xml index 9c7351ae..02fb7a75 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:UnnecessaryParentheses:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java b/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java index 6194fe8d..bebd88d5 100644 --- a/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java +++ b/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); } diff --git a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java index 3183ac0c..723bba98 100644 --- a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java +++ b/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 prefix, SymbolicSuffix suffix, DTLeaf le // update old leaf boolean removed = leaf.removeShortPrefix(prefix); - assert (removed); // must not split a prefix that isn't there + assert removed; // must not split a prefix that isn't there //SDT tqr2 = leaf.getPrimePrefix().computeTQR(suffix, oracle); PathResult r2 = PathResult.computePathResult(oracle, leaf.getPrimePrefix(), node.getSuffixes(), ioMode); diff --git a/src/main/java/de/learnlib/ralib/learning/SymbolicSuffix.java b/src/main/java/de/learnlib/ralib/learning/SymbolicSuffix.java index d348855d..d7a388b3 100644 --- a/src/main/java/de/learnlib/ralib/learning/SymbolicSuffix.java +++ b/src/main/java/de/learnlib/ralib/learning/SymbolicSuffix.java @@ -202,7 +202,7 @@ public SymbolicSuffix(Word actions, Map (a.getValue().equals(sv))) + .stream().filter((a) -> a.getValue().equals(sv)) .sorted(Map.Entry.comparingByKey(Comparator.naturalOrder())) .findFirst() .get() diff --git a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryBranching.java b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryBranching.java index 2b0eee1d..4c7546e4 100644 --- a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryBranching.java +++ b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryBranching.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"); @@ -88,7 +88,7 @@ void toString(StringBuilder sb, String indentation) { protected Map> collectDVs() { Map> dvs = new LinkedHashMap(); - if (!(this.next.keySet()).isEmpty()) { + if (! this.next.keySet().isEmpty()) { dvs.put(this.parameter, this.next.keySet()); for (Map.Entry e : this.next.entrySet()) { dvs.putAll(e.getValue().collectDVs()); @@ -99,7 +99,7 @@ protected Map> collectDVs() { protected Map> collectGuards() { Map> guards = new LinkedHashMap(); - if (!(this.next.keySet()).isEmpty()) { + if (! this.next.keySet().isEmpty()) { guards.put(this.parameter, new LinkedHashSet(this.guards.values())); for (Map.Entry e : this.next.entrySet()) { guards.putAll(e.getValue().collectGuards()); @@ -109,7 +109,7 @@ protected Map> collectGuards() { } protected SDT buildFakeSDT() { - if (!(this.next.keySet()).isEmpty()) { + if (! this.next.keySet().isEmpty()) { Map map = new LinkedHashMap(); for (Map.Entry e : this.next.entrySet()) { SDTGuard guard = guards.get(e.getKey()); diff --git a/src/main/java/de/learnlib/ralib/smt/SMTUtil.java b/src/main/java/de/learnlib/ralib/smt/SMTUtil.java index 3c376e2d..80e62129 100644 --- a/src/main/java/de/learnlib/ralib/smt/SMTUtil.java +++ b/src/main/java/de/learnlib/ralib/smt/SMTUtil.java @@ -91,7 +91,7 @@ private static Variable getOrCreate(SymbolicDataValue dv, Map mergeGuards(Map eqs, SDT List ds = new ArrayList<>(); ds.add(eqGuard); LOGGER.trace("remapping: " + ds); - if (!(eqSdt.isEquivalentUnder(deqSdt, ds))) { + if (! eqSdt.isEquivalentUnder(deqSdt, ds)) { LOGGER.trace("--> not eq."); deqList.add(SDTGuard.toDeqGuard(eqGuard)); eqList.add(eqGuard); diff --git a/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java b/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java index d74cf0ea..24d4f65d 100644 --- a/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java +++ b/src/main/java/de/learnlib/ralib/theory/inequality/InequalityTheoryWithEq.java @@ -585,7 +585,7 @@ public DataValue instantiate( throw new IllegalStateException("only =, != or interval allowed. Got " + guard); } - if (!(oldDvs.isEmpty())) { + if (! oldDvs.isEmpty()) { for (DataValue oldDv : oldDvs) { Valuation newVal = new Valuation(); newVal.putAll(val); diff --git a/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java b/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java index 3d50aec3..a64eeeab 100644 --- a/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.java +++ b/src/main/java/de/learnlib/ralib/tools/classanalyzer/ClasssAnalyzerDataWordSUL.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"); @@ -132,9 +132,9 @@ public PSymbolInstance step(PSymbolInstance i) throws SULException { } assert ret instanceof BigDecimal : "The class analyzer only works for BigDecimal values!"; - DataValue retVal = (isFresh(in.getRetType(), ret)) + DataValue retVal = isFresh(in.getRetType(), ret) ? registerFreshValue(in.getRetType(), ret) - : new DataValue(in.getRetType(), (BigDecimal) ret); + : new DataValue(in.getRetType(), (BigDecimal)ret); //updateSeen(retVal); return new PSymbolInstance(in.getOutput(), retVal); diff --git a/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java b/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java index 5aea1e21..e836bd85 100644 --- a/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java +++ b/src/main/java/de/learnlib/ralib/tools/theories/DoubleInequalityTheory.java @@ -56,7 +56,7 @@ public int compare(DataValue one, DataValue other) { } } - private final ConstraintSolver solver = (new NativeZ3SolverProvider()).createSolver(new Properties()); + private final ConstraintSolver solver = new NativeZ3SolverProvider().createSolver(new Properties()); private static final Logger LOGGER = LoggerFactory.getLogger(DoubleInequalityTheory.class); @@ -103,7 +103,7 @@ private List> instantiateGuard(SDTGuard g, Valuation val) { // get the register value from the valuation DataValue sdi = new DataValue(type, val.getValue(si)); // add the register value as a constant - gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (sdi.getValue())); + gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, sdi.getValue()); // add the constant equivalence expression to the list eList.add(new NumericBooleanExpression(wm, NumericComparator.EQ, si)); @@ -113,18 +113,18 @@ private List> instantiateGuard(SDTGuard g, Valuation val) { // get the register value from the valuation DataValue sdi = new DataValue(type, val.getValue(si)); // add the register value as a constant - gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (sdi.getValue())); + gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, sdi.getValue()); // add the constant equivalence expression to the list eList.add(new NumericBooleanExpression(wm, NumericComparator.EQ, si)); throw new RuntimeException("this seems to be wrong ..."); } else if (g instanceof SDTGuard.IntervalGuard iGuard) { if (!iGuard.isBiggerGuard()) { - SDTGuardElement r = iGuard.greaterElement(); + SDTGuardElement r = iGuard.greaterElement(); assert r != null; DataValue ri = (r instanceof DataValue) ? (DataValue) r : new DataValue(type, (BigDecimal) val.getValue( (Variable) r)); - gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (ri.getValue())); + gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, ri.getValue()); // add the constant equivalence expression to the list eList.add(new NumericBooleanExpression(wm, NumericComparator.EQ, r.asExpression())); } @@ -133,7 +133,7 @@ private List> instantiateGuard(SDTGuard g, Valuation val) { assert l != null; DataValue li = (l instanceof DataValue) ? (DataValue) l : new DataValue(type, (BigDecimal) val.getValue( (Variable) l)); - gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (li.getValue())); + gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, li.getValue()); // add the constant equivalence expression to the list eList.add(new NumericBooleanExpression(wm, NumericComparator.EQ, l.asExpression())); } @@ -168,14 +168,14 @@ public DataValue instantiate(SDTGuard g, Valuation val, Constants c, Collection< // add disequalities for (DataValue au : alreadyUsedValues) { - gov.nasa.jpf.constraints.expressions.Constant w = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (au.getValue())); + gov.nasa.jpf.constraints.expressions.Constant w = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, au.getValue()); Expression auExpr = new NumericBooleanExpression(w, NumericComparator.NE, sp); eList.add(auExpr); } if (newVal.containsValueFor(sp)) { DataValue spDouble = new DataValue(type, newVal.getValue(sp)); - gov.nasa.jpf.constraints.expressions.Constant spw = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, (spDouble.getValue())); + gov.nasa.jpf.constraints.expressions.Constant spw = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, spDouble.getValue()); Expression spExpr = new NumericBooleanExpression(spw, NumericComparator.EQ, sp); eList.add(spExpr); } @@ -251,8 +251,8 @@ public Collection getAllNextValues( //(d1 + ((d2 - d1) / 2)))); } } - nextValues.add(new DataValue(type, (Collections.min(vals, new Cpr()).getValue().subtract(BigDecimal.ONE)))); - nextValues.add(new DataValue(type, (Collections.max(vals, new Cpr()).getValue().add(BigDecimal.ONE)))); + nextValues.add(new DataValue(type, Collections.min(vals, new Cpr()).getValue().subtract(BigDecimal.ONE))); + nextValues.add(new DataValue(type, Collections.max(vals, new Cpr()).getValue().add(BigDecimal.ONE))); } return nextValues; } From f0ead814a9460489b8bcfad8ac1fe375f4e3f73b Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 23 Dec 2025 16:52:13 +0100 Subject: [PATCH 08/16] Make a public constant array private --- pom.xml | 2 +- src/main/java/de/learnlib/ralib/learning/QueryStatistics.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pom.xml b/pom.xml index 02fb7a75..4e206758 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:MutablePublicArray:OFF -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/main/java/de/learnlib/ralib/learning/QueryStatistics.java b/src/main/java/de/learnlib/ralib/learning/QueryStatistics.java index 324174a1..5b0d9a30 100644 --- a/src/main/java/de/learnlib/ralib/learning/QueryStatistics.java +++ b/src/main/java/de/learnlib/ralib/learning/QueryStatistics.java @@ -16,7 +16,7 @@ public class QueryStatistics { public static final int CE_ANALYSIS = 2; public static final int CE_PROCESSING = 3; public static final int OTHER = 4; - public static final String[] PHASES = {"Testing", "CE Optimization", "CE Analysis", "Processing / Refinement", "Other"}; + private static final String[] PHASES = {"Testing", "CE Optimization", "CE Analysis", "Processing / Refinement", "Other"}; private static final int MEASUREMENTS = 5; private final QueryCounter queryCounter; From fff98b6594b8c9d73bfee75ed781879653a04ce0 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 23 Dec 2025 18:03:04 +0100 Subject: [PATCH 09/16] Remove two unused methods --- pom.xml | 2 +- .../ralib/automata/xml/RegisterAutomatonImporter.java | 4 ---- .../learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java | 8 +------- 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/pom.xml b/pom.xml index 4e206758..891d2f13 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:UnusedMethod:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java index b38a1ccf..2cfff071 100644 --- a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java +++ b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java @@ -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 buildValueMap( Map ... maps) { Map ret = new LinkedHashMap<>(); diff --git a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java index 200f1b23..af2b5e5a 100644 --- a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java +++ b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java @@ -173,12 +173,6 @@ private Node createFreshNode(int i, Word prefix, ParameterizedS } } - private Node createNode(int i, Word prefix, ParameterizedSymbol ps, SuffixValuation pval, - SDT... sdts) { - Node n = createNode(i, prefix, ps, pval, new LinkedHashMap<>(), sdts); - return n; - } - private Node createNode(int i, Word prefix, ParameterizedSymbol ps, SuffixValuation pval, Map> oldDvMap, SDT... sdts) { @@ -459,7 +453,7 @@ public Branching updateBranching(Word prefix, ParameterizedSymb updated[0] = oldBranching.buildFakeSDT(); System.arraycopy(sdts, 0, updated, 1, sdts.length); - Node n = createNode(1, prefix, ps, new SuffixValuation(),oldDvs, updated); + Node n = createNode(1, prefix, ps, new SuffixValuation(), oldDvs, updated); MultiTheoryBranching mtb = new MultiTheoryBranching(prefix, ps, n, constants, updated); return mtb; } From 06769145328d391512fbe813acdeb8a6bee65424 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Tue, 23 Dec 2025 19:13:39 +0100 Subject: [PATCH 10/16] Make a test public --- .../ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java b/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java index cc684de6..bd8dc476 100644 --- a/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java +++ b/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java @@ -501,7 +501,7 @@ public void testExtendSuffixRevealingRegisters() { } @Test - private void testSDTPrune() { + public void testSDTPrune() { DataType type = new DataType("int"); final Map teachers = new LinkedHashMap<>(); From 89c1af95cff446df0ab310829a8638f35099ba61 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Wed, 24 Dec 2025 10:00:30 +0100 Subject: [PATCH 11/16] Simplify some code by using instanceof with a variable --- pom.xml | 2 +- .../learnlib/ralib/automata/util/RAToDot.java | 4 +- .../xml/RegisterAutomatonExporter.java | 15 +++-- .../xml/RegisterAutomatonImporter.java | 4 +- src/main/java/de/learnlib/ralib/dt/DT.java | 4 +- .../ralib/learning/IOAutomatonBuilder.java | 8 +-- .../oracles/mto/MultiTheoryTreeOracle.java | 10 +-- .../ralib/theory/SuffixValueRestriction.java | 12 ++-- .../theory/equality/EqualRestriction.java | 4 +- .../ralib/theory/equality/EqualityTheory.java | 8 +-- .../inequality/InequalityTheoryWithEq.java | 61 ++++++++----------- .../theories/DoubleInequalityTheory.java | 4 +- .../example/priority/PriorityQueueSUL.java | 8 +-- 13 files changed, 65 insertions(+), 79 deletions(-) diff --git a/pom.xml b/pom.xml index 891d2f13..a9b0196a 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:PatternMatchingInstanceof:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java b/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java index bebd88d5..a2c595a1 100644 --- a/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java +++ b/src/main/java/de/learnlib/ralib/automata/util/RAToDot.java @@ -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 ); } diff --git a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java index 723bba98..b34e8b97 100644 --- a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java +++ b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonExporter.java @@ -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 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); } } diff --git a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java index 2cfff071..00fe8809 100644 --- a/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java +++ b/src/main/java/de/learnlib/ralib/automata/xml/RegisterAutomatonImporter.java @@ -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 diff --git a/src/main/java/de/learnlib/ralib/dt/DT.java b/src/main/java/de/learnlib/ralib/dt/DT.java index d2656dec..92225347 100644 --- a/src/main/java/de/learnlib/ralib/dt/DT.java +++ b/src/main/java/de/learnlib/ralib/dt/DT.java @@ -166,8 +166,8 @@ private DTLeaf sift(MappedPrefix mp, DTInnerNode from, boolean add) { } while (leaf == null); if (add && !leaf.getAccessSequence().equals(mp.getPrefix())) { - if (mp instanceof ShortPrefix) { - leaf.addShortPrefix((ShortPrefix) mp); + if (mp instanceof ShortPrefix shortPrefix) { + leaf.addShortPrefix(shortPrefix); } else { leaf.addPrefix(mp); } diff --git a/src/main/java/de/learnlib/ralib/learning/IOAutomatonBuilder.java b/src/main/java/de/learnlib/ralib/learning/IOAutomatonBuilder.java index ab8cfd65..7fa42d1f 100644 --- a/src/main/java/de/learnlib/ralib/learning/IOAutomatonBuilder.java +++ b/src/main/java/de/learnlib/ralib/learning/IOAutomatonBuilder.java @@ -83,7 +83,7 @@ protected Transition createTransition(ParameterizedSymbol action, return null; } - if (!(action instanceof OutputSymbol)) { + if (!(action instanceof OutputSymbol outputSymbol)) { return super.createTransition(action, guard, src_loc, dest_loc, assign); } @@ -105,7 +105,7 @@ protected Transition createTransition(ParameterizedSymbol action, OutputMapping outMap = new OutputMapping(fresh, outmap); return new OutputTransition(ExpressionUtil.TRUE, - outMap, (OutputSymbol) action, src_loc, dest_loc, assign); + outMap, outputSymbol, src_loc, dest_loc, assign); } private void analyzeExpression(Expression expr, @@ -125,12 +125,12 @@ else if (expr instanceof NumericBooleanExpression nbe) { Parameter p = null; SymbolicDataValue sv = null; - if (left instanceof Parameter) { + if (left instanceof Parameter parameter) { if (right instanceof Parameter) { throw new UnsupportedOperationException("not implemented yet."); } else { - p = (Parameter) left; + p = parameter; sv = (SymbolicDataValue) right; } } diff --git a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java index af2b5e5a..b18def16 100644 --- a/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java +++ b/src/main/java/de/learnlib/ralib/oracles/mto/MultiTheoryTreeOracle.java @@ -318,15 +318,15 @@ public SDTGuard conjoin(SDTGuard guard1, SDTGuard guard2) { return guard1; } - if (guard1 instanceof SDTGuard.SDTAndGuard && guard2 instanceof SDTGuard.SDTAndGuard) { - List guards = new ArrayList(((SDTGuard.SDTAndGuard) guard1).conjuncts()); - guards.addAll(((SDTGuard.SDTAndGuard) guard2).conjuncts()); + if (guard1 instanceof SDTGuard.SDTAndGuard sdtAndGuard1 && guard2 instanceof SDTGuard.SDTAndGuard sdtAndGuard2) { + List guards = new ArrayList(sdtAndGuard1.conjuncts()); + guards.addAll(sdtAndGuard2.conjuncts()); return new SDTGuard.SDTAndGuard(guard1.getParameter(), guards); } if (guard1 instanceof SDTGuard.SDTAndGuard || guard2 instanceof SDTGuard.SDTAndGuard) { - SDTGuard.SDTAndGuard andGuard = guard1 instanceof SDTGuard.SDTAndGuard ? - (SDTGuard.SDTAndGuard) guard1 : (SDTGuard.SDTAndGuard) guard2; + SDTGuard.SDTAndGuard andGuard = guard1 instanceof SDTGuard.SDTAndGuard sdtAndGuard ? + sdtAndGuard : (SDTGuard.SDTAndGuard) guard2; SDTGuard otherGuard = guard2 instanceof SDTGuard.SDTAndGuard ? guard1 : guard2; List conjuncts = andGuard.conjuncts(); conjuncts.add(otherGuard); diff --git a/src/main/java/de/learnlib/ralib/theory/SuffixValueRestriction.java b/src/main/java/de/learnlib/ralib/theory/SuffixValueRestriction.java index 9db47c0e..c50777ba 100644 --- a/src/main/java/de/learnlib/ralib/theory/SuffixValueRestriction.java +++ b/src/main/java/de/learnlib/ralib/theory/SuffixValueRestriction.java @@ -120,14 +120,14 @@ public static SuffixValueRestriction genericRestriction(SDTGuard guard, Map prior) { assert other.getParameter().equals(parameter); if (prior.get(equalParam) instanceof FreshSuffixValue) { - if (other instanceof EqualRestriction && - ((EqualRestriction) other).equalParam.equals(equalParam)) { + if (other instanceof EqualRestriction equalRestriction && + equalRestriction.equalParam.equals(equalParam)) { // equality only if the same equality and that parameter is fresh return this; } diff --git a/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java b/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java index 31aca361..f653ca3b 100644 --- a/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java +++ b/src/main/java/de/learnlib/ralib/theory/equality/EqualityTheory.java @@ -329,8 +329,8 @@ public DataValue instantiate(Word prefix, ParameterizedSymbol p } else if (SDTGuardElement.isConstant(ereg)) { return constants.get((Constant) ereg); } - } else if (current instanceof SDTGuard.SDTAndGuard) { - guards.addAll(((SDTGuard.SDTAndGuard) current).conjuncts()); + } else if (current instanceof SDTGuard.SDTAndGuard sdtAndGuard) { + guards.addAll(sdtAndGuard.conjuncts()); } // todo: this only works under the assumption that disjunctions only contain disequality guards } @@ -422,9 +422,9 @@ public SuffixValueRestriction restrictSuffixValue(SDTGuard guard, Map mergeGuards(Map sdts, if (merged.size() == 1) { Map.Entry entry = merged.entrySet().iterator().next(); SDTGuard g = entry.getKey(); - if (g instanceof SDTGuard.DisequalityGuard || (g instanceof SDTGuard.IntervalGuard && ((SDTGuard.IntervalGuard) g).isBiggerGuard())) { + if (g instanceof SDTGuard.DisequalityGuard || (g instanceof SDTGuard.IntervalGuard intervalGuard && intervalGuard.isBiggerGuard())) { merged = new LinkedHashMap<>(); merged.put(new SDTGuard.SDTTrueGuard(g.getParameter()), entry.getValue()); } @@ -320,11 +320,9 @@ private boolean equivalentWithRenaming(SDT sdt1, SDTGuard guard1, SDT sdt2, SDTG */ private SDTGuard mergeIntervals(SDTGuard leftGuard, SDTGuard rightGuard) { SuffixValue suffixValue = leftGuard.getParameter(); - if (leftGuard instanceof SDTGuard.EqualityGuard) { - SDTGuard.EqualityGuard egLeft = (SDTGuard.EqualityGuard) leftGuard; + if (leftGuard instanceof SDTGuard.EqualityGuard egLeft) { SDTGuardElement rl = egLeft.register(); - if (rightGuard instanceof SDTGuard.IntervalGuard) { - SDTGuard.IntervalGuard igRight = (SDTGuard.IntervalGuard) rightGuard; + if (rightGuard instanceof SDTGuard.IntervalGuard igRight) { if (!igRight.isSmallerGuard() && igRight.smallerElement().equals(rl)) { if (igRight.isBiggerGuard()) { return SDTGuard.IntervalGuard.greaterOrEqualGuard(suffixValue, rl); @@ -333,16 +331,14 @@ private SDTGuard mergeIntervals(SDTGuard leftGuard, SDTGuard rightGuard) { } } } - } else if (leftGuard instanceof SDTGuard.IntervalGuard && !((SDTGuard.IntervalGuard) leftGuard).isBiggerGuard()) { - SDTGuard.IntervalGuard igLeft = (SDTGuard.IntervalGuard) leftGuard; + } else if (leftGuard instanceof SDTGuard.IntervalGuard igLeft && !igLeft.isBiggerGuard()) { SDTGuardElement rr = igLeft.greaterElement(); if (igLeft.isSmallerGuard()) { - if (rightGuard instanceof SDTGuard.EqualityGuard && ((SDTGuard.EqualityGuard) rightGuard).register().equals(rr)) { + if (rightGuard instanceof SDTGuard.EqualityGuard equalityGuard && equalityGuard.register().equals(rr)) { return SDTGuard.IntervalGuard.lessOrEqualGuard(suffixValue, rr); - } else if (rightGuard instanceof SDTGuard.IntervalGuard && - !((SDTGuard.IntervalGuard) rightGuard).isSmallerGuard() && - ((SDTGuard.IntervalGuard) rightGuard).smallerElement().equals(rr)) { - SDTGuard.IntervalGuard igRight = (SDTGuard.IntervalGuard) rightGuard; + } else if (rightGuard instanceof SDTGuard.IntervalGuard igRight && + !igRight.isSmallerGuard() && + igRight.smallerElement().equals(rr)) { if (igRight.isIntervalGuard()) { return SDTGuard.IntervalGuard.lessGuard(suffixValue, igRight.greaterElement()); } else { @@ -350,12 +346,11 @@ private SDTGuard mergeIntervals(SDTGuard leftGuard, SDTGuard rightGuard) { } } } else if (igLeft.isIntervalGuard()) { - if (rightGuard instanceof SDTGuard.EqualityGuard && ((SDTGuard.EqualityGuard) rightGuard).register().equals(rr)) { + if (rightGuard instanceof SDTGuard.EqualityGuard equalityGuard && equalityGuard.register().equals(rr)) { return new SDTGuard.IntervalGuard(suffixValue, igLeft.smallerElement(), rr, igLeft.isLeftClosed(), true); - } else if (rightGuard instanceof SDTGuard.IntervalGuard && - !((SDTGuard.IntervalGuard) rightGuard).isSmallerGuard() && - ((SDTGuard.IntervalGuard) rightGuard).smallerElement().equals(rr)) { - SDTGuard.IntervalGuard igRight = (SDTGuard.IntervalGuard) rightGuard; + } else if (rightGuard instanceof SDTGuard.IntervalGuard igRight && + !igRight.isSmallerGuard() && + igRight.smallerElement().equals(rr)) { if (igRight.isBiggerGuard()) { return new SDTGuard.IntervalGuard(suffixValue, igLeft.smallerElement(), null, igLeft.isLeftClosed(), false); } else { @@ -380,8 +375,8 @@ private Map checkForDisequality(Map guards) { if (size < 1 || size > 3) return guards; - Optional less = guards.keySet().stream().filter(g -> g instanceof SDTGuard.IntervalGuard && ((SDTGuard.IntervalGuard) g).isSmallerGuard()).findAny(); - Optional greater = guards.keySet().stream().filter(g -> g instanceof SDTGuard.IntervalGuard && ((SDTGuard.IntervalGuard) g).isBiggerGuard()).findAny(); + Optional less = guards.keySet().stream().filter(g -> g instanceof SDTGuard.IntervalGuard intervalGuard && intervalGuard.isSmallerGuard()).findAny(); + Optional greater = guards.keySet().stream().filter(g -> g instanceof SDTGuard.IntervalGuard intervalGuard && intervalGuard.isBiggerGuard()).findAny(); if (less.isPresent() && greater.isPresent()) { SDTGuard.IntervalGuard lg = (SDTGuard.IntervalGuard) less.get(); SDTGuard.IntervalGuard gg = (SDTGuard.IntervalGuard) greater.get(); @@ -522,9 +517,7 @@ public DataValue instantiate( DataValue returnThis = null; List prefixValues = Arrays.asList(DataWords.valsOf(prefix)); - if (guard instanceof SDTGuard.EqualityGuard) { - SDTGuard.EqualityGuard eqGuard = (SDTGuard.EqualityGuard) guard; - + if (guard instanceof SDTGuard.EqualityGuard eqGuard) { SDTGuardElement ereg = eqGuard.register(); if (SDTGuardElement.isDataValue(ereg)) { returnThis = (DataValue) ereg; @@ -535,7 +528,6 @@ public DataValue instantiate( } assert returnThis != null; } else if (guard instanceof SDTGuard.SDTTrueGuard || guard instanceof SDTGuard.DisequalityGuard) { - Collection potSet = DataWords.joinValsToSet( constants.values(type), DataWords.valSet(prefix, type), @@ -549,9 +541,8 @@ public DataValue instantiate( DataWords.valSet(prefix, type), pval.values(type)); Valuation val = new Valuation(); - if (guard instanceof SDTGuard.IntervalGuard) { - SDTGuard.IntervalGuard iGuard = (SDTGuard.IntervalGuard) guard; - if (!iGuard.isBiggerGuard()) { + if (guard instanceof SDTGuard.IntervalGuard iGuard) { + if (!iGuard.isBiggerGuard()) { SDTGuardElement r = iGuard.greaterElement(); if (SDTGuardElement.isSuffixValue(r) || SDTGuardElement.isConstant(r)) { DataValue regVal = getRegisterValue(r, prefixValues, constants, pval); @@ -668,8 +659,7 @@ public SuffixValueRestriction restrictSuffixValue(SuffixValue suffixValue, Word< public SuffixValueRestriction restrictSuffixValue(SDTGuard guard, Map prior) { SuffixValue sv = guard.getParameter(); - if (guard instanceof SDTGuard.IntervalGuard) { - SDTGuard.IntervalGuard ig = (SDTGuard.IntervalGuard) guard; + if (guard instanceof SDTGuard.IntervalGuard ig) { if (ig.isBiggerGuard()) { return new GreaterSuffixValue(sv); } else if (ig.isSmallerGuard()) { @@ -685,24 +675,23 @@ public SuffixValueRestriction restrictSuffixValue(SDTGuard guard, Map> instantiateGuard(SDTGuard g, Valuation val) { if (!iGuard.isBiggerGuard()) { SDTGuardElement r = iGuard.greaterElement(); assert r != null; - DataValue ri = (r instanceof DataValue) ? (DataValue) r : + DataValue ri = (r instanceof DataValue dataValue) ? dataValue : new DataValue(type, (BigDecimal) val.getValue( (Variable) r)); gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, ri.getValue()); // add the constant equivalence expression to the list @@ -131,7 +131,7 @@ private List> instantiateGuard(SDTGuard g, Valuation val) { if (!iGuard.isSmallerGuard()) { SDTGuardElement l = iGuard.smallerElement(); assert l != null; - DataValue li = (l instanceof DataValue) ? (DataValue) l : + DataValue li = (l instanceof DataValue dataValue) ? dataValue : new DataValue(type, (BigDecimal) val.getValue( (Variable) l)); gov.nasa.jpf.constraints.expressions.Constant wm = new gov.nasa.jpf.constraints.expressions.Constant(BuiltinTypes.DECIMAL, li.getValue()); // add the constant equivalence expression to the list diff --git a/src/test/java/de/learnlib/ralib/example/priority/PriorityQueueSUL.java b/src/test/java/de/learnlib/ralib/example/priority/PriorityQueueSUL.java index e93069f5..c3e4bae6 100644 --- a/src/test/java/de/learnlib/ralib/example/priority/PriorityQueueSUL.java +++ b/src/test/java/de/learnlib/ralib/example/priority/PriorityQueueSUL.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"); @@ -38,7 +38,6 @@ public class PriorityQueueSUL extends DataWordSUL { public static final ParameterizedSymbol OFFER = new InputSymbol("offer", DOUBLE_TYPE); - public final ParameterizedSymbol[] getInputSymbols() { return new ParameterizedSymbol[] { POLL, OFFER }; } @@ -59,7 +58,6 @@ public final ParameterizedSymbol[] getActionSymbols() { return new ParameterizedSymbol[] { POLL, OFFER, OUTPUT, OK, NOK, ERROR }; } - private PQWrapper pqueue; private final int capacity; @@ -83,8 +81,8 @@ public void post() { } private PSymbolInstance createOutputSymbol(Object x) { - if (x instanceof Boolean) { - return new PSymbolInstance( ((Boolean) x) ? OK : NOK); + if (x instanceof Boolean b) { + return new PSymbolInstance(b ? OK : NOK); } else if (x instanceof java.lang.Exception) { return new PSymbolInstance(ERROR); } else if (x == null) { From c813b712736c3997b9cd30641b63ee6abdda1d07 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Wed, 24 Dec 2025 10:53:48 +0100 Subject: [PATCH 12/16] Add an extra assertion to a test --- src/test/java/de/learnlib/ralib/data/BijectionTest.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/java/de/learnlib/ralib/data/BijectionTest.java b/src/test/java/de/learnlib/ralib/data/BijectionTest.java index 5e6be7d2..66f1da9a 100644 --- a/src/test/java/de/learnlib/ralib/data/BijectionTest.java +++ b/src/test/java/de/learnlib/ralib/data/BijectionTest.java @@ -80,5 +80,6 @@ public void testException() { } Assert.assertTrue(exceptionCaught); + Assert.assertEquals(bi.size(), 0); } } From 637e5745eefe4f80f4d671ec38bc20a8b3cd93d9 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Wed, 24 Dec 2025 10:54:57 +0100 Subject: [PATCH 13/16] Remove or comment out some unnecessary code from tests --- pom.xml | 2 +- .../OptimizedSymbolicSuffixBuilderTest.java | 4 ---- .../theory/inequality/IneqGuardMergeTest.java | 21 +++++++++---------- .../IntervalGuardInstaniateTest.java | 7 ++----- 4 files changed, 13 insertions(+), 21 deletions(-) diff --git a/pom.xml b/pom.xml index a9b0196a..48b9052a 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:ModifiedButNotUsed:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java b/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java index bd8dc476..0740bdeb 100644 --- a/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java +++ b/src/test/java/de/learnlib/ralib/oracles/mto/OptimizedSymbolicSuffixBuilderTest.java @@ -346,10 +346,6 @@ public void testBuildOptimizedSuffix() { DataType type = new DataType("int"); InputSymbol a = new InputSymbol("a", type); - final Map teachers = new LinkedHashMap<>(); - IntegerEqualityTheory dit = new IntegerEqualityTheory(type); - teachers.put(type, dit); - SuffixValueGenerator sgen = new SymbolicDataValueGenerator.SuffixValueGenerator(); SuffixValue s1 = sgen.next(type); SuffixValue s2 = sgen.next(type); diff --git a/src/test/java/de/learnlib/ralib/theory/inequality/IneqGuardMergeTest.java b/src/test/java/de/learnlib/ralib/theory/inequality/IneqGuardMergeTest.java index 04e5895e..3d44aa2f 100644 --- a/src/test/java/de/learnlib/ralib/theory/inequality/IneqGuardMergeTest.java +++ b/src/test/java/de/learnlib/ralib/theory/inequality/IneqGuardMergeTest.java @@ -19,7 +19,6 @@ import de.learnlib.ralib.theory.SDT; import de.learnlib.ralib.theory.SDTGuard; import de.learnlib.ralib.theory.SDTLeaf; -import de.learnlib.ralib.theory.Theory; import de.learnlib.ralib.tools.theories.DoubleInequalityTheory; public class IneqGuardMergeTest extends RaLibTestSuite { @@ -28,10 +27,10 @@ public class IneqGuardMergeTest extends RaLibTestSuite { public void testIntervalMerge() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); dit.useSuffixOptimization(true); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValueGenerator svgen = new SuffixValueGenerator(); RegisterGenerator rgen = new RegisterGenerator(); @@ -155,10 +154,10 @@ public void testIntervalMerge() { public void testTrueGuard() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); dit.useSuffixOptimization(true); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValueGenerator svgen = new SuffixValueGenerator(); RegisterGenerator rgen = new RegisterGenerator(); @@ -203,10 +202,10 @@ public void testTrueGuard() { public void testFilteredDataValues() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); dit.useSuffixOptimization(true); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValueGenerator svgen = new SuffixValueGenerator(); RegisterGenerator rgen = new RegisterGenerator(); @@ -266,10 +265,10 @@ public void testFilteredDataValues() { public void testSDTSubtree() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); dit.useSuffixOptimization(true); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValueGenerator svgen = new SuffixValueGenerator(); RegisterGenerator rgen = new RegisterGenerator(); @@ -328,10 +327,10 @@ public void testSDTSubtree() { public void testDisequalityGuard() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); dit.useSuffixOptimization(true); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValueGenerator svgen = new SuffixValueGenerator(); RegisterGenerator rgen = new RegisterGenerator(); diff --git a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java index 4eaa507f..fed0ae95 100644 --- a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java +++ b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java @@ -3,8 +3,6 @@ import java.math.BigDecimal; import java.util.ArrayList; import java.util.Collection; -import java.util.LinkedHashMap; -import java.util.Map; import org.testng.Assert; import org.testng.annotations.Test; @@ -16,7 +14,6 @@ import de.learnlib.ralib.data.SymbolicDataValue.Register; import de.learnlib.ralib.data.SymbolicDataValue.SuffixValue; import de.learnlib.ralib.theory.SDTGuard; -import de.learnlib.ralib.theory.Theory; import de.learnlib.ralib.tools.theories.DoubleInequalityTheory; import gov.nasa.jpf.constraints.api.Valuation; @@ -27,9 +24,9 @@ public void testInstantiateInterval() { final DataType D_TYPE = new DataType("double"); - final Map teachers = new LinkedHashMap<>(); + //final Map teachers = new LinkedHashMap<>(); DoubleInequalityTheory dit = new DoubleInequalityTheory(D_TYPE); - teachers.put(D_TYPE, dit); + //teachers.put(D_TYPE, dit); SuffixValue s1 = new SuffixValue(D_TYPE, 1); Register r1 = new Register(D_TYPE, 1); From cc2db1c7d66dd5f12a2dc1128dd68f5c7f236262 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Wed, 24 Dec 2025 11:22:02 +0100 Subject: [PATCH 14/16] Sanitize the compareTo comparison to be zero It's an implementation detail whether compareTo returns {-1, 0, 1} or some other value, so all comparisons should be against zero. --- pom.xml | 2 +- .../ralib/theory/inequality/IntervalGuardInstaniateTest.java | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pom.xml b/pom.xml index 48b9052a..6ed1140c 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:CompareToZero:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:MissingCasesInEnumSwitch:OFF diff --git a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java index fed0ae95..3982da44 100644 --- a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java +++ b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java @@ -66,7 +66,7 @@ public void testInstantiateInterval() { Assert.assertNotEquals(dvle.getValue().compareTo(dv1.getValue()), 1); Assert.assertEquals(dvr.getValue().compareTo(dv1.getValue()), 1); Assert.assertNotEquals(dvre.getValue().compareTo(dv1.getValue()), -1); - Assert.assertTrue(dvi.getValue().compareTo(dv1.getValue()) == 1 && dvi.getValue().compareTo(dv3.getValue()) == -1); - Assert.assertFalse(dvic.getValue().compareTo(dv1.getValue()) == -1 && dvic.getValue().compareTo(dv3.getValue()) == 1); + Assert.assertTrue(dvi.getValue().compareTo(dv1.getValue()) > 0 && dvi.getValue().compareTo(dv3.getValue()) < 0); + Assert.assertFalse(dvic.getValue().compareTo(dv1.getValue()) < 0 && dvic.getValue().compareTo(dv3.getValue()) > 0); } } From aa1fef0a36f9b932f35dd561d5233f6cb8ced60b Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Wed, 24 Dec 2025 12:24:41 +0100 Subject: [PATCH 15/16] Add missing cases in two switch statements --- pom.xml | 2 +- .../ralib/example/sdts/LoginExampleTreeOracle.java | 9 ++++++--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/pom.xml b/pom.xml index 6ed1140c..1d77eac2 100644 --- a/pom.xml +++ b/pom.xml @@ -254,7 +254,7 @@ -Xlint:deprecation -XDcompilePolicy=simple --should-stop=ifError=FLOW - -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF -Xep:MissingCasesInEnumSwitch:OFF + -Xplugin:ErrorProne -Xep:ObjectToString:OFF -Xep:BadInstanceof:OFF -Xep:UnusedVariable:OFF -Xep:EqualsGetClass:OFF -Xep:BigDecimalEquals:OFF -Xep:ReferenceEquality:OFF -Xep:ArrayAsKeyOfSetOrMap:OFF -Xep:IterableAndIterator:OFF -Xep:ObjectsHashCodePrimitive:OFF -Xep:StatementSwitchToExpressionSwitch:OFF -Xep:JdkObsolete:OFF -Xep:AddressSelection:OFF -Xep:EmptyBlockTag:OFF -Xep:MissingSummary:OFF -Xep:NonApiType:OFF -Xep:StringSplitter:OFF -Xep:WaitNotInLoop:OFF -Xep:StringConcatToTextBlock:OFF diff --git a/src/test/java/de/learnlib/ralib/example/sdts/LoginExampleTreeOracle.java b/src/test/java/de/learnlib/ralib/example/sdts/LoginExampleTreeOracle.java index 991b0680..70b30b7b 100644 --- a/src/test/java/de/learnlib/ralib/example/sdts/LoginExampleTreeOracle.java +++ b/src/test/java/de/learnlib/ralib/example/sdts/LoginExampleTreeOracle.java @@ -69,8 +69,7 @@ public LoginExampleTreeOracle() { } @Override - public SDT treeQuery( - Word prefix, SymbolicSuffix suffix) { + public SDT treeQuery(Word prefix, SymbolicSuffix suffix) { if (prefix.length() < 1) { return new LoginExampleSDT(SDTClass.REJECT, suffix, new LinkedHashSet()); @@ -109,6 +108,8 @@ public SDT treeQuery( state = State.ERROR; } break; + case ERROR: + break; } if (state == State.ERROR) { @@ -135,6 +136,9 @@ public SDT treeQuery( break; } break; + case INIT: + case ERROR: + break; } return new LoginExampleSDT(clazz, suffix, new LinkedHashSet()); @@ -200,7 +204,6 @@ public Branching getInitialBranching(Word prefix, public Branching updateBranching(Word prefix, ParameterizedSymbol ps, Branching current, SDT... sdts) { - return getInitialBranching(prefix, ps, sdts); } From 469ef5443403c197474602a13ce4727ce8b0a250 Mon Sep 17 00:00:00 2001 From: Kostis Sagonas Date: Sun, 28 Dec 2025 17:12:04 +0100 Subject: [PATCH 16/16] Remove unused code from some tests --- src/test/java/de/learnlib/ralib/dt/DTTest.java | 9 --------- .../ralib/dt/RegisterConsistencyTest.java | 9 +-------- .../learnlib/ralib/example/sdts/SDTOracle.java | 1 - .../oracles/mto/SecondSDTBranchingTest.java | 4 ++-- .../ralib/oracles/mto/UntypedBranchingTest.java | 17 ++++------------- .../theory/EquivalenceClassCoverageTest.java | 3 --- .../ralib/theory/SDTEquivalenceTest.java | 3 --- .../inequality/IntervalGuardInstaniateTest.java | 5 ++--- 8 files changed, 9 insertions(+), 42 deletions(-) diff --git a/src/test/java/de/learnlib/ralib/dt/DTTest.java b/src/test/java/de/learnlib/ralib/dt/DTTest.java index 5e312a41..14b39f22 100644 --- a/src/test/java/de/learnlib/ralib/dt/DTTest.java +++ b/src/test/java/de/learnlib/ralib/dt/DTTest.java @@ -22,7 +22,6 @@ import de.learnlib.ralib.oracles.mto.MultiTheorySDTLogicOracle; import de.learnlib.ralib.oracles.mto.MultiTheoryTreeOracle; import de.learnlib.ralib.smt.ConstraintSolver; -import de.learnlib.ralib.theory.SDT; import de.learnlib.ralib.theory.Theory; import de.learnlib.ralib.tools.theories.IntegerEqualityTheory; import de.learnlib.ralib.words.PSymbolInstance; @@ -44,11 +43,6 @@ private DT buildFullTreePrimesOnly(TreeOracle oracle) { SymbolicSuffix suffPop = new SymbolicSuffix(epsilon, prePop); SymbolicSuffix suffPush = new SymbolicSuffix(epsilon, prePush); - SDT tqrPop = oracle.treeQuery(prePop, suffEps); - SDT tqrEps = oracle.treeQuery(epsilon, suffPop); - SDT tqrPush = oracle.treeQuery(prePush, suffPush); - SDT tqrPushPush = oracle.treeQuery(prePushPush, suffPush); - DTInnerNode nodeEps = new DTInnerNode(suffEps); DTInnerNode nodePop = new DTInnerNode(suffPop); DTInnerNode nodePush = new DTInnerNode(suffPush); @@ -97,9 +91,6 @@ private DT buildSimpleTree(TreeOracle oracle) { SymbolicSuffix suffEps = new SymbolicSuffix(epsilon, epsilon); SymbolicSuffix suffPop = new SymbolicSuffix(epsilon, prePop); - SDT tqrPop = oracle.treeQuery(prePop, suffEps); - SDT tqrEps = oracle.treeQuery(epsilon, suffPop); - DTInnerNode nodeEps = new DTInnerNode(suffEps); DTInnerNode nodePop = new DTInnerNode(suffPop); diff --git a/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java b/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java index 9ea4215d..d7a35a4f 100644 --- a/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java +++ b/src/test/java/de/learnlib/ralib/dt/RegisterConsistencyTest.java @@ -9,10 +9,7 @@ import de.learnlib.ralib.RaLibTestSuite; import de.learnlib.ralib.data.*; -import de.learnlib.ralib.data.SymbolicDataValue.Parameter; import de.learnlib.ralib.data.SymbolicDataValue.SuffixValue; -import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.ParameterGenerator; -import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.RegisterGenerator; import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.SuffixValueGenerator; import de.learnlib.ralib.learning.SymbolicSuffix; import de.learnlib.ralib.oracles.Branching; @@ -111,14 +108,10 @@ public void testSymmetry() { SymbolicSuffix symSuffixPrefix = new SymbolicSuffix(prefix, word.suffix(1)); SymbolicSuffix symSuffixExpected = new SymbolicSuffix(prefix, suffixExpected); - RegisterGenerator rgen = new RegisterGenerator(); - ParameterGenerator pgen = new ParameterGenerator(); SuffixValueGenerator svgen = new SuffixValueGenerator(); - Parameter p1 = pgen.next(T_INT); - Parameter p2 = pgen.next(T_INT); DataValue r1 = new DataValue(T_INT, BigDecimal.ZERO); //rgen.next(T_INT); - DataValue r2 = new DataValue(T_INT, BigDecimal.ONE); // rgen.next(T_INT); + DataValue r2 = new DataValue(T_INT, BigDecimal.ONE); //rgen.next(T_INT); SuffixValue s1 = svgen.next(T_INT); SuffixValue s2 = svgen.next(T_INT); diff --git a/src/test/java/de/learnlib/ralib/example/sdts/SDTOracle.java b/src/test/java/de/learnlib/ralib/example/sdts/SDTOracle.java index 7f910abe..8035966d 100644 --- a/src/test/java/de/learnlib/ralib/example/sdts/SDTOracle.java +++ b/src/test/java/de/learnlib/ralib/example/sdts/SDTOracle.java @@ -53,7 +53,6 @@ public void processQueries(Collection> else { Word suffix = computeSuffix(query.getInput()); Mapping vals = computeMapping(suffix); - boolean answer = sdt.isAccepting(vals, consts); query.answer(sdt.isAccepting(vals, consts)); } } diff --git a/src/test/java/de/learnlib/ralib/oracles/mto/SecondSDTBranchingTest.java b/src/test/java/de/learnlib/ralib/oracles/mto/SecondSDTBranchingTest.java index 33a57bb7..b05a1441 100644 --- a/src/test/java/de/learnlib/ralib/oracles/mto/SecondSDTBranchingTest.java +++ b/src/test/java/de/learnlib/ralib/oracles/mto/SecondSDTBranchingTest.java @@ -30,8 +30,6 @@ import de.learnlib.ralib.automata.RegisterAutomaton; import de.learnlib.ralib.automata.xml.RegisterAutomatonImporter; import de.learnlib.ralib.data.*; -import de.learnlib.ralib.data.SymbolicDataValue.Register; -import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.RegisterGenerator; import de.learnlib.ralib.learning.SymbolicSuffix; import de.learnlib.ralib.oracles.Branching; import de.learnlib.ralib.smt.ConstraintSolver; @@ -111,9 +109,11 @@ public void testModelswithOutput2() { SDT tqr1 = mto.treeQuery(prefix, symSuffix1); SDT tqr2 = mto.treeQuery(prefix, symSuffix2); + /* RegisterGenerator rgen = new RegisterGenerator(); Register r1 = rgen.next(intType); Register r2 = rgen.next(intType); + */ SDTRelabeling remap = new SDTRelabeling(); /* remap.put(r1, r2); diff --git a/src/test/java/de/learnlib/ralib/oracles/mto/UntypedBranchingTest.java b/src/test/java/de/learnlib/ralib/oracles/mto/UntypedBranchingTest.java index 30c829d5..a5484777 100644 --- a/src/test/java/de/learnlib/ralib/oracles/mto/UntypedBranchingTest.java +++ b/src/test/java/de/learnlib/ralib/oracles/mto/UntypedBranchingTest.java @@ -28,11 +28,10 @@ import de.learnlib.ralib.TestUtil; import de.learnlib.ralib.automata.RegisterAutomaton; import de.learnlib.ralib.automata.xml.RegisterAutomatonImporter; -import de.learnlib.ralib.data.*; -import de.learnlib.ralib.data.SymbolicDataValue.Parameter; -import de.learnlib.ralib.data.SymbolicDataValue.Register; -import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.ParameterGenerator; -import de.learnlib.ralib.data.util.SymbolicDataValueGenerator.RegisterGenerator; +import de.learnlib.ralib.data.Constants; +import de.learnlib.ralib.data.DataType; +import de.learnlib.ralib.data.DataValue; +import de.learnlib.ralib.data.SDTRelabeling; import de.learnlib.ralib.learning.SymbolicSuffix; import de.learnlib.ralib.oracles.Branching; import de.learnlib.ralib.smt.ConstraintSolver; @@ -106,14 +105,6 @@ public void testBranching() { SDT sdt = res; - ParameterGenerator pgen = new ParameterGenerator(); - RegisterGenerator rgen = new RegisterGenerator(); - - Parameter p1 = pgen.next(intType); - Parameter p2 = pgen.next(intType); - Register r1 = rgen.next(intType); - Register r2 = rgen.next(intType); - SDTRelabeling map = new SDTRelabeling(); sdt = sdt.relabel(map); diff --git a/src/test/java/de/learnlib/ralib/theory/EquivalenceClassCoverageTest.java b/src/test/java/de/learnlib/ralib/theory/EquivalenceClassCoverageTest.java index 29241dde..b7914173 100644 --- a/src/test/java/de/learnlib/ralib/theory/EquivalenceClassCoverageTest.java +++ b/src/test/java/de/learnlib/ralib/theory/EquivalenceClassCoverageTest.java @@ -45,9 +45,6 @@ public void testEqualityTheory() { InputSymbol A = new InputSymbol("a", type); DataValue d0 = new DataValue(type, BigDecimal.ZERO); - DataValue d1 = new DataValue(type, BigDecimal.ONE); - DataValue d2 = new DataValue(type, new BigDecimal(2)); - DataValue d3 = new DataValue(type, new BigDecimal(3)); PSymbolInstance symbol = new PSymbolInstance(A, d0); Word prefix = Word.epsilon(); diff --git a/src/test/java/de/learnlib/ralib/theory/SDTEquivalenceTest.java b/src/test/java/de/learnlib/ralib/theory/SDTEquivalenceTest.java index e94e3ecd..026a18d0 100644 --- a/src/test/java/de/learnlib/ralib/theory/SDTEquivalenceTest.java +++ b/src/test/java/de/learnlib/ralib/theory/SDTEquivalenceTest.java @@ -11,7 +11,6 @@ import de.learnlib.ralib.data.DataType; import de.learnlib.ralib.data.DataValue; import de.learnlib.ralib.data.SymbolicDataValue.SuffixValue; -import de.learnlib.ralib.smt.ConstraintSolver; public class SDTEquivalenceTest extends RaLibTestSuite { @@ -19,7 +18,6 @@ public class SDTEquivalenceTest extends RaLibTestSuite { @Test public void testEquivalence() { - ConstraintSolver solver = new ConstraintSolver(); SuffixValue s1 = new SuffixValue(DT, 1); SuffixValue s2 = new SuffixValue(DT, 2); @@ -65,7 +63,6 @@ public void testEquivalence() { @Test public void testEquivalenceUnderBijection() { - ConstraintSolver solver = new ConstraintSolver(); SuffixValue s1 = new SuffixValue(DT, 1); SuffixValue s2 = new SuffixValue(DT, 2); diff --git a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java index 3982da44..01ed4d07 100644 --- a/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java +++ b/src/test/java/de/learnlib/ralib/theory/inequality/IntervalGuardInstaniateTest.java @@ -32,14 +32,13 @@ public void testInstantiateInterval() { Register r1 = new Register(D_TYPE, 1); Register r2 = new Register(D_TYPE, 2); - DataValue dv0 = new DataValue(D_TYPE, BigDecimal.ZERO); + //DataValue dv0 = new DataValue(D_TYPE, BigDecimal.ZERO); DataValue dv1 = new DataValue(D_TYPE, BigDecimal.ONE); DataValue dv2 = new DataValue(D_TYPE, BigDecimal.valueOf(2)); DataValue dv3 = new DataValue(D_TYPE, BigDecimal.valueOf(3)); - DataValue dv4 = new DataValue(D_TYPE, BigDecimal.valueOf(4)); Valuation val = new Valuation(); - val.setValue(r1 , dv1.getValue()); + val.setValue(r1, dv1.getValue()); val.setValue(r2, dv2.getValue()); Collection alreadyUsed = new ArrayList<>();