module TRANS (DATA, CHANNELS) is

process Trans [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack, TDreq: Dreq]
              (n, id: Nat, v: Version) is
   hide TX0: none in
      par TX0 in
         TransReq [LDreq, LDcon, TDreq, TX0] (n, id)
      ||
         TransRes [LDind, LDres, TX0] (id, v)
      end par
   end hide
end process

------------------------------------------------------------------------------

process TransReq [LDreq: Dreq, LDcon: Dcon, TDreq: Dreq, TX0: none]
                 (n, id: Nat) is
   var dest: Nat, h: HEADER, d: DATA, a: ACK in
      loop
         TDreq (id, ?dest, ?h, ?d) where dest <= n;
         alt
            TX0
         []
            null
         end alt;
         i; -- this "i" corresponds to the ">>" operator in the LOTOS specification
         LDreq (id, dest, h, d);
         alt
            if dest = n then
               LDcon (id, broadsent)
            else
               a := any ACK;
               LDcon (id, ackrec (a))
            end if
         []
            LDcon (id, ackmiss)
         end alt
      end loop
   end var
end process

------------------------------------------------------------------------------

process TransRes [LDind: Dind, LDres: Ack, TX0: none] (id: Nat, v: Version) is
   var l: LIN_DIND, a: ACK in
      loop
         LDind (id, ?l);
         if is_broadrec (l) then
            case v in
               ko ->
                  -- original (incorrect) specification
                  LDres (id, a1, no_op)
            |  ok ->
                  -- correct specification
                  null
            end case
         else
            a := any ACK;
            alt
               -- concatenated response = lock transaction
               TX0;
               LDres (id, a, hold)
            []
               -- split response
               LDres (id, a, release)
            end alt
         end if
      end loop
   end var
end process

end module