Show a subclass's call on the state set it inherits from a superclass's spec

server/pom.xml

@@ -172,7 +172,7 @@
 		<dependency>
 		  <groupId>io.github.liquid-java</groupId>
 		  <artifactId>liquidjava-fsm</artifactId>
-		  <version>0.2.2</version>
+		  <version>0.2.3</version>
 		</dependency>
 		<dependency>
 			<groupId>tools.aqua</groupId>

server/src/main/java/dtos/errors/StateRefinementErrorDTO.java

@@ -1,15 +1,22 @@
 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.processor.context.RefinedFunction;
 import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
+import utils.PathUtils;
 
 /**
  * DTO for serializing StateRefinementError instances to JSON
@@ -28,14 +35,37 @@ 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(), specFiles(), 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 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<StateMachineDTO> stateMachines(String declarationFile, Collection<String> specFiles,
+            StateErrorContext context) {
+        String declarationUri = PathUtils.toFileUri(declarationFile);
+        List<StateMachine> sms = context == null ? StateMachineParser.parseAll(declarationUri)
+                : StateMachineParser.parseAll(Stream.concat(Stream.of(declarationUri),
+                        specFiles.stream().map(PathUtils::toFileUri)).toList(), context.receiverClass());
+        return StateMachineDTO.from(sms, context);
+    }
+
+    /** The files of the state sets and state refinements of the last verification */
+    static List<String> specFiles() {
+        ContextHistory history = ContextHistory.getInstance();
+        Stream<String> stateSets = history.getGhosts().stream().map(GhostState::getFile);
+        Stream<String> 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();
+    }
 }

server/src/test/java/dtos/errors/StateRefinementErrorDTOTest.java

@@ -0,0 +1,74 @@
+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.api.CommandLineLauncher;
+import liquidjava.diagnostics.errors.StateErrorContext;
+import liquidjava.fsm.StateMachineTransition;
+
+class StateRefinementErrorDTOTest {
+
+    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 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<String> methods(StateMachineDTO sm) {
+        return sm.transitions().stream().map(StateMachineTransition::label).distinct().toList();
+    }
+
+    @Test
+    void showsTheCallOnTheStateSetItsClassInheritsFromTheSuperclassSpec() {
+        List<StateMachineDTO> 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"), methods(sm));
+        assertEquals(List.of("displayable"), sm.errorContext().invalidStates());
+        assertEquals(List.of("notDisplayable"), sm.errorContext().acceptedStates());
+    }
+
+    @Test
+    void showsTheMethodsOfASuperclassSpecWithoutStateSet() {
+        List<StateMachineDTO> 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<StateMachineDTO> 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() {
+        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());
+    }
+}

server/src/test/resources/hierarchy/A_WindowRefinements.java

@@ -0,0 +1,14 @@
+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")
+interface WindowRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void dispose();
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+}

server/src/test/resources/hierarchy/B_FrameRefinements.java

@@ -0,0 +1,12 @@
+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")
+interface FrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void Frame(String title);
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

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);
+}

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);
+    }
+}