Function trip_count 

pub fn trip_count<V: ValueAlgebra>(
    t0: &V,
    step: &V,
    bound: &V,
    relation: &str,
) -> Result<V, String>

How many times While t <relation> bound: runs when each step adds step to t, starting from t0: ⌈(bound − t0)/step⌉ for a strict bound, ⌊…⌋ + 1 for an inclusive one, 0 when the guard is false at the start. −1 — not counted, so the loop runs as written — when the clock is not a number, or when a standard step walks away from its bound; a refusal when an infinitesimal step does, since that loop could never end.