11.08., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

automatic code clean-up

parent ecaf55bd
......@@ -64,7 +64,7 @@ public final class HashMapAutomaton<S, A extends OmegaAcceptance> implements
private Map<S, S> uniqueStates;
private final ValuationSetFactory valuationSetFactory;
@Nullable
private String name = null;
private String name;
private State state = State.READ;
HashMapAutomaton(ValuationSetFactory valuationSetFactory, A acceptance) {
......
......@@ -346,7 +346,7 @@ public class GeneralizedRabinAcceptance extends OmegaAcceptance {
public static final class Builder {
private final List<RabinPair> pairs = new ArrayList<>();
private int sets = 0;
private int sets;
public RabinPair add(@Nonnegative int infSets) {
RabinPair pair = new RabinPair(sets, sets + infSets);
......
......@@ -119,7 +119,7 @@ public final class RabinAcceptance extends GeneralizedRabinAcceptance {
public static final class Builder {
private final List<RabinPair> pairs = new ArrayList<>(); // NOPMD
private int sets = 0;
private int sets;
public RabinPair add() {
RabinPair pair = new RabinPair(sets, sets + 1);
......
......@@ -45,7 +45,7 @@ final class Tarjan<S> {
private final Set<S> processedNodes = new HashSet<>();
private final Map<S, TarjanState<S>> stateMap = new HashMap<>();
private final SuccessorFunction<S> successorFunction;
private int index = 0;
private int index;
Tarjan(SuccessorFunction<S> successorFunction, Predicate<? super Set<S>> earlyTermination) {
this.successorFunction = successorFunction;
......
......@@ -23,7 +23,6 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
......@@ -37,15 +36,16 @@ import owl.util.BitSetUtil;
public class BackwardDirectSimulation<S>
implements SimulationType<S, MultipebbleSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
MultipebbleSimulationState<S> initialState;
MultipebbleSimulationState<S> sinkState;
int pebbleCount;
Set<Pair<S, S>> knownPairs;
final Automaton<S, BuchiAcceptance> leftAutomaton;
final Automaton<S, BuchiAcceptance> rightAutomaton;
final ValuationSetFactory factory;
final S leftState;
final S rightState;
final MultipebbleSimulationState<S> initialState;
final MultipebbleSimulationState<S> sinkState;
final int pebbleCount;
final Set<Pair<S, S>> knownPairs;
public BackwardDirectSimulation(
Automaton<S, BuchiAcceptance> leftAutomaton,
......@@ -127,20 +127,16 @@ public class BackwardDirectSimulation<S>
return out;
}
predecessors.forEach(pred -> {
leftAutomaton.edgeMap(pred).forEach((e, vS) -> {
if (e.successor().equals(state.odd().state())) {
vS.forEach(val -> {
state.odd().predecessors(leftAutomaton, val).forEach(p -> {
var target = MultipebbleSimulationState.of(
p, state.even().setFlag(false), val
);
out.put(Edge.of(target, 0), factory.universe());
});
});
}
});
});
predecessors.forEach(pred -> leftAutomaton.edgeMap(pred).forEach((e, vS) -> {
if (e.successor().equals(state.odd().state())) {
vS.forEach(val -> state.odd().predecessors(leftAutomaton, val).forEach(p -> {
var target = MultipebbleSimulationState.of(
p, state.even().setFlag(false), val
);
out.put(Edge.of(target, 0), factory.universe());
}));
}
}));
} else {
var possibilities = state.even()
.predecessors(leftAutomaton, BitSetUtil.fromInt(state.valuation()));
......
......@@ -23,7 +23,6 @@ import static owl.translations.nbadet.NbaDet.overrideLogLevel;
import static owl.translations.nbadet.NbaDet.restoreLogLevel;
import com.google.common.collect.Sets;
import java.io.IOException;
import java.util.HashMap;
import java.util.HashSet;
......@@ -36,7 +35,6 @@ import java.util.logging.Handler;
import java.util.logging.Level;
import java.util.logging.Logger;
import java.util.stream.Collectors;
import owl.automaton.Automaton;
import owl.automaton.Views;
import owl.automaton.acceptance.BuchiAcceptance;
......@@ -529,8 +527,8 @@ public final class BuchiSimulation {
}
private static class SimulationStats {
public long computationTime;
public int graphSize;
public final long computationTime;
public final int graphSize;
private SimulationStats(long ct, int gs) {
computationTime = ct;
......
......@@ -20,7 +20,6 @@
package owl.automaton.algorithm.simulations;
import com.google.auto.value.AutoValue;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.Option;
import org.apache.commons.cli.Options;
......@@ -93,7 +92,7 @@ public abstract class BuchiSimulationArguments {
.desc("Use logging level FINE for more output")
.build();
public static Options options = new Options()
public static final Options options = new Options()
.addOption(optDirect)
.addOption(optVerboseFine)
.addOption(optDelayed)
......
......@@ -20,7 +20,6 @@
package owl.automaton.algorithm.simulations;
import com.google.auto.value.AutoValue;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.Collection;
......@@ -30,7 +29,6 @@ import java.util.Map;
import java.util.Set;
import java.util.concurrent.atomic.AtomicBoolean;
import java.util.stream.Collectors;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.collections.Pair;
......@@ -45,14 +43,14 @@ import owl.util.BitSetUtil;
* @param <S> Type of state for the underlying automaton.
*/
public class ColorRefinement<S> {
Automaton<S, BuchiAcceptance> aut;
ValuationSetFactory factory;
final Automaton<S, BuchiAcceptance> aut;
final ValuationSetFactory factory;
Ordering po;
final Ordering po;
Ordering oldPo;
Coloring<S> col;
final Coloring<S> col;
Coloring<S> oldCol;
Map<S, Pair<Integer, Neighborhood>> intermediate;
final Map<S, Pair<Integer, Neighborhood>> intermediate;
private ColorRefinement(Automaton<S, BuchiAcceptance> automaton) {
aut = automaton;
......@@ -155,7 +153,6 @@ public class ColorRefinement<S> {
Map<Pair<ValuationSet, ValuationSet>, Integer> intermC = new HashMap<>();
Map<ValuationSet, Integer> setColouring = new HashMap<>();
Map<Integer, Pair<ValuationSet, ValuationSet>> rIntermC = new HashMap<>();
Map<Integer, ValuationSet> colouringSet = new HashMap<>();
// we iterate over all states and possible valuations to create something like a transition
// profile for each state. We collect all symbols on which an accepting transition is available
......@@ -186,7 +183,6 @@ public class ColorRefinement<S> {
int i = 0;
for (var set : maxAcceptingVal.values()) {
if (!setColouring.containsKey(set)) {
colouringSet.put(i, set);
setColouring.put(set, i++);
}
}
......@@ -203,9 +199,9 @@ public class ColorRefinement<S> {
interm.forEach((key, value) -> col.set(key, intermC.get(value)));
for (int c : col.values()) {
for (var key : rIntermC.keySet()) {
for (Map.Entry<Integer, Pair<ValuationSet, ValuationSet>> entry : rIntermC.entrySet()) {
var p1 = rIntermC.get(c);
var p2 = rIntermC.get(key);
var p2 = entry.getValue();
AtomicBoolean contained = new AtomicBoolean(true);
p1.fst().forEach(val -> {
if (!p2.fst().contains(val)) {
......@@ -214,7 +210,7 @@ public class ColorRefinement<S> {
});
if (contained.get()
&& aut.factory().implies(p1.snd(), p2.snd())) {
po.set(c, key);
po.set(c, entry.getKey());
}
}
}
......@@ -480,8 +476,8 @@ public class ColorRefinement<S> {
@Override
public String toString() {
StringBuilder sb = new StringBuilder();
for (var s : col.keySet()) {
sb.append(s).append(" -> ").append(col.get(s)).append('\n');
for (Map.Entry<S, Integer> entry : col.entrySet()) {
sb.append(entry.getKey()).append(" -> ").append(entry.getValue()).append('\n');
}
return sb.toString();
}
......@@ -559,8 +555,8 @@ public class ColorRefinement<S> {
public String toString() {
StringBuilder sb = new StringBuilder();
sb.append("ordering size: ").append(size()).append('\n');
for (var key : ord.keySet()) {
sb.append(key).append(" <= ").append(ord.get(key)).append('\n');
for (Map.Entry<Integer, Set<Integer>> entry : ord.entrySet()) {
sb.append(entry.getKey()).append(" <= ").append(entry.getValue()).append('\n');
}
return sb.toString();
}
......
......@@ -23,7 +23,6 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
......@@ -37,16 +36,17 @@ import owl.util.BitSetUtil;
public class ForwardDelayedSimulation<S>
implements SimulationType<S, MultipebbleSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
MultipebbleSimulationState<S> initialState;
MultipebbleSimulationState<S> sinkState;
int pebbleCount;
Set<Pair<S, S>> knownPairs;
Set<MultipebbleSimulationState<S>> stateSet;
final Automaton<S, BuchiAcceptance> leftAutomaton;
final Automaton<S, BuchiAcceptance> rightAutomaton;
final ValuationSetFactory factory;
final S leftState;
final S rightState;
final MultipebbleSimulationState<S> initialState;
final MultipebbleSimulationState<S> sinkState;
final int pebbleCount;
final Set<Pair<S, S>> knownPairs;
final Set<MultipebbleSimulationState<S>> stateSet;
public ForwardDelayedSimulation(
Automaton<S, BuchiAcceptance> leftAutomaton,
......
......@@ -24,7 +24,6 @@ import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
......@@ -37,15 +36,15 @@ import owl.run.Environment;
public class ForwardDirectLookaheadSimulation<S>
implements SimulationType<S, LookaheadSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
LookaheadSimulationState<S> initialState;
LookaheadSimulationState<S> sinkState;
Set<Pair<S, S>> knownPairs;
int maxLookahead;
final Automaton<S, BuchiAcceptance> leftAutomaton;
final Automaton<S, BuchiAcceptance> rightAutomaton;
final ValuationSetFactory factory;
final S leftState;
final S rightState;
final LookaheadSimulationState<S> initialState;
final LookaheadSimulationState<S> sinkState;
final Set<Pair<S, S>> knownPairs;
final int maxLookahead;
public ForwardDirectLookaheadSimulation(
Automaton<S, BuchiAcceptance> leftAutomaton,
......
......@@ -24,7 +24,6 @@ import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
......@@ -43,15 +42,15 @@ import owl.util.BitSetUtil;
*/
public class ForwardDirectSimulation<S>
implements SimulationType<S, SimulationStates.MultipebbleSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
MultipebbleSimulationState<S> initialState;
SimulationStates.MultipebbleSimulationState<S> sinkState;
int pebbleCount;
Set<Pair<S, S>> knownPairs;
final Automaton<S, BuchiAcceptance> leftAutomaton;
final Automaton<S, BuchiAcceptance> rightAutomaton;
final ValuationSetFactory factory;
final S leftState;
final S rightState;
final MultipebbleSimulationState<S> initialState;
final SimulationStates.MultipebbleSimulationState<S> sinkState;
final int pebbleCount;
final Set<Pair<S, S>> knownPairs;
/**
* Constructs a simulation game for two given automata and two states.
......
......@@ -23,7 +23,6 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import owl.automaton.Automaton;
import owl.automaton.acceptance.BuchiAcceptance;
import owl.automaton.acceptance.ParityAcceptance;
......@@ -37,16 +36,16 @@ import owl.util.BitSetUtil;
public class ForwardFairSimulation<S>
implements SimulationType<S, SimulationStates.MultipebbleSimulationState<S>> {
Automaton<S, BuchiAcceptance> leftAutomaton;
Automaton<S, BuchiAcceptance> rightAutomaton;
ValuationSetFactory factory;
S leftState;
S rightState;
MultipebbleSimulationState<S> initialState;
MultipebbleSimulationState<S> sinkState;
int pebbleCount;
Set<Pair<S, S>> knownPairs;
Set<MultipebbleSimulationState<S>> stateSet;
final Automaton<S, BuchiAcceptance> leftAutomaton;
final Automaton<S, BuchiAcceptance> rightAutomaton;
final ValuationSetFactory factory;
final S leftState;
final S rightState;
final MultipebbleSimulationState<S> initialState;
final MultipebbleSimulationState<S> sinkState;
final int pebbleCount;
final Set<Pair<S, S>> knownPairs;
final Set<MultipebbleSimulationState<S>> stateSet;
public ForwardFairSimulation(
Automaton<S, BuchiAcceptance> leftAutomaton,
......
......@@ -42,7 +42,7 @@ import owl.game.Game;
public class SimulationGame<S, T extends SimulationState<S>> implements
Game<T, ParityAcceptance>,
EdgeMapAutomatonMixin<T, ParityAcceptance> {
SimulationType<S, T> simulationType;
final SimulationType<S, T> simulationType;
public SimulationGame(SimulationType<S, T> type) {
simulationType = type;
......
......@@ -58,7 +58,7 @@ public class SimulationStates {
public String toString() {
return (owner().isOdd() ? "O: " : "E: ")
+ odd().toString()
+ "|"
+ '|'
+ even().toString()
+ (moves().isEmpty() ? "" : moves().toString());
}
......@@ -135,9 +135,9 @@ public class SimulationStates {
public String toString() {
return (owner().isOdd() ? "O: " : "E: ")
+ odd().toString()
+ "|"
+ '|'
+ even().toString()
+ " "
+ ' '
+ valuation();
}
}
......
......@@ -134,7 +134,7 @@ public abstract class Transition<S> {
@Override
public String toString() {
return "-" + (flag() ? ">>" : ">") + target();
return '-' + (flag() ? ">>" : ">") + target();
}
public boolean isValid(S base, Automaton<S, BuchiAcceptance> aut) {
......
......@@ -92,7 +92,7 @@ public final class HoaWriter {
private final EnumSet<HoaOption> options;
private final Object2IntMap<S> stateNumbers;
@Nullable
private S currentState = null;
private S currentState;
final Visitor visitor = new Visitor();
Wrapper(HOAConsumer consumer, List<String> aliases, OmegaAcceptance acceptance,
......
......@@ -304,7 +304,7 @@ public final class GfgCoBuchiMinimization {
}
enum EdgeType {
ACCEPTING, REJECTING, UNKNOWN;
ACCEPTING, REJECTING, UNKNOWN
}
private static <S> int componentId(S state, List<Set<S>> components) {
......
......@@ -145,8 +145,8 @@ public final class Collections3 {
@Override
public Iterator<E> iterator() {
return new Iterator<>() {
Iterator<E> iterator = set.iterator();
boolean elementReturned = false;
final Iterator<E> iterator = set.iterator();
boolean elementReturned;
@Override
public boolean hasNext() {
......
......@@ -20,7 +20,6 @@
package owl.collections;
import com.google.auto.value.AutoValue;
import java.util.HashSet;
import java.util.Set;
import java.util.function.Function;
......@@ -51,20 +50,20 @@ public abstract class NullablePair<A, B> {
return pairs;
}
public Pair<B,A> swap() {
return Pair.of(snd(), fst());
public NullablePair<B,A> swap() {
return NullablePair.of(snd(), fst());
}
public <C> Pair<C,B> mapFst(Function<A,C> fun) {
return Pair.<C,B>of(fun.apply(fst()), snd());
public <C> NullablePair<C,B> mapFst(Function<A,C> fun) {
return NullablePair.of(fun.apply(fst()), snd());
}
public <C> Pair<A,C> mapSnd(Function<B,C> fun) {
return Pair.<A,C>of(fst(), fun.apply(snd()));
public <C> NullablePair<A,C> mapSnd(Function<B,C> fun) {
return NullablePair.of(fst(), fun.apply(snd()));
}
@Override
public String toString() {
return "(" + fst() + "," + snd() + ")";
return "(" + fst() + ',' + snd() + ')';
}
}
......@@ -20,7 +20,6 @@
package owl.collections;
import com.google.auto.value.AutoValue;
import java.util.HashSet;
import java.util.Objects;
import java.util.Set;
......@@ -56,15 +55,15 @@ public abstract class Pair<A, B> {
}
public <C> Pair<C,B> mapFst(Function<A,C> fun) {
return Pair.<C,B>of(fun.apply(fst()), snd());
return Pair.of(fun.apply(fst()), snd());
}
public <C> Pair<A,C> mapSnd(Function<B,C> fun) {
return Pair.<A,C>of(fst(), fun.apply(snd()));
return Pair.of(fst(), fun.apply(snd()));
}
@Override
public String toString() {
return "(" + fst() + "," + snd() + ")";
return "(" + fst() + ',' + snd() + ')';
}
}
......@@ -32,9 +32,9 @@ import javax.annotation.Nullable;
*/
public class TrieMap<K,V> {
@Nullable
private V value = null;
private V value;
public Map<K, TrieMap<K,V>> suc = new HashMap<>();
public final Map<K, TrieMap<K,V>> suc = new HashMap<>();
/** Returns a fresh empty trie. */
public static <K,V> TrieMap<K,V> create() {
......@@ -61,7 +61,7 @@ public class TrieMap<K,V> {
/** Put value at provided key position. Will replace existing. */
public void put(List<K> ks, V val) {
var curr = traverse(ks, true).get(); //safe to do, as we create if missing
var curr = traverse(ks, true).orElseThrow(); //safe to do, as we create if missing
curr.value = val;
}
......
......@@ -36,7 +36,7 @@ public final class JBddSupplier implements FactorySupplier {
return INSTANCE;
}
private Bdd create(int size) {
private static Bdd create(int size) {
var configuration = ImmutableBddConfiguration.builder()
.logStatisticsOnShutdown(false)
.useGlobalComposeCache(false)
......
......@@ -107,7 +107,6 @@ public final class GameFactory {
Map<Edge<S>, ValuationSet> labelledEdges = new HashMap<>();
graph.edges().stream().filter(x -> x.source().equals(state)).forEach(x -> {
//noinspection ConstantConditions
ValueEdge valueEdge = graph.edgeValue(x.source(), x.target()).get();
Edge<S> edge = valueEdge.colour() == -1
? Edge.of(x.target())
......
......@@ -48,7 +48,6 @@ public final class GameUtil {
"pg-solver",
"Writes the given max even parity game in PG Solver format",
(commandLine, environment) -> (writer, input) -> {
//noinspection resource,IOResourceOpenedButNotSafelyClosed
PrintWriter printStream = writer instanceof PrintWriter
? (PrintWriter) writer
: new PrintWriter(writer, true);
......
......@@ -26,7 +26,6 @@ import javax.annotation.Nullable;
@AutoValue
public abstract class Aig {
@SuppressWarnings("StaticInitializerReferencesSubClass")
public static final Aig FALSE = new AutoValue_Aig(0, null, false, null, false);
public abstract int variable();
......
......@@ -47,7 +47,7 @@ public final class Disjunction extends Formula.NaryPropositionalOperator {
// Internal constructor.
@SuppressWarnings("PMD.UnusedFormalParameter")
private Disjunction(List<? extends Formula> disjuncts, @Nullable Void internal) {
super(Conjunction.class, List.copyOf(disjuncts));
super(Disjunction.class, List.copyOf(disjuncts));
}
public static Formula of(Formula e1, Formula e2) {
......
......@@ -235,7 +235,7 @@ public final class NormalForms {
@Override
public Iterator<Set<Formula>> iterator() {
return new Iterator<>() {
Iterator<BitSet> internalIterator = clauses.iterator();
final Iterator<BitSet> internalIterator = clauses.iterator();
@Override
public boolean hasNext() {
......
......@@ -69,8 +69,8 @@ public final class PrintVisitor implements Visitor<String> {
@Override
public String visit(Biconditional biconditional) {
return "(" + visitParenthesized(biconditional.leftOperand())
+ " <-> " + visitParenthesized(biconditional.rightOperand()) + ")";
return '(' + visitParenthesized(biconditional.leftOperand())
+ " <-> " + visitParenthesized(biconditional.rightOperand()) + ')';
}
@Override
......
......@@ -92,7 +92,6 @@ public final class DefaultCli {
}
String destination = settings.getOptionValue("fileout");
@SuppressWarnings("resource")
WritableByteChannel writer = destination == null || "-".equals(destination)
? Channels.newChannel(GuardedStream.sysout)
: Files.newByteChannel(Paths.get(destination),
......@@ -103,7 +102,6 @@ public final class DefaultCli {
}
}
@SuppressWarnings("resource")
private static ReadableByteChannel createReader(List<String> inputs) {
// Build the byte array now, since the inputs list may get cleared after this call.
StringJoiner joiner = new StringJoiner(System.lineSeparator());
......
......@@ -20,6 +20,7 @@
package owl.run.modules;
import java.util.Collection;
import java.util.EnumMap;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
......@@ -179,7 +180,7 @@ public class OwlModuleRegistry {
}
public Map<Type, OwlModule<?>> get(String name) {
Map<Type, OwlModule<?>> types = new HashMap<>();
Map<Type, OwlModule<?>> types = new EnumMap<>(Type.class);
var reader = readers.get(name);
......@@ -232,7 +233,7 @@ public class OwlModuleRegistry {
}
public enum Type {
READER, TRANSFORMER, WRITER;
READER, TRANSFORMER, WRITER
}
public static class OwlModuleNotFoundException extends Exception {
......
......@@ -50,7 +50,6 @@ public final class OwlParser {
this.globalSettings = globalSettings;
}
@SuppressWarnings("NestedTryStatement")
@Nullable
public static OwlParser parse(String[] arguments, CommandLineParser cliParser,
Options globalOptions, OwlModuleRegistry registry) {
......