Skip to content

Clean up CF definitions #101

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mtf90 merged 4 commits into from
Jan 23, 2026
Merged

Clean up CF definitions #101

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7a0b44d
initial refactoring
mtf90 Jan 5, 2026
2a87153
some more cleanups
mtf90 Jan 22, 2026
e9327aa
cleanups
mtf90 Jan 23, 2026
ed8fd01
Merge branch 'develop' into cf-assert-rework
mtf90 Jan 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions api/src/main/java/net/automatalib/automaton/visualization/ProceduralVisualizationHelper.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,9 @@ protected Collection<Pair<I, S>> initialNodes() {

for (Entry<I, UniversalDeterministicAutomaton<S, I, ?, ?, ?>> e : subModels.entrySet()) {
final S init = e.getValue().getInitialState();
assert init != null;
initialNodes.add(Pair.of(e.getKey(), init));
if (init != null) {
initialNodes.add(Pair.of(e.getKey(), init));
}
}

return initialNodes;
Expand Down
23 changes: 15 additions & 8 deletions build-config/src/main/resources/automatalib-spotbugs-exclusions.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,21 @@ limitations under the License.
</Match>
<Match>
<Bug pattern="NP_NULL_ON_SOME_PATH_FROM_RETURN_VALUE"/>
<And>
<!-- Fine according to JavaDoc -->
<Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
<Or>
<Method name="popBack" returns="java.lang.Object"/>
<Method name="popFront" returns="java.lang.Object"/>
</Or>
</And>
<Or>
<And>
<!-- Fine according to data-flow -->
<Class name="net.automatalib.util.automaton.ads.LeeYannakakis"/>
<Method name="computeValidities"/>
</And>
<And>
<!-- Fine according to JavaDoc -->
<Class name="net.automatalib.common.smartcollection.AbstractLinkedList"/>
<Or>
<Method name="popBack" returns="java.lang.Object"/>
<Method name="popFront" returns="java.lang.Object"/>
</Or>
</And>
</Or>
</Match>
<Match>
<!-- Passing references is mostly fine for performance reasons. Since we do not deal with security-related code,
Expand Down
4 changes: 0 additions & 4 deletions build-parent/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,6 @@ limitations under the License.
<goal>compile</goal>
</goals>
<configuration>
<failOnWarning>true</failOnWarning>
<fork>true</fork>
<outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
<annotationProcessorPaths combine.children="append">
Expand Down Expand Up @@ -273,7 +272,6 @@ limitations under the License.
</arg>
<arg>-AskipUses=^java.(awt.*|util.(Arrays|Map|ArrayDeque)|io.StreamTokenizer)|^javax.swing.*</arg>
<arg>-AsuppressWarnings=uninitialized</arg>
<arg>-AassumeAssertionsAreEnabled</arg>
<arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
</compilerArgs>
</configuration>
Expand All @@ -285,7 +283,6 @@ limitations under the License.
<goal>testCompile</goal>
</goals>
<configuration>
<failOnWarning>true</failOnWarning>
<fork>true</fork>
<outputDirectory>${project.build.directory}/checkerframework</outputDirectory>
<annotationProcessorPaths combine.children="append">
Expand All @@ -311,7 +308,6 @@ limitations under the License.
<arg>-AonlyDefs=^net\.automatalib</arg>
<arg>-AskipUses=.*</arg>
<arg>-AsuppressWarnings=uninitialized</arg>
<arg>-AassumeAssertionsAreEnabled</arg>
<arg>-Astubs=collection-object-parameters-may-be-null.astub</arg>
</compilerArgs>
</configuration>
Expand Down
2 changes: 2 additions & 0 deletions ...artcollections/src/main/java/net/automatalib/common/smartcollection/ReflexiveMapView.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ public class ReflexiveMapView<T> extends AbstractMap<T, T> {

private final Set<@KeyFor("this") T> domain;

@SuppressWarnings("type") // the provided items become keys for this map view
public ReflexiveMapView(Set<T> domain) {
this.domain = Collections.unmodifiableSet(domain);
}
Expand Down Expand Up @@ -68,6 +69,7 @@ public boolean containsKey(@Nullable Object key) {
}

@Override
@SuppressWarnings("return") // it is okay that values are also keys for this map
public Set<T> values() {
return this.domain;
}
Expand Down
6 changes: 4 additions & 2 deletions core/src/main/java/net/automatalib/automaton/mmlt/impl/DefaultMMLTSemantics.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimedOutput;
import net.automatalib.symbol.time.TimeoutSymbol;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
Expand Down Expand Up @@ -132,8 +133,9 @@ public MealyTransition<State<S, O>, TimedOutput<O>> getTransition(State<S, O> so
}
}

assert lastOutput != null;
return new MealyTransition<>(currentConfig, new TimedOutput<>(lastOutput));
@SuppressWarnings("nullness") // since remainingTime must be > 0, the while loop iterates at least once
final @NonNull O output = lastOutput;
return new MealyTransition<>(currentConfig, new TimedOutput<>(output));
} else {
throw new IllegalArgumentException("Unknown input symbol type");
}
Expand Down
2 changes: 1 addition & 1 deletion core/src/main/java/net/automatalib/automaton/procedural/impl/StackSPA.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ public StackSPA(ProceduralInputAlphabet<I> alphabet,
}

@Override
public StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
public @Nullable StackState<S, I, DFA<S, I>> getTransition(StackState<S, I, DFA<S, I>> state, I input) {
if (state.isTerm()) {
return null;
} else if (alphabet.isInternalSymbol(input)) {
Expand Down
8 changes: 4 additions & 4 deletions core/src/main/java/net/automatalib/automaton/procedural/impl/StackState.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@
*/
package net.automatalib.automaton.procedural.impl;

import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
Expand Down Expand Up @@ -54,21 +53,25 @@ StackState<S, I, P> push(P newProcedure, S newState) {
return new StackState<>(this, newProcedure, newState);
}

@SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
StackState<S, I, P> pop() {
assert !isStatic() : "This method should never be called on static states";
return prev;
}

@SuppressWarnings("type") // since this method is package-private, we are happy to only assert nullability
StackState<S, I, P> updateState(S state) {
assert !isStatic() : "This method should never be called on static states";
return new StackState<>(prev, procedure, state);
}

@SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
P getProcedure() {
assert !isStatic() : "This method should never be called on static states";
return procedure;
}

@SuppressWarnings("return") // since this method is package-private, we are happy to only assert nullability
S getCurrentState() {
assert !isStatic() : "This method should never be called on static states";
return procedureState;
Expand All @@ -92,9 +95,6 @@ boolean isTerm() {
return this == TERM;
}

// contract is satisfied by definition of constructors
@SuppressWarnings("contracts.conditional.postcondition")
@EnsuresNonNullIf(expression = {"this.prev", "this.procedure", "this.procedureState"}, result = false)
private boolean isStatic() {
return isInit() || isTerm();
}
Expand Down
9 changes: 5 additions & 4 deletions examples/src/main/java/net/automatalib/example/graph/DFSExample.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@
import net.automatalib.visualization.Visualization;
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.visualization.VisualizationHelper.EdgeStyles;
import org.checkerframework.checker.nullness.qual.NonNull;

/**
* A small example of a {@link GraphTraversal graph traversal} that uses a custom {@link GraphTraversalVisitor} to
Expand Down Expand Up @@ -168,16 +169,16 @@ static class DFSResultDOTHelper<N, E> implements VisualizationHelper<N, E> {
@Override
public boolean getNodeProperties(N node, Map<String, String> properties) {
String lbl = properties.get(NodeAttrs.LABEL);
DFSData record = records.get(node);
assert record != null;
@SuppressWarnings("nullness") // we have traversed all nodes before
@NonNull DFSData record = records.get(node);
properties.put(NodeAttrs.LABEL, lbl + " [#" + record.dfsNumber + "]");
return true;
}

@Override
public boolean getEdgeProperties(N src, E edge, N tgt, Map<String, String> properties) {
EdgeType et = edgeTypes.get(edge);
assert et != null;
@SuppressWarnings("nullness") // we have traversed all nodes before
@NonNull EdgeType et = edgeTypes.get(edge);
properties.put(EdgeAttrs.STYLE, et.getStyle());
properties.remove(EdgeAttrs.LABEL);
return true;
Expand Down
8 changes: 5 additions & 3 deletions incremental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalDFADAGBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
import net.automatalib.incremental.ConflictException;
import net.automatalib.incremental.dfa.Acceptance;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
Expand Down Expand Up @@ -74,7 +75,6 @@ public Acceptance lookup(Word<? extends I> word) {
*/
@Override
public void insert(Word<? extends I> word, boolean accepting) {
int len = word.length();
Acceptance acc = Acceptance.fromBoolean(accepting);

State curr = init;
Expand All @@ -99,6 +99,7 @@ public void insert(Word<? extends I> word, boolean accepting) {
curr = succ;
}

int len = word.length();
int prefixLen = path.size();

State last = curr;
Expand Down Expand Up @@ -139,8 +140,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
// confluence always requires cloning, to separate this path from other paths
last = hiddenClone(last);
if (conf == null) {
Transition peek = path.peek();
assert peek != null;
// the root node is never confluent so in this context, the path always contains at least one node
@SuppressWarnings("nullness")
@NonNull Transition peek = path.peek();
State prev = peek.state;
if (prev == init) {
updateInitSignature(peek.transIdx, last);
Expand Down
6 changes: 4 additions & 2 deletions ...emental/src/main/java/net/automatalib/incremental/dfa/dag/IncrementalPCDFADAGBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
import net.automatalib.incremental.ConflictException;
import net.automatalib.incremental.dfa.Acceptance;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.NonNull;

/**
* The prefix-closed version of {@link IncrementalDFADAGBuilder}. Contrary to the regular lookup semantics, where an
Expand Down Expand Up @@ -145,8 +146,9 @@ public void insert(Word<? extends I> word, boolean accepting) {
}
last = hiddenClone(last);
if (conf == null) {
Transition peek = path.peek();
assert peek != null;
// the root node is never confluent so in this context, the path always contains at least one node
@SuppressWarnings("nullness")
@NonNull Transition peek = path.peek();
State prev = peek.state;
if (prev == init) {
updateInitSignature(peek.transIdx, last);
Expand Down
6 changes: 4 additions & 2 deletions ...ental/src/main/java/net/automatalib/incremental/mealy/dag/IncrementalMealyDAGBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
import net.automatalib.visualization.VisualizationHelper;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
Expand Down Expand Up @@ -181,8 +182,9 @@ public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
}
last = hiddenClone(last);
if (conf == null) {
Transition<O> peek = path.peek();
assert peek != null;
// the root node is never confluent so in this context, the path always contains at least one node
@SuppressWarnings("nullness")
@NonNull Transition<O> peek = path.peek();
State<O> prev = peek.state;
if (prev == init) {
updateInitSignature(peek.transIdx, last);
Expand Down
12 changes: 8 additions & 4 deletions ...ental/src/main/java/net/automatalib/incremental/moore/dag/IncrementalMooreDAGBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
Expand Down Expand Up @@ -201,8 +202,9 @@ public void insert(Word<? extends I> word, Word<? extends O> outputWord) {
}
last = hiddenClone(last);
if (conf == null) {
Transition<O> peek = path.peek();
assert peek != null;
// the root node is never confluent so in this context, the path always contains at least one node
@SuppressWarnings("nullness")
@NonNull Transition<O> peek = path.peek();
State<O> prev = peek.state;
if (prev == init) {
updateInitSignature(peek.transIdx, last);
Expand Down Expand Up @@ -342,7 +344,8 @@ private State<O> updateSignature(State<O> state, int idx, State<O> succ) {
* the new successor state
*/
private void updateInitSignature(int idx, State<O> succ) {
assert init != null;
@SuppressWarnings("nullness") // this internal method is only called after the root node has been initialized
@NonNull State<O> init = this.init;
StateSignature<O> sig = init.getSignature();
State<O> oldSucc = sig.successors.get(idx);
if (oldSucc == succ) {
Expand All @@ -366,7 +369,8 @@ private void updateInitSignature(int idx, State<O> succ) {
* the output symbol
*/
private void updateInitSignature(int idx, State<O> succ, O out) {
assert init != null;
@SuppressWarnings("nullness") // this internal method is only called after the root node has been initialized
@NonNull State<O> init = this.init;
StateSignature<O> sig = init.getSignature();
State<O> oldSucc = sig.successors.get(idx);
if (oldSucc == succ && Objects.equals(out, succ.getOutput())) {
Expand Down
4 changes: 2 additions & 2 deletions ...lchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/AbstractDDSolver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -418,8 +418,8 @@ private <E> T getEdgeTransformer(WorkUnit<?, E> unit, E edge) {
final ProceduralModalProcessGraph<?, L, E, AP, ?> pmpg = unit.pmpg;
final L label = pmpg.getEdgeLabel(edge);
if (isProcessEdge(pmpg, edge)) {
final WorkUnit<?, ?> edgeUnit = workUnits.get(label);
assert edgeUnit != null;
@SuppressWarnings("nullness") // we constructed work units based on labels
final @NonNull WorkUnit<?, ?> edgeUnit = workUnits.get(label);
edgeTransformer = getInitialEdgeTransformer(edgeUnit);
} else {
if (isMustEdge(pmpg, edge)) {
Expand Down
5 changes: 2 additions & 3 deletions modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTree.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,9 @@ public class WitnessTree<L, AP> extends CompactUniversalGraph<WitnessTreeState<?

private @MonotonicNonNull Word<L> result;

@SuppressWarnings("nullness") // the witness tree is returned only after the path has been computed
public Word<L> getWitness() {
assert result != null;
return result;
return this.result;
}

void computePath(int finishingNode) {
Expand All @@ -50,7 +50,6 @@ void computePath(int finishingNode) {

while (currentNode >= 0) {
final WitnessTreeState<?, L, ?, AP> prop = super.getNodeProperty(currentNode);
assert prop != null;

final L label = prop.edgeLabel;
prop.isPartOfResult = true;
Expand Down
18 changes: 9 additions & 9 deletions ...cking/m3c/src/main/java/net/automatalib/modelchecker/m3c/solver/WitnessTreeExtractor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,8 +81,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
FormulaNode<L, AP> formula) {

final Deque<WitnessTreeState<?, L, ?, AP>> queue = new ArrayDeque<>();
final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> mainUnit = units.get(cfmps.getMainProcess());
assert mainUnit != null;
@SuppressWarnings("nullness") // we constructed work units based on all labels
final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> mainUnit = units.get(cfmps.getMainProcess());
final WitnessTreeState<?, L, ?, AP> init = getInitialTreeState(mainUnit, formula);

queue.add(init);
Expand Down Expand Up @@ -167,7 +167,6 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
private <N> List<WitnessTreeState<?, L, ?, AP>> exploreDia(DiamondNode<L, AP> formula,
WitnessTreeState<N, L, ?, AP> queueElement) {
if (Objects.equals(queueElement.state, queueElement.pmpg.getFinalNode())) {
assert queueElement.stack != null;
return findDiaMoveEndNodeReturn(queueElement);
} else if (formula.getAction() == null) {
return findDiaMoveWithEmpty(queueElement, formula);
Expand Down Expand Up @@ -199,8 +198,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
result.add(toAdd);
}
} else {
final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> unit = units.get(label);
assert unit != null;
@SuppressWarnings("nullness") // we constructed work units based on all labels
final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> unit = units.get(label);
final WitnessTreeState<?, L, ?, AP> toAdd =
buildProcessNode(queueElement, unit, label, target, formula);

Expand All @@ -215,8 +214,9 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A

private <N, E> List<WitnessTreeState<?, L, ?, AP>> findDiaMoveEndNodeReturn(WitnessTreeState<N, L, E, AP> queueElement) {

assert queueElement.stack != null;
final WitnessTreeState<?, L, ?, AP> toAdd = buildReturnNode(queueElement, queueElement.stack);
@SuppressWarnings("nullness") // only the root node has no stack and it will never be mapped to a final/end node
@NonNull WitnessTreeState<?, L, ?, AP> prev = queueElement.stack;
final WitnessTreeState<?, L, ?, AP> toAdd = buildReturnNode(queueElement, prev);

return Collections.singletonList(toAdd);
}
Expand Down Expand Up @@ -245,8 +245,8 @@ private WitnessTree<L, AP> computeWitnessStep(ContextFreeModalProcessSystem<L, A
result.add(toAdd);
}
} else {
final AbstractDDSolver<?, L, AP>.WorkUnit<?, ?> unit = units.get(label);
assert unit != null;
@SuppressWarnings("nullness") // we constructed work units based on all labels
final AbstractDDSolver<?, L, AP>.@NonNull WorkUnit<?, ?> unit = units.get(label);
final WitnessTreeState<?, L, ?, AP> toAdd =
buildProcessNode(queueElement, unit, label, target, formula);

Expand Down
Loading