From 634107df5cee0771971b2fb93a9e3bedff569ec2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:56:42 +0000 Subject: [PATCH 1/6] 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 3429e5ee..2afea5ff 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 5dd2b84939966e2c043ac3642f56516ac4bf5a40 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:30:05 +0000 Subject: [PATCH 2/6] 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 1e30bc3cccb0f28ba54c3d52ef2d6f39be3dfe8e Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:36:12 +0000 Subject: [PATCH 3/6] 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 1783aecacaf4bf51a4787068b166b304c7f214d1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 13:44:04 +0000 Subject: [PATCH 4/6] 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 79a819c2d2c3d2e1833defdbf4d538c52581e142 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 15:47:55 +0000 Subject: [PATCH 5/6] 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 c9a5ba1694991fa007e48cda82beeb6bad6f84d2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 16:43:58 +0000 Subject: [PATCH 6/6] 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 2afea5ff..1cd7630d 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("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); }