diff options
Diffstat (limited to 'Chalice/examples/OwickiGries.chalice')
| -rw-r--r-- | Chalice/examples/OwickiGries.chalice | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/examples/OwickiGries.chalice index 63f029e8..f466b58a 100644 --- a/Chalice/examples/OwickiGries.chalice +++ b/Chalice/examples/OwickiGries.chalice @@ -17,7 +17,7 @@ class OwickiGries { }
method Worker(b: bool)
- requires rd(mu) && maxlock << mu
+ 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
|