MATLAB

The MATLAB toolbox is self-contained: the compiled core ships inside the .mltbx, so there is nothing else to install. The sentil package is the programmatic API, and the SENTIL Monitor block runs the streaming monitor inside a Simulink model, so a controller is checked against its specification as the simulation steps. A formula parsed here returns the same robustness as the same formula in Rust or Python, because every class calls the same engine through one MEX gateway.

Native-backed classes such as sentil.Trace, sentil.Formula, and sentil.OnlineMonitor are handle objects that free their engine memory in delete; touching one after it has been closed or consumed raises sentil:handle. The configuration types, sentil.SmcConfig through sentil.SmoothConfig, are value classes with validated, defaulted properties: set a field, pass the object, nothing to free.

Install

Two routes hand you the same file, and the third builds it. Sentil.mltbx from the File Exchange is the one to reach for: a single package carries the compiled gateway for Linux, macOS, and Windows, so no Rust toolchain and no compiler enter the picture. The same package is attached to each GitHub release, which is the route to a specific tag rather than whatever the listing currently serves. Build from source when you are changing the binding, or when you want the gateway compiled against a core you built yourself.

On macOS the published package carries only the Apple silicon .mexmaca64, an extension that did not exist before R2023b, so it needs R2023b or newer there and holds nothing an Intel Mac can load. Build from source on one.

From the File Exchange

matlab.addons.toolbox.installToolbox('Sentil.mltbx')

v = sentil.version()   % struct: major 0, minor 3, patch 0

From a GitHub release

matlab.addons.toolbox.installToolbox('Sentil.mltbx')

trace = sentil.Trace([0 1 2 3 4], 'speed', [12 9 7 4 6]);
sentil.Formula.parse('G (speed > 5)').robustness(trace)   % -1

From source

You need a Rust toolchain from rustup.rs and a compiler mex accepts, which comes from a different place on each system. build_sentil compiles the Simulink S-Function alongside the gateway, so Simulink has to be installed; the CI job that runs the build installs that product first.

xcode-select --install

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

build_sentil
% +sentil/private/sentil_mex.mexa64   the gateway; .mexmaca64 on Apple silicon, .mexw64 on Windows
% blocks/sentil_s_function.mexa64     the Simulink S-Function
% a copy of libsentil.so lands beside each one

addpath(pwd)
runtests('tests')   % test_sentil, plus test_oracle against the shared deterministic oracle
sentil.version()    % major 0, minor 3, patch 0

The clone-and-build step every binding shares is on install from source. package_sentil turns the built tree into a distributable Sentil.mltbx and needs R2023a or newer for the ToolboxOptions API; it is listed with the other toolbox functions.

Your first monitor

trace = sentil.Trace([0 1 2 3 4], 'speed', [12 9 7 4 6]);
phi = sentil.Formula.parse('G (speed > 5)');
phi.robustness(trace)   % -1.0

Robustness is -1.0 because the worst sample, the 4 at t = 3, misses the bound by one; negative says violated, and the size says by how much. What robustness means has the full account. robustness_signal gives the value at every sample, violations gives the failing [start, end] spans, and robustness_dense evaluates between samples by interpolation, which discrete versus dense covers.

Loading traces

The constructor takes a strictly increasing time vector, optionally with one named signal; add_signal attaches more on the same grid.

trace = sentil.Trace([0 1 2 3 4], 'speed', [12 9 7 4 6]);
trace.add_signal('altitude', [100 120 140 130 90]);

flight = sentil.Trace.from_path('flight.csv');   % csv or tsv, by extension

from_path reads CSV and TSV. For .mat, Parquet, and the rest, read the data with MATLAB's own loaders and hand the arrays to the constructor; the engine-level format list is on trace formats. resample reads a trace onto a new grid through a sentil.Interpolation, and prepare returns a sentil.PreparedTrace that makes repeated resampling cheap. The full surface is in the reference.

Streaming

sentil.OnlineMonitor is the streaming half of the toolbox. Each update folds in a single reading at O(1) amortized cost, and the monotonic deque underneath caps memory at the widest window, so a monitor can sit in a control loop indefinitely.

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

update returns a struct with five fields: resolved, satisfied, value, lower, and upper. A future-bounded operator cannot settle until its window has passed, so an early verdict is an interval: lower and upper bracket the eventual robustness, value sits midway between them, and resolved stays false until the window closes, which is why the [0, 10] bound above matters on a live stream. satisfied reads value >= 0, so consult it only after resolved turns true.

A sample can be a struct or a containers.Map; anything else raises sentil:sample. A MATLAB call into the gateway costs about 6.49 microseconds, the highest per-call overhead of the bindings, so in a tight loop look up each variable's position once with symbol_index and feed update_packed(time, values) a row vector in that order.

Live probability

Probabilistic streaming goes through OnlineMonitor.with_lifting, which tracks a P-wrapped formula with a particle ensemble lifted through a noise registry. The formula is borrowed, not consumed.

phi = sentil.Formula.parse('P>=0.9 (G[0, 10] (x > 0))');
lifting = sentil.LiftingRegistry();
lifting.register('x', sentil.NoiseModel.gaussian(0.0, 0.3));

m = sentil.OnlineMonitor.with_lifting(phi, lifting);
for t = 0:19
    r = m.update(t, struct('x', 0.4 + 0.05 * t));
end
p = m.last_probability()   % the running satisfaction estimate

On a probabilistic monitor the verdict's lower and upper carry the confidence bounds, and last_probability reads the live estimate directly; it returns NaN on a deterministic monitor or before the first update. To advance many formulas, deterministic and probabilistic side by side, on one clock, use sentil.MultiMonitor from the reference.

Probabilistic monitoring

A P~p operator sets a floor, or a ceiling, on the probability that a formula holds over noisy readings (what PrSTL is). Register a noise model per variable, then check estimates the satisfaction probability with a confidence interval.

times = 0:19;
trace = sentil.Trace(times, 'x', 0.4 + 0.05 * times);

lifting = sentil.LiftingRegistry();
lifting.register('x', sentil.NoiseModel.gaussian(0.0, 0.3));

phi = sentil.Formula.parse('P>=0.9 (G (x > 0))');
config = sentil.SmcConfig;
config.samples = 5000;

result = phi.check(trace, lifting, config);
% result.probability, result.interval.lower / .upper / .level,
% result.satisfactions, result.samples, result.holds

register consumes the noise model: the registry owns it afterward, and reusing the original raises sentil:handle. Its optional fourth argument is a sentil.NoiseInteraction, Additive by default, Multiplicative for noise that scales with the reading. The 17 families, the fitters, and the registry surface are in the reference; choosing and fitting a model is covered in noise models.

check uses the Wilson interval unless config.method says otherwise. check_conservative swaps in Clopper-Pearson, and check_distribution also returns the robustness distribution the estimate saw. The choice of interval is a real decision; confidence intervals walks it.

Sequential and Bayesian tests

A fixed sample budget wastes draws on an easy instance; the sequential tests quit the moment the hypothesis is settled.

sprt = sentil.SprtConfig(0.85, 0.95);
r = phi.check_sequential(trace, lifting, sprt);
% r.verdict is a sentil.SprtVerdict; also r.samples, r.log_likelihood

bayes = sentil.BayesConfig(0.9);
r = phi.check_bayesian(trace, lifting, bayes);
% r.verdict is a sentil.BayesVerdict; also r.samples, r.posterior

Both configs are required arguments here; their remaining properties and defaults are in the config table.

Rare events

Below the probabilities plain Monte Carlo resolves, check_rare_event runs adaptive multilevel splitting over a sentil.StochasticSystem, a system the engine can simulate from a seed. The custom form takes MATLAB callbacks for the dynamics.

sys = sentil.StochasticSystem.custom({'x'}, 1.0, 8, ...
    @(seed) 0.0, @(prev, t, seed) prev + (2 * mod(double(seed), 2) - 1) * 0.6);
r = phi.check_rare_event(sys);
% r.probability, r.violation_probability, r.holds, r.simulations

The GPU path takes a declarative sentil.SimModel instead of callbacks, because the model must run on the device, and it throws when no GPU is present. Gate it on the capability check; the CPU path stays available regardless.

if sentil.Gpu.is_available()
    est = phi.check_rare_event_gpu(model);   % model is a sentil.SimModel
    % est.violation_probability, est.particles, est.levels
end

Rare events explains the splitting method; both system classes are documented below.

Synthesis

sentil.Synthesis.synthesize searches for a control input sequence that satisfies a specification on a model. The smallest case: x starts at one, each step adds the input, and the spec keeps x positive for three steps under inputs bounded by one.

model = sentil.SystemModel.linear(1, 1, 1, {'x'}, 1.0, 3);
spec = sentil.Formula.parse('G (x > 0)');
bounds = sentil.Bounds([-1 -1 -1], [1 1 1]);

result = sentil.Synthesis.synthesize(model, spec, bounds);
% result.input, result.robustness, result.holds,
% result.backend (a sentil.Backend naming the solver that ran)

The backend defaults to Auto, which picks by the problem's structure; the choices and their tradeoffs are on synthesis backends. For closed-loop control, sentil.Controller replans a short horizon each step inside a hard time budget, and sentil.SafetyFilter shields any nominal input:

c = sentil.Controller(model, spec, 1, 1e6, sentil.Bounds(-3, 3));   % consumes model and spec
u = c.control(0.0);   % the input for the current state, within 1 ms

shield = sentil.SafetyFilter(sentil.Bounds([-1 -1 -1], [1 1 1]));
shield.filter([2.0 0.5 -3.0])   % [1 0.5 -1], clamped into the box

Going the other way, phi.falsify and phi.find_counterexample search for an input that breaks a spec, and Synthesis.mine_tightest_parameter finds the tightest parameter a family of formulas can hold at. The full surface, including the optimizers, the chance-constraint validator, and the convex solvers, is in the reference.

The Simulink block

The toolbox ships one masked Level-2 S-Function block, SENTIL Monitor, wrapping the same streaming engine as sentil.OnlineMonitor. One input port carries the formula's variables; one output port carries the verdict.

create_sentil_library("sentil_lib");   % writes sentil_lib.slx

add_block('sentil_lib/SENTIL Monitor', 'my_model/Monitor');
set_param('my_model/Monitor', ...
    'formula_str', 'G (speed < 120)', ...
    'var_names_str', 'speed', ...
    'mode_sel', 'Deterministic');

The mask carries six parameters; the last three appear only when the mode is Probabilistic/SMC.

In deterministic mode the output port carries the running robustness at each solver step. In probabilistic mode it is three wide, labeled [value, lower, upper]: the running satisfaction estimate bracketed by its interval, so the model can react to a probability as it simulates.

A worked model is in the Simulink block recipe, and the insulin pump case study monitors a full closed loop this way.

Errors

Failures throw MExceptions under the sentil: namespace. The message text comes from the engine and names the construct at fault and where it sits.

try
    phi = sentil.Formula.parse('G (speed >');
catch err
    fprintf('%s: %s\n', err.identifier, err.message);   % sentil:parse: ...
end

The sentil:handle you are most likely to meet comes from a consumed handle rather than a deleted one. These calls take ownership of their arguments: every Formula combinator plus Formula.predicate and Formula.probability; the Formula given to sentil.Monitor; the NoiseModel given to register and the components given to NoiseModel.mixture; the expression and noise arrays given to SimModel.create; the operands of Expr.binary, Expr.call, and the arithmetic shorthands on Expr and SimExpr; a SpecBuilder passed through with_variant, with_param, or into_monitor; the model and spec given to Controller; the Bounds given to SafetyFilter; and the spec given to ChanceConstraint. After such a call the argument object is closed, so rebuild it if you need it again. By contrast, OnlineMonitor.from_formula, OnlineMonitor.with_lifting, MultiMonitor.add, and FormulaBank.add borrow.

How the identifiers map to engine status codes, and how the other bindings surface the same failures, is on error codes and handling errors across bindings.

Reference

Signatures use the call form you write; statics carry the full package path.

Traces

sentil.Trace carries signals sampled on one strictly increasing time grid; sentil.PreparedTrace precomputes interpolation for repeated resampling.

Formulas

sentil.Formula.parse builds most formulas; the statics build them programmatically. Every builder consumes the pieces it is given.

Evaluation over a trace:

Probabilistic checks, each over a P-wrapped formula:

Search and gradients:

The combinators, each consuming the formulas it is given:

Predicate expressions

sentil.Expr builds the arithmetic inside a predicate when you construct formulas programmatically rather than parsing. The combinators consume their operands, like the formula builders.

lhs = sentil.Expr.var('x').mul(sentil.Expr.literal(2));
phi = sentil.Formula.predicate(lhs, sentil.ComparisonOp.Gt, sentil.Expr.literal(5));
% the same formula as sentil.Formula.parse('x * 2 > 5')

Monitors

Three classes. sentil.OnlineMonitor is the pure streaming monitor from the guide above. sentil.Monitor evaluates offline and incrementally while honoring a sentil.Config time mode, and it is what the specification library's into_monitor returns, carrying a spec's recommended settings. sentil.Config holds the time mode.

Many formulas on one clock

sentil.MultiMonitor advances any number of named streaming monitors with one update; sentil.FormulaBank is its offline counterpart for batch evaluation.

m = sentil.MultiMonitor();
m.add('floor', 'x > 0');
m.add('ceiling', 'x < 10');
r = m.update(0, struct('x', 3));
% r('floor').value is 3, r('ceiling').value is 7

Ring buffer

Derived features often need a bounded slice of recent history; sentil.RingBuffer holds one, at most capacity samples with running statistics maintained as samples arrive. Pushing past capacity evicts the oldest sample, and queries with no answer return [].

b = sentil.RingBuffer(3);
b.push(0, 10); b.push(1, 20); b.push(2, 30);
b.mean()        % 20
b.push(3, 40);  % returns the evicted sample from t = 0
b.mean()        % 30

Noise models and lifting

sentil.NoiseModel is one noise distribution, named directly or fitted from calibration data. sentil.LiftingRegistry maps variables to models so a clean trace lifts into noisy realizations.

Fitting, serialization, and moments:

Statistics and configs

sentil.Stats exposes the interval estimators, the sample-size rules, and the sequential tests directly; each interval returns a struct with lower, upper, and level, and level defaults to 0.95 throughout.

ci = sentil.Stats.wilson(50, 100);                    % lower 0.403831, upper 0.596169
sentil.Stats.z_score(0.95)                            % 1.959964
sentil.Stats.chernoff_hoeffding_samples(0.1, 0.05)    % 185
sentil.Stats.wilson_samples(0.01, 0.95)               % 9604

sentil.Gpu.is_available() reports whether a usable GPU device is present; it is the check to run before check_rare_event_gpu.

The six configuration types are value classes whose properties validate on assignment. Their defaults:

Stochastic systems and simulation models

Rare-event estimation and chance-constraint validation need a system the engine can simulate from a seed. sentil.StochasticSystem.custom wraps MATLAB callbacks; sentil.SimModel declares the dynamics as engine-side expressions, which is what the GPU path requires.

The callback contract: init(seed) returns the initial state row and step(prev, time, seed) returns the next one. Each must return its row; an error raised inside either surfaces as your own MATLAB error, or as sentil:callback if it carries no identifier.

sentil.SimExpr builds the declarative update rules; positions are 1-based, and the arithmetic combinators consume their operands.

x0 = sentil.SimExpr.constant(0);
step = sentil.SimExpr.prev(1).add(sentil.SimExpr.noise(1));
model = sentil.SimModel.create({'x'}, 1.0, 10, x0, step, sentil.NoiseModel.gaussian(0, 1));
t = model.simulate(42);   % a random walk, as a sentil.Trace

Synthesis classes

sentil.Synthesis holds the entry points, sentil.SystemModel the dynamics, sentil.Bounds the box constraints. The remaining classes close the loop: online control, shielding, and risk validation.

Specifications library

sentil.SpecBuilder loads a spec by name from the embedded specifications library, so a property can start from a cited standard rather than from scratch. with_variant, with_param, and into_monitor consume the builder, so keep the returned one and rebuild from the name to retry.

names = sentil.SpecBuilder.available();          % every embedded spec, sorted
b = sentil.SpecBuilder('aerospace/airspeed_envelope');
b = b.with_param('V_stall', 110);                % consumes; keep the return value
phi = b.build_probabilistic_formula();
reg = b.build_lifting_registry();                % the spec's own noise models

Enums

Each enum is an int32-backed MATLAB enumeration class matching the C ABI constant.

Toolbox functions

The functions that live beside the package rather than in it.

Related pages