From a model to a released package

One model end to end: from the model store to a package taktwerk loads, released, run, and back from the run’s record. The model is aerobic_fed_batch, an aerobic fed-batch culture on glucose, with offgas, an estimator that tracks it from the off-gas and the dissolved oxygen. Both packages it ends in are generated; a third, a filter written by hand, shows what you write when the model language is not the tool.

How to write a model is in the modeling tutorials, which this page does not repeat: your first model, composition and balances, estimation and identifiability.

Fences tagged exec run in document order, in one shell session, from the root of the clone; just tutorial runs them after Getting started. Each chapter ends in a command and the result to check.

Before you start

Getting started, cc, zig and cargo-zigbuild for the packages, and taktwerk 0.11 or newer as taktwerk on your PATH:

cargo build --quiet -p labinetix
export PATH="$PWD/target/debug:$PATH"
taktwerk --version

taktwerk 0.…

1. The model in the store

models/aerobic_fed_batch/ is one entity of the store:

• authoring/aerobic_fed_batch.toml, what you write: species with their formulas, two reactions (growth and maintenance) on biomass, a feed, oxygen transfer by a kLa correlation and a quasi-steady gas phase. The biomass yield y_xs is the one given coefficient; oxygen, CO2, water and ammonia follow from the elements.
• aerobic_fed_batch.lock.json, the content hash and version;
• generated/, what labinetix define sync writes from it: the IR, a ModelingToolkit view and the raw package, a crate with its header and descriptor. The kernel itself goes to crates/kernels/core-models/generated/.
• scenarios/ and estimators/, pinned to the model’s hash.

labinetix define list | grep aerobic_fed_batch

estimator	offgas	1.0.0	sha256:…
model_scaffold	aerobic_fed_batch	1.0.0	sha256:5572908c…

define check re-generates the whole store and compares every file byte for byte; silence is success. An edit to authoring/ is followed by define sync, which moves the hash; every scenario and estimator pinned to the old one is then refused until you review and re-pin it.

labinetix define check

The balance report says what the composition is and what the estimator’s instruments determine. The starred coefficients are derived; the electron residual of each reaction is zero to rounding. Off-gas O2 and CO2 and the biomass determine both reaction rates with one degree of redundancy, a balance test on the measurements:

labinetix define balance model_scaffold/aerobic_fed_batch --estimator offgas

  off_gas_o2       measures oxygen
  off_gas_co2      measures co2
  do_pct           measures oxygen
  c_x_out          measures biomass
  parameter states: y_xs
…
  growth          0.5000     -1.0000     -0.3835*     0.5722*     0.3805*    -0.0692*    …
  maintenance           .    -1.0000     -1.0657*     1.4657*     0.6000*           .    …
…
  rank 2 of 2 reactions, redundancy 1: every reaction rate is determined
  determined directions: 2; balance tests on the measured rates: 1

2. Simulate a scenario

scenarios/batch-then-feed.toml pins the model’s content hash and says how to run it: RK4, steps of 0.01 h in 200 substeps, 1600 steps, a row every tenth. The culture grows on 25 g/L glucose, exhausts it at about 8 h, and from step 850 (8.5 h) a feed of 0.01 L/h keeps it glucose-limited to 16 h. analyze simulate steps the generated kernel through core-integrate, the same code the package runs; its output is the committed prediction, byte for byte:

labinetix analyze simulate models/aerobic_fed_batch/scenarios/batch-then-feed.toml \
  | cmp - models/aerobic_fed_batch/scenarios/batch-then-feed.prediction.json && echo identical

identical

3. The estimator and its EKF package

estimators/offgas/authoring/offgas.toml is an estimator entity: the model it is pinned to, every state’s initial value and noise, the biomass yield as a random-walk parameter state, and the measured outputs in row order:

[model]
entity = "model_scaffold/aerobic_fed_batch"
version = "1.0.0"
content_hash = "sha256:5572908c88754a75694b93f793aa22d0fb5a73c0b2142e90d35d3fe14c572d6a"

[[parameter_states]]
parameter = "y_xs"
q = 1e-8
p0 = 1e-2
min = 0.0

[[measured]]
output = "off_gas_o2"
r = 1e-8

define sync estimator/offgas writes an EKF package from it under its generated/raw/: the model’s kernel with its exact Jacobians, core-filters’ EKF, behind aerobic_fed_batch_ekf_offgas.h. Because y_xs is the model’s free yield, the derived coefficients follow it through the balances: the filter cannot leave them. The package’s inputs are the model’s inputs and one <output>_meas per measured row, NaN when a sample is missing; Q, R and the χ² gate are tunables; the outputs are the estimate, the model’s outputs at it, the variances and the update’s report (nis, rows, flags).

ls models/aerobic_fed_batch/estimators/offgas/generated/raw/package

aerobic_fed_batch_ekf_offgas.h
taktwerk-model.toml

The proof estimators/offgas/scenarios/batch-then-feed.toml runs the model scenario of chapter 2 as the plant, the off-gas and the dissolved oxygen read every step, the biomass once an hour, and starts the estimator 36 % high on biomass and at y_xs = 0.4 where the plant’s is 0.5. The committed record beside it holds the hash of every row and the yield the filter ends at:

grep -E '"(rows|bit_identical|final_parameter_states)"' \
  models/aerobic_fed_batch/estimators/offgas/scenarios/batch-then-feed.taktwerk.json

  "rows": 1600,
  "bit_identical": true,
  "final_parameter_states": { "y_xs": 0.500006… }

just raw-ekf-proof reproduces it: both packages wired in one taktwerk project, an offline row a fault value of NaN cleared at each sample, against the host reference that steps the packages’ own Rust in taktwerk’s order. Every row must be bit-identical (--write rewrites the record; a test holds the committed one to its hashes without taktwerk):

just raw-ekf-proof aerobic_fed_batch

aerobic_fed_batch/offgas/batch-then-feed: bit-identical, 1600 rows × 24 values

4. A hand-written algorithm

What the model language does not hold, you write by hand: a filter, a controller, a plant with its instruments. It takes two crates. The kernel, under crates/kernels/core-*, holds the arithmetic: no_std, no unsafe, no allocation, no I/O. The package, under crates/packages/raw-<name>, binds C structs to it and holds no math. The example is a first-order low-pass filter, τ·ẏ = u − y.

crates/kernels/core-lowpass samples it exactly for an input held over each step, y ← y + a·(u − y) with a = 1 − exp(−T/τ), so the step response at the samples is 1 − exp(−k·T/τ) at any step size; τ = 0 passes the input through. Its test compares the step response with that closed form.

crates/packages/raw-lowpass is liblowpass.so behind package/lowpass.h:

lowpass_init, lowpass_step and lowpass_terminate are the only unsafe code, a site listed with its count in policy/unsafe-allowlist.toml; they read and write the engine’s structs around Filter, the instance in safe Rust that the package’s tests step. The descriptor package/taktwerk-model.toml is what taktwerk import-header --shape lowpass.h reads from the header, and tests/header.rs compiles the header with cc and compares every size and offset with the Rust structs.

A package has no evidence until a committed run proves it: raw-lowpass has no evidence.toml, so it ships as experimental (chapter 5).

cargo test -p core-lowpass -p raw-lowpass 2>&1
just boundary-lint

test the_step_response_is_the_continuous_filter_sampled ... ok
…
test a_step_input_rises_with_the_time_constant ... ok
…
test header_layout_matches_the_rust_structs ... ok

5. A package per target

A target is a file under hardware/targets/: a triple and, for a device, the newest glibc its libraries may reference. The host target writes no triple; it is the build machine:

labinetix build target host-linux

id host-linux
description The build host

build raw-package builds every package for a target, hand-written and generated, checks each library against the target’s glibc floor, and writes dist/<name>-<version>-<arch>/ (with -glibc<floor> for a device target): the descriptor, the header, lib/<arch>/lib<name>.so and package.toml, plus one deterministic tarball each and dist/SHA256SUMS. A device target is the same command with its name; the build cross-compiles for aarch64, x86_64 or armv7 through zig.

labinetix build raw-package host-linux 2>&1 | grep -E 'aerobic_fed_batch|lowpass|packages for'

raw-package: dist/aerobic_fed_batch-…-….tar.gz interface sha256:69a901fd…
raw-package: dist/aerobic_fed_batch_ekf_offgas-…-….tar.gz interface sha256:4738e7f0…
raw-package: dist/lowpass-…-….tar.gz interface sha256:f67d7b1a…
raw-package: … packages for host-linux in dist/, SHA256SUMS

package.toml is for people and release tooling; taktwerk does not read it. It carries the product version (one for every package of a release), the target, the interface fingerprint (SHA-256 over the descriptor’s name, dimensions and each variable’s name, causality, type and shape, in order: a changed default or unit moves nothing, a renamed or reordered variable does) and the maturity with its evidence: simulated for a committed proof in simulation, plant for a run on a real plant cited by run id and hash, experimental otherwise.

export version=$(labinetix --version | cut -d' ' -f2) arch=$(uname -m)
cat dist/aerobic_fed_batch-$version-$arch/package.toml
grep maturity dist/aerobic_fed_batch_ekf_offgas-$version-$arch/package.toml \
  dist/lowpass-$version-$arch/package.toml

name = "aerobic_fed_batch"
version = "…"
target = "host-linux"
interface = "sha256:69a901fd…"
maturity = "simulated"
record = "models/aerobic_fed_batch/scenarios/batch-then-feed.three-way.json"
dist/aerobic_fed_batch_ekf_offgas-…/package.toml:maturity = "simulated"
dist/lowpass-…/package.toml:maturity = "experimental"

An interface change that appends an input or tunable, off at its default with the old behaviour bit for bit, is minor; anything else is major.

The built filter runs under taktwerk as it is: a step from 0 to 1 with a time constant of 10 s, one tick a second. After ten ticks, one time constant, it is 1 − 1/e of the way:

rm -rf target/lifecycle && mkdir -p target/lifecycle
cat > target/lifecycle/lowpass.toml <<EOF
[engine]
tick_ms = 1000.0

[models.lowpass]
kind = "raw"
path = "../../dist/lowpass-$version-$arch"

[[instance]]
id = "lp"
model = "lowpass"

[instance.parameters]
y0 = 0.0
time_factor = 1.0

[[recorder]]
id = "step"
signals = ["lp.y", "lp.e"]
EOF
taktwerk run target/lifecycle/lowpass.toml --speed max --no-connectors --cycles 10 \
  --set lp.u=1.0 --set lp.tau=10.0 --record-dir target/lifecycle/records 2>/dev/null
gzip -dc target/lifecycle/records/lowpass/step/*/part-0001.csv.gz | tail -1

9,9.0,0.6321205588285577,0.36787944117144233

The three-way proof

A generated package is proven by its model’s scenarios: just raw-three-way runs each through analyze simulate, through the package under taktwerk run --speed max and through the package’s FMU under taktwerk’s FMI adapter, and requires every recorded row identical in every state, output, input and t. taktwerk records after each tick’s step, so the prediction’s initial row has no recorded twin. --write commits the result beside the scenario as batch-then-feed.three-way.json, the record the plant package’s maturity cites:

just raw-three-way aerobic_fed_batch

aerobic_fed_batch/batch-then-feed: bit-identical, 160 rows × 14 values, raw and fmi

Sidebar: the FMU

Any FMI 3 host runs a package as a co-simulation FMU: taktwerk fmu-wrap wraps a dist/ directory, the tunables’ start values as the FMU’s start values, --target for another architecture. A release carries the package; an FMU is made from it.

taktwerk fmu-wrap dist/aerobic_fed_batch-$version-$arch \
  -o target/lifecycle/aerobic_fed_batch.fmu --write 2>&1 | tail -1
taktwerk inspect --kind fmi target/lifecycle/aerobic_fed_batch.fmu | head -1

wrote target/lifecycle/aerobic_fed_batch.fmu
model aerobic_fed_batch (fmi)

6. Release and hand-over

dist/ is the hand-over. Build output is never committed: a release attaches one tarball per package and architecture, <name>-<version>-<arch>[-glibc<floor>].tar.gz, and SHA256SUMS over all of them. A tarball unpacks to the package directory taktwerk loads and is packed deterministically (sorted entries, mtime 0, owner 0). Whoever receives it checks it first:

(cd dist && sha256sum -c SHA256SUMS)

aerobic_fed_batch-…-….tar.gz: OK
aerobic_fed_batch_ekf_offgas-…-….tar.gz: OK
lowpass-…-….tar.gz: OK

The receiver reads package.toml for what it is: version, target, interface fingerprint, maturity and the evidence behind it. The model and its proofs stay here, in the store, pinned by the hashes the evidence cites.

7. Continue in taktwerk

examples/tutorial-lifecycle/ is a taktwerk project of the two generated packages: the model’s as the plant, the estimator’s reading the plant’s off-gas, dissolved oxygen and biomass (scenario.toml is the model scenario batch-then-feed as taktwerk events). One tick is one step of 0.01 h, 36 s of engine time. The plant’s [[instance]] table is what labinetix define instance writes from the model’s defaults and the scenario; parameter values are instance configuration, never baked into a library (--parameter-set adds estimated ones):

diff <(labinetix define instance model_scaffold/aerobic_fed_batch --scenario batch-then-feed \
         | sed -n '/^\[instance.parameters\]/,$p') \
     <(sed -n '/^\[instance.parameters\]/,/^$/{/^$/q;p}' examples/tutorial-lifecycle/project.toml) \
  && echo "the plant's parameters are the scenario's"

the plant's parameters are the scenario's

just example stages the project with its packages from dist/ under target/examples/tutorial-lifecycle/ and runs it there, as fast as the machine computes it. The @io recorder keeps every input and output of every tick:

just example tutorial-lifecycle --scenario scenario.toml --speed max 2>&1 | tail -1

cycles 1600  published 1600  overruns 0  stale 0  …  stop time limit reached

Without --speed max the same project runs in real time, its tunables open over taktwerk’s OPC UA server. The workbench, devices and deployment are taktwerk’s: its tutorial From a package to a running device takes a package from here to an edge device and a plant.

The store in the workbench

labinetix serve shows this repository’s store read-only in the taktwerk workbench: entities and their locks, each model’s interface, equations, composition and balances, scenarios with their predictions, estimators with their proofs, and packages with their descriptors, evidence and dist/ artefacts. It prints its own address and announces itself, so a taktwerk serve on the same machine lists it under Add-ons; a package’s staged example opens in taktwerk from there. The UI is built once with just workbench-ui (needs node), before cargo build:

just workbench-ui && cargo build -p labinetix
labinetix serve        # in another terminal: taktwerk serve <folder>, then Add-ons → labinetix

8. Back from the plant

A record comes back as a run directory, <dir>/<project>/<recorder>/<run-id>/. analyze replay re-runs its inputs on the host through the packages’ own Rust, with the tunables of its events.csv and the parameters of the project file it pins by hash, and compares every recorded output bit for bit. It is how you know a record is what the package computes, and not a fault, a skipped tick or a swapped library:

export run=$(ls -d target/examples/tutorial-lifecycle/records/project/io/*/)
labinetix analyze replay "$run" --project target/examples/tutorial-lifecycle/project.toml

plant (aerobic_fed_batch): 1600 rows × 11 outputs bit-identical
ekf (aerobic_fed_batch_ekf_offgas): 1600 rows × 20 outputs bit-identical

analyze import-record turns the record into a run of a dataset of the model: the outputs to observe with their standard deviations, the inputs as recorded, each held from the tick that used it, and the initial state from the project. Here the biomass and the off-gas CO2 once an hour; the biomass at 8 h is the prediction’s of chapter 2, to the last digit. A dry run by default; --write writes it under models/aerobic_fed_batch/datasets/, labinetix define sync dataset/<name> locks it, and estimation fits the model to it.

labinetix analyze import-record "$run" --model-dir models/aerobic_fed_batch \
  --dataset tutorial-lifecycle --dataset-doc "The lifecycle tutorial's run under taktwerk" \
  --run batch-then-feed --instance plant --inputs n_st,f_air,f_in \
  --observe c_x_out=0.05,off_gas_co2=0.0001 --every 100 \
  --project target/examples/tutorial-lifecycle/project.toml 2>&1
grep '"t": 8.0,' models/aerobic_fed_batch/scenarios/batch-then-feed.prediction.json

8.0,c_x_out,10.485139388858332,0.05
…
8.5,f_in,0.01
…
dry run: run `batch-then-feed` of dataset/tutorial-lifecycle is not written; --write writes it
    {"t": 8.0, "x": [5.0,10.485139388858332,…

Where to go next

• taktwerk’s documentation: projects, scenarios with events and faults, recorders, campaigns, and From a package to a running device.
• CLI reference: define instance, define balance, build raw-package, analyze replay, analyze import-record.