diff --git a/docs/development/ci.md b/docs/development/ci.md index 698c57b..533496b 100644 --- a/docs/development/ci.md +++ b/docs/development/ci.md @@ -49,7 +49,13 @@ before it decides: | a violation of any other property (`newAccountBalanceIsZero` fires on one android seed) | red: a real finding, but not the one this leg gates on | | no violation and exit 0 | red: the fuzzer stopped finding a bug that is still there | | no trace at all, on exit 0 or 2 | red: the run recorded nothing, so there is no verdict to read | -| exit 1, or any other code | red: the harness broke, and the code propagates | +| exit 1, or any other code | red: the run produced no verdict, and the code propagates | + +Exit 1 is two things now, and both fail the leg. The harness broke, or the run +finished cleanly holding no verdict to report: no properties, no step that +reached the verifier, or an action generator that never drove the app and found +nothing. The second kind leaves a full run directory and names itself on stderr, +so the log says which happened. The first two rows are why the check is worth the code it takes. A `TypeError` in `predicates.ts` and a fuzzer that no longer reaches the bug both used to diff --git a/docs/manual/cli.md b/docs/manual/cli.md index e6b46c1..ac07774 100644 --- a/docs/manual/cli.md +++ b/docs/manual/cli.md @@ -25,7 +25,8 @@ Run a spec against an app for a fixed duration. | `--duration` | `5m` | Total test duration (`30s`, `5m`, `2h`, `1d`). | | `--max-steps` | `0` | Stop after this many steps (`0` = no cap, the duration governs). A step budget is what makes two generators comparable. | | `--exit-on-violation` | `false` | Stop the run at the first property violation and exit `2`. | -| `--allow-no-properties` | `false` | Run a spec that registers no properties. Such a run judges nothing and can only report no violations, so it is refused by default; pass this when the run measures what the spec extracts or where the generator reaches. | +| `--allow-no-properties` | `false` | Run a spec that registers no properties. Such a run judges nothing and can only report no violations, so it is refused by default; pass this when the run measures what the spec extracts. | +| `--allow-no-generator-actions` | `false` | Finish a run the action generator never drove. Such a run judged whatever screen the spec's setup left it on and explored nothing, so it is refused by default; pass this when the run measures where the generator reaches and reaching nothing is the measurement. A run that recorded a violation is never refused, flag or no flag. | | `--arm` | optional | Experiment label recorded in the run's metadata. Used by the campaign tool to tell one sweep cell from another. | | `--seed` | `0` | PRNG seed. `0` uses a random seed and records it in `meta.json`. | | `--generator` | `seeded` | Who picks each action: `seeded` (the run's PRNG) or `llm` (a vision model). See [the LLM generator](../spec-language/#llm-generator). | @@ -35,6 +36,8 @@ Run a spec against an app for a fixed duration. Exit codes: `0` the run finished (violations, if any, are in the summary), `2` the run stopped on a violation under `--exit-on-violation`, `1` something went wrong. CI reads the difference between `2` and `1` to tell a found bug from a broken harness. +`1` also covers a run that finished cleanly and holds no verdict, which is not a broken harness but is not evidence either: a spec that registers no properties, a run no step of which reached the verifier, and a run whose action generator never drove the app and found nothing. Each names itself on stderr and leaves its full run directory behind, and each has a flag that says "this is the measurement" when it is. + ## `sanderling replay [run-or-runs-dir]` Serve a local web UI for browsing traces. The positional argument is optional and may point at either a runs directory (the parent of many runs) or a single run directory (auto-detected by the presence of `meta.json`). Defaults to `./runs`.