def format_time(time):
  mins = int(time/60)
  secs = int(time % 60)
  ms = int( (time * 1000) % 1000)
  return "%02d:%02d.%03d" % (mins, secs, ms)
dataset/ETHPy150Open ucb-sts/sts/sts/control_flow/event_scheduler.py/format_time/original