1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

use super::Bounds;
use crate::trace::Trace;
use crate::{Formula, Metric};

pub struct Always<P> {
    phi: P,
    bounds: Option<Bounds>,
}

impl<P> Always<P> {
    pub fn new(phi: P) -> Always<P> {
        Always { phi, bounds: None }
    }

    pub fn new_bounded<B: Into<Bounds>>(phi: P, bounds: B) -> Self {
        Self {
            phi,
            bounds: Some(bounds.into()),
        }
    }
}

impl<T, P> Formula<Trace<T>> for Always<P>
where
    P: Formula<Trace<T>>,
{
    type Error = P::Error;

    fn satisfied_by(&self, trace: &Trace<T>) -> Result<bool, Self::Error> {
        let mut bounded_trace = trace.clone();

        if let Some(bounds) = &self.bounds {
            bounded_trace.retain_between(bounds.lower.into_inner(), bounds.upper.into_inner());
        }

        let subtraces = bounded_trace.into_subtraces();

        for subtrace in subtraces {
            let result = self.phi.satisfied_by(&subtrace)?;

            if !result {
                return Ok(false);
            }
        }

        Ok(true)
    }
}

impl<T, P> Metric<Trace<T>> for Always<P>
where
    P: Metric<Trace<T>>,
{
    type Error = P::Error;

    fn distance(&self, trace: &Trace<T>) -> Result<f64, Self::Error> {
        let mut bounded_trace = trace.clone();

        if let Some(bounds) = &self.bounds {
            bounded_trace.retain_between(bounds.lower.into_inner(), bounds.upper.into_inner());
        }

        let subtraces = bounded_trace.into_subtraces();
        let mut min_dist = f64::INFINITY;

        for subtrace in subtraces {
            let dist = self.phi.distance(&subtrace)?;
            min_dist = f64::min(dist, min_dist);
        }

        Ok(min_dist)
    }
}