diff options
Diffstat (limited to 'Chalice/examples/prog4.chalice')
-rw-r--r-- | Chalice/examples/prog4.chalice | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Chalice/examples/prog4.chalice b/Chalice/examples/prog4.chalice index 655c5815..bc6aef99 100644 --- a/Chalice/examples/prog4.chalice +++ b/Chalice/examples/prog4.chalice @@ -22,7 +22,7 @@ class LoopTargets { acquire t
var s := true
while (s)
- invariant acc(t.mu) && maxlock == t.mu
+ invariant acc(t.mu) && waitlevel == t.mu
{
release t // error: loop invariant does not say holds(t) (414)
acquire t
@@ -37,7 +37,7 @@ class LoopTargets { var s := true
while (s)
invariant rd(t.mu)
- invariant holds(t) && maxlock == t.mu
+ invariant holds(t) && waitlevel == t.mu
{
release t
acquire t
|