From 3d16cf315f87829d3581cb1ae498f08583481b9e Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Tue, 3 Aug 2010 06:31:52 +0000
Subject: Chalice: abstract Shorr-Waite algorithm verified

---
 Chalice/examples/refinement/DSW3.chalice | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/Chalice/examples/refinement/DSW3.chalice b/Chalice/examples/refinement/DSW3.chalice
index f5eb975b..dbf161cd 100644
--- a/Chalice/examples/refinement/DSW3.chalice
+++ b/Chalice/examples/refinement/DSW3.chalice
@@ -6,7 +6,7 @@
 // Added parent pointer p (stack remains)
 // Note: the challenge is to update children field of nodes on stack so that we can recover 
 //  parent pointer in pop operation
-// Add parent field to Node and made stack ghost (verification time , limited functions)
+// Add parent field to Node and made stack ghost (verification time 80s, limited functions)
 class Node {
   var children: seq<Node>;
   var marked: bool;
@@ -78,20 +78,17 @@ class Main {
         t := n;
         t.marked := true;
         assert Reachable(t.path[0], t.path[1..], root); // limited function
-        assert Reachable(t, t.path, root);
         assert forall x in S :: x.marked ==> Reachable(x, x.path, root);
         assume forall x in S :: x.marked ==> Reachable(x, x.path, root);
-      } else {              
+      } else {    
         // pop
         if (p == null) {
           stop := true;
-        } else {                 
-          t.parent := null;   
+        } else {                          
           t := p;
-          p := p.parent;
-          stack := stack[1..];  
-          assert t !in stack;
-          assert 0 < |stack| ==> p == stack[0];
+          p := t.parent;
+          t.parent := null;
+          stack := stack[1..];
         }
       }
     }
@@ -104,6 +101,6 @@ class Main {
     ensures x != null ==> x in p && ! x.marked;
     ensures x == null ==> (forall n in p :: n.marked);
   {
-    assume false; // magic!
+    assume false;
   }
 }
-- 
cgit v1.2.3