From 10e5d0b2254dfefecc2c56fb412948342642a31f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:22:10 +0000 Subject: [PATCH 1/2] Inherit the state sets and methods of the supertypes' specs A class whose @StateSet is in a superclass's spec, such as java.awt.Frame with the displayable states declared for java.awt.Window, had no state machine, and the superclass's machine did not have the subclass's methods. parseAll(List uris, String className) builds one model from several files and merges the specs of the class's supertypes in them, as the verifier does when it builds a receiver's machine: the class's own state sets first, then those of its supertypes, nearest first. A call uses the class's own refinement of a method, otherwise that of the nearest type that declares it, so an inherited refinement is left out when a nearer spec refines the method, when a nearer type redeclares it, or when not every caller can call it. Constructors stay the class's own. parseAll(uri, className) does the same for the specs in one file. Co-Authored-By: Claude Opus 5.5 --- README.md | 8 + .../liquidjava/fsm/StateMachineParser.java | 225 ++++++++++++++++-- .../fsm/StateMachineParserTests.java | 40 ++++ src/test/resources/fsm/InheritedOverride.java | 31 +++ src/test/resources/fsm/InheritedStateSet.java | 32 +++ .../fsm/inherited/FrameRefinements.java | 14 ++ .../fsm/inherited/WindowRefinements.java | 15 ++ 7 files changed, 344 insertions(+), 21 deletions(-) create mode 100644 src/test/resources/fsm/InheritedOverride.java create mode 100644 src/test/resources/fsm/InheritedStateSet.java create mode 100644 src/test/resources/fsm/inherited/FrameRefinements.java create mode 100644 src/test/resources/fsm/inherited/WindowRefinements.java diff --git a/README.md b/README.md index a2e0c83..3e97b2f 100644 --- a/README.md +++ b/README.md @@ -38,8 +38,16 @@ StateMachine stateMachine = StateMachineParser.parse(path.toUri().toString()); StateMachine named = StateMachineParser.parse(path.toUri().toString(), "example.File"); // one state machine per @StateSet, in declaration order List stateMachines = StateMachineParser.parseAll(path.toUri().toString()); +// with the state sets and methods java.awt.Frame inherits from the specs of its supertypes in these files +List inherited = StateMachineParser.parseAll(List.of(frameSpec, windowSpec), "java.awt.Frame"); ``` +A class inherits the state sets and methods of the specs of its supertypes in the parsed files, as in the verifier. +Its own state sets come first, then those of its supertypes, nearest first. A call uses the class's own refinement of a +method, otherwise that of the nearest type that declares the method, so an inherited refinement is left out when a +nearer spec refines the method, when a nearer type redeclares it, or when not every caller can call it. Constructors are +the class's own. + A class with several `@StateSet` annotations has one state machine per state set, since each changes independently. `stateSet` is the index of the state set, the same order the verifier uses in `StateErrorContext`. A state machine only has the transitions that mention its states. States of other state sets in a `from` are kept as diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 1325903..c0fdedc 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -1,10 +1,16 @@ package liquidjava.fsm; import java.net.URI; +import java.net.URISyntaxException; import java.nio.file.Paths; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; +import java.util.Deque; +import java.util.HashSet; import java.util.List; +import java.util.Set; +import java.util.stream.Stream; import liquidjava.rj_language.ast.*; import liquidjava.rj_language.parsing.RefinementsParser; @@ -16,6 +22,7 @@ import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtType; +import spoon.reflect.reference.CtTypeReference; public class StateMachineParser { @@ -63,22 +70,32 @@ public static List parseAll(String uri) { * @return the state machines of the state sets with transitions, in declaration order */ public static List parseAll(String uri, String className) { + return parseAll(List.of(uri), className); + } + + /** + * Parses the class or interface with the given name in the given uris, with the state sets and methods it inherits + * from the specs of its supertypes in them, and extracts one state machine per state set + * As in the verifier, the state sets of the class come first, then those of its supertypes, nearest first, and a + * call uses the class's own refinement of a method, otherwise that of the nearest type that declares the method + * @param uris the document URIs + * @param className the qualified class name, or the name given by ExternalRefinementsFor + * @return the state machines of the state sets with transitions, in declaration order + */ + public static List parseAll(List uris, String className) { try { - String filePath = Paths.get(new URI(uri)).toString(); - Launcher launcher = new Launcher(); - launcher.getEnvironment().setNoClasspath(true); - launcher.getEnvironment().setAutoImports(true); - launcher.addInputResource(filePath); - launcher.buildModel(); - CtModel model = launcher.getModel(); + CtModel model = buildModel(uris); // get class or interface CtType ctType = getType(model, className); if (ctType == null) return List.of(); // no class or interface found - // extract class name and state sets - List> stateSets = getStateSets(ctType); + // extract class name, state sets and methods, with those inherited from the specs of the supertypes + List> supertypes = getSupertypes(model, ctType); + List> specs = getSpecs(model, ctType, supertypes); + List> stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList(); + List> methods = getMethods(specs, supertypes); String qualifiedName = getClassName(ctType); List stateMachines = new ArrayList<>(); for (int i = 0; i < stateSets.size(); i++) { @@ -87,7 +104,7 @@ public static List parseAll(String uri, String className) { if (j != i) otherStates.addAll(stateSets.get(j)); } - StateMachine sm = parseStateSet(ctType, qualifiedName, i, stateSets.get(i), otherStates); + StateMachine sm = parseStateSet(ctType, methods, qualifiedName, i, stateSets.get(i), otherStates); if (sm != null) stateMachines.add(sm); } @@ -99,17 +116,29 @@ public static List parseAll(String uri, String className) { } } + private static CtModel buildModel(List uris) throws URISyntaxException { + Launcher launcher = new Launcher(); + launcher.getEnvironment().setNoClasspath(true); + launcher.getEnvironment().setAutoImports(true); + for (String uri : uris.stream().distinct().toList()) { + launcher.addInputResource(Paths.get(new URI(uri)).toString()); + } + launcher.buildModel(); + return launcher.getModel(); + } + /** * Extracts the state machine of one state set * @param ctType the CtType (class or interface) + * @param methods the methods of the class, with those it inherits * @param qualifiedName the class name * @param stateSet the index of the state set * @param states the states of the state set * @param otherStates the states of the other state sets * @return StateMachine or null if the state set has no transitions */ - private static StateMachine parseStateSet(CtType ctType, String qualifiedName, int stateSet, - List states, List otherStates) { + private static StateMachine parseStateSet(CtType ctType, List> methods, String qualifiedName, + int stateSet, List states, List otherStates) { if (states.isEmpty()) return null; // no states found String simpleClassName = Utils.getSimpleName(qualifiedName); @@ -124,7 +153,7 @@ private static StateMachine parseStateSet(CtType ctType, String qualifiedName initialTransitions = new ArrayList<>(initialTransitions); initialTransitions.addAll(factoryTransitions); List entryTransitions = new ArrayList<>(); - List transitions = getTransitions(ctType, simpleClassName, states, otherStates, entryTransitions); + List transitions = getTransitions(methods, states, otherStates, entryTransitions); if (transitions.isEmpty() && entryTransitions.isEmpty()) return null; // no transitions found @@ -145,6 +174,164 @@ private static CtType getType(CtModel model, String className) { return null; } + /** + * Gets the supertypes of a class whose specs it may inherit, nearest first: its superclasses, then the interfaces + * they implement, as in the verifier + * @param model the CtModel + * @param ctType the CtType (class or interface) + * @return the supertypes, or none if the model has no other type with a spec + */ + private static List> getSupertypes(CtModel model, CtType ctType) { + if (model.getAllTypes().size() == 1) + return List.of(); + CtTypeReference type = getClassReference(ctType); + List> superclasses = new ArrayList<>(); + Deque> interfaces = new ArrayDeque<>(); + Set seen = new HashSet<>(Set.of(type.getQualifiedName())); + for (CtTypeReference t = type; t != null; t = getSuperclass(t)) { + if (t != type && seen.add(t.getQualifiedName())) + superclasses.add(t); + interfaces.addAll(getSuperInterfaces(t)); + } + List> supertypes = new ArrayList<>(superclasses); + while (!interfaces.isEmpty()) { + CtTypeReference t = interfaces.poll(); + if (seen.add(t.getQualifiedName())) { + supertypes.add(t); + interfaces.addAll(getSuperInterfaces(t)); + } + } + return supertypes; + } + + // a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch + private static CtTypeReference getSuperclass(CtTypeReference type) { + try { + return type.getSuperclass(); + } catch (RuntimeException e) { + return null; + } + } + + private static Set> getSuperInterfaces(CtTypeReference type) { + try { + return type.getSuperInterfaces(); + } catch (RuntimeException e) { + return Set.of(); + } + } + + /** + * Gets the reference to the class a class or interface specifies + * @param ctType the CtType (class or interface) + * @return the reference to the class named by ExternalRefinementsFor, or to the class itself + */ + private static CtTypeReference getClassReference(CtType ctType) { + return ctType.getFactory().Type().createReference(getClassName(ctType)); + } + + /** + * Gets the specs of a class and of its supertypes in the model + * @param model the CtModel + * @param ctType the CtType (class or interface) of the class + * @param supertypes the supertypes of the class, nearest first + * @return the CtType of the class, followed by those of its supertypes that have one + */ + private static List> getSpecs(CtModel model, CtType ctType, List> supertypes) { + List> specs = new ArrayList<>(List.of(ctType)); + for (CtTypeReference supertype : supertypes) { + CtType spec = getType(model, supertype.getQualifiedName()); + if (spec != null) + specs.add(spec); + } + return specs; + } + + /** + * Gets the methods of a class and those it inherits from the specs of its supertypes, as the verifier applies them + * An inherited method is left out if a nearer spec refines it, if the nearest type that declares it is not the one + * it is specified for, or if not every caller can call it + * @param specs the CtType of the class, followed by those of its supertypes + * @param supertypes the supertypes of the class, nearest first + * @return the methods, without the constructors of interfaces + */ + private static List> getMethods(List> specs, List> supertypes) { + CtType ctType = specs.get(0); + List> hierarchy = new ArrayList<>(List.of(getClassReference(ctType))); + hierarchy.addAll(supertypes); + List> methods = new ArrayList<>(getDeclaredMethods(ctType)); + for (CtType spec : specs.subList(1, specs.size())) { + for (CtMethod method : getDeclaredMethods(spec)) { + if (!isRefinedIn(method, methods) && resolvesTo(method, spec, hierarchy) && isPublic(method, spec)) + methods.add(method); + } + } + return methods; + } + + /** + * Gets the methods of a class or interface, without the methods of interfaces that stand for constructors + * @param ctType the CtType (class or interface) + * @return the methods + */ + private static List> getDeclaredMethods(CtType ctType) { + String className = Utils.getSimpleName(getClassName(ctType)); + return ctType.getMethods().stream() + .filter(method -> !(ctType.isInterface() && method.getSimpleName().equals(className))).toList(); + } + + private static boolean isRefinedIn(CtMethod method, List> methods) { + return methods.stream().anyMatch(m -> m.getSimpleName().equals(method.getSimpleName()) + && getQualifiedParameterTypes(m).equals(getQualifiedParameterTypes(method))); + } + + private static List getQualifiedParameterTypes(CtMethod method) { + return method.getParameters().stream() + .map(parameter -> parameter.getType() == null ? "" : parameter.getType().getQualifiedName()).toList(); + } + + /** + * Checks whether the nearest type in the hierarchy that declares a method is the one a spec is for, which is where + * the verifier looks up the refinement of a call + * @param method the method of the spec + * @param spec the CtType (class or interface) of the spec + * @param hierarchy the class, followed by its supertypes, nearest first + * @return whether a call on the class uses the spec's refinement of the method + */ + private static boolean resolvesTo(CtMethod method, CtType spec, List> hierarchy) { + for (CtTypeReference type : hierarchy) { + CtType declaration = type.getTypeDeclaration(); + if (declaration == null) + return false; // cannot tell which type declares it + if (getDeclarations(method, declaration).findAny().isPresent()) + return type.getQualifiedName().equals(getClassName(spec)); + } + return false; + } + + /** + * Checks whether every caller can call a method on a subtype of the class a spec is for, since the diagram is + * shared by every caller + * @param method the method of the spec + * @param spec the CtType (class or interface) of the spec + * @return whether the method is public in the class + */ + private static boolean isPublic(CtMethod method, CtType spec) { + CtType declaring = getClassReference(spec).getTypeDeclaration(); + if (declaring == null) + return false; // cannot tell whether it is public + // interface methods are public unless declared private + return getDeclarations(method, declaring).allMatch(m -> declaring.isInterface() ? !m.isPrivate() : m.isPublic()); + } + + /** + * Gets the methods of a type that a method of a spec may refer to: those with its name and number of parameters + */ + private static Stream> getDeclarations(CtMethod method, CtType type) { + return type.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName()) + && m.getParameters().size() == method.getParameters().size()); + } + /** * Gets the qualified name from a class or interface * Uses name from ExternalRefinementsFor if present, otherwise uses class or interface name @@ -273,21 +460,17 @@ private static String getParameterTypes(CtExecutable element) { } /** - * Gets transitions from a class or interface - * @param ctType the CtType (class or interface) - * @param className the class name + * Gets transitions from the methods of a class or interface + * @param methods the methods, without the constructors of interfaces * @param states the list of states * @param otherStates the states of the other state sets * @param entryTransitions the list where the entry transitions are added * @return list of StateMachineTransition */ - private static List getTransitions(CtType ctType, String className, List states, + private static List getTransitions(List> methods, List states, List otherStates, List entryTransitions) { List transitions = new ArrayList<>(); - for (CtMethod method : ctType.getMethods()) { - // for interfaces we skip constructor methods (methods with same name as class) - if (ctType.isInterface() && method.getSimpleName().equals(className)) - continue; + for (CtMethod method : methods) { // the verifier uses the first StateRefinement whose from matches, so the states that an earlier from // always matches are not reached by the later ones List coveredStates = new ArrayList<>(); diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index 2072f0a..c533659 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -342,6 +342,46 @@ public void testStateMachinePerStateSet() { assertEquals(List.of(), StateMachineParser.parseAll(uri("TwoStateClasses.java"), "fsm.Missing")); } + private static final StateMachine FRAME = new StateMachine("java.awt.Frame", 0, + List.of("displayable", "notDisplayable"), + List.of(new StateMachineTransition("notDisplayable", "notDisplayable", "setUndecorated"), + new StateMachineTransition("displayable", "notDisplayable", "dispose"), + new StateMachineTransition("notDisplayable", "notDisplayable", "dispose"), + new StateMachineTransition("displayable", "displayable", "pack"), + new StateMachineTransition("notDisplayable", "displayable", "pack")), + List.of(new StateMachineInitialTransition("notDisplayable"))); + + @Test + public void testStateSetAndMethodsInheritedFromTheSuperclassSpec() { + // addNotify is left out: Frame redeclares it, so a call on a Frame does not use the Window spec's refinement + List sms = StateMachineParser.parseAll(uri("InheritedStateSet.java"), "java.awt.Frame"); + assertEquals(1, sms.size()); + assertStateMachineEquals(FRAME, sms.get(0)); + assertTrue(StateMachineParser.parse(uri("InheritedStateSet.java"), "java.awt.Window").transitions().stream() + .anyMatch(transition -> transition.label().equals("addNotify"))); + } + + @Test + public void testSpecsInheritedFromOtherFiles() { + List sms = StateMachineParser.parseAll( + List.of(uri("inherited/FrameRefinements.java"), uri("inherited/WindowRefinements.java")), + "java.awt.Frame"); + assertEquals(1, sms.size()); + assertStateMachineEquals(FRAME, sms.get(0)); + assertEquals(List.of(), StateMachineParser.parseAll(uri("inherited/FrameRefinements.java"), "java.awt.Frame")); + } + + @Test + public void testOverriddenAndPackagePrivateInheritedMethods() { + // the child's next replaces its parent's, and inPackage cannot be called by every caller + StateMachine sm = StateMachineParser.parse(uri("InheritedOverride.java"), "fsm.InheritedOverrideChild"); + assertStateMachineEquals(stateMachine("InheritedOverrideChild", List.of("a", "b", "c"), + List.of(new StateMachineTransition("a", "c", "next"), + new StateMachineTransition("b", "a", "reset"), + new StateMachineTransition("c", "c", "useC")), + List.of(new StateMachineInitialTransition("a"))), sm); + } + @Test public void testVerifierStatesAreStatesOfTheDiagram() { for (String directory : List.of("errors/door", "errors/tree", "errors/udp", "errors/image")) { diff --git a/src/test/resources/fsm/InheritedOverride.java b/src/test/resources/fsm/InheritedOverride.java new file mode 100644 index 0000000..5822028 --- /dev/null +++ b/src/test/resources/fsm/InheritedOverride.java @@ -0,0 +1,31 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"a", "b", "c"}) +public class InheritedOverride { + + @StateRefinement(from = "a(this)", to = "b(this)") + public void next() {} + + @StateRefinement(from = "c(this)") + public void useC() {} + + @StateRefinement(from = "a(this)", to = "c(this)") + void inPackage() {} +} + +// overrides next with a stronger transition and adds one to the states it inherits +class InheritedOverrideChild extends InheritedOverride { + + @StateRefinement(to = "a(this)") + public InheritedOverrideChild() {} + + @Override + @StateRefinement(from = "a(this)", to = "c(this)") + public void next() {} + + @StateRefinement(from = "b(this)", to = "a(this)") + public void reset() {} +} diff --git a/src/test/resources/fsm/InheritedStateSet.java b/src/test/resources/fsm/InheritedStateSet.java new file mode 100644 index 0000000..0977587 --- /dev/null +++ b/src/test/resources/fsm/InheritedStateSet.java @@ -0,0 +1,32 @@ +package fsm; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Window(java.awt.Frame owner); + + @StateRefinement(to = "notDisplayable(this)") + void dispose(); + + @StateRefinement(to = "displayable(this)") + void pack(); + + // Frame redeclares addNotify, so on a Frame the verifier does not apply this refinement + @StateRefinement(to = "displayable(this)") + void addNotify(); +} + +// the state set is declared in the superclass's spec +@ExternalRefinementsFor("java.awt.Frame") +interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/src/test/resources/fsm/inherited/FrameRefinements.java b/src/test/resources/fsm/inherited/FrameRefinements.java new file mode 100644 index 0000000..63637bf --- /dev/null +++ b/src/test/resources/fsm/inherited/FrameRefinements.java @@ -0,0 +1,14 @@ +package fsm.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/src/test/resources/fsm/inherited/WindowRefinements.java b/src/test/resources/fsm/inherited/WindowRefinements.java new file mode 100644 index 0000000..2814511 --- /dev/null +++ b/src/test/resources/fsm/inherited/WindowRefinements.java @@ -0,0 +1,15 @@ +package fsm.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 0ae018e63aa446a89fdb1c44fae1b65ac218666a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:39:38 +0000 Subject: [PATCH 2/2] Skip a missing file and test a supertype spec without a state set A file that no longer exists made the model fail to build, which discarded the specs in the other files. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/fsm/StateMachineParser.java | 7 ++++++- .../fsm/StateMachineParserTests.java | 18 ++++++++++++++++++ .../fsm/inherited/JFrameRefinements.java | 14 ++++++++++++++ 3 files changed, 38 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/fsm/inherited/JFrameRefinements.java diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index c0fdedc..06c333b 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -2,6 +2,8 @@ import java.net.URI; import java.net.URISyntaxException; +import java.nio.file.Files; +import java.nio.file.Path; import java.nio.file.Paths; import java.util.ArrayDeque; import java.util.ArrayList; @@ -116,12 +118,15 @@ public static List parseAll(List uris, String className) { } } + // a file that no longer exists is skipped, so that it does not discard the specs in the others private static CtModel buildModel(List uris) throws URISyntaxException { Launcher launcher = new Launcher(); launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setAutoImports(true); for (String uri : uris.stream().distinct().toList()) { - launcher.addInputResource(Paths.get(new URI(uri)).toString()); + Path path = Paths.get(new URI(uri)); + if (Files.isRegularFile(path)) + launcher.addInputResource(path.toString()); } launcher.buildModel(); return launcher.getModel(); diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index c533659..3876961 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -371,6 +371,24 @@ public void testSpecsInheritedFromOtherFiles() { assertEquals(List.of(), StateMachineParser.parseAll(uri("inherited/FrameRefinements.java"), "java.awt.Frame")); } + @Test + public void testMethodsInheritedFromASpecWithoutStateSet() { + StateMachine sm = StateMachineParser.parseAll(List.of(uri("inherited/JFrameRefinements.java"), + uri("inherited/FrameRefinements.java"), uri("inherited/WindowRefinements.java")), "javax.swing.JFrame") + .get(0); + assertEquals(List.of("setDefaultCloseOperation", "setUndecorated", "dispose", "pack"), + sm.transitions().stream().map(StateMachineTransition::label).distinct().toList()); + assertEquals(List.of(new StateMachineInitialTransition("notDisplayable", null, "new JFrame(String)")), + sm.initialTransitions()); + } + + @Test + public void testMissingFileDoesNotDiscardTheOthers() { + List sms = StateMachineParser.parseAll(List.of(uri("inherited/FrameRefinements.java"), + uri("inherited/WindowRefinements.java"), uri("inherited/Missing.java")), "java.awt.Frame"); + assertEquals(List.of(FRAME.transitions()), sms.stream().map(StateMachine::transitions).toList()); + } + @Test public void testOverriddenAndPackagePrivateInheritedMethods() { // the child's next replaces its parent's, and inPackage cannot be called by every caller diff --git a/src/test/resources/fsm/inherited/JFrameRefinements.java b/src/test/resources/fsm/inherited/JFrameRefinements.java new file mode 100644 index 0000000..51f040c --- /dev/null +++ b/src/test/resources/fsm/inherited/JFrameRefinements.java @@ -0,0 +1,14 @@ +package fsm.inherited; + +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") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setDefaultCloseOperation(int operation); +}