module Module {
  var request: boolean;
  var status: enum { busy, ready };
  var auxiliary: enum { a, b };

  next {
    auxiliary' = auxiliary;
    if (request) {
      if (status == ready) {
        status' = busy;
      }
    }

  }
  invariant spec: (!request || (status == busy));

}
