pub trait Oracle: Clone + Sync {
// Required methods
fn update_state(&mut self, state: &[bool]);
fn update_time(&mut self, time: Time);
fn output_assumes(&self) -> impl Iterator<Item = Option<bool>>;
fn output_guarantees(&self) -> impl Iterator<Item = Option<bool>>;
fn final_output_assumes(&self) -> impl Iterator<Item = bool>;
fn final_output_guarantees(&self) -> impl Iterator<Item = bool>;
}Expand description
Implementators are induced by a temporal property. They can update their internal state when fed a new state of a trace, and establish whether their corresponding property holds on such trace.
Required Methods§
Sourcefn update_state(&mut self, state: &[bool])
fn update_state(&mut self, state: &[bool])
Update the internal state of the Oracle with the latest state of a temporal trace.
Sourcefn update_time(&mut self, time: Time)
fn update_time(&mut self, time: Time)
Update the internal state of the Oracle with the latest state of a temporal trace.
Sourcefn output_assumes(&self) -> impl Iterator<Item = Option<bool>>
fn output_assumes(&self) -> impl Iterator<Item = Option<bool>>
Returns the values of the “assume” properties, if already determined.
Sourcefn output_guarantees(&self) -> impl Iterator<Item = Option<bool>>
fn output_guarantees(&self) -> impl Iterator<Item = Option<bool>>
Returns the values of the “guarantee” properties, if already determined.
Sourcefn final_output_assumes(&self) -> impl Iterator<Item = bool>
fn final_output_assumes(&self) -> impl Iterator<Item = bool>
As the trace ends, the values of the “assume” properties is determined to be either true or false.
Sourcefn final_output_guarantees(&self) -> impl Iterator<Item = bool>
fn final_output_guarantees(&self) -> impl Iterator<Item = bool>
As the trace ends, the values of the “guarantee” properties is determined to be either true or false.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.