1 files changed, 0 insertions, 87 deletions
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice
deleted file mode 100644
index 9ed9f0a9..00000000
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.chalice
+++ /dev/null
@@ -1,87 +0,0 @@
-// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)
-
-// msg tag indicates what the type of the message
-// channel is freed by Getter when it completes
-// ack works, but an assume is needed and negative credits are sent over channels! 
-
-// Conjecture: it is ok to send debit for yourself over yourself.
-// Why: Suppose a channel that allows self-debt is involved in a deadlock. The either that channel is empty, which means there's no difference between the situation with or with self-debt. Or the channel is non-empty. This means that we can make progress by receiving the message stored in the channel! Does this make any sense?
-
-channel C(msg: int, n: Node) where 
-  (msg == 0 || msg == 1 || msg == 2) &&
-  (msg == 0 ==> credit(this, -1)) && // ack
-  (msg == 1 ==> n != null && acc(n.next) && acc(n.mu) && credit(this, -1)) && // cell
-  (msg == 2 ==> acc(this.mu, 50)); // done
-  
-
-class Node {
-  var next: Node;
-  
-  function length(): int
-    requires this.list;
-  {
-    unfolding this.list in 1 + (next == null ? 0 : next.length())
-  }
-  
-  predicate list {
-    acc(next) && acc(mu) && (next != null ==> next.list)
-  }
-}
-
-class Program {
-  method Putter(e: C, x0: Node) 
-    requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));
-  {
-    var x: Node := x0;
-    var t: Node;
-    
-    while(x != null) 
-      invariant (x != null ==> x.list) && acc(e.mu, 50) && credit(e, - 1);
-    {
-      unfold x.list;
-      t := x.next;
-      send e(1, x);
-      x := t;
-      var ack;
-      assume waitlevel << e.mu; // Chalice should be able to figure this out itself
-      receive ack, t := e;
-      if(ack != 2) { assume false; /* abort */ }
-    }
-    send e(2, null);
-  }  
-  
-  method Getter(f: C) 
-    requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu;
-  {
-    var x: Node := null;
-    var msg := 1;
-    while(msg != 0)
-      invariant msg == 0 || msg == 1;
-      invariant acc(f.mu, 50) && waitlevel << f.mu && (credit(f, 1));
-    {
-      assert msg == 1
-      receive msg, x := f;
-      
-      if(msg == 1) {
-        free x;
-      }
-      send f(0, null);
-      if(msg == 2) { assume false; /* abort */ }
-    }
-    receive msg, x := f;
-    if (msg != 2) { assume false; /* abort */ }
-    free f; // close the channel
-  } 
-
-  method Main(x: Node)
-    requires x != null;
-    requires x.list;
-  {
-    var e := new C;
-    fork Putter(e, x);
-    fork Getter(e);
-  }  
-}
-
-
-