Java

The Java package binds the same engine every other language uses, through a small JNI shim. The published jar carries the compiled core for your platform, so a project with a JDK and nothing else can monitor a trace. Everything lives in the flat package io.github.sedislab.sentil.

Types that hold a native handle, Formula, Trace, OnlineMonitor, NoiseModel, and their kin, extend the public NativeResource base and implement AutoCloseable, so open them in try-with-resources and the handle frees at the end of the scope. Value types like Robustness and Interval are plain immutable objects with nothing to manage. Every call that can fail throws a checked SentilException. A robustness call from Java measures about 680 ns over the core in the cross-language benchmark.

Install

Two ways in. The jar from Maven Central is the one to reach for, since it carries the compiled engine and a project with a JDK needs nothing else. A build from a checkout covers an unreleased change, a platform the published jar does not carry, or work on the binding itself. There is no download route: the releases page carries no Java asset, because Maven Central is where the jar is published.

From Maven Central

<dependency>
  <groupId>io.github.sedislab</groupId>
  <artifactId>sentil</artifactId>
  <version>0.3.0</version>
</dependency>

implementation 'io.github.sedislab:sentil:0.3.0'

import io.github.sedislab.sentil.Sentil;

public class Check {
    public static void main(String[] args) {
        System.out.println(Sentil.version());   // 0.3.0
    }
}

The jar carries two shared libraries per platform under native/<os>-<arch>/, the engine and the JNI shim, each named the way its own platform names libraries: libsentil.so and libsentil_jni.so on Linux, the same pair with .dylib on macOS, sentil.dll and sentil_jni.dll on Windows. The first time you touch a native-backed type, both are extracted to a temporary directory and loaded, engine first, so the shim resolves the engine sitting beside it. There is nothing to configure, and no system property or environment variable overrides that path. Four platforms are inside the published jar: Linux x86_64, macOS x86_64, macOS arm64, and Windows x86_64. On anything else, Linux on arm64 included, the load throws an UncheckedIOException naming the folder it looked for, and the source build below is the way in.

From source

Maven drives all three toolchains: one package runs cargo build --release --package=sentil-ffi for the engine, javac -h for the JNI headers, and CMake for the shim. You need Maven, a Rust toolchain from rustup.rs, CMake 3.16 or newer, a C++17 compiler, and a JDK 11 or newer whose include directory carries jni.h. A runtime-only Java install does not carry that header; Adoptium publishes full JDKs for Linux, macOS, and Windows.

xcode-select --install

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

mvn -DskipTests package

mvn -B test

javac -cp target/sentil-0.3.0.jar Check.java
java -cp target/sentil-0.3.0.jar:. Check    # prints 0.3.0; on Windows the classpath separator is ;

Your first monitor

Two handles in one try-with-resources, one robustness call.

import io.github.sedislab.sentil.Formula;
import io.github.sedislab.sentil.Trace;

try (Trace trace = Trace.create(new double[] {0, 1, 2, 3, 4});
        Formula phi = Formula.parse("G (speed > 5)")) {
    trace.addSignal("speed", new double[] {12, 9, 7, 4, 6});
    System.out.println(phi.robustness(trace));   // -1.0
}

The result is -1.0, the margin at t = 3, where speed sits at 4 against the bound of 5. What is STL explains how to read the number, and the operator reference covers G, read always, and its siblings.

One robustness value summarizes the whole trace. Three more calls give the detail behind it:

double[] curve = phi.robustnessSignal(trace);   // robustness at every sample
double dense = phi.robustnessDense(trace);      // dense time, reads between samples
for (Interval v : phi.violations(trace)) {      // the spans where it fails
    System.out.println(v.start() + " to " + v.end());
}

robustnessDense and robustnessDenseSignal interpolate between samples so an inter-sample crossing is not missed; the discrete versus dense guide covers when the two differ.

Traces

A Trace collects named signals over a shared time vector that must strictly increase. Build one from arrays, or read one from a file and let the reader dispatch on the extension:

try (Trace a = Trace.fromSignal(new double[] {0, 1, 2}, "x", new double[] {1.0, 0.5, 0.2});
        Trace b = Trace.fromPath("flight.csv")) {
    a.addSignal("y", new double[] {0.0, 0.1, 0.4});
    System.out.println(b.variables());
}

fromPath reads csv, tsv, parquet, and the other formats on the trace formats reference; fromCsv and fromTsv parse in-memory text. resample reads a trace onto a new grid under an Interpolation mode, and prepare fixes the interpolation coefficients into a PreparedTrace when you resample the same signal many times.

Streaming

An OnlineMonitor watches a live stream without ever storing it: memory stays proportional to the largest temporal window and each update is O(1) amortized. The monotonic deque is the structure underneath.

import io.github.sedislab.sentil.OnlineMonitor;
import io.github.sedislab.sentil.Robustness;
import java.util.Map;

try (OnlineMonitor monitor = OnlineMonitor.create("G[0, 10] (x > -0.9)")) {
    for (int t = 0; t < 60; t++) {
        Robustness verdict = monitor.update(t, Map.of("x", Math.sin(t * 0.3)));
        if (verdict.resolved() && !verdict.satisfied()) {
            System.out.printf("violated at t=%d, robustness=%.3f%n", t, verdict.value());
            break;
        }
    }
}

While the monitor is still filling a future-time window, resolved() is false and satisfied() is provisional, which is why the formula bounds its horizon with [0, 10].

The packed hot path

update takes a map, which means boxed doubles and a name lookup on every call. symbolIndex gives each variable's position once, and updatePacked then takes a plain double[] with neither cost:

try (OnlineMonitor monitor = OnlineMonitor.create("G[0, 5] (x > 0 & y < 2)")) {
    int xi = (int) monitor.symbolIndex("x").getAsLong();
    int yi = (int) monitor.symbolIndex("y").getAsLong();
    double[] packed = new double[(int) monitor.variableCount()];
    packed[xi] = 0.7;
    packed[yi] = 1.1;
    monitor.updatePacked(0.0, packed);
}

Do not assume the order; symbolIndex is the contract, and it returns an empty OptionalLong for a variable the formula never reads.

Streaming probability

A streaming monitor can track a probabilistic formula online. OnlineMonitor.withLifting lifts each reading into a particle ensemble through a noise registry, and lastProbability() reads the running satisfaction estimate after any update:

try (Formula phi = Formula.parse("P>=0.95 (G[0, 10] (x > 0))");
        LiftingRegistry lifting = new LiftingRegistry();
        NoiseModel noise = NoiseModel.gaussian(0.0, 0.3)) {
    lifting.register("x", noise);
    try (OnlineMonitor monitor = OnlineMonitor.withLifting(phi, lifting,
            new SmcConfig().samples(500))) {
        for (int t = 0; t < 40; t++) {
            monitor.update(t, Map.of("x", 0.4 + 0.05 * t));
            monitor.lastProbability().ifPresent(p -> System.out.println("P = " + p));
        }
    }
}

lastProbability() returns an empty OptionalDouble for a deterministic formula or before the first update. withLifting borrows the formula and the registry, so both stay usable after.

To run several formulas under one clock, use a MultiMonitor; to score a batch of named formulas over one recorded trace, a FormulaBank. Both are tabled in the reference below.

Probabilistic monitoring

Attach a NoiseModel to each sensor variable through a LiftingRegistry; check then estimates how often the inner formula holds under that noise and reports a confidence interval. For the operator itself, start at what is PrSTL:

import io.github.sedislab.sentil.*;

double[] times = new double[20];
double[] xs = new double[20];
for (int i = 0; i < 20; i++) {
    times[i] = i;
    xs[i] = 0.4 + 0.05 * i;
}
try (Trace trace = Trace.create(times);
        LiftingRegistry lifting = new LiftingRegistry();
        Formula phi = Formula.parse("P>=0.9 (G (x > 0))")) {
    trace.addSignal("x", xs);
    lifting.register("x", NoiseModel.gaussian(0.0, 0.3));

    SmcResult result = phi.check(trace, lifting, new SmcConfig().samples(5000));
    System.out.printf("P = %.3f in [%.3f, %.3f], holds %b%n",
            result.probability(), result.interval().lower(),
            result.interval().upper(), result.holds());
}

The two-argument register(variable, model) uses the additive interaction; pass a NoiseInteraction third argument for a multiplicative residual. The model is consumed by registration. Families and fitting are on the noise models reference, and the interval math on confidence intervals.

Two variants refine the fixed-budget check. checkConservative reports the exact Clopper-Pearson interval instead of Wilson. checkDistribution also returns the robustness distribution across the ensemble, which tells you how close the population sits to the threshold rather than only how often it clears it.

Sequential tests

The fixed-budget check above spent 5000 draws on a question a sequential test settles in a few dozen:

SprtResult sprt = phi.checkSequential(trace, lifting, new SprtConfig(0.85, 0.95));
// sprt.verdict() is ACCEPT_H0, ACCEPT_H1, or INCONCLUSIVE; sprt.samples() says how
// many draws the decision took

BayesResult bayes = phi.checkBayesian(trace, lifting, new BayesConfig(0.9));
// bayes.verdict() is HOLDS, FAILS, or INCONCLUSIVE; bayes.posterior() is the
// posterior satisfaction estimate under the Beta(1, 1) prior

SprtConfig(p0, p1) is Wald's SPRT over the indifference band [p0, p1] with error rates alpha and beta defaulting to 0.05. BayesConfig(threshold) stops when the Bayes factor passes its cutoff, 100 by default. Both cap at maxSamples (100000) and take a seed. The three regimes are compared on the statistical methods reference.

Rare events

Monte Carlo cannot resolve a probability far below one in a million; adaptive multilevel splitting can. Describe the system as a SimModel, one init and one advance expression per variable, convert it, and check:

try (Formula phi = Formula.parse("P>=0.9999 (G[0, 200] (q < 1))");
        SimModel model = SimModel.create(
                new String[] {"q"}, 1.0, 200,
                new SimExpr[] {SimExpr.constant(0.0)},
                new SimExpr[] {SimExpr.prev(0).mul(0.9).add(SimExpr.noise(0))},
                new NoiseModel[] {NoiseModel.gaussian(0.0, 0.1)});
        StochasticSystem system = model.toStochasticSystem()) {
    RareEventResult r = phi.checkRareEvent(system);
    // r.probability() and r.violationProbability() sum to one;
    // r.simulations() counts the trajectories the splitter ran
}

For dynamics that will not fit a declarative model, StochasticSystem.custom wraps two host callbacks, a SystemInit and a SystemStep. When a GPU is present, Gpu.isAvailable() returns true and checkRareEventGpu(model, config) runs the splitting on the device; the CPU path stays available either way. How splitting works is on the rare events concept page.

Synthesis

Every value below is checked by the binding's test suite: an integrator driven by five inputs bounded to [-3, 3], with a spec that wants x past 5 within the horizon.

try (SystemModel model = SystemModel.linear(
                new double[][] {{1.0}}, new double[][] {{1.0}},
                new double[] {0.0}, new String[] {"x"}, 1.0, 5);
        Formula spec = Formula.parse("F[0, 5] (x > 5)");
        Bounds bounds = new Bounds(new double[] {-3, -3, -3, -3, -3},
                new double[] {3, 3, 3, 3, 3})) {
    SynthesisResult r = Synthesis.synthesize(model, spec, bounds,
            new SmoothConfig(), Backend.GRADIENT, 200, 0);
    // r.input() is {3, 3, 3, 3, 3}: push as hard as allowed every step
    // r.robustness() is 10.0 and r.holds() is true; x reaches 15 > 5
}

The bounds arrays run one entry per input element over the whole horizon. synthesize borrows the model and spec, and shorter overloads drop the smoothing, backend, iteration cap, and population to let the library choose; backend tradeoffs are on the synthesis backends reference.

Controller, SafetyFilter, ChanceConstraint, and the falsification pair falsify and findCounterexample are all tabled in the synthesis reference below.

Errors

Every fallible call throws a checked SentilException carrying the engine's message, which names the offending construct and where it arose. Three subclasses split the kinds:

try {
    Formula phi = Formula.parse("G (speed >");   // throws before any resource exists
    phi.close();
} catch (ParseException e) {
    System.err.println("bad formula: " + e.getMessage());
} catch (SentilException e) {
    System.err.println("error " + e.errorCode() + ": " + e.getMessage());
}

All three subclasses extend SentilException and share its (String message, int code) constructor, so catching the base catches everything. errorCode() returns the stable ErrorCode behind the failure and code() its integer form, the same status the C ABI and every other binding surface; ErrorCode.fromCode(int) maps an integer back to the enum, yielding UNKNOWN for an unrecognized value. The full code list is on the error codes reference, and the cross-language mapping on handling errors across bindings.

Handles and consumption

NativeResource, the public base of every handle-owning type, implements AutoCloseable with an idempotent close(); a Cleaner frees a handle you forget, but try-with-resources is the idiom. Using a closed handle throws an unchecked IllegalStateException naming the type.

Some calls hand a handle to the core, which closes the Java object as a side effect. Reusing a consumed object throws the same IllegalStateException, so write consuming chains as one expression:

Everything else borrows. In particular OnlineMonitor.fromFormula and withLifting, MultiMonitor.add and addProbabilistic, FormulaBank.add, Synthesis.synthesize, findCounterexample, and falsify leave their arguments usable. Closing a consumed object again is harmless.

Reference

Everything below lives in io.github.sedislab.sentil. Methods that reach the engine declare throws SentilException; the accessors on plain result types do not throw.

Library

Formulas

Formula is the parsed specification. Parse, inspect, and evaluate:

The combinators build a formula operator by operator, consuming their operands:

The probabilistic and synthesis evaluation methods on Formula are tabled with statistical checks and synthesis.

The Expr builder

Expr builds predicates programmatically, for formulas assembled from data rather than parsed from text. Start a term with a static factory, combine terms, then compare two terms to get a Formula. Every method consumes the terms it acts on, so chain:

try (Formula phi = Expr.var("speed").sub(5).abs().lt(2)) {
    // the predicate |speed - 5| < 2
}

The BinaryOp enum (ADD, SUB, MUL, DIV, MOD, POW) and ComparisonOp enum (LT, LE, GT, GE, EQ, NE) name the operations these methods encode.

Traces

PreparedTrace.resample(double[] times) reads the prepared signal onto a grid without refitting. Interpolation is LINEAR, ZERO_ORDER_HOLD, or CUBIC_SPLINE.

Monitors and streaming

Monitor pairs one formula with a Config and works both offline and one sample at a time. Its constructors consume the formula; the static parse factories skip the intermediate Formula entirely.

Monitor.check uses the monitor's own SMC settings, which are the defaults unless the monitor came from SpecBuilder.intoMonitor, where the spec's recommended settings ride along. Config carries the time mode: new Config() is discrete, new Config(TimeMode.DENSE) evaluates densely, and timeMode() reads it back.

OnlineMonitor is the dedicated streaming monitor from the streaming section:

Robustness reports resolved(), satisfied(), and value(); while a probabilistic verdict is unresolved, value() is the midpoint of [lower(), upper()].

MultiMonitor drives several streaming formulas under one clock:

FormulaBank takes add(id, formula) in either form, plus ids(), size(), and isEmpty(); robustness(trace) and robustnessDense(trace) return a map keyed by id. If any formula fails to evaluate, the call throws and names the offending id rather than returning a partial map.

RingBuffer keeps the newest samples up to a fixed capacity, with running statistics maintained as samples enter and leave:

Sample carries found(), time(), and value(); a query with no answer returns a sample whose found() is false.

Noise models and lifting

NoiseModel has one static constructor per family:

Fitting and inspection:

NoiseInteraction is ADDITIVE or MULTIPLICATIVE. LiftingRegistry connects models to signals: register(variable, model, interaction) or the two-argument additive form, variables(), isEmpty(), and lift(trace, seed) for one seeded noisy realization of a trace.

Statistical checks

The checking methods on Formula:

The configuration and result types:

StochasticSystem is the sampling form the estimators consume. custom(String[] variables, double dt, long horizon, SystemInit init, SystemStep step) wraps host callbacks, simulate(long seed) draws one trajectory, and variables(), dt(), and horizon() describe it. SystemInit.init(long seed) returns the initial state; SystemStep.step(double[] previous, double time, long seed) returns the next. Both may run on several threads, so they must be thread-safe.

SimModel is the declarative alternative and the only form the GPU path accepts: create(variables, dt, horizon, init, advance, noise) consumes its expression and noise arrays, then simulate(seed), variables(), dt(), horizon(), and toStochasticSystem(). SimExpr terms come from prev(variable), time(), constant(value), and noise(source), combine with add, sub, mul, div (each also accepting a double), min, max, and pass through abs, sin, cos, sqrt, exp, ln, and negate, consuming like Expr.

Stats exposes the interval and sizing primitives directly, over raw counts rather than traces:

Stats.wilson(50, 100, 0.95);               // [0.403831, 0.596169]
Stats.clopperPearson(50, 100, 0.95);       // [0.398321, 0.601679]
Stats.jeffreys(50, 100, 0.95);             // the Beta(1/2, 1/2) credible interval
Stats.agrestiCoull(50, 100, 0.95);         // the Agresti-Coull approximation
Stats.interval(IntervalMethod.WILSON, 50, 100, 0.95);   // pick the method at run time
Stats.zScore(0.95);                        // 1.959964
Stats.chernoffHoeffdingSamples(0.1, 0.05); // 185
Stats.wilsonSamples(0.01, 0.95);           // 9604

sequentialTest(SprtConfig config, BooleanSupplier draw) and bayesSequentialTest(BayesConfig config, BooleanSupplier draw) run the sequential machinery over any Bernoulli source you supply, one draw per call on the calling thread.

Synthesis.adaptiveMultilevelSplitting(AmsInterface simulator, long particles, double targetScore, long maxSteps, long seed) runs the splitter over a fully user-defined simulator and returns a RareEventEstimate with probability() and simulations(). AmsInterface packs its state into bytes: implement stateSize(), initialState(seed), step(state, seed), isTerminal(state, inRareEvent), and score(state), all thread-safe.

Synthesis and optimization

The static entry points on Synthesis:

A concrete anchor, verified by the test suite: Synthesis.maximize on the concave objective -(x-3)^2 - (y+1)^2 climbs to the peak at (3, -1), and mineTightestParameter over G[0, 2](x < c) on traces peaking at 3 and 5 returns 5.0.

Models, bounds, and results:

The online and search surface:

Formula.smoothRobustness(trace) and smoothRobustness(trace, config) evaluate the differentiable surrogate. smoothValueAndGradient(trace, config) returns a SignalGradient, the value with a [variable][sample] gradient in sorted variable order, and smoothGradient(model, initial, input, config) returns an InputGradient, the value with one gradient entry per input coordinate; both gradient types expose value() and gradient(). findCounterexample(model, bounds, maxIters, smooth) descends the smooth robustness; falsify(model, bounds, config, restarts) searches globally with restarted CMA-ES on exact robustness. The callback interfaces are single-method: GradientObjective.evaluate(x, gradient) returns the value and fills the gradient, BatchObjective.evaluate(points) scores a population, ParameterFormula.make(param) builds the formula the miner probes, and Rollout.rollout(initial, input) returns a trajectory as one row of horizon + 1 samples per variable.

The specifications library

Every binding and the CLI expose one registry of shipped specifications, and SpecBuilder is Java's door into it. Pick one by name, adjust it, and turn it into a formula or a preloaded monitor:

import io.github.sedislab.sentil.SpecBuilder;

System.out.println(SpecBuilder.available().size());   // 54, sorted names

try (SpecBuilder spec = new SpecBuilder("aerospace/airspeed_envelope")
        .withParam("V_stall", 115.0);
        Formula phi = spec.buildFormula()) {
    System.out.println(spec.buildDeterministic());   // the formula text, filled in
}

withVariant and withParam consume the builder and return a new one, so chain them; a rejected name or parameter still consumes the input, so start again from the name.

The settings carriers are plain: SpecSmcSettings has confidence() and sampleBudget(); SpecSprtSettings has p0(), p1(), alpha(), beta(), and maxSamples(); SpecAmsSettings has numParticles() and maxSteps(). The catalog itself is on the specifications reference.

Enums

Every enum carries code(), the integer the C ABI uses.

ErrorCode.UTF8 covers a string argument that was not valid UTF-8, and ErrorCode.fromCode(int) is the reverse mapping. The value types Robustness, Interval, Sample, ConfidenceInterval, SmcResult, SprtResult, BayesResult, RareEventResult, RareEventEstimate, GpuSplittingEstimate, RobustnessDistribution, ChanceReport, SynthesisResult, and Version override toString with a readable dump, and Version adds value-based equals and hashCode.

Related links