1 files changed, 15 insertions, 49 deletions
diff --git a/Chalice/refinements/DSW.chalice b/Chalice/refinements/DSW.chalice
index 78a84354..5be52f96 100644
--- a/Chalice/refinements/DSW.chalice
+++ b/Chalice/refinements/DSW.chalice
@@ -5,8 +5,6 @@ class Node {
   var children: seq<Node>;
   var marked: bool;
   ghost var path: seq<Node>;
-
-  var parent: Node;
 }
 
 class DSW0 {
@@ -58,13 +56,7 @@ class DSW0 {
       // termination
       invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked);
     {
-      var n: Node;
-
-      // stupid syntactic trick to make transformers go around call
-      if (true) {
-        call n := PickUnmarked(t.children); 
-      }
-
+      call n := PickUnmarked(t.children); 
       if (n != null) {
         // push             
         stack := [t] ++ stack;          
@@ -95,43 +87,17 @@ class DSW0 {
   }
 }
 
-class DSW1 refines DSW0 {
-  transforms IterativeMark(root: Node, S: seq<Node>) 
-  {
-    assume forall n in S :: n.parent == null;
-    _
-    while 
-      invariant forall n in S :: n !in stack ==> n.parent == null;
-      invariant forall i in [1..|stack|] :: stack[i-1].parent == stack[i];
-    {
-      _
-      if {*}
-      if {
-        // push
-        if (|stack| > 0) {
-          t.parent := stack[0];
-        }
-        *
-      } else {
-        // pop
-        if {*} else {
-          _
-          t.parent := null;
-        }
-      }
-    }
-  }
-
-  transforms PickUnmarked(p: seq<Node>) returns (x: Node)
-  {
-    replaces x by {
-      if (|p| == 0) {
-        x := null;
-      } else if (! p[0].marked) {
-        x := p[0];
-      } else {
-        call x := PickUnmarked(p[1..]);
-      }
-    }
-  }
-}
-\ No newline at end of file
+class DSW1 refines DSW0 {
+  transforms PickUnmarked(p: seq<Node>) returns (x: Node)
+  {
+    replaces x by {
+      if (|p| == 0) {
+        x := null;
+      } else if (! p[0].marked) {
+        x := p[0];
+      } else {
+        call x := PickUnmarked(p[1..]);
+      }
+    }
+  }
+}