From a9a1dd8c73c504ecfaf0569e76227fd231c7f770 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 17:14:56 +0000 Subject: [PATCH 1/5] Suggest only calls allowed in any state when the receiver's state is unknown With an unknown state, the hint listed every transition into the states the call needs, even when the transition needed a state that was just as unknown, and named those states in every combination with the state sets the call does not check. It now names the needed state in the checked state sets only, and suggests the shortest call sequences that are allowed in every state. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateHintKnownAnyState.java | 31 ++++++++ .../ErrorStateHintUnknownAnyState.java | 28 ++++++++ .../ErrorStateHintUnknownDisjunction.java | 26 +++++++ .../testSuite/ErrorStateHintUnknownField.java | 30 ++++++++ .../ErrorStateHintUnknownThreeSets.java | 27 +++++++ .../ErrorStateHintUnknownTwoSetGoal.java | 29 ++++++++ .../state_hint_undo_manager_error/Editor.java | 15 ++++ .../UndoManagerRefinements.java | 26 +++++++ .../liquidjava/diagnostics/hints/Hint.java | 4 +- .../diagnostics/hints/StateHints.java | 70 ++++++++++++++----- .../processor/state_machine/State.java | 6 ++ .../processor/state_machine/StateMachine.java | 22 ++++-- .../liquidjava/api/tests/TestStateHints.java | 58 ++++++++++++++- .../state_machine/StateMachineTest.java | 55 +++++++++++++++ 14 files changed, 399 insertions(+), 28 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java new file mode 100644 index 00000000..64bd2e04 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java @@ -0,0 +1,31 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The class of ErrorStateHintUnknownAnyState with a known state: the hint starts from that state +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintKnownAnyState { + + @StateRefinement(to = "created(this)") + public ErrorStateHintKnownAnyState() {} + + @StateRefinement(to = "created(this)") + public void reset() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public static void main(String[] args) { + ErrorStateHintKnownAnyState f = new ErrorStateHintKnownAnyState(); + f.open(); + f.close(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java new file mode 100644 index 00000000..07bf3c46 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// reset() works in any state, so it is suggested even though the state is unknown; open() alone is not +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintUnknownAnyState { + + @StateRefinement(to = "created(this)") + public ErrorStateHintUnknownAnyState() {} + + @StateRefinement(to = "created(this)") + public void reset() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public static void use(ErrorStateHintUnknownAnyState f) { + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java new file mode 100644 index 00000000..4241b7a2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java @@ -0,0 +1,26 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// read() accepts two states of one set. The other set is not named, and no call reaches either state from any state +@StateSet({"created", "open", "ready"}) +@StateSet({"quiet", "loud"}) +public class ErrorStateHintUnknownDisjunction { + + @StateRefinement(to = "created(this) && quiet(this)") + public ErrorStateHintUnknownDisjunction() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this) || ready(this)") + public void read() {} + + @StateRefinement(to = "loud(this)") + public void shout() {} + + public static void use(ErrorStateHintUnknownDisjunction s) { + s.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java new file mode 100644 index 00000000..71898816 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A field whose state is unknown: forceOpen() works in any state, and only the state set read() checks is named +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintUnknownField { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintUnknownField() {} + + @StateRefinement(to = "opened(this)") + public void forceOpen() {} + + @StateRefinement(from = "opened(this)") + public void read() {} + + @StateRefinement(from = "locked(this)", to = "unlocked(this)") + public void unlock() {} +} + +class ErrorStateHintUnknownFieldUser { + ErrorStateHintUnknownField door; + + void use() { + door.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java new file mode 100644 index 00000000..5569cbef --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Only the state set that redo() checks is named, not its combinations with the other two +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public class ErrorStateHintUnknownThreeSets { + + @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") + public ErrorStateHintUnknownThreeSets() {} + + @StateRefinement(from = "start(this)", to = "canEdit(this)") + public void addEdit() {} + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + public void redo() {} + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + public void undo() {} + + public static void redoLast(ErrorStateHintUnknownThreeSets history) { + history.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java new file mode 100644 index 00000000..8cb92474 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// open() checks both state sets, so both are named. reset() reaches them from any state; slam() fixes only one set +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintUnknownTwoSetGoal { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintUnknownTwoSetGoal() {} + + @StateRefinement(to = "closed(this) && unlocked(this)") + public void reset() {} + + @StateRefinement(to = "closed(this)") + public void slam() {} + + @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "locked(this)", to = "unlocked(this)") + public void unlock() {} + + public static void enter(ErrorStateHintUnknownTwoSetGoal door) { + door.open(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java new file mode 100644 index 00000000..05c5c612 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java @@ -0,0 +1,15 @@ +package testSuite.classes.state_hint_undo_manager_error; + +import javax.swing.undo.UndoManager; + +public class Editor { + + static UndoManager history() { + return new UndoManager(); + } + + static void redoLast() { + UndoManager undoManager = history(); + undoManager.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java new file mode 100644 index 00000000..8bee5cd1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_hint_undo_manager_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Issue #454: with an unknown state, redo() needs redoable, and the only call that leads there, undo(), needs +// undoable, which is just as unknown +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public interface UndoManagerRefinements { + + @StateRefinement(to = "notUndoable(this) && notRedoable(this)") + void UndoManager(); + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + void redo(); + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + void undo(); + + @StateRefinement(from = "redoable(this)", to = "return && redoable(this)") + @StateRefinement(to = "return ? redoable(this) : notRedoable(this)") + boolean canRedo(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index bb6834dc..5d739a40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -25,7 +25,9 @@ public enum Kind { PATH_DEPENDENT_STATE, /** The object is in a state where no call with a state refinement is allowed */ FINAL_STATE, - /** The object's state is unknown, so these are the calls that lead to a state that allows the failing call */ + /** + * The object's state is unknown: the state the failing call needs, and the constructors that create it in one + */ REACHING_CALLS } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 72e9723b..15540a07 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -2,12 +2,11 @@ import java.util.ArrayList; import java.util.Collection; -import java.util.LinkedHashMap; import java.util.List; -import java.util.Map; import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; +import java.util.stream.IntStream; import java.util.stream.Stream; import liquidjava.diagnostics.categories.ErrorCategory; @@ -17,7 +16,6 @@ import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; -import liquidjava.processor.state_machine.Transition; import liquidjava.utils.Utils; import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; @@ -61,7 +59,7 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set StateHints hints = new StateHints(machine, receiver); if (category == ErrorCategory.UNKNOWN) - return hints.reachingCalls(call, goal); + return hints.unknownState(current, call, goal); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(), hints.allowedCalls(current).stream()).toList(); @@ -79,19 +77,37 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) deciding.call().position().getLine(), receiver, values)); } - /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */ - private List reachingCalls(RefinedFunction call, Set goal) { - Map> sources = new LinkedHashMap<>(); - for (Transition t : machine.transitionsEnabling(call)) - sources.computeIfAbsent(t.method(), m -> new ArrayList<>()).add(t.from()); - Stream constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor); - Stream calls = sources.entrySet().stream() - .map(e -> call(e.getKey()) + " (from " + names(e.getValue()) + ")"); - List ways = Stream.concat(constructors, calls).toList(); - if (ways.isEmpty()) + /** + * Nothing is known about the receiver's state: name the state {@code call} needs, in the state sets it checks, and + * the calls that get there from any state. A call allowed in only some states is never suggested, since whether it + * is allowed is just as unknown. Calls that only tell which state the object is in are not in the machine, so no + * hint suggests checking one first. + */ + private List unknownState(Set current, RefinedFunction call, Set goal) { + List checked = machine.stateSetsConstraining(goal); + if (checked.isEmpty()) + return List.of(); // every state allows the call, but no single state refinement covers them all + List hints = new ArrayList<>(); + hints.add(neededState(call, goal, checked)); + hints.addAll(callsFromAnyState(current, call, checked)); + return hints; + } + + /** The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} */ + private List callsFromAnyState(Set current, RefinedFunction call, List checked) { + Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); + if (search.isEmpty() || search.get().isEmpty() || search.get().get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return List.of(new Hint(Kind.REACHING_CALLS, String.format( - "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways)))); + return search.get().stream().map(sequence -> callSequence(current, sequence, "any state", checked)).toList(); + } + + private Hint neededState(RefinedFunction call, Set goal, List checked) { + String message = String.format("The state of %s is unknown here, and this call needs it to be %s", receiver, + names(goal, checked)); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); + if (!constructors.isEmpty()) + message += ". Objects created with " + String.join(" or ", constructors) + " start in such a state"; + return new Hint(Kind.REACHING_CALLS, message); } private List howToReach(Set current, RefinedFunction call, Set goal, boolean pathDependent) { @@ -103,16 +119,27 @@ private List howToReach(Set current, RefinedFunction call, Set MAX_SEQUENCE_LENGTH) return List.of(); - return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence, names(current), allStateSets())) + .toList(); } - private Hint callSequence(Set current, List sequence) { + /** + * @param from + * how to name {@code current} + * @param shown + * the state sets to name the reached states in + */ + private Hint callSequence(Set current, List sequence, String from, List shown) { Set reached = current; for (RefinedFunction method : sequence) reached = machine.after(reached, method); String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, - receiver, names(current), names(reached))); + receiver, from, names(reached, shown))); + } + + private List allStateSets() { + return IntStream.range(0, machine.states().get(0).names().size()).boxed().toList(); } private Hint unreachable(Set current, RefinedFunction call, Set goal, boolean pathDependent) { @@ -167,6 +194,11 @@ private static String names(Collection states) { return states.stream().map(State::name).collect(Collectors.joining(" or ")); } + /** {@code states} named only in the state sets {@code shown}, each name once */ + private static String names(Collection states, List shown) { + return states.stream().map(s -> s.name(shown)).distinct().collect(Collectors.joining(" or ")); + } + private static String list(List items) { if (items.size() <= MAX_LISTED_CALLS) return String.join(", ", items); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java index df7d0184..724451f3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java @@ -1,6 +1,7 @@ package liquidjava.processor.state_machine; import java.util.List; +import java.util.stream.Collectors; import liquidjava.rj_language.Predicate; @@ -22,4 +23,9 @@ public record State(List names, Predicate predicate) { public String name() { return String.join(" and ", names); } + + /** The state names in the given state sets only, as indexes into {@link #names()} */ + public String name(List stateSets) { + return stateSets.stream().map(names::get).collect(Collectors.joining(" and ")); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 1bfa1926..fee292bd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -11,6 +11,7 @@ import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; +import java.util.stream.IntStream; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; @@ -107,16 +108,22 @@ public Optional>> shortestPaths(Set current, R return Optional.of(List.of()); } - /** The transitions from a state where {@code call} is not allowed to states where it is */ - public List transitionsEnabling(RefinedFunction call) { - return transitions.stream().filter(t -> !allows(Set.of(t.from()), call) && allows(t.to(), call)).toList(); - } - /** The constructors that create the object in a state where {@code call} is allowed */ public List constructorsEnabling(RefinedFunction call) { return constructors.entrySet().stream().filter(e -> allows(e.getValue(), call)).map(Map.Entry::getKey).toList(); } + /** + * The state sets that {@code subset} depends on, as indexes into {@link State#names()}: those where changing only + * the state in that set can take a state out of {@code subset}. Every other state set can be in any of its states. + */ + public List stateSetsConstraining(Set subset) { + int stateSets = states.isEmpty() ? 0 : states.get(0).names().size(); + return IntStream.range(0, stateSets).filter(set -> subset.stream().anyMatch( + state -> states.stream().anyMatch(other -> !subset.contains(other) && differOnlyIn(state, other, set)))) + .boxed().toList(); + } + /** {@code subset} in declaration order */ public Set ordered(Collection subset) { return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new)); @@ -126,6 +133,11 @@ private Optional transition(State from, RefinedFunction method) { return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst(); } + private static boolean differOnlyIn(State state, State other, int stateSet) { + return IntStream.range(0, state.names().size()) + .allMatch(set -> set == stateSet || state.names().get(set).equals(other.names().get(set))); + } + private static List append(List path, RefinedFunction method) { List extended = new ArrayList<>(path); extended.add(method); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 8f5b4282..3afb2670 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -85,9 +85,61 @@ void receiverThatIsNotAVariableGetsNoHints() { } @Test - void unknownStateListsTheCallsThatLeadToTheExpectedState() { - assertHints("ErrorStateHintUnknownState.java", new Hint(Kind.REACHING_CALLS, - "The state of f is unknown here. To get it to open, use: f.open() (from created)")); + void unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState() { + assertHints("ErrorStateHintUnknownState.java", + new Hint(Kind.REACHING_CALLS, "The state of f is unknown here, and this call needs it to be open")); + } + + @Test + void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { + assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.REACHING_CALLS, + "The state of undoManager is unknown here, and this call needs it to be redoable")); + } + + @Test + void unknownStateWithThreeStateSetsNamesOnlyTheCheckedOne() { + assertHints("ErrorStateHintUnknownThreeSets.java", new Hint(Kind.REACHING_CALLS, + "The state of history is unknown here, and this call needs it to be redoable")); + } + + @Test + void unknownStateSuggestsCallsAllowedInAnyState() { + assertHints("ErrorStateHintUnknownAnyState.java", + new Hint(Kind.REACHING_CALLS, "The state of f is unknown here, and this call needs it to be open"), + new Hint(Kind.CALL_SEQUENCE, + "Call f.reset(), then f.open() before this call to move f from any state to open")); + } + + @Test + void knownStateStartsTheSequenceFromThatState() { + assertHints("ErrorStateHintKnownAnyState.java", + new Hint(Kind.CALL_SEQUENCE, + "Call f.reset(), then f.open() before this call to move f from closed to open"), + new Hint(Kind.AVAILABLE_CALLS, "In state closed, f can call: reset()")); + } + + @Test + void unknownStateNamesEveryStateSetTheCallChecks() { + assertHints("ErrorStateHintUnknownTwoSetGoal.java", + new Hint(Kind.REACHING_CALLS, + "The state of door is unknown here, and this call needs it to be closed and unlocked. " + + "Objects created with new ErrorStateHintUnknownTwoSetGoal() start in such a state"), + new Hint(Kind.CALL_SEQUENCE, + "Call door.reset() before this call to move door from any state to closed and unlocked")); + } + + @Test + void unknownStateOfAFieldSuggestsCallsAllowedInAnyState() { + assertHints("ErrorStateHintUnknownField.java", + new Hint(Kind.REACHING_CALLS, "The state of door is unknown here, and this call needs it to be opened"), + new Hint(Kind.CALL_SEQUENCE, + "Call door.forceOpen() before this call to move door from any state to opened")); + } + + @Test + void unknownStateNamesEveryStateTheCallAccepts() { + assertHints("ErrorStateHintUnknownDisjunction.java", new Hint(Kind.REACHING_CALLS, + "The state of s is unknown here, and this call needs it to be open or ready")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java new file mode 100644 index 00000000..09b724cb --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -0,0 +1,55 @@ +package liquidjava.processor.state_machine; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; +import java.util.Map; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import liquidjava.rj_language.Predicate; + +class StateMachineTest { + + // two state sets, {open, closed} and {locked, unlocked}, combined in declaration order + private static final State OPEN_LOCKED = state("open", "locked"); + private static final State OPEN_UNLOCKED = state("open", "unlocked"); + private static final State CLOSED_LOCKED = state("closed", "locked"); + private static final State CLOSED_UNLOCKED = state("closed", "unlocked"); + private static final StateMachine MACHINE = new StateMachine( + List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED), List.of(), List.of(), Map.of(), true); + + @Test + void statesOfOneSetConstrainOnlyThatSet() { + assertEquals(List.of(0), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, OPEN_UNLOCKED))); + assertEquals(List.of(1), MACHINE.stateSetsConstraining(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); + } + + @Test + void singleStateConstrainsEverySet() { + assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(CLOSED_UNLOCKED))); + } + + @Test + void statesDifferingInBothSetsConstrainBoth() { + assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, CLOSED_UNLOCKED))); + // open || locked + assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + } + + @Test + void everyStateConstrainsNoSet() { + assertEquals(List.of(), MACHINE.stateSetsConstraining(Set.copyOf(MACHINE.states()))); + } + + @Test + void stateIsNamedInTheGivenSetsOnly() { + assertEquals("locked", OPEN_LOCKED.name(List.of(1))); + assertEquals("open and locked", OPEN_LOCKED.name(List.of(0, 1))); + } + + private static State state(String... names) { + return new State(List.of(names), new Predicate()); + } +} From 2fa8e6efdc8bfb4328b8f25898666e0a174e0dc0 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 22:03:34 +0000 Subject: [PATCH 2/5] Name states briefly in every state hint, and tell a failed check from an unknown state - Name a set of states as the fewest groups that each fix the state in some state sets, so open(this) || loud(this) reads "open or loud" and a partly known state is named in its known state sets only. Every state hint uses this, for the current, needed and reached states. - Only call a state unknown when nothing mentions it. When it is mentioned only through another value, such as the result of an earlier check, say that what is known does not decide it. - Always name the needed state and the constructors, even when every state allows the call by a different state refinement. - Do not suggest creating a new object when the receiver is this. - Rename the hint kind REACHING_CALLS to NEEDED_STATE, and share the call sequence search between known and unknown states. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorStateHintPartlyKnown.java | 25 ++++ ...ErrorStateHintUnknownCrossDisjunction.java | 20 +++ .../ErrorStateHintUnknownLongPath.java | 31 ++++ .../ErrorStateHintUnknownSeveralWays.java | 28 ++++ .../testSuite/ErrorStateHintUnknownThis.java | 22 +++ .../ErrorStateHintUnknownToggle.java | 20 +++ .../ErrorStateHintUnknownTwoRefinements.java | 22 +++ .../Reader.java | 13 ++ .../ScannerRefinements.java | 17 +++ .../liquidjava/diagnostics/hints/Hint.java | 6 +- .../diagnostics/hints/StateHints.java | 105 ++++++------- .../refinement_checker/TypeChecker.java | 5 + .../refinement_checker/VCChecker.java | 5 + .../object_checkers/AuxStateHandler.java | 6 +- .../processor/state_machine/State.java | 6 - .../processor/state_machine/StateCover.java | 138 ++++++++++++++++++ .../state_machine/StateErrorCategories.java | 14 +- .../processor/state_machine/StateMachine.java | 18 +-- .../api/tests/TestErrorCategories.java | 5 + .../liquidjava/api/tests/TestStateHints.java | 73 ++++++++- .../state_machine/StateMachineTest.java | 61 ++++++-- 21 files changed, 531 insertions(+), 109 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java new file mode 100644 index 00000000..53b35f87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java @@ -0,0 +1,25 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Only one of three state sets is known (notRedoable), so the hints name that set only +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public class ErrorStateHintPartlyKnown { + + @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") + public ErrorStateHintPartlyKnown() {} + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + public void redo() {} + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + public void undo() {} + + @StateRefinement(from = "notRedoable(this)") + public void check() { + this.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java new file mode 100644 index 00000000..123a3fbf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java @@ -0,0 +1,20 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// read() accepts a state of either set, so each is named alone, not combined with every state of the other set +@StateSet({"created", "open", "ready"}) +@StateSet({"quiet", "loud"}) +public class ErrorStateHintUnknownCrossDisjunction { + + @StateRefinement(to = "created(this) && quiet(this)") + public ErrorStateHintUnknownCrossDisjunction() {} + + @StateRefinement(from = "open(this) || loud(this)") + public void read() {} + + public static void use(ErrorStateHintUnknownCrossDisjunction s) { + s.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java new file mode 100644 index 00000000..f7499aff --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java @@ -0,0 +1,31 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// From any state, go() needs four calls (reset, a, b, c), more than a hint suggests +@StateSet({"s0", "s1", "s2", "s3"}) +public class ErrorStateHintUnknownLongPath { + + @StateRefinement(to = "s0(this)") + public ErrorStateHintUnknownLongPath() {} + + @StateRefinement(to = "s0(this)") + public void reset() {} + + @StateRefinement(from = "s0(this)", to = "s1(this)") + public void a() {} + + @StateRefinement(from = "s1(this)", to = "s2(this)") + public void b() {} + + @StateRefinement(from = "s2(this)", to = "s3(this)") + public void c() {} + + @StateRefinement(from = "s3(this)") + public void go() {} + + public static void use(ErrorStateHintUnknownLongPath x) { + x.go(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java new file mode 100644 index 00000000..da359dd0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// go() accepts s1 or s2, and a different call reaches each of them from any state +@StateSet({"s0", "s1", "s2", "s3"}) +public class ErrorStateHintUnknownSeveralWays { + + @StateRefinement(to = "s0(this)") + public ErrorStateHintUnknownSeveralWays() {} + + @StateRefinement(to = "s1(this)") + public void one() {} + + @StateRefinement(to = "s2(this)") + public void two() {} + + @StateRefinement(to = "s3(this)") + public void three() {} + + @StateRefinement(from = "s1(this) || s2(this)") + public void go() {} + + public static void use(ErrorStateHintUnknownSeveralWays x) { + x.go(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java new file mode 100644 index 00000000..32294528 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The receiver is this, so creating a new object, though it would start in open, is not suggested +@StateSet({"open", "closed"}) +public class ErrorStateHintUnknownThis { + + @StateRefinement(to = "open(this)") + public ErrorStateHintUnknownThis() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public void helper() { + this.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java new file mode 100644 index 00000000..b5287264 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java @@ -0,0 +1,20 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// flip() is allowed in every state, but by a different state refinement in each, so an unknown state rejects it +@StateSet({"up", "down"}) +public class ErrorStateHintUnknownToggle { + + @StateRefinement(to = "up(this)") + public ErrorStateHintUnknownToggle() {} + + @StateRefinement(from = "up(this)", to = "down(this)") + @StateRefinement(from = "down(this)", to = "up(this)") + public void flip() {} + + public static void use(ErrorStateHintUnknownToggle t) { + t.flip(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java new file mode 100644 index 00000000..525db2d9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Like UndoManager.undoOrRedo(): one state refinement per state set, so the call needs undoable or redoable +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public class ErrorStateHintUnknownTwoRefinements { + + @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") + public ErrorStateHintUnknownTwoRefinements() {} + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && notRedoable(this)") + @StateRefinement(from = "redoable(this)", to = "notUndoable(this) && notRedoable(this)") + public void undoOrRedo() {} + + public static void use(ErrorStateHintUnknownTwoRefinements history) { + history.undoOrRedo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java new file mode 100644 index 00000000..a9d50e63 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java @@ -0,0 +1,13 @@ +package testSuite.classes.state_hint_checked_state_error; + +import java.util.Scanner; + +// The state was checked and the check failed: the state is not unknown, but the check does not decide it either +public class Reader { + + public static void nextWhenThereIsNone(Scanner it) { + if (!it.hasNext()) { + it.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java new file mode 100644 index 00000000..7dedf5ed --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_checked_state_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface ScannerRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index 5d739a40..4ce0e7ac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -25,10 +25,8 @@ public enum Kind { PATH_DEPENDENT_STATE, /** The object is in a state where no call with a state refinement is allowed */ FINAL_STATE, - /** - * The object's state is unknown: the state the failing call needs, and the constructors that create it in one - */ - REACHING_CALLS + /** The object can be in any state: the state the failing call needs, and the constructors that create it */ + NEEDED_STATE } public static Hint general(String message) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 15540a07..6068ab80 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -5,8 +5,8 @@ import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.function.Supplier; import java.util.stream.Collectors; -import java.util.stream.IntStream; import java.util.stream.Stream; import liquidjava.diagnostics.categories.ErrorCategory; @@ -17,6 +17,7 @@ import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; @@ -59,10 +60,13 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set StateHints hints = new StateHints(machine, receiver); if (category == ErrorCategory.UNKNOWN) - return hints.unknownState(current, call, goal); + return hints.anyState(current, call, goal, false); + if (category == null && current.size() == machine.states().size()) + return hints.anyState(current, call, goal, true); // something is known, e.g. an earlier check failed boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; - return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(), - hints.allowedCalls(current).stream()).toList(); + List sequences = hints.howToReach(current, call, hints.names(current), + () -> machine.complete() ? List.of(hints.unreachable(current, call, goal, pathDependent)) : List.of()); + return Stream.concat(sequences.stream(), hints.allowedCalls(current).stream()).toList(); } /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */ @@ -78,68 +82,52 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) } /** - * Nothing is known about the receiver's state: name the state {@code call} needs, in the state sets it checks, and - * the calls that get there from any state. A call allowed in only some states is never suggested, since whether it - * is allowed is just as unknown. Calls that only tell which state the object is in are not in the machine, so no - * hint suggests checking one first. + * The receiver can be in any state: name the state {@code call} needs and the calls that get there from any state. + * A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that + * only tell which state the object is in are not in the machine, so no hint suggests checking one first. + * + * @param somethingKnown + * whether anything is known about the state, though not enough to rule out any state */ - private List unknownState(Set current, RefinedFunction call, Set goal) { - List checked = machine.stateSetsConstraining(goal); - if (checked.isEmpty()) - return List.of(); // every state allows the call, but no single state refinement covers them all + private List anyState(Set current, RefinedFunction call, Set goal, boolean somethingKnown) { + String known = somethingKnown ? "What is known here does not decide the state of " + receiver + : "The state of " + receiver + " is unknown here"; + String message = known + ", and this call needs it to be " + names(goal); + message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); List hints = new ArrayList<>(); - hints.add(neededState(call, goal, checked)); - hints.addAll(callsFromAnyState(current, call, checked)); + hints.add(new Hint(Kind.NEEDED_STATE, message)); + hints.addAll(howToReach(current, call, "any state", List::of)); return hints; } - /** The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} */ - private List callsFromAnyState(Set current, RefinedFunction call, List checked) { - Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); - if (search.isEmpty() || search.get().isEmpty() || search.get().get(0).size() > MAX_SEQUENCE_LENGTH) - return List.of(); - return search.get().stream().map(sequence -> callSequence(current, sequence, "any state", checked)).toList(); - } - - private Hint neededState(RefinedFunction call, Set goal, List checked) { - String message = String.format("The state of %s is unknown here, and this call needs it to be %s", receiver, - names(goal, checked)); - List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); - if (!constructors.isEmpty()) - message += ". Objects created with " + String.join(" or ", constructors) + " start in such a state"; - return new Hint(Kind.REACHING_CALLS, message); - } - - private List howToReach(Set current, RefinedFunction call, Set goal, boolean pathDependent) { + /** + * The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} + * + * @param from + * how to name {@code current} + * @param unreachable + * the hints to give if no sequence exists + */ + private List howToReach(Set current, RefinedFunction call, String from, + Supplier> unreachable) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) return List.of(); List> sequences = search.get(); if (sequences.isEmpty()) - return machine.complete() ? List.of(unreachable(current, call, goal, pathDependent)) : List.of(); + return unreachable.get(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return sequences.stream().map(sequence -> callSequence(current, sequence, names(current), allStateSets())) - .toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence, from)).toList(); } - /** - * @param from - * how to name {@code current} - * @param shown - * the state sets to name the reached states in - */ - private Hint callSequence(Set current, List sequence, String from, List shown) { + private Hint callSequence(Set current, List sequence, String from) { Set reached = current; for (RefinedFunction method : sequence) reached = machine.after(reached, method); String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, - receiver, from, names(reached, shown))); - } - - private List allStateSets() { - return IntStream.range(0, machine.states().get(0).names().size()).boxed().toList(); + receiver, from, names(reached))); } private Hint unreachable(Set current, RefinedFunction call, Set goal, boolean pathDependent) { @@ -150,9 +138,7 @@ private Hint unreachable(Set current, RefinedFunction call, Set go receiver, names(current), names(goal), receiver)); String message = String.format("No sequence of calls moves %s from %s to %s", receiver, names(current), names(goal)); - List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); - if (!constructors.isEmpty()) - message += ". Create a new object instead with " + String.join(" or ", constructors); + message += newObjects(call).map(c -> ". Create a new object instead with " + c).orElse(""); return new Hint(Kind.UNREACHABLE_STATE, message); } @@ -172,6 +158,14 @@ private List allowedCalls(Set current) { return List.of(); } + /** The constructors that create an object where {@code call} is allowed, unless the receiver is this object */ + private Optional newObjects(RefinedFunction call) { + if (receiver.equals(Keys.THIS)) + return Optional.empty(); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); + return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors)); + } + private String call(RefinedFunction method) { return receiver + "." + signature(method); } @@ -190,13 +184,10 @@ private static String parameters(RefinedFunction function) { .collect(Collectors.joining(", ", "(", ")")); } - private static String names(Collection states) { - return states.stream().map(State::name).collect(Collectors.joining(" or ")); - } - - /** {@code states} named only in the state sets {@code shown}, each name once */ - private static String names(Collection states, List shown) { - return states.stream().map(s -> s.name(shown)).distinct().collect(Collectors.joining(" or ")); + /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ + private String names(Collection states) { + return machine.describe(states).stream().map(group -> String.join(" and ", group)) + .collect(Collectors.joining(" or ")); } private static String list(List items) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index fb9efd2e..66a443dd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -430,6 +430,11 @@ private SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, S needsCounterexample); } + /** What a state refinement error from {@code found} to {@code expected} shows as found */ + public Predicate shownFound(Predicate found, Predicate expected) { + return vcChecker.shownFound(found, expected); + } + public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { vcChecker.throwRefinementError(position, declarationPosition, expectedType, foundType, null, customMessage); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 819e4b6a..97289505 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -446,6 +446,11 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl customMessage); } + /** What a state refinement error shows as found: what is known about the variables of both predicates */ + protected Predicate shownFound(Predicate found, Predicate expected) { + return buildPremiseChain(new TranslationTable(), expected, found).simplify().getImplication().toPredicate(); + } + protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, StateErrorContext context) throws StateRefinementError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 38fe52cd..55575c50 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -794,10 +794,10 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, instanceName, prevState, invocation); + Predicate expected = expectedStatesDisjunction; ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE - : states.flatMap( - r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, ghostStates)) - .orElse(null); + : states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, + tc.shownFound(prevState, expected), ghostStates)).orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() : states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java index 724451f3..df7d0184 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java @@ -1,7 +1,6 @@ package liquidjava.processor.state_machine; import java.util.List; -import java.util.stream.Collectors; import liquidjava.rj_language.Predicate; @@ -23,9 +22,4 @@ public record State(List names, Predicate predicate) { public String name() { return String.join(" and ", names); } - - /** The state names in the given state sets only, as indexes into {@link #names()} */ - public String name(List stateSets) { - return stateSets.stream().map(names::get).collect(Collectors.joining(" and ")); - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java new file mode 100644 index 00000000..fe741363 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java @@ -0,0 +1,138 @@ +package liquidjava.processor.state_machine; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Comparator; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.stream.IntStream; + +/** + * Names a set of states as briefly as possible: as the fewest groups that each fix the state in some state sets and + * allow any state in the others. For example, the states where {@code open(this) || loud(this)} holds are named + * {@code open} or {@code loud}, not as every combination with the other state sets. + */ +final class StateCover { + + /** Above this many candidate groups, the smallest cover is approximated instead of searched for */ + private static final int MAX_EXACT = 12; + private static final int ANY = -1; + + private final List states; + private final List> values; + + private StateCover(List states) { + this.states = states; + int stateSets = states.get(0).names().size(); + this.values = IntStream.range(0, stateSets) + .mapToObj(set -> states.stream().map(s -> s.names().get(set)).distinct().toList()).toList(); + } + + /** + * @param states + * every state of the class, one for each combination of the states of its state sets + * + * @return the groups, each given by the states it fixes, in the order the state sets are declared; if + * {@code subset} has every state, each state on its own + */ + static List> of(List states, Set subset) { + if (subset.isEmpty()) + return List.of(); + if (subset.size() == states.size()) + return states.stream().map(State::names).toList(); + StateCover cover = new StateCover(states); + return cover.smallestCover(cover.largestGroupsWithin(subset), subset).stream().map(cover::names).toList(); + } + + /** The groups of states inside {@code subset} that no larger group inside it contains, in declaration order */ + private List largestGroupsWithin(Set subset) { + List within = new ArrayList<>(); + groups(new int[values.size()], 0, within, subset); + return within.stream().filter(g -> within.stream().noneMatch(other -> other != g && contains(other, g))) + .sorted(declarationOrder()).toList(); + } + + private void groups(int[] group, int set, List within, Set subset) { + if (set == values.size()) { + if (members(group).stream().allMatch(subset::contains)) + within.add(group.clone()); + return; + } + for (int value = ANY; value < values.get(set).size(); value++) { + group[set] = value; + groups(group, set + 1, within, subset); + } + } + + /** The fewest of {@code candidates} that together hold every state of {@code subset} */ + private List smallestCover(List candidates, Set subset) { + if (candidates.size() <= MAX_EXACT) { + for (int size = 1; size <= candidates.size(); size++) { + List chosen = firstCover(candidates, subset, size, 0, new ArrayList<>()); + if (chosen != null) + return chosen; + } + } + List chosen = new ArrayList<>(); + Set left = new HashSet<>(subset); + while (!left.isEmpty()) { + int[] best = candidates.stream() + .max(Comparator.comparingLong(g -> members(g).stream().filter(left::contains).count())).get(); + chosen.add(best); + members(best).forEach(left::remove); + } + return chosen.stream().sorted(declarationOrder()).toList(); + } + + /** The first {@code size} candidates from {@code next} on, in order, that cover {@code subset}, or null */ + private List firstCover(List candidates, Set subset, int size, int next, List chosen) { + if (chosen.size() == size) + return covers(chosen, subset) ? List.copyOf(chosen) : null; + for (int i = next; i < candidates.size(); i++) { + chosen.add(candidates.get(i)); + List found = firstCover(candidates, subset, size, i + 1, chosen); + chosen.remove(chosen.size() - 1); + if (found != null) + return found; + } + return null; + } + + private boolean covers(List groups, Set subset) { + Set covered = new HashSet<>(); + groups.forEach(g -> covered.addAll(members(g))); + return covered.containsAll(subset); + } + + private List members(int[] group) { + return states.stream() + .filter(s -> IntStream.range(0, group.length).allMatch( + set -> group[set] == ANY || values.get(set).get(group[set]).equals(s.names().get(set)))) + .toList(); + } + + /** Whether {@code larger} holds every state of {@code smaller} */ + private static boolean contains(int[] larger, int[] smaller) { + return !Arrays.equals(larger, smaller) + && IntStream.range(0, larger.length).allMatch(set -> larger[set] == ANY || larger[set] == smaller[set]); + } + + /** Groups fixing earlier state sets first, then by the order of the states within a set */ + private static Comparator declarationOrder() { + return (a, b) -> { + for (int set = 0; set < a.length; set++) { + int x = a[set] == ANY ? Integer.MAX_VALUE : a[set]; + int y = b[set] == ANY ? Integer.MAX_VALUE : b[set]; + if (x != y) + return Integer.compare(x, y); + } + return 0; + }; + } + + private List names(int[] group) { + return IntStream.range(0, group.length).filter(set -> group[set] != ANY) + .mapToObj(set -> values.get(set).get(group[set])).toList(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java index e0e1fbb8..2c3f8d88 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java @@ -21,17 +21,23 @@ private StateErrorCategories() { * the states the receiver can be in before the call * @param found * what is known about the receiver before the call + * @param shownFound + * what the error shows as found: {@code found} with what is known about the values it mentions, such as + * the result of an earlier call that checked the receiver's state * @param ghostStates * the ghost states of the receiver's class * * @return the category, or nothing if it cannot be decided */ public static Optional categorize(StateMachine machine, Set current, Predicate found, - List ghostStates) { + Predicate shownFound, List ghostStates) { List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); - // all states are possible and none is mentioned: nothing is known, which differs from a join of every state - if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) - return Optional.of(ErrorCategory.UNKNOWN); + if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) { + // all states are possible and none is mentioned: nothing is known, which differs from a join of every + // state; a state mentioned only through another value, like a check's result, is not a lack of knowledge + return shownFound.getStateInvocations(states).isEmpty() ? Optional.of(ErrorCategory.UNKNOWN) + : Optional.empty(); + } if (current.size() == 1) return Optional.of(ErrorCategory.OUT_OF_ORDER); // with several state sets, the states may differ only in a set the call does not check diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index fee292bd..09012c0d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -11,7 +11,6 @@ import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; -import java.util.stream.IntStream; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; @@ -114,14 +113,12 @@ public List constructorsEnabling(RefinedFunction call) { } /** - * The state sets that {@code subset} depends on, as indexes into {@link State#names()}: those where changing only - * the state in that set can take a state out of {@code subset}. Every other state set can be in any of its states. + * {@code subset} named as briefly as possible, as groups of states that each fix the state in some state sets and + * allow any state in the others, e.g. {@code [[open], [loud]]} for the states where {@code open(this) || + * loud(this)} holds */ - public List stateSetsConstraining(Set subset) { - int stateSets = states.isEmpty() ? 0 : states.get(0).names().size(); - return IntStream.range(0, stateSets).filter(set -> subset.stream().anyMatch( - state -> states.stream().anyMatch(other -> !subset.contains(other) && differOnlyIn(state, other, set)))) - .boxed().toList(); + public List> describe(Collection subset) { + return StateCover.of(states, Set.copyOf(subset)); } /** {@code subset} in declaration order */ @@ -133,11 +130,6 @@ private Optional transition(State from, RefinedFunction method) { return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst(); } - private static boolean differOnlyIn(State state, State other, int stateSet) { - return IntStream.range(0, state.names().size()) - .allMatch(set -> set == stateSet || state.names().get(set).equals(other.names().get(set))); - } - private static List append(List path, RefinedFunction method) { List extended = new ArrayList<>(path); extended.add(method); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java index 2d978d4e..62bba174 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java @@ -54,6 +54,11 @@ void nothingKnownAboutStateIsUnknown() { assertCategory("ErrorStateHintUnknownState.java", ErrorCategory.UNKNOWN); } + @Test + void stateMentionedOnlyByAnEarlierCheckIsNotUnknown() { + assertNoCategory("classes/state_hint_checked_state_error"); + } + @Test void stateErrorWithoutStateSetGetsNoCategory() { assertNoCategory("ErrorUnconstrainedStateRefinement.java"); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 3afb2670..ff043446 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -87,25 +87,25 @@ void receiverThatIsNotAVariableGetsNoHints() { @Test void unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState() { assertHints("ErrorStateHintUnknownState.java", - new Hint(Kind.REACHING_CALLS, "The state of f is unknown here, and this call needs it to be open")); + new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open")); } @Test void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { - assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.REACHING_CALLS, + assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.NEEDED_STATE, "The state of undoManager is unknown here, and this call needs it to be redoable")); } @Test void unknownStateWithThreeStateSetsNamesOnlyTheCheckedOne() { - assertHints("ErrorStateHintUnknownThreeSets.java", new Hint(Kind.REACHING_CALLS, + assertHints("ErrorStateHintUnknownThreeSets.java", new Hint(Kind.NEEDED_STATE, "The state of history is unknown here, and this call needs it to be redoable")); } @Test void unknownStateSuggestsCallsAllowedInAnyState() { assertHints("ErrorStateHintUnknownAnyState.java", - new Hint(Kind.REACHING_CALLS, "The state of f is unknown here, and this call needs it to be open"), + new Hint(Kind.NEEDED_STATE, "The state of f is unknown here, and this call needs it to be open"), new Hint(Kind.CALL_SEQUENCE, "Call f.reset(), then f.open() before this call to move f from any state to open")); } @@ -121,7 +121,7 @@ void knownStateStartsTheSequenceFromThatState() { @Test void unknownStateNamesEveryStateSetTheCallChecks() { assertHints("ErrorStateHintUnknownTwoSetGoal.java", - new Hint(Kind.REACHING_CALLS, + new Hint(Kind.NEEDED_STATE, "The state of door is unknown here, and this call needs it to be closed and unlocked. " + "Objects created with new ErrorStateHintUnknownTwoSetGoal() start in such a state"), new Hint(Kind.CALL_SEQUENCE, @@ -131,17 +131,76 @@ void unknownStateNamesEveryStateSetTheCallChecks() { @Test void unknownStateOfAFieldSuggestsCallsAllowedInAnyState() { assertHints("ErrorStateHintUnknownField.java", - new Hint(Kind.REACHING_CALLS, "The state of door is unknown here, and this call needs it to be opened"), + new Hint(Kind.NEEDED_STATE, "The state of door is unknown here, and this call needs it to be opened"), new Hint(Kind.CALL_SEQUENCE, "Call door.forceOpen() before this call to move door from any state to opened")); } @Test void unknownStateNamesEveryStateTheCallAccepts() { - assertHints("ErrorStateHintUnknownDisjunction.java", new Hint(Kind.REACHING_CALLS, + assertHints("ErrorStateHintUnknownDisjunction.java", new Hint(Kind.NEEDED_STATE, "The state of s is unknown here, and this call needs it to be open or ready")); } + @Test + void disjunctionAcrossStateSetsNamesEachStateAlone() { + assertHints("ErrorStateHintUnknownCrossDisjunction.java", new Hint(Kind.NEEDED_STATE, + "The state of s is unknown here, and this call needs it to be open or loud")); + } + + @Test + void oneRefinementPerStateSetNamesEachStateAlone() { + assertHints("ErrorStateHintUnknownTwoRefinements.java", new Hint(Kind.NEEDED_STATE, + "The state of history is unknown here, and this call needs it to be undoable or redoable")); + } + + @Test + void callAllowedInEveryStateByDifferentRefinementsStillNamesTheStatesAndConstructors() { + assertHints("ErrorStateHintUnknownToggle.java", + new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be up or down. " + + "Objects created with new ErrorStateHintUnknownToggle() start in such a state")); + } + + @Test + void unknownStateDoesNotSuggestSequencesLongerThanTheLimit() { + assertHints("ErrorStateHintUnknownLongPath.java", + new Hint(Kind.NEEDED_STATE, "The state of x is unknown here, and this call needs it to be s3")); + } + + @Test + void unknownStateSuggestsEverySequenceOfTheShortestLength() { + assertHints("ErrorStateHintUnknownSeveralWays.java", + new Hint(Kind.NEEDED_STATE, "The state of x is unknown here, and this call needs it to be s1 or s2"), + new Hint(Kind.CALL_SEQUENCE, "Call x.one() before this call to move x from any state to s1"), + new Hint(Kind.CALL_SEQUENCE, "Call x.two() before this call to move x from any state to s2")); + } + + @Test + void thisReceiverIsNotToldToCreateANewObject() { + assertHints("ErrorStateHintUnknownThis.java", + new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be open")); + } + + @Test + void stateCheckedByAnEarlierCallIsNotCalledUnknown() { + assertHints("classes/state_hint_checked_state_error", new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of it, and this call needs it to be hasMore")); + } + + @Test + void partlyKnownStateIsNamedInTheKnownStateSetsOnly() { + assertHints("ErrorStateHintPartlyKnown.java", + new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable"), + new Hint(Kind.AVAILABLE_CALLS, "In state notRedoable, this can call: check()")); + } + + @Test + void statesDifferingInAnotherStateSetAreNamedOnce() { + assertHints("ErrorPathDependentOtherStateSet.java", + new Hint(Kind.CALL_SEQUENCE, "Call d.open() before this call to move d from closed to opened"), + new Hint(Kind.AVAILABLE_CALLS, "In state closed, d can call: open()")); + } + @Test void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT, diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 09b724cb..664d4b2e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -2,6 +2,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import java.util.ArrayList; import java.util.List; import java.util.Map; import java.util.Set; @@ -17,36 +18,66 @@ class StateMachineTest { private static final State OPEN_UNLOCKED = state("open", "unlocked"); private static final State CLOSED_LOCKED = state("closed", "locked"); private static final State CLOSED_UNLOCKED = state("closed", "unlocked"); - private static final StateMachine MACHINE = new StateMachine( - List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED), List.of(), List.of(), Map.of(), true); + private static final StateMachine MACHINE = machine( + List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED)); @Test - void statesOfOneSetConstrainOnlyThatSet() { - assertEquals(List.of(0), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, OPEN_UNLOCKED))); - assertEquals(List.of(1), MACHINE.stateSetsConstraining(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); + void statesDifferingOnlyInOneSetAreNamedByTheOther() { + assertEquals(List.of(List.of("open")), MACHINE.describe(Set.of(OPEN_LOCKED, OPEN_UNLOCKED))); + assertEquals(List.of(List.of("unlocked")), MACHINE.describe(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); } @Test - void singleStateConstrainsEverySet() { - assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(CLOSED_UNLOCKED))); + void singleStateIsNamedInEverySet() { + assertEquals(List.of(List.of("closed", "unlocked")), MACHINE.describe(Set.of(CLOSED_UNLOCKED))); } @Test - void statesDifferingInBothSetsConstrainBoth() { - assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, CLOSED_UNLOCKED))); + void statesDifferingInBothSetsAreNamedInBoth() { + assertEquals(List.of(List.of("open", "locked"), List.of("closed", "unlocked")), + MACHINE.describe(Set.of(CLOSED_UNLOCKED, OPEN_LOCKED))); + } + + @Test + void disjunctionAcrossSetsNamesEachStateAlone() { // open || locked - assertEquals(List.of(0, 1), MACHINE.stateSetsConstraining(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + assertEquals(List.of(List.of("open"), List.of("locked")), + MACHINE.describe(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + } + + @Test + void everyStateIsNamedStateByState() { + assertEquals(List.of(List.of("open", "locked"), List.of("open", "unlocked"), List.of("closed", "locked"), + List.of("closed", "unlocked")), MACHINE.describe(Set.copyOf(MACHINE.states()))); } @Test - void everyStateConstrainsNoSet() { - assertEquals(List.of(), MACHINE.stateSetsConstraining(Set.copyOf(MACHINE.states()))); + void noStatesAreNamedByNothing() { + assertEquals(List.of(), MACHINE.describe(Set.of())); } @Test - void stateIsNamedInTheGivenSetsOnly() { - assertEquals("locked", OPEN_LOCKED.name(List.of(1))); - assertEquals("open and locked", OPEN_LOCKED.name(List.of(0, 1))); + void disjunctionOverThreeSetsNamesOnlyTheCheckedStates() { + // {start, canEdit, end} x {undoable, notUndoable} x {redoable, notRedoable}, and undoable || redoable + List states = new ArrayList<>(); + for (String edit : List.of("start", "canEdit", "end")) + for (String undo : List.of("undoable", "notUndoable")) + for (String redo : List.of("redoable", "notRedoable")) + states.add(state(edit, undo, redo)); + Set goal = Set.copyOf(states.stream() + .filter(s -> s.names().get(1).equals("undoable") || s.names().get(2).equals("redoable")).toList()); + assertEquals(List.of(List.of("undoable"), List.of("redoable")), machine(states).describe(goal)); + } + + @Test + void statesOfOneSetAreNamedInDeclarationOrder() { + List states = List.of(state("s0"), state("s1"), state("s2"), state("s3")); + assertEquals(List.of(List.of("s1"), List.of("s3")), + machine(states).describe(Set.of(states.get(3), states.get(1)))); + } + + private static StateMachine machine(List states) { + return new StateMachine(states, List.of(), List.of(), Map.of(), true); } private static State state(String... names) { From d01610cdd655e4d464898a46be49792bd096f1e4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 12:58:56 +0000 Subject: [PATCH 3/5] Do not suggest constructors that cannot be called A state machine left out constructors only when it could not model them, so hints could suggest creating an abstract class, an interface, an enum or a class whose constructor is private. Constructors of such types are now left out of the machine. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateHintUnknownAbstract.java | 19 ++++++++++ .../ErrorStateHintUnknownConcrete.java | 19 ++++++++++ ...rorStateHintUnknownPrivateConstructor.java | 21 +++++++++++ .../InputStreamRefinements.java | 20 +++++++++++ .../state_hint_abstract_spec_error/Use.java | 11 ++++++ .../RunnableFutureRefinements.java | 17 +++++++++ .../state_hint_interface_spec_error/Use.java | 10 ++++++ .../state_machine/StateMachineBuilder.java | 35 +++++++++++++++++++ .../liquidjava/api/tests/TestStateHints.java | 31 ++++++++++++++++ 9 files changed, 183 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java new file mode 100644 index 00000000..c407ba76 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The constructor creates the needed state, but the class is abstract, so no new object can be suggested +@StateSet({"fresh", "ready"}) +public abstract class ErrorStateHintUnknownAbstract { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintUnknownAbstract() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + static void fail(ErrorStateHintUnknownAbstract value) { + value.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java new file mode 100644 index 00000000..dc18804c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The same class as ErrorStateHintUnknownAbstract, but concrete: the constructor is suggested +@StateSet({"fresh", "ready"}) +public class ErrorStateHintUnknownConcrete { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintUnknownConcrete() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + static void fail(ErrorStateHintUnknownConcrete value) { + value.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java new file mode 100644 index 00000000..d77d253f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The constructor creates the needed state, but it is private, so no new object can be suggested +@StateSet({"fresh", "ready"}) +public class ErrorStateHintUnknownPrivateConstructor { + + @StateRefinement(to = "ready(this)") + private ErrorStateHintUnknownPrivateConstructor() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} +} + +class ErrorStateHintUnknownPrivateConstructorUser { + static void fail(ErrorStateHintUnknownPrivateConstructor value) { + value.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java new file mode 100644 index 00000000..726b1d8e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java @@ -0,0 +1,20 @@ +package testSuite.classes.state_hint_abstract_spec_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A spec for an abstract JDK class: its constructor creates the needed state, but no client can call new InputStream() +@ExternalRefinementsFor("java.io.InputStream") +@StateSet({"open", "closed"}) +public interface InputStreamRefinements { + + @StateRefinement(to = "open(this)") + void InputStream(); + + @StateRefinement(from = "open(this)") + int read(); + + @StateRefinement(from = "open(this)", to = "closed(this)") + void close(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java new file mode 100644 index 00000000..8640cbbf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java @@ -0,0 +1,11 @@ +package testSuite.classes.state_hint_abstract_spec_error; + +import java.io.IOException; +import java.io.InputStream; + +public class Use { + + static int first(InputStream in) throws IOException { + return in.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java new file mode 100644 index 00000000..52c1c948 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_interface_spec_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A spec for an interface: it has no constructor, so no new object is suggested +@ExternalRefinementsFor("java.util.concurrent.RunnableFuture") +@StateSet({"pending", "done"}) +public interface RunnableFutureRefinements { + + @StateRefinement(from = "pending(this)", to = "done(this)") + void run(); + + @StateRefinement(from = "done(this)") + boolean isDone(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java new file mode 100644 index 00000000..0600c134 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java @@ -0,0 +1,10 @@ +package testSuite.classes.state_hint_interface_spec_error; + +import java.util.concurrent.RunnableFuture; + +public class Use { + + static boolean finished(RunnableFuture task) { + return task.isDone(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 617c4c4a..05314849 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -19,7 +19,10 @@ import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; +import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtModifiable; +import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; @@ -131,6 +134,8 @@ private StateMachine build(String className, CtTypeReference type) throws LJE if (!className.equals(function.getTargetClass()) || !function.hasStateChange()) continue; if (CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) { + if (abstractType(type) || privateConstructor(function, type)) + continue; // cannot be suggested as a new object Optional> created = createdStates(function); created.ifPresent(s -> constructors.put(function, s)); continue; @@ -154,6 +159,36 @@ private boolean relatedClassChangesState(String className, CtTypeReference ty .anyMatch(other -> other.isSubtypeOf(type) || type.isSubtypeOf(other)); } + private static boolean abstractType(CtTypeReference type) { + CtType declaration = type.getTypeDeclaration(); + return declaration == null || declaration.isInterface() || declaration.isAbstract(); + } + + /** + * Whether {@code constructor} cannot be called from outside its class: it is private, or the class is an enum. A + * constructor that is not found in the class's declaration is assumed callable. The machine is shared by every + * caller, so a private constructor is left out even for calls inside its class. + */ + private static boolean privateConstructor(RefinedFunction constructor, CtTypeReference type) { + try { + CtType declaration = type.getTypeDeclaration(); + if (declaration.isEnum()) + return true; + if (!(declaration instanceof CtClass declared)) + return false; + List parameters = constructor.getArguments().stream().map(a -> typeName(a.getType())).toList(); + return declared.getConstructors().stream() + .filter(c -> c.getParameters().stream().map(p -> typeName(p.getType())).toList().equals(parameters)) + .anyMatch(CtModifiable::isPrivate); + } catch (RuntimeException e) { + return false; // a declaration that cannot be built is not evidence that the constructor is private + } + } + + private static String typeName(CtTypeReference type) { + return type == null ? "" : type.getQualifiedName(); + } + /** The transitions of {@code method}, or nothing if they depend on more than the state of {@code this} */ private Optional> transitionsOf(RefinedFunction method) throws LJError { if (!canModel(method)) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index ff043446..2b1ef6e7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -181,6 +181,37 @@ void thisReceiverIsNotToldToCreateANewObject() { new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be open")); } + @Test + void abstractClassIsNotToldToCreateANewObject() { + assertHints("ErrorStateHintUnknownAbstract.java", + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); + } + + @Test + void abstractClassWithAnExternalSpecIsNotToldToCreateANewObject() { + assertHints("classes/state_hint_abstract_spec_error", + new Hint(Kind.NEEDED_STATE, "The state of in is unknown here, and this call needs it to be open")); + } + + @Test + void interfaceWithAnExternalSpecIsNotToldToCreateANewObject() { + assertHints("classes/state_hint_interface_spec_error", + new Hint(Kind.NEEDED_STATE, "The state of task is unknown here, and this call needs it to be done")); + } + + @Test + void privateConstructorIsNotSuggested() { + assertHints("ErrorStateHintUnknownPrivateConstructor.java", + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); + } + + @Test + void concreteClassIsToldToCreateANewObject() { + assertHints("ErrorStateHintUnknownConcrete.java", + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready. " + + "Objects created with new ErrorStateHintUnknownConcrete() start in such a state")); + } + @Test void stateCheckedByAnEarlierCallIsNotCalledUnknown() { assertHints("classes/state_hint_checked_state_error", new Hint(Kind.NEEDED_STATE, From b9683e91b4e90830c3aa41be7d39ed7bbd344b3b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 14:24:38 +0000 Subject: [PATCH 4/5] Count only checks of the receiver, and keep joins out of the checked case - A state mentioned through another value counts as a check only when it is applied to the receiver's instance or to an object the solver proves equal to it. A check of another object leaves the state unknown. What the error shows as found is only computed when needed. - A join of every state across several state sets is no longer taken for a check, so it keeps the "No sequence of calls" hint. - Name the receiver's states in every state set the call checks, so a join that differs in a checked set still lists each state. - When every state allows the call, each by its own state refinement, name the needed state per refinement. - Search the smallest cover exactly up to 13 candidate groups. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateHintJoinOneOfTwoSets.java | 29 ++++++++ .../testSuite/ErrorStateHintJoinTwoSets.java | 31 ++++++++ .../ErrorStateHintUnknownToggleTwoSets.java | 21 ++++++ .../state_hint_checked_copy_error/Reader.java | 14 ++++ .../ScannerRefinements.java | 17 +++++ .../Reader.java | 13 ++++ .../ScannerRefinements.java | 17 +++++ .../Reader.java | 13 ++++ .../ScannerRefinements.java | 17 +++++ .../diagnostics/hints/StateHints.java | 72 +++++++++++++------ .../object_checkers/AuxStateHandler.java | 28 ++++++-- .../processor/state_machine/StateCover.java | 54 +++++++++++--- .../state_machine/StateErrorCategories.java | 65 ++++++++++++++--- .../processor/state_machine/StateMachine.java | 23 +++++- .../api/tests/TestErrorCategories.java | 12 ++++ .../liquidjava/api/tests/TestStateHints.java | 42 +++++++++++ .../state_machine/StateMachineTest.java | 16 +++++ 17 files changed, 433 insertions(+), 51 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java new file mode 100644 index 00000000..58cfb5c3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The paths differ in one of two state sets, so the states are named in both sets the call checks +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintJoinOneOfTwoSets { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintJoinOneOfTwoSets() {} + + @StateRefinement(from = "closed(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "unlocked(this)", to = "locked(this)") + public void lock() {} + + @StateRefinement(from = "closed(this) && unlocked(this)") + public void enter() {} + + public static void use(boolean p) { + ErrorStateHintJoinOneOfTwoSets d = new ErrorStateHintJoinOneOfTwoSets(); + if (p) + d.open(); + d.enter(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java new file mode 100644 index 00000000..8dbfcc1b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java @@ -0,0 +1,31 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Every combination of two state sets is reached on some path: a join of every state, not a lack of knowledge +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintJoinTwoSets { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintJoinTwoSets() {} + + @StateRefinement(from = "closed(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "unlocked(this)", to = "locked(this)") + public void lock() {} + + @StateRefinement(from = "closed(this) && unlocked(this)") + public void enter() {} + + public static void use(boolean p, boolean q) { + ErrorStateHintJoinTwoSets d = new ErrorStateHintJoinTwoSets(); + if (p) + d.open(); + if (q) + d.lock(); + d.enter(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java new file mode 100644 index 00000000..761a0653 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Every state allows flip(), by the refinement for a or the one for b, so the hint names a or b, not all six states +@StateSet({"a", "b"}) +@StateSet({"x", "y", "z"}) +public class ErrorStateHintUnknownToggleTwoSets { + + @StateRefinement(to = "a(this) && x(this)") + public ErrorStateHintUnknownToggleTwoSets() {} + + @StateRefinement(from = "a(this)", to = "b(this)") + @StateRefinement(from = "b(this)", to = "a(this)") + public void flip() {} + + public static void use(ErrorStateHintUnknownToggleTwoSets t) { + t.flip(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java new file mode 100644 index 00000000..84181e98 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java @@ -0,0 +1,14 @@ +package testSuite.classes.state_hint_checked_copy_error; + +import java.util.Scanner; + +// The failed check is on it and the call on a variable holding the same scanner, so the state was checked +public class Reader { + + public static void nextOfTheSameScanner(Scanner it) { + Scanner same = it; + if (!it.hasNext()) { + same.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java new file mode 100644 index 00000000..34b6e53a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_checked_copy_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface ScannerRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java new file mode 100644 index 00000000..69bbbcbc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java @@ -0,0 +1,13 @@ +package testSuite.classes.state_hint_checked_other_object_error; + +import java.util.Scanner; + +// Another scanner was checked, so nothing is known about the state of the receiver +public class Reader { + + public static void nextOfTheOther(Scanner other, Scanner it) { + if (other.hasNext()) { + it.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java new file mode 100644 index 00000000..deb922b3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_checked_other_object_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface ScannerRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java new file mode 100644 index 00000000..035aa37a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java @@ -0,0 +1,13 @@ +package testSuite.classes.state_hint_checked_wrong_object_error; + +import java.util.Scanner; + +// The check is on it, but the call is on another scanner, whose state is unknown +public class Reader { + + public static void checkedTheWrongObject(Scanner it, Scanner other) { + if (it.hasNext()) { + other.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java new file mode 100644 index 00000000..8c436aab --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_hint_checked_wrong_object_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface ScannerRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 6068ab80..6ce60139 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.TreeSet; import java.util.function.Supplier; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -34,10 +35,17 @@ public final class StateHints { private final StateMachine machine; private final String receiver; + /** The states that allow the failing call, grouped by the state refinement that allows it */ + private final List> goals; + /** The state sets the failing call checks, as indexes into {@link State#names()} */ + private final Set checked; - private StateHints(StateMachine machine, String receiver) { + private StateHints(StateMachine machine, String receiver, RefinedFunction call) { this.machine = machine; this.receiver = receiver; + this.goals = machine.statesAllowingByRefinement(call); + this.checked = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) + .collect(Collectors.toCollection(TreeSet::new)); } /** @@ -49,23 +57,24 @@ private StateHints(StateMachine machine, String receiver) { * the receiver as written in the code * @param category * the error's category, or {@code null} if it has none + * @param checked + * whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose + * result says which state it is in */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category) { + ErrorCategory category, boolean checked) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed Set goal = machine.statesAllowing(call); if (goal.isEmpty()) return List.of(); - StateHints hints = new StateHints(machine, receiver); - if (category == ErrorCategory.UNKNOWN) - return hints.anyState(current, call, goal, false); - if (category == null && current.size() == machine.states().size()) - return hints.anyState(current, call, goal, true); // something is known, e.g. an earlier check failed + StateHints hints = new StateHints(machine, receiver, call); + if (category == ErrorCategory.UNKNOWN || checked) + return hints.anyState(current, call, checked); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; - List sequences = hints.howToReach(current, call, hints.names(current), - () -> machine.complete() ? List.of(hints.unreachable(current, call, goal, pathDependent)) : List.of()); + List sequences = hints.howToReach(current, call, hints.namesHere(current), + () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); return Stream.concat(sequences.stream(), hints.allowedCalls(current).stream()).toList(); } @@ -86,13 +95,13 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) * A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that * only tell which state the object is in are not in the machine, so no hint suggests checking one first. * - * @param somethingKnown - * whether anything is known about the state, though not enough to rule out any state + * @param checked + * whether the state was checked, though the check did not decide it */ - private List anyState(Set current, RefinedFunction call, Set goal, boolean somethingKnown) { - String known = somethingKnown ? "What is known here does not decide the state of " + receiver + private List anyState(Set current, RefinedFunction call, boolean checked) { + String known = checked ? "What is known here does not decide the state of " + receiver : "The state of " + receiver + " is unknown here"; - String message = known + ", and this call needs it to be " + names(goal); + String message = known + ", and this call needs it to be " + needed(); message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); List hints = new ArrayList<>(); hints.add(new Hint(Kind.NEEDED_STATE, message)); @@ -130,14 +139,14 @@ private Hint callSequence(Set current, List sequence, St receiver, from, names(reached))); } - private Hint unreachable(Set current, RefinedFunction call, Set goal, boolean pathDependent) { + private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { if (pathDependent) return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. " + "Make %s reach this line in the same state on every path", - receiver, names(current), names(goal), receiver)); - String message = String.format("No sequence of calls moves %s from %s to %s", receiver, names(current), - names(goal)); + receiver, namesHere(current), needed(), receiver)); + String message = String.format("No sequence of calls moves %s from %s to %s", receiver, namesHere(current), + needed()); message += newObjects(call).map(c -> ". Create a new object instead with " + c).orElse(""); return new Hint(Kind.UNREACHABLE_STATE, message); } @@ -148,13 +157,13 @@ private List allowedCalls(Set current) { List signatures = allowed.stream().map(StateHints::signature).toList(); String others = machine.complete() ? "" : " (and possibly others)"; return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("In state %s, %s can call: %s%s", - names(current), receiver, list(signatures), others))); + namesHere(current), receiver, list(signatures), others))); } boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty()); if (machine.complete() && noCallsInAnyState) return List.of(new Hint(Kind.FINAL_STATE, String.format("%s is in state %s, where none of its methods with state refinements can be called", - receiver, names(current)))); + receiver, namesHere(current)))); return List.of(); } @@ -186,8 +195,27 @@ private static String parameters(RefinedFunction function) { /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ private String names(Collection states) { - return machine.describe(states).stream().map(group -> String.join(" and ", group)) - .collect(Collectors.joining(" or ")); + return names(machine.describe(states)); + } + + /** The states the receiver can be in, named in the state sets the call checks and any set they all agree on */ + private String namesHere(Collection current) { + return names(machine.describe(current, checked)); + } + + /** + * The states that allow the call. If every state does, each by a different state refinement, the states each + * refinement allows are named on their own: {@code a or b}, not every state. + */ + private String needed() { + Set goal = machine.ordered(goals.stream().flatMap(Set::stream).toList()); + if (goal.size() < machine.states().size()) + return names(goal); + return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or ")); + } + + private static String names(List> groups) { + return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or ")); } private static String list(List items) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 55575c50..90a068fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -795,12 +795,15 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, instanceName, prevState, invocation); Predicate expected = expectedStatesDisjunction; - ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE - : states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, - tc.shownFound(prevState, expected), ghostStates)).orElse(null); + boolean checked = states + .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, ghostStates, invocation)) + .orElse(false); + ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states.flatMap( + r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, ghostStates)) + .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() - : states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of()); + : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); @@ -833,6 +836,19 @@ private static Optional receiverStates(TypeChecker tc, RefinedFu } } + /** Best effort, like {@link #receiverStates}: see {@link StateErrorCategories#checkedElsewhere} */ + private static boolean checkedElsewhere(TypeChecker tc, ReceiverStates states, Predicate found, Predicate expected, + String instanceName, List ghostStates, CtElement invocation) { + try { + return StateErrorCategories.checkedElsewhere(states.machine(), states.current(), found, + () -> tc.shownFound(found, expected), instanceName, ghostStates, + new StateSolver(tc, invocation.getPosition())); + } catch (RuntimeException e) { + DebugLog.warn("Could not tell whether the receiver's state was checked: " + e.getMessage()); + return false; + } + } + /** Best effort, like {@link #receiverStates} */ private static Optional decidingArgument(TypeChecker tc, VariableInstance receiver, RefinedFunction function, List ghostStates, CtElement invocation) { @@ -846,11 +862,11 @@ private static Optional decidingArgument(TypeChecker tc, Varia /** Hints on how to fix a call to {@code function} made in a state that does not allow it */ private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, - CtElement invocation) { + boolean checked, CtElement invocation) { Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); - return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category); + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java index fe741363..4ef2b8c3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java @@ -6,6 +6,8 @@ import java.util.HashSet; import java.util.List; import java.util.Set; +import java.util.TreeSet; +import java.util.stream.Collectors; import java.util.stream.IntStream; /** @@ -15,8 +17,12 @@ */ final class StateCover { - /** Above this many candidate groups, the smallest cover is approximated instead of searched for */ - private static final int MAX_EXACT = 12; + /** + * Above this many candidate groups, the smallest cover is approximated instead of searched for. With several state + * sets and the machine's limit of 16 states there are at most 13; with one state set the groups are single states, + * which the approximation covers exactly. + */ + private static final int MAX_EXACT = 13; private static final int ANY = -1; private final List states; @@ -32,36 +38,62 @@ private StateCover(List states) { /** * @param states * every state of the class, one for each combination of the states of its state sets + * @param named + * the state sets every group must fix, as indexes into {@link State#names()} * * @return the groups, each given by the states it fixes, in the order the state sets are declared; if - * {@code subset} has every state, each state on its own + * {@code subset} has every state and no set must be named, each state on its own */ - static List> of(List states, Set subset) { + static List> of(List states, Set subset, Set named) { if (subset.isEmpty()) return List.of(); - if (subset.size() == states.size()) + if (subset.size() == states.size() && named.isEmpty()) return states.stream().map(State::names).toList(); StateCover cover = new StateCover(states); - return cover.smallestCover(cover.largestGroupsWithin(subset), subset).stream().map(cover::names).toList(); + return cover.cover(subset, named).stream().map(cover::names).toList(); } - /** The groups of states inside {@code subset} that no larger group inside it contains, in declaration order */ - private List largestGroupsWithin(Set subset) { + /** The state sets that the groups naming {@code subset} fix, as indexes into {@link State#names()} */ + static Set fixedSets(List states, Set subset) { + if (subset.isEmpty()) + return Set.of(); + StateCover cover = new StateCover(states); + return cover.cover(subset, Set.of()).stream() + .flatMap(group -> IntStream.range(0, group.length).filter(set -> group[set] != ANY).boxed()) + .collect(Collectors.toCollection(TreeSet::new)); + } + + private List cover(Set subset, Set named) { + return smallestCover(largestGroupsWithin(subset, named), subset); + } + + /** + * The groups of states inside {@code subset} that fix the sets {@code named} and that no larger such group + * contains, in declaration order + */ + private List largestGroupsWithin(Set subset, Set named) { List within = new ArrayList<>(); - groups(new int[values.size()], 0, within, subset); + groups(new int[values.size()], 0, within, subset, named); return within.stream().filter(g -> within.stream().noneMatch(other -> other != g && contains(other, g))) .sorted(declarationOrder()).toList(); } - private void groups(int[] group, int set, List within, Set subset) { + private void groups(int[] group, int set, List within, Set subset, Set named) { if (set == values.size()) { if (members(group).stream().allMatch(subset::contains)) within.add(group.clone()); return; } + if (named.contains(set)) { + for (int value = 0; value < values.get(set).size(); value++) { + group[set] = value; + groups(group, set + 1, within, subset, named); + } + return; + } for (int value = ANY; value < values.get(set).size(); value++) { group[set] = value; - groups(group, set + 1, within, subset); + groups(group, set + 1, within, subset, named); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java index 2c3f8d88..3562d3e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java @@ -1,12 +1,18 @@ package liquidjava.processor.state_machine; +import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.function.Supplier; import liquidjava.diagnostics.categories.ErrorCategory; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.GhostState; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; /** * The {@link ErrorCategory} of a call made in a state that does not allow it @@ -21,23 +27,20 @@ private StateErrorCategories() { * the states the receiver can be in before the call * @param found * what is known about the receiver before the call - * @param shownFound - * what the error shows as found: {@code found} with what is known about the values it mentions, such as - * the result of an earlier call that checked the receiver's state + * @param checked + * whether its state was only checked elsewhere, as told by {@link #checkedElsewhere} * @param ghostStates * the ghost states of the receiver's class * * @return the category, or nothing if it cannot be decided */ public static Optional categorize(StateMachine machine, Set current, Predicate found, - Predicate shownFound, List ghostStates) { - List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); - if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) { - // all states are possible and none is mentioned: nothing is known, which differs from a join of every - // state; a state mentioned only through another value, like a check's result, is not a lack of knowledge - return shownFound.getStateInvocations(states).isEmpty() ? Optional.of(ErrorCategory.UNKNOWN) - : Optional.empty(); - } + boolean checked, List ghostStates) { + List states = stateGhosts(ghostStates); + // all states are possible and none is mentioned: nothing is known, which differs from a join of every state + // and from a check whose result did not decide the state + if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) + return checked ? Optional.empty() : Optional.of(ErrorCategory.UNKNOWN); if (current.size() == 1) return Optional.of(ErrorCategory.OUT_OF_ORDER); // with several state sets, the states may differ only in a set the call does not check @@ -46,4 +49,44 @@ public static Optional categorize(StateMachine machine, Set current, Predicate found, + Supplier shownFound, String instance, List ghostStates, StateSolver solver) + throws LJError { + List states = stateGhosts(ghostStates); + if (current.size() != machine.states().size() || !found.getStateInvocations(states).isEmpty()) + return false; + Predicate shown = shownFound.get(); + Predicate receiver = Predicate.createVar(instance); + for (String object : objectsWithState(shown.getExpression(), states, new LinkedHashSet<>())) + if (object.equals(instance) + || solver.implies(shown, Predicate.createEquals(Predicate.createVar(object), receiver))) + return true; + return false; + } + + /** The variables that {@code expression} applies one of {@code states} to */ + private static Set objectsWithState(Expression expression, List states, Set objects) { + if (expression instanceof FunctionInvocation invocation + && states.stream().anyMatch(g -> g.matches(invocation.getName()))) + invocation.getArgs().stream().filter(Var.class::isInstance).map(v -> ((Var) v).getName()) + .forEach(objects::add); + expression.getChildren().forEach(child -> objectsWithState(child, states, objects)); + return objects; + } + + private static List stateGhosts(List ghostStates) { + return ghostStates.stream().filter(g -> g.getParent() != null).toList(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 09012c0d..42f3abfb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -118,7 +118,28 @@ public List constructorsEnabling(RefinedFunction call) { * loud(this)} holds */ public List> describe(Collection subset) { - return StateCover.of(states, Set.copyOf(subset)); + return describe(subset, Set.of()); + } + + /** Like {@link #describe(Collection)}, but naming the state of every set in {@code named} */ + public List> describe(Collection subset, Set named) { + return StateCover.of(states, Set.copyOf(subset), named); + } + + /** + * The state sets that {@code subset} depends on, as indexes into {@link State#names()}: those its + * {@link #describe(Collection) description} names + */ + public Set stateSetsNamed(Collection subset) { + return StateCover.fixedSets(states, Set.copyOf(subset)); + } + + /** The states where {@code method} can be called, for each of its state refinements that applies in some state */ + public List> statesAllowingByRefinement(RefinedFunction method) { + Map> byChange = new LinkedHashMap<>(); + transitions.stream().filter(t -> t.method().equals(method)) + .forEach(t -> byChange.computeIfAbsent(t.change(), c -> new ArrayList<>()).add(t.from())); + return byChange.values().stream().map(this::ordered).toList(); } /** {@code subset} in declaration order */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java index 62bba174..4d24d3de 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java @@ -57,6 +57,18 @@ void nothingKnownAboutStateIsUnknown() { @Test void stateMentionedOnlyByAnEarlierCheckIsNotUnknown() { assertNoCategory("classes/state_hint_checked_state_error"); + assertNoCategory("classes/state_hint_checked_copy_error"); + } + + @Test + void checkOfAnotherObjectLeavesTheStateUnknown() { + assertCategory("classes/state_hint_checked_other_object_error", ErrorCategory.UNKNOWN); + assertCategory("classes/state_hint_checked_wrong_object_error", ErrorCategory.UNKNOWN); + } + + @Test + void joinOfEveryStateOfTwoSetsGetsNoCategory() { + assertNoCategory("ErrorStateHintJoinTwoSets.java"); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 2b1ef6e7..a5b4e019 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -212,6 +212,48 @@ void concreteClassIsToldToCreateANewObject() { + "Objects created with new ErrorStateHintUnknownConcrete() start in such a state")); } + @Test + void checkOfAnotherObjectLeavesTheStateUnknown() { + assertHints("classes/state_hint_checked_other_object_error", + new Hint(Kind.NEEDED_STATE, "The state of it is unknown here, and this call needs it to be hasMore")); + } + + @Test + void callOnAnObjectOtherThanTheCheckedOneLeavesItsStateUnknown() { + assertHints("classes/state_hint_checked_wrong_object_error", new Hint(Kind.NEEDED_STATE, + "The state of other is unknown here, and this call needs it to be hasMore")); + } + + @Test + void checkOfAVariableHoldingTheSameObjectChecksTheReceiver() { + assertHints("classes/state_hint_checked_copy_error", new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of same, and this call needs it to be hasMore")); + } + + @Test + void joinOfEveryStateOfTwoSetsKeepsTheUnreachableHint() { + assertHints("ErrorStateHintJoinTwoSets.java", new Hint(Kind.UNREACHABLE_STATE, + "No sequence of calls moves d from closed and unlocked or closed and locked or opened and unlocked " + + "or opened and locked to closed and unlocked. " + + "Create a new object instead with new ErrorStateHintJoinTwoSets()")); + } + + @Test + void joinDifferingInOneOfTwoSetsNamesTheStatesInTheCheckedSets() { + assertHints("ErrorStateHintJoinOneOfTwoSets.java", new Hint(Kind.UNREACHABLE_STATE, + "No sequence of calls moves d from closed and unlocked or opened and unlocked to closed and unlocked. " + + "Create a new object instead with new ErrorStateHintJoinOneOfTwoSets()"), + new Hint(Kind.AVAILABLE_CALLS, + "In state closed and unlocked or opened and unlocked, d can call: lock()")); + } + + @Test + void callAllowedInEveryStateNamesTheStatesOfEachRefinement() { + assertHints("ErrorStateHintUnknownToggleTwoSets.java", + new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be a or b. " + + "Objects created with new ErrorStateHintUnknownToggleTwoSets() start in such a state")); + } + @Test void stateCheckedByAnEarlierCallIsNotCalledUnknown() { assertHints("classes/state_hint_checked_state_error", new Hint(Kind.NEEDED_STATE, diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 664d4b2e..24d4db72 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -51,6 +51,22 @@ void everyStateIsNamedStateByState() { List.of("closed", "unlocked")), MACHINE.describe(Set.copyOf(MACHINE.states()))); } + @Test + void statesAreNamedInEverySetAsked() { + // the states differ in the first set, which must still be named + assertEquals(List.of(List.of("open", "unlocked"), List.of("closed", "unlocked")), + MACHINE.describe(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED), Set.of(0))); + assertEquals(List.of(List.of("open"), List.of("closed")), + MACHINE.describe(Set.copyOf(MACHINE.states()), Set.of(0))); + } + + @Test + void setsNamedAreThoseTheDescriptionFixes() { + assertEquals(Set.of(1), MACHINE.stateSetsNamed(Set.of(OPEN_UNLOCKED, CLOSED_UNLOCKED))); + assertEquals(Set.of(0, 1), MACHINE.stateSetsNamed(Set.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED))); + assertEquals(Set.of(), MACHINE.stateSetsNamed(Set.of())); + } + @Test void noStatesAreNamedByNothing() { assertEquals(List.of(), MACHINE.describe(Set.of())); From 878738a115f2e0de96506912b16465bb6146e035 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 19:20:22 +0000 Subject: [PATCH 5/5] Tidy the state hint code and keep only the tests that pin a behaviour - StateCover: search the smallest cover exactly, without the greedy fallback, keeping each group's states with it. - StateHints: take the needed states from one source, and give the set of checked state sets and the check flag distinct names. - StateErrorCategories: share the test for "every state possible and none mentioned" between categorize and checkedElsewhere. - StateMachine: derive statesAllowing from statesAllowingByRefinement. - AuxStateHandler: only look for a check when no argument decided the state. - Tests: merge the hint fixtures into one file per behaviour, each with several errors, so far fewer runs of the verifier are needed. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorStateHintConstructors.java | 55 +++++ .../ErrorStateHintJoinOneOfTwoSets.java | 29 --- ...nTwoSets.java => ErrorStateHintJoins.java} | 19 +- .../ErrorStateHintKnownAnyState.java | 31 --- .../java/testSuite/ErrorStateHintNaming.java | 59 +++++ .../testSuite/ErrorStateHintPartlyKnown.java | 25 --- .../ErrorStateHintUnknownAbstract.java | 19 -- .../ErrorStateHintUnknownConcrete.java | 19 -- ...ErrorStateHintUnknownCrossDisjunction.java | 20 -- .../ErrorStateHintUnknownDisjunction.java | 26 --- .../testSuite/ErrorStateHintUnknownField.java | 30 --- .../ErrorStateHintUnknownLongPath.java | 31 --- ...rorStateHintUnknownPrivateConstructor.java | 21 -- .../ErrorStateHintUnknownSeveralWays.java | 28 --- .../testSuite/ErrorStateHintUnknownThis.java | 22 -- .../ErrorStateHintUnknownThreeSets.java | 27 --- .../ErrorStateHintUnknownToggle.java | 20 -- .../ErrorStateHintUnknownToggleTwoSets.java | 21 -- .../ErrorStateHintUnknownTwoRefinements.java | 22 -- .../ErrorStateHintUnknownTwoSetGoal.java | 29 --- .../InputStreamRefinements.java | 20 -- .../state_hint_abstract_spec_error/Use.java | 11 - .../state_hint_checked_copy_error/Reader.java | 14 -- .../state_hint_checked_error/Reader.java | 26 +++ .../ScannerRefinements.java | 2 +- .../Reader.java | 13 -- .../ScannerRefinements.java | 17 -- .../Reader.java | 13 -- .../ScannerRefinements.java | 17 -- .../Reader.java | 13 -- .../ScannerRefinements.java | 17 -- .../RunnableFutureRefinements.java | 17 -- .../state_hint_interface_spec_error/Use.java | 10 - .../diagnostics/hints/StateHints.java | 29 ++- .../object_checkers/AuxStateHandler.java | 2 +- .../processor/state_machine/StateCover.java | 118 +++++----- .../state_machine/StateErrorCategories.java | 19 +- .../processor/state_machine/StateMachine.java | 4 +- .../api/tests/TestErrorCategories.java | 17 -- .../liquidjava/api/tests/TestStateHints.java | 203 +++++------------- 40 files changed, 283 insertions(+), 852 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java rename liquidjava-example/src/main/java/testSuite/{ErrorStateHintJoinTwoSets.java => ErrorStateHintJoins.java} (50%) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java rename liquidjava-example/src/main/java/testSuite/classes/{state_hint_checked_copy_error => state_hint_checked_error}/ScannerRefinements.java (89%) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java new file mode 100644 index 00000000..f1487c62 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java @@ -0,0 +1,55 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Each constructor creates the needed state, but only one that can be called is suggested +@StateSet({"fresh", "ready"}) +public class ErrorStateHintConstructors { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintConstructors() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + // a concrete class: the constructor is suggested + static void concrete(ErrorStateHintConstructors value) { + value.use(); // Expect: State Refinement Error + } + + // the receiver is this object, which a new object would not change + public void self() { + this.use(); // Expect: State Refinement Error + } +} + +@StateSet({"fresh", "ready"}) +abstract class ErrorStateHintConstructorsAbstract { + + @StateRefinement(to = "ready(this)") + public ErrorStateHintConstructorsAbstract() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} + + static void fail(ErrorStateHintConstructorsAbstract value) { + value.use(); // Expect: State Refinement Error + } +} + +@StateSet({"fresh", "ready"}) +class ErrorStateHintConstructorsPrivate { + + @StateRefinement(to = "ready(this)") + private ErrorStateHintConstructorsPrivate() {} + + @StateRefinement(from = "ready(this)", to = "fresh(this)") + public void use() {} +} + +class ErrorStateHintConstructorsPrivateUser { + static void fail(ErrorStateHintConstructorsPrivate value) { + value.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java deleted file mode 100644 index 58cfb5c3..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOneOfTwoSets.java +++ /dev/null @@ -1,29 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The paths differ in one of two state sets, so the states are named in both sets the call checks -@StateSet({"closed", "opened"}) -@StateSet({"unlocked", "locked"}) -public class ErrorStateHintJoinOneOfTwoSets { - - @StateRefinement(to = "closed(this) && unlocked(this)") - public ErrorStateHintJoinOneOfTwoSets() {} - - @StateRefinement(from = "closed(this)", to = "opened(this)") - public void open() {} - - @StateRefinement(from = "unlocked(this)", to = "locked(this)") - public void lock() {} - - @StateRefinement(from = "closed(this) && unlocked(this)") - public void enter() {} - - public static void use(boolean p) { - ErrorStateHintJoinOneOfTwoSets d = new ErrorStateHintJoinOneOfTwoSets(); - if (p) - d.open(); - d.enter(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java similarity index 50% rename from liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java rename to liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java index 8dbfcc1b..7ea7f352 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinTwoSets.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java @@ -3,13 +3,13 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -// Every combination of two state sets is reached on some path: a join of every state, not a lack of knowledge +// Joins of the states reached on different paths are not a lack of knowledge @StateSet({"closed", "opened"}) @StateSet({"unlocked", "locked"}) -public class ErrorStateHintJoinTwoSets { +public class ErrorStateHintJoins { @StateRefinement(to = "closed(this) && unlocked(this)") - public ErrorStateHintJoinTwoSets() {} + public ErrorStateHintJoins() {} @StateRefinement(from = "closed(this)", to = "opened(this)") public void open() {} @@ -20,12 +20,21 @@ public void lock() {} @StateRefinement(from = "closed(this) && unlocked(this)") public void enter() {} - public static void use(boolean p, boolean q) { - ErrorStateHintJoinTwoSets d = new ErrorStateHintJoinTwoSets(); + // every combination of the two state sets is reached on some path + public static void everyState(boolean p, boolean q) { + ErrorStateHintJoins d = new ErrorStateHintJoins(); if (p) d.open(); if (q) d.lock(); d.enter(); // Expect: State Refinement Error } + + // the paths differ in one of the two state sets the call checks, so both states are named in full + public static void oneSet(boolean p) { + ErrorStateHintJoins d = new ErrorStateHintJoins(); + if (p) + d.open(); + d.enter(); // Expect: State Refinement Error + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java deleted file mode 100644 index 64bd2e04..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintKnownAnyState.java +++ /dev/null @@ -1,31 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The class of ErrorStateHintUnknownAnyState with a known state: the hint starts from that state -@StateSet({"created", "open", "closed"}) -public class ErrorStateHintKnownAnyState { - - @StateRefinement(to = "created(this)") - public ErrorStateHintKnownAnyState() {} - - @StateRefinement(to = "created(this)") - public void reset() {} - - @StateRefinement(from = "created(this)", to = "open(this)") - public void open() {} - - @StateRefinement(from = "open(this)") - public void read() {} - - @StateRefinement(from = "open(this)", to = "closed(this)") - public void close() {} - - public static void main(String[] args) { - ErrorStateHintKnownAnyState f = new ErrorStateHintKnownAnyState(); - f.open(); - f.close(); - f.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java new file mode 100644 index 00000000..c91896ed --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java @@ -0,0 +1,59 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The needed and current states are named only in the state sets that matter +@StateSet({"created", "open", "ready"}) +@StateSet({"quiet", "loud"}) +public class ErrorStateHintNaming { + + @StateRefinement(to = "created(this) && quiet(this)") + public ErrorStateHintNaming() {} + + // a state of either set: each is named alone, not combined with every state of the other set + @StateRefinement(from = "open(this) || loud(this)") + public void read() {} + + public static void use(ErrorStateHintNaming s) { + s.read(); // Expect: State Refinement Error + } +} + +// every state allows flip(), each by its own refinement: a or b, not all six states +@StateSet({"a", "b"}) +@StateSet({"x", "y", "z"}) +class ErrorStateHintNamingToggle { + + @StateRefinement(to = "a(this) && x(this)") + public ErrorStateHintNamingToggle() {} + + @StateRefinement(from = "a(this)", to = "b(this)") + @StateRefinement(from = "b(this)", to = "a(this)") + public void flip() {} + + public static void use(ErrorStateHintNamingToggle t) { + t.flip(); // Expect: State Refinement Error + } +} + +// known in one of three state sets: only that set is named +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +class ErrorStateHintNamingPartlyKnown { + + @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") + public ErrorStateHintNamingPartlyKnown() {} + + @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") + public void redo() {} + + @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") + public void undo() {} + + @StateRefinement(from = "notRedoable(this)") + public void check() { + this.redo(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java deleted file mode 100644 index 53b35f87..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintPartlyKnown.java +++ /dev/null @@ -1,25 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// Only one of three state sets is known (notRedoable), so the hints name that set only -@StateSet({"start", "canEdit", "end"}) -@StateSet({"undoable", "notUndoable"}) -@StateSet({"redoable", "notRedoable"}) -public class ErrorStateHintPartlyKnown { - - @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") - public ErrorStateHintPartlyKnown() {} - - @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") - public void redo() {} - - @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") - public void undo() {} - - @StateRefinement(from = "notRedoable(this)") - public void check() { - this.redo(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java deleted file mode 100644 index c407ba76..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAbstract.java +++ /dev/null @@ -1,19 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The constructor creates the needed state, but the class is abstract, so no new object can be suggested -@StateSet({"fresh", "ready"}) -public abstract class ErrorStateHintUnknownAbstract { - - @StateRefinement(to = "ready(this)") - public ErrorStateHintUnknownAbstract() {} - - @StateRefinement(from = "ready(this)", to = "fresh(this)") - public void use() {} - - static void fail(ErrorStateHintUnknownAbstract value) { - value.use(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java deleted file mode 100644 index dc18804c..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownConcrete.java +++ /dev/null @@ -1,19 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The same class as ErrorStateHintUnknownAbstract, but concrete: the constructor is suggested -@StateSet({"fresh", "ready"}) -public class ErrorStateHintUnknownConcrete { - - @StateRefinement(to = "ready(this)") - public ErrorStateHintUnknownConcrete() {} - - @StateRefinement(from = "ready(this)", to = "fresh(this)") - public void use() {} - - static void fail(ErrorStateHintUnknownConcrete value) { - value.use(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java deleted file mode 100644 index 123a3fbf..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownCrossDisjunction.java +++ /dev/null @@ -1,20 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// read() accepts a state of either set, so each is named alone, not combined with every state of the other set -@StateSet({"created", "open", "ready"}) -@StateSet({"quiet", "loud"}) -public class ErrorStateHintUnknownCrossDisjunction { - - @StateRefinement(to = "created(this) && quiet(this)") - public ErrorStateHintUnknownCrossDisjunction() {} - - @StateRefinement(from = "open(this) || loud(this)") - public void read() {} - - public static void use(ErrorStateHintUnknownCrossDisjunction s) { - s.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java deleted file mode 100644 index 4241b7a2..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownDisjunction.java +++ /dev/null @@ -1,26 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// read() accepts two states of one set. The other set is not named, and no call reaches either state from any state -@StateSet({"created", "open", "ready"}) -@StateSet({"quiet", "loud"}) -public class ErrorStateHintUnknownDisjunction { - - @StateRefinement(to = "created(this) && quiet(this)") - public ErrorStateHintUnknownDisjunction() {} - - @StateRefinement(from = "created(this)", to = "open(this)") - public void open() {} - - @StateRefinement(from = "open(this) || ready(this)") - public void read() {} - - @StateRefinement(to = "loud(this)") - public void shout() {} - - public static void use(ErrorStateHintUnknownDisjunction s) { - s.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java deleted file mode 100644 index 71898816..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownField.java +++ /dev/null @@ -1,30 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// A field whose state is unknown: forceOpen() works in any state, and only the state set read() checks is named -@StateSet({"closed", "opened"}) -@StateSet({"unlocked", "locked"}) -public class ErrorStateHintUnknownField { - - @StateRefinement(to = "closed(this) && unlocked(this)") - public ErrorStateHintUnknownField() {} - - @StateRefinement(to = "opened(this)") - public void forceOpen() {} - - @StateRefinement(from = "opened(this)") - public void read() {} - - @StateRefinement(from = "locked(this)", to = "unlocked(this)") - public void unlock() {} -} - -class ErrorStateHintUnknownFieldUser { - ErrorStateHintUnknownField door; - - void use() { - door.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java deleted file mode 100644 index f7499aff..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownLongPath.java +++ /dev/null @@ -1,31 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// From any state, go() needs four calls (reset, a, b, c), more than a hint suggests -@StateSet({"s0", "s1", "s2", "s3"}) -public class ErrorStateHintUnknownLongPath { - - @StateRefinement(to = "s0(this)") - public ErrorStateHintUnknownLongPath() {} - - @StateRefinement(to = "s0(this)") - public void reset() {} - - @StateRefinement(from = "s0(this)", to = "s1(this)") - public void a() {} - - @StateRefinement(from = "s1(this)", to = "s2(this)") - public void b() {} - - @StateRefinement(from = "s2(this)", to = "s3(this)") - public void c() {} - - @StateRefinement(from = "s3(this)") - public void go() {} - - public static void use(ErrorStateHintUnknownLongPath x) { - x.go(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java deleted file mode 100644 index d77d253f..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownPrivateConstructor.java +++ /dev/null @@ -1,21 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The constructor creates the needed state, but it is private, so no new object can be suggested -@StateSet({"fresh", "ready"}) -public class ErrorStateHintUnknownPrivateConstructor { - - @StateRefinement(to = "ready(this)") - private ErrorStateHintUnknownPrivateConstructor() {} - - @StateRefinement(from = "ready(this)", to = "fresh(this)") - public void use() {} -} - -class ErrorStateHintUnknownPrivateConstructorUser { - static void fail(ErrorStateHintUnknownPrivateConstructor value) { - value.use(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java deleted file mode 100644 index da359dd0..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownSeveralWays.java +++ /dev/null @@ -1,28 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// go() accepts s1 or s2, and a different call reaches each of them from any state -@StateSet({"s0", "s1", "s2", "s3"}) -public class ErrorStateHintUnknownSeveralWays { - - @StateRefinement(to = "s0(this)") - public ErrorStateHintUnknownSeveralWays() {} - - @StateRefinement(to = "s1(this)") - public void one() {} - - @StateRefinement(to = "s2(this)") - public void two() {} - - @StateRefinement(to = "s3(this)") - public void three() {} - - @StateRefinement(from = "s1(this) || s2(this)") - public void go() {} - - public static void use(ErrorStateHintUnknownSeveralWays x) { - x.go(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java deleted file mode 100644 index 32294528..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThis.java +++ /dev/null @@ -1,22 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The receiver is this, so creating a new object, though it would start in open, is not suggested -@StateSet({"open", "closed"}) -public class ErrorStateHintUnknownThis { - - @StateRefinement(to = "open(this)") - public ErrorStateHintUnknownThis() {} - - @StateRefinement(from = "open(this)") - public void read() {} - - @StateRefinement(from = "open(this)", to = "closed(this)") - public void close() {} - - public void helper() { - this.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java deleted file mode 100644 index 5569cbef..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownThreeSets.java +++ /dev/null @@ -1,27 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// Only the state set that redo() checks is named, not its combinations with the other two -@StateSet({"start", "canEdit", "end"}) -@StateSet({"undoable", "notUndoable"}) -@StateSet({"redoable", "notRedoable"}) -public class ErrorStateHintUnknownThreeSets { - - @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") - public ErrorStateHintUnknownThreeSets() {} - - @StateRefinement(from = "start(this)", to = "canEdit(this)") - public void addEdit() {} - - @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)") - public void redo() {} - - @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)") - public void undo() {} - - public static void redoLast(ErrorStateHintUnknownThreeSets history) { - history.redo(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java deleted file mode 100644 index b5287264..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggle.java +++ /dev/null @@ -1,20 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// flip() is allowed in every state, but by a different state refinement in each, so an unknown state rejects it -@StateSet({"up", "down"}) -public class ErrorStateHintUnknownToggle { - - @StateRefinement(to = "up(this)") - public ErrorStateHintUnknownToggle() {} - - @StateRefinement(from = "up(this)", to = "down(this)") - @StateRefinement(from = "down(this)", to = "up(this)") - public void flip() {} - - public static void use(ErrorStateHintUnknownToggle t) { - t.flip(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java deleted file mode 100644 index 761a0653..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownToggleTwoSets.java +++ /dev/null @@ -1,21 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// Every state allows flip(), by the refinement for a or the one for b, so the hint names a or b, not all six states -@StateSet({"a", "b"}) -@StateSet({"x", "y", "z"}) -public class ErrorStateHintUnknownToggleTwoSets { - - @StateRefinement(to = "a(this) && x(this)") - public ErrorStateHintUnknownToggleTwoSets() {} - - @StateRefinement(from = "a(this)", to = "b(this)") - @StateRefinement(from = "b(this)", to = "a(this)") - public void flip() {} - - public static void use(ErrorStateHintUnknownToggleTwoSets t) { - t.flip(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java deleted file mode 100644 index 525db2d9..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoRefinements.java +++ /dev/null @@ -1,22 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// Like UndoManager.undoOrRedo(): one state refinement per state set, so the call needs undoable or redoable -@StateSet({"start", "canEdit", "end"}) -@StateSet({"undoable", "notUndoable"}) -@StateSet({"redoable", "notRedoable"}) -public class ErrorStateHintUnknownTwoRefinements { - - @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)") - public ErrorStateHintUnknownTwoRefinements() {} - - @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && notRedoable(this)") - @StateRefinement(from = "redoable(this)", to = "notUndoable(this) && notRedoable(this)") - public void undoOrRedo() {} - - public static void use(ErrorStateHintUnknownTwoRefinements history) { - history.undoOrRedo(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java deleted file mode 100644 index 8cb92474..00000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownTwoSetGoal.java +++ /dev/null @@ -1,29 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// open() checks both state sets, so both are named. reset() reaches them from any state; slam() fixes only one set -@StateSet({"closed", "opened"}) -@StateSet({"unlocked", "locked"}) -public class ErrorStateHintUnknownTwoSetGoal { - - @StateRefinement(to = "closed(this) && unlocked(this)") - public ErrorStateHintUnknownTwoSetGoal() {} - - @StateRefinement(to = "closed(this) && unlocked(this)") - public void reset() {} - - @StateRefinement(to = "closed(this)") - public void slam() {} - - @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)") - public void open() {} - - @StateRefinement(from = "locked(this)", to = "unlocked(this)") - public void unlock() {} - - public static void enter(ErrorStateHintUnknownTwoSetGoal door) { - door.open(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java deleted file mode 100644 index 726b1d8e..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/InputStreamRefinements.java +++ /dev/null @@ -1,20 +0,0 @@ -package testSuite.classes.state_hint_abstract_spec_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// A spec for an abstract JDK class: its constructor creates the needed state, but no client can call new InputStream() -@ExternalRefinementsFor("java.io.InputStream") -@StateSet({"open", "closed"}) -public interface InputStreamRefinements { - - @StateRefinement(to = "open(this)") - void InputStream(); - - @StateRefinement(from = "open(this)") - int read(); - - @StateRefinement(from = "open(this)", to = "closed(this)") - void close(); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java deleted file mode 100644 index 8640cbbf..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_abstract_spec_error/Use.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite.classes.state_hint_abstract_spec_error; - -import java.io.IOException; -import java.io.InputStream; - -public class Use { - - static int first(InputStream in) throws IOException { - return in.read(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java deleted file mode 100644 index 84181e98..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/Reader.java +++ /dev/null @@ -1,14 +0,0 @@ -package testSuite.classes.state_hint_checked_copy_error; - -import java.util.Scanner; - -// The failed check is on it and the call on a variable holding the same scanner, so the state was checked -public class Reader { - - public static void nextOfTheSameScanner(Scanner it) { - Scanner same = it; - if (!it.hasNext()) { - same.next(); // Expect: State Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java new file mode 100644 index 00000000..1477fa12 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_hint_checked_error; + +import java.util.Scanner; + +// A failed check of the receiver does not decide its state; a check of another object says nothing about it +public class Reader { + + public static void failedCheck(Scanner it) { + if (!it.hasNext()) { + it.next(); // Expect: State Refinement Error + } + } + + public static void failedCheckOfTheSameScanner(Scanner scanner) { + Scanner same = scanner; + if (!scanner.hasNext()) { + same.next(); // Expect: State Refinement Error + } + } + + public static void checkOfAnotherScanner(Scanner other, Scanner input) { + if (other.hasNext()) { + input.next(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java similarity index 89% rename from liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java rename to liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java index 34b6e53a..3f39486d 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_copy_error/ScannerRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java @@ -1,4 +1,4 @@ -package testSuite.classes.state_hint_checked_copy_error; +package testSuite.classes.state_hint_checked_error; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java deleted file mode 100644 index 69bbbcbc..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/Reader.java +++ /dev/null @@ -1,13 +0,0 @@ -package testSuite.classes.state_hint_checked_other_object_error; - -import java.util.Scanner; - -// Another scanner was checked, so nothing is known about the state of the receiver -public class Reader { - - public static void nextOfTheOther(Scanner other, Scanner it) { - if (other.hasNext()) { - it.next(); // Expect: State Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java deleted file mode 100644 index deb922b3..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_other_object_error/ScannerRefinements.java +++ /dev/null @@ -1,17 +0,0 @@ -package testSuite.classes.state_hint_checked_other_object_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@StateSet({"hasMore", "noMore"}) -@ExternalRefinementsFor("java.util.Scanner") -public interface ScannerRefinements { - - @Refinement("_ == true --> hasMore(this)") - boolean hasNext(); - - @StateRefinement(from = "hasMore(this)", to = "noMore(this)") - String next(); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java deleted file mode 100644 index a9d50e63..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/Reader.java +++ /dev/null @@ -1,13 +0,0 @@ -package testSuite.classes.state_hint_checked_state_error; - -import java.util.Scanner; - -// The state was checked and the check failed: the state is not unknown, but the check does not decide it either -public class Reader { - - public static void nextWhenThereIsNone(Scanner it) { - if (!it.hasNext()) { - it.next(); // Expect: State Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java deleted file mode 100644 index 7dedf5ed..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_state_error/ScannerRefinements.java +++ /dev/null @@ -1,17 +0,0 @@ -package testSuite.classes.state_hint_checked_state_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@StateSet({"hasMore", "noMore"}) -@ExternalRefinementsFor("java.util.Scanner") -public interface ScannerRefinements { - - @Refinement("_ == true --> hasMore(this)") - boolean hasNext(); - - @StateRefinement(from = "hasMore(this)", to = "noMore(this)") - String next(); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java deleted file mode 100644 index 035aa37a..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/Reader.java +++ /dev/null @@ -1,13 +0,0 @@ -package testSuite.classes.state_hint_checked_wrong_object_error; - -import java.util.Scanner; - -// The check is on it, but the call is on another scanner, whose state is unknown -public class Reader { - - public static void checkedTheWrongObject(Scanner it, Scanner other) { - if (it.hasNext()) { - other.next(); // Expect: State Refinement Error - } - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java deleted file mode 100644 index 8c436aab..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_wrong_object_error/ScannerRefinements.java +++ /dev/null @@ -1,17 +0,0 @@ -package testSuite.classes.state_hint_checked_wrong_object_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@StateSet({"hasMore", "noMore"}) -@ExternalRefinementsFor("java.util.Scanner") -public interface ScannerRefinements { - - @Refinement("_ == true --> hasMore(this)") - boolean hasNext(); - - @StateRefinement(from = "hasMore(this)", to = "noMore(this)") - String next(); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java deleted file mode 100644 index 52c1c948..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/RunnableFutureRefinements.java +++ /dev/null @@ -1,17 +0,0 @@ -package testSuite.classes.state_hint_interface_spec_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// A spec for an interface: it has no constructor, so no new object is suggested -@ExternalRefinementsFor("java.util.concurrent.RunnableFuture") -@StateSet({"pending", "done"}) -public interface RunnableFutureRefinements { - - @StateRefinement(from = "pending(this)", to = "done(this)") - void run(); - - @StateRefinement(from = "done(this)") - boolean isDone(); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java deleted file mode 100644 index 0600c134..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_interface_spec_error/Use.java +++ /dev/null @@ -1,10 +0,0 @@ -package testSuite.classes.state_hint_interface_spec_error; - -import java.util.concurrent.RunnableFuture; - -public class Use { - - static boolean finished(RunnableFuture task) { - return task.isDone(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 6ce60139..f173b383 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -38,13 +38,13 @@ public final class StateHints { /** The states that allow the failing call, grouped by the state refinement that allows it */ private final List> goals; /** The state sets the failing call checks, as indexes into {@link State#names()} */ - private final Set checked; + private final Set checkedSets; private StateHints(StateMachine machine, String receiver, RefinedFunction call) { this.machine = machine; this.receiver = receiver; this.goals = machine.statesAllowingByRefinement(call); - this.checked = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) + this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) .collect(Collectors.toCollection(TreeSet::new)); } @@ -57,21 +57,20 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call) * the receiver as written in the code * @param category * the error's category, or {@code null} if it has none - * @param checked + * @param checkedElsewhere * whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose * result says which state it is in */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category, boolean checked) { + ErrorCategory category, boolean checkedElsewhere) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed - Set goal = machine.statesAllowing(call); - if (goal.isEmpty()) + StateHints hints = new StateHints(machine, receiver, call); + if (hints.goals.isEmpty()) return List.of(); - StateHints hints = new StateHints(machine, receiver, call); - if (category == ErrorCategory.UNKNOWN || checked) - return hints.anyState(current, call, checked); + if (category == ErrorCategory.UNKNOWN || checkedElsewhere) + return hints.anyState(current, call, checkedElsewhere); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; List sequences = hints.howToReach(current, call, hints.namesHere(current), () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); @@ -95,11 +94,11 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) * A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that * only tell which state the object is in are not in the machine, so no hint suggests checking one first. * - * @param checked + * @param checkedElsewhere * whether the state was checked, though the check did not decide it */ - private List anyState(Set current, RefinedFunction call, boolean checked) { - String known = checked ? "What is known here does not decide the state of " + receiver + private List anyState(Set current, RefinedFunction call, boolean checkedElsewhere) { + String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver : "The state of " + receiver + " is unknown here"; String message = known + ", and this call needs it to be " + needed(); message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); @@ -195,12 +194,12 @@ private static String parameters(RefinedFunction function) { /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ private String names(Collection states) { - return names(machine.describe(states)); + return join(machine.describe(states)); } /** The states the receiver can be in, named in the state sets the call checks and any set they all agree on */ private String namesHere(Collection current) { - return names(machine.describe(current, checked)); + return join(machine.describe(current, checkedSets)); } /** @@ -214,7 +213,7 @@ private String needed() { return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or ")); } - private static String names(List> groups) { + private static String join(List> groups) { return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or ")); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 90a068fd..6d17712b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -795,7 +795,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, instanceName, prevState, invocation); Predicate expected = expectedStatesDisjunction; - boolean checked = states + boolean checked = deciding.isEmpty() && states .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, ghostStates, invocation)) .orElse(false); ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states.flatMap( diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java index 4ef2b8c3..4909824a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateCover.java @@ -17,13 +17,18 @@ */ final class StateCover { + private static final int ANY = -1; + /** - * Above this many candidate groups, the smallest cover is approximated instead of searched for. With several state - * sets and the machine's limit of 16 states there are at most 13; with one state set the groups are single states, - * which the approximation covers exactly. + * States that fix the state of some state sets and allow any state in the others + * + * @param values + * the index of the fixed state in each state set, or {@link #ANY} + * @param members + * the states in the group */ - private static final int MAX_EXACT = 13; - private static final int ANY = -1; + private record Group(int[] values, Set members) { + } private final List states; private final List> values; @@ -54,76 +59,59 @@ static List> of(List states, Set subset, Set } /** The state sets that the groups naming {@code subset} fix, as indexes into {@link State#names()} */ - static Set fixedSets(List states, Set subset) { + static Set namedSets(List states, Set subset) { if (subset.isEmpty()) return Set.of(); - StateCover cover = new StateCover(states); - return cover.cover(subset, Set.of()).stream() - .flatMap(group -> IntStream.range(0, group.length).filter(set -> group[set] != ANY).boxed()) + return new StateCover(states).cover(subset, Set.of()).stream().flatMap( + group -> IntStream.range(0, group.values().length).filter(set -> group.values()[set] != ANY).boxed()) .collect(Collectors.toCollection(TreeSet::new)); } - private List cover(Set subset, Set named) { - return smallestCover(largestGroupsWithin(subset, named), subset); + /** The fewest of the largest groups inside {@code subset} that fix the sets {@code named} and hold all of it */ + private List cover(Set subset, Set named) { + List candidates = largestGroupsWithin(subset, named); + for (int size = 1;; size++) { + List chosen = firstCover(candidates, subset, size, 0, new ArrayList<>()); + if (chosen != null) + return chosen; + } } - /** - * The groups of states inside {@code subset} that fix the sets {@code named} and that no larger such group - * contains, in declaration order - */ - private List largestGroupsWithin(Set subset, Set named) { - List within = new ArrayList<>(); + /** The groups inside {@code subset} that fix the sets {@code named} and no larger such group holds */ + private List largestGroupsWithin(Set subset, Set named) { + List within = new ArrayList<>(); groups(new int[values.size()], 0, within, subset, named); return within.stream().filter(g -> within.stream().noneMatch(other -> other != g && contains(other, g))) .sorted(declarationOrder()).toList(); } - private void groups(int[] group, int set, List within, Set subset, Set named) { + /** Whether {@code larger} fixes fewer state sets than {@code smaller}, to the same states */ + private static boolean contains(Group larger, Group smaller) { + return !Arrays.equals(larger.values(), smaller.values()) && IntStream.range(0, larger.values().length) + .allMatch(set -> larger.values()[set] == ANY || larger.values()[set] == smaller.values()[set]); + } + + private void groups(int[] group, int set, List within, Set subset, Set named) { if (set == values.size()) { - if (members(group).stream().allMatch(subset::contains)) - within.add(group.clone()); + Set members = members(group); + if (subset.containsAll(members)) + within.add(new Group(group.clone(), members)); return; } - if (named.contains(set)) { - for (int value = 0; value < values.get(set).size(); value++) { - group[set] = value; - groups(group, set + 1, within, subset, named); - } - return; - } - for (int value = ANY; value < values.get(set).size(); value++) { + for (int value = named.contains(set) ? 0 : ANY; value < values.get(set).size(); value++) { group[set] = value; groups(group, set + 1, within, subset, named); } } - /** The fewest of {@code candidates} that together hold every state of {@code subset} */ - private List smallestCover(List candidates, Set subset) { - if (candidates.size() <= MAX_EXACT) { - for (int size = 1; size <= candidates.size(); size++) { - List chosen = firstCover(candidates, subset, size, 0, new ArrayList<>()); - if (chosen != null) - return chosen; - } - } - List chosen = new ArrayList<>(); - Set left = new HashSet<>(subset); - while (!left.isEmpty()) { - int[] best = candidates.stream() - .max(Comparator.comparingLong(g -> members(g).stream().filter(left::contains).count())).get(); - chosen.add(best); - members(best).forEach(left::remove); - } - return chosen.stream().sorted(declarationOrder()).toList(); - } - - /** The first {@code size} candidates from {@code next} on, in order, that cover {@code subset}, or null */ - private List firstCover(List candidates, Set subset, int size, int next, List chosen) { + /** The first {@code size} candidates from {@code next} on, in order, that hold all of {@code subset}, or null */ + private static List firstCover(List candidates, Set subset, int size, int next, + List chosen) { if (chosen.size() == size) return covers(chosen, subset) ? List.copyOf(chosen) : null; for (int i = next; i < candidates.size(); i++) { chosen.add(candidates.get(i)); - List found = firstCover(candidates, subset, size, i + 1, chosen); + List found = firstCover(candidates, subset, size, i + 1, chosen); chosen.remove(chosen.size() - 1); if (found != null) return found; @@ -131,31 +119,25 @@ private List firstCover(List candidates, Set subset, int si return null; } - private boolean covers(List groups, Set subset) { + private static boolean covers(List groups, Set subset) { Set covered = new HashSet<>(); - groups.forEach(g -> covered.addAll(members(g))); + groups.forEach(g -> covered.addAll(g.members())); return covered.containsAll(subset); } - private List members(int[] group) { + private Set members(int[] group) { return states.stream() .filter(s -> IntStream.range(0, group.length).allMatch( set -> group[set] == ANY || values.get(set).get(group[set]).equals(s.names().get(set)))) - .toList(); - } - - /** Whether {@code larger} holds every state of {@code smaller} */ - private static boolean contains(int[] larger, int[] smaller) { - return !Arrays.equals(larger, smaller) - && IntStream.range(0, larger.length).allMatch(set -> larger[set] == ANY || larger[set] == smaller[set]); + .collect(Collectors.toSet()); } /** Groups fixing earlier state sets first, then by the order of the states within a set */ - private static Comparator declarationOrder() { + private static Comparator declarationOrder() { return (a, b) -> { - for (int set = 0; set < a.length; set++) { - int x = a[set] == ANY ? Integer.MAX_VALUE : a[set]; - int y = b[set] == ANY ? Integer.MAX_VALUE : b[set]; + for (int set = 0; set < a.values().length; set++) { + int x = a.values()[set] == ANY ? Integer.MAX_VALUE : a.values()[set]; + int y = b.values()[set] == ANY ? Integer.MAX_VALUE : b.values()[set]; if (x != y) return Integer.compare(x, y); } @@ -163,8 +145,8 @@ private static Comparator declarationOrder() { }; } - private List names(int[] group) { - return IntStream.range(0, group.length).filter(set -> group[set] != ANY) - .mapToObj(set -> values.get(set).get(group[set])).toList(); + private List names(Group group) { + return IntStream.range(0, group.values().length).filter(set -> group.values()[set] != ANY) + .mapToObj(set -> values.get(set).get(group.values()[set])).toList(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java index 3562d3e8..03ff1d0a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java @@ -27,7 +27,7 @@ private StateErrorCategories() { * the states the receiver can be in before the call * @param found * what is known about the receiver before the call - * @param checked + * @param checkedElsewhere * whether its state was only checked elsewhere, as told by {@link #checkedElsewhere} * @param ghostStates * the ghost states of the receiver's class @@ -35,12 +35,11 @@ private StateErrorCategories() { * @return the category, or nothing if it cannot be decided */ public static Optional categorize(StateMachine machine, Set current, Predicate found, - boolean checked, List ghostStates) { + boolean checkedElsewhere, List ghostStates) { List states = stateGhosts(ghostStates); - // all states are possible and none is mentioned: nothing is known, which differs from a join of every state - // and from a check whose result did not decide the state - if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) - return checked ? Optional.empty() : Optional.of(ErrorCategory.UNKNOWN); + // nothing is known, which differs from a join of every state and from a check that did not decide the state + if (nothingMentioned(machine, current, found, states)) + return checkedElsewhere ? Optional.empty() : Optional.of(ErrorCategory.UNKNOWN); if (current.size() == 1) return Optional.of(ErrorCategory.OUT_OF_ORDER); // with several state sets, the states may differ only in a set the call does not check @@ -65,7 +64,7 @@ public static boolean checkedElsewhere(StateMachine machine, Set current, Supplier shownFound, String instance, List ghostStates, StateSolver solver) throws LJError { List states = stateGhosts(ghostStates); - if (current.size() != machine.states().size() || !found.getStateInvocations(states).isEmpty()) + if (!nothingMentioned(machine, current, found, states)) return false; Predicate shown = shownFound.get(); Predicate receiver = Predicate.createVar(instance); @@ -86,6 +85,12 @@ private static Set objectsWithState(Expression expression, List current, Predicate found, + List states) { + return current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty(); + } + private static List stateGhosts(List ghostStates) { return ghostStates.stream().filter(g -> g.getParent() != null).toList(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 42f3abfb..524b079a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -66,7 +66,7 @@ public List allowedIn(Set current) { /** The states where {@code method} can be called */ public Set statesAllowing(RefinedFunction method) { - return ordered(transitions.stream().filter(t -> t.method().equals(method)).map(Transition::from).toList()); + return ordered(statesAllowingByRefinement(method).stream().flatMap(Set::stream).toList()); } /** The states the object can be in after calling {@code method}, which must be allowed in all of {@code current} */ @@ -131,7 +131,7 @@ public List> describe(Collection subset, Set named) * {@link #describe(Collection) description} names */ public Set stateSetsNamed(Collection subset) { - return StateCover.fixedSets(states, Set.copyOf(subset)); + return StateCover.namedSets(states, Set.copyOf(subset)); } /** The states where {@code method} can be called, for each of its state refinements that applies in some state */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java index 4d24d3de..2d978d4e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java @@ -54,23 +54,6 @@ void nothingKnownAboutStateIsUnknown() { assertCategory("ErrorStateHintUnknownState.java", ErrorCategory.UNKNOWN); } - @Test - void stateMentionedOnlyByAnEarlierCheckIsNotUnknown() { - assertNoCategory("classes/state_hint_checked_state_error"); - assertNoCategory("classes/state_hint_checked_copy_error"); - } - - @Test - void checkOfAnotherObjectLeavesTheStateUnknown() { - assertCategory("classes/state_hint_checked_other_object_error", ErrorCategory.UNKNOWN); - assertCategory("classes/state_hint_checked_wrong_object_error", ErrorCategory.UNKNOWN); - } - - @Test - void joinOfEveryStateOfTwoSetsGetsNoCategory() { - assertNoCategory("ErrorStateHintJoinTwoSets.java"); - } - @Test void stateErrorWithoutStateSetGetsNoCategory() { assertNoCategory("ErrorUnconstrainedStateRefinement.java"); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index a5b4e019..ce9eded2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -3,11 +3,13 @@ import static org.junit.jupiter.api.Assertions.*; import java.util.List; +import java.util.Optional; import org.junit.jupiter.api.Test; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.diagnostics.hints.Hint; @@ -96,12 +98,6 @@ void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { "The state of undoManager is unknown here, and this call needs it to be redoable")); } - @Test - void unknownStateWithThreeStateSetsNamesOnlyTheCheckedOne() { - assertHints("ErrorStateHintUnknownThreeSets.java", new Hint(Kind.NEEDED_STATE, - "The state of history is unknown here, and this call needs it to be redoable")); - } - @Test void unknownStateSuggestsCallsAllowedInAnyState() { assertHints("ErrorStateHintUnknownAnyState.java", @@ -111,167 +107,58 @@ void unknownStateSuggestsCallsAllowedInAnyState() { } @Test - void knownStateStartsTheSequenceFromThatState() { - assertHints("ErrorStateHintKnownAnyState.java", - new Hint(Kind.CALL_SEQUENCE, - "Call f.reset(), then f.open() before this call to move f from closed to open"), - new Hint(Kind.AVAILABLE_CALLS, "In state closed, f can call: reset()")); - } - - @Test - void unknownStateNamesEveryStateSetTheCallChecks() { - assertHints("ErrorStateHintUnknownTwoSetGoal.java", - new Hint(Kind.NEEDED_STATE, - "The state of door is unknown here, and this call needs it to be closed and unlocked. " - + "Objects created with new ErrorStateHintUnknownTwoSetGoal() start in such a state"), - new Hint(Kind.CALL_SEQUENCE, - "Call door.reset() before this call to move door from any state to closed and unlocked")); - } - - @Test - void unknownStateOfAFieldSuggestsCallsAllowedInAnyState() { - assertHints("ErrorStateHintUnknownField.java", - new Hint(Kind.NEEDED_STATE, "The state of door is unknown here, and this call needs it to be opened"), - new Hint(Kind.CALL_SEQUENCE, - "Call door.forceOpen() before this call to move door from any state to opened")); - } - - @Test - void unknownStateNamesEveryStateTheCallAccepts() { - assertHints("ErrorStateHintUnknownDisjunction.java", new Hint(Kind.NEEDED_STATE, - "The state of s is unknown here, and this call needs it to be open or ready")); - } - - @Test - void disjunctionAcrossStateSetsNamesEachStateAlone() { - assertHints("ErrorStateHintUnknownCrossDisjunction.java", new Hint(Kind.NEEDED_STATE, + void statesAreNamedOnlyInTheStateSetsThatMatter() { + List errors = errors("ErrorStateHintNaming.java", 3); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, "The state of s is unknown here, and this call needs it to be open or loud")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be a or b. " + + "Objects created with new ErrorStateHintNamingToggle() start in such a state")); + assertHints(errors.get(2), + new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable"), + new Hint(Kind.AVAILABLE_CALLS, "In state notRedoable, this can call: check()")); } @Test - void oneRefinementPerStateSetNamesEachStateAlone() { - assertHints("ErrorStateHintUnknownTwoRefinements.java", new Hint(Kind.NEEDED_STATE, - "The state of history is unknown here, and this call needs it to be undoable or redoable")); - } - - @Test - void callAllowedInEveryStateByDifferentRefinementsStillNamesTheStatesAndConstructors() { - assertHints("ErrorStateHintUnknownToggle.java", - new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be up or down. " - + "Objects created with new ErrorStateHintUnknownToggle() start in such a state")); - } - - @Test - void unknownStateDoesNotSuggestSequencesLongerThanTheLimit() { - assertHints("ErrorStateHintUnknownLongPath.java", - new Hint(Kind.NEEDED_STATE, "The state of x is unknown here, and this call needs it to be s3")); - } - - @Test - void unknownStateSuggestsEverySequenceOfTheShortestLength() { - assertHints("ErrorStateHintUnknownSeveralWays.java", - new Hint(Kind.NEEDED_STATE, "The state of x is unknown here, and this call needs it to be s1 or s2"), - new Hint(Kind.CALL_SEQUENCE, "Call x.one() before this call to move x from any state to s1"), - new Hint(Kind.CALL_SEQUENCE, "Call x.two() before this call to move x from any state to s2")); - } - - @Test - void thisReceiverIsNotToldToCreateANewObject() { - assertHints("ErrorStateHintUnknownThis.java", - new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be open")); - } - - @Test - void abstractClassIsNotToldToCreateANewObject() { - assertHints("ErrorStateHintUnknownAbstract.java", - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); - } - - @Test - void abstractClassWithAnExternalSpecIsNotToldToCreateANewObject() { - assertHints("classes/state_hint_abstract_spec_error", - new Hint(Kind.NEEDED_STATE, "The state of in is unknown here, and this call needs it to be open")); - } - - @Test - void interfaceWithAnExternalSpecIsNotToldToCreateANewObject() { - assertHints("classes/state_hint_interface_spec_error", - new Hint(Kind.NEEDED_STATE, "The state of task is unknown here, and this call needs it to be done")); - } - - @Test - void privateConstructorIsNotSuggested() { - assertHints("ErrorStateHintUnknownPrivateConstructor.java", - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); - } - - @Test - void concreteClassIsToldToCreateANewObject() { - assertHints("ErrorStateHintUnknownConcrete.java", - new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready. " - + "Objects created with new ErrorStateHintUnknownConcrete() start in such a state")); - } - - @Test - void checkOfAnotherObjectLeavesTheStateUnknown() { - assertHints("classes/state_hint_checked_other_object_error", - new Hint(Kind.NEEDED_STATE, "The state of it is unknown here, and this call needs it to be hasMore")); - } - - @Test - void callOnAnObjectOtherThanTheCheckedOneLeavesItsStateUnknown() { - assertHints("classes/state_hint_checked_wrong_object_error", new Hint(Kind.NEEDED_STATE, - "The state of other is unknown here, and this call needs it to be hasMore")); - } - - @Test - void checkOfAVariableHoldingTheSameObjectChecksTheReceiver() { - assertHints("classes/state_hint_checked_copy_error", new Hint(Kind.NEEDED_STATE, + void failedCheckOfTheReceiverIsNotAnUnknownState() { + List errors = errors("classes/state_hint_checked_error", 3); + assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of it, and this call needs it to be hasMore")); + assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, "What is known here does not decide the state of same, and this call needs it to be hasMore")); + assertHints(errors.get(2), new Hint(Kind.NEEDED_STATE, + "The state of input is unknown here, and this call needs it to be hasMore")); + assertEquals(List.of(Optional.empty(), Optional.empty(), Optional.of(ErrorCategory.UNKNOWN)), + errors.stream().map(LJError::getCategory).toList()); } @Test - void joinOfEveryStateOfTwoSetsKeepsTheUnreachableHint() { - assertHints("ErrorStateHintJoinTwoSets.java", new Hint(Kind.UNREACHABLE_STATE, + void joinsAreNotTakenForAnUnknownState() { + List errors = errors("ErrorStateHintJoins.java", 2); + assertHints(errors.get(0), new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves d from closed and unlocked or closed and locked or opened and unlocked " + "or opened and locked to closed and unlocked. " - + "Create a new object instead with new ErrorStateHintJoinTwoSets()")); - } - - @Test - void joinDifferingInOneOfTwoSetsNamesTheStatesInTheCheckedSets() { - assertHints("ErrorStateHintJoinOneOfTwoSets.java", new Hint(Kind.UNREACHABLE_STATE, + + "Create a new object instead with new ErrorStateHintJoins()")); + assertHints(errors.get(1), new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves d from closed and unlocked or opened and unlocked to closed and unlocked. " - + "Create a new object instead with new ErrorStateHintJoinOneOfTwoSets()"), + + "Create a new object instead with new ErrorStateHintJoins()"), new Hint(Kind.AVAILABLE_CALLS, "In state closed and unlocked or opened and unlocked, d can call: lock()")); + assertEquals(Optional.empty(), errors.get(0).getCategory()); } @Test - void callAllowedInEveryStateNamesTheStatesOfEachRefinement() { - assertHints("ErrorStateHintUnknownToggleTwoSets.java", - new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be a or b. " - + "Objects created with new ErrorStateHintUnknownToggleTwoSets() start in such a state")); - } - - @Test - void stateCheckedByAnEarlierCallIsNotCalledUnknown() { - assertHints("classes/state_hint_checked_state_error", new Hint(Kind.NEEDED_STATE, - "What is known here does not decide the state of it, and this call needs it to be hasMore")); - } - - @Test - void partlyKnownStateIsNamedInTheKnownStateSetsOnly() { - assertHints("ErrorStateHintPartlyKnown.java", - new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable"), - new Hint(Kind.AVAILABLE_CALLS, "In state notRedoable, this can call: check()")); - } - - @Test - void statesDifferingInAnotherStateSetAreNamedOnce() { - assertHints("ErrorPathDependentOtherStateSet.java", - new Hint(Kind.CALL_SEQUENCE, "Call d.open() before this call to move d from closed to opened"), - new Hint(Kind.AVAILABLE_CALLS, "In state closed, d can call: open()")); + void onlyConstructorsThatCanBeCalledAreSuggested() { + List errors = errors("ErrorStateHintConstructors.java", 4); + assertHints(errors.get(0), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready. " + + "Objects created with new ErrorStateHintConstructors() start in such a state")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, "The state of this is unknown here, and this call needs it to be ready")); + assertHints(errors.get(2), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); + assertHints(errors.get(3), + new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); } @Test @@ -293,10 +180,18 @@ void classWithoutStateSetKeepsTheGeneralHint() { } private static void assertHints(String test, Hint... expected) { + assertHints(errors(test, 1).get(0), expected); + } + + private static void assertHints(StateRefinementError error, Hint... expected) { + assertEquals(List.of(expected), error.getHints()); + } + + /** The {@code count} errors {@code test} reports, in the order they are reported */ + private static List errors(String test, int count) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); - assertEquals(1, errors.size(), "Expected exactly one error from " + test); - StateRefinementError error = assertInstanceOf(StateRefinementError.class, errors.get(0)); - assertEquals(List.of(expected), error.getHints()); + assertEquals(count, errors.size(), "Unexpected number of errors from " + test); + return errors.stream().map(e -> assertInstanceOf(StateRefinementError.class, e)).toList(); } }