Examples
Examples
Short recipes for the tasks you actually need to hit the ground running on a project.
We include five examples in every language binding, namely, offline monitoring in discrete time, offline monitoring in dense time, online streaming, probabilistic monitoring, and synthesis. Each example is a self-contained program that you can run to see the monitor in action and it's purpose is to get you started quickly with SENTIL.
The canonical set
Offline monitoring, discrete time
Evaluate a trace against a formula and read the robustness, the per-sample signal, and the violation intervals.
Offline monitoring, dense time
Read the same trace as a continuous signal so that a dip between two samples is counted.
Online streaming
Fold one timestamped sample at a time and read a running verdict.
Checking a PrSTL property
Register a sensor noise model, lift each reading into an ensemble, and estimate satisfaction probability with a confidence interval.
Synthesis
Solve a specification for a control input, then shield a nominal controller with a safety filter.
Migrating from another tool
If you already have formulas written for another monitor, these pages translate them and show you how to migrate from that tool to SENTIL.
Coming from RTAMT
Discrete and dense STL monitoring, offline and online, with the operator names lined up.
Coming from Breach
Dense-time robustness, with a reference case study.
Coming from UPPAAL-SMC
Statistical model checking of a probabilistic property against a known satisfaction probability.
Recipes
Short, task-shaped answers for the work that comes after the first monitor runs.
Load traces
Read CSV, Parquet, Arrow, and the other trace formats into a Trace.
Use the spec library
Reach for a premade, standards-derived specification instead of writing one.
The Simulink block
Drop the streaming monitor into a model as an S-Function block.
Reproduce a claim
Run a single entry from the claims ledger and check the artifact against the expected value.
Run the benchmarks
Drive the benchmark runners and plot SENTIL against the baseline tools.
New to the library? Start with your first monitor, then come back here to see the same idea in every language.