def HHMMSS_to_seconds(string):
  """Converts a colon-separated time string (HH:MM:SS) to seconds since
  midnight"""
  (hhs,mms,sss) = string.split(':')
  return (int(hhs)*60 + int(mms))*60 + int(sss)