mirror of
https://github.com/vercel-labs/fx.git
synced 2026-10-28 10:15:17 +08:00
Move the TLA+ Bun drivers into tests/tla/drivers
- Move `drive.mjs`, `drive-agents.mjs`, `agent-process.mjs`, and `graph.mjs` from `tests/tla/sdk/` to `tests/tla/drivers/`. They read the state graphs that `tests/tla/sdk/check.sh` writes. - Point CI, `AGENTS.md`, `sdk/AGENTS.md`, and the `tests/tla` notes at the new paths.
This commit is contained in:
13 files changed
+52
-45
No files matched your search
+13
-13
@@ -374,19 +374,19 @@ jobs:
|
||||
curl -fsSL -o "$jar" https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
|
||||
echo "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 $jar" | sha256sum -c -
|
||||
TLA2TOOLS_JAR="$jar" tests/tla/sdk/check.sh
|
||||
bun tests/tla/sdk/drive.mjs send --walks 40
|
||||
bun tests/tla/sdk/drive.mjs lookup --walks 40 --seed 7
|
||||
bun tests/tla/sdk/drive.mjs send --walks 20 --seed 3 --durability world
|
||||
bun tests/tla/sdk/drive.mjs lookup --walks 20 --seed 9 --durability world
|
||||
bun tests/tla/sdk/drive.mjs write --walks 20 --seed 4
|
||||
bun tests/tla/sdk/drive.mjs cutoff --walks 20 --seed 5
|
||||
bun tests/tla/sdk/drive.mjs leased --walks 40 --seed 12
|
||||
bun tests/tla/sdk/drive.mjs queue --walks 40 --seed 4
|
||||
bun tests/tla/sdk/drive-agents.mjs send --walks 60 --seed 11
|
||||
bun tests/tla/sdk/drive-agents.mjs consume --walks 60 --seed 13
|
||||
bun tests/tla/sdk/drive-steer.mjs ideal --walks 20 --seed 2
|
||||
bun tests/tla/sdk/drive-steer.mjs faults --walks 20 --seed 4
|
||||
bun tests/tla/sdk/drive-steer.mjs faults --walks 10 --seed 6 --backend wasm
|
||||
bun tests/tla/drivers/drive.mjs send --walks 40
|
||||
bun tests/tla/drivers/drive.mjs lookup --walks 40 --seed 7
|
||||
bun tests/tla/drivers/drive.mjs send --walks 20 --seed 3 --durability world
|
||||
bun tests/tla/drivers/drive.mjs lookup --walks 20 --seed 9 --durability world
|
||||
bun tests/tla/drivers/drive.mjs write --walks 20 --seed 4
|
||||
bun tests/tla/drivers/drive.mjs cutoff --walks 20 --seed 5
|
||||
bun tests/tla/drivers/drive.mjs leased --walks 40 --seed 12
|
||||
bun tests/tla/drivers/drive.mjs queue --walks 40 --seed 4
|
||||
bun tests/tla/drivers/drive-agents.mjs send --walks 60 --seed 11
|
||||
bun tests/tla/drivers/drive-agents.mjs consume --walks 60 --seed 13
|
||||
bun tests/tla/drivers/drive-steer.mjs ideal --walks 20 --seed 2
|
||||
bun tests/tla/drivers/drive-steer.mjs faults --walks 20 --seed 4
|
||||
bun tests/tla/drivers/drive-steer.mjs faults --walks 10 --seed 6 --backend wasm
|
||||
|
||||
- name: Test libfx on a World
|
||||
run: |
|
||||
|
||||
@@ -282,7 +282,8 @@ Every TLA+ spec, its TLC checker, the Bun drivers that walk real code along a sp
|
||||
|
||||
* `tests/tla/session_manager/`: the session manager's specs, mutants, and trace checkers, plus `system-design.md`, which defines the `D1` to `D62` decision numbers that session code cites
|
||||
* `tests/tla/indexer/`: the indexer refresh model; `check.sh` requires each config's expected verdict
|
||||
* `tests/tla/sdk/`: the libfx durable session and agent routing specs and their Bun drivers, which CI runs in the `SDK (Bun + N-API/WASM)` job
|
||||
* `tests/tla/sdk/`: the libfx durable session, agent routing, and steering specs
|
||||
* `tests/tla/drivers/`: the Bun drivers that walk the real SDK code along the `sdk/` specs' state graphs; CI runs them with the SDK specs in the `SDK (Bun + N-API/WASM)` job
|
||||
|
||||
Code comments cite a spec by its path, such as `tests/tla/session_manager/Wiring.tla`. When a change alters behavior that a spec models, update the spec in the same change and run its checker.
|
||||
|
||||
|
||||
+1
-1
@@ -114,7 +114,7 @@ python3 benchmarks/first_frame.py --binary /tmp/fx-before --binary ./zig-out/bin
|
||||
|
||||
### Check a TLA+ model
|
||||
|
||||
`tests/tla/` holds TLA+ models of the session manager, the workspace indexer, and libfx durable sessions. CI runs the libfx model; run the matching checker yourself when you change behavior that one of the others describes. You need Java and `tla2tools.jar`, and `tests/tla/README.md` covers setup.
|
||||
`tests/tla/` holds TLA+ models of the session manager, the workspace indexer, and libfx durable sessions and steering. CI runs the libfx model; run the matching checker yourself when you change behavior that one of the others describes. You need Java and `tla2tools.jar`, and `tests/tla/README.md` covers setup.
|
||||
|
||||
```bash
|
||||
tests/tla/session_manager/check.sh SessionLog
|
||||
|
||||
+2
-2
@@ -59,8 +59,8 @@ Do not treat the demos or this file as the implementation contract. When prose a
|
||||
| `encodeXtermKeyEvent()` or `xtermAdapter()` only | `sdk/node/test-xterm-adapter.mjs` |
|
||||
| Core debugger query behavior or automation state | `sdk/tests/test-core-browser.mjs` |
|
||||
| Terminal demo asset references, integrity, or cache policy | Package into a fresh temporary directory and inspect the generated HTML, manifest, and headers |
|
||||
| Durable sessions: leases, fencing, takeovers, tool reruns, the UI stream | `sdk/tests/test-durable-core.mjs` on memory, local, world, and queue (the core with a scripted harness; world is an app-built World passed to `world()`, queue one whose queue delivers as Vercel Queues does, with `queueLeases`), `sdk/tests/test-durable.mjs` on memory, local, and world, then `tests/tla/sdk/check.sh` and `bun tests/tla/sdk/drive.mjs send`, `lookup`, `write`, `cutoff` (deadline cut-offs up to their bound), `leased` (a World without liveness, where each worker renews a short lease), and `queue` (a World whose queue shows whether a worker lives, so leases are held without renewals), which walk the real code along the TLC state graphs of `DurableSession.tla`; change the spec with the code. For agent names and routing, also `bun tests/tla/sdk/drive-agents.mjs send` and `consume`, which walk `AgentRouting.tla`'s graphs with each process in a worker thread of its own. With a Vercel access token, also run both against Vercel's World: `test-durable.mjs vercel native` and `drive.mjs --durability vercel`, configured as `sdk/tests/vercel-storage.mjs` describes |
|
||||
| Steering: interrupts, waits during tools, joins, hand-backs on cancel, image handoffs, steer ids | The libfx steering tests in `src/acp/libfx_steering.zig`, `sdk/tests/test-agent-steering.mjs` and `sdk/tests/test-durable.mjs` on native and wasm, then `tests/tla/sdk/check.sh` and `bun tests/tla/sdk/drive-steer.mjs ideal` and `faults`, with `--backend wasm` too, which walk the real code along the TLC state graphs of `DurableSteer.tla`; change the spec with the code |
|
||||
| Durable sessions: leases, fencing, takeovers, tool reruns, the UI stream | `sdk/tests/test-durable-core.mjs` on memory, local, world, and queue (the core with a scripted harness; world is an app-built World passed to `world()`, queue one whose queue delivers as Vercel Queues does, with `queueLeases`), `sdk/tests/test-durable.mjs` on memory, local, and world, then `tests/tla/sdk/check.sh` and `bun tests/tla/drivers/drive.mjs send`, `lookup`, `write`, `cutoff` (deadline cut-offs up to their bound), `leased` (a World without liveness, where each worker renews a short lease), and `queue` (a World whose queue shows whether a worker lives, so leases are held without renewals), which walk the real code along the TLC state graphs of `DurableSession.tla`; change the spec with the code. For agent names and routing, also `bun tests/tla/drivers/drive-agents.mjs send` and `consume`, which walk `AgentRouting.tla`'s graphs with each process in a worker thread of its own. With a Vercel access token, also run both against Vercel's World: `test-durable.mjs vercel native` and `drive.mjs --durability vercel`, configured as `sdk/tests/vercel-storage.mjs` describes |
|
||||
| Steering: interrupts, waits during tools, joins, hand-backs on cancel, image handoffs, steer ids | The libfx steering tests in `src/acp/libfx_steering.zig`, `sdk/tests/test-agent-steering.mjs` and `sdk/tests/test-durable.mjs` on native and wasm, then `tests/tla/sdk/check.sh` and `bun tests/tla/drivers/drive-steer.mjs ideal` and `faults`, with `--backend wasm` too, which walk the real code along the TLC state graphs of `DurableSteer.tla`; change the spec with the code |
|
||||
| Supported public behavior or setup | Update `sdk/README.md` in the same change |
|
||||
|
||||
Use Node.js 24 for SDK tests. CI relies on its JSPI implementation behind `--experimental-wasm-jspi`.
|
||||
|
||||
+11
-9
@@ -6,7 +6,8 @@ TLA+ specifications for fx, checked with TLC, together with the scripts and Bun
|
||||
|---|---|---|
|
||||
| `session_manager/` | The session log, turn lifecycle, writer lock, snapshots, fork, subagents, catalog, host wiring, the side-file move, and v1 conversion. `system-design.md` is the design record the specs check and defines the `D1` to `D62` decision numbers that code comments cite. | `session_manager/check.sh` |
|
||||
| `indexer/` | Refreshing a scanned root, and when a previous listing may be reused. | `indexer/check.sh` |
|
||||
| `sdk/` | libfx durable sessions (`DurableSession.tla`) and agent names and routing (`AgentRouting.tla`). `drive.mjs` and `drive-agents.mjs` walk the real SDK code along TLC's state graphs and check every step against the model. | `sdk/check.sh`, then the drivers |
|
||||
| `sdk/` | libfx durable sessions (`DurableSession.tla`), agent names and routing (`AgentRouting.tla`), and steering (`DurableSteer.tla`). `check.sh` also writes the TLC state graphs the drivers walk. | `sdk/check.sh`, then the drivers |
|
||||
| `drivers/` | The Bun drivers. `drive.mjs`, `drive-agents.mjs`, and `drive-steer.mjs` walk the real SDK code along the `sdk/` state graphs and check every step against the model. | `bun drivers/drive.mjs`, `bun drivers/drive-agents.mjs` |
|
||||
|
||||
## Requirements
|
||||
|
||||
@@ -33,14 +34,15 @@ npm ci --prefix sdk/durable
|
||||
From the repository root:
|
||||
|
||||
```sh
|
||||
tests/tla/session_manager/check.sh # every session spec
|
||||
tests/tla/session_manager/check.sh SessionLog Fork # selected specs
|
||||
tests/tla/session_manager/mutants.py # every planted bug must be caught
|
||||
tests/tla/session_manager/trace/selftest.sh # the trace validator must accept and reject
|
||||
tests/tla/indexer/check.sh # every refresh config and its expected verdict
|
||||
tests/tla/sdk/check.sh # the SDK specs; writes the state graphs the drivers walk
|
||||
bun tests/tla/sdk/drive.mjs send --walks 40 # one durable-session graph; see .github/workflows/ci.yml for the rest
|
||||
bun tests/tla/sdk/drive-agents.mjs send --walks 60 # agent routing
|
||||
tests/tla/session_manager/check.sh # every session spec
|
||||
tests/tla/session_manager/check.sh SessionLog Fork # selected specs
|
||||
tests/tla/session_manager/mutants.py # every planted bug must be caught
|
||||
tests/tla/session_manager/trace/selftest.sh # the trace validator must accept and reject
|
||||
tests/tla/indexer/check.sh # every refresh config and its expected verdict
|
||||
tests/tla/sdk/check.sh # the SDK specs; writes the state graphs the drivers walk
|
||||
bun tests/tla/drivers/drive.mjs send --walks 40 # one durable-session graph; see .github/workflows/ci.yml for the rest
|
||||
bun tests/tla/drivers/drive-agents.mjs send --walks 60 # agent routing
|
||||
bun tests/tla/drivers/drive-steer.mjs ideal --walks 20 # steering
|
||||
```
|
||||
|
||||
`Fork` and `V1Conversion` can run for many minutes. `session_manager/README.md` describes each session spec, the planted bugs, and the trace checkers.
|
||||
File renamed without changes.
@@ -2,7 +2,7 @@
|
||||
// AgentRouting.tla, and checks after every step that the code is where the
|
||||
// model allows.
|
||||
//
|
||||
// bun tests/tla/sdk/drive-agents.mjs [send|consume] [--walks N] [--depth N] [--seed S]
|
||||
// bun tests/tla/drivers/drive-agents.mjs [send|consume] [--walks N] [--depth N] [--seed S]
|
||||
//
|
||||
// Two processes, p1 and p2, are two worker threads (agent-process.mjs), each
|
||||
// with a module instance and a globalThis of its own: p1 has the agents S
|
||||
@@ -45,7 +45,7 @@ const random = () => {
|
||||
const pick = (items) => items[Math.floor(random() * items.length)];
|
||||
|
||||
const here = fileURLToPath(new URL(".", import.meta.url));
|
||||
const graph = await loadGraph(resolve(here, "graphs", `agents-${mode}.dot`));
|
||||
const graph = await loadGraph(resolve(here, "../sdk/graphs", `agents-${mode}.dot`));
|
||||
const hosts = { p1: ["S", "C"], p2: ["S"] };
|
||||
|
||||
// The queue the processes share: every message, until a step delivers it.
|
||||
@@ -3,10 +3,11 @@
|
||||
// WebAssembly, along paths of the TLC state graph of DurableSteer.tla, and
|
||||
// checks after every step that the code is in a state the model allows.
|
||||
//
|
||||
// bun tests/tla/sdk/drive-steer.mjs [ideal|faults] [--walks N] [--seed S]
|
||||
// bun tests/tla/drivers/drive-steer.mjs [ideal|faults] [--walks N] [--seed S]
|
||||
// [--backend native|wasm] [--durability local|world] [--verbose]
|
||||
//
|
||||
// `./check.sh` model-checks the spec and writes graphs/steer-<graph>.dot. The
|
||||
// `tests/tla/sdk/check.sh` model-checks the spec and writes its
|
||||
// graphs/steer-<graph>.dot. The
|
||||
// ideal graph has no faults; the faults graph adds cancels, deadline handoffs
|
||||
// and client retries.
|
||||
//
|
||||
@@ -352,7 +353,7 @@ const random = () => {
|
||||
return seed / 2147483648;
|
||||
};
|
||||
|
||||
const graph = await loadGraph(resolve(here, "graphs", `steer-${graphName}.dot`));
|
||||
const graph = await loadGraph(resolve(here, "../sdk/graphs", `steer-${graphName}.dot`));
|
||||
const covered = new Set();
|
||||
const totalEdges = [...graph.next.values()].reduce((sum, targets) => sum + targets.size, 0);
|
||||
let steps = 0;
|
||||
@@ -3,7 +3,7 @@
|
||||
// WebAssembly, along paths of the TLC state graph of DurableSession.tla, and
|
||||
// checks after every step that the code is in a state the model allows.
|
||||
//
|
||||
// bun tests/tla/sdk/drive.mjs [send|lookup|write|cutoff|leased|queue] [--walks N] [--seed S] [--backend native|wasm]
|
||||
// bun tests/tla/drivers/drive.mjs [send|lookup|write|cutoff|leased|queue] [--walks N] [--seed S] [--backend native|wasm]
|
||||
// [--durability local|world|vercel]
|
||||
//
|
||||
// The lookup and cutoff graphs run a lookup, which starts before its intent
|
||||
@@ -32,7 +32,8 @@
|
||||
// session in Vercel's World (see sdk/tests/vercel-storage.mjs for what it
|
||||
// needs) instead of files.
|
||||
//
|
||||
// `./check.sh` model-checks the spec and writes graphs/<graph>.dot; the cutoff
|
||||
// `tests/tla/sdk/check.sh` model-checks the spec and writes its
|
||||
// graphs/<graph>.dot; the cutoff
|
||||
// graph runs lookup with more claims and no freezes, so a step can be cut off
|
||||
// at the deadline until the bound stops running it. Each walk
|
||||
// starts two agents, A and B, on one local() World directory. Every model
|
||||
@@ -493,7 +494,7 @@ const random = () => {
|
||||
return seed / 2147483648;
|
||||
};
|
||||
|
||||
const graph = await loadGraph(resolve(here, "graphs", `${graphName}.dot`));
|
||||
const graph = await loadGraph(resolve(here, "../sdk/graphs", `${graphName}.dot`));
|
||||
const covered = new Set();
|
||||
const totalEdges = [...graph.next.values()].reduce((sum, targets) => sum + targets.size, 0);
|
||||
let steps = 0;
|
||||
@@ -1,4 +1,4 @@
|
||||
// The state graphs check.sh has TLC write, as the model drivers read them.
|
||||
// The state graphs tests/tla/sdk/check.sh has TLC write, as the drivers read them.
|
||||
import { strict as assert } from "node:assert";
|
||||
import { readFile } from "node:fs/promises";
|
||||
|
||||
@@ -66,7 +66,7 @@
|
||||
(* *)
|
||||
(* `act` names each step and its worker, so a driver can replay any path *)
|
||||
(* of the state graph against the real code and compare every state: *)
|
||||
(* tests/tla/sdk/drive.mjs. *)
|
||||
(* tests/tla/drivers/drive.mjs. *)
|
||||
(***************************************************************************)
|
||||
EXTENDS Naturals, Sequences
|
||||
|
||||
|
||||
@@ -31,7 +31,7 @@
|
||||
(* Each rule has a constant. Setting one to FALSE gives the behavior libfx *)
|
||||
(* had before this model, and each witness config shows the property that *)
|
||||
(* rule protects then fails. `act` names each step so that *)
|
||||
(* tests/tla/sdk/drive-steer.mjs can drive the real code along any path *)
|
||||
(* tests/tla/drivers/drive-steer.mjs can drive the real code along any path*)
|
||||
(* of the state graph and compare every state. *)
|
||||
(***************************************************************************)
|
||||
EXTENDS Naturals, Sequences, FiniteSets
|
||||
|
||||
+10
-8
@@ -1,6 +1,7 @@
|
||||
#!/bin/sh
|
||||
# Model-checks DurableSession.tla with TLC, confirms each witness is
|
||||
# violated, and writes the state graphs drive.mjs walks against the code.
|
||||
# violated, and writes the state graphs ../drivers/drive.mjs walks against
|
||||
# the code.
|
||||
#
|
||||
# Needs Java 11+ and tla2tools.jar:
|
||||
# brew install openjdk
|
||||
@@ -8,12 +9,13 @@
|
||||
# curl -fL -o ~/.local/share/tla/tla2tools.jar \
|
||||
# https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
|
||||
#
|
||||
# Then drive the code along the graphs:
|
||||
# bun drive.mjs send && bun drive.mjs lookup && bun drive.mjs write && bun drive.mjs cutoff
|
||||
# bun drive.mjs leased # the Heartbeat graph, on a World without liveness
|
||||
# bun drive.mjs queue # the QueueHeld graph, on a World whose queue shows it
|
||||
# bun drive-agents.mjs send && bun drive-agents.mjs consume # AgentRouting
|
||||
# bun drive-steer.mjs ideal && bun drive-steer.mjs faults
|
||||
# Then drive the code along the graphs with the drivers in ../drivers/:
|
||||
# bun ../drivers/drive.mjs send && bun ../drivers/drive.mjs lookup
|
||||
# bun ../drivers/drive.mjs write && bun ../drivers/drive.mjs cutoff
|
||||
# bun ../drivers/drive.mjs leased # the Heartbeat graph, on a World without liveness
|
||||
# bun ../drivers/drive.mjs queue # the QueueHeld graph, on a World whose queue shows it
|
||||
# bun ../drivers/drive-agents.mjs send && bun ../drivers/drive-agents.mjs consume # AgentRouting
|
||||
# bun ../drivers/drive-steer.mjs ideal && bun ../drivers/drive-steer.mjs faults # DurableSteer
|
||||
set -eu
|
||||
cd "$(dirname "$0")"
|
||||
|
||||
@@ -93,7 +95,7 @@ for pair in NoInterrupt:NoSteerWaitsOnReply NoHandBack:NothingLost \
|
||||
done
|
||||
|
||||
# AgentRouting.tla: which agent runs a session's turns when an app has
|
||||
# several. Its graphs are what drive-agents.mjs walks: inputs stored when
|
||||
# several. Its graphs are what ../drivers/drive-agents.mjs walks: inputs stored when
|
||||
# sent (memory, local) and when delivered (Vercel), with process p2 lacking
|
||||
# one agent. Drains is checked under fairness, a simulation runs a larger
|
||||
# config, and each witness breaks RunsOnOwner: NoNames is routing without
|
||||
|
||||
Reference in new issue
Block a user