Struct MtlOracle 

pub struct MtlOracle { /* private fields */ }

An oracle for (simple) Mtl properties.

Currently limited to properties of the form p U q.

Implementations

impl MtlOracle

pub fn add_guarantee(&mut self, mtl: Mtl<usize>)

Add a new guarantee property to the Oracle.

pub fn add_assume(&mut self, mtl: Mtl<usize>)

Add a new assume property to the Oracle.

Trait Implementations

impl Clone for MtlOracle

fn clone(&self) -> MtlOracle

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for MtlOracle

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for MtlOracle

fn default() -> MtlOracle

Returns the “default value” for a type.

impl Oracle for MtlOracle

fn update_state(&mut self, state: &[bool])

Update the internal state of the Oracle with the latest state of a temporal trace.

fn output_assumes(&self) -> impl Iterator<Item = Option<bool>>

Returns the values of the “assume” properties, if already determined.

fn output_guarantees(&self) -> impl Iterator<Item = Option<bool>>

Returns the values of the “guarantee” properties, if already determined.

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.

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.

fn update_time(&mut self, time: Time)

Update the internal state of the Oracle with the latest state of a temporal trace.