Struct LinearTemporalLogic 

pub struct LinearTemporalLogic {
    pub formula: String,
}

A Linear Temporal Logic (LTL) formula represented as a string.

The current implementation uses a simplified embedded DSL rather than a full LTL parser.

Fields

formula: String

The LTL formula expressed in textual form.

Implementations

impl LinearTemporalLogic

pub fn new(formula: impl Into<String>) -> Self

Create a new LTL formula.

pub fn check_safety<S, F>(&self, trace: &[S], predicate: F) -> bool

where F: Fn(&S) -> bool,

Check a safety property: returns true if the formula is satisfied for all positions in trace.

Safety properties have the form “always P” – here predicate is evaluated on every state.

pub fn check_liveness<S, F>(&self, trace: &[S], predicate: F) -> bool

where F: Fn(&S) -> bool,

Check a liveness property: returns true if predicate is true at least once in trace.

Liveness properties have the form “eventually P”.

pub fn check_next<S, F, G>(&self, trace: &[S], trigger: F, predicate: G) -> bool

where F: Fn(&S) -> bool, G: Fn(&S) -> bool,

Check a “next” property: returns true if predicate holds at every state immediately following a state where trigger holds.

pub fn check_until<S, F, G>(&self, trace: &[S], left: F, right: G) -> bool

where F: Fn(&S) -> bool, G: Fn(&S) -> bool,

Check an “until” property: left must hold until right holds.

Trait Implementations

impl Clone for LinearTemporalLogic

fn clone(&self) -> LinearTemporalLogic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LinearTemporalLogic

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

Formats the value using the given formatter.