1 files changed, 93 insertions, 0 deletions
diff --git a/Chalice/examples/dining-philosophers.chalice b/Chalice/examples/dining-philosophers.chalice
new file mode 100644
index 00000000..6a67174c
--- /dev/null
+++ b/Chalice/examples/dining-philosophers.chalice
@@ -0,0 +1,93 @@
+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 maxlock << getLeft().mu;
+    requires maxlock << getRight().mu;
+    requires getLeft().mu << getRight().mu;
+  {
+    while(true)
+      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && maxlock << getLeft().mu && maxlock << 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