Add MLet Refinements

rcosta358 · rcosta358 · commit 2f1213174c5d · 2026-02-02T13:55:19.000Z
diff --git a/examples/demo/src/main/java/com/mLet/MLetRefinements.java b/examples/demo/src/main/java/com/mLet/MLetRefinements.java
@@ -0,0 +1,51 @@
+package com.mLet;
+
+import java.net.URL;
+import java.net.URLStreamHandlerFactory;
+import java.util.Set;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("javax.management.loading.MLet")
+@StateSet({"unregistered", "registered"})
+public interface MLetRefinements {
+    
+    @StateRefinement(to="unregistered(this)")
+    public void MLet();
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls);
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls, ClassLoader parent);
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory);
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls, boolean delegateToCLR);
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls, ClassLoader parent, boolean delegateToCLR);
+
+    @StateRefinement(to="unregistered(this)")
+    public void MLet(URL[] urls, ClassLoader parent, URLStreamHandlerFactory factory, boolean delegateToCLR);
+
+    // cant write "registrationDone ? registered(this) : unregistered(this)"" because it uses Boolean instead of boolean
+    @StateRefinement(from="unregistered(this)", to="registered(this)") 
+    public void postRegister(Boolean registrationDone);
+
+    @StateRefinement(from="registered(this)")
+    public void preDeregister();
+
+    @StateRefinement(from="registered(this)", to="unregistered(this)")
+    public void postDeregister();
+
+    @StateRefinement(from="registered(this)")
+    public Set<Object> getMBeansFromURL(URL url);
+
+    @StateRefinement(from="registered(this)")
+    public Set<Object> getMBeansFromURL(String url);
+}
diff --git a/examples/demo/src/main/java/com/mLet/MLetTests.java b/examples/demo/src/main/java/com/mLet/MLetTests.java
@@ -0,0 +1,32 @@
+package com.mLet;
+
+import javax.management.loading.MLet;
+
+public class MLetTests {
+    
+    public void testOk() throws Exception {
+        MLet mlet = new MLet();
+        mlet.addURL("");
+        mlet.preRegister(null, null);
+        mlet.postRegister(true);
+        mlet.preDeregister();
+        mlet.postDeregister();
+    }
+
+    public void testNotRegistering() throws Exception {
+        MLet mlet = new MLet();
+        mlet.addURL("");
+        mlet.preRegister(null, null);
+        mlet.getMBeansFromURL(""); // error
+    }
+
+    public void testUnregisterTwice() throws Exception {
+        MLet mlet = new MLet();
+        mlet.addURL("");
+        mlet.preRegister(null, null);
+        mlet.postRegister(true);
+        mlet.preDeregister();
+        mlet.postDeregister();
+        mlet.postDeregister(); // error
+    }
+}
