From 2ce43f406851d6c07b661e7c28a15ac9daa11cb2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:22:33 +0000 Subject: [PATCH 1/3] Show a subclass's call on the state set it inherits from a superclass's spec When a state error was on a method declared in a subclass's spec (Frame's setUndecorated) and the state set in a superclass's spec (Window), the State Machine view showed no diagram for the error, or Window's diagram without the call and without any marked state. The diagrams of a state error are now parsed for the receiver's class with liquidjava-fsm 0.2.3, which merges the specs of its supertypes as the verifier does. Besides the declaration's file, the parser reads the files of the state sets the verifier knows, where those specs may be. Co-Authored-By: Claude Opus 5.5 --- server/pom.xml | 2 +- .../dtos/errors/StateRefinementErrorDTO.java | 34 +++++++++++--- .../errors/StateRefinementErrorDTOTest.java | 44 +++++++++++++++++++ .../resources/inherited/FrameRefinements.java | 14 ++++++ .../inherited/WindowRefinements.java | 15 +++++++ 5 files changed, 103 insertions(+), 6 deletions(-) create mode 100644 server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java create mode 100644 server/src/test/resources/inherited/FrameRefinements.java create mode 100644 server/src/test/resources/inherited/WindowRefinements.java diff --git a/server/pom.xml b/server/pom.xml index cc6d090..4c9a8ff 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-fsm - 0.2.2 + 0.2.3 tools.aqua diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index 0940d97..bb3bd9d 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -1,15 +1,21 @@ package dtos.errors; -import java.io.File; +import java.util.Collection; import java.util.List; +import java.util.Objects; +import java.util.stream.Stream; import dtos.diagnostics.SourcePositionDTO; import dtos.diagnostics.VCSimplificationResultDTO; import dtos.fsm.StateMachineDTO; import liquidjava.diagnostics.errors.StateErrorContext; import liquidjava.diagnostics.errors.StateRefinementError; +import liquidjava.fsm.StateMachine; import liquidjava.fsm.StateMachineParser; +import liquidjava.processor.context.ContextHistory; +import liquidjava.processor.context.GhostState; import liquidjava.rj_language.ast.formatter.ExpressionFormatter; +import utils.PathUtils; /** * DTO for serializing StateRefinementError instances to JSON @@ -28,14 +34,32 @@ public StateRefinementErrorDTO(StateRefinementError error) { this.found = VCSimplificationResultDTO.from(error.getFoundSimplification()); this.customMessage = error.getCustomMessage(); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); - StateErrorContext context = error.getContext(); this.stateMachines = declarationPosition == null || declarationPosition.file() == null ? List.of() - : StateMachineDTO.from(StateMachineParser.parseAll( - new File(declarationPosition.file()).toURI().toString(), - context == null ? null : context.receiverClass()), context); + : stateMachines(declarationPosition.file(), stateSetFiles(), error.getContext()); } public static StateRefinementErrorDTO from(StateRefinementError error) { return new StateRefinementErrorDTO(error); } + + /** + * The diagrams of the receiver's class, which may inherit the state sets and methods of its supertypes' specs + * @param declarationFile the file of the spec of the called method + * @param stateSetFiles the files that declare state sets, where the specs of the supertypes may be + * @param context the state error, or null if the verifier gives no states, in which case the diagrams are those of + * the first class of the declaration's file + */ + static List stateMachines(String declarationFile, Collection stateSetFiles, + StateErrorContext context) { + String declarationUri = PathUtils.toFileUri(declarationFile); + List sms = context == null ? StateMachineParser.parseAll(declarationUri) + : StateMachineParser.parseAll(Stream.concat(Stream.of(declarationUri), + stateSetFiles.stream().map(PathUtils::toFileUri)).toList(), context.receiverClass()); + return StateMachineDTO.from(sms, context); + } + + private static List stateSetFiles() { + return ContextHistory.getInstance().getGhosts().stream().map(GhostState::getFile).filter(Objects::nonNull) + .distinct().toList(); + } } diff --git a/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java new file mode 100644 index 0000000..6842824 --- /dev/null +++ b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java @@ -0,0 +1,44 @@ +package dtos.errors; + +import static org.junit.jupiter.api.Assertions.*; + +import java.nio.file.Path; +import java.util.List; + +import org.junit.jupiter.api.Test; + +import dtos.fsm.StateMachineDTO; +import liquidjava.diagnostics.errors.StateErrorContext; +import liquidjava.fsm.StateMachineTransition; + +class StateRefinementErrorDTOTest { + + private static final String WINDOW = file("WindowRefinements.java"); + private static final String FRAME = file("FrameRefinements.java"); + private static final StateErrorContext SET_UNDECORATED = new StateErrorContext("host", "java.awt.Frame", + "setUndecorated(boolean)", List.of(List.of("displayable")), List.of(List.of("notDisplayable")), true); + + private static String file(String name) { + return Path.of("src", "test", "resources", "inherited", name).toAbsolutePath().toString(); + } + + @Test + void showsTheCallOnTheStateSetItsClassInheritsFromTheSuperclassSpec() { + List dtos = StateRefinementErrorDTO.stateMachines(FRAME, List.of(WINDOW), SET_UNDECORATED); + assertEquals(1, dtos.size()); + StateMachineDTO sm = dtos.get(0); + assertEquals("java.awt.Frame", sm.className()); + assertEquals(List.of("displayable", "notDisplayable"), sm.states()); + assertEquals(List.of("setUndecorated", "dispose", "pack"), + sm.transitions().stream().map(StateMachineTransition::label).distinct().toList()); + assertEquals(List.of("displayable"), sm.errorContext().invalidStates()); + assertEquals(List.of("notDisplayable"), sm.errorContext().acceptedStates()); + } + + @Test + void showsTheDeclarationFilesFirstClassWithoutTheVerifiersStates() { + List dtos = StateRefinementErrorDTO.stateMachines(WINDOW, List.of(FRAME), null); + assertEquals(List.of("java.awt.Window"), dtos.stream().map(StateMachineDTO::className).toList()); + assertNull(dtos.get(0).errorContext()); + } +} diff --git a/server/src/test/resources/inherited/FrameRefinements.java b/server/src/test/resources/inherited/FrameRefinements.java new file mode 100644 index 0000000..c8df129 --- /dev/null +++ b/server/src/test/resources/inherited/FrameRefinements.java @@ -0,0 +1,14 @@ +package inherited; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; + +// the state set is declared in the superclass's spec, in another file +@ExternalRefinementsFor("java.awt.Frame") +public interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/server/src/test/resources/inherited/WindowRefinements.java b/server/src/test/resources/inherited/WindowRefinements.java new file mode 100644 index 0000000..d6a38b2 --- /dev/null +++ b/server/src/test/resources/inherited/WindowRefinements.java @@ -0,0 +1,15 @@ +package inherited; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void dispose(); + + @StateRefinement(to = "displayable(this)") + void pack(); +} From 1ce5b5b90cc5e34d131d7a2087b995ad19cba9c2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:39:41 +0000 Subject: [PATCH 2/3] Read the specs of supertypes that only refine methods A supertype's spec without a state set, such as Frame's between JFrame and Window, was not read, so its methods were missing from the diagram. The server now also passes the files of the verifier's state refinements. Co-Authored-By: Claude Opus 5.5 --- .../dtos/errors/StateRefinementErrorDTO.java | 20 +++++---- .../errors/StateRefinementErrorDTOTest.java | 41 +++++++++++++++---- .../A_WindowRefinements.java} | 5 +-- .../B_FrameRefinements.java} | 4 +- .../hierarchy/C_JFrameRefinements.java | 12 ++++++ server/src/test/resources/hierarchy/Use.java | 9 ++++ 6 files changed, 70 insertions(+), 21 deletions(-) rename server/src/test/resources/{inherited/WindowRefinements.java => hierarchy/A_WindowRefinements.java} (74%) rename server/src/test/resources/{inherited/FrameRefinements.java => hierarchy/B_FrameRefinements.java} (87%) create mode 100644 server/src/test/resources/hierarchy/C_JFrameRefinements.java create mode 100644 server/src/test/resources/hierarchy/Use.java diff --git a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java index bb3bd9d..e994a45 100644 --- a/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java +++ b/server/src/main/java/dtos/errors/StateRefinementErrorDTO.java @@ -14,6 +14,7 @@ import liquidjava.fsm.StateMachineParser; import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostState; +import liquidjava.processor.context.RefinedFunction; import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import utils.PathUtils; @@ -35,7 +36,7 @@ public StateRefinementErrorDTO(StateRefinementError error) { this.customMessage = error.getCustomMessage(); this.declarationPosition = SourcePositionDTO.from(error.getDeclarationPosition()); this.stateMachines = declarationPosition == null || declarationPosition.file() == null ? List.of() - : stateMachines(declarationPosition.file(), stateSetFiles(), error.getContext()); + : stateMachines(declarationPosition.file(), specFiles(), error.getContext()); } public static StateRefinementErrorDTO from(StateRefinementError error) { @@ -45,21 +46,26 @@ public static StateRefinementErrorDTO from(StateRefinementError error) { /** * The diagrams of the receiver's class, which may inherit the state sets and methods of its supertypes' specs * @param declarationFile the file of the spec of the called method - * @param stateSetFiles the files that declare state sets, where the specs of the supertypes may be + * @param specFiles the files of the other specs, where those of the supertypes may be * @param context the state error, or null if the verifier gives no states, in which case the diagrams are those of * the first class of the declaration's file */ - static List stateMachines(String declarationFile, Collection stateSetFiles, + static List stateMachines(String declarationFile, Collection specFiles, StateErrorContext context) { String declarationUri = PathUtils.toFileUri(declarationFile); List sms = context == null ? StateMachineParser.parseAll(declarationUri) : StateMachineParser.parseAll(Stream.concat(Stream.of(declarationUri), - stateSetFiles.stream().map(PathUtils::toFileUri)).toList(), context.receiverClass()); + specFiles.stream().map(PathUtils::toFileUri)).toList(), context.receiverClass()); return StateMachineDTO.from(sms, context); } - private static List stateSetFiles() { - return ContextHistory.getInstance().getGhosts().stream().map(GhostState::getFile).filter(Objects::nonNull) - .distinct().toList(); + /** The files of the state sets and state refinements of the last verification */ + static List specFiles() { + ContextHistory history = ContextHistory.getInstance(); + Stream stateSets = history.getGhosts().stream().map(GhostState::getFile); + Stream stateRefinements = history.getMethods().stream().filter(RefinedFunction::hasStateChange) + .map(method -> SourcePositionDTO.from(method.getPlacementInCode().getPosition())) + .filter(Objects::nonNull).map(SourcePositionDTO::file); + return Stream.concat(stateSets, stateRefinements).filter(Objects::nonNull).distinct().toList(); } } diff --git a/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java index 6842824..ec0d110 100644 --- a/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java +++ b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java @@ -8,37 +8,62 @@ import org.junit.jupiter.api.Test; import dtos.fsm.StateMachineDTO; +import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.errors.StateErrorContext; import liquidjava.fsm.StateMachineTransition; class StateRefinementErrorDTOTest { - private static final String WINDOW = file("WindowRefinements.java"); - private static final String FRAME = file("FrameRefinements.java"); - private static final StateErrorContext SET_UNDECORATED = new StateErrorContext("host", "java.awt.Frame", - "setUndecorated(boolean)", List.of(List.of("displayable")), List.of(List.of("notDisplayable")), true); + private static final Path HIERARCHY = Path.of("src", "test", "resources", "hierarchy").toAbsolutePath(); + private static final String WINDOW = file("A_WindowRefinements.java"); + private static final String FRAME = file("B_FrameRefinements.java"); + private static final String JFRAME = file("C_JFrameRefinements.java"); private static String file(String name) { - return Path.of("src", "test", "resources", "inherited", name).toAbsolutePath().toString(); + return HIERARCHY.resolve(name).toString(); + } + + private static StateErrorContext call(String receiverClass, String method) { + return new StateErrorContext("host", receiverClass, method, List.of(List.of("displayable")), + List.of(List.of("notDisplayable")), true); + } + + private static List methods(StateMachineDTO sm) { + return sm.transitions().stream().map(StateMachineTransition::label).distinct().toList(); } @Test void showsTheCallOnTheStateSetItsClassInheritsFromTheSuperclassSpec() { - List dtos = StateRefinementErrorDTO.stateMachines(FRAME, List.of(WINDOW), SET_UNDECORATED); + List dtos = StateRefinementErrorDTO.stateMachines(FRAME, List.of(WINDOW), + call("java.awt.Frame", "setUndecorated(boolean)")); assertEquals(1, dtos.size()); StateMachineDTO sm = dtos.get(0); assertEquals("java.awt.Frame", sm.className()); assertEquals(List.of("displayable", "notDisplayable"), sm.states()); - assertEquals(List.of("setUndecorated", "dispose", "pack"), - sm.transitions().stream().map(StateMachineTransition::label).distinct().toList()); + assertEquals(List.of("setUndecorated", "dispose", "pack"), methods(sm)); assertEquals(List.of("displayable"), sm.errorContext().invalidStates()); assertEquals(List.of("notDisplayable"), sm.errorContext().acceptedStates()); } + @Test + void showsTheMethodsOfASuperclassSpecWithoutStateSet() { + List dtos = StateRefinementErrorDTO.stateMachines(JFRAME, List.of(WINDOW, FRAME), + call("javax.swing.JFrame", "setDefaultCloseOperation(int)")); + assertEquals(List.of("setDefaultCloseOperation", "setUndecorated", "dispose", "pack"), methods(dtos.get(0))); + } + @Test void showsTheDeclarationFilesFirstClassWithoutTheVerifiersStates() { List dtos = StateRefinementErrorDTO.stateMachines(WINDOW, List.of(FRAME), null); assertEquals(List.of("java.awt.Window"), dtos.stream().map(StateMachineDTO::className).toList()); assertNull(dtos.get(0).errorContext()); } + + @Test + void readsTheSpecsOfTheStateSetsAndOfTheMethodsWithoutStateSet() { + CommandLineLauncher.cmdArgs.lspMode = true; + CommandLineLauncher.launch(HIERARCHY.toString()); + assertTrue(StateRefinementErrorDTO.specFiles().containsAll(List.of(WINDOW, FRAME, JFRAME)), + StateRefinementErrorDTO.specFiles().toString()); + } } diff --git a/server/src/test/resources/inherited/WindowRefinements.java b/server/src/test/resources/hierarchy/A_WindowRefinements.java similarity index 74% rename from server/src/test/resources/inherited/WindowRefinements.java rename to server/src/test/resources/hierarchy/A_WindowRefinements.java index d6a38b2..f7dc9b8 100644 --- a/server/src/test/resources/inherited/WindowRefinements.java +++ b/server/src/test/resources/hierarchy/A_WindowRefinements.java @@ -1,12 +1,11 @@ -package inherited; - import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; +// the files are named so that the verifier reads the superclasses' specs first (liquidjava#461) @StateSet({"displayable", "notDisplayable"}) @ExternalRefinementsFor("java.awt.Window") -public interface WindowRefinements { +interface WindowRefinements { @StateRefinement(to = "notDisplayable(this)") void dispose(); diff --git a/server/src/test/resources/inherited/FrameRefinements.java b/server/src/test/resources/hierarchy/B_FrameRefinements.java similarity index 87% rename from server/src/test/resources/inherited/FrameRefinements.java rename to server/src/test/resources/hierarchy/B_FrameRefinements.java index c8df129..542559f 100644 --- a/server/src/test/resources/inherited/FrameRefinements.java +++ b/server/src/test/resources/hierarchy/B_FrameRefinements.java @@ -1,11 +1,9 @@ -package inherited; - import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.StateRefinement; // the state set is declared in the superclass's spec, in another file @ExternalRefinementsFor("java.awt.Frame") -public interface FrameRefinements { +interface FrameRefinements { @StateRefinement(to = "notDisplayable(this)") void Frame(String title); diff --git a/server/src/test/resources/hierarchy/C_JFrameRefinements.java b/server/src/test/resources/hierarchy/C_JFrameRefinements.java new file mode 100644 index 0000000..5744173 --- /dev/null +++ b/server/src/test/resources/hierarchy/C_JFrameRefinements.java @@ -0,0 +1,12 @@ +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; + +// inherits the state set from Window's spec and setUndecorated from Frame's, which has no state set +@ExternalRefinementsFor("javax.swing.JFrame") +interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setDefaultCloseOperation(int operation); +} diff --git a/server/src/test/resources/hierarchy/Use.java b/server/src/test/resources/hierarchy/Use.java new file mode 100644 index 0000000..d1bfb64 --- /dev/null +++ b/server/src/test/resources/hierarchy/Use.java @@ -0,0 +1,9 @@ +import java.awt.Frame; + +class Use { + static void borderless() { + Frame host = new Frame("Playfield"); + host.pack(); + host.setUndecorated(true); + } +} From a0b32aa931dbc30478ec72777f4b6ebae7f80f5c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:42:08 +0000 Subject: [PATCH 3/3] Restore the verifier's IDE mode after the spec files test Co-Authored-By: Claude Opus 5.5 --- .../java/dtos/errors/StateRefinementErrorDTOTest.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java index ec0d110..6836529 100644 --- a/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java +++ b/server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java @@ -61,8 +61,13 @@ void showsTheDeclarationFilesFirstClassWithoutTheVerifiersStates() { @Test void readsTheSpecsOfTheStateSetsAndOfTheMethodsWithoutStateSet() { - CommandLineLauncher.cmdArgs.lspMode = true; - CommandLineLauncher.launch(HIERARCHY.toString()); + boolean lspMode = CommandLineLauncher.cmdArgs.lspMode; + CommandLineLauncher.cmdArgs.lspMode = true; // the verifier only keeps its context history in the IDE + try { + CommandLineLauncher.launch(HIERARCHY.toString()); + } finally { + CommandLineLauncher.cmdArgs.lspMode = lspMode; + } assertTrue(StateRefinementErrorDTO.specFiles().containsAll(List.of(WINDOW, FRAME, JFRAME)), StateRefinementErrorDTO.specFiles().toString()); }