From 4194b0e9741efd85dc47f3a9ff8d0a399c3ade98 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 28 Jan 2026 17:21:06 +0000 Subject: [PATCH 1/8] window --- .../src/main/java/com/window/TestWindows.java | 32 ++++++++++ .../java/com/window/WindowRefinements.java | 59 +++++++++++++++++++ 2 files changed, 91 insertions(+) create mode 100644 examples/demo/src/main/java/com/window/TestWindows.java create mode 100644 examples/demo/src/main/java/com/window/WindowRefinements.java diff --git a/examples/demo/src/main/java/com/window/TestWindows.java b/examples/demo/src/main/java/com/window/TestWindows.java new file mode 100644 index 0000000..a80ba5b --- /dev/null +++ b/examples/demo/src/main/java/com/window/TestWindows.java @@ -0,0 +1,32 @@ +package com.window; + +import java.awt.Window; + +public class TestWindows { + void test1(){ + Window w = new Window(null); + w.pack(); + w.setType(Window.Type.NORMAL); + } + + void test2(){ + Window w = new Window(null); + w.setType(Window.Type.NORMAL); + w.setVisible(false); + w.createBufferStrategy(1); + } + + void test3(){ + Window w = new Window(null); + w.setType(Window.Type.NORMAL); + w.setVisible(true); + w.dispose(); + w.createBufferStrategy(1); + } + + void test4(){ + Window w = new Window(null); + w.pack(); + w.setType(Window.Type.NORMAL); + } +} diff --git a/examples/demo/src/main/java/com/window/WindowRefinements.java b/examples/demo/src/main/java/com/window/WindowRefinements.java new file mode 100644 index 0000000..80a9e39 --- /dev/null +++ b/examples/demo/src/main/java/com/window/WindowRefinements.java @@ -0,0 +1,59 @@ +package com.window; + +import java.awt.AWTKeyStroke; +import java.awt.BufferCapabilities; +import java.awt.Frame; +import java.awt.GraphicsConfiguration; +import java.awt.Window; +import java.util.Set; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements{ + + @StateRefinement(to="notDisplayable(this)") + void Window(Frame owner); + + @StateRefinement(to="notDisplayable(this)") + void Window(Window owner); + + @StateRefinement(to="notDisplayable(this)") + void Window(Window owner, GraphicsConfiguration gc); + + + // to displayable + @StateRefinement(to="displayable(this)") + void addNotify(); // Makes this Window displayable by creating the connection to its native screen resource. This method is called internally by the toolkit and should not be called directly by programs. + + @StateRefinement(to="displayable(this)") + void pack(); //If the window and/or its owner are not displayable yet, both of them are made displayable + + @StateRefinement(from="notDisplayable(this)") + @StateRefinement(from="notDisplayable(this) && b",to="displayable(this)") // if its not displayable yet, is made displayable + @StateRefinement(from="displayable(this)") // stays displayable + void setVisible(boolean b); + + + @StateRefinement(to="notDisplayable(this)") + void dispose(); // makes not displayable. It can be displayed again later by calling pack(). + + @StateRefinement(from="displayable(this)") + void createBufferStrategy(@Refinement("_ > 0")int numBuffers);// IllegalStateException - if the component is not displayable + + + void createBufferStrategy(@Refinement("_ > 0") int numBuffers, BufferCapabilities caps); + + @StateRefinement(from="notDisplayable(this)") + void setType(Window.Type type); // Sets the type of the window. This method can only be called while the window is not displayable. + + + Set getFocusTraversalKeys(@Refinement("_ >= 0 && _ <= 3") int id); + + void setOpacity(@Refinement("_ >= 0 && _ <= 1") float opacity); + +} From e1643c48363477e7f6ca16513daf69c9c1e4a641 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 29 Jan 2026 00:23:34 +0000 Subject: [PATCH 2/8] required model and undomanager --- .../RequiredModelMBeanRefinements.java | 79 +++++++++++++++++++ .../requiredmodelbean/TestRequiredModel.java | 34 ++++++++ .../java/com/undomanager/TestUndoManager.java | 41 ++++++++++ .../undomanager/UndoManagerRefinements.java | 68 ++++++++++++++++ 4 files changed, 222 insertions(+) create mode 100644 examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java create mode 100644 examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java create mode 100644 examples/demo/src/main/java/com/undomanager/TestUndoManager.java create mode 100644 examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java diff --git a/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java new file mode 100644 index 0000000..0269fc0 --- /dev/null +++ b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java @@ -0,0 +1,79 @@ +package com.requiredmodelbean; + +import javax.management.MBeanServer; +import javax.management.ObjectName; +import javax.management.modelmbean.ModelMBeanInfo; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.modelmbean.RequiredModelMBean") +@StateSet({"unregistered", "registered"}) +interface RequiredModelMBeanRefinements{ + + @StateRefinement(to="unregistered(this)") + void RequiredModelMBean(); + + @StateRefinement(to="unregistered(this)") + void RequiredModelMBean(ModelMBeanInfo mbi); + + + @StateRefinement(from="unregistered(this)") + ObjectName preRegister(MBeanServer server, ObjectName name); + + @StateRefinement(to="registered(this)") + void postRegister(Boolean registrationDone); + + + @StateRefinement(from="registered(this)") + void preDeregister(); + + @StateRefinement(from="registered(this)", to="unregistered(this)") + void postDeregister(); + + @StateRefinement(from="unregistered(this)") + void setModelMBeanInfo(ModelMBeanInfo mbi); + + @StateRefinement(from="unregistered(this)") + void load(); + + // void addAttributeChangeNotificationListener(NotificationListener inlistener, String inAttributeName, Object inhandback); + + // void addNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + // Object getAttribute(String attrName); + + // AttributeList getAttributes(String[] attrNames); + + // MBeanInfo getMBeanInfo(); + + // MBeanNotificationInfo[] getNotificationInfo(); + + // Object invoke(String opName, Object[] opArgs, String[] sig); + + // void removeAttributeChangeNotificationListener(NotificationListener inlistener, String inAttributeName); + + // void removeNotificationListener(NotificationListener listener); + + // void removeNotificationListener(NotificationListener listener, NotificationFilter filter, Object handback); + + // void sendAttributeChangeNotification(AttributeChangeNotification ntfyObj); + + // void sendAttributeChangeNotification(Attribute inOldVal, Attribute inNewVal); + + // void sendNotification(String ntfyText); + + // void sendNotification(Notification ntfyObj); + + // void setAttribute(Attribute attribute); + + // AttributeList setAttributes(AttributeList attributes); + + // void setManagedResource(Object mr, String mr_type); + + // void store(); + + + +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java b/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java new file mode 100644 index 0000000..f6cb544 --- /dev/null +++ b/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java @@ -0,0 +1,34 @@ +package com.requiredmodelbean; + +import javax.management.modelmbean.ModelMBeanInfo; +import javax.management.modelmbean.RequiredModelMBean; + +public class TestRequiredModel { + + void test1() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.postRegister(Boolean.TRUE); + r.setModelMBeanInfo(null); //error + } + + void test2() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.setModelMBeanInfo(null); + r.setManagedResource(r, null); + r.postRegister(null); + r.load(); //error + } + + void test3() throws Exception { + RequiredModelMBean r = new RequiredModelMBean(); + r.setModelMBeanInfo(null); + r.load(); + r.setManagedResource(r, null); + r.postRegister(null); + r.store(); + r.postDeregister(); + r.load(); + } +} diff --git a/examples/demo/src/main/java/com/undomanager/TestUndoManager.java b/examples/demo/src/main/java/com/undomanager/TestUndoManager.java new file mode 100644 index 0000000..d837986 --- /dev/null +++ b/examples/demo/src/main/java/com/undomanager/TestUndoManager.java @@ -0,0 +1,41 @@ + +package com.undomanager; + +import javax.swing.undo.UndoManager; + +public class TestUndoManager { + + void test1(){ + UndoManager u = new UndoManager(); + u.addEdit(null); + u.redo(); + u.setLimit(10); + u.redo(); + u.end(); + u.setLimit(10); //error + } + + void testGood(){ + UndoManager u = new UndoManager(); + u.addEdit(null); + u.redo(); + u.setLimit(10); + u.redo(); + u.end(); + u.undoOrRedo(); + } + + void test2(){ + UndoManager u = new UndoManager(); + u.undo(); + u.addEdit(null); + } + + void test3(){ + UndoManager u = new UndoManager(); + u.undoableEditHappened(null); + u.undo(); + u.end(); + u.setLimit(100);//error + } +} \ No newline at end of file diff --git a/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java b/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java new file mode 100644 index 0000000..64825d6 --- /dev/null +++ b/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java @@ -0,0 +1,68 @@ +package com.undomanager; + +import javax.swing.event.UndoableEditEvent; +import javax.swing.undo.UndoableEdit; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"start", "canEdit", "end"}) +public interface UndoManagerRefinements { + + @StateRefinement(to="start(this)") + void UndoManager(); + + @StateRefinement(from="start(this)", to="canEdit(this)") + boolean addEdit(UndoableEdit anEdit); + + @StateRefinement(from="canEdit(this)") + void discardAllEdits(); + + @StateRefinement(to="end(this)") + void end(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoOrRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void redo(); + + @StateRefinement(from="start(this)") + @StateRefinement(from="canEdit(this)") + void setLimit(int l); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undo(); + + @StateRefinement(from="start(this)", to="canEdit(this)") + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undoableEditHappened(UndoableEditEvent e); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + void undoOrRedo(); + + + + // int getLimit(); //any + // boolean canRedo(); + + // boolean canUndo(); + + // boolean canUndoOrRedo(); + +} From 6138e4a0f1db0e31026e97e616fe6558f609a308 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 30 Jan 2026 19:51:26 +0000 Subject: [PATCH 3/8] uuid --- .../demo/src/main/java/com/uuid/Test.java | 34 +++++++++++ .../main/java/com/uuid/UUIDRefinements.java | 59 +++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 examples/demo/src/main/java/com/uuid/Test.java create mode 100644 examples/demo/src/main/java/com/uuid/UUIDRefinements.java diff --git a/examples/demo/src/main/java/com/uuid/Test.java b/examples/demo/src/main/java/com/uuid/Test.java new file mode 100644 index 0000000..767ee58 --- /dev/null +++ b/examples/demo/src/main/java/com/uuid/Test.java @@ -0,0 +1,34 @@ +package com.uuid; + +import java.util.UUID; + +public class Test { + + void test1(){ + UUID t = new UUID(10000L, 0L); + t.clockSequence(); // possible + } + + void test2(){ + UUID t = UUID.randomUUID(); + t.clockSequence(); + } + + void test3(){ + UUID t = UUID.fromString("smt"); + t.clockSequence(); //possible + t.node(); + t.variant(); + } + + void test4(){ + byte[] bytes = {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}; + UUID t = UUID.nameUUIDFromBytes(bytes); + t.variant(); + t.version(); + t.timestamp();//error + + } + + +} diff --git a/examples/demo/src/main/java/com/uuid/UUIDRefinements.java b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java new file mode 100644 index 0000000..e887790 --- /dev/null +++ b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java @@ -0,0 +1,59 @@ +package com.uuid; + +import java.util.UUID; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; +// 0x000000000000F000 +// (v/4096) % 16; + +@ExternalRefinementsFor("java.util.UUID") +@StateSet({"other", "maybeTime"}) +@RefinementAlias("Version(int v) {v >= 0 && v <= 4}") +@RefinementAlias("Variant(int v) {v == 0 || v == 2 || v == 6 || v == 7}") +public interface UUIDRefinements { + + // creation + // would be cool to add + // @StateRefinement(to="((mostSigBits/4096) % 16 == 1) ? timeBased(this) : other(this)") + @StateRefinement(to="maybeTime(this)") + void UUID(long mostSigBits, long leastSigBits); + + //static + @Refinement("maybeTime(return)") + UUID fromString(String name); + + //static + @Refinement("other(return)") + UUID nameUUIDFromBytes(byte[] name); + + //static + @Refinement("other(return)") + UUID randomUUID(); + + + @StateRefinement(from="maybeTime(this)") + int clockSequence(); + + @StateRefinement(from="maybeTime(this)") + long timestamp(); + + @StateRefinement(from="maybeTime(this)") + long node(); + + @Refinement("Variant(_)") + int variant(); + @Refinement("Version(_)") + int version(); + + // int compareTo(UUID val); + // boolean equals(Object obj); + // long getLeastSignificantBits(); + // long getMostSignificantBits(); + // int hashCode(); + // String toString(); + +} From 487f1ba2a827dfcf4827a2e816d0f2ead5966f0f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 31 Jan 2026 15:59:46 +0000 Subject: [PATCH 4/8] pipedwriter --- .../pipedwriter/PipedWriterRefinements.java | 36 +++++++++++++++++++ .../src/main/java/com/pipedwriter/Test.java | 33 +++++++++++++++++ 2 files changed, 69 insertions(+) create mode 100644 examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java create mode 100644 examples/demo/src/main/java/com/pipedwriter/Test.java diff --git a/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java b/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java new file mode 100644 index 0000000..33ddbf1 --- /dev/null +++ b/examples/demo/src/main/java/com/pipedwriter/PipedWriterRefinements.java @@ -0,0 +1,36 @@ +package com.pipedwriter; + +import java.io.PipedReader; +import java.io.PipedWriter; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.PipedWriter") +@StateSet({"started", "connected", "closed"}) +public interface PipedWriterRefinements { + + @StateRefinement(to="started(this)") + void PipedWriter(); + + @StateRefinement(to="started(this)") + void PipedWriter(PipedReader snk); + + @StateRefinement(from="!closed(this)", to="closed(this)") + void close(); + + @StateRefinement(from="started(this)", to="connected(this)") + void connect(PipedReader snk); + + @StateRefinement(from="connected(this)") + void flush(); + + @StateRefinement(from="connected(this)") + void write(char[] cbuf, @Refinement("_ > 0") int off, @Refinement("_ > 0") int len); + + @StateRefinement(from="connected(this)") + void write(int c); + +} diff --git a/examples/demo/src/main/java/com/pipedwriter/Test.java b/examples/demo/src/main/java/com/pipedwriter/Test.java new file mode 100644 index 0000000..da0c1b1 --- /dev/null +++ b/examples/demo/src/main/java/com/pipedwriter/Test.java @@ -0,0 +1,33 @@ +package com.pipedwriter; + +import java.io.IOException; +import java.io.PipedReader; +import java.io.PipedWriter; + +public class Test { + + void test1() throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.write(0); + } + + void test2()throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.connect(new PipedReader()); + pw.write("null"); + pw.flush(); + pw.close(); + pw.write(0); + } + + + void test3()throws IOException{ + PipedWriter pw = new PipedWriter(); + pw.connect(new PipedReader()); + pw.write("null"); + pw.flush(); + pw.close(); + pw.write(0); + } + +} From 82cf9cc0bcef303c9e3137b07ecb9af6686804cd Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 31 Jan 2026 16:33:58 +0000 Subject: [PATCH 5/8] abstractundo --- .../abstractundo/AbstractUndoRefinements.java | 39 +++++++++++++++++++ .../com/abstractundo/TestAbstractUndo.java | 28 +++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java create mode 100644 examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java diff --git a/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java b/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java new file mode 100644 index 0000000..514e6bd --- /dev/null +++ b/examples/demo/src/main/java/com/abstractundo/AbstractUndoRefinements.java @@ -0,0 +1,39 @@ +package com.abstractundo; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoRefinements { + + @StateRefinement(to="aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from="aliveNotDone(this)", to="aliveDone(this)") + void redo(); + + @StateRefinement(from="aliveDone(this)", to="aliveNotDone(this)") + void undo(); + + @StateRefinement(from="!notAlive(this)", to="notAlive(this)") + void die(); + + + // anything + // boolean canRedo(); + // boolean canUndo(); + + // boolean addEdit(UndoableEdit anEdit); + // String getPresentationName(); + // String getRedoPresentationName(); + // String getUndoPresentationName(); + // boolean isSignificant(); + // boolean replaceEdit(UndoableEdit anEdit); + // String toString(); + + +} diff --git a/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java b/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java new file mode 100644 index 0000000..511fcff --- /dev/null +++ b/examples/demo/src/main/java/com/abstractundo/TestAbstractUndo.java @@ -0,0 +1,28 @@ +package com.abstractundo; + +import javax.swing.undo.AbstractUndoableEdit; + +public class TestAbstractUndo { + + void test1(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.redo(); + } + + void test2(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.undo(); + a.redo(); + a.undo(); + a.undo(); + } + + void test3(){ + AbstractUndoableEdit a = new AbstractUndoableEdit(); + a.undo(); + a.redo(); + a.undo(); + a.die(); + a.redo(); + } +} From cf8465992042861e883dadba6f733d9025f0b9bd Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Feb 2026 14:54:28 +0000 Subject: [PATCH 6/8] mlet example --- .../main/java/com/mlet/MLetRefinements.java | 62 +++++++++++++++++++ .../demo/src/main/java/com/mlet/TestMLet.java | 53 ++++++++++++++++ 2 files changed, 115 insertions(+) create mode 100644 examples/demo/src/main/java/com/mlet/MLetRefinements.java create mode 100644 examples/demo/src/main/java/com/mlet/TestMLet.java diff --git a/examples/demo/src/main/java/com/mlet/MLetRefinements.java b/examples/demo/src/main/java/com/mlet/MLetRefinements.java new file mode 100644 index 0000000..56598f2 --- /dev/null +++ b/examples/demo/src/main/java/com/mlet/MLetRefinements.java @@ -0,0 +1,62 @@ +package com.mlet; + +import java.io.ObjectInput; +import java.io.ObjectOutput; +import java.net.URL; +import java.net.URLStreamHandlerFactory; +import java.util.Set; + +import javax.management.MBeanServer; +import javax.management.ObjectName; +import javax.management.loading.ClassLoaderRepository; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.management.loading.MLet") +@StateSet({"start", "preRegistered", "registered", "preDeregistered"}) +public interface MLetRefinements { + + @StateRefinement(to="start(this)") + void MLet(); + @StateRefinement(to="start(this)") + void MLet(URL[] urls); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, boolean delegateToCLR); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, boolean delegateToCLR); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory); + @StateRefinement(to="start(this)") + void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory, boolean delegateToCLR); + + + @StateRefinement(from="start(this)", to="preRegistered(this)") + ObjectName preRegister(MBeanServer server, ObjectName name); + @StateRefinement(from="preRegistered(this)", to="registered(this)") + void postRegister(Boolean registrationDone); + @StateRefinement(from="registered(this)", to="preDeregistered(this)") + void preDeregister(); + @StateRefinement(from="preDeregistered(this)", to="start(this)") + void postDeregister(); + + @StateRefinement(from="registered(this)") + Set getMBeansFromURL(String url); + @StateRefinement(from="registered(this)") + Set getMBeansFromURL(URL url); + + + // void addURL(String url); + // void addURL(URL url); + // String getLibraryDirectory(); + + // URL[] getURLs(); + // Class loadClass(String name, ClassLoaderRepository clr); + // void readExternal(ObjectInput in); + // void setLibraryDirectory(String libdir); + // void writeExternal(ObjectOutput out); + +} diff --git a/examples/demo/src/main/java/com/mlet/TestMLet.java b/examples/demo/src/main/java/com/mlet/TestMLet.java new file mode 100644 index 0000000..5459d54 --- /dev/null +++ b/examples/demo/src/main/java/com/mlet/TestMLet.java @@ -0,0 +1,53 @@ +package com.mlet; + +import javax.management.loading.MLet; + +public class TestMLet { + + void test1() throws Exception{ + MLet m = new MLet(); + m.preDeregister(); + } + + void test2() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.preDeregister(); + m.postDeregister(); + } + + void test3() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + m.preDeregister(); + m.setLibraryDirectory(null); + m.getMBeansFromURL("null"); + } + + void test4() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + m.preDeregister(); + m.setLibraryDirectory(null); + m.preDeregister(); + } + + + void testGood() throws Exception{ + MLet m = new MLet(); + m.addURL("null"); + m.preRegister(null, null); + m.postRegister(null); + + m.getMBeansFromURL("null"); + + m.preDeregister(); + m.postDeregister(); + } + +} From bd5c86cd4f5f92a17835fac99cf30a372830adb4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Feb 2026 10:25:39 +0000 Subject: [PATCH 7/8] add requiredmodelmbean --- .../RequiredModelMBeanRefinements.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java index 0269fc0..96474a0 100644 --- a/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java +++ b/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java @@ -9,7 +9,7 @@ import liquidjava.specification.StateSet; @ExternalRefinementsFor("javax.management.modelmbean.RequiredModelMBean") -@StateSet({"unregistered", "registered"}) +@StateSet({"unregistered", "preRegistered", "registered", "preUnregistered"}) interface RequiredModelMBeanRefinements{ @StateRefinement(to="unregistered(this)") @@ -18,18 +18,16 @@ interface RequiredModelMBeanRefinements{ @StateRefinement(to="unregistered(this)") void RequiredModelMBean(ModelMBeanInfo mbi); - - @StateRefinement(from="unregistered(this)") + @StateRefinement(from="unregistered(this)", to="preRegistered(this)") ObjectName preRegister(MBeanServer server, ObjectName name); - @StateRefinement(to="registered(this)") + @StateRefinement(from="preRegistered(this)", to="registered(this)") void postRegister(Boolean registrationDone); - - @StateRefinement(from="registered(this)") + @StateRefinement(from="registered(this)", to="preUnregistered(this)") void preDeregister(); - @StateRefinement(from="registered(this)", to="unregistered(this)") + @StateRefinement(from="preUnregistered(this)", to="unregistered(this)") void postDeregister(); @StateRefinement(from="unregistered(this)") From d6019dc69b2d81ff7aba5c775901749ee0b1f300 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 16 Feb 2026 13:46:21 +0000 Subject: [PATCH 8/8] change uuid to use long support in refinements --- .../demo/src/main/java/com/uuid/Test.java | 22 +++++++++++++++---- .../main/java/com/uuid/UUIDRefinements.java | 9 ++++---- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/examples/demo/src/main/java/com/uuid/Test.java b/examples/demo/src/main/java/com/uuid/Test.java index 767ee58..f49d945 100644 --- a/examples/demo/src/main/java/com/uuid/Test.java +++ b/examples/demo/src/main/java/com/uuid/Test.java @@ -5,23 +5,30 @@ public class Test { void test1(){ - UUID t = new UUID(10000L, 0L); + long mostSigBits = 0x0000000000001000; + UUID t = new UUID(mostSigBits, 0L); t.clockSequence(); // possible } void test2(){ - UUID t = UUID.randomUUID(); - t.clockSequence(); + long mostSigBits = 0x0670034000001222L; + UUID t = new UUID(mostSigBits, 0L); + t.clockSequence(); // possible } void test3(){ + UUID t = UUID.randomUUID(); + t.clockSequence(); //error + } + + void test4(){ UUID t = UUID.fromString("smt"); t.clockSequence(); //possible t.node(); t.variant(); } - void test4(){ + void test5(){ byte[] bytes = {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}; UUID t = UUID.nameUUIDFromBytes(bytes); t.variant(); @@ -31,4 +38,11 @@ void test4(){ } + void test6(){ + long mostSigBits = 0x0000000000002000; + UUID t = new UUID(mostSigBits, 0L); + t.clockSequence(); // error + } + + } diff --git a/examples/demo/src/main/java/com/uuid/UUIDRefinements.java b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java index e887790..edf7764 100644 --- a/examples/demo/src/main/java/com/uuid/UUIDRefinements.java +++ b/examples/demo/src/main/java/com/uuid/UUIDRefinements.java @@ -11,15 +11,13 @@ // (v/4096) % 16; @ExternalRefinementsFor("java.util.UUID") -@StateSet({"other", "maybeTime"}) +@StateSet({"other", "maybeTime", "timeBased"}) @RefinementAlias("Version(int v) {v >= 0 && v <= 4}") @RefinementAlias("Variant(int v) {v == 0 || v == 2 || v == 6 || v == 7}") public interface UUIDRefinements { // creation - // would be cool to add - // @StateRefinement(to="((mostSigBits/4096) % 16 == 1) ? timeBased(this) : other(this)") - @StateRefinement(to="maybeTime(this)") + @StateRefinement(to="((mostSigBits/4096) % 16 == 1) ? timeBased(this) : other(this)") void UUID(long mostSigBits, long leastSigBits); //static @@ -36,12 +34,15 @@ public interface UUIDRefinements { @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") int clockSequence(); @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") long timestamp(); @StateRefinement(from="maybeTime(this)") + @StateRefinement(from="timeBased(this)") long node(); @Refinement("Variant(_)")