class Cell {
  var val: int
}

channel Ch(c: Cell) where
  c != null ==> acc(c.val) && 0 <= c.val && credit(this)

class Program {
  method Main() {
    var ch := new Ch
    fork tk0 := Producer(ch)
    fork tk1 := Consumer(ch)
    join tk0
    join tk1
  }
  method Producer(ch: Ch)
    requires ch != null
    ensures credit(ch)
  {
    var i := 0
    while (i < 25)
    {
      var x := i*i
      var c := new Cell { val := x }
      send ch(c)
      i := i + 1
    }
    send ch(null)
  }
  method Consumer(ch: Ch)
    requires rd(ch.mu) && waitlevel << ch.mu
    requires credit(ch)
    ensures rd(ch.mu)
  {
    var c: Cell
    receive c := ch
    while (c != null)
      invariant rd(ch.mu) && waitlevel << ch.mu
      invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
    {
      var i := c.val
      receive c := ch
    }
  }
}