logic/operators/
eventually.rs

1use super::Bounds;
2use crate::trace::Trace;
3use crate::{Formula, Metric};
4
5pub struct Eventually<P> {
6    phi: P,
7    bounds: Option<Bounds>,
8}
9
10impl<P> Eventually<P> {
11    pub fn new(phi: P) -> Eventually<P> {
12        Eventually { phi, bounds: None }
13    }
14
15    pub fn new_bounded<B: Into<Bounds>>(bounds: B, phi: P) -> Self {
16        Self {
17            phi,
18            bounds: Some(bounds.into()),
19        }
20    }
21}
22
23impl<T, P> Formula<Trace<T>> for Eventually<P>
24where
25    P: Formula<Trace<T>>,
26{
27    type Error = P::Error;
28
29    fn satisfied_by(&self, trace: &Trace<T>) -> Result<bool, Self::Error> {
30        let mut bounded_trace = trace.clone();
31
32        if let Some(bounds) = &self.bounds {
33            bounded_trace.retain_between(bounds.lower.into_inner(), bounds.upper.into_inner());
34        }
35
36        let subtraces = bounded_trace.into_subtraces();
37
38        for subtrace in subtraces {
39            let result = self.phi.satisfied_by(&subtrace)?;
40
41            if result {
42                return Ok(true);
43            }
44        }
45
46        Ok(false)
47    }
48}
49
50impl<T, P> Metric<Trace<T>> for Eventually<P>
51where
52    P: Metric<Trace<T>>,
53{
54    type Error = P::Error;
55
56    fn distance(&self, trace: &Trace<T>) -> Result<f64, Self::Error> {
57        let mut bounded_trace = trace.clone();
58
59        if let Some(bounds) = &self.bounds {
60            bounded_trace.retain_between(bounds.lower.into_inner(), bounds.upper.into_inner());
61        }
62
63        let subtraces = bounded_trace.into_subtraces();
64        let mut max_dist = f64::NEG_INFINITY;
65
66        for subtrace in subtraces {
67            let dist = self.phi.distance(&subtrace)?;
68            max_dist = f64::max(max_dist, dist);
69        }
70
71        Ok(max_dist)
72    }
73}
logic/operators/eventually.rs

logic/operators/
eventually.rs
