CTLFORM
var req,ack;
const m = 5; 
define gotack as <><ack> ;
ctldc
 AG (     #[]([[req]] && slen=m-1 => gotack)# 
     && #[[ ack => req]]#) ;

SYSTEM vis arbiter 
input req1,req2,req3,req4,req5;
output ack1,ack2,ack3,ack4,ack5;

OBSERVE
   req := req1 ;
   ack := ack1 ;
.