def str2ms(s):
    """
    Convert the time strings from an SRT file to milliseconds.

    Arguments:
        s: A time value in the format HH:MM:SS,mmm where H, M, S and m are
           digits.

    Returns:
        The time string converted to an integer value in milliseconds.
    """
    s = s.strip()
    time, ms = s.split(",")
    h, m, s = time.split(":")
    return int(ms) + 1000 * (int(s) + 60 * (int(m) + 60 * int(h)))