module LINK (DATA, CHANNELS) is

process Link [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
              PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
             (n, id: Nat) is
   Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon, PCind]
         (n, id, void)
end process

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

process Link0 [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
               PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
              (n, id: Nat, buffer: SIG_TUPLE) is
   alt
      if is_void (buffer) then
         var dest: Nat, h: HEADER, d: DATA, b: SIG_TUPLE in
            LDreq (id, ?dest, ?h, ?d);
            b := quadruple (dhead,
                            destsig (dest),
                            headsig (h, crc (h)),
                            datasig (d, crc (d)));
            Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, b)
         end var
      else
         PAreq (id, fair);
         -- here, the LOTOS process Link1 was expanded in-line
         -- (see footnote 8 in the research report [Sighireanu-Mateescu-97])
         alt
            PAcon (id, won);
            -- here, process Link2 represents the LOTOS process Link2req
            Link2 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, void, buffer)
         []
            PAcon (id, lost);
            Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer)
         end alt
      end if
   []
      var p: SIGNAL in
         PDind (id, ?p);
         if p = Start then
            Link4 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer)
         else
            Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer)
         end if
      end var
   end alt
end process

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

process Link1 [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
               PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
              (n, id: Nat, buffer: SIG_TUPLE, p: SIGNAL) is
   -- process Link1 factors code repeated thrice in process Link3 below
   LDcon (id, ackmiss);
   if p = subactgap then
      Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon, PCind]
            (n, id, buffer)
   else
      LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon, PCind]
              (n, id, buffer, n)
   end if
end process

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

process Link2 [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
               PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
              (n, id: Nat, buffer: SIG_TUPLE, p: SIG_TUPLE) is
   -- process Link2 unifies the two LOTOS processes Link2req and Link2resp
   PCind (id);
   PDreq (id, Start);
   PCind (id);
   PDreq (id, p.dh);
   PCind (id);
   PDreq (id, p.dest);
   PCind (id);
   PDreq (id, p.header);
   PCind (id);
   PDreq (id, p.data);
   PCind (id);
   PDreq (id, End);
   if getdest (p.dest) = n then
      LDcon (id, broadsent);
      Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon, PCind]
            (n, id, buffer)
   else
      -- here, the LOTOS process Link3 was expanded in-line (called only once)
      var p, a, e: SIGNAL in
         loop L in
            PDind (id, ?p);
            if p <> Prefix then
               break L
            end if
         end loop;
         if p <> Start then
            Link1 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer, p)
         else
            -- here, the LOTOS process Link3RA was expanded (called only once)
            PDind (id, ?a);
            if is_physig (a) then
               Link1 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                      PCind] (n, id, buffer, a)
            else
               -- here, the process Link3RE was expanded (called only once)
               PDind (id, ?e);
               if valid_ack (a) and ((e = End) or (e = Prefix)) then
                  LDcon (id, ackrec (getack (a)));
                  LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq,
                           PAcon, PCind] (n, id, buffer, n)
               else
                  Link1 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq,
                         PAcon, PCind] (n, id, buffer, e)
               end if
            end if
         end if
      end var
   end if
end process

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

process Link4 [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
               PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
              (n, id: Nat, buffer: SIG_TUPLE) is
   var s1, s2, s3, s4, s5: SIGNAL, dest: Nat in
      PDind (id, ?s1);
      if s1 = subactgap then
         Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon, PCind]
               (n, id, buffer)
      elsif is_physig (s1) then
         LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                  PCind] (n, id, buffer, n)
      else
         -- here, the process Link4DH was expanded in-line (called only once)
         PDind (id, ?s2);
         if s2 = subactgap then
            Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer)
         elsif not (is_dest (s2)) or else
               ((getdest (s2) <> id) and (getdest (s2) <> n)) then
            LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                     PCind] (n, id, buffer, n)
         else
            dest := getdest (s2);
            if dest = id then
               PAreq (id, immediate)
            end if;
            -- here, the LOTOS process Link4RH was expanded (called only once)
            PDind (id, ?s3);
            if not (valid_hpart (s3)) then
               -- here, the process Link4RD was expanded (called only once)
               LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                        PCind] (n, id, buffer, dest)
            else
               PDind (id, ?s4);
               if not (is_data (s4)) then
                  LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq,
                           PAcon, PCind] (n, id, buffer, dest)
               else
                  -- here, the process Link4RE was expanded (called only once)
                  PDind (id, ?s5);
                  if (s5 <> End) and (s5 <> Prefix) then
                     LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq,
                              PAcon, PCind] (n, id, buffer, dest)
                  elsif dest <> id then
                     -- here, the process Link4BRec was expanded (called only once)
                     if getdcrc (s4) = check then
                        LDind (id, broadrec (gethead (s3), getdata (s4)))
                     end if;
                     Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq,
                            PAcon, PCind] (n, id, buffer)
                  else
                     -- here, the process Link4DRec was expanded (called only once)
                     if getdcrc (s4) = check then
                        LDind (id, good (gethead (s3), getdata (s4)))
                     else
                        LDind (id, dcrc_err (gethead (s3)))
                     end if;
                     PAcon (id, won);
                     -- here, the process Link5 was expanded (called only once)
                     loop L in
                        alt
                           PCind (id);
                           PDreq (id, Prefix)
                        []
                           break L
                        end alt
                     end loop;
                     var a: ACK, b: BOC, p: SIGNAL in
                        LDres (id, ?a, ?b);
                        p := acksig (a, crc (a));
                        -- here, the process Link6 was expanded (called only once)
                        PCind (id);
                        PDreq (id, Start);
                        PCind (id);
                        PDreq (id, p);
                        PCind (id);
                        if b = release then
                           PDreq (id, End);
                           Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind,
                                  PAreq, PAcon, PCind] (n, id, buffer)
                        else
                           PDreq (id, Prefix);
                           -- here, the process Link7 was expanded (called only once)
                           loop L in
                              alt
                                 PCind (id);
                                 PDreq (id, Prefix)
                              []
                                 break L
                              end alt
                           end loop;
                           var dest: Nat, h: HEADER, d: DATA, t: SIG_TUPLE in
                              LDreq (id, ?dest, ?h, ?d);
                              t := quadruple (dhead,
                                              destsig (dest),
                                              headsig (h, crc (h)),
                                              datasig (d, crc (d)));
                              -- here, Link2 represents the LOTOS process Link2resp
                              Link2 [LDreq, LDcon, LDind, LDres, PDreq, PDind,
                                     PAreq, PAcon, PCind] (n, id, buffer, t)
                           end var
                        end if
                     end var
                  end if
               end if
            end if
          end if
      end if
   end var
end process

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

process LinkWSA [LDreq: Dreq, LDcon: Dcon, LDind: Dind, LDres: Ack,
                 PDreq, PDind: Sig, PAreq: Areq, PAcon: Acon, PCind: Id]
                (n, id: Nat, buffer: SIG_TUPLE, dest: Nat) is
   alt
      var p: SIGNAL in
         PDind (id, ?p);
         if p = subactgap then
               Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                      PCind] (n, id, buffer)
         else
               LinkWSA [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                        PCind] (n, id, buffer, dest)
         end if
      end var
   []
      only if dest = id then
            PAcon (id, won);
            PCind (id);
            PDreq (id, End);
            Link0 [LDreq, LDcon, LDind, LDres, PDreq, PDind, PAreq, PAcon,
                   PCind] (n, id, buffer)
      end if
   end alt
end process

end module