pub fn obligation_globally(prop: u64, trace: &[NQuin]) -> DeonticStatusExpand description
O(Gφ) — the obligation that property prop holds globally across a state trace.
Discharged iff prop holds in every state; otherwise Violated. (Continuous protections:
“no one shall be subjected to torture” must hold in every state, not just eventually.)