Command line

The sentil binary runs the engine with no code to write. It is built for a pipe: data on stdout, progress and errors on stderr, a verdict in the exit code, and a stable JSON contract for scripts. Use it for batch checks, CI gates, live monitoring, and the ad-hoc questions that do not justify a program.

Install

Five package managers carry the CLI: Homebrew on macOS and Linux, Scoop and winget on Windows, the AUR on Arch, and cargo install wherever a Rust toolchain lives. Reach for the one your machine already has. Where none fits, every release attaches a prebuilt archive per platform, and a source build covers an unreleased change or a target the release matrix misses. ARM Linux has three archives of its own, described under on a Raspberry Pi.

From a package manager

brew install sedislab/sentil/sentil

scoop bucket add sedislab https://github.com/sedislab/scoop-sentil
scoop install sentil

winget install SEDIS.SENTIL

yay -S sentil

git clone https://aur.archlinux.org/sentil.git
cd sentil && makepkg -si

cargo install sentil-cli

All five leave the binary on your PATH, so one check covers them:

sentil --version

The first line reads sentil 0.3.0, and the commit hash and commit date the binary was built from follow it.

From a GitHub release

Each tagged release attaches one archive per platform. Inside is bin/sentil, or bin\sentil.exe on Windows, the four completion scripts under completions/, the man page at man/sentil.1, both licenses, and the package README.

No checksum file is published beside the archives. The Homebrew formula, the Scoop manifest, the winget manifest, and the AUR PKGBUILD each pin the SHA-256 of the exact file they fetch, so a package-manager install verifies itself and a hand download does not.

curl -LO https://github.com/sedislab/SENTIL/releases/download/v0.3.0/sentil-0.3.0-x86_64-unknown-linux-gnu.tar.gz
tar xzf sentil-0.3.0-x86_64-unknown-linux-gnu.tar.gz
cd sentil-0.3.0-x86_64-unknown-linux-gnu

curl -LO https://github.com/sedislab/SENTIL/releases/download/v0.3.0/sentil-0.3.0-aarch64-apple-darwin.tar.gz
tar xzf sentil-0.3.0-aarch64-apple-darwin.tar.gz
cd sentil-0.3.0-aarch64-apple-darwin

$url = "https://github.com/sedislab/SENTIL/releases/download/v0.3.0/sentil-0.3.0-x86_64-pc-windows-msvc.zip"
Invoke-WebRequest -Uri $url -OutFile sentil.zip
Expand-Archive sentil.zip -DestinationPath .

sudo cp bin/sentil /usr/local/bin/
sudo cp completions/sentil.bash /usr/share/bash-completion/completions/sentil
sudo cp completions/_sentil /usr/share/zsh/site-functions/_sentil
sudo cp completions/sentil.fish /usr/share/fish/vendor_completions.d/sentil.fish
sudo cp man/sentil.1 /usr/local/share/man/man1/

sudo cp bin/sentil /usr/local/bin/
sudo cp man/sentil.1 /usr/local/share/man/man1/

$bin = "$PWD\sentil-0.3.0-x86_64-pc-windows-msvc\bin"
$user = [Environment]::GetEnvironmentVariable('Path', 'User')
[Environment]::SetEnvironmentVariable('Path', "$user;$bin", 'User')

sentil --version

From source

A source build needs a Rust toolchain from rustup.rs and a linker, which comes from a different place on each system. Nothing else: the CLI links the engine statically, so there is no shared library to find and no environment variable to set.

xcode-select --install

git clone https://github.com/sedislab/SENTIL
cd SENTIL

cargo install --path sentil-cli
# or build in place; the binary lands at target/release/sentil
cargo build --release -p sentil-cli

sentil completion bash > sentil.bash
sentil man > sentil.1

cargo test -p sentil-cli
sentil --version

The same checkout builds every other binding against that core; installing from source is the shared entry point.

On a Raspberry Pi

The same release page carries the Pi archives. The gnu builds bundle more than the CLI: libsentil, the C header, and the pkg-config and CMake files ride along. Pick by board and OS:

The static musl build is one file with no library dependencies, the right shape for a sensor loop you copy onto a board and forget. From inside the extracted archive:

sudo cp bin/sentil /usr/local/bin/
sentil --version

sudo cp lib/libsentil.so lib/libsentil.a /usr/local/lib/
sudo cp include/sentil.h /usr/local/include/
sudo mkdir -p /usr/local/lib/pkgconfig
sudo cp lib/pkgconfig/sentil.pc /usr/local/lib/pkgconfig/
sudo cp -r lib/cmake /usr/local/lib/
sudo ldconfig

sensor | sentil monitor -f 'G (temperature < 80)'

Your first check

check evaluates a formula over a recorded trace. This five-sample trace is the one every SENTIL guide starts from:

time,speed
0,12
1,9
2,7
3,4
4,6

sentil check -f 'G (speed > 5)' -t speeds.csv

check
  formula     G (speed > 5)
  trace       speeds.csv
  semantics   dense
  verdict     violated
  robustness  -1.000000

The worst reading is the 4 at t=3, one short of the bound, so the robustness is -1.0: the same signed margin every binding computes, negative by exactly the amount the trace missed. What is STL covers how that number is built. The exit code of this run is 10, the violation verdict, so sentil check ... && deploy deploys only when the spec holds.

For a machine reader, -o json writes one self-describing object:

sentil check -f 'G (speed > 5)' -t speeds.csv -o json

{"backend":"cpu","elapsed_ms":0.0098,"formula":"G (speed > 5)","robustness":-1.0,"schema_version":"1.0","semantics":"dense","trace":"speeds.csv","verb":"check","verdict":"violated"}

Every JSON record the tool writes carries "schema_version": "1.0"; each verb's fields are tabulated under JSON output, and the elapsed_ms value varies run to run, shortened here.

Two flags widen the answer. --signal prints the robustness at every sample rather than the one value at the start, and --violations prints the intervals where the formula fails, [0.000, 3.000] on this trace. Dense semantics are the default and read the signal between samples to catch an inter-sample crossing; --semantics discrete evaluates only at the sample points and is the mode the next-step operator X needs.

Traces

A trace file pairs a time column with a column per signal. -t accepts csv, tsv, txt, json, and ndjson, sniffing the format from the content, so an extensionless file works; a .tsv extension forces tab splitting, and MATLAB .mat files read in the default build too. - reads the trace from stdin, which is how a pipeline hands one forward:

cat speeds.csv | sentil check -f 'G (speed > 5)' -t -

When a formula variable and a column differ in name, bind them with --map variable=column, repeatable once per variable. Parquet, Arrow, and SQLite need a binary built with --features formats; the release archives are default builds, and handing them such a file fails with a help line naming that flag. The trace formats reference has the column conventions per format.

Monitoring a live stream

monitor, alias stream, turns stdin into verdicts as each sample lands, so a live sensor pipes straight in and an alerter consumes the other end:

sensor | sentil monitor -f 'G[0,2] (speed > 5)' -o ndjson | alerter

Each input line is one JSON object with a time field and a numeric field per signal, like {"time": 3, "speed": 4}; --map variable=field bridges differing names. Several formulas run at once when separated by semicolons, and each gets an id in order: f0, f1, and so on. Save the five samples from above as JSON lines and the ndjson stream is:

{"time": 0, "speed": 12}
{"time": 1, "speed": 9}
{"time": 2, "speed": 7}
{"time": 3, "speed": 4}
{"time": 4, "speed": 6}

sentil monitor -f 'G[0,2] (speed > 5)' -o ndjson < samples.ndjson

{"event":"formulas","formulas":{"f0":"G[0,2] (speed > 5)"},"schema_version":"1.0"}
{"event":"sample","results":{"f0":{"resolved":false,"robustness":"-inf","satisfied":false}},"schema_version":"1.0","time":0.0}
{"event":"sample","results":{"f0":{"resolved":false,"robustness":"-inf","satisfied":false}},"schema_version":"1.0","time":1.0}
{"event":"sample","results":{"f0":{"resolved":true,"robustness":2.0,"satisfied":true}},"schema_version":"1.0","time":2.0}
{"event":"sample","results":{"f0":{"resolved":true,"robustness":-1.0,"satisfied":false}},"schema_version":"1.0","time":3.0}
{"event":"sample","results":{"f0":{"resolved":true,"robustness":-1.0,"satisfied":false}},"schema_version":"1.0","time":4.0}
{"event":"summary","samples":5,"schema_version":"1.0"}

Three record kinds make up the stream. A formulas record opens it, naming each id. One sample record follows per input line, its results mapping each id to {robustness, satisfied, resolved, probability?}. A summary record closes it with the total count when stdin ends. resolved turns true once the window a verdict depends on has fully passed; until then robustness is the string "-inf" or "inf" and satisfied is not yet meaningful. Here the first window [0,2] completes at t=2 with robustness 2.0, the tightest of the margins 7, 4, and 2, and each later sample completes the next window, so the dip drags the verdict to -1.0 at t=3. Text mode prints the same result one line per sample, colored on a terminal.

To monitor a probabilistic formula online, give each noisy signal a model with --noise and set the per-step particle count with --particles (default 1000). The estimate rides along the stream: text mode appends P= to each line, colored by whether the bound holds, and ndjson adds a probability field to each result. This is the CLI face of the live probability accessor every binding exposes.

sentil monitor -f 'P>=0.9(G[0,2] (speed > 5))' --noise 'speed=gaussian:0,0.3' --particles 500 < samples.ndjson

[t=0.000]  f0 viol P=0.0000
[t=1.000]  f0 viol P=0.0000
[t=2.000]  f0 sat P=1.0000
[t=3.000]  f0 viol P=0.0000
[t=4.000]  f0 viol P=0.0000

The window completing at t=2 has margin 2.0 against gaussian noise of standard deviation 0.3, better than six sigma of headroom, so every particle clears it and P=1.0000. The window at t=3 carries the dip, more than three sigma below the bound, and the estimate collapses to zero. Before t=2 no window has resolved yet.

Estimating a probabilistic specification

smc, alias prob, decides a P~p formula offline by simulation. It lifts the base trace into an ensemble under the noise models, evaluates the inner formula on every member, and reports the satisfaction probability with a confidence interval; what is PrSTL explains the operator.

sentil smc -f 'P>=0.9(G (speed > 3))' -t speeds.csv --noise 'speed=gaussian:0,0.5' --samples 10000

smc
  formula     P>=0.9(G (speed > 3))
  algorithm   smc
  samples     10000
  satisfied   9763
  probability 0.976300
  interval    [0.973131, 0.979103] at 95%
  verdict     holds

You can check that estimate by hand. The trace's closest call is the dip to 4, one unit above this bound, which is two standard deviations under noise of 0.5, so about 2.3 percent of realizations cross and the true probability sits near 0.977. The estimate lands on 0.9763 with a Wilson interval around it, and the verdict compares the result against the 0.9 threshold. The exit code follows the verdict: 0 for holds, 10 for does not hold.

--samples takes scientific notation such as 1e6, --seed (default 42) makes a run reproduce exactly, --confidence sets the interval level, and --interval chooses wilson or clopper-pearson; choosing an interval weighs them. --algo picks the decision procedure:

The sequential tests answer with a decision rather than an interval, and on an easy instance they answer fast:

sentil smc -f 'P>=0.9(G (speed > 3))' -t speeds.csv --noise 'speed=gaussian:0,0.5' --algo sprt

smc
  formula     P>=0.9(G (speed > 3))
  algorithm   sprt
  samples     27
  decision    accept_h1
  verdict     holds

Twenty-seven draws instead of ten thousand, because a true probability near 0.977 is far from the 0.9 threshold and the evidence is decisive early. The statistical methods reference covers all four procedures. Rare-event splitting is a library capability rather than a CLI verb; rare events shows where it lives.

When the noise should come from data instead of a guess, fit reads paired ground-truth and sensor columns and prints the fitted model:

sentil fit -t calib.csv --truth temp_true --sensor temp_meas --model gaussian

fit
  truth       temp_true
  sensor      temp_meas
  interaction additive
  model       gaussian
  residuals   200
  mean        0.003460
  std         0.298769

That calibration file was 200 rows of a sensor wandering around the truth with noise of standard deviation 0.3, and the fit recovers 0.2988 from the residuals. --model fits gaussian, bootstrap (the empirical distribution), or mixture (fit by EM, with --components setting how many, default 2), and --interaction chooses additive residuals y - g or multiplicative residuals y / g.

lift applies noise models to a trace and writes the lifted result as CSV on stdout, which is how you inspect what smc samples from:

sentil lift --noise 'speed=gaussian:0,0.5' -t speeds.csv --members 2 > lifted.csv

--members above one writes several realizations distinguished by a leading member column, and --seed (default 42) makes the draw reproducible. The full --noise grammar, all fifteen families with their aliases and the interaction suffix, is below.

Synthesis and falsification

synth reads an affine model from JSON and searches for the control-input sequence that best satisfies a spec on it. The model names its dynamics a and b, the start state x0, the variables, dt, horizon, and optionally bounds:

{"a": [[1.0]], "b": [[1.0]], "x0": [0.0], "variables": ["x"], "dt": 1.0, "horizon": 10, "bounds": {"lower": [-1.0], "upper": [1.0]}}

sentil synth -f 'F[0,10] (x > 4)' --model system.json

synth
  spec        F[0,10] (x > 4)
  method      gradient
  result      feasible
  robustness  6.000000
  input       [1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000]

This integrator gains at most 1 per step, so full push for ten steps reaches x=10 and clears the target of 4 by exactly the reported 6.0. --method is gradient by default, projected gradient ascent on the smooth robustness; cmaes switches to black-box search and milp to the complete mixed-integer encoding, a built-in branch and bound that works in the default build. An infeasible spec returns the minimally violating input rather than nothing, with exit code 10. The synthesis backends reference says when each fits.

falsify searches the same model shape for an input that violates the spec, and its exit code 10 means a counterexample was found, so 10 reads as "the spec fails" on every verb:

sentil falsify -f 'G[0,10] (x < 5)' --model system.json

falsify
  spec        G[0,10] (x < 5)
  method      cmaes
  result      counterexample found
  robustness  -5.000000
  input       [1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000, 1.0000]

Its --method accepts gradient and cmaes only; asking for milp is refused at runtime with "falsify searches with gradient or cmaes, not milp". --restarts (default 1) reruns cmaes from fresh starting points.

mine goes the other way: given a trace and a spec with a numeric parameter, it finds the tightest value that still holds. On a step response peaking at 1.08 against a reference of 1:

sentil mine --spec controls/overshoot --parameter max_overshoot -t step.csv

mine
  spec        controls/overshoot
  parameter   max_overshoot
  range       [0, 1]
  tightest    0.080000

The step overshoots by 0.08, and that is the answer. --range LO,HI overrides the parameter's declared range.

Specifications

The premade library replaces a hand-written formula. sentil specs lists the catalog, sentil specs <name> prints one in full with its formula, parameters, variants, and references, and --spec <name> stands in for -f on any verb that takes a formula. Override a parameter with -p key=value, repeatable, and select a variant with --variant:

sentil specs --filter overshoot
sentil specs controls/overshoot
sentil check --spec controls/overshoot -p max_overshoot=0.1 -t step.csv

On the step trace above that check passes with robustness 0.02, the room between the 1.08 peak and the loosened bound of 1.1. The catalog is on the specifications reference.

Errors and exit codes

Data goes to stdout; progress, logs, and errors go to stderr, and the spinner appears only on a terminal text run, so redirects stay clean. Color follows --color: auto colors a terminal, drops color in a pipe, and honors the NO_COLOR and CLICOLOR_FORCE conventions. The default SIGPIPE handler is restored at startup, so sentil specs | head ends the way Unix tools do. Run with no arguments, sentil prints the help and exits 2; it never prompts, and init, the one interactive verb, refuses to start without a terminal or under --no-input.

Failures render as diagnostics with a stable code, and a parse error underlines the offending token:

sentil::parse

  × could not parse the formula
   ╭────
 1 │ G (speed >> 5)
   ·           ┬
   ·           ╰── expected a value or `(`, found `>`
   ╰────

The exit code is the scripting contract:

monitor, fit, mine, and lift exit 0 on any successful run; the verdict codes come from check, smc, synth, and falsify. sentil explain exit-codes prints this table in the terminal.

Reference

The tables below cover every verb, flag, exit code, and output field the binary has; sentil <verb> --help renders the same flags inline.

The verbs

Global options

Every verb takes these, placed before or after its name.

check

Evaluate a formula over a recorded trace.

monitor

Stream stdin to verdicts; the flags mirror check minus the trace, plus the online noise pair.

smc

Estimate a probabilistic specification offline.

synth

Synthesize a control-input sequence against a model.

fit

Fit a noise model from paired ground-truth and sensor columns.

mine

Find the tightest value of a spec parameter that still holds on a trace. There is no -f here; mining needs a spec's declared parameters.

falsify

Search a model's input space for a spec violation.

lift

Apply noise models to a trace and write the result as CSV on stdout.

specs, explain, and completion

The operator topics are predicate, not, and, or, implies, always, eventually, until, historically, once, since, next, and probabilistic; exit-codes prints the exit table; and --fields covers check, monitor, smc, synth, falsify, fit, mine, lift, and specs, with lift describing its CSV shape since lift does not write JSON. Each operator answer pairs the grammar with the robustness rule:

sentil explain always

always
  grammar    always[a, b] phi  (unbounded as always phi)
  robustness the infimum of robustness over [t+a, t+b]; the property holds throughout the window

Noise model grammar

A --noise value reads signal=distribution:params[:additive|:multiplicative], parameters comma-separated. The optional third component sets how the noise couples to the signal and defaults to additive; speed=gaussian:0,0.3 adds zero-mean noise, while gain=dirac:0.5:multiplicative halves the signal deterministically.

The binomial trial count must be a whole number between 1 and 1,000,000. An unknown name errors with this list. bootstrap and mixture models cannot be written inline; they come from fit or from a spec's registered models. What each family is good for is on the noise models reference.

JSON output

-o json writes one object on stdout; -o ndjson writes one object per line and is monitor's natural mode. sentil explain <verb> --fields prints these tables in the terminal.

check

monitor

smc

synth and falsify

fit

mine

specs

lift writes CSV rather than JSON: a time column, one column per signal, and a leading member column when --members exceeds one.

Configuration

Configuration merges from several sources so a team sets defaults once. Highest to lowest: a command-line flag, a SENTIL_OUTPUT or SENTIL_COLOR environment variable, ./sentil.toml, the user config (~/.config/sentil/config.toml on Linux), /etc/sentil/config.toml, then the built-in default. An explicit --config FILE replaces the whole chain. sentil config shows which files exist and the values in effect, and an invalid value in a file warns rather than fails.

A file sets output and color, and defines aliases that expand when the name is not a built-in verb:

output = "json"
color = "never"

[alias]
overshoot = "check --spec controls/overshoot"

With that file, sentil overshoot -t step.csv expands to the full check, quoting preserved, and answers in JSON. An alias body can also be an argument list, overshoot = ["check", "--spec", "controls/overshoot"], for when a token would confuse whitespace splitting. An alias must expand to a real verb, and aliases do not chain.

Plugins

A verb that is neither built in nor an alias runs as an external command: sentil foo executes sentil-foo found on PATH (with .exe appended on Windows), passing the remaining arguments through and forwarding the child's exit code, or 70 when that code cannot be read. This is how a team grows subcommands without changing the binary. When no executable matches either, the error suggests both mechanisms.

Build features

cargo install sentil-cli builds with an empty default feature set, lean enough for the ARM and musl cross-builds. Two features widen it:

The CLI links the core directly rather than through the C ABI, so it runs at native engine speed.

Related pages