Skip to main content

Crate mstlo

Crate mstlo 

Source
Expand description

§mstlo - Online Signal Temporal Logic

mstlo provides runtime and macro-based tooling to parse, build, and execute Signal Temporal Logic (STL) monitors over streaming data.

It includes:

  • a high-level monitor builder API,
  • incremental evaluation backend,
  • multiple semantics (qualitative, quantitative, RoSI), and
  • optional multi-signal synchronization/interpolation.

§Simple usage

   use mstlo::monitor::*;
   use mstlo::{step, stl};

   // Build a monitor from the macro DSL.
   let formula = stl!(G[0, 1](x > 5.0));
   let mut monitor = StlMonitor::builder()
       .formula(formula)
       .algorithm(Algorithm::Incremental)
       .semantics(DelayedQuantitative)
       .build()
       .unwrap();

   // Stream updates
   let out1 = monitor.update(&step!("x", 7.0, 0s));
   let out2 = monitor.update(&step!("x", 6.0, 1s));
   let out3 = monitor.update(&step!("x", 4.0, 2s));
   let out4 = monitor.update(&step!("x", 7.0, 3s));

   assert_eq!(out1.verdicts(), vec![]);
   assert_eq!(out2.verdicts(), vec![step!("x", 1.0, 0s)]);
   assert_eq!(out3.verdicts(), vec![step!("x", -1.0, 1s)]);
   assert_eq!(out4.verdicts(), vec![step!("x", -1.0, 2s)]);

Re-exports§

pub use monitor::semantic_markers::DelayedQualitative;
pub use monitor::semantic_markers::DelayedQuantitative;
pub use monitor::semantic_markers::EagerQualitative;
pub use monitor::semantic_markers::Rosi;
pub use monitor::semantic_markers::SemanticType;
pub use monitor::Algorithm;
pub use monitor::MonitorOutput;
pub use monitor::Semantics;
pub use monitor::StlMonitor;
pub use monitor::StlMonitorBuilder;
pub use monitor::SyncStepResult;

Modules§

monitor
High-level STL monitor API.

Macros§

step
Convenience macro to construct a ::mstlo::Step.
stl
The main entry point for the stl! procedural macro.

Structs§

ParseError
Error type for STL formula parsing.
RingBuffer
VecDeque-backed ring buffer for timestamped signal steps.
RobustnessInterval
Interval-valued robustness, represented as (lower, upper) bounds.
Step
A single sampled value of a named signal at a given timestamp.
Synchronizer
Synchronizer struct that handles interpolation of missing steps across multiple signals. It maintains a timeline of all timestamps and the last known step for each active signal. A signal is considered active if it has received at least one step.
TimeInterval
Closed temporal interval $[start, end]$ used by STL temporal operators.
Variables
A container for runtime variable bindings.

Enums§

FormulaDefinition
An enum representing the definition of an STL formula.
SynchronizationStrategy
Strategy used to synthesize missing samples at known timeline timestamps.

Traits§

Interpolatable
Value requirements for synchronization interpolation.
RingBufferTrait
Common interface for timestamped ring buffers.
RobustnessSemantics
Semantic operations required by STL operators for a robustness domain.
SignalIdentifier
Trait for extracting referenced signal names from operator/formula trees.

Functions§

get_formulas
Returns the vector of Signal Temporal Logic formulas. If ids is not empty, returns only the formulas with the specified IDs.
parse_stl
Parse an STL formula from a string.