Function all_until 

pub fn all_until(
    graph: &[NQuin],
    start: u64,
    phi: u64,
    psi: u64,
    next: u64,
    holds: u64,
) -> bool

A[φ U ψ] — on EVERY path from start, phi holds at each state until psi becomes true (and psi is reached on every path). Least-fixpoint labelling. Bounded + zero-heap. Completes the CTL operator set (EX, AX, EF, AF, EG, AG, EU, AU).