specification Railroad_Crossing : exit

type natural is boolean
  sorts nat
  opns + : nat,nat->nat
       - : nat,nat->nat
endtype

behaviour
 hide approach, leave, lower, raise, into, outto, down, up in

  ( Train[approach,leave,into,outto]
    |[approach,leave]|
    Controller[approach,lower,leave,raise] )
  |[lower,raise]|
  Gate[lower,raise,down,up]

where

  process Train[approach,leave,into,outto] : noexit :=
    approach;
    ( ( into; outto; leave; exit )
      |[into,outto,leave]|
      ( ( delay(300,500) into{200}; exit )
        |||
        ( delay(300,500) outto{200}; exit )
        |||
        ( delay(300,500) leave{200}; exit ) ) )
    >> Train[approach,leave,into,outto]
  endproc

  process Controller[approach,lower,leave,raise] : noexit :=
    approach; delay(100) lower;
    leave; latency(100) raise{100}; 
    Controller[approach,lower,leave,raise]
  endproc

  process Gate[lower,raise,down,up] : noexit :=
    lower; latency(100) down{100}; 
    raise; delay(100,200) up{100};
    Gate[lower,raise,down,up]
  endproc

endspec