Refactor and fix environments in modelling.

Examples/PassGH/arc.cvf

@@ -19,9 +19,8 @@ thread Int c, pval;
 
 method init() {
   {| emp |}
-    // TODO: broken local command syntax.
-    ret = %{new ArcNode};
-    <%{[|ret|].count := 1}>;
+    <{ ret = %{new ArcNode};
+       %{[|ret|].count := 1}; }>;
   {| arc(ret) |}
 }
 
@@ -33,16 +32,14 @@ method clone(ArcNode x) {
 
 method print(ArcNode x) {
   {| arc(x) |}
-    // TODO: broken local command syntax.
-    pval = %{ [|x|].val };
+    <pval = %{ [|x|].val }>;
   {| arc(x) |}
 }
 
 method drop(ArcNode x) {
   {| arc(x) |}
-    // TODO: broken local command syntax.
-    c = %{ [|x|].count };
-    <%{ [|x|].count := [|x|].count - 1 }>;
+    <{ c = %{ [|x|].count };
+       %{ [|x|].count := [|x|].count - 1 }; }>;
   {| countCopy(x, c) |}
     if (c == 1) {
       {| countCopy(x, 1) |}

Examples/PassGH/clhLock.cvf

@@ -23,7 +23,7 @@ method lock(Node mynode) {
   {| queued(mynode, mypred) |}
     do {
       {| queued(mynode, mypred) |}
-        test = %{ [|mypred|].lock };
+        <test = %{ [|mypred|].lock }>;
       {| if test then queued(mynode, mypred) else holdLock(mynode, mypred) |}
     } while (test);
   {| holdLock(mynode, mypred) |}

Examples/PassGH/lclist.cvf

@@ -21,11 +21,11 @@ method deleteVal(int v) {
   {| wf(v) * isHead(prev) |}
    <{ %{ waitLock([|prev|]); takeLock([|prev|]) }; }>;
   {| wf(v) * has1LockAnon(prev) * isHead(prev) |}
-   curr = %{ [|prev|].next };
+   < curr = %{ [|prev|].next } >;
   {| wf(v) * has1Lock(prev, curr) * isHead(prev) |}
    <{ %{ waitLock([|curr|]); takeLock([|curr|]) }; }>;
   {| wf(v) * has2Lock(prev, curr) |}
-   cv = %{ [|curr|].val };
+   < cv = %{ [|curr|].val } >;
   {| wf(v) * has2Lock(prev,curr) * isVal(curr, cv) |}
     while (cv < v ) {
       {| wf(v) * wf(cv) * has2Lock(prev, curr) * isVal(curr, cv) |}

Examples/PassGH/spinLock.cvf

@@ -13,7 +13,7 @@ view newLock(Lock x), holdLock(Lock x), isLock(Lock x);
 
 method newLock() {
   {| emp |}
-    ret = %{new Lock};
+    <ret = %{new Lock}>;
   {| newLock(ret) |}
     <%{[|ret|].lock := false}>;
   {| isLock(ret) |}
@@ -25,7 +25,7 @@ method lock(Lock x) {
       {| isLock(x) |}
         test = false;
       {| if test == false then isLock(x) else False() |}
-        test = %{ CAS_to_true([|x|]) };
+        <test = %{ CAS_to_true([|x|]) }>;
       {| if test == false then isLock(x) else holdLock(x) |}
     } while (test == false);
   {| holdLock(x) |}

Examples/PassGH/ticketLock.cvf

@@ -13,20 +13,20 @@ view newLock(Lock x), holdTick(Lock x, int t), holdLock(Lock x), isLock(Lock x);
 
 method newLock() {
   {| emp |}
-    ret = %{new Lock};
+    <ret = %{new Lock}>;
   {| newLock(ret) |} 
     <%{[|ret|].ticket := 0; [|ret|].serving := 0}>;
   {| isLock(ret) |}
 }
 
 method lock(Lock x) {
   {| isLock(x) |}
-    t = %{ [|x|].ticket };
-    <%{ [|x|].ticket := [|x|].ticket + 1 }>;
+    <{ t = %{ [|x|].ticket };
+       %{ [|x|].ticket := [|x|].ticket + 1 }; }>;
   {| holdTick(x, t) |}
     do {
       {| holdTick(x, t) |}
-        s = %{ [|x|].serving };
+        <s = %{ [|x|].serving }>;
       {| if s == t then holdLock(x) else holdTick(x, t) |}
     } while (s != t);
   {| holdLock(x) |}