Chalice:

* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration

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