1 files changed, 35 insertions, 0 deletions
diff --git a/Chalice/tests/examples/OwickiGries.chalice b/Chalice/tests/examples/OwickiGries.chalice
new file mode 100644
index 00000000..f466b58a
--- /dev/null
+++ b/Chalice/tests/examples/OwickiGries.chalice
@@ -0,0 +1,35 @@
+class OwickiGries {
+  var counter: int
+  ghost var c0: int
+  ghost var c1: int
+  invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1
+
+  method Main() {
+    var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 }
+    share og
+
+    fork tk0 := og.Worker(false)
+    fork tk1 := og.Worker(true)
+    join tk0; join tk1
+
+    acquire og; unshare og
+    assert og.counter == 2
+  }
+
+  method Worker(b: bool)
+    requires rd(mu) && waitlevel << mu
+    requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50))
+    ensures rd(mu)
+    ensures !b ==> acc(c0,50) && c0 == old(c0) + 1
+    ensures b ==> acc(c1,50) && c1 == old(c1) + 1
+  {
+    lock (this) {
+      counter := counter + 1
+      if (!b) {
+        c0 := c0 + 1
+      } else {
+        c1 := c1 + 1
+      }
+    }
+  }
+}