From 899d1f3d30abf3343b88c0e4c6e44db130c6345b Mon Sep 17 00:00:00 2001
From: "peter mueller peter.mueller@inf.ethz.ch" <unknown>
Date: Thu, 29 Sep 2011 19:32:48 +0200
Subject: Dafny: Added TreeBarrier as a test case

---
 Test/dafny2/Answer          |   6 ++
 Test/dafny2/TreeBarrier.dfy | 143 ++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny2/runtest.bat     |   2 +-
 3 files changed, 150 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny2/TreeBarrier.dfy

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 3eb32da8..bef70cf1 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -1,4 +1,10 @@
 
 -------------------- SnapshotableTrees.dfy --------------------
+Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft.
 
 Dafny program verifier finished with 37 verified, 0 errors
+
+-------------------- TreeBarrier.dfy --------------------
+Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft.
+
+Dafny program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy
new file mode 100644
index 00000000..f4cc25d2
--- /dev/null
+++ b/Test/dafny2/TreeBarrier.dfy
@@ -0,0 +1,143 @@
+class Node {
+  var left: Node;
+  var right: Node;
+  var parent: Node;
+  var anc: set<Node>;
+  var desc: set<Node>;
+  var sense: bool;
+  var pc: int;
+
+
+  function validDown(): bool
+    reads this, desc;    
+  {
+    this !in desc &&
+    null !in desc &&
+    left != right &&  // not needed, but speeds up verification
+
+    (right != null ==> right in desc && left !in right.desc) &&
+
+    (left != null ==> 
+      left in desc && 
+      (right != null ==> desc == {left,right} + left.desc + right.desc)  &&
+      (right == null ==> desc == {left} + left.desc)  &&
+      left.validDown()) &&
+    (left == null ==> 
+      (right != null ==> desc == {right} + right.desc)  &&
+      (right == null ==> desc == {})) &&
+
+    (right != null ==> right.validDown()) &&
+
+    (blocked() ==> forall m :: m in desc ==> m.blocked()) &&
+    (after() ==> forall m :: m in desc ==> m.blocked() || m.after())
+//    (left != null && right != null ==> left.desc !! right.desc)  // not needed
+  }
+
+
+
+
+  function  validUp(): bool
+    reads this, anc;    
+  {
+    this !in anc &&
+    null !in anc &&
+    (parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) &&
+    (parent == null ==> anc == {}) &&
+    (after() ==> forall m :: m in anc ==> m.after())
+  }
+
+  function valid(): bool
+    reads this, desc, anc;
+  { validUp() && validDown() && desc !! anc }
+
+  function before(): bool
+    reads this;
+  { !sense && pc <= 2 }
+
+  function blocked(): bool
+    reads this;
+  { sense }
+
+  function after(): bool
+    reads this;
+  { !sense && 3 <= pc }
+
+
+  method barrier()
+    requires valid();
+    requires before();
+    modifies this, left, right;
+  {
+
+//A
+    pc := 1;
+    if(left != null) {
+      while(!left.sense) 
+        modifies left;
+        invariant validDown(); // this seems necessary to get the necessary unfolding of functions
+        invariant valid();
+        decreases *;  // to by-pass termination checking for this loop
+      {
+        // this loop body is supposed to model what the "left" thread
+        // might do to its node. This body models a transition from
+        // "before" to "blocked" by setting sense to true. A transition
+        // all the way to "after" is not permitted; this would require
+        // a change of pc.
+        // We assume that "left" preserves the validity of its subtree,
+        // which means in particular that it goes to "blocked" only if
+        // all its descendants are already blocked.
+        left.sense := *; 
+        assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked();
+      }  
+    }
+    if(right != null) {
+      while(!right.sense) 
+        modifies right;
+        invariant validDown(); // this seems necessary to get the necessary unfolding of functions
+        invariant valid();
+        decreases *;  // to by-pass termination checking for this loop
+      {
+        // analogous to the previous loop
+        right.sense := *; 
+        assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked();
+      }  
+    }
+
+//B
+    pc := 2;
+    if(parent != null) {
+      sense := true; 
+    }
+//C
+    pc := 3;
+    while(sense)
+        modifies this;
+        invariant validUp(); // this seems necessary to get the necessary unfolding of functions
+        invariant valid();
+        invariant left == old(left);
+        invariant right == old(right);
+        invariant sense ==> parent != null;
+        decreases *;  // to by-pass termination checking for this loop
+    {
+      // this loop body is supposed to model what the "parent" thread
+      // might do to its node. The body models a transition from
+      // "blocked" to "after" by setting sense to false.
+      // We assume that "parent" initiates this transition only
+      // after it went to state "after" itself.
+      sense := *;
+      assume !sense ==> parent.after();
+    }
+//D
+    pc := 4;
+    if(left != null) {
+      left.sense := false;
+    }
+//E
+    pc := 5;
+    if(right != null) {
+      right.sense := false;
+    }
+//F
+    pc := 6;
+  }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index a58b03c6..62b0b6fe 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 
-for %%f in (SnapshotableTrees.dfy) do (
+for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy) do (
   echo.
   echo -------------------- %%f --------------------
 
-- 
cgit v1.2.3