scan_core/oracle/
mtl.rs

1use crate::{Oracle, Time};
2
3/// An Metric Temporal Logic (MTL) formula.
4#[derive(Debug, Clone)]
5pub enum Mtl<V: Clone> {
6    /// An atomic proposition in an [`Mtl`] formula.
7    Atom(V),
8    /// An [`Mtl`] formula of the form `p U q`.
9    Until(V, V),
10}
11
12/// An oracle for (simple) [`Mtl`] properties.
13///
14/// Currently limited to properties of the form `p U q`.
15#[derive(Debug, Default, Clone)]
16pub struct MtlOracle {
17    assumes: Vec<(Mtl<usize>, Option<bool>)>,
18    guarantees: Vec<(Mtl<usize>, Option<bool>)>,
19    time: Time,
20}
21
22impl MtlOracle {
23    /// Add a new guarantee property to the [`Oracle`].
24    pub fn add_guarantee(&mut self, mtl: Mtl<usize>) {
25        self.guarantees.push((mtl, None));
26    }
27
28    /// Add a new assume property to the [`Oracle`].
29    pub fn add_assume(&mut self, mtl: Mtl<usize>) {
30        self.guarantees.push((mtl, None));
31    }
32}
33
34impl Oracle for MtlOracle {
35    fn update_state(&mut self, state: &[bool]) {
36        self.guarantees
37            .iter_mut()
38            .chain(self.assumes.iter_mut())
39            .for_each(|(mtl, opt)| {
40                *opt = match mtl {
41                    Mtl::Atom(i) => state.get(*i).cloned(),
42                    Mtl::Until(lhs, rhs) => {
43                        if opt.is_some() {
44                            *opt
45                        } else if state.get(*rhs).is_some_and(|b| *b) {
46                            Some(true)
47                        } else if state.get(*lhs).is_some_and(|b| *b) {
48                            None
49                        } else {
50                            Some(false)
51                        }
52                    }
53                }
54            })
55    }
56
57    fn output_assumes(&self) -> impl Iterator<Item = Option<bool>> {
58        self.assumes.iter().map(|(_, opt)| *opt)
59    }
60
61    fn output_guarantees(&self) -> impl Iterator<Item = Option<bool>> {
62        self.guarantees.iter().map(|(_, opt)| *opt)
63    }
64
65    fn final_output_assumes(&self) -> impl Iterator<Item = bool> {
66        self.assumes.iter().map(|(_, opt)| opt.unwrap_or(false))
67    }
68
69    fn final_output_guarantees(&self) -> impl Iterator<Item = bool> {
70        self.guarantees.iter().map(|(_, opt)| opt.unwrap_or(false))
71    }
72
73    fn update_time(&mut self, time: Time) {
74        self.time = time;
75    }
76}
scan_core/oracle/mtl.rs

scan_core/oracle/
mtl.rs
