diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java index 83091c68..7bb8101c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java @@ -71,6 +71,14 @@ static void severalChecks() { GuardCoarse g = GuardCoarse.make(); g.run(); // Expect: State Refinement Error } + + // a call reaches the needed state on every path: the check is not suggested, as it would skip the call where it fails + static void reachableOnEveryPath(boolean shown) { + GuardFrame f = new GuardFrame(); + if (shown) + f.show(); + f.decorate(); // Expect: State Refinement Error + } } @StateSet({"open", "closed"}) @@ -216,3 +224,21 @@ public GuardReader() {} @StateRefinement(from = "eof(this)") public void finish() {} } + +@StateSet({"hidden", "shown"}) +class GuardFrame { + @StateRefinement(to = "hidden(this)") + public GuardFrame() {} + + @StateRefinement(to = "shown(this)") + public void show() {} + + @StateRefinement(to = "hidden(this)") + public void dispose() {} + + @StateRefinement(to = "return ? shown(this) : hidden(this)") + public boolean isShown() { return true; } + + @StateRefinement(from = "hidden(this)") + public void decorate() {} +} 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 7bd300d7..a87b1063 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -20,6 +20,9 @@ import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; import spoon.reflect.reference.CtExecutableReference; @@ -89,12 +92,17 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set if (category == ErrorCategory.UNKNOWN || checkedElsewhere) return hints.anyState(current, call, checkedElsewhere); boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; - List sequences = hints.howToReach(current, call, false, + List sequences = hints.howToReach(current, call, () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); - // in a known state, a check is suggested only when no sequence of calls reaches a state that allows the call + // a check is suggested only when no sequence of calls reaches a state that allows the call: wrapping the call + // in it would skip the call in the states where it fails boolean reachable = sequences.stream().anyMatch(h -> h.kind() == Kind.CALL_SEQUENCE); - List guards = reachable && current.size() == 1 ? List.of() : hints.guard(current, call); - return Stream.of(sequences, guards, hints.allowedCalls(current)).flatMap(List::stream).toList(); + List found = reachable ? sequences + : Stream.concat(sequences.stream(), hints.guard(current, call).stream()).toList(); + // the calls allowed now are listed only when nothing else is suggested + Stream allowed = hints.allowedCalls(current).stream() + .filter(h -> found.isEmpty() || h.kind() != Kind.AVAILABLE_CALLS); + return Stream.concat(found.stream(), allowed).toList(); } /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */ @@ -127,20 +135,17 @@ private List anyState(Set current, RefinedFunction call, boolean ch List hints = new ArrayList<>(); hints.add(new Hint(Kind.NEEDED_STATE, message)); hints.addAll(guard(current, call)); - hints.addAll(howToReach(current, call, true, List::of)); + hints.addAll(howToReach(current, call, List::of)); return hints; } /** * The shortest sequences of calls that are allowed in every state of {@code current} and lead to {@code call} * - * @param fromAnyState - * whether to name {@code current} as any state * @param unreachable * the hints to give if no sequence exists */ - private List howToReach(Set current, RefinedFunction call, boolean fromAnyState, - Supplier> unreachable) { + private List howToReach(Set current, RefinedFunction call, Supplier> unreachable) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) return List.of(); @@ -149,7 +154,7 @@ private List howToReach(Set current, RefinedFunction call, boolean return unreachable.get(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return sequences.stream().map(sequence -> callSequence(current, sequence, fromAnyState)).toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); } /** @@ -172,12 +177,11 @@ private List guard(Set current, RefinedFunction call) { if (guards.size() != 1) return List.of(); CallVariant guard = guards.get(0); - boolean negated = guard.negatedResult(); - String check = (negated ? "!" : "") + guardCall(guard.method()); + String check = (guard.negatedResult() ? "!" : "") + guardCall(guard.method()); String arguments = guard.method().getArguments().isEmpty() ? "" : ", filling in the arguments of " + declaration(guard.method()); - String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s", check, arguments, - !negated, (asValues ? "" : receiver + " is ") + needed()); + String message = String.format("Guard this call with if (%s)%s; inside it, %s", check, arguments, + isIn(needed())); return List.of(new Hint(Kind.GUARD, message)); } @@ -208,16 +212,18 @@ private boolean namesCheckedState(RefinedFunction method) { return refinements.anyMatch(p -> StateMachine.mayName(p, checked)); } - /** The states before and after {@code sequence} are named only in the state sets it changes */ - private Hint callSequence(Set current, List sequence, boolean fromAnyState) { + /** + * The state after {@code sequence} is named only in the state sets it changes. The state before is in the error's + * message. + */ + private Hint callSequence(Set current, List sequence) { Set reached = current; for (CallVariant step : sequence) reached = machine.after(reached, step); Set changed = machine.stateSetsChanged(current, reached); - String from = fromAnyState ? "any state" : join(machine.describeOnly(current, changed)); 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, join(machine.describeOnly(reached, changed)))); + return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call; afterwards %s", calls, + isIn(join(machine.describeOnly(reached, changed))))); } private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { @@ -286,14 +292,37 @@ private static String declaration(RefinedFunction method) { } /** - * A step of a sequence, with the condition on its arguments if it has one, e.g. - * {@code p.setMode(int mode) with mode == 2} + * A step of a sequence, with the condition on its arguments if it has one: as the call with its argument when the + * condition gives the only parameter a value, e.g. {@code p.setMode(2)}, and otherwise after the call, e.g. + * {@code p.set(int lo, int hi) with lo < hi} */ private String call(CallVariant step) { if (step.kind() != CallVariant.Kind.ARGUMENTS) return call(step.method()); - return receiver + "." + declaration(step.method()) + " with " - + step.condition().getExpression().toDisplayString(); + Expression condition = step.condition().getExpression(); + return argumentValue(step.method(), condition) + .map(value -> receiver + "." + Utils.getSimpleName(step.method().getName()) + "(" + value + ")") + .orElse(receiver + "." + declaration(step.method()) + " with " + condition.toDisplayString()); + } + + /** The value {@code condition} gives the only parameter of {@code method}, as {@code 2} in {@code mode == 2} */ + private static Optional argumentValue(RefinedFunction method, Expression condition) { + if (method.getArguments().size() != 1 || !(condition instanceof BinaryExpression equality) + || !equality.getOperator().equals("==")) + return Optional.empty(); + Var parameter = new Var(method.getArguments().get(0).getName()); + if (equality.getFirstOperand().equals(parameter)) + return constant(equality.getSecondOperand()); + if (equality.getSecondOperand().equals(parameter)) + return constant(equality.getFirstOperand()); + return Optional.empty(); + } + + /** {@code e} as shown in hints, if it names no variable */ + private static Optional constant(Expression e) { + List variables = new ArrayList<>(); + e.getVariableNames(variables); + return variables.isEmpty() ? Optional.of(e.toDisplayString()) : Optional.empty(); } /** A method as shown in hints, e.g. {@code open(int)} */ @@ -315,6 +344,11 @@ private static String parameters(RefinedFunction function) { .collect(Collectors.joining(", ", "(", ")")); } + /** That the receiver is in {@code states}, e.g. {@code f is open}, or {@code states} if they name the receiver */ + private String isIn(String states) { + return (asValues ? "" : receiver + " is ") + states; + } + /** {@code states} named as briefly as possible, e.g. {@code open or loud} */ private String names(Collection states) { return join(machine.describe(states)); 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 f22dc673..cd9727b1 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -22,26 +22,21 @@ class TestStateHints { private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; @Test - void missingCallIsSuggestedWithTheCallsAllowedNow() { + void missingCallIsSuggestedWithTheStateItLeadsTo() { assertHints("ErrorStateHintCallSequence.java", - new Hint(Kind.CALL_SEQUENCE, "Call f.open() before this call to move f from created to open"), - new Hint(Kind.AVAILABLE_CALLS, "In state created, f can call: open()")); + new Hint(Kind.CALL_SEQUENCE, "Call f.open() before this call; afterwards f is open")); } @Test void missingCallsAreSuggestedInOrder() { - assertHints("ErrorStateHintTwoCalls.java", - new Hint(Kind.CALL_SEQUENCE, - "Call r.prepare(), then r.start() before this call to move r from idle to running"), - new Hint(Kind.AVAILABLE_CALLS, "In state idle, r can call: prepare()")); + assertHints("ErrorStateHintTwoCalls.java", new Hint(Kind.CALL_SEQUENCE, + "Call r.prepare(), then r.start() before this call; afterwards r is running")); } @Test void callSequenceNamesOnlyTheStateSetsItChanges() { - assertHints("ErrorStateHintMultipleSets.java", new Hint(Kind.CALL_SEQUENCE, - "Call d.unlock() before this call to move d from lockState(d) == locked to lockState(d) == unlocked"), - new Hint(Kind.AVAILABLE_CALLS, - "When doorState(d) == closed and lockState(d) == locked, d can call: unlock()")); + assertHints("ErrorStateHintMultipleSets.java", + new Hint(Kind.CALL_SEQUENCE, "Call d.unlock() before this call; afterwards lockState(d) == unlocked")); } @Test @@ -55,7 +50,7 @@ void finalStateSuggestsCreatingANewObject() { @Test void transitionDependingOnArgumentsIsSuggestedWithItsConditionButPreventsClaimingStateIsFinal() { assertHints("ErrorStateHintIncomplete.java", new Hint(Kind.CALL_SEQUENCE, - "Call f.reopen(int attempts) with attempts > 0 before this call to move f from closed to open")); + "Call f.reopen(int attempts) with attempts > 0 before this call; afterwards f is open")); } @Test @@ -66,40 +61,31 @@ void subclassTransitionsPreventClaimingStateIsUnreachable() { @Test void subclassReceiverCanUseItsOwnTransitionsOnInheritedStates() { assertHints("ErrorStateHintInheritedStates.java", - new Hint(Kind.CALL_SEQUENCE, "Call s.bc() before this call to move s from b to c"), - new Hint(Kind.AVAILABLE_CALLS, "In state b, s can call: bc()")); + new Hint(Kind.CALL_SEQUENCE, "Call s.bc() before this call; afterwards s is c")); } @Test void overrideInTheReceiversClassReplacesTheInheritedTransition() { assertHints("ErrorStateHintOverride.java", - new Hint(Kind.CALL_SEQUENCE, "Call s.next() before this call to move s from a to c"), - new Hint(Kind.AVAILABLE_CALLS, "In state a, s can call: next()")); + new Hint(Kind.CALL_SEQUENCE, "Call s.next() before this call; afterwards s is c")); } @Test void stateSetAndMethodsFromSpecsOfTheReceiversSuperclasses() { - assertHints("classes/state_hints_grandchild_spec_error", - new Hint(Kind.CALL_SEQUENCE, - "Call window.dispose() before this call to move window from displayable to notDisplayable"), - new Hint(Kind.AVAILABLE_CALLS, "In state displayable, window can call: dispose(), pack()")); + assertHints("classes/state_hints_grandchild_spec_error", new Hint(Kind.CALL_SEQUENCE, + "Call window.dispose() before this call; afterwards window is notDisplayable")); } @Test void superclassRefinementOfAMethodTheReceiversClassRedeclaresIsNotSuggested() { - assertHints("classes/state_hints_redeclared_method_error", - new Hint(Kind.CALL_SEQUENCE, - "Call host.dispose() before this call to move host from displayable to notDisplayable"), - new Hint(Kind.AVAILABLE_CALLS, - "In state displayable, host can call: dispose(), pack() (and possibly others)")); + assertHints("classes/state_hints_redeclared_method_error", new Hint(Kind.CALL_SEQUENCE, + "Call host.dispose() before this call; afterwards host is notDisplayable")); } @Test void stateSetAndMethodsFromTheReceiversSuperclassSpec() { - assertHints("classes/state_hints_superclass_spec_error", - new Hint(Kind.CALL_SEQUENCE, - "Call host.dispose() before this call to move host from displayable to notDisplayable"), - new Hint(Kind.AVAILABLE_CALLS, "In state displayable, host can call: dispose(), pack()")); + assertHints("classes/state_hints_superclass_spec_error", new Hint(Kind.CALL_SEQUENCE, + "Call host.dispose() before this call; afterwards host is notDisplayable")); } @Test @@ -110,8 +96,7 @@ void ownGenericRefinementOfAnInheritedMethodIsNotSuggested() { @Test void statesOfAnotherClassWithTheSimpleNameOfASupertypeAreLeftOut() { assertHints("classes/state_hints_same_simple_name_error", - new Hint(Kind.CALL_SEQUENCE, "Call l.add(E) before this call to move l from empty to nonEmpty"), - new Hint(Kind.AVAILABLE_CALLS, "In state empty, l can call: add(E)")); + new Hint(Kind.CALL_SEQUENCE, "Call l.add(E) before this call; afterwards l is nonEmpty")); } @Test @@ -152,15 +137,14 @@ void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { new Hint(Kind.NEEDED_STATE, "The state of undoManager is unknown here, and this call needs it to be redoable"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable")); + "Guard this call with if (undoManager.canRedo()); inside it, undoManager is redoable")); } @Test void unknownStateSuggestsCallsAllowedInAnyState() { assertHints("ErrorStateHintUnknownAnyState.java", 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")); + new Hint(Kind.CALL_SEQUENCE, "Call f.reset(), then f.open() before this call; afterwards f is open")); } @Test @@ -172,8 +156,7 @@ void statesAreNamedOnlyInTheStateSetsThatMatter() { 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()")); + new Hint(Kind.UNREACHABLE_STATE, "No sequence of calls moves this from notRedoable to redoable")); } @Test @@ -183,16 +166,14 @@ void failedCheckOfTheReceiverIsNotAnUnknownState() { 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"), - new Hint(Kind.GUARD, "Guard this call with if (it.hasNext()): when it returns true, it is hasMore")); + new Hint(Kind.GUARD, "Guard this call with if (it.hasNext()); inside it, it is 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"), - new Hint(Kind.GUARD, - "Guard this call with if (same.hasNext()): when it returns true, same is hasMore")); + new Hint(Kind.GUARD, "Guard this call with if (same.hasNext()); inside it, same is 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"), - new Hint(Kind.GUARD, - "Guard this call with if (input.hasNext()): when it returns true, input is hasMore")); + new Hint(Kind.GUARD, "Guard this call with if (input.hasNext()); inside it, input is hasMore")); assertEquals(List.of(Optional.empty(), Optional.empty(), Optional.of(ErrorCategory.UNKNOWN)), errors.stream().map(LJError::getCategory).toList()); } @@ -206,9 +187,7 @@ void joinsAreNotTakenForAnUnknownState() { + "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 ErrorStateHintJoins()"), - new Hint(Kind.AVAILABLE_CALLS, - "In state (closed and unlocked) or (opened and unlocked), d can call: lock()")); + + "Create a new object instead with new ErrorStateHintJoins()")); assertEquals(Optional.empty(), errors.get(0).getCategory()); } @@ -232,12 +211,8 @@ void onlyPublicInheritedMethodsAreSuggested() { // the files are verified in no fixed order assertEquals(Set.of( List.of(new Hint(Kind.CALL_SEQUENCE, - "Call hatch.openPublicly() before this call to move hatch from closed to open"), - new Hint(Kind.AVAILABLE_CALLS, - "In state closed, hatch can call: openPublicly() (and possibly others)")), - List.of(new Hint(Kind.CALL_SEQUENCE, - "Call door.push() before this call to move door from shut to ajar"), - new Hint(Kind.AVAILABLE_CALLS, "In state shut, door can call: push() (and possibly others)"))), + "Call hatch.openPublicly() before this call; afterwards hatch is open")), + List.of(new Hint(Kind.CALL_SEQUENCE, "Call door.push() before this call; afterwards door is ajar"))), errors.stream().map(StateRefinementError::getHints).collect(Collectors.toSet())); } @@ -255,23 +230,20 @@ void deciderIsTheLastCallThatChangedTheCheckedStateSet() { @Test void checksAreSuggestedOnlyWhenTheRefinementsProveThem() { - List errors = errors("ErrorStateHintGuards.java", 11); + List errors = errors("ErrorStateHintGuards.java", 12); assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, "The state of c is unknown here, and this call needs it to be open. " + "Objects created with new GuardChannel() start in such a state"), - new Hint(Kind.GUARD, "Guard this call with if (!c.isClosed()): when it returns false, c is open")); - assertHints(errors.get(1), - new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(...)), " - + "filling in the arguments of tryLock(long timeout): when it returns true, l is locked"), - new Hint(Kind.AVAILABLE_CALLS, "In state unlocked, l can call: tryLock(long) (and possibly others)")); + new Hint(Kind.GUARD, "Guard this call with if (!c.isClosed()); inside it, c is open")); + assertHints(errors.get(1), new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(...)), " + + "filling in the arguments of tryLock(long timeout); inside it, l is locked")); assertHints(errors.get(2), new Hint(Kind.NEEDED_STATE, "The state of p is unknown here, and this call needs it to be ready")); assertHints(errors.get(3), new Hint(Kind.NEEDED_STATE, "The state of w is unknown here, and this call needs it to be accept")); assertHints(errors.get(4), - new Hint(Kind.GUARD, "Guard this call with if (w.canWrite()): when it returns true, w is accept"), - new Hint(Kind.AVAILABLE_CALLS, "In state start, w can call: canWrite() (and possibly others)")); + new Hint(Kind.GUARD, "Guard this call with if (w.canWrite()); inside it, w is accept")); assertHints(errors.get(5), new Hint(Kind.NEEDED_STATE, "The state of b is unknown here, and this call needs it to be undoable and redoable")); assertHints(errors.get(6), @@ -285,21 +257,19 @@ void checksAreSuggestedOnlyWhenTheRefinementsProveThem() { new Hint(Kind.AVAILABLE_CALLS, "In state live, r can call: read() (and possibly others)")); assertHints(errors.get(10), new Hint(Kind.NEEDED_STATE, "The state of g is unknown here, and this call needs it to be running")); + assertHints(errors.get(11), + new Hint(Kind.CALL_SEQUENCE, "Call f.dispose() before this call; afterwards f is hidden")); } @Test void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() { List errors = errors("ErrorStateHintArgumentConditions.java", 7); - assertHints(errors.get(0), - new Hint(Kind.CALL_SEQUENCE, - "Call r.set(int lo, int hi) with lo < hi before this call to move r from low to high"), - new Hint(Kind.AVAILABLE_CALLS, "In state low, r can call: set(int, int) (and possibly others)")); + assertHints(errors.get(0), new Hint(Kind.CALL_SEQUENCE, + "Call r.set(int lo, int hi) with lo < hi before this call; afterwards r is high")); assertHints(errors.get(1), new Hint(Kind.CALL_SEQUENCE, - "Call chain.pick(int k) with k == 1, then chain.next() before this call to move chain from a to c"), - new Hint(Kind.AVAILABLE_CALLS, "In state a, chain can call: pick(int) (and possibly others)")); + "Call chain.pick(1), then chain.next() before this call; afterwards chain is c")); assertHints(errors.get(2), new Hint(Kind.CALL_SEQUENCE, - "Call l.setLimit(int limit) with limit <= 0 before this call to move l from bounded to unbounded"), - new Hint(Kind.AVAILABLE_CALLS, "In state bounded, l can call: setLimit(int) (and possibly others)")); + "Call l.setLimit(int limit) with limit <= 0 before this call; afterwards l is unbounded")); // no condition, and no value of the earlier call's argument, is claimed to allow the call for (StateRefinementError error : errors.subList(3, 5)) assertHints(error, @@ -313,9 +283,7 @@ void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() { @Test void callWhoseStateDependsOnItsArgumentIsSuggestedWithTheCondition() { assertHints("classes/state_hint_compression_mode_error", new Hint(Kind.CALL_SEQUENCE, - "Call wParam.setCompressionMode(int mode) with mode == 2 before this call to move wParam from startCompression to compressionExplicit"), - new Hint(Kind.AVAILABLE_CALLS, - "In state startCompression, wParam can call: setCompressionMode(int) (and possibly others)")); + "Call wParam.setCompressionMode(2) before this call; afterwards wParam is compressionExplicit")); } @Test @@ -325,12 +293,12 @@ void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() { new Hint(Kind.NEEDED_STATE, "The state of undoManager is unknown here, and this call needs it to be redoable"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable")); + "Guard this call with if (undoManager.canRedo()); inside it, undoManager is redoable")); assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, "The state of undoManager is unknown here, and this call needs it to be undoable"), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable")); + "Guard this call with if (undoManager.canUndo()); inside it, undoManager is undoable")); } @Test @@ -356,16 +324,14 @@ void setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand() { StateRefinementError error = errors("ErrorStateSetNameInSuperclass.java", 1).get(0); assertEquals("found ready(c) && idle(c) but expected ready(c) && busy(c)", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); - assertHints(error, new Hint(Kind.CALL_SEQUENCE, "Call c.start() before this call to move c from idle to busy"), - new Hint(Kind.AVAILABLE_CALLS, "In state idle and ready, c can call: start()")); + assertHints(error, new Hint(Kind.CALL_SEQUENCE, "Call c.start() before this call; afterwards c is busy")); } @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs lock(d) == unlocked"), - new Hint(Kind.GUARD, - "Guard this call with if (d.isUnlocked()): when it returns true, lock(d) == unlocked")); + new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()); inside it, lock(d) == unlocked")); } @Test