Function obligation_until 

pub fn obligation_until(
    ante: u64,
    consequent: u64,
    trace: &[NQuin],
) -> DeonticStatus

O(φ U ψ) — the obligation that ante holds until consequent becomes true (provisional measures: “detention standards apply until release”). Discharged iff the until-formula holds over the trace; otherwise Violated.