-- Synchronous bus arbiter as modelled by de Simon in Esterel

var  req1,ack1,tokin1,grantin1,
     req2,ack2,tokin2,grantin2,
     req3,ack3,tokin3,grantin3,
     req4,ack4,tokin4,grantin4,
     req5,ack5,tokin5,grantin5;

const n=4 ;

define cell[req,ack,tokin,tokout,grantin,grantout] as
   [[
      ack <=> req && (tokin || grantin) 
   ]]
&& [[
      grantout <=> !req && (tokin || grantin)
   ]]

&& [](    (<tokin>^slen=1   => true^<tokout>) 
       && (<!tokin>^slen=1   => true^<!tokout>) 
     )

;

define inittok as
    <tokin1 && !tokin2 && !tokin3 && !tokin4 && !tokin5>^true
;

define arbiter5 as
    cell[ req1, ack1, tokin1, tokin2, grantin1, grantin2 ]
&&
    cell[ req2, ack2, tokin2, tokin3, grantin2, grantin3 ]
&&
    cell[ req3, ack3, tokin3, tokin4, grantin3, grantin4 ]
&&
    cell[ req4, ack4, tokin4, tokin5, grantin4, grantin5 ]
&&
    cell[ req5, ack5, tokin5, tokin1, grantin5, grantin1 ]
&&  
    inittok
;


define Exclusion as
[[    ( ack1 => !(ack2 || ack3 || ack4 || ack5))
  &&  ( ack2 => !(ack1 || ack3 || ack4 || ack5))
  &&  ( ack3 => !(ack1 || ack2 || ack4 || ack5))
  &&  ( ack4 => !(ack1 || ack2 || ack3 || ack5))
]]
;

define Response as
  [[ (req1 || req2 || req3 || req4 || req5)
     => (ack1 || ack2 || ack3 || ack4 || ack5)
  ]]
;

define Firstcome[freq,fack,sreq,sack] as
  [] ( [[freq && !fack]] => !(<!sreq>^<><sack>))
;

define Fairness[req,ack] as
 [] ([[req]] && slen=n-1 => <> <ack>)
;

infer
  arbiter5 => Exclusion
        -- && Response && Fairness 
.