Python

The binding is a PyO3 native extension module rather than a wrapper over the C ABI. Crossing into native code costs about 521 ns per call in the cross-language benchmark.

Install

We have two ways of installing SENTIL for Python. Through pip, or building it from source.

From PyPI

pip install sentil

pip install 'sentil[pandas]' 'sentil[plotting]'

python -c "import sentil; print(sentil.__version__)"

0.3.0

From source

You need a Rust toolchain from rustup.rs, maturin, and a linker.

xcode-select --install

git clone https://github.com/sedislab/SENTIL
cd SENTIL/sentil-py

pip install maturin
maturin develop --release --extras pandas,plotting

python -m pytest tests
python -c "import sentil; print(sentil.__version__)"

0.3.0

To build a wheel rather than install in place, maturin build --release --out dist -m sentil-py/Cargo.toml from the repository root writes it to dist/.

First monitor

A dict of channels over a list of timestamps is a trace; one parsed formula scores it.

import sentil
from sentil import Formula

trace = sentil.Trace([0, 1, 2, 3, 4], {"speed": [12, 9, 7, 4, 6]})
phi = Formula.parse("G (speed > 5)")

print(phi.robustness(trace))  # -1.0

The predicate scores speed - 5 at each sample, giving 7, 4, 2, -1, 1, and G, read always, keeps the worst of them: speed drops to 4 at $t = 3$, one unit under the bound, so the answer is $-1.0$. Why a signed margin instead of a boolean is the subject of what STL is; the syntax parse accepts is in the grammar. The same formula also answers per-sample, dense-time, and where-did-it-fail questions:

phi.robustness_signal(trace)   # [-1. -1. -1. -1.  1.], the value at every sample
phi.robustness_dense(trace)    # -1.0 under dense-time interpolation
phi.violations(trace)          # one Interval with .start 0.0 and .end 3.0

violations returns the spans of evaluation times where the formula fails; here the suffix starting anywhere in [0, 3] contains the dip, and the suffix starting at 4 does not.

Traces

A Trace pairs one time vector with named signals of matching length. Feed it lists, tuples, or NumPy arrays; times must be strictly increasing. It behaves like a read-only mapping: len(trace) counts samples, trace["speed"] returns the values as a NumPy array, "speed" in trace tests membership, iteration yields signal names, and trace.get(name, default) mirrors dict.get.

import sentil
from sentil import Interpolation, Trace

t = Trace.from_csv("time,speed\n0,12\n1,9\n2,7\n3,4\n4,6")
t5 = Trace.indexed(5)               # times 0 through 4, add signals afterwards
t5.add_signal("speed", [12, 9, 7, 4, 6])

tr = Trace([0, 2, 4], {"x": [0.0, 2.0, 0.0]})
tr.resample([0, 1, 2, 3, 4], Interpolation.Linear)["x"]   # [0. 1. 2. 1. 0.]
prep = tr.prepare(Interpolation.CubicSpline)
prep.resample([1.0, 3.0])["x"]                            # [1.375 1.375]

Trace.from_path reads csv, tsv, and txt out of the box, and parquet, arrow, sqlite, hdf5, mat, and mcap when the core is built with the matching format features; see trace formats. For data already in a DataFrame, the [pandas] extra converts directly:

import pandas as pd
from sentil import Formula
from sentil.pandas import trace_from_dataframe

df = pd.DataFrame({"time": [0, 1, 2, 3, 4], "speed": [12, 9, 7, 4, 6]})
trace = trace_from_dataframe(df)
print(Formula.parse("G (speed > 5)").robustness(trace))  # -1.0

trace_from_dataframe takes the timestamps from time_column (default "time") and turns every other column into a signal, or only the ones you name in value_columns. A missing column raises KeyError naming it.

Streaming

OnlineMonitor ingests samples as they arrive and holds only what the temporal windows need, O(1) amortized per update; the mechanism is the monotonic deque. Each update returns a Robustness verdict.

import math
import sentil

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

violated at t=15, robustness=-0.078

A verdict is resolved once the window it depends on has fully passed; until then .resolved is false and .value reads the midpoint of the running [.lower, .upper] bounds. To replay a recorded trace through the same incremental path, run returns the verdict after each sample:

import sentil

m = sentil.OnlineMonitor("G[0, 2] (speed > 5)")
verdicts = m.run(sentil.Trace([0, 1, 2, 3, 4], {"speed": [12, 9, 7, 4, 6]}))
[(v.resolved, v.value) for v in verdicts]
# [(False, -inf), (False, -inf), (True, 2.0), (True, -1.0), (True, -1.0)]

The first two are unresolved because the [0, 2] window is still open; the third closes the window for time 0 with margin 2.0. A dict is rebuilt on every update; in a tight loop, look up each variable's slot once with symbol_index and pass update_packed a packed array in slot order instead.

Live probability

A monitor built with with_lifting tracks a P~p formula as samples arrive, and last_probability reads the current satisfaction estimate, None before the first resolved window.

from sentil import LiftingRegistry, NoiseModel, OnlineMonitor, SmcConfig

lifting = LiftingRegistry()
lifting.register("x", NoiseModel.gaussian(0.0, 0.3))

pm = OnlineMonitor.with_lifting("P>=0.9 (G[0, 5] (x > 0))", lifting, SmcConfig(samples=1000))
for t in range(12):
    pm.update(float(t), {"x": 0.4 + 0.05 * t})
print(pm.last_probability())  # 0.978

To watch many formulas under one clock, MultiMonitor keys each by an id: add for deterministic formulas, add_probabilistic for P~p ones, and each update returns a dict of verdicts. probability(id) and probabilities() read the live estimates, None for deterministic ids.

Probabilistic checking

A P~p formula asserts a property holds with probability at least, or at most, p once each reading is treated as a noisy observation. Register a noise model per channel (the interaction defaults to NoiseInteraction.Additive, residual y - g; pass Multiplicative for y / g), then check lifts the trace into an ensemble, evaluates the inner formula on each sample, and estimates the satisfaction probability with a confidence interval.

import sentil
from sentil import Formula, LiftingRegistry, NoiseModel, SmcConfig

trace = sentil.Trace(list(range(20)), {"x": [0.4 + 0.05 * i for i in range(20)]})
lifting = LiftingRegistry()
lifting.register("x", NoiseModel.gaussian(0.0, 0.3))

phi = Formula.parse("P>=0.9 (G (x > 0))")
r = phi.check(trace, lifting, SmcConfig(samples=5000))
print(f"probability {r.probability:.3f}, interval [{r.interval.lower:.3f}, {r.interval.upper:.3f}], holds {r.holds}")

probability 0.733, interval [0.721, 0.745], holds False

The margins run from 0.4 to 1.35 while the noise sigma is 0.3, so a lifted trajectory has a real chance of dipping below zero somewhere in twenty samples: 73 percent of the ensemble satisfies, short of the 0.9 bar. How the operator and the decision rule work is covered in what PrSTL is and confidence intervals.

SmcConfig carries the four knobs: samples (default 10000), confidence (0.95), seed (42, so runs reproduce), and method, one of the four IntervalMethod variants with Wilson the default. check_conservative is a shortcut that reruns the interval as Clopper-Pearson, the exact conservative choice; the point estimate and verdict are unchanged. check_distribution additionally returns a RobustnessDistribution summarizing the ensemble's robustness values; on the run above it reports mean 0.104, standard deviation 0.188, and extremes -0.716 and 0.658 over the 5000 samples.

Sequential decisions

When a verdict matters more than the estimate, the sequential tests stop as soon as the evidence decides, usually after far fewer lifted samples than a fixed budget. Continuing with the trace, lifting, and formula from prstl.py:

from sentil import BayesConfig, SprtConfig

sprt = phi.check_sequential(trace, lifting, SprtConfig(p0=0.85, p1=0.95))
sprt.verdict, sprt.samples     # (SprtVerdict.AcceptH0, 32)

bayes = phi.check_bayesian(trace, lifting, BayesConfig(threshold=0.9))
bayes.verdict, bayes.samples   # (BayesVerdict.Fails, 60)

Wald's SPRT decides H0: p <= p0 against H1: p >= p1 with Type I and II error bounded by alpha and beta; here it settles on the failing side after 32 samples instead of 5000. The Bayesian test runs a Beta(1, 1) prior to a Bayes-factor cutoff and agrees at 60, with posterior 0.0008 as the remaining belief that the threshold is met.

Rare events

Describe the system as a SimModel, and check_rare_event runs adaptive multilevel splitting over it; the concept page is rare events.

from sentil import Formula, NoiseModel, RareEventConfig, SimExpr, SimModel

x = SimExpr.prev(0) * SimExpr.constant(0.9) + SimExpr.noise(0)
model = SimModel(["x"], 1.0, 50, [SimExpr.constant(0.0)], [x], [NoiseModel.gaussian(0.0, 1.0)])
system = model.to_stochastic_system()

phi = Formula.parse("P>=0.99999 (G (x < 12))")
res = phi.check_rare_event(system, RareEventConfig(particles=2000, seed=3))
res.violation_probability   # 1.83e-06
res.holds                   # True

The model is an AR(1) process that rarely wanders past 12; splitting resolves the 2-in-a-million tail from 2000 particles. With a GPU present, check_rare_event_gpu(model) moves the fixed-effort splitting onto the device and returns a GpuSplittingEstimate; sentil.gpu.is_available() is the runtime capability check, and without a device the GPU call raises EvaluationError ("no compatible GPU adapter for the splitting path") rather than silently falling back. See rare events on the GPU.

Synthesis

sentil.synthesis turns a specification into an input sequence, and Controller closes the loop online. The worked model below is one state with x' = x + u, started at 1.

from sentil import Bounds, Formula, SafetyFilter, SystemModel, synthesis

model = SystemModel.linear([[1.0]], [[1.0]], [1.0], ["x"], 1.0, 3)
spec = Formula.parse("G (x > 0)")
bounds = Bounds([-1.0] * 3, [1.0] * 3)

r = synthesis.synthesize(model, spec, bounds)
r.input, r.robustness, r.holds, r.backend
# ([1., -1., 0.], 1.0, True, Backend.Milp)

shield = SafetyFilter(bounds)
shield.filter([2.0, 0.5, -3.0])   # [1.0, 0.5, -1.0]

Backend.Auto routed this problem to the exact MILP encoding because the dynamics are affine and the spec is plain STL; the built-in simplex solves it with no external dependency. The robustness 1.0 is optimal here, since the fixed start x0 = 1 caps the worst margin at 1. Pass backend=Backend.Gradient or Backend.CmaEs to choose the smooth-gradient or black-box path instead, smooth=SmoothConfig(...) to tune the soft semantics, and max_iters or population to bound the search. The routing rules are in synthesis backends.

The receding-horizon Controller re-plans within a hard per-step budget in nanoseconds, anytime: it returns the best input found when the clock runs out. Here altitude decays 20 percent a step and the controller holds it by applying exactly the lost 0.6:

from sentil import Bounds, Controller, Formula, SystemModel

model = SystemModel.linear([[0.8]], [[1.0]], [3.0], ["alt"], 1.0, 5)
ctl = Controller(model, Formula.parse("G (alt > 2)"), 1, 2_000_000, Bounds([-1.0] * 5, [1.0] * 5))
alt = 3.0
for step in range(3):
    u = ctl.control([alt])[0]
    alt = 0.8 * alt + u
    print(f"u={u:.3f} alt={alt:.3f}")

u=0.600 alt=3.000
u=0.600 alt=3.000
u=0.600 alt=3.000

Falsification runs the same machinery in reverse. falsify is a Formula method: it searches for an input whose trajectory violates the formula and returns a Witness whose negative robustness is the proof.

from sentil import Bounds, CmaConfig, Formula, SystemModel

model = SystemModel.linear([[1.0]], [[1.0]], [1.0], ["x"], 1.0, 3)
bounds = Bounds([-1.0] * 3, [1.0] * 3)

unsafe = Formula.parse("G (x < 3)")
w = unsafe.falsify(model, bounds, CmaConfig(max_generations=100), restarts=2)
w.input, w.robustness    # ([1., 1., 1.], -1.0): x runs 1, 2, 3, 4 and breaches at 4

cex = Formula.parse("G (x > 0)").find_counterexample(model, bounds, max_iters=100)
cex.input, cex.robustness    # ([-1., -1., -1.], -2.0), driving x down to -2

ChanceConstraint(spec, probability) states a probabilistic requirement for synthesis, with optional confidence and tightening, and validate(system) checks it against a StochasticSystem by sampling, returning a ChanceReport with the estimate and its lower confidence bound.

Errors

Everything raises from one small hierarchy, so except SentilError catches all of it and a subclass separates the kind. Nothing in the library can crash the interpreter, and no handle discipline is needed: objects are plain garbage-collected Python objects and no call consumes its arguments.

from sentil import Formula, ParseError, SentilError

try:
    Formula.parse("G (speed >")
except ParseError as e:
    print(e)   # parse error at line 1, column 11: expected a value or `(`, found end of input

The messages are the core's own and say what to do next; evaluating a formula over a trace missing speed raises SemanticError with "no value available for variable speed; add a signal named speed to the trace, or include it in the streaming update". The code-to-family mapping shared by every binding is on error handling across languages.

Reference

The rest of this page lists the whole public surface, task by task. sentil.__version__ is the version string. Five submodules hang off the top level: sentil.stats (interval and sample-size functions), sentil.synthesis (the optimization entry points), sentil.gpu (the capability check), and the two extras sentil.pandas and sentil.plotting. The builder DSL functions below are re-exported at the top level, so from sentil import var, always works.

Building formulas

Formula is a parsed PrSTL tree; build one from text, from the builder functions, or from Expr comparisons.

The boolean connectives are operator overloads: phi & psi is and, phi | psi is or, ~phi is not, and phi >> psi is implies.

The builder DSL offers the same combinators as free functions, handy for building formulas bottom-up without method chains:

Expr is the arithmetic layer under the predicates. Expr.var(name) and Expr.constant(value) are the leaves; the operators + - * / % ** and unary - combine them; abs(expr) and the methods sqrt, exp, log (base 10), ln (natural), sin, cos, tan, floor, ceil, min(other), and max(other) cover the function set; and the comparisons > >= < <= against an Expr or a number yield a Formula. Equality predicates (==, !=) exist in the text grammar only, not as Expr overloads.

Scoring robustness

Five Formula methods evaluate against a Trace; each Interval in a violations list carries .start and .end.

Traces

Ring buffer

RingBuffer(capacity) holds the newest capacity samples as (time, value) pairs, with mean, variance, and extrema maintained in O(1). When full, push evicts the oldest sample and returns it.

Monitors

Config(time=TimeMode.Discrete) selects the time semantics and exposes it as .time. Every monitor verdict is a Robustness with .resolved, .satisfied, .value, .lower, and .upper; float(verdict) reads .value, and .satisfied is meaningful only once .resolved is true.

FormulaBank() scores a set of named formulas against a whole trace: add(id, formula) registers, ids and len(bank) enumerate, and robustness(trace) and robustness_dense(trace) return a dict of values keyed by id, sharing one pass over the trace.

Noise models and lifting

NoiseModel describes one channel's noise; build it from any of seventeen families or learn it with one of four fitters.

LiftingRegistry() maps variables to models: register(variable, model, interaction=NoiseInteraction.Additive) adds one, variables and is_empty inspect, and lift(trace, seed=42) draws one noisy realization of a trace, the same operation check repeats per sample. The families and fitting workflow are covered in noise models.

Probability estimates

The entry points are the Formula methods check(trace, lifting, config=None), check_conservative(...) (same estimate, Clopper-Pearson interval), and check_distribution(...) which returns the pair (SmcResult, RobustnessDistribution).

Sequential tests

Run them with phi.check_sequential(trace, lifting, sprt_config) and phi.check_bayesian(trace, lifting, bayes_config), or from a Monitor. The theory is on statistical methods.

The stats functions

sentil.stats exposes the interval mathematics directly, useful for sizing an experiment before running it.

from sentil import stats

stats.wilson_interval(50, 100, 0.95)          # [0.4038, 0.5962]
stats.clopper_pearson(50, 100, 0.95)          # [0.3983, 0.6017], wider as promised
stats.z_score(0.95)                           # 1.959964
stats.chernoff_hoeffding_samples(0.1, 0.05)   # 185
stats.wilson_samples(0.01, 0.95)              # 9604

Stochastic systems and rare events

SimExpr terms describe update rules declaratively so the sampler can run them fast: SimExpr.prev(i) reads variable i at the previous step, SimExpr.time() the current time, SimExpr.constant(value) a literal, and SimExpr.noise(i) a draw from the i-th noise model. Terms combine with + - * /, abs, the methods sin, cos, tan, sqrt, exp, log, ln, floor, ceil, and min(other) / max(other).

Synthesis

The sentil.synthesis functions, and the Formula methods that share the smooth-robustness machinery.

The numeric helpers are checkable by hand: solve_qp([[2, 0], [0, 2]], [-2, -4], [[1, 1]], [1]) returns [0.0, 1.0], solve_spd([[4, 1], [1, 3]], [1, 2]) returns [1/11, 7/11], and symmetric_eigen([[2, 1], [1, 2]]) finds eigenvalues [1.0, 3.0].

The specifications library

SpecBuilder loads a vetted, standards-derived specification by name and instantiates it with your parameters. There are 54 in the catalog; browse them under specifications.

from sentil import SpecBuilder

len(SpecBuilder.available())     # 54
b = SpecBuilder("controls/overshoot")
b.parameters()                   # {'max_overshoot': 0.05, 'step_amplitude': 1.0, 'T': 30.0, 'p': 0.95}
b.available_variants             # ['bidirectional', 'step_down', 'step_up']
b.with_param("max_overshoot", 0.02).build_deterministic()
# 'always[0, 30.0](output - reference < 0.02 * 1.0)'

An unknown parameter raises EvaluationError naming the ones the template defines.

pandas and plotting

Both modules are extras; each raises ModuleNotFoundError with the install command if its dependency is absent. Every plotting function returns the Matplotlib Figure, so you decide whether to show, save, or compose it.

Enums

Eight value enums, every member listed.

Related