Sometimes you need a monitor to run forever on a live stream and SENTIL's online monitrs do just this. SENTIL's online monitors fold one timestamped sample at a time into a running verdict.

The example drives a sine wave through the property that x stays above -0.9 over a sliding ten-step window.

The program

online_streaming.py

import math
import sentil

monitor = sentil.OnlineMonitor("G[0, 10] (x > -0.9)")
for t in range(60):
    x = math.sin(t * 0.3)
    verdict = monitor.update(float(t), {"x": x})
    if verdict.resolved and not verdict.satisfied:
        print(f"violated at t={t}, robustness={verdict.value:.3f}")
        break
else:
    print("held over the whole stream")

online_streaming.rs

use sentil::{Monitor, MonitorConfig};

fn main() -> sentil::Result<()> {
    let mut monitor = Monitor::new("G[0, 10] (x > -0.9)", MonitorConfig::new())?;
    for t in 0..60 {
        let x = (f64::from(t) * 0.3).sin();
        let verdict = monitor.update(f64::from(t), &[("x", x)])?;
        if verdict.is_resolved() && verdict.value() < 0.0 {
            println!("violated at t={t}, robustness={:.3}", verdict.value());
            return Ok(());
        }
    }
    println!("held over the whole stream");
    Ok(())
}

online_streaming.cpp

#include <sentil/sentil.hpp>
#include <cmath>
#include <cstdio>

int main() {
    sentil::OnlineMonitor monitor("G[0, 10] (x > -0.9)");
    for (int t = 0; t < 60; ++t) {
        double x = std::sin(t * 0.3);
        sentil::Robustness verdict = monitor.update(static_cast<double>(t), {{"x", x}});
        if (verdict.resolved && !verdict.satisfied) {
            std::printf("violated at t=%d, robustness=%.3f\n", t, verdict.value);
            return 0;
        }
    }
    std::printf("held over the whole stream\n");
    return 0;
}

online_streaming.c

#include "sentil.h"
#include <math.h>
#include <stdio.h>

int main(void) {
    sentil_monitor_t *monitor = sentil_monitor_parse("G[0, 10] (x > -0.9)", NULL);
    const char *names[] = {"x"};
    for (int t = 0; t < 60; ++t) {
        double x = sin(t * 0.3);
        sentil_robustness_t out;
        sentil_monitor_update(monitor, (double)t, names, &x, 1, &out);
        if (out.resolved && !out.satisfied) {
            printf("violated at t=%d, robustness=%.3f\n", t, out.value);
            sentil_monitor_destroy(monitor);
            return 0;
        }
    }
    printf("held over the whole stream\n");
    sentil_monitor_destroy(monitor);
    return 0;
}

OnlineStreaming.java

import io.github.sedislab.sentil.OnlineMonitor;
import io.github.sedislab.sentil.Robustness;
import java.util.Collections;

public class OnlineStreaming {
    public static void main(String[] args) throws Exception {
        try (OnlineMonitor monitor = OnlineMonitor.create("G[0, 10] (x > -0.9)")) {
            for (int t = 0; t < 60; t++) {
                double x = Math.sin(t * 0.3);
                Robustness verdict = monitor.update(t, Collections.singletonMap("x", x));
                if (verdict.resolved() && !verdict.satisfied()) {
                    System.out.printf("violated at t=%d, robustness=%.3f%n", t, verdict.value());
                    return;
                }
            }
            System.out.println("held over the whole stream");
        }
    }
}

online_streaming.jl

using Sentil

monitor = OnlineMonitor("G[0, 10] (x > -0.9)")
for t in 0:59
    x = sin(t * 0.3)
    verdict = update!(monitor, Float64(t), Dict("x" => x))
    if verdict.resolved && !verdict.satisfied
        println("violated at t=", t, ", robustness=", round(verdict.value; digits = 3))
        break
    end
end

online_streaming.m

monitor = sentil.OnlineMonitor('G[0, 10] (x > -0.9)');
for t = 0:59
    x = sin(t * 0.3);
    verdict = monitor.update(t, struct('x', x));
    if verdict.resolved && ~verdict.satisfied
        fprintf('violated at t=%d, robustness=%.3f\n', t, verdict.value);
        return
    end
end
fprintf('held over the whole stream\n');

online_streaming.sh

awk 'BEGIN { for (t = 0; t < 60; t++) printf "{\"time\":%d,\"x\":%.6f}\n", t, sin(t * 0.3) }' \
  | sentil monitor -f 'G[0, 10] (x > -0.9)' -o ndjson

The monitor subcommand reads one JSON sample per line and writes one verdict per line, so it drops into a pipe between a sensor feed and whatever consumes the verdict. Here awk generates the same sine stream the other tabs compute in code.

The verdict has three fields

Running the Python version prints:

violated at t=15, robustness=-0.078

At $t = 15$ , the wave reads $\sin(4.5) = -0.978$ , which is 0.078 below the -0.9 bound. Because of this, the verdict resolves to a violation with margin -0.078.

Each update returns a small verdict record. resolved says whether the monitor has seen enough of the future to commit to a final answer for the current time. satisfied is the sign of the verdict once it resolves. value is the robustness.

The distinction between resolved and unresolved is what a bounded future operator forces. G[0, 10](x > -0.9) at time $t$ depends on samples out to $t + 10$ , so until those arrive the verdict for $t$ is provisional and the monitor reports the tightest bound it can from what it has seen, and sets resolved to false. The moment an incoming sample drives the window below the bound, the verdict resolves to a violation.

Why streaming stays flat

The bounded operators run on a monotonic-deque sliding minimum and maximum, so each sample costs O(1) amortized work and memory stays proportional to the window. See why the deque is O(1) amortized. On the streaming benchmark, that comes out to a per-sample median of 110 nanoseconds with a p99 of 150 nanoseconds, about nine million updates a second, and the footprint stays fixed no matter how long the stream runs.

For handling bounded operators in a stream, see bounded operators. To monitor a probabilistic property online, see checking a PrSTL property.

Online streaming

The program

The verdict has three fields

Why streaming stays flat

On this page