Specification Alternating_Bit_protocol systemprocess; timescale seconds;

type  { ... is used to specify that an implementer
              must define these types for his environment.}
    U_Data_type = ...;     { user data }

{ Channel definitions for communication between the processes }

channel U_access_point(User,Provider);
    by User:
        U_DATreq (msg:  U_Data_type);

channel N_access_point(User,Provider);
    by User:
        DT (msg:        U_Data_type;
            ctlbit:     boolean);
    by Provider:
        ACK (ackbit:    boolean);


module Sender process;
    ip {interaction point list }
       U:  U_access_point(Provider) common queue;
       N:  N_access_point(User)     individual queue;
end; { of module header definition }


body Sender_body for Sender;

var     msg_buffer:   U_Data_type;
        ctlbit:       boolean;

state WfAck, WfReq; { state definition part }

function Korrekt: boolean; external;
  (* <=> no bit error detectable *)

function Ack_ok(b: boolean): boolean;
  begin
    Ack_ok := (b = ctlbit) and Korrekt;
  end;

procedure Alt_ctlbit;
  begin
    ctlbit := not ctlbit
  end;

initialize { initialization-part of the Sender process }

to WfReq  { initialize major state variable to WfReq }
   begin  { initialize variables }
     ctlbit := false;
   end;

trans {  transition-declaration-part of the Sender process   }

from WfReq
    to WfAck
       when U.U_DATreq
         begin
           msg_buffer := msg; (* Hold msg for negative ACK *)
           output N.DT(msg,ctlbit);
         end;

from WfAck
    to WfReq
      when N.ACK
        provided Ack_ok(ackbit)
          begin                    
            Alt_ctlbit
          end;

from WfAck
    to same
      when N.ACK
        provided not Ack_ok(ackbit)
          begin
            output N.DT(msg_buffer,ctlbit);
          end;

end; {  of the Sender_body}

modvar
    { module-variable-declaration-part of the specification }

    Send_entity: Sender;

initialize { initialization-part of the specification }
  begin { module initialization }
    init Send_entity with Sender_body;
  end; { of module initialization within the
        specification's initialization-part }

end.  { End of specification; the specification has no transition part }