Rust

The sentil crate is the engine every other binding wraps. The first half of this page is a working tour and the second half is the complete reference. Snippets that use ? assume an enclosing function returning sentil::Result<()>.

Install

The crate is on crates.io, so we run cargo add sentil.

From crates.io

cargo add sentil

[dependencies]
sentil = { version = "0.3.0", features = ["gpu", "parquet"] }

cargo add sentil --no-default-features --features std

cargo tree -p sentil --depth 0   # sentil v0.3.0

From the repository tip

[dependencies]
sentil = { git = "https://github.com/sedislab/SENTIL" }

cargo tree -p sentil --depth 0

From source

You need a Rust toolchain from rustup.rs and a C compiler, since the default sqlite feature builds a bundled SQLite.

xcode-select --install

git clone https://github.com/sedislab/SENTIL
cd SENTIL
cargo build -p sentil

[dependencies]
sentil = { path = "../SENTIL/sentil-core" }

cargo run -p sentil --example offline_monitoring

robustness:       -1
per sample:       [-1.0, -1.0, -1.0, -1.0, 1.0]
dense robustness: -1

rust-toolchain.toml also installs the aarch64 and armv7 Linux targets, and .cargo/config.toml names the cross-linkers for the gnu ones. The prebuilt ARM archives and which board takes which are on the CLI page. The same checkout builds the CLI and the C ABI, and from source has those two commands.

First monitor

Build a trace, specify a formula, and see the robustness.

use sentil::{Formula, Trace};

fn main() -> sentil::Result<()> {
    let mut trace = Trace::new(vec![0.0, 1.0, 2.0, 3.0, 4.0])?;
    trace.add_signal("speed", vec![12.0, 9.0, 7.0, 4.0, 6.0])?;

    let phi = Formula::parse("G (speed > 5)")?;
    println!("robustness: {}", phi.robustness(&trace)?); // robustness: -1
    Ok(())
}

The robustness is $-1.0$. What STL is covers how to read the robustness. phi.robustness_signal(&trace)? returns the robustness at every sample, and phi.robustness_dense(&trace)? returns the dense robustness.

Traces

A Trace is one strictly increasing time vector with named, equal-length signals over it. Beyond Trace::new plus add_signal, you can read one from CSV text, from a file, or resample onto a new grid.

use sentil::{Interpolation, Trace};

let trace = Trace::from_csv_str("time,speed\n0,12\n1,9\n2,7\n3,4\n4,6")?;
assert_eq!(trace.variables(), vec!["speed"]);

let halves: Vec<f64> = (0..9).map(|i| f64::from(i) * 0.5).collect();
let fine = trace.resample(halves, Interpolation::Linear)?;
assert_eq!(fine.signal("speed").unwrap()[7], 5.0); // interpolated between 4 and 6 at t = 3.5

The time column is detected by name, or the first column is taken when no column is named time. The other columns that are not named time are treated as signals. time, timestamp, t, time_s, time_sec, time_ms, time_ns, elapsed, elapsed_time, epoch are all recognized as time columns.Trace::from_path picks a reader from the extension. We support CSVs, TSVs, text, MATLAB .mat files, Parquet, Arrow, SQLite, HDF5, and MCAP files. We go into more detail about trace formats in format features. Interpolation is Linear, ZeroOrderHold, or CubicSpline.

Streaming

For a live loop, Monitor folds one timestamped sample at a time and holds memory proportional to the largest temporal window, not the stream. Each update returns a Robustness verdict you can act on the instant it resolves.

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(())
}

This prints violated at t=15, robustness=-0.078. Until the ten-second window behind a sample has fully passed, is_resolved() stays false and value() reports a provisional midpoint. The bounded operators run on the monotonic deque, which is what keeps the per-sample cost flat. The benchmark sustains a median of 81 ns per sample and more than eleven million updates a second, well past a 10 kHz control loop. The deque page explains the structure and its proof.

On the hot path, skip the name lookup by just resolving each variable's slot once with symbol_index, then pushing plain slices.

let slot = monitor.symbol_index("x")?.expect("x is in the formula");
let mut values = [0.0];
for t in 0..60 {
    values[slot] = (f64::from(t) * 0.3).sin();
    monitor.update_packed(f64::from(t), &values)?;
}

A probabilistic formula streams the same way, and the running satisfaction estimate is readable at any instant through the live-probability accessor. Monitor::last_probability prints out the last probability and the StreamMonitor object shows you the full result.

use sentil::{Formula, LiftingRegistry, NoiseInteraction, NoiseModel, SmcConfig, StreamMonitor};

let phi = Formula::parse("P>=0.9 (G[0, 5] (x > 0))")?;
let mut lifting = LiftingRegistry::new();
lifting.register("x", NoiseModel::gaussian(0.0, 0.3)?, NoiseInteraction::Additive);
let config = SmcConfig { samples: 200, ..SmcConfig::default() };

let mut monitor = StreamMonitor::with_lifting(&phi, &lifting, &config)?;
for t in 0..20 {
    monitor.update(f64::from(t), &[("x", 0.8)])?;
    if let Some(p) = monitor.last_probability() {
        println!("running probability {p:.3}"); // 0.975 by the final sample
    }
}

Probabilistic checking

A formula like P>=0.9 (G (x > 0)) asks whether under noise the inner property holds with at least 90 percent probability. We give each channel a noise model, then call check on the formula.

use sentil::{Formula, LiftingRegistry, NoiseInteraction, NoiseModel, SmcConfig, Trace};

fn main() -> sentil::Result<()> {
    let times: Vec<f64> = (0..20).map(f64::from).collect();
    let mut trace = Trace::new(times)?;
    trace.add_signal("x", (0..20).map(|i| 0.4 + 0.05 * f64::from(i)).collect::<Vec<_>>())?;

    let mut lifting = LiftingRegistry::new();
    lifting.register("x", NoiseModel::gaussian(0.0, 0.3)?, NoiseInteraction::Additive);

    let phi = Formula::parse("P>=0.9 (G (x > 0))")?;
    let config = SmcConfig { samples: 5000, ..SmcConfig::default() };
    let result = phi.check(&trace, &lifting, &config)?;
    println!(
        "probability {:.3}, interval [{:.3}, {:.3}], holds {}",
        result.probability, result.interval.lower, result.interval.upper, result.holds
    );
    Ok(())
}

This prints probability 0.733, interval [0.721, 0.745], holds false. The early samples sit near 0.4, so noise with a 0.3 standard deviation pushes them below zero often enough that the 0.9 threshold fails, and the Wilson interval around the estimate says 5000 samples were plenty to be sure. register returns &mut Self for chaining, not a Result, so no ? goes after it. SmcConfig defaults to 10,000 samples, 0.95 confidence, seed 42, and the Wilson interval. What PrSTL is covers the operator, and confidence intervals the surety about the estimate.

Instead of check, you can use check_conservative to rerun the verdict with the Clopper-Pearson exact interval or check_distribution which returns how the inner robustness spread across the ensemble.

Sequential tests

A sequential test draws only as many samples as the decision needs as compared to a fixed-budget test. Wald's SPRT decides between an indifference region's two hypotheses with bounded error rates:

use sentil::{SprtConfig, SprtResult};

let sprt = SprtConfig::new(0.85, 0.95, 0.05, 0.05, 10_000)?;
match phi.check_sequential(&trace, &lifting, &sprt)? {
    SprtResult::AcceptH1 { samples } => println!("holds, decided after {samples} draws"),
    SprtResult::AcceptH0 { samples } => println!("fails, decided after {samples} draws"),
    SprtResult::Inconclusive { samples, .. } => println!("undecided after {samples} draws"),
}

On a trace that clearly satisfies the property, this decides after a few dozen draws where the fixed-budget check would burn thousands. The Bayesian alternative starts from a uniform Beta(1, 1) prior and stops when the Bayes factor clears a cutoff:

use sentil::{BayesConfig, BayesResult};

let bayes = BayesConfig::new(0.9, 100.0, 10_000)?;
match phi.check_bayesian(&trace, &lifting, &bayes)? {
    BayesResult::Holds { samples, posterior } => println!("holds after {samples} draws, posterior {posterior:.3}"),
    BayesResult::Fails { samples, .. } => println!("fails after {samples} draws"),
    BayesResult::Inconclusive { samples, .. } => println!("undecided after {samples} draws"),
}

The SPRT concept page derives the decision bounds and statistical methods compares the three methods.

Rare events

Below probabilities below $10^{-5}$, plain Monte Carlo ceases to be effective. The rare-event path runs adaptive multilevel splitting over a StochasticSystem and is able to resolve probabilities down to $10^{-12}$ or lower.

use sentil::{Formula, NoiseModel, RareEventConfig, StochasticSystem};

// A random walk with Gaussian steps; drifting past 12 within the horizon is rare.
let step = NoiseModel::gaussian(0.0, 0.3)?;
let system = StochasticSystem::new(["x"], 1.0, 100, |_rng| vec![0.0], move |prev, _t, rng| {
    vec![prev[0] + step.sample(rng)]
})?;

let phi = Formula::parse("P>=0.9999 (G (x < 12))")?;
let config = RareEventConfig { particles: 4096, ..RareEventConfig::default() };
let result = phi.check_rare_event(&system, &config)?;
println!(
    "violation probability {:.2e} from {} simulations, holds {}",
    result.violation_probability, result.simulations, result.holds
);

This resolves a violation probability near $5 \times 10^{-5}$, far below what 4096 plain samples could see. The inner formula should be a G, over a predicate. The rare events page explains the algorithm, and the GPU guide covers the gpu-feature path for large particle counts.

Synthesis

Given a system model and a spec, can we find the input that satisfies it? This is the problem that Synthesis seeks to solve. The default backend is projected gradient ascent on a smooth robustness.

use sentil::{Backend, Bounds, Formula, LinearModel, SynthesisProblem, Synthesizer};

fn main() -> sentil::Result<()> {
    // A single integrator x_{t+1} = x_t + u_t, five steps from x0 = 0.
    let model = LinearModel::new(vec![vec![1.0]], vec![vec![1.0]], [0.0], ["pos"], 1.0, 5)?;
    let spec = Formula::parse("F[0, 5] (pos > 2)")?;

    let problem = SynthesisProblem::new(&model, &spec)
        .with_bounds(Bounds::new(vec![-1.0; 5], vec![1.0; 5])?)
        .with_backend(Backend::Gradient)
        .with_budget(200);
    let result = Synthesizer::solve(&problem)?;
    println!(
        "input {:?}, robustness {:.3}, holds {}",
        result.input, result.robustness, result.holds
    );
    Ok(())
}

This finds input [1.0, 1.0, 1.0, 1.0, 1.0] with robustness 3.0: pushing at full bound reaches position 5, three units past the target. An infeasible spec returns the least-violating input rather than an error. Online, Controller re-plans a short horizon every step inside a hard deadline:

use std::time::Duration;
use sentil::{Bounds, Controller, Formula, LinearModel};

let model = LinearModel::new(vec![vec![1.0]], vec![vec![1.0]], [0.0], ["pos"], 1.0, 8)?;
let spec = Formula::parse("F[0, 8] (pos > 2)")?;
let mut controller = Controller::new(&model, &spec, 1, Duration::from_millis(5))
    .with_bounds(Bounds::new(vec![-1.0; 8], vec![1.0; 8])?);

let mut state = vec![0.0];
for _ in 0..8 {
    let u = controller.control(&state)?;
    state[0] += u[0]; // ends at 8.0, well past the target
}

The same machinery searches in reverse: spec.falsify(&model, &bounds, CmaConfig::default(), 3)? hunts for a violating input and returns it as a Witness, and mine_tightest_parameter finds the sharpest constant a spec supports on recorded traces. On the first-monitor trace it recovers exactly the dip:

use sentil::mine_tightest_parameter;

let traces = [trace]; // the first-monitor trace
let c = mine_tightest_parameter(
    |c| Formula::parse(&format!("G (speed > {c})")),
    &traces,
    0.0,
    20.0,
)?;
// c is 4.000, the tightest threshold the trace satisfies

Backend selection, the smooth semantics, and the MILP encoding are covered in synthesis backends; the synthesis guides work through receding horizon control, falsification, chance constraints, and the safety filter.

Errors

Anything fallible returns sentil::Result<T>, an alias for Result<T, sentil::Error>. Nothing reachable from user input panics. Match the variant you can act on and propagate the rest with ?:

use sentil::{Error, Formula};

match Formula::parse("G (speed >") {
    Ok(phi) => println!("{:?}", phi.variables()),
    Err(Error::Parse(e)) => {
        eprintln!("parse failed at line {}, column {}: {}", e.line, e.column, e.message);
    }
    Err(e) => eprintln!("{e}"),
}

This prints parse failed at line 1, column 11: expected a value or `(`, found end of input; both coordinates are 1-based. The failure a first session actually hits is a name mismatch between formula and trace, which arrives as Error::UnknownVariable:

let phi = Formula::parse("G (velocity > 5)")?;
match phi.robustness(&trace) {
    Err(Error::UnknownVariable { name }) => {
        eprintln!("the trace has no signal named {name}"); // velocity
    }
    other => println!("{other:?}"),
}

Error is #[non_exhaustive], so a match always carries a catch-all arm; it implements std::error::Error and fits any error chain. The reference table below lists all twenty variants, and the same messages cross into every binding: see errors across bindings and the error-code mapping.

Cargo features

Everything below this point is the reference: every public item, grouped by task. It starts with the features that gate the layers.

The default set is std, statistical, ingest, parallel, synthesis, specs, and sqlite. A monitor-only build is --no-default-features --features std.

Three gate consequences are easy to miss. First, the statistical methods on the monitor family disappear in a monitor-only build: MonitorConfig::smc/rare/smc_config/rare_config, Monitor::check/check_sequential/check_rare/last_probability, StreamMonitor::with_lifting/last_probability, MultiFormulaMonitor::add_probabilistic/probabilities/probability, and FormulaBank::check are all behind statistical. Second, SynthesisProblem::on_gpu needs synthesis-gpu, not plain synthesis, and solve_milp additionally needs std. Third, GPU entry points return a typed Error::Gpu when no device is present rather than silently switching; call sentil::gpu::is_available() to decide, once, whether to take the GPU path. The feature reference has the cross-package matrix.

The error type

Result<T> is an alias for core::result::Result<T, Error>. Error has twenty variants, each carrying what a caller needs to fix the input; the enum and its richer variants are #[non_exhaustive], so match with a catch-all arm and destructure struct variants with ...

ParseError is { message: String, line: usize, column: usize } with public fields, both coordinates 1-based, and ParseError::at(message, line, column) constructs one when a tool of your own wants to report positions the same way. Every variant maps to a stable C ABI status code; the error-code reference has the table.

Formulas and the syntax tree

Formula is a parsed PrSTL syntax tree; the grammar defines the text it accepts and the operator reference the semantics of each node.

The tree itself is public under sentil::formula, so you can build formulas without the parser and bindings can inspect them. Formula has thirteen variants:

A built tree compares equal to its parsed twin:

use sentil::formula::{ComparisonOp, Expr, Formula, Interval, Predicate};

let phi = Formula::Always(
    Interval::bounded(0.0, 10.0)?,
    Box::new(Formula::Predicate(Predicate {
        lhs: Expr::Variable("speed".to_owned()),
        op: ComparisonOp::Greater,
        rhs: Expr::Literal(5.0),
    })),
);
assert_eq!(phi, Formula::parse("G[0, 10] (speed > 5)")?);

The supporting types, all under sentil::formula:

Interval is the time window a temporal operator quantifies over; its fields are private and every constructor validates.

Note that is_bounded and is_unbounded are not complements: Interval::from_lower(2.0)? is neither, since it has no finite upper bound but is not the whole future.

Evaluating robustness

Five methods on Formula and one free function score a formula against a trace. The robustness semantics page gives the exact value each operator computes, in both time models.

On the first-monitor trace, Formula::parse("speed > 5")?.robustness_signal(&trace)? is [7.0, 4.0, 2.0, -1.0, 1.0] and violations returns [(3.0, 3.0)], the single dip as a degenerate span.

Monitors

Monitor wraps one formula with a configuration and serves offline evaluation, streaming, and statistical checking from one handle. MonitorConfig is a consuming builder; TimeMode is Discrete (the default) or Dense.

The same checks exist directly on Formula when you would rather pass the config per call: check, check_distribution, check_conservative, check_sequential, check_bayesian, check_rare_event, and, under gpu, check_rare_event_gpu. Only the Bayesian regime has no Monitor form.

Streaming verdicts

Robustness is the verdict every streaming update returns. It is an enum, not a struct: Concrete(f64) once the value is final, Interval(f64, f64) while future samples can still move it.

use sentil::Robustness;

let pending = Robustness::Interval(-0.5, 2.0);
assert!(!pending.is_resolved());
assert_eq!(pending.value(), 0.75); // midpoint until the window closes

let done = Robustness::Concrete(1.5);
assert_eq!(done.concrete(), Some(1.5));
assert!(done.is_satisfied());

Treat is_satisfied on an unresolved verdict as provisional; gate alarms on is_resolved() first, as the streaming example above does.

Multi-formula monitoring

Three types run more than one property, or strip the single-formula path to its core. All are crate-root exports.

StreamMonitor is the bare streaming engine behind Monitor, with no config and no offline path:

MultiFormulaMonitor advances many streaming formulas under one clock, each keyed by an id:

use sentil::MultiFormulaMonitor;

let mut fleet = MultiFormulaMonitor::new();
fleet.add("speed-floor", "G[0, 10] (speed > 5)")?;
fleet.add("accel-cap", "G[0, 10] (accel < 3)")?;

let verdicts = fleet.update(0.0, &[("speed", 9.0), ("accel", 1.0)])?;
for (id, verdict) in &verdicts {
    if verdict.is_resolved() && !verdict.is_satisfied() {
        println!("{id} violated");
    }
}

FormulaBank is the offline counterpart, evaluating many named formulas over one trace; per-formula failures come back as per-id Results rather than failing the batch:

Traces and buffers

The trace types in full. Construction and file reading:

Reading and resampling:

RingBuffer is a fixed-capacity rolling window with running statistics, the piece you reach for when a monitor's verdict should react to recent history you manage yourself:

use sentil::RingBuffer;

let mut window = RingBuffer::new(4)?;
for (t, v) in [(0.0, 12.0), (1.0, 9.0), (2.0, 7.0), (3.0, 4.0), (4.0, 6.0)] {
    window.push(t, v)?; // the fifth push evicts (0.0, 12.0) and returns it
}
assert_eq!(window.min(), Some(4.0));
assert_eq!(window.mean(), Some(6.5));

Noise models and lifting

Everything here is behind statistical. NoiseModel carries seventeen families, each behind a validating constructor; the noise models reference describes when each fits.

Fitting a model from paired calibration data is a two-step: compute residuals under an interaction, then fit a family to them.

use sentil::{NoiseInteraction, NoiseModel};

let residuals = NoiseModel::residuals(&ground_truth, &readings, NoiseInteraction::Additive)?;
let fitted = NoiseModel::fit_gaussian(&residuals)?;

LiftingRegistry maps variables to noise models and turns a deterministic trace into noisy realizations:

The lifting guide walks a full calibration.

Confidence intervals and sample sizing

The interval machinery is public on its own, and the free functions live at the sentil::stats:: path rather than the crate root.

A number to check the wiring with: stats::clopper_pearson(50, 100, 0.95) is [0.398321, 0.601679], slightly wider than Wilson's [0.4038, 0.5962] on the same counts, which is the exact interval's price. Confidence intervals explains how to choose, and the sample-size guide budgets a run.

The Monte Carlo configuration and results:

Sequential test configuration

SprtConfig and BayesConfig validate on construction and again on deserialization under serde, so an invalid shape cannot arrive from a config file.

The two free functions accept any draw closure, so they also test things that are not formulas; feeding sequential_test a source that succeeds nine times in ten decides AcceptH1 within a handful of draws. The SPRT guide tunes the error rates.

Stochastic systems and rare events

StochasticSystem wraps two closures into a sampling-ready simulator; it drives both check_rare_event and ChanceConstraint::validate.

The splitting configuration and result:

Underneath sits a generic estimator you can drive with your own state machine, at the sentil::stats:: path:

SimModel is the declarative twin of StochasticSystem: dynamics as SimExpr terms instead of closures, which is what lets the GPU transpile them. Both re-export at the crate root under the gpu feature.

Synthesis reference

The synthesis surface in full. The worked path is in the synthesis section above; backends and their tradeoffs are on synthesis backends.

Models. SystemModel is the trait the synthesizer drives, and implementing it is how custom dynamics plug in; the cart in this example damps its velocity by ten percent per step:

use sentil::{Bounds, Formula, SynthesisProblem, Synthesizer, SystemModel, Trace};

struct Cart {
    x0: [f64; 2],
}

impl SystemModel for Cart {
    fn input_dimension(&self) -> usize {
        10
    }

    fn initial_state(&self) -> &[f64] {
        &self.x0
    }

    fn rollout_from(&self, initial: &[f64], input: &[f64]) -> sentil::Result<Trace> {
        let (mut pos, mut vel) = (initial[0], initial[1]);
        let mut positions = Vec::with_capacity(input.len());
        for u in input {
            vel = 0.9 * vel + u;
            pos += vel;
            positions.push(pos);
        }
        let times: Vec<f64> = (1..=input.len()).map(|i| i as f64).collect();
        Trace::from_signal(times, "pos", positions)
    }
}

let model = Cart { x0: [0.0, 0.0] };
let spec = Formula::parse("F[0, 10] (pos > 4)")?;
let problem = SynthesisProblem::new(&model, &spec)
    .with_bounds(Bounds::new(vec![-1.0; 10], vec![1.0; 10])?);
assert!(Synthesizer::solve(&problem)?.holds);

Problems and solving:

Smoothing. Synthesis differentiates through a soft robustness; the smooth semantics page defines it exactly.

Control:

Falsification and mining:

Numeric building blocks, at the sentil::synthesis:: path; useful when you drive the optimizers directly:

The specifications library

Behind specs, the crate embeds the standards-derived specification templates and resolves them by name. The catalog itself is browsable under specifications.

use sentil::SpecRegistry;

let builder = SpecRegistry::global()
    .builder("controls/overshoot")?
    .with_param("max_overshoot", 0.02)?
    .with_variant("bidirectional")?;

println!("{}", builder.build_deterministic()?);
// always[0, 30.0](abs(output - reference) < 0.02 * 1.0)
let monitor = SpecRegistry::global().builder("controls/overshoot")?.into_monitor()?;

with_param rejects a name the template does not define, so a typo fails at build time rather than monitoring the wrong thing; controls/overshoot takes max_overshoot, step_amplitude, T, and p. The builder methods consume self and return Result<Self>, so chain them with ?.

The template's component types live at the sentil::spec_builder:: path; you meet them when authoring templates or introspecting one:

Related pages