required model and undomanager

CatarinaGamboa · CatarinaGamboa · commit e1643c483634 · 2026-01-29T00:23:34.000Z
diff --git a/examples/demo/src/main/java/com/requiredmodelbean/RequiredModelMBeanRefinements.java 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();
+
+
+
+}
diff --git a/examples/demo/src/main/java/com/requiredmodelbean/TestRequiredModel.java 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
@@ -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
+    }
+}
diff --git a/examples/demo/src/main/java/com/undomanager/UndoManagerRefinements.java 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();
+
+}
