Julia

The Julia package binds the engine through ccall, so there is no glue layer and no build step of your own: add the package, point SENTIL_LIB at the core, and using Sentil brings the full surface into scope. Formulas build from the operators Julia already has, the way a JuMP constraint comes from a comparison, and mutating functions carry the trailing bang. The binding costs nothing you can feel: reading a robustness measures 114 ns against 112 ns for calling the core from Rust itself.

Install

Two pieces have to meet: the Julia package, which compiles nothing of its own because it is pure ccall, and the shared library it calls into. The package comes from the General registry. The library comes from a C ABI release bundle or from a cargo build in a checkout, and SENTIL_LIB names the file for the loader. The package does declare a per-platform artifact as a fallback, but the 0.3.0 entries in its Artifacts.toml still carry placeholder hashes and name tarballs no release builds, so the download fails and SENTIL_LIB is the route that works rather than an override.

From the Julia registry

At the Pkg REPL (press ]):

add Sentil

From a script it is import Pkg; Pkg.add("Sentil"). Julia 1.10 or newer. Every dependency is a standard library, so nothing builds and no compiler is involved on the Julia side.

using Sentil raises an InitError at this point, with SENTIL_LIB named in the message, because no core is on disk yet. A release bundle or a source build puts one there, and both are below.

From a GitHub release

Every tagged release attaches one C ABI bundle per platform. Julia reads the shared library inside it and ignores the rest; include/sentil.h and the pkg-config and CMake files under lib/ are there for the C and C++ builds.

No bundle here covers Linux on arm64 or Windows on arm64. For a Raspberry Pi or another ARM Linux board, the gnu archives on the CLI page carry lib/libsentil.so next to the binary and serve the same purpose, while the musl archive holds the CLI alone. Those ARM cores are built without the GPU feature, so gpu_available() raises on one rather than returning false. Windows on arm64 builds from source.

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

curl -LO https://github.com/sedislab/SENTIL/releases/download/v0.3.0/sentil-0.3.0-macos-arm64.tar.gz
tar xzf sentil-0.3.0-macos-arm64.tar.gz

$url = "https://github.com/sedislab/SENTIL/releases/download/v0.3.0/sentil-0.3.0-windows-x86_64.tar.gz"
Invoke-WebRequest -Uri $url -OutFile sentil.tar.gz
tar xzf sentil.tar.gz

export SENTIL_LIB="$PWD/sentil-0.3.0-linux-x86_64/lib/libsentil.so"

export SENTIL_LIB="$PWD/sentil-0.3.0-macos-arm64/lib/libsentil.dylib"

$env:SENTIL_LIB = "$PWD\sentil-0.3.0-windows-x86_64\lib\sentil.dll"

using Sentil
version()   # (0, 3, 0)

From source

Building the core needs a Rust toolchain from rustup.rs and a linker, which comes from a different place on each system. The repository-wide steps are on install from source; what follows is the Julia path through them.

xcode-select --install

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

export SENTIL_LIB="$PWD/target/release/libsentil.so"

export SENTIL_LIB="$PWD/target/release/libsentil.dylib"

$env:SENTIL_LIB = "$PWD\target\release\sentil.dll"

import Pkg
Pkg.develop(path="sentil-jl")

using Sentil
version()   # (0, 3, 0)

Your first monitor

using Sentil

phi = formula("G (speed > 5)")
trace = Trace(collect(0.0:1.0:4.0), "speed", [12.0, 9.0, 7.0, 4.0, 6.0])
robustness(phi, trace)   # -1.0

The result is -1.0: G, read always, keeps the worst margin, and the worst comes at t = 3 where the speed reads 4 against the 5 bound. A negative value is a violation and its size is how far the trace missed. What robustness means covers the semantics, and the grammar reference covers everything formula accepts.

Traces

A Trace maps signal names onto one time grid. Build one from vectors, a Dict, a file, or delimited text, and read values back by name.

trace = Trace([0.0, 1.0, 2.0], Dict("x" => [1.0, 2.0, 3.0], "y" => [0.5, 0.4, 0.3]))
add_signal!(trace, "z", [9.0, 8.0, 7.0])

trace["x"]           # [1.0, 2.0, 3.0]; an unknown name raises SemanticError
haskey(trace, "y")   # true
length(trace)        # 3

logged = read_trace("run.csv")            # format from the .csv or .tsv extension
inline = parse_trace("t,x\n0,1\n1,2")     # in-memory text; format=:csv or :tsv

The shipped core reads CSV and TSV; the extended formats on the trace formats reference need a core built with the matching features. For dense-time work, resample interpolates onto a new grid, and prepare fixes the interpolation once so resampling onto many grids is cheap:

fine = resample(trace, collect(0.0:0.1:2.0); interp=Interpolation.Cubic)
p = prepare(trace; interp=Interpolation.Linear)   # a PreparedTrace
finer = resample(p, collect(0.0:0.05:2.0))

The full constructor and accessor set is under trace functions below.

Streaming

An OnlineMonitor takes one update! per reading, and neither cost nor memory grows with the stream; the monotonic deque page covers how.

using Sentil

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

Each update! returns a Robustness; the loop's guard, verdict.resolved && !verdict.satisfied, alarms only on settled violations, since an open window reports value as the midpoint of lower and upper. A bounded horizon like the [0, 10] here is what lets a live stream ever resolve.

Every update! through a Dict allocates; resolve each variable's slot once with symbol_index and hand update_packed! a preallocated vector in that order.

i = symbol_index(monitor, "x")                        # 1-based slot in packed order
buf = Vector{Float64}(undef, variable_count(monitor))
buf[i] = read_sensor()
update_packed!(monitor, t, buf)

reset! rewinds the state, and run!(monitor, trace) replays a recorded trace, returning the verdict at every step.

Live probability

Give the constructor a lifting registry and the monitor tracks a P~p formula live; last_probability reads the running estimate after any update. It returns nothing for a deterministic formula and before the first sample arrives.

lifting = LiftingRegistry()
register_noise!(lifting, "x", gaussian(0.0, 0.3))

pm = OnlineMonitor(formula("P>=0.9 (G[0, 10] (x > -0.9))"), lifting)
update!(pm, 0.0, Dict("x" => 0.2))
last_probability(pm)   # the current satisfaction estimate

Probabilistic monitoring

Attach a noise model per sensor, and a check lifts the trace into an ensemble, evaluates the formula on every member, and reports a probability with a confidence interval; the P~p operator itself is covered in what PrSTL is.

Fit the model from calibration data rather than guessing it:

using Sentil

truth  = [10.0, 10.5, 11.0, 10.8, 10.2, 9.9, 10.4]
sensor = [10.2, 10.3, 11.3, 10.6, 10.5, 10.1, 10.2]
noise = fit_gaussian(residuals(truth, sensor))

lifting = LiftingRegistry()
register_noise!(lifting, "x", noise)   # consumes the model handle

trace = Trace(collect(0.0:1.0:30.0), "x", fill(10.5, 31))
phi = formula("P>=0.9 (G (x > 9))")

result = check(phi, trace, lifting)
result.probability   # the estimate over 10000 sampled trajectories
result.interval      # a ConfidenceInterval with lower, upper, level
result.holds         # whether the estimate meets the P>=0.9 threshold

check takes its settings as a keyword: check(phi, trace, lifting; config=SmcConfig(samples=5000, confidence=0.99)). check_conservative swaps in the Clopper-Pearson exact interval, check_distribution also returns the spread of robustness values across the ensemble, and lift(lifting, trace; seed=42) hands you one noisy realization when you want to see what the ensemble is made of. Choosing an interval is covered in confidence intervals, the seventeen families in noise models.

Sequential and Bayesian decisions

If a yes or no is all you need, the sequential tests get there in far fewer lifted samples than an estimate. Both take their config positionally, unlike check:

check_sequential(phi, trace, lifting, SprtConfig(0.85, 0.95)).verdict   # AcceptH0, AcceptH1, or Inconclusive
check_bayesian(phi, trace, lifting, BayesConfig(0.9)).verdict           # Holds, Fails, or Inconclusive

sequential_test and bayes_sequential_test run the same tests over any () -> Bool source you supply, with no trace involved.

Rare events

check_rare_event runs adaptive multilevel splitting over a StochasticSystem, with its config as a keyword; rare events explains how the splitter reaches probabilities sampling cannot:

system = StochasticSystem(["x"], 1.0, 200;
    init = seed -> [0.0],
    step = (prev, t, seed) -> [0.9 * prev[1] + 0.1 * randn()])

rare = check_rare_event(phi, system; config=RareEventConfig(particles=8192))
rare.probability   # with rare.violation_probability, rare.holds, rare.simulations

The GPU path takes a declarative SimModel, not a StochasticSystem, because the dynamics must lower onto the device. Without a gpu build and a present device it raises EvaluationError with code SENTIL_ERR_GPU rather than silently falling back to the CPU; probe with gpu_available() first. Declaring a SimModel is shown under stochastic systems.

Synthesis

Synthesis runs the engine backward: given a system model, bounds, and a spec, find an input that satisfies it. The package covers open-loop synthesis, a receding-horizon controller, falsification, and parameter mining; the solvers behind them are on synthesis backends.

using Sentil

a = reshape([1.0], 1, 1)
b = reshape([1.0], 1, 1)
model = linear_model(a, b, [0.0], ["x"], 1.0, 10)
spec = formula("F[0, 10](x > 5) & G[0, 10](x < 12)")

result = synthesize(model, spec; bounds=Bounds(fill(-3.0, 10), fill(3.0, 10)))
result.input        # the input sequence found
result.robustness   # positive when the spec is met
result.holds
result.backend      # the solver that ran, e.g. Backend.Gradient

synthesize is keyword-driven: bounds, smooth, backend, max_iters, and population all have working defaults, and Backend.Auto picks a solver from the problem's structure. An infeasible spec returns the least violating input rather than nothing.

The online form is a Controller that re-plans every step within a hard deadline, here one millisecond:

controller = Controller(linear_model(a, b, [0.0], ["x"], 1.0, 10), spec, 1, 1_000_000;
                        bounds=Bounds([-3.0], [3.0]))
u = control(controller, [0.0])   # the planned input for this step

Controller consumes the model and spec it is built from. SafetyFilter, ChanceConstraint, falsification, and parameter mining are all under synthesis and optimization.

Errors and the consume contract

Every failure raises a subtype of the abstract SentilError: ParseError for text that does not parse, with the offending column in the message; SemanticError for well-formed input the engine cannot use, an unknown variable or a statistical check on a formula with no P operator; EvaluationError for everything at runtime, from an invalid config to a failed fit. Each carries msg and a code::SentilErrorCode, the same stable status every binding surfaces, enumerated on error codes.

try
    formula("G (speed >")
catch e
    e isa ParseError && println("bad formula: ", e.msg)
end

One contract is worth knowing before it bites: composition consumes its operands. always(f) and its family, &, |, !, until, since, probability, Monitor(f), register_noise! on its model, mixture on its components, Controller, ChanceConstraint, and SafetyFilter on theirs, and the SpecBuilder chain all take ownership of the handles they build on. Touching a consumed handle raises EvaluationError saying the handle is no longer usable. The escape hatch is copy(f):

p = formula("speed > 5")
g = always(copy(p))    # the copy is consumed, p stays usable
h = eventually(p)      # p is consumed here
# robustness(p, trace) would now raise EvaluationError

Handles free their native memory through finalizers; close!(handle) releases it eagerly instead. Calling it twice is safe, and a closed handle raises the same typed error rather than touching freed memory. The cross-binding conventions are in handling errors across bindings.

Reference

The exported names in full; signatures show keyword defaults exactly as the source defines them.

Package and handles

Enums

Each enum is a small module, so members read as TimeMode.Dense and never collide across enums.

SentilErrorCode is a flat @enum of the C status integers, SENTIL_OK = 0 through SENTIL_ERR_PANIC = 17.

Trace functions

A Trace owns its grid and signals; the accessors copy values out, so what you get back is yours.

Base extensions: length, isempty, haskey(trace, name), and indexing trace[name] (getindex), which raises SemanticError for a name the trace does not carry.

Ring buffers

RingBuffer(capacity) holds the newest timed samples with running statistics. Queries with no answer return nothing; positional queries return a Sample with found, time, and value.

Base extensions: length, isempty, and 1-based indexing b[i], which raises BoundsError out of range.

Formula building

Parse text, or build from terms. A term is a Sentil.Expr (deliberately unexported, so the name never shadows Base.Expr), created by variable and literal and combined with ordinary operators; comparing two terms yields a predicate Formula rather than a Bool. Every combinator consumes its operands, per the contract above.

Base extensions on terms and formulas: arithmetic +, -, *, /, % (also mod), and ^ with Real coercion on either side; comparisons <, <=, >, >=, ==, != building predicates; boolean !, ~, &, | on formulas; and the math functions abs, sqrt, exp, log, sin, cos, tan, floor, ceil, min, max on terms.

speed = variable("speed")
phi = always(speed > 5; lower=0.0, upper=10.0)   # G[0, 10](speed > 5)

Formula evaluation

dense=true interpolates between samples so a crossing between grid points still counts; discrete versus dense is the guide.

Monitors

Monitor compiles a formula once and serves both whole-trace and streaming evaluation under a Config. Building one from a Formula consumes it; building from text does not involve a handle at all.

Streaming monitors

OnlineMonitor is the streaming-only form: no whole-trace calls and the smallest state. Its constructors borrow their arguments rather than consuming them.

Both monitor types return a Robustness struct: resolved, satisfied, value, lower, upper.

Multi-formula monitoring

MultiMonitor advances several named formulas from one sample stream; FormulaBank evaluates a named set over a whole trace at once. add! borrows a Formula, so yours stays usable.

length and isempty work on both.

Noise models and lifting

Each of the seventeen families has its own constructor returning a NoiseModel. One naming caveat: binomial is deliberately unexported because the bare name is Base's binomial coefficient, so qualify it as Sentil.binomial(n, p); a bare binomial(20, 0.4) reaches Base.binomial and fails on the Float64.

Fitting and registration:

Statistical checks

The estimators behind check, and the interval helpers usable with no trace at all. Every number here is checkable by hand.

SmcResult carries probability, interval::ConfidenceInterval, satisfactions, samples, and holds. RobustnessDistribution carries count, mean, variance, std_dev, min, max.

Sequential tests

Both configs are positional in the check calls, and both tests also run standalone over a Bernoulli source you supply.

SprtResult is verdict, samples, log_likelihood; BayesResult is verdict, samples, posterior. The theory is on the SPRT page.

Stochastic systems and simulation

Two ways to describe dynamics. A SimModel is declarative, built from SimExpr terms, which is what allows it to lower onto a GPU. A StochasticSystem runs host callbacks, so any Julia function can be the dynamics.

SimExpr supports +, -, *, / and the math functions abs, sin, cos, tan, sqrt, exp, log, floor, ceil, min, max, each combination consuming its operands, the same contract formulas follow. An AR(1) process in three lines:

ar1 = SimModel(["x"], 1.0, 200,
               [sim_const(0.0)],
               [sim_prev(1) * 0.9 + sim_noise(1)],
               [gaussian(0.0, 1.0)])
trace = simulate(ar1; seed=7)

Rare-event estimation

RareEventResult is probability, violation_probability, holds, simulations; RareEventEstimate is probability and simulations; GpuSplittingEstimate is violation_probability, particles, levels. For adaptive_multilevel_splitting, initial_state(seed) and step(state, seed) return a state, is_terminal(state) returns (terminal, in_rare_event), and score(state) returns a real. The method itself is on rare events.

Synthesis and optimization

The synthesizers, controllers, and search entry points, then the smooth semantics and numeric helpers they are built from.

SynthesisResult is input, robustness, holds, and backend::Backend.T, the solver that actually ran. Witness is input, robustness, and the trace it produces. ChanceReport is estimate, lower_bound, samples, holds.

Specification library

The shipped specification catalog, resolved by name. The builder chain consumes itself at each step, so keep the returned builder, not the one you passed in.

available_specs()   # includes "aerospace/altitude_hold"
b = with_param(SpecBuilder("aerospace/altitude_hold"), "tolerance", 50.0)
build_deterministic(b)       # the PrSTL text
monitor = build_monitor(b)   # consumes b

The library itself, with each spec's source and citation, is documented under specifications.

Related pages