Struct SafetyMonitor 

pub struct SafetyMonitor {
    pub invariant: u64,
    pub violated: bool,
}

An incremental monitor for the safety fragment G(p) (“p always holds”) — the practical Büchi-automaton acceptance for stream monitoring: it stays Safe while every streamed event satisfies p, and latches to Violated permanently on the first event that does not. Zero-heap.

Fields

invariant: u64

violated: bool

Implementations

impl SafetyMonitor

pub fn new(invariant: u64) -> Self

Start monitoring G(invariant).

pub fn step(&mut self, event_predicate: u64) -> bool

Feed the next streamed event predicate; returns true while still safe.

pub fn is_safe(&self) -> bool

Is the monitored safety property still holding?

Trait Implementations

impl Clone for SafetyMonitor

fn clone(&self) -> SafetyMonitor

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SafetyMonitor

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

Formats the value using the given formatter.

impl PartialEq for SafetyMonitor

fn eq(&self, other: &SafetyMonitor) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for SafetyMonitor

impl Eq for SafetyMonitor

impl StructuralPartialEq for SafetyMonitor