module main(req1,req2,ack1,ack2)
{
  input req1,req2 : boolean;
  output ack1,ack2 : boolean;

  ack1 := req1 ;
  ack2 := req2 & ~req1;

  /* Only one acknowlegment at a time */
  mutex : assert G( ~(ack1 & ack2) );
  
  /* If there is a request, there is an immediate acknowlegment. */
  serve : assert G( (req1 | req2) -> (ack1 | ack2) ) ;
  
  /* Acknowlegement only happen when, there is a corresponding. */
  waste1 : assert G( ack1 -> req1 );
  waste2 : assert G( ack2 -> req2 );
  
  /* Each request is eventually served or retracted. */
  /* Unfortunately this implementation does not satisfy both */
  z_eventualy1 : assert G( F( !req1 | ack1 ) ) ;
  z_eventualy2 : assert G( F( !req2 | ack2 ) ) ;
}