CTLFORM
var RequestIn, AckOut, Lostcycle;

const n = 5;


define Respond as
  [[ !Lostcycle
  ]]
;

define PROP as
[]  ( [[RequestIn]] && (slen = n-1) => <><AckOut> );

ctldc
--  No spurious Response 
!EF #![[ AckOut => RequestIn ]]# ;

--  No lost cycles
!EF #!Respond# ;

--  Bounded Response
!EF #!PROP# ;

SYSTEM vest Arbiter5
input RequestIn1, RequestIn2, RequestIn3, RequestIn4, RequestIn5;
output AckOut1, AckOut2, AckOut3, AckOut4, AckOut5;

OBSERVE
   RequestIn := RequestIn1;
   AckOut := AckOut1 ;
   Lostcycle := (RequestIn1 || RequestIn2 || RequestIn3 || RequestIn4 
      || RequestIn5) && ! (AckOut1 || AckOut2 || AckOut3 
      || AckOut4 || AckOut5) ;
.