specification SPROT_spec [PUT,GET] :noexit

  behaviour

    hide msg,ack in
    (
      PSEND [PUT,msg,ack]
      |[msg,ack]|
      PRECV [msg,GET,ack]
    )

where

   process PSEND [PUT,msg,ack] :noexit :=
     PUT; msg; ack;
       PSEND[PUT,msg,ack]
   endproc

   process PRECV [msg,GET,ack]:noexit:=
     msg; GET; ack;
       PRECV[msg,GET,ack]
   endproc

endspec