module MS (TYPES, CHANNELS) is

-------------------------------------------------------------------------------
-- this module is only used by the asynchronous specification HAVi_asyn
-------------------------------------------------------------------------------

type Buffer is
   list of MesFrame
   with head, tail
end type

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

function MaxBuf : Nat3 is
   return 1
end function

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

function append (mf: MesFrame, buf: Buffer) : Buffer is
   case buf 
      var mf2: MesFrame, buf2: Buffer
   in
      nil -> return cons (mf, nil)
   |  cons (mf2, buf2) -> return cons (mf2, append (mf, buf2))
   end case
end function

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

function length (buf: Buffer) : Nat3 is
   case buf
      var buf2: Buffer
   in
      nil -> return 0
   |  cons (any MesFrame, buf2) -> return 1 + length (buf2)
   end case
end function

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

channel IOChannel is
   (Id: Nat3, m: Message1),
   (Id: Nat3, mf: MesFrame)
end channel

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

process MS [gUpDown: UpDownChannel, gBusReset: BusResetChannel,
        gDMin, gDMout: IOChannel] (Id: Nat3) is
   MSDown [gUpDown, gBusReset, gDMin, gDMout] (Id)
end process

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

process MSDown [gUpDown: UpDownChannel, gBusReset: BusResetChannel,
        gDMin, gDMout: IOChannel] (Id: Nat3) is
   disrupt
      FlushBusReset [gBusReset]
   by
      gUpDown (Id, power_change);
      MSUp [gUpDown, gBusReset, gDMin, gDMout] (Id, nil)
   end disrupt
end process

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

process MSUp [gUpDown: UpDownChannel, gBusReset: BusResetChannel,
        gDMin, gDMout: IOChannel] (Id: Nat3, buf: Buffer) is
   disrupt
      MSSuspend [gBusReset, gDMin, gDMout] (Id, buf)
   by
      gUpDown (Id, power_change);
      MSDown [gUpDown, gBusReset, gDMin, gDMout] (Id)
   end disrupt
end process

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

process MSSuspend [gBusReset: BusResetChannel, gDMin, gDMout: IOChannel]
        (Id: Nat3, buf: Buffer) is
      alt
         gDMin (Id, empty);
         MSSuspend [gBusReset, gDMin, gDMout] (Id, nil)
      []
         only if length (buf) > 0 then
            gDMout (Id, head (buf));
            MSSuspend [gBusReset, gDMin, gDMout] (Id, tail (buf))
         end if
      []
         gBusReset (bus_reset_end, ?any Network);
         MSReady [gBusReset, gDMin, gDMout] (Id, buf)
      end alt
end process

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

process MSReady [gBusReset: BusResetChannel, gDMin, gDMout: IOChannel]
        (Id: Nat3, buf: Buffer) is
   alt
      only if length (buf) < maxBuf then
         var mf: MesFrame in
            mf := any MesFrame;
            gDMin (Id, mf);
            MSReady [gBusReset, gDMin, gDMout] (Id, append (mf, buf))
         end var
      end if
   []
      gDMin (Id, empty);
      MSReady [gBusReset, gDMin, gDMout] (Id, nil)
   []
      only if length (buf) > 0 then
         gDMout (Id, head (buf));
         MSReady [gBusReset, gDMin, gDMout] (Id, tail (buf))
      end if
   []
      gBusReset (bus_reset_start);
      MSSuspend [gBusReset, gDMin, gDMout] (Id, buf)
   end alt
end process
 
-------------------------------------------------------------------------------

end module