channel NumberStream(x: int) where 2 <= x ==> credit(this);

class Sieve {
  method Counter(n: NumberStream, to: int)  // sends the plurals along n
    requires rd(n.mu) && credit(n,-1) && 0 <= to;
  {
    var i := 2;
    while (i < to)
      invariant rd(n.mu);
      invariant 2 <= i;
      invariant credit(n, -1)
    {
      send n(i);
      i := i + 1;
    }
    send n(-1);
  }

  method Filter(prime: int, r: NumberStream, s: NumberStream)
    requires 2 <= prime;
    requires rd(r.mu) && waitlevel << r.mu;
    requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1);
  {
    receive x := r;
    while (2 <= x)
      invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu;
      invariant 2<= x ==> credit(r);
      invariant credit(s, -1);
    {
      if (x % prime != 0) {  // suppress multiples of prime
        send s(x);
      }
      receive x := r;
      
    }
    send s(-1);
  }

  method Start()
  {
    var ch := new NumberStream;
    fork Counter(ch, 101);
    var p: int;
    receive p := ch;
    while (2 <= p)
      invariant ch != null;
      invariant 2 <= p ==> credit(ch, 1);
      invariant rd*(ch.mu) && waitlevel << ch.mu;
    {
      // print p--it's a prime!
      var cp := new ChalicePrint;  call cp.Int(p);

      var n := new NumberStream between waitlevel and ch;
      fork Filter(p, ch, n);
      ch := n;
      receive p := ch;
    }
  }
}

external class ChalicePrint {
  method Int(x: int) { }
}