def successor(i, k, l):
    """
    Computes the successor of time `i` in a k-l loop.

    .. note::
        References, see Definition 6
        in Biere et al - ``Bounded Model Checking'' - 2003

    .. note::
        An other implementation of this function (w/ the same semantics) exists
        in :mod:`pynusmv.bmc.utils`. This version is merely re-implemented to
        1. show that it can be easily done
        2. stick closely to the definition given in the paper by Biere et al.
            (see other note)

    .. warning::
        To be consistent with the way the loop condition is implemented (equiv
        of all the state variables), we have that walking 'k' steps means to be
        back at step 'l'. Hence, the value of i can only vary from 0 to k-1
        (and will repeat itself in the range [l; k-1]

    :param i: the current time
    :param k: the maximum (horizon/bound) time of the problem
    :param l: the time where the loop starts

    :return: the k-l loop successor of i
    """
    return i + 1 if i < k - 1 else l
