v0.13.2
Finite-trace verdict semantics (RFC-049) — Direction 4 of the RFC-047 research agenda — plus the documentation and site restructure around the six bug classes.
Changed
- Timeout is always INCONCLUSIVE, never PASS. A
test()that ends by hitting itstimeoutnow finalizes INCONCLUSIVE even if everyeventually()it declared was satisfied before the deadline. The body did not reach a declared completion (natural return orterminate_when=), so the run is a truncated prefix and a green verdict would over-claim. Long-running /reuse=Truespecs that want a definite PASS must declareterminate_when=. Legacy synchronousdef test_*()functions are unaffected. - Unbounded
always(p)under timeout is INCONCLUSIVE. A never-violated unbounded safety property (nobetween=) finalizes INCONCLUSIVE on timeout (LTL₃ prefix); at natural completion orterminate_when=it stays a definitive PASS (LTL_f). Boundedalways(p, between=(a,b))is unchanged.
Added
vacuous_propertywarning event. When analways(p, between=)start anchor never fires, the window never opens and the predicate is never evaluated. The verdict stays PASS (the window may be legitimately untriggered), but the runtime now emits avacuous_propertyevent so a typo'd or misnamed anchor surfaces instead of hiding as a silent green.
Docs
- Tutorial Part 1 reframed to the bug-class + boundary story; new Seeding Data & Initial State guide; new checkout Kafka outage use case; fault-level guidance in choosing-fault-levels.
- RFC-048 (causal-guided exploration) and RFC-050 (gray/metastable faults) added as drafts; RFC-049 marked Accepted.
Verification: full host suite + go test ./testops/... -race + go vet green; Lima sweep 21/21 PASS across the 6 integration spec suites (binary, container+proxy, mocks, Kafka fd-passing, MySQL). See CHANGELOG.md.
What's Changed
- RFC-049: finite-trace verdict semantics (D4) — LTL₃/LTL_f by @avatar29A in #133
- docs: bug-class positioning - tutorial reading order, guides, showcase spec by @avatar29A in #135
Full Changelog: release-0.13.1...release-0.13.2