scan_core/oracle.rs
1mod mtl;
2mod pmtl;
3
4use crate::Time;
5pub use mtl::{Mtl, MtlOracle};
6pub use pmtl::{Pmtl, PmtlOracle};
7
8/// Implementators are induced by a temporal property.
9/// They can update their internal state when fed a new state of a trace,
10/// and establish whether their corresponding property holds on such trace.
11pub trait Oracle: Clone + Sync {
12 /// Update the internal state of the [`Oracle`] with the latest state of a temporal trace.
13 fn update_state(&mut self, state: &[bool]);
14
15 /// Update the internal state of the [`Oracle`] with the latest state of a temporal trace.
16 fn update_time(&mut self, time: Time);
17
18 /// Returns the values of the "assume" properties,
19 /// if already determined.
20 fn output_assumes(&self) -> impl Iterator<Item = Option<bool>>;
21
22 /// Returns the values of the "guarantee" properties,
23 /// if already determined.
24 fn output_guarantees(&self) -> impl Iterator<Item = Option<bool>>;
25
26 /// As the trace ends, the values of the "assume" properties is determined to be either true or false.
27 fn final_output_assumes(&self) -> impl Iterator<Item = bool>;
28
29 /// As the trace ends, the values of the "guarantee" properties is determined to be either true or false.
30 fn final_output_guarantees(&self) -> impl Iterator<Item = bool>;
31}