logic/operators/
next.rs

1use super::error::TimedOperatorError;
2use crate::trace::Trace;
3use crate::{Formula, Metric};
4
5pub struct Next<P> {
6    phi: P,
7}
8
9impl<P> Next<P> {
10    pub fn new(phi: P) -> Next<P> {
11        Next { phi }
12    }
13}
14
15impl<T, P> Formula<Trace<T>> for Next<P>
16where
17    P: Formula<Trace<T>>,
18{
19    type Error = TimedOperatorError<P::Error>;
20
21    fn satisfied_by(&self, trace: &Trace<T>) -> Result<bool, Self::Error> {
22        if trace.len() < 1 {
23            return Err(TimedOperatorError::EmptyTrace);
24        }
25
26        let second_time = trace.times().nth(1);
27        let future_trace = second_time.and_then(|time| trace.clone().split_at(time));
28
29        match future_trace {
30            Some(future) => self
31                .phi
32                .satisfied_by(&future)
33                .map_err(TimedOperatorError::SubformulaError),
34            None => Ok(false),
35        }
36    }
37}
38
39impl<T, P> Metric<Trace<T>> for Next<P>
40where
41    P: Metric<Trace<T>>,
42{
43    type Error = TimedOperatorError<P::Error>;
44
45    fn distance(&self, trace: &Trace<T>) -> Result<f64, Self::Error> {
46        if trace.len() < 1 {
47            return Err(TimedOperatorError::EmptyTrace);
48        }
49
50        let second_time = trace.times().nth(1);
51        let future_trace = second_time.and_then(|time| trace.clone().split_at(time));
52
53        match future_trace {
54            Some(future) => self.phi.distance(&future).map_err(TimedOperatorError::SubformulaError),
55            None => Ok(f64::NEG_INFINITY),
56        }
57    }
58}