component QueueFull
{
  provides IP pp;
  requires IR rp;
  
  behaviour
  {
    on pp.ia(): rp.ia();
    on rp.oa(): {}
  }
  
  // Verifying model QueueFull =>
  //   queue full
  // For trace
  //   pp.ia
  //   rp.ia
  //   rp.oa
  //   rp.oa
  //   rp.oa
  //   rp.oa
  //   rp.return
}

interface IP
{
  in void ia();
  
  behaviour
  {
    on ia: {}
  }
}

interface IR
{
  in void ia();
  out void oa();
  
  behaviour
  {
    on ia: {oa; oa; oa; oa;}
  }
}