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

  prev : 1..2 ;
  
  if( prev=2 ) {
    ack1 := req1 ;
    ack2 := req2 & ~req1 ; }
  else {
    ack2 := req2 ;
    ack1 := req1 & ~req2 ; }

  if( ack1 )      next(prev) := 1 ;
  else if( ack2 ) next(prev) := 2 ;
  
  /* 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. */
  z_eventualy1 : assert G( F( !req1 | ack1 ) ) ;
  z_eventualy2 : assert G( F( !req2 | ack2 ) ) ;
  
  /* In fact the we can make a stronger assertion:
  * Each request is acknowleged in 0 or 1 time cycles. */
  fast1 : assert G( req1 -> ack1 | X(req1 -> ack1) ) ;
  fast2 : assert G( req2 -> ack2 | X(req2 -> ack2) ) ;
}