specification SPROT [PUT,GET] :noexit

  library SPROT endlib 

  behaviour

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

where

   process PSEND [PUT,channel,ack] :noexit :=
     PUT ?message:MSG;
       channel !message;
         ack;
           PSEND[PUT,channel,ack]
   endproc

   process PRECV [channel,GET,ack]:noexit:=
     channel ?message:MSG;
       GET !message;
         ack;
           PRECV[channel,GET,ack]
   endproc

endspec