qualia_core_db/modalities/
temporal_ltl.rs

1use crate::NQuin;
2
3pub const OP_LTL_GLOBALLY: u8 = 0x40;
4pub const OP_LTL_FINALLY: u8 = 0x41;
5pub const OP_LTL_NEXT: u8 = 0x42;
6pub const OP_LTL_UNTIL: u8 = 0x43;
7pub const OP_LTL_RELEASE: u8 = 0x44;
8
9#[repr(C)]
10#[derive(Debug, Clone, Copy, PartialEq, Eq)]
11pub enum LtlFormula {
12    Globally(u64),
13    Finally(u64),
14    Next(u64),
15    Until { ante: u64, consequent: u64 },
16    Release { trigger: u64, invariant: u64 },
17}
18
19#[derive(Debug)]
20pub enum TemporalError {
21    AbortedTimeout,
22}
23
24pub fn evaluate_lock_lease(
25    lock_granted_at: u64,
26    current_time: u64,
27    ttl_seconds: u64,
28) -> Result<(), TemporalError> {
29    if current_time > lock_granted_at + ttl_seconds {
30        return Err(TemporalError::AbortedTimeout);
31    }
32    Ok(())
33}
34
35pub fn evaluate_ltl_trace(trace: &[NQuin], formula: &LtlFormula) -> bool {
36    match formula {
37        LtlFormula::Globally(p) => {
38            if trace.is_empty() {
39                return false;
40            }
41            for quin in trace {
42                if quin.predicate != *p {
43                    return false;
44                }
45            }
46            true
47        }
48        LtlFormula::Finally(p) => {
49            if trace.is_empty() {
50                return false;
51            }
52            for quin in trace {
53                if quin.predicate == *p {
54                    return true;
55                }
56            }
57            false
58        }
59        LtlFormula::Next(p) => {
60            if trace.len() < 2 {
61                return false;
62            }
63            trace[1].predicate == *p
64        }
65        LtlFormula::Until { ante, consequent } => {
66            if trace.is_empty() {
67                return false;
68            }
69            for (i, quin) in trace.iter().enumerate() {
70                if quin.predicate == *consequent {
71                    let mut ante_held = true;
72                    for j in 0..i {
73                        if trace[j].predicate != *ante {
74                            ante_held = false;
75                            break;
76                        }
77                    }
78                    if ante_held {
79                        return true;
80                    }
81                }
82            }
83            false
84        }
85        LtlFormula::Release { trigger, invariant } => {
86            if trace.is_empty() {
87                return true;
88            }
89            for (i, quin) in trace.iter().enumerate() {
90                if quin.predicate != *invariant {
91                    let mut triggered = false;
92                    for j in 0..=i {
93                        if trace[j].predicate == *trigger {
94                            triggered = true;
95                            break;
96                        }
97                    }
98                    if !triggered {
99                        return false;
100                    }
101                }
102            }
103            true
104        }
105    }
106}
107
108/// Metric temporal (MTL) "within": after the EARLIEST occurrence of `trigger`
109/// (each event quin carries its timestamp in `metadata`), `target` must occur at
110/// some time `t1` with `t0 <= t1 <= t0 + window`. Models deadlines — e.g. "remedy
111/// within 30 days of breach". Zero-heap (two linear scans; no allocation).
112pub fn holds_within(trace: &[NQuin], trigger: u64, target: u64, window: u64) -> bool {
113    // t0 = earliest timestamp at which the trigger holds.
114    let mut t0: Option<u64> = None;
115    for q in trace {
116        if q.predicate == trigger {
117            t0 = Some(match t0 {
118                Some(prev) => prev.min(q.metadata),
119                None => q.metadata,
120            });
121        }
122    }
123    let t0 = match t0 {
124        Some(t) => t,
125        None => return false, // trigger never occurred
126    };
127    let deadline = t0.saturating_add(window);
128    for q in trace {
129        if q.predicate == target && q.metadata >= t0 && q.metadata <= deadline {
130            return true;
131        }
132    }
133    false
134}
135
136/// MTL **bounded-globally** `G[t0, t0+window] inv`: from the earliest `trigger` timestamp `t0`,
137/// the `invariant` must hold at *every* event whose timestamp lies in `[t0, t0+window]`. Returns
138/// `true` vacuously if no in-window events. Zero-heap.
139pub fn holds_globally_within(trace: &[NQuin], trigger: u64, invariant: u64, window: u64) -> bool {
140    let mut t0: Option<u64> = None;
141    for q in trace {
142        if q.predicate == trigger {
143            t0 = Some(t0.map_or(q.metadata, |p| p.min(q.metadata)));
144        }
145    }
146    let t0 = match t0 {
147        Some(t) => t,
148        None => return false,
149    };
150    let deadline = t0.saturating_add(window);
151    // Every event in the window must satisfy the invariant.
152    for q in trace {
153        if q.metadata >= t0
154            && q.metadata <= deadline
155            && q.predicate != invariant
156            && q.predicate != trigger
157        {
158            return false;
159        }
160    }
161    true
162}
163
164// ─── Past-time LTL (Once, Historically, Since) ────────────────────────────────────
165
166/// **Once** `O p` (past ◇): `p` held at some point in the trace (the past-time dual of `Finally`).
167pub fn evaluate_once(trace: &[NQuin], p: u64) -> bool {
168    trace.iter().any(|q| q.predicate == p)
169}
170
171/// **Historically** `H p` (past □): `p` held at *every* point in the trace (dual of `Globally`).
172/// Vacuously true on an empty trace (nothing in the past violated it).
173pub fn evaluate_historically(trace: &[NQuin], p: u64) -> bool {
174    trace.iter().all(|q| q.predicate == p)
175}
176
177/// **Since** `p S q`: at the end of the trace, `q` held at some past point and `p` has held at
178/// every point since (inclusive of after `q`). Retrospective legal analysis ("the duty has held
179/// since the breach"). Zero-heap.
180pub fn evaluate_since(trace: &[NQuin], p: u64, q: u64) -> bool {
181    // Find the latest index where q held; require p at every index after it.
182    let mut q_at: Option<usize> = None;
183    for (i, ev) in trace.iter().enumerate() {
184        if ev.predicate == q {
185            q_at = Some(i);
186        }
187    }
188    match q_at {
189        None => false,
190        Some(qi) => trace[qi + 1..].iter().all(|ev| ev.predicate == p),
191    }
192}
193
194// ─── Büchi-style streaming monitor (continuous safety monitoring) ─────────────────
195
196/// An incremental monitor for the safety fragment `G(p)` ("`p` always holds") — the practical
197/// Büchi-automaton acceptance for stream monitoring: it stays `Safe` while every streamed event
198/// satisfies `p`, and latches to `Violated` permanently on the first event that does not. Zero-heap.
199#[derive(Debug, Clone, Copy, PartialEq, Eq)]
200pub struct SafetyMonitor {
201    pub invariant: u64,
202    pub violated: bool,
203}
204
205impl SafetyMonitor {
206    /// Start monitoring `G(invariant)`.
207    pub fn new(invariant: u64) -> Self {
208        Self {
209            invariant,
210            violated: false,
211        }
212    }
213    /// Feed the next streamed event predicate; returns `true` while still safe.
214    pub fn step(&mut self, event_predicate: u64) -> bool {
215        if event_predicate != self.invariant {
216            self.violated = true;
217        }
218        !self.violated
219    }
220    /// Is the monitored safety property still holding?
221    #[inline]
222    pub fn is_safe(&self) -> bool {
223        !self.violated
224    }
225}
226
227// ─── Allen-interval bridge ────────────────────────────────────────────────────────
228
229/// Extract the `[first, last]` timestamp interval over which `predicate` occurs in the timed
230/// `trace` (each event's timestamp in `metadata`), or `None` if it never occurs. The bridge to
231/// the Allen Interval Algebra (`interval_reasoning::allen_relation` relates two such intervals).
232pub fn predicate_interval(trace: &[NQuin], predicate: u64) -> Option<(u64, u64)> {
233    let mut lo: Option<u64> = None;
234    let mut hi: Option<u64> = None;
235    for q in trace {
236        if q.predicate == predicate {
237            lo = Some(lo.map_or(q.metadata, |v| v.min(q.metadata)));
238            hi = Some(hi.map_or(q.metadata, |v| v.max(q.metadata)));
239        }
240    }
241    Some((lo?, hi?))
242}
243
244#[cfg(test)]
245mod tests {
246    use super::*;
247    use crate::NQuin;
248
249    fn timed(predicate: u64, t: u64) -> NQuin {
250        NQuin {
251            subject: 0,
252            predicate,
253            object: 0,
254            context: 0,
255            metadata: t,
256            parity: 0,
257        }
258    }
259
260    #[test]
261    fn test_mtl_holds_within() {
262        let breach = 1u64;
263        let remedy = 2u64;
264        // breach at t=10, remedy at t=25 → within window 30.
265        let trace = [timed(breach, 10), timed(remedy, 25)];
266        assert!(
267            holds_within(&trace, breach, remedy, 30),
268            "remedy 15 after breach ≤ 30 window"
269        );
270        assert!(
271            !holds_within(&trace, breach, remedy, 10),
272            "remedy 15 after breach > 10 window"
273        );
274        // remedy before the breach does not count.
275        let late = [timed(remedy, 5), timed(breach, 10)];
276        assert!(
277            !holds_within(&late, breach, remedy, 30),
278            "a remedy before the breach is not within"
279        );
280        // no trigger → false.
281        assert!(!holds_within(&[timed(remedy, 25)], breach, remedy, 30));
282    }
283
284    fn make_quin(predicate: u64) -> NQuin {
285        NQuin {
286            subject: 0,
287            predicate,
288            object: 0,
289            context: 0,
290            metadata: 0,
291            parity: 0,
292        }
293    }
294
295    #[test]
296    fn test_ltl_globally() {
297        let p = 100;
298        let q_p = make_quin(p);
299        let q_not_p = make_quin(99);
300
301        assert!(evaluate_ltl_trace(
302            &[q_p, q_p, q_p],
303            &LtlFormula::Globally(p)
304        ));
305        assert!(!evaluate_ltl_trace(
306            &[q_p, q_not_p, q_p],
307            &LtlFormula::Globally(p)
308        ));
309        assert!(!evaluate_ltl_trace(&[], &LtlFormula::Globally(p)));
310    }
311
312    #[test]
313    fn test_ltl_finally() {
314        let p = 100;
315        let q_p = make_quin(p);
316        let q_not_p = make_quin(99);
317
318        assert!(evaluate_ltl_trace(
319            &[q_not_p, q_not_p, q_p],
320            &LtlFormula::Finally(p)
321        ));
322        assert!(!evaluate_ltl_trace(
323            &[q_not_p, q_not_p],
324            &LtlFormula::Finally(p)
325        ));
326        assert!(!evaluate_ltl_trace(&[], &LtlFormula::Finally(p)));
327    }
328
329    #[test]
330    fn test_ltl_next() {
331        let p = 100;
332        let q_p = make_quin(p);
333        let q_not_p = make_quin(99);
334
335        assert!(evaluate_ltl_trace(&[q_not_p, q_p], &LtlFormula::Next(p)));
336        assert!(!evaluate_ltl_trace(&[q_p, q_not_p], &LtlFormula::Next(p)));
337        assert!(!evaluate_ltl_trace(&[q_p], &LtlFormula::Next(p)));
338        assert!(!evaluate_ltl_trace(&[], &LtlFormula::Next(p)));
339    }
340
341    #[test]
342    fn test_ltl_until() {
343        let p = 100;
344        let q = 200;
345        let q_p = make_quin(p);
346        let q_q = make_quin(q);
347        let q_other = make_quin(99);
348
349        assert!(evaluate_ltl_trace(
350            &[q_p, q_p, q_q],
351            &LtlFormula::Until {
352                ante: p,
353                consequent: q
354            }
355        ));
356        assert!(evaluate_ltl_trace(
357            &[q_q],
358            &LtlFormula::Until {
359                ante: p,
360                consequent: q
361            }
362        ));
363        assert!(!evaluate_ltl_trace(
364            &[q_p, q_p, q_p],
365            &LtlFormula::Until {
366                ante: p,
367                consequent: q
368            }
369        ));
370        assert!(!evaluate_ltl_trace(
371            &[q_p, q_other, q_q],
372            &LtlFormula::Until {
373                ante: p,
374                consequent: q
375            }
376        ));
377        assert!(!evaluate_ltl_trace(
378            &[],
379            &LtlFormula::Until {
380                ante: p,
381                consequent: q
382            }
383        ));
384    }
385
386    #[test]
387    fn test_ltl_release() {
388        let trigger = 100;
389        let invariant = 200;
390        let q_t = make_quin(trigger);
391        let q_i = make_quin(invariant);
392        let q_other = make_quin(99);
393
394        assert!(evaluate_ltl_trace(
395            &[q_i, q_i, q_i],
396            &LtlFormula::Release { trigger, invariant }
397        ));
398        assert!(evaluate_ltl_trace(
399            &[q_i, q_t, q_other],
400            &LtlFormula::Release { trigger, invariant }
401        ));
402        assert!(!evaluate_ltl_trace(
403            &[q_i, q_other, q_t],
404            &LtlFormula::Release { trigger, invariant }
405        ));
406        assert!(evaluate_ltl_trace(
407            &[],
408            &LtlFormula::Release { trigger, invariant }
409        ));
410    }
411
412    #[test]
413    fn past_time_ltl_once_historically_since() {
414        let (breach, duty, repaired) = (1u64, 2u64, 3u64);
415        let trace = [make_quin(breach), make_quin(duty), make_quin(duty)];
416        // Once: breach happened at some past point.
417        assert!(evaluate_once(&trace, breach));
418        assert!(!evaluate_once(&trace, repaired));
419        // Historically: duty did NOT hold at every point (breach was first).
420        assert!(!evaluate_historically(&trace, duty));
421        assert!(evaluate_historically(
422            &[make_quin(duty), make_quin(duty)],
423            duty
424        ));
425        // Since: the duty has held since the breach (every point after breach is duty).
426        assert!(evaluate_since(&trace, duty, breach));
427        // Not "since" if the consequent never held.
428        assert!(!evaluate_since(&trace, duty, repaired));
429    }
430
431    #[test]
432    fn streaming_safety_monitor_latches_on_violation() {
433        let safe = 100u64;
434        let mut mon = SafetyMonitor::new(safe);
435        assert!(mon.step(safe) && mon.step(safe), "still safe");
436        assert!(!mon.step(999), "a non-conforming event violates G(p)");
437        assert!(!mon.step(safe), "violation latches permanently");
438        assert!(!mon.is_safe());
439    }
440
441    #[test]
442    fn metric_globally_and_allen_interval() {
443        let (start, ok, bad) = (1u64, 2u64, 3u64);
444        // From trigger@10, invariant `ok` holds across the window [10,40].
445        let good = [timed(start, 10), timed(ok, 20), timed(ok, 35)];
446        assert!(holds_globally_within(&good, start, ok, 30));
447        // A bad event inside the window breaks it.
448        let broken = [timed(start, 10), timed(bad, 25)];
449        assert!(!holds_globally_within(&broken, start, ok, 30));
450        // Allen-interval extraction: `ok` spans [20,35].
451        assert_eq!(predicate_interval(&good, ok), Some((20, 35)));
452        assert_eq!(predicate_interval(&good, bad), None);
453    }
454}
qualia_core_db/modalities/temporal_ltl.rs

qualia_core_db/modalities/
temporal_ltl.rs
