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