module BUS (DATA, CHANNELS) is

process Bus [PAreq: Areq, PDreq, PDind: Sig, PAcon: Acon, PCind: Id,
             arbresgap, losesignal: none] (n: Nat) is
   BusIdle [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
           (n, init (n))
end process

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

process BusIdle [PAreq: Areq, PDreq, PDind: Sig, PAcon: Acon, PCind: Id,
                 arbresgap, losesignal: none] (n: Nat, t: BoolTABLE) is
   alt
      var id: Nat in
         PAreq (?id, ?any PHY_AREQ) where id < n;
         -- here, the LOTOS process DecideIdle was expanded in-line
         -- (see footnote 7 in the research report [Sighireanu-Mateescu-97])
         if get (id, t) = false then
            PAcon (id, won);
            BusBusy [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
                    (n, invert (id, t), init (n), init (n), id)
         else
            PAcon (id, lost);
            BusIdle [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
                    (n, t)
         end if
      end var
   []
      only if not (zero (t)) then
         arbresgap;
         BusIdle [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
                 (n, init (n))
      end if
   end alt
end process

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

process BusBusy [PAreq: Areq, PDreq, PDind: Sig, PAcon: Acon, PCind: Id,
                 arbresgap, losesignal: none] (n: Nat, t: BoolTABLE,
                 in var next: BoolTABLE, destfault: BoolTABLE, busy: Nat) is
   alt
      var j: Nat in
         PAreq (?j, fair) where j < n;
         PAcon (j, lost);
         BusBusy [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
                 (n, t, next, destfault, busy)
      end var
   []
      var j: Nat in
         PAreq (?j, immediate) where not (get (j, next)) and (j < n);
         BusBusy [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
                 (n, t, invert (j, next), destfault, busy)
      end var
   []
      if busy < n then
         var p: SIGNAL in
            PCind (busy);
            PDreq (busy, ?p);
            Distribute [PAreq, PDreq, PDind, PAcon, PCind, arbresgap,
                        losesignal] (n, t, next, destfault, busy, p)
         end var
      elsif zero (next) then
         SubactionGap [PAreq, PDreq, PDind, PAcon, PCind, arbresgap,
                       losesignal] (n, t)
      else
         -- here, the LOTOS process Resolve was expanded (called only once)
         var j: Nat, p: SIGNAL in
            for j := 0  while j < n by j := j + 1 loop
               if get (j, next) then
                  PAcon (j, won);
                  PCind (j)
               end if
            end loop;
            -- here, the LOTOS process Resolve2 was expanded (called only once)
            while more (next) loop
               PDreq (?j, End) where get (j, next) and (j < n);
               next := invert (j, next)
            end loop;
            PDreq (?j, ?p) where j < n;
            if p = End then
               SubactionGap [PAreq, PDreq, PDind, PAcon, PCind, arbresgap,
                             losesignal] (n, t)
            else
               Distribute [PAreq, PDreq, PDind, PAcon, PCind, arbresgap,
                           losesignal] (n, t, init (n), init (n), j, p)
            end if
         end var
      end if
   end alt
end process

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

process SubactionGap [PAreq: Areq, PDreq, PDind: Sig, PAcon: Acon, PCind: Id,
                      arbresgap, losesignal: none] (n: Nat, t: BoolTABLE) is
   var j: Nat in
      for j := 0 while j < n by j := j + 1 loop
         PDind (j, subactgap)
      end loop;
      BusIdle [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal] (n, t)
   end var
end process

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

process Distribute [PAreq: Areq, PDreq, PDind: Sig, PAcon: Acon, PCind: Id,
                    arbresgap, losesignal: none] (n: Nat, t: BoolTABLE,
                    in var next, destfault: BoolTABLE, busy: Nat, p: SIGNAL) is
   var j, incr: Nat in
      for j := 0 while j < n by j := j + incr loop
         incr := 1;
         if j <> busy then
            alt
               only if not (is_header (p) and get (j, destfault)) then
                  PDind (j, p)
               end if
            []
               only if is_dest (p) then
                  var dest: Nat in
                     dest := any Nat;
                     PDind (j, destsig (dest));
                     destfault := invert (j, destfault)
                  end var
               end if
            []
               only if is_header (p) or is_data (p) or is_ack (p) then
                  alt
                     PDind (j, corrupt (p))
                  []
                     losesignal
                  end alt
               end if
            []
               only if is_data (p) then
                  PDind (j, p);
                  PDind (j, Dummy)
               end if
            []
               PAreq (j, immediate) where not (get (j, next));
               incr := 0; -- instead of 1, here
               next := invert (j, next)
            end alt
         end if
      end loop;
      if p = End then
         j := n
      else
         j := busy
      end if;
      BusBusy [PAreq, PDreq, PDind, PAcon, PCind, arbresgap, losesignal]
              (n, t, next, destfault, j)
   end var
end process

end module