From 6dd421a2388857f31b145b36296ab2bf163d4704 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 01:17:17 +0000 Subject: [PATCH 1/4] Show states of named sets by their set in state hints and declared-here The headline of a state error shows a state of a named set as a value of its set, e.g. lockState(d) == locked. The hints now name such states the same way (lockState == locked), and group alternatives in parentheses so "and" and "or" cannot be misread. The declared-here excerpt stays as written, with a "where" line under it saying what each shorthand state in it means. Display only: the VC, verdict, hints chosen and category do not change. States of unnamed sets, and names shared by sets with different names, keep the shorthand, as in the headline. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/diagnostics/LJDiagnostic.java | 26 +++++++++++++++++- .../errors/StateRefinementError.java | 27 +++++++++++++++++++ .../diagnostics/hints/StateHints.java | 21 ++++++++++----- .../object_checkers/AuxStateHandler.java | 16 ++++++++--- .../liquidjava/rj_language/StateValues.java | 24 ++++++++++++----- .../liquidjava/api/tests/TestStateHints.java | 23 ++++++++++------ 6 files changed, 111 insertions(+), 26 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 6eafd068..a49828dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -75,6 +75,16 @@ public List getMessageNotes() { return List.of(); } + /** + * Lines printed under the excerpt of where the refinement is declared that explain it + * + * @param declaration + * the declaration's text on the first line of the excerpt + */ + public List getDeclarationNotes(String declaration) { + return List.of(); + } + public void setPosition(SourcePosition pos) { if (pos == null || pos.getFile() == null) return; @@ -145,8 +155,11 @@ public String toString() { if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) { sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET); String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true); - if (declarationSnippet != null) + if (declarationSnippet != null) { sb.append(declarationSnippet); + for (String note : getDeclarationNotes(getDeclarationText(declPos))) + sb.append(" ").append(note).append("\n"); + } sb.append("\n").append(declPos.getFile().getPath()).append(":").append(declPos.getLine()) .append(Colors.RESET).append("\n"); @@ -159,6 +172,17 @@ public String getSnippet() { return getSnippet(position, 2, 2, accentColor, customMessage, false); } + /** The text {@code position} spans on its first line, or an empty string if it cannot be read */ + private static String getDeclarationText(SourcePosition position) { + try { + String line = Files.readAllLines(position.getFile().toPath()).get(position.getLine() - 1); + int end = position.getEndLine() == position.getLine() ? position.getEndColumn() : line.length(); + return line.substring(Math.max(0, position.getColumn() - 1), Math.min(line.length(), end)); + } catch (Exception e) { + return ""; + } + } + private String getSnippet(SourcePosition snippetPosition, int contextBefore, int contextAfter, String markerColor, String markerMessage, boolean firstLineOnly) { if (snippetPosition == null || snippetPosition.getFile() == null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index d1c58ed6..48d6a752 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,8 +2,11 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import java.util.ArrayList; import java.util.List; import java.util.function.UnaryOperator; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; @@ -12,6 +15,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.VCSimplificationResult; import spoon.reflect.cu.SourcePosition; @@ -22,10 +26,14 @@ */ public class StateRefinementError extends LJError { + /** A call with one argument that is a name, e.g. {@code closed(this)} */ + private static final Pattern ON_A_NAME = Pattern.compile("([A-Za-z_$][\\w$.]*)\\(\\s*([A-Za-z_$][\\w$]*)\\s*\\)"); + private final Predicate expected; private final VCSimplificationResult found; private final SourcePosition declarationPosition; private final StateErrorContext context; + private final UnaryOperator display; /** * @param display @@ -42,6 +50,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP this.expected = new Predicate(display.apply(expected.getExpression())); this.found = found.map(display); this.context = context; + this.display = display; hints.forEach(this::addHint); setCategory(category); if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression())) @@ -56,6 +65,24 @@ private static boolean appliesGhost(Expression expression) { || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost); } + /** + * What each state the declaration writes as a shorthand means as the message shows it, e.g. + * {@code closed(this) means doorState(this) == closed}: the declaration is shown as written + */ + @Override + public List getDeclarationNotes(String declaration) { + List meanings = new ArrayList<>(); + Matcher call = ON_A_NAME.matcher(declaration); + while (call.find()) { + Expression state = new FunctionInvocation(call.group(1), List.of(new Var(call.group(2)))); + Expression shown = display.apply(state); + String meaning = state.toDisplayString() + " means " + shown.toDisplayString(); + if (!shown.equals(state) && !meanings.contains(meaning)) + meanings.add(meaning); + } + return meanings.isEmpty() ? List.of() : List.of("where " + String.join(", ", meanings)); + } + @Override public SourcePosition getDeclarationPosition() { return declarationPosition; 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 62629559..98aa130a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -7,6 +7,7 @@ import java.util.Set; import java.util.TreeSet; import java.util.function.Supplier; +import java.util.function.UnaryOperator; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -41,10 +42,12 @@ public final class StateHints { private final List> goals; /** The state sets the failing call checks, as indexes into {@link State#names()} */ private final Set checkedSets; + private final UnaryOperator stateName; - private StateHints(StateMachine machine, String receiver, RefinedFunction call) { + private StateHints(StateMachine machine, String receiver, RefinedFunction call, UnaryOperator stateName) { this.machine = machine; this.receiver = receiver; + this.stateName = stateName; this.goals = machine.statesAllowingByRefinement(call); this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) .collect(Collectors.toCollection(TreeSet::new)); @@ -62,12 +65,14 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call) * @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 + * @param stateName + * a state's name as the error shows it, e.g. {@code lockState == locked} for {@code locked} */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category, boolean checkedElsewhere) { + ErrorCategory category, boolean checkedElsewhere, UnaryOperator stateName) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed - StateHints hints = new StateHints(machine, receiver, call); + StateHints hints = new StateHints(machine, receiver, call, stateName); if (hints.goals.isEmpty()) return List.of(); @@ -311,11 +316,15 @@ 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 ")); + return join(goals.stream().flatMap(g -> machine.describe(g).stream()).distinct().toList()); } - private static String join(List> groups) { - return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or ")); + /** The groups joined by {@code or}, each in parentheses if it has several states and there are other groups */ + private String join(List> groups) { + return groups.stream().map(group -> { + String states = group.stream().map(stateName).collect(Collectors.joining(" and ")); + return groups.size() > 1 && group.size() > 1 ? "(" + states + ")" : states; + }).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 c2d00a08..42f22da7 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 @@ -2,6 +2,7 @@ import java.lang.annotation.Annotation; import java.util.*; +import java.util.function.UnaryOperator; import java.util.stream.Collectors; import liquidjava.diagnostics.DebugLog; @@ -23,6 +24,7 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -805,7 +807,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() - : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); + : states.map(r -> stateHints(tc, r, function, category, checked, invocation)).orElse(List.of()); StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); @@ -883,13 +885,19 @@ 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. Best effort, like * {@link #receiverStates}: the machine asks the solver about some calls only when a hint needs them */ - private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, - boolean checked, CtElement invocation) { + private static List stateHints(TypeChecker tc, ReceiverStates states, RefinedFunction function, + ErrorCategory category, boolean checked, CtElement invocation) { Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); + // states are named as the message names them: by their set, unless it shows the shorthand + Context context = tc.getContext(); + UnaryOperator stateName = state -> StateValues + .setNameOf(state, context.getGhostStates(), context.getGhosts()).map(set -> set + " == " + state) + .orElse(state); try { - return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked, + stateName); } catch (RuntimeException e) { DebugLog.warn("Could not compute the state hints: " + e.getMessage()); return List.of(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index 369ac126..82d8ac87 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -123,17 +123,27 @@ private static Expression rewriteToSetForm(Expression e, List states /** {@code set(e) op state} when {@code e} is the state {@code state(e)} of a set with one, given name */ private static Optional setValue(Expression e, String op, List states, List ghosts) { - if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1) - || ghosts.stream().anyMatch(g -> g.matches(invocation.getName())) - || states.stream().anyMatch(s -> s.getParent() == null && s.matches(invocation.getName()))) + if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1)) return Optional.empty(); - List setNames = states.stream().filter(s -> s.getParent() != null && s.matches(invocation.getName())) + return setNameOf(invocation.getName(), states, ghosts).map(setName -> new BinaryExpression( + new FunctionInvocation(qualifiedLike(invocation.getName(), setName), + List.of(invocation.getArgs().get(0).clone())), + op, new Var(Utils.getSimpleName(invocation.getName())))); + } + + /** + * The name of the state set that {@link #toSetForm} shows the state {@code state} as a value of, or empty when it + * keeps the shorthand + */ + public static Optional setNameOf(String state, List states, List ghosts) { + if (ghosts.stream().anyMatch(g -> g.matches(state)) + || states.stream().anyMatch(s -> s.getParent() == null && s.matches(state))) + return Optional.empty(); + List setNames = states.stream().filter(s -> s.getParent() != null && s.matches(state)) .map(s -> s.getParent().getName()).distinct().toList(); if (setNames.size() != 1 || setNames.get(0).matches(Formats.STATE_SET_NAMES)) return Optional.empty(); - FunctionInvocation set = new FunctionInvocation(qualifiedLike(invocation.getName(), setNames.get(0)), - List.of(invocation.getArgs().get(0).clone())); - return Optional.of(new BinaryExpression(set, op, new Var(Utils.getSimpleName(invocation.getName())))); + return Optional.of(setNames.get(0)); } /** The states of {@code set}, or only those named {@code name} when it is not null */ 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 9b6a9c2a..ff8684f3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -39,8 +39,10 @@ void missingCallsAreSuggestedInOrder() { @Test void callSequenceNamesOnlyTheStateSetsItChanges() { assertHints("ErrorStateHintMultipleSets.java", - new Hint(Kind.CALL_SEQUENCE, "Call d.unlock() before this call to move d from locked to unlocked"), - new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()")); + new Hint(Kind.CALL_SEQUENCE, + "Call d.unlock() before this call to move d from lockState == locked to lockState == unlocked"), + new Hint(Kind.AVAILABLE_CALLS, + "In state doorState == closed and lockState == locked, d can call: unlock()")); } @Test @@ -200,14 +202,14 @@ void failedCheckOfTheReceiverIsNotAnUnknownState() { 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. " + "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 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. " + "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()")); + "In state (closed and unlocked) or (opened and unlocked), d can call: lock()")); assertEquals(Optional.empty(), errors.get(0).getCategory()); } @@ -345,13 +347,18 @@ void foundKeepsANamedStateSetByItsName() { assertEquals( "found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + // the declaration is shown as written, with what its states mean under it + assertTrue(error.toString().contains(" where closed(this) means doorState(this) == closed, " + + "unlocked(this) means lockState(this) == unlocked\n")); } @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", - new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs it to be unlocked"), - new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked")); + new Hint(Kind.NEEDED_STATE, + "The state of d is unknown here, and this call needs it to be lock == unlocked"), + new Hint(Kind.GUARD, + "Guard this call with if (d.isUnlocked()): when it returns true, d is lock == unlocked")); } @Test From 9a1d86c3ee53e468f13926b9e0656d686083e1cc Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 01:24:50 +0000 Subject: [PATCH 2/4] Keep the shorthand for a set name that sets of different classes share When a class and its superclass each have a set with the same name, their states would read as values of one set (phase == ready and phase == busy), in the headline and in the hints. They keep the shorthand instead. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateSetNameInSuperclass.java | 29 +++++++++++++++++++ .../errors/StateRefinementError.java | 5 ++-- .../liquidjava/rj_language/StateValues.java | 8 +++-- .../liquidjava/api/tests/TestStateHints.java | 9 ++++++ 4 files changed, 47 insertions(+), 4 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java new file mode 100644 index 00000000..1208429e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The class and its superclass each have a set named phase: their states keep the shorthand, since phase == ready +// and phase == busy would read as two values of one set +@StateSet(name = "phase", value = {"ready", "done"}) +class ErrorStateSetNameInSuperclassBase { + @StateRefinement(to = "ready(this)") + ErrorStateSetNameInSuperclassBase() {} +} + +@StateSet(name = "phase", value = {"busy", "idle"}) +public class ErrorStateSetNameInSuperclass extends ErrorStateSetNameInSuperclassBase { + @StateRefinement(to = "ready(this) && idle(this)") + ErrorStateSetNameInSuperclass() {} + + @StateRefinement(from = "idle(this)", to = "busy(this)") + void start() {} + + @StateRefinement(from = "ready(this) && busy(this)") + void use() {} + + public static void main(String[] args) { + ErrorStateSetNameInSuperclass c = new ErrorStateSetNameInSuperclass(); + c.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 48d6a752..c2f566c8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -27,7 +27,8 @@ public class StateRefinementError extends LJError { /** A call with one argument that is a name, e.g. {@code closed(this)} */ - private static final Pattern ON_A_NAME = Pattern.compile("([A-Za-z_$][\\w$.]*)\\(\\s*([A-Za-z_$][\\w$]*)\\s*\\)"); + private static final Pattern CALL_ON_A_NAME = Pattern + .compile("([A-Za-z_$][\\w$.]*)\\(\\s*([A-Za-z_$][\\w$]*)\\s*\\)"); private final Predicate expected; private final VCSimplificationResult found; @@ -72,7 +73,7 @@ private static boolean appliesGhost(Expression expression) { @Override public List getDeclarationNotes(String declaration) { List meanings = new ArrayList<>(); - Matcher call = ON_A_NAME.matcher(declaration); + Matcher call = CALL_ON_A_NAME.matcher(declaration); while (call.find()) { Expression state = new FunctionInvocation(call.group(1), List.of(new Var(call.group(2)))); Expression shown = display.apply(state); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index 82d8ac87..77862087 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -133,7 +133,8 @@ private static Optional setValue(Expression e, String op, List /** * The name of the state set that {@link #toSetForm} shows the state {@code state} as a value of, or empty when it - * keeps the shorthand + * keeps the shorthand. It also keeps it when sets of different classes have that set name, e.g. a class and its + * superclass: their values would read as values of one set */ public static Optional setNameOf(String state, List states, List ghosts) { if (ghosts.stream().anyMatch(g -> g.matches(state)) @@ -143,7 +144,10 @@ public static Optional setNameOf(String state, List states, .map(s -> s.getParent().getName()).distinct().toList(); if (setNames.size() != 1 || setNames.get(0).matches(Formats.STATE_SET_NAMES)) return Optional.empty(); - return Optional.of(setNames.get(0)); + long setsWithName = states.stream().map(GhostState::getParent) + .filter(p -> p != null && p.getName().equals(setNames.get(0))).map(GhostFunction::getQualifiedName) + .distinct().count(); + return setsWithName == 1 ? Optional.of(setNames.get(0)) : Optional.empty(); } /** The states of {@code set}, or only those named {@code name} when it is not null */ 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 ff8684f3..dd5b6b4c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -352,6 +352,15 @@ void foundKeepsANamedStateSetByItsName() { + "unlocked(this) means lockState(this) == unlocked\n")); } + @Test + 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()")); + } + @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", From e2ce936fc27c88a7810d4ec9456572dc89d7dfc7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 01:46:42 +0000 Subject: [PATCH 3/4] Show states in hints in the headline's form, with the receiver As the PM decided: a hint names a state of a named set as the message does, lockState(d) == locked, and the sentences that said "d is" or "needs it to be" a state now state the condition, e.g. "needs undoState(um) == undoable". Classes without named sets keep the shorthand wording. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/hints/StateHints.java | 60 ++++++++++++++----- .../object_checkers/AuxStateHandler.java | 7 +-- .../liquidjava/api/tests/TestStateHints.java | 12 ++-- 3 files changed, 50 insertions(+), 29 deletions(-) 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 98aa130a..7bd300d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -7,7 +7,7 @@ import java.util.Set; import java.util.TreeSet; import java.util.function.Supplier; -import java.util.function.UnaryOperator; +import java.util.function.Function; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -42,12 +42,21 @@ public final class StateHints { private final List> goals; /** The state sets the failing call checks, as indexes into {@link State#names()} */ private final Set checkedSets; - private final UnaryOperator stateName; + /** The name of the state set a state is shown as a value of, or empty when it keeps the shorthand */ + private final Function> setNameOf; + /** + * Whether states are shown as the error's message shows them, e.g. {@code lockState(d) == locked}: when some state + * set of the class is shown by its name + */ + private final boolean asValues; - private StateHints(StateMachine machine, String receiver, RefinedFunction call, UnaryOperator stateName) { + private StateHints(StateMachine machine, String receiver, RefinedFunction call, + Function> setNameOf) { this.machine = machine; this.receiver = receiver; - this.stateName = stateName; + this.setNameOf = setNameOf; + this.asValues = machine.states().stream().flatMap(s -> s.names().stream()) + .anyMatch(name -> setNameOf.apply(name).isPresent()); this.goals = machine.statesAllowingByRefinement(call); this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) .collect(Collectors.toCollection(TreeSet::new)); @@ -65,14 +74,15 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call, * @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 - * @param stateName - * a state's name as the error shows it, e.g. {@code lockState == locked} for {@code locked} + * @param setNameOf + * the name of the state set the error's message shows a state as a value of, or empty when it shows the + * shorthand */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category, boolean checkedElsewhere, UnaryOperator stateName) { + ErrorCategory category, boolean checkedElsewhere, Function> setNameOf) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed - StateHints hints = new StateHints(machine, receiver, call, stateName); + StateHints hints = new StateHints(machine, receiver, call, setNameOf); if (hints.goals.isEmpty()) return List.of(); @@ -112,7 +122,7 @@ public static Hint decidingArgument(DecidingArgument deciding, String 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(); + String message = known + ", and this call needs " + (asValues ? "" : "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)); @@ -166,8 +176,8 @@ private List guard(Set current, RefinedFunction call) { String check = (negated ? "!" : "") + 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 is %s", check, arguments, - !negated, receiver, needed()); + String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s", check, arguments, + !negated, (asValues ? "" : receiver + " is ") + needed()); return List.of(new Hint(Kind.GUARD, message)); } @@ -211,6 +221,11 @@ private Hint callSequence(Set current, List sequence, boolea } private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { + if (pathDependent && asValues) + return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( + "Depending on the path taken, %s here, and no sequence of calls moves %s from all of them to %s. " + + "Make %s reach this line in the same state on every path", + namesHere(current), receiver, needed(), receiver)); 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. " @@ -227,13 +242,15 @@ private List allowedCalls(Set current) { if (!allowed.isEmpty()) { 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", - namesHere(current), receiver, list(signatures), others))); + return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("%s %s, %s can call: %s%s", + asValues ? "When" : "In state", 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", + return List.of(new Hint(Kind.FINAL_STATE, asValues + ? String.format("When %s, none of the methods of %s with state refinements can be called", + namesHere(current), receiver) + : String.format("%s is in state %s, where none of its methods with state refinements can be called", receiver, namesHere(current)))); return List.of(); } @@ -322,11 +339,22 @@ private String needed() { /** The groups joined by {@code or}, each in parentheses if it has several states and there are other groups */ private String join(List> groups) { return groups.stream().map(group -> { - String states = group.stream().map(stateName).collect(Collectors.joining(" and ")); + String states = group.stream().map(this::stateName).collect(Collectors.joining(" and ")); return groups.size() > 1 && group.size() > 1 ? "(" + states + ")" : states; }).collect(Collectors.joining(" or ")); } + /** + * A state as the error's message shows it, e.g. {@code lockState(d) == locked}, or {@code closed(d)} for a state + * that keeps the shorthand, or only its name if no state set of the class is shown by its name + */ + private String stateName(String state) { + if (!asValues) + return state; + return setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state) + .orElse(state + "(" + receiver + ")"); + } + 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/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 42f22da7..3dc2148e 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 @@ -2,7 +2,6 @@ import java.lang.annotation.Annotation; import java.util.*; -import java.util.function.UnaryOperator; import java.util.stream.Collectors; import liquidjava.diagnostics.DebugLog; @@ -890,14 +889,10 @@ private static List stateHints(TypeChecker tc, ReceiverStates states, Refi Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); - // states are named as the message names them: by their set, unless it shows the shorthand Context context = tc.getContext(); - UnaryOperator stateName = state -> StateValues - .setNameOf(state, context.getGhostStates(), context.getGhosts()).map(set -> set + " == " + state) - .orElse(state); try { return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked, - stateName); + state -> StateValues.setNameOf(state, context.getGhostStates(), context.getGhosts())); } catch (RuntimeException e) { DebugLog.warn("Could not compute the state hints: " + e.getMessage()); return List.of(); 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 dd5b6b4c..f22dc673 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -38,11 +38,10 @@ void missingCallsAreSuggestedInOrder() { @Test void callSequenceNamesOnlyTheStateSetsItChanges() { - assertHints("ErrorStateHintMultipleSets.java", - new Hint(Kind.CALL_SEQUENCE, - "Call d.unlock() before this call to move d from lockState == locked to lockState == unlocked"), + 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, - "In state doorState == closed and lockState == locked, d can call: unlock()")); + "When doorState(d) == closed and lockState(d) == locked, d can call: unlock()")); } @Test @@ -364,10 +363,9 @@ void setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand() { @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", - new Hint(Kind.NEEDED_STATE, - "The state of d is unknown here, and this call needs it to be lock == unlocked"), + 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, d is lock == unlocked")); + "Guard this call with if (d.isUnlocked()): when it returns true, lock(d) == unlocked")); } @Test From 361d4636c10fd03d9453e385cb845ea6c11e8e12 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 02:05:23 +0000 Subject: [PATCH 4/4] Find the states the declaration explains in its AST, not its text The note under "declared here" was found by matching calls in the source line. It now walks the declaration's from as parsed, before states written as values of their sets are read as the shorthand, so only a state of a named set written as the shorthand is explained. The notes are computed where the error is built and passed to it. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/diagnostics/LJDiagnostic.java | 22 ++--------- .../errors/StateRefinementError.java | 34 ++++------------- .../processor/context/ObjectState.java | 11 ++++++ .../refinement_checker/TypeChecker.java | 7 ++-- .../refinement_checker/VCChecker.java | 5 ++- .../object_checkers/AuxStateHandler.java | 38 +++++++++++++++++-- .../RefinementErrorCounterexampleTest.java | 2 +- 7 files changed, 64 insertions(+), 55 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index a49828dc..6224bb67 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -75,13 +75,8 @@ public List getMessageNotes() { return List.of(); } - /** - * Lines printed under the excerpt of where the refinement is declared that explain it - * - * @param declaration - * the declaration's text on the first line of the excerpt - */ - public List getDeclarationNotes(String declaration) { + /** Lines printed under the excerpt of where the refinement is declared that explain it */ + public List getDeclarationNotes() { return List.of(); } @@ -157,7 +152,7 @@ public String toString() { String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true); if (declarationSnippet != null) { sb.append(declarationSnippet); - for (String note : getDeclarationNotes(getDeclarationText(declPos))) + for (String note : getDeclarationNotes()) sb.append(" ").append(note).append("\n"); } @@ -172,17 +167,6 @@ public String getSnippet() { return getSnippet(position, 2, 2, accentColor, customMessage, false); } - /** The text {@code position} spans on its first line, or an empty string if it cannot be read */ - private static String getDeclarationText(SourcePosition position) { - try { - String line = Files.readAllLines(position.getFile().toPath()).get(position.getLine() - 1); - int end = position.getEndLine() == position.getLine() ? position.getEndColumn() : line.length(); - return line.substring(Math.max(0, position.getColumn() - 1), Math.min(line.length(), end)); - } catch (Exception e) { - return ""; - } - } - private String getSnippet(SourcePosition snippetPosition, int contextBefore, int contextAfter, String markerColor, String markerMessage, boolean firstLineOnly) { if (snippetPosition == null || snippetPosition.getFile() == null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index c2f566c8..139ebba9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,11 +2,8 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; -import java.util.ArrayList; import java.util.List; import java.util.function.UnaryOperator; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; @@ -15,7 +12,6 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; -import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.VCSimplificationResult; import spoon.reflect.cu.SourcePosition; @@ -26,24 +22,23 @@ */ public class StateRefinementError extends LJError { - /** A call with one argument that is a name, e.g. {@code closed(this)} */ - private static final Pattern CALL_ON_A_NAME = Pattern - .compile("([A-Za-z_$][\\w$.]*)\\(\\s*([A-Za-z_$][\\w$]*)\\s*\\)"); - private final Predicate expected; private final VCSimplificationResult found; private final SourcePosition declarationPosition; private final StateErrorContext context; - private final UnaryOperator display; + private final List declarationNotes; /** * @param display * rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are * chosen on them as given + * @param declarationNotes + * lines that explain the declaration, printed under its excerpt */ public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, - ErrorCategory category, StateErrorContext context, UnaryOperator display) { + ErrorCategory category, StateErrorContext context, UnaryOperator display, + List declarationNotes) { super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable, customMessage); @@ -51,7 +46,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP this.expected = new Predicate(display.apply(expected.getExpression())); this.found = found.map(display); this.context = context; - this.display = display; + this.declarationNotes = declarationNotes; hints.forEach(this::addHint); setCategory(category); if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression())) @@ -66,22 +61,9 @@ private static boolean appliesGhost(Expression expression) { || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost); } - /** - * What each state the declaration writes as a shorthand means as the message shows it, e.g. - * {@code closed(this) means doorState(this) == closed}: the declaration is shown as written - */ @Override - public List getDeclarationNotes(String declaration) { - List meanings = new ArrayList<>(); - Matcher call = CALL_ON_A_NAME.matcher(declaration); - while (call.find()) { - Expression state = new FunctionInvocation(call.group(1), List.of(new Var(call.group(2)))); - Expression shown = display.apply(state); - String meaning = state.toDisplayString() + " means " + shown.toDisplayString(); - if (!shown.equals(state) && !meanings.contains(meaning)) - meanings.add(meaning); - } - return meanings.isEmpty() ? List.of() : List.of("where " + String.join(", ", meanings)); + public List getDeclarationNotes() { + return declarationNotes; } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java index 3d03fd95..8d44fba1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java @@ -7,6 +7,8 @@ public class ObjectState { Predicate from; Predicate to; + /** {@code from} as written, before states written as values of their sets are read as the shorthand */ + Predicate writtenFrom; SourcePosition fromPosition; SourcePosition toPosition; String message; @@ -33,6 +35,14 @@ public void setTo(Predicate to) { this.to = to; } + public Predicate getWrittenFrom() { + return writtenFrom; + } + + public void setWrittenFrom(Predicate writtenFrom) { + this.writtenFrom = writtenFrom; + } + public SourcePosition getFromPosition() { return fromPosition; } @@ -77,6 +87,7 @@ public ObjectState clone() { Predicate clonedFrom = from == null ? null : from.clone(); Predicate clonedTo = to == null ? null : to.clone(); ObjectState clone = new ObjectState(clonedFrom, clonedTo, message); + clone.setWrittenFrom(writtenFrom); clone.setFromPosition(fromPosition); clone.setToPosition(toPosition); return clone; 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 4bcaf9ff..f01e4f6e 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 @@ -588,14 +588,15 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage) throws LJError { - throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null); + throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null, + List.of()); } public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context) throws LJError { + StateErrorContext context, List declarationNotes) throws LJError { vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints, - category, context); + category, context, declarationNotes); } public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError { 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 86749010..84d285e4 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 @@ -457,7 +457,7 @@ protected Predicate shownFound(Predicate found, Predicate expected) { protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context) throws StateRefinementError { + StateErrorContext context, List declarationNotes) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected)); @@ -465,7 +465,8 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, category, context, - e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts())); + e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), + declarationNotes); } /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */ 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 3dc2148e..6c1d7167 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 @@ -24,6 +24,8 @@ import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -412,7 +414,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota // has from if (from != null) { - state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false)); + Predicate written = new Predicate(from, e, prefix); + state.setWrittenFrom(written); + state.setFrom(createStatePredicate(written, from, f.getTargetClass(), tc, e, false)); state.setFromPosition(Utils.getLJAnnotationPosition(e, from)); } @@ -792,9 +796,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc // combine messages of all state changes String message = stateChanges.stream().map(ObjectState::getMessage) .filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); - SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom) - .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst() + Optional declaration = stateChanges.stream().filter(ObjectState::hasFrom) + .filter(s -> s.getFromPosition() != null).findFirst(); + SourcePosition declarationPosition = declaration.map(ObjectState::getFromPosition) .orElse(function.getPlacementInCode().getPosition()); + List declarationNotes = declaration.map(ObjectState::getWrittenFrom).filter(Objects::nonNull) + .map(written -> declarationNotes(written.getExpression(), tc.getContext())).orElse(List.of()); List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, vi, prevState, invocation); @@ -811,10 +818,33 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState, - expectedStatesDisjunction, message, hints, category, context); + expectedStatesDisjunction, message, hints, category, context, declarationNotes); } } + /** + * What each state of a named set that {@code written} writes as the shorthand means as the error's message shows + * it, e.g. {@code where closed(this) means doorState(this) == closed}: the declaration is shown as written + */ + private static List declarationNotes(Expression written, Context context) { + List meanings = new ArrayList<>(); + addMeanings(written, context, meanings); + return meanings.isEmpty() ? List.of() : List.of("where " + String.join(", ", meanings)); + } + + private static void addMeanings(Expression e, Context context, List meanings) { + if (e instanceof FunctionInvocation state && state.getArgs().size() == 1 + && StateValues.setNameOf(state.getName(), context.getGhostStates(), context.getGhosts()).isPresent()) { + String meaning = state.toDisplayString() + " means " + + StateValues.toSetForm(state, context.getGhostStates(), context.getGhosts()).toDisplayString(); + if (!meanings.contains(meaning)) + meanings.add(meaning); + return; + } + for (Expression child : e.getChildren()) + addMeanings(child, context, meanings); + } + /** * The state machine of the receiver's class, the states the receiver can be in before a call, and the ghost states * of the class and its supertypes diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index 46e51d46..ffb487cc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -144,7 +144,7 @@ void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { new Predicate(RefinementsParser.createAST("full(box)", "")), new VCSimplificationResult( vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")), - new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity()); + new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity(), List.of()); assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage()); }