Skip to main content

obligation_globally

Function obligation_globally 

Source
pub fn obligation_globally(prop: u64, trace: &[NQuin]) -> DeonticStatus
Expand 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.)