1 files changed, 120 insertions, 0 deletions
diff --git a/Chalice/tests/refinements/original/DSW10.chalice b/Chalice/tests/refinements/original/DSW10.chalice
new file mode 100644
index 00000000..3bf70eeb
--- /dev/null
+++ b/Chalice/tests/refinements/original/DSW10.chalice
@@ -0,0 +1,120 @@
+// Schorr-Waite algorithm in Chalice
+// (see Test/dafny1/SchorrWaite.dfy)
+
+// Arbitrary number of children
+// Added visited field to refine non-det choice with a conditional
+// Added a client
+class Node {
+  var children: seq<Node>;
+  var marked: bool;
+  var visited: int;
+  ghost var path: seq<Node>;
+}
+
+class Main {
+  method Test() 
+  {
+    var a := new Node {marked := false, visited := 0};
+    var b := new Node {marked := false, visited := 0};
+    var c := new Node {marked := false, visited := 0};
+    var d := new Node {marked := false, visited := 0};
+    a.children := [b];
+    b.children := [c,a];
+    c.children := [b];
+    d.children := [a,b,c];
+    // a <-> b <-> c
+    //  ^ \  ^  / ^
+    //       d    
+    assert [a,b,c,d][0] == a; // root is in sequence
+    call IterativeMark(a, [a,b,c,d]);
+    assert a.marked;
+    assert a.children[0] == b; // b should be marked
+    assert b.marked;
+    assert b.children[0] == c; // c should be marked
+    assert c.marked;
+    assert !d.marked;
+  }
+
+  function Reachable(to: Node, p:seq<Node>, from: Node): bool
+    requires acc(p[*].children);
+  {
+    |p| == 0 ? to == from :
+      (p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from))
+  }
+  
+  method IterativeMark(root: Node, S: seq<Node>)
+    requires acc(S[*].*);
+    requires root in S;
+    requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S); 
+    requires forall n in S :: ! n.marked;
+    requires forall n in S :: n.visited == 0;
+    ensures acc(S[*].*);
+    // graph structure is the same
+    ensures forall n in S :: n.children == old(n.children);
+    ensures forall n in S :: n.visited == 0;
+    // all nodes reachable from root are marked
+    ensures root.marked;
+    ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked);      
+    // all marked nodes are reachable from root
+    ensures forall n in S :: n.marked ==> 
+      (forall m in n.path :: m in S) && 
+      Reachable(n, n.path, root);
+  {
+    var t:Node := root;
+    t.marked := true;
+    var stack: seq<Node> := [];
+    t.path := stack;
+
+    var stop := false;
+    while(!stop)
+      invariant acc(S[*].*);
+      invariant root.marked && t in S && t.marked && t !in stack;
+      // no duplicates in the stack
+      invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j];    
+      // stack well-formed
+      invariant forall n in stack :: n in S;
+      invariant forall n in S :: n in stack || n == t ==>
+        n.marked &&
+        0 <= n.visited && n.visited <= |n.children| &&
+        (forall i in [0..n.visited] :: n.children[i] in S && n.children[i].marked);
+      invariant forall n in stack :: n.visited < |n.children|;	  
+      // stack is linked
+      invariant forall i in [1..|stack|] :: stack[i-1] == stack[i].children[stack[i].visited];
+      invariant 0 < |stack| ==> t == stack[0].children[stack[0].visited];
+      // goal
+      invariant forall n in S :: n.marked && n !in stack && n != t ==> 
+        (forall ch in n.children :: ch in S && ch.marked);
+      invariant forall n in S :: n.marked ==> 
+        (forall m in n.path :: m in S) && 
+        Reachable(n, n.path, root);
+      // preservation
+      invariant forall n in S :: n !in stack && n != t ==> n.visited == old(n.visited);
+      invariant forall n in S :: n.children == old(n.children);
+      // termination
+      invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked) && t.visited == 0;
+    {  
+      if (t.visited == |t.children|) {
+        // pop
+        t.visited := 0;
+        if (|stack| == 0) {
+          stop := true;
+        } else {
+          t := stack[0];
+          stack := stack[1..];
+          t.visited := t.visited + 1;
+        }
+      } else if (t.children[t.visited].marked) {
+        // skip
+        t.visited := t.visited + 1;
+      } else {
+        // push
+        ghost var oldt:Node := t;
+        stack := [t] ++ stack;        
+        t := t.children[t.visited];        
+        t.path := [oldt] ++ oldt.path; // TODO: in fact, this is stack        
+        t.marked := true;
+        assert Reachable(oldt, oldt.path, root); // needed for limited function
+      }
+    }
+  }
+}