diff --git a/examples/demo/src/main/java/com/example/awt/PopupMenu.java b/examples/demo/src/main/java/com/example/awt/PopupMenu.java
new file mode 100644
index 0000000..2214ecc
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/awt/PopupMenu.java
@@ -0,0 +1,18 @@
+package com.example.awt;
+
+import java.awt.Component;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+
+
+
+@ExternalRefinementsFor("java.awt.PopupMenu")
+@Ghost("boolean isShowing")
+public interface PopupMenu {
+	
+    /* Should also include hierarchy, but we do not support sets. */
+    public void show(@Refinement("isShowing(origin) && isShowing(this)") Component origin, int x, int y);
+
+}
diff --git a/examples/demo/src/main/java/com/example/awt/Window.java b/examples/demo/src/main/java/com/example/awt/Window.java
new file mode 100644
index 0000000..3aaf5ca
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/awt/Window.java
@@ -0,0 +1,67 @@
+package com.example.awt;
+
+import java.awt.AWTException;
+import java.awt.BufferCapabilities;
+import java.awt.Frame;
+import java.awt.GraphicsConfiguration;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+
+
+@ExternalRefinementsFor("java.awt.Window")
+@StateSet({"invisible", "visible"})
+@StateSet({"displayable", "notDisplayable"})
+@StateSet({"notFullscreen", "fullscreen"})
+@StateSet({"decorated", "undecorated"})
+public interface Window {
+    @StateRefinement(to="invisible(this)")
+    @StateRefinement(to="notDisplayable(this)")
+    @StateRefinement(to="fullscreen(this)")
+    @StateRefinement(to="undecorated(this)")
+    void Window(Frame owner); 
+
+    @StateRefinement(to="invisible(this)")
+    @StateRefinement(to="notDisplayable(this)")
+    @StateRefinement(to="fullscreen(this)")
+    @StateRefinement(to="undecorated(this)")
+    void Window(Window owner); 
+
+    @StateRefinement(to="invisible(this)")
+    @StateRefinement(to="notDisplayable(this)")
+    @StateRefinement(to="fullscreen(this)")
+    @StateRefinement(to="undecorated(this)")
+    void Window(Window owner, GraphicsConfiguration gc); 
+    
+    @StateRefinement(from="notDisplayable(this)")
+    void setType(java.awt.Window.Type type);
+
+    @StateRefinement(to="displayable(this)")
+    public void addNotify();
+
+    @StateRefinement(to="displayable(this)")
+    public void pack();
+
+    // Check this
+    @StateRefinement(to="(visible ? displayable(this) : true) && (visible ? visible(this) : invisible(this))")
+    public void setVisible(boolean visible);
+
+    @StateRefinement(from="displayable(this)", to="notDisplayable(this) && invisible(this)")
+    public void dispose();
+
+    @StateRefinement(from="displayable(this)")
+    public void createBufferStrategy(@Refinement("numBuffers >= 1") int numBuffers);
+
+    public void createBufferStrategy(@Refinement("numBuffers >= 1") int numBuffers, BufferCapabilities caps) throws AWTException;
+
+    // Check this, not intuitive from javadoc
+    @StateRefinement(from="undecorated(this) || notFullscreen(this) || opacity == 1.0")
+    public void setOpacity(@Refinement("opacity >= 0.0 && opacity <= 1.0") float opacity);
+
+
+    // TODO: Requires NULL support and constants
+    // public void setShape(Shape shape);
+}
diff --git a/examples/demo/src/main/java/com/example/simple/SimpleExample.java b/examples/demo/src/main/java/com/example/simple/SimpleExample.java
index 160f23e..a9b36f7 100644
--- a/examples/demo/src/main/java/com/example/simple/SimpleExample.java
+++ b/examples/demo/src/main/java/com/example/simple/SimpleExample.java
@@ -1,4 +1,5 @@
 package com.example.simple;
+
 import liquidjava.specification.Refinement;
 
 public class SimpleExample {
diff --git a/examples/demo/src/main/java/com/example/xml/TransformerException.java b/examples/demo/src/main/java/com/example/xml/TransformerException.java
new file mode 100644
index 0000000..63330da
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/xml/TransformerException.java
@@ -0,0 +1,47 @@
+package com.example.xml;
+
+import javax.xml.transform.SourceLocator;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+
+/*
+State machine:
+
+withCause (Constructors with throwable)
+
+^ initCause
+
+withoutCause (other constructors)
+
+*/
+
+@ExternalRefinementsFor("javax.xml.transform.TransformerException")
+@StateSet({"withoutCause", "withCause"})
+public interface TransformerException {
+	
+	@StateRefinement(to="withoutCause(this)")
+	public void TransformerException(String msg);
+
+    @StateRefinement(to="withoutCause(this)")
+	public void TransformerException(String msg, SourceLocator locator);
+
+    @StateRefinement(to="withCause(this)")
+	public void TransformerException(Throwable cause);
+	
+    @StateRefinement(to="withCause(this)")
+	public void TransformerException(String message, Throwable cause);
+
+    @StateRefinement(to="withCause(this)")
+	public void TransformerException(String message, SourceLocator locator, Throwable cause);
+
+    @StateRefinement(from="withoutCause(this)", to="withCause(this)")
+    public Throwable initCause(Throwable cause);
+
+    // This would be useful if we wanted to get rid of nulls.
+    // Same for location
+	//@StateRefinement(from="withCause(this)")
+	public Throwable getCause();
+}
diff --git a/examples/demo/src/main/java/com/example/zip/ZipFile.java b/examples/demo/src/main/java/com/example/zip/ZipFile.java
new file mode 100644
index 0000000..099aad5
--- /dev/null
+++ b/examples/demo/src/main/java/com/example/zip/ZipFile.java
@@ -0,0 +1,60 @@
+package com.example.zip;
+
+import java.io.File;
+import java.io.InputStream;
+import java.nio.charset.Charset;
+import java.util.Enumeration;
+import java.util.zip.ZipEntry;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+
+/*
+State machine:
+
+closed
+
+^ close
+
+opened.  @ getEntry, getIS, stream, entries
+
+*/
+
+@ExternalRefinementsFor("java.util.zip.ZipFile")
+@StateSet({"opened", "closed"})
+public interface ZipFile {
+	
+	@StateRefinement(to="opened(this)")
+	public void ZipFile(File file);
+
+    @StateRefinement(to="opened(this)")
+	public void ZipFile(File file, int mode);
+
+    @StateRefinement(to="opened(this)")
+	public void ZipFile(File file, int mode, Charset cs);
+
+    @StateRefinement(to="opened(this)")
+	public void ZipFile(File file, Charset cs);
+
+    @StateRefinement(to="opened(this)")
+	public void ZipFile(String name);
+
+    @StateRefinement(to="opened(this)")
+	public void ZipFile(String name, Charset cs);
+
+    @StateRefinement(from="opened(this)", to="closed(this)")
+    public void close();
+
+    @StateRefinement(from="opened(this)")
+    public Enumeration<? extends ZipEntry> entries();
+
+    @StateRefinement(from="opened(this)")
+    public ZipEntry getEntry(String name);
+
+    @StateRefinement(from="opened(this)")
+    public InputStream getInputStream(ZipEntry e);
+
+
+}
diff --git a/examples/demo/src/test/java/com/example/AppTest.java b/examples/demo/src/test/java/com/example/AppTest.java
index 22a94ca..d473de3 100644
--- a/examples/demo/src/test/java/com/example/AppTest.java
+++ b/examples/demo/src/test/java/com/example/AppTest.java
@@ -1,7 +1,6 @@
 package com.example;
 
 import static org.junit.Assert.assertTrue;
-
 import org.junit.Test;
 
 /**