From 6a52577832f4a32c0fc849ac2f00a3360af376b4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:56:42 +0000 Subject: [PATCH 1/7] Allow an optional name on @StateSet A named state set's ghost function takes that name instead of the generated stateN, so messages, hints and the equalities that keep unmentioned sets print e.g. redo(um), and specs can use it like any ghost (redo(old(this))). Unnamed sets keep stateN. A name must be a lowercase identifier that is not already a state, ghost or other state set of the class. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/specification/StateSet.java | 14 ++++++ .../testSuite/ErrorStateHintMultipleSets.java | 2 +- .../java/testSuite/ErrorStateSetNames.java | 20 +++++++++ .../EditCommand.java | 8 ++++ .../UndoManagerRefinementsExpert.java | 10 ++--- .../ExternalRefinementTypeChecker.java | 3 +- .../refinement_checker/TypeChecker.java | 44 ++++++++++++++++--- .../liquidjava/api/tests/TestStateHints.java | 8 ++++ 8 files changed, 96 insertions(+), 13 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java index ad074c48..35f668f5 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java @@ -45,6 +45,20 @@ */ String[] value(); + /** + * Optional name of the state set, used in messages and usable in predicates as a function that gives the current + * state of the set (e.g. {@code redo(this) == old(redo(this))}). It must be a lowercase identifier that is not + * already the name of a state, ghost or other state set of the class. Unnamed sets get a generated name. + *

+ * Example: + * 

+     * {@code
+     * @StateSet(name = "redo", value = {"redoable", "notRedoable"})
+     * }
+     *
+ */ + String name() default ""; + /** * Container annotation used by {@link Repeatable} to support multiple state sets. */ diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java index f3bc2ce1..b052fb55 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java @@ -3,7 +3,7 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -@StateSet({"closed", "opened"}) +@StateSet(name = "door", value = {"closed", "opened"}) @StateSet({"unlocked", "locked"}) public class ErrorStateHintMultipleSets { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java new file mode 100644 index 00000000..c38a69b1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java @@ -0,0 +1,20 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateSet; + +// A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses +@StateSet(name = "Door", value = {"closed", "opened"}) // Expect: Error +public class ErrorStateSetNames {} + +@StateSet(name = "locked", value = {"closed", "opened"}) // Expect: Error +@StateSet({"unlocked", "locked"}) +class ErrorStateSetNameOfAState {} + +@StateSet(name = "lock", value = {"closed", "opened"}) // Expect: Error +@Ghost("int lock") +class ErrorStateSetNameOfAGhost {} + +@StateSet(name = "door", value = {"closed", "opened"}) // Expect: Error +@StateSet(name = "door", value = {"unlocked", "locked"}) +class ErrorStateSetNameOfAnotherSet {} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java index cadcced5..139a10b6 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java @@ -26,6 +26,14 @@ public void execute() { default -> { } } } + + // canUndo() keeps the undo set when it returns false, so the edit added before can still be undone + static void undoAfterAsking(javax.swing.undo.UndoableEdit edit) { + UndoManager undoManager = new UndoManager(); + undoManager.addEdit(edit); + undoManager.canUndo(); + undoManager.undo(); + } } enum StandardActions { diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java index 7015d9d7..b8c58588 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java @@ -16,9 +16,9 @@ // JDK 21: after end() the manager is one CompoundEdit, and undo/redo alternate over all edits at // once (AbstractUndoableEdit.hasBeenDone), so end() makes it undoable and not redoable. @ExternalRefinementsFor("javax.swing.undo.UndoManager") -@StateSet({"start", "canEdit", "end"}) -@StateSet({"undoable", "notUndoable"}) -@StateSet({"redoable", "notRedoable"}) +@StateSet(name="phase", value={"start", "canEdit", "end"}) +@StateSet(name="undo", value={"undoable", "notUndoable"}) +@StateSet(name="redo", value={"redoable", "notRedoable"}) public interface UndoManagerRefinementsExpert { @StateRefinement(to="start(this) && notUndoable(this) && notRedoable(this)") @@ -81,8 +81,8 @@ public interface UndoManagerRefinementsExpert { // Queries: they never change the manager, they tell the verifier which state it is in. When it is // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose // state is unknown) the answer decides. - @StateRefinement(from="undoable(this)", to="return && undoable(this)") - @StateRefinement(to="return ? undoable(this) : notUndoable(this)") + // canUndo() keeps its set by name when it returns false. + @StateRefinement(to="return ? undoable(this) : undo(this) == undo(old(this))") boolean canUndo(); @StateRefinement(from="redoable(this)", to="return && redoable(this)") diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 077c1a74..d152d9c4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -119,12 +119,11 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition } @Override - protected Optional createStateGhost(int order, CtElement element) { + protected Optional createStateGhost(String name, CtElement element) { String klass = Utils.getSimpleName(prefix); if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = List.of(klass); - String name = String.format("state%d", order); GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix); return Optional.of(gh); } 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 0e886a0e..33a0dc4a 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 @@ -3,6 +3,7 @@ import java.lang.annotation.Annotation; import java.util.Collections; import java.util.HashMap; +import java.util.LinkedHashMap; import java.util.List; import java.util.Map; import java.util.Optional; @@ -200,20 +201,53 @@ public Optional getMessageFromAnnotation(CtElement element) { @SuppressWarnings("unchecked") public void handleStateSetsFromAnnotation(CtElement element) throws LJError { int set = 0; + Map namedSets = new LinkedHashMap<>(); for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getAnnotationType().getQualifiedName(); if (an.contentEquals("liquidjava.specification.StateSet")) { set++; - createStateSet((CtNewArray) ann.getAllValues().get("value"), set, element); + CtExpression nameValue = ann.getValues().get("name"); + String name = nameValue == null ? null : getStringFromAnnotation(nameValue); + SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); + if (name != null && name.isEmpty()) + name = null; + if (name != null && (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") + || name.equals("false"))) + throw new CustomError(String.format( + "State set name '%s' must be an identifier that starts with a lowercase letter", name), + namePosition); + GhostFunction g = createStateSet((CtNewArray) ann.getAllValues().get("value"), + name != null ? name : String.format("state%d", set), element); + if (name != null) + namedSets.put(g, namePosition); } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); createStateGhost(s.getValue(), element, Utils.getAnnotationValuePosition(s)); } } + // checked once every set and ghost of the class exists, so the order of the annotations does not matter + for (Map.Entry named : namedSets.entrySet()) + checkStateSetNameIsFree(named.getKey(), named.getValue()); } - private void createStateSet(CtNewArray e, int set, CtElement element) throws LJError { + /** Reports a named state set whose name is also the name of a state, ghost or other state set of its class */ + private void checkStateSetNameIsFree(GhostFunction set, SourcePosition position) throws LJError { + String name = set.getName(); + String usedBy = null; + for (GhostState gs : context.getGhostState(set.getParentClassName())) + if (gs.getPrefix().equals(set.getPrefix()) && gs.getName().equals(name)) + usedBy = gs.getParent() != null ? "a state" : "a ghost"; + for (GhostFunction g : context.getGhosts()) + if (usedBy == null && g != set && g.getPrefix().equals(set.getPrefix()) && g.getName().equals(name)) + usedBy = context.getGhostStates().stream().anyMatch(gs -> gs.getParent() == g) ? "another state set" + : "a ghost"; + if (usedBy != null) + throw new CustomError(String.format("State set name '%s' is already the name of %s of %s", name, usedBy, + set.getParentClassName()), position); + } + + private GhostFunction createStateSet(CtNewArray e, String name, CtElement element) throws LJError { // if any of the states starts with uppercase, throw error (reserved for alias) for (CtExpression ce : e.getElements()) { @@ -227,7 +261,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } } - Optional og = createStateGhost(set, element); + Optional og = createStateGhost(name, element); if (og.isEmpty()) { throw new RuntimeException("Error in creation of GhostFunction"); } @@ -252,6 +286,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } order++; } + return g; } protected GhostDTO getGhostDeclaration(String value, SourcePosition position) throws LJError { @@ -294,13 +329,12 @@ protected String getSimpleClassName(CtElement element) { return getEnclosingType(element).map(CtType::getSimpleName).orElse(null); } - protected Optional createStateGhost(int order, CtElement element) { + protected Optional createStateGhost(String name, CtElement element) { Optional> enclosingType = getEnclosingType(element); if (enclosingType.isPresent()) { CtType type = enclosingType.get(); CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = Collections.singletonList(type.getSimpleName()); - String name = String.format("state%d", order); GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName()); return Optional.of(gh); } 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 4d853f4b..037e576f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -339,6 +339,14 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } + @Test + void foundKeepsANamedStateSetByItsName() { + StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0); + assertEquals( + "found closed(d@26) && unlocked(d@26) && locked(d) && door(d) == door(d@26) but expected closed(d) && unlocked(d)", + error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( From 3f8c1325812b1d43d5463a4b603a18601c93fc56 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:30:05 +0000 Subject: [PATCH 2/7] Report a state set name that is not a string literal Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 ++ 1 file changed, 2 insertions(+) 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 33a0dc4a..f190e1ea 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 @@ -209,6 +209,8 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { CtExpression nameValue = ann.getValues().get("name"); String name = nameValue == null ? null : getStringFromAnnotation(nameValue); SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); + if (nameValue != null && name == null) + throw new CustomError("State set name must be a string literal", namePosition); if (name != null && name.isEmpty()) name = null; if (name != null && (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") From 68d2fcd05ac168cb6e179c88b63281eb408b2505 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:36:12 +0000 Subject: [PATCH 3/7] Keep canUndo()'s known-undoable refinement in the named-sets fixture Co-Authored-By: Claude Opus 5.5 --- .../state_hint_study_undo_manager_correct/EditCommand.java | 6 +++--- .../UndoManagerRefinementsExpert.java | 3 ++- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java index 139a10b6..9db91bee 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java @@ -27,11 +27,11 @@ public void execute() { } } - // canUndo() keeps the undo set when it returns false, so the edit added before can still be undone + // When canUndo() returns false its spec keeps the undo set by name, so the manager is still notUndoable static void undoAfterAsking(javax.swing.undo.UndoableEdit edit) { UndoManager undoManager = new UndoManager(); - undoManager.addEdit(edit); - undoManager.canUndo(); + if (!undoManager.canUndo()) + undoManager.addEdit(edit); undoManager.undo(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java index b8c58588..24b334cc 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java @@ -81,7 +81,8 @@ public interface UndoManagerRefinementsExpert { // Queries: they never change the manager, they tell the verifier which state it is in. When it is // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose // state is unknown) the answer decides. - // canUndo() keeps its set by name when it returns false. + // When canUndo() returns false it keeps the undo set by name. + @StateRefinement(from="undoable(this)", to="return && undoable(this)") @StateRefinement(to="return ? undoable(this) : undo(this) == undo(old(this))") boolean canUndo(); From 93a3759fe90986361db5481e8300ef20ed003dc2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:44:04 +0000 Subject: [PATCH 4/7] Accept only a plain string literal as a state set name Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 f190e1ea..38030fd9 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 @@ -207,7 +207,8 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { if (an.contentEquals("liquidjava.specification.StateSet")) { set++; CtExpression nameValue = ann.getValues().get("name"); - String name = nameValue == null ? null : getStringFromAnnotation(nameValue); + String name = nameValue instanceof CtLiteral literal && literal.getValue()instanceof String value + ? value : null; SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); if (nameValue != null && name == null) throw new CustomError("State set name must be a string literal", namePosition); From 37048861a68e443501c10d637dcad847af14d102 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 15:47:55 +0000 Subject: [PATCH 5/7] Read a state set's name in its own method Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/TypeChecker.java | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) 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 38030fd9..ed01d33e 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 @@ -207,18 +207,8 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { if (an.contentEquals("liquidjava.specification.StateSet")) { set++; CtExpression nameValue = ann.getValues().get("name"); - String name = nameValue instanceof CtLiteral literal && literal.getValue()instanceof String value - ? value : null; SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); - if (nameValue != null && name == null) - throw new CustomError("State set name must be a string literal", namePosition); - if (name != null && name.isEmpty()) - name = null; - if (name != null && (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") - || name.equals("false"))) - throw new CustomError(String.format( - "State set name '%s' must be an identifier that starts with a lowercase letter", name), - namePosition); + String name = stateSetName(nameValue, namePosition); GhostFunction g = createStateSet((CtNewArray) ann.getAllValues().get("value"), name != null ? name : String.format("state%d", set), element); if (name != null) @@ -234,6 +224,20 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { checkStateSetNameIsFree(named.getKey(), named.getValue()); } + /** The name given to a state set, or null when it has none */ + private static String stateSetName(CtExpression nameValue, SourcePosition position) throws LJError { + if (nameValue == null) + return null; + if (!(nameValue instanceof CtLiteral literal && literal.getValue()instanceof String name)) + throw new CustomError("State set name must be a string literal", position); + if (name.isEmpty()) + return null; + if (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") || name.equals("false")) + throw new CustomError(String.format( + "State set name '%s' must be an identifier that starts with a lowercase letter", name), position); + return name; + } + /** Reports a named state set whose name is also the name of a state, ghost or other state set of its class */ private void checkStateSetNameIsFree(GhostFunction set, SourcePosition position) throws LJError { String name = set.getName(); From 627285122c59019dd7c68ec281ca6d26385af320 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 16:43:58 +0000 Subject: [PATCH 6/7] Name both state sets in ErrorStateHintMultipleSets Co-Authored-By: Claude Opus 5.5 --- .../src/main/java/testSuite/ErrorStateHintMultipleSets.java | 4 ++-- .../src/test/java/liquidjava/api/tests/TestStateHints.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java index b052fb55..7c1f696e 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java @@ -3,8 +3,8 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -@StateSet(name = "door", value = {"closed", "opened"}) -@StateSet({"unlocked", "locked"}) +@StateSet(name = "doorState", value = {"closed", "opened"}) +@StateSet(name = "lockState", value = {"unlocked", "locked"}) public class ErrorStateHintMultipleSets { @StateRefinement(to = "closed(this) && unlocked(this)") 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 037e576f..1a99b4e5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -343,7 +343,7 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { void foundKeepsANamedStateSetByItsName() { StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0); assertEquals( - "found closed(d@26) && unlocked(d@26) && locked(d) && door(d) == door(d@26) but expected closed(d) && unlocked(d)", + "found closed(d@26) && unlocked(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } From 1d67db4358cdac63a448982b831c224271c9c2a4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 9 Nov 2026 17:12:07 +0000 Subject: [PATCH 7/7] Expect the Found of ErrorStateHintMultipleSets without the unrelated lock set Co-Authored-By: Claude Opus 5.5 --- .../src/test/java/liquidjava/api/tests/TestStateHints.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1a99b4e5..459f460d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -343,7 +343,7 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { void foundKeepsANamedStateSetByItsName() { StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0); assertEquals( - "found closed(d@26) && unlocked(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)", + "found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); }