Struct PmtlOracle 

pub struct PmtlOracle { /* private fields */ }

An oracle for PMTL properties over timed, dense traces.

Implementations

impl PmtlOracle

pub fn new(assumes: &[Pmtl<usize>], guarantees: &[Pmtl<usize>]) -> Self

Creates an oracle from assumes and guarantees PMTL formulae.

Trait Implementations

impl Clone for PmtlOracle

fn clone(&self) -> PmtlOracle

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PmtlOracle

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

Formats the value using the given formatter.

impl Oracle for PmtlOracle

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_state(&mut self, state: &[bool])

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

fn update_time(&mut self, time: Time)

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