1 files changed, 0 insertions, 93 deletions
diff --git a/Chalice/tests/examples/dining-philosophers.chalice b/Chalice/tests/examples/dining-philosophers.chalice
deleted file mode 100644
index f4a7d1a6..00000000
--- a/Chalice/tests/examples/dining-philosophers.chalice
+++ /dev/null
@@ -1,93 +0,0 @@
-class Philosopher module Philosophers {
-  var left: Fork;
-  var right: Fork;
-  
-  method init(f1: Fork, f2: Fork) 
-    requires f1!=null && f2!=null;
-    requires acc(this.*);
-    ensures valid;
-    ensures getLeft()==f1 && getRight()==f2;
-  {
-    left := f1;
-    right := f2;
-    fold valid;
-  }
-
-  method run()
-    requires valid;
-    requires acc(getLeft().mu, 10);
-    requires acc(getRight().mu, 10);
-    requires waitlevel << getLeft().mu;
-    requires waitlevel << getRight().mu;
-    requires getLeft().mu << getRight().mu;
-  {
-    while(true)
-      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && waitlevel << getLeft().mu && waitlevel << getRight().mu && getLeft().mu << getRight().mu;
-    {
-      unfold valid;
-      acquire left;
-      acquire right;
-      //eat
-      release left;
-      release right;
-      fold valid;
-    }
-  }
-
-  function getLeft(): Fork 
-    requires valid;
-    ensures result!=null;
-  {
-    unfolding valid in left
-  }
-
-  function getRight(): Fork 
-    requires valid;
-    ensures result!=null;
-  {
-    unfolding valid in right
-  }
-
-  predicate valid {
-    acc(left) && acc(right) && left!=null && right!=null
-  }
-}
-
-class Fork module Dining {
-  invariant true;
-}
-
-class Program module Main {
-  method main(){
-    // create forks
-    var f1 := new Fork;
-    var f2 := new Fork;
-    var f3 := new Fork;
-
-    share f1;
-    share f2 above f1;
-    share f3 above f1, f2;
-
-    // create philosophers
-    var aristotle := new Philosopher;
-    call aristotle.init(f1, f2);
-
-    var plato := new Philosopher;
-    call plato.init(f2, f3);
-
-    var kant := new Philosopher;
-    call kant.init(f1, f3);
-    
-    assert f2.mu << f3.mu;
-
-    // start eating
-    fork tk0 := aristotle.run();
-    fork tk1 := plato.run();
-    fork tk2 := kant.run();
-
-    // everyone's done
-    join tk0;
-    join tk1;
-    join tk2;
-  }
-}
-\ No newline at end of file