Fix testfile

src/concurrency/flow/positive/counter.imp

@@ -1,43 +1,77 @@
-incr(x, max, l) {
+// Increment `x` while satisfying `x <= max`
+incr(x, min_max, l) {
     acq(l);
-    assert(*x <= max);
+    check(x, min_max);
+    let (_, max) = min_max in
     if *x < max then {
         x := *x + 1;
-        assert(*x <= max);
+        check(x, min_max);
         rel(l);
     } else {
         rel(l);
-        incr(x, max, l);
+        incr(x, min_max, l);
+    }
+}
+
+// Increment `x` nondeterminstic times
+repeat_incr(x, min_max, l) {
+    if _ then ()
+    else {
+        incr(x, min_max, l);
+        repeat_incr(x, min_max, l)
     }
 }
 
-decr(x, min, l) {
+// Decrement `x` while satisfying `min <= x`
+decr(x, min_max, l) {
     acq(l);
-    assert(min <= *x);
+    check(x, min_max);
+    let (min, _) = min_max in
     if min < *x then {
         x := *x - 1;
-        assert(min <= *x);
+        check(x, min_max);
         rel(l);
     } else {
         rel(l);
-        decr(x, min, l);
+        decr(x, min_max, l);
+    }
+}
+
+// Decrement `x` nondeterminstic times
+repeat_decr(x, min_max, l) {
+    if _ then ()
+    else {
+        decr(x, min_max, l);
+        repeat_decr(x, min_max, l)
     }
 }
 
+check(x, min_max) {
+    let (min, max) = min_max in {
+        assert(min <= *x);
+        assert(*x <= max);
+    }
+}
+
+// Limited Counter:
+// Repeat increment and decrement the counter nondeterministic times
+// while keeping the value between `min` and `max`.
 {
-    let min = 0 in
-    let max = 2 in
-    let x = mkref min in
-    let l = newlock() in
-    let t = fork({
-        decr(x, min, l);
-        decr(x, min, l);
-        decr(x, min, l);
-    }) in {
-        incr(x, max, l);
-        incr(x, max, l);
-        incr(x, max, l);
-        wait(t);
-        freelock(l)
+    let min = (_: ~ >= 0) in
+    let max = (_: ~ >= min) in
+    let min_max = (min, max) in
+    let counter = mkref min in {
+        check(counter, min_max);
+        let l = newlock() in
+        let t = fork({
+            repeat_decr(counter, min_max, l);
+        }) in {
+            repeat_incr(counter, min_max, l);
+
+            wait(t);
+            freelock(l);
+
+            check(counter, min_max);
+        }
     }
 }

src/concurrency/flow/positive/counter2.imp

@@ -0,0 +1,43 @@
+incr(x, max, l) {
+    acq(l);
+    assert(*x <= max);
+    if *x < max then {
+        x := *x + 1;
+        assert(*x <= max);
+        rel(l);
+    } else {
+        rel(l);
+        incr(x, max, l);
+    }
+}
+
+decr(x, min, l) {
+    acq(l);
+    assert(min <= *x);
+    if min < *x then {
+        x := *x - 1;
+        assert(min <= *x);
+        rel(l);
+    } else {
+        rel(l);
+        decr(x, min, l);
+    }
+}
+
+{
+    let min = 0 in
+    let max = 2 in
+    let x = mkref min in
+    let l = newlock() in
+    let t = fork({
+        decr(x, min, l);
+        decr(x, min, l);
+        decr(x, min, l);
+    }) in {
+        incr(x, max, l);
+        incr(x, max, l);
+        incr(x, max, l);
+        wait(t);
+        freelock(l)
+    }
+}

src/concurrency/flow/positive/queue.imp

@@ -98,19 +98,32 @@ pop(q, l) {
   }
 }
 
+repeat_push(q, l) {
+  if _ then ()
+  else {
+      push(q, _, l);
+      repeat_push(q, l)
+  }
+}
+
+repeat_pop(q, l) {
+  if _ then ()
+  else {
+      push(q, _, l);
+      repeat_push(q, l)
+  }
+}
+
 {
-  let q = mkqueue(2) in
+  let n = (_: ~ > 0) in
+  let q = mkqueue(n) in
   let l = newlock() in
   let t = fork({
-    push(q, _, l);
-    push(q, _, l);
-    push(q, _, l);
+    repeat_push(q, l);
   }) in {
-    pop(q, l);
-    pop(q, l);
-    pop(q, l);
+    repeat_pop(q, l);
     wait(t);
     freelock(l);
-    check(q)
+    check(q);
   }
 }

src/concurrency/flow/positive/wip/return_lock.imp

@@ -0,0 +1,29 @@
+create(init){
+    let x = mkref init in
+    let l = newlock() in
+    (x, l) 
+}
+
+blocking_update(xl, y) {
+    let (x, l) = xl in {
+        acq(l);
+        x := y;
+        rel(l);
+        alias(xl.0 = x);
+        alias(xl.1 = l);
+    }
+}
+
+{
+    let xl = create(3) in
+    let t = fork(
+        blocking_update(xl, 2)
+    ) in {
+        blocking_update(xl, 4);
+        wait(t);
+        let (x, l) = xl in {
+            freelock(l);
+            assert(*x > 0);
+        }
+    }
+}