difftilt

Falsification of cyber-physical systems by tilting a pretrained generative prior toward inputs that violate an STL specification. difftilt is a psy-taliro Optimizer: psy-taliro owns system modelling, STL evaluation, signal parameterization, budget accounting and parallelism, and difftilt contributes the search strategy — draw candidates from a trained joint prior over (input signals × output traces), reweight or steer them with a surrogate, hand the flat samples back to psy-taliro to simulate.

Training is out of scope. The prior is loaded from a checkpoint.

Two tilt mechanisms:

mechanism	how
selection	draw a pool from the prior untilted, reweight by exp(-beta * score)
guidance	steer the reverse diffusion with the surrogate's gradient

Sign convention throughout: lower = closer to failure.

Install

uv sync                      # package + test/lint/type tooling + the lazy-import deps
uv sync --extra at           # + matlabengine, for the Simulink AT benchmark

Requires Python 3.9 or 3.10. .python-version pins 3.9 because that is the interpreter matlabengine==9.12.21 (MATLAB R2022a) is built for. The test suite passes identically on both — see Python version.

Documentation

Built with Sphinx and organised on Diátaxis — tutorial, how-to, reference, explanation, kept separate because they answer different questions.

uv sync --group docs
uv run sphinx-build -b html docs docs/_build/html

Tutorial	one lesson, start to finish, no MATLAB or GPU needed
How-to guides	bring your own model · check a prior · choose a tilt · custom surrogate
Check a prior	the hygiene doctor: bounds, padding, normalizer statistics
Reference	740 signatures, autodoc'd from the source so it cannot drift
Explanation	who declares what · known issues

Verify

uv run pytest -q                  # 1208 passed, 39 skipped   (no GPU, no MATLAB, no artifacts)

The 35 skips beyond the 4 permanent ones are golden-value tests that read the machine-local ~850 MB preprocessing archives. Point at them to run those too:

DIFFTILT_REPO_ROOT=/path/to/research/tree uv run pytest -q --slow
# 1243 passed, 4 skipped

The 4 remaining skips are legitimate N/A conformance cases (identity declares no bounds, rank-only does not support gradients), not deferred work.

Bring your own model

demos/at/at_falsification.py is the file to copy. Everything in it is either a declaration about your system or a declaration about your checkpoint; difftilt supplies the rest and refuses to guess the parts you leave out.

at = dt.SystemSpec(                       # the PROBLEM -- yours
    name="AT",
    inputs=[dt.Signal("throttle", bounds=(0., 100.), control_points=1001),
            dt.Signal("brake",    bounds=(0., 325.), control_points=1001)],
    traces=["speed", "rpm"],
    interval=(0., 50.),
)
schema = at.model_schema(x_length=1008, y_length=5008,   # the CHECKPOINT's geometry
                         trace_native_length=5001, padding="zero")
prior = dt.PriorBundle.from_state_dict("demos/at/models/dual_joint_epoch220.pt",
                                       architecture="dual_unet_joint",
                                       schema=schema, normalizer=normalizer).build_prior()
result = staliro(model, spec, dt.DiffTilt(prior, surrogate_factory=dt.GPSurrogate), options)

Who declares what — nothing is typed twice:

fact	declared by
input names, search bounds, control points, interval	you, in SystemSpec
trace names and their STL order	you, in SystemSpec
tensor lengths, padding scheme, normalization	the checkpoint
total simulation budget	derived from warmup, verify_per_round, online_iterations

Any disagreement between the two sides is a load-time error with a diff, never a shape mismatch deep inside load_state_dict and never silence.

Run it against the shipped AT benchmark:

uv run --extra torch python demos/at/check_prior.py     # check the wiring first
uv run --extra at    python demos/at/at_falsification.py

Check failures against evaluations in the output. With the default failure_policy="skip" a campaign absorbs every rejection and still reports an ordinary-looking round count, so if those two numbers are equal, nothing was measured.

Layout

src/difftilt/     THE PACKAGE -- 15 modules, ~13,500 lines. This is the software.
tests/            the contract
demos/            two worked examples of USING difftilt. Neither is part of the
                  package, and neither ships in the wheel.
  at/               automatic transmission: zero padding, per-channel affine,
                    2 traces. at_falsification.py is the file to copy.
  cc/               chasing cars: EDGE padding, logit on inputs, scalar affine
                    on traces, 4 traces. Same package, no changes to it.
  */check_prior.py  the hygiene doctor, run against that checkpoint
docs/             tutorial · how-to · reference · explanation

The split is the point: a checkpoint, a Simulink model, an STL formula and a surrogate are what a user brings. The two demos differ in every one of those and the package absorbs both by declaration alone — which is the clearest statement of what difftilt does and does not own. Neither ships in the wheel, which contains exactly the 16 modules and py.typed.

src/ is load-bearing rather than fashionable: the repo, the distribution and the import package are all called difftilt, so "am I importing the installed one or the source tree?" needs an unambiguous answer. tests/test_import_hygiene.py is the test that cares.

Import cost

import difftilt pulls in numpy and nothing else — no torch, no staliro, no matplotlib. The names that need them (DiffTilt, the tilt mechanisms, the diffusion prior) resolve on first attribute access via PEP 562. That is why torch, diffusers, scikit-learn and gpytorch are optional extras rather than dependencies. test_import_hygiene.py asserts it; do not break it by hoisting an import to module level.

Three environment constraints that are not preferences

Each was established by something breaking.

1. psy-taliro == 1.0.0b9, exact. difftilt targets the beta API (staliro.core.optimizer.Optimizer, staliro.core.sample.Sample, staliro.optimizers.Behavior). 2.x and 3.x moved all three.
2. torch must be imported before matlab.engine. MATLAB ships its own zlib and shadows the system one; a torch imported afterwards cannot read its own .pt files and fails with archive does not contain any files on a file that is perfectly intact. Every campaign script has import torch as its first non-stdlib import.
3. Start the MATLAB engine before loading the prior. Engine startup fails intermittently, and one of its two failure modes kills the process outright with no traceback, so a try/except around construction does not catch it. The prior load costs ~30 s of GPU time; discovering a dead engine after paying that is pure waste.

Also: nvidia-smi enumerates this machine's GPUs in the reverse order to torch, so following nvidia-smi picks the sm_61 GTX 1080 that the pinned torch cannot use instead of the sm_75 Quadro RTX 4000. difftilt.priors.resolve_device already handles this — do not "fix" it to follow nvidia-smi.

Python version

Both 3.9 and 3.10 pass the full suite. The constraint is MATLAB, not difftilt — the matlabengine version tracks your MATLAB release:

interpreter	matlabengine	MATLAB
3.9 (default)	9.12.21	R2022a
3.10	24.1.x	R2024a — a different Simulink engine, so results are not comparable across the two

psy-taliro 1.0.0b9 itself declares >=3.8,<3.11, which is the upper bound.

Known issues

Carried forward honestly in docs/KNOWN-ISSUES.md — seven of them, all pre-existing, none introduced by packaging.