diff --git a/CHANGELOG.md b/CHANGELOG.md index 0c41459..42ad777 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,66 @@ All notable changes to this workspace are documented here. The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and this project adheres to [Semantic Versioning](https://semver.org/). +## 0.5.0 — 2026-04-28 + +### `default(...)` is a real LCA-aware transition + +`default(...)` is now modeled the same way as any event-driven +transition. It fires immediately after the declaring state's entries +finish and its durings start, applying the standard exit-to-LCA / +enter-to-target algorithm. Three behavioral changes follow from this: + +- **Optional.** A state with children no longer must declare a + `default(...)`. When omitted, the state itself is the resting + innermost active state; substates are reachable only via explicit + transitions. This is the "microwave Standby" pattern — `Standby` + has substates like `LowPower` you enter only on demand, and + `=> Standby;` lands at `Standby` itself with no descent. +- **Targets anywhere.** The default target may be any state in the + chart — a child (the classic descent case), a sibling, an ancestor, + anywhere. `default()` exits the just-entered + state as part of the default-fire transition; the same uniform + rule covers descent, redirection, and up-bounce. +- **Cycle-checked at compile time.** The default-edge graph + (out-degree ≤ 1 per node) is rejected if it contains any cycle, + including `default(self)`. The check guarantees default chains + terminate at runtime — entering any state in a cycle would loop + forever before reaching user code. + +### Breaking changes + +- **Journal format.** Default-fires now emit `TransitionFired` (with + `reason: TransitionReason::Internal`) and `TransitionComplete` + brackets around their entry sequence. `Internal` was previously + reserved and never emitted; it is now active. Charts that + hand-build expected journal sequences (replay-style tests) must + include these brackets around every default-fire — see the + per-test diffs in this release for the pattern. +- **Validation.** Two compile-time errors went away: + `default()` is now valid (the target may be + anywhere), and `default` on a childless state is now valid + (the leaf transitions out immediately on entry). Code relying + on these as guard rails must adapt. A new compile-time error + takes their place: any cycle in the default graph is rejected + with a pinpoint message naming the cycle (e.g. + `default-transition cycle detected: A -> B -> A`). + +### Other + +- README and `docs/002. hsmc-semantics-formal.md` rewritten so the + default-as-transition framing is the primary description; the old + "automatic transition into a child" language is gone. +- New integration tests covering each branch of the new semantics: + `det_optional_default` (microwave pattern), `det_default_sibling` + (lateral default), `det_default_chained` (multi-link default + chain), `det_default_ancestor` (up-default landing on an + ancestor). +- New compile-fail UI fixtures for cycle detection + (`t9_4_default_self_cycle`, `t9_5_default_two_cycle`) and new + compile-pass fixtures for non-child default targets + (`composite_without_default`, `default_targets_sibling`, + `default_targets_ancestor`). + ## 0.4.1 — 2026-04-28 ### Performance — dispatch hot path diff --git a/Cargo.lock b/Cargo.lock index b6f8ce6..a6644d6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -495,7 +495,7 @@ checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "hsmc" -version = "0.4.1" +version = "0.5.0" dependencies = [ "crossterm", "defmt 0.3.100", @@ -515,7 +515,7 @@ dependencies = [ [[package]] name = "hsmc-macros" -version = "0.4.1" +version = "0.5.0" dependencies = [ "hsmc", "proc-macro2", @@ -526,7 +526,7 @@ dependencies = [ [[package]] name = "hsmc-verification" -version = "0.4.1" +version = "0.5.0" dependencies = [ "creusot-std", "hsmc", diff --git a/Cargo.toml b/Cargo.toml index e4b89ee..954fb85 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ resolver = "2" members = ["hsmc", "hsmc-macros", "verification"] [workspace.package] -version = "0.4.1" +version = "0.5.0" edition = "2021" license = "MIT OR Apache-2.0" authors = ["Stephen Waits "] diff --git a/README.md b/README.md index 44cf7c5..738e14b 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,9 @@ statechart! { ## What it does - **Harel-style hierarchical states.** Nested states with `entry:`/`exit:` - actions, LCA-aware transitions, default-child descent, `terminate`. + actions, LCA-aware transitions, optional `default(...)` (a transition + that may target any state — descend, redirect to a sibling, bounce + to an ancestor — with a compile-time cycle check), `terminate`. - **Event-driven transitions and actions.** Typed payload bindings: `on(PacketRx { rssi: i16 }) => handler;`. - **Timer triggers.** `on(after Duration::from_secs(5)) => Next;` and @@ -50,12 +52,9 @@ statechart! { records every action, transition, timer, and event in order — same inputs, byte-identical journal. The runtime queue and timer table carry Pearlite specs that Creusot + Why3 + alt-ergo + z3 discharge - mechanically (`just verify`). 159 tests pin every spec rule - (journal sequences + trace-format regression + integration). -- **Backward-compatible chart syntax.** Every v0.1 / v0.2 / v0.3 - statechart compiles under v0.4 unchanged. The 0.4 breaks are in - observability surface area only — see - [Migration](#migration-from-v03). + mechanically (`just verify`). The integration suite pins every + spec rule with byte-equal expected-vs-actual journals, trace-format + regression checks, and per-feature behavior tests. ## How a chart behaves — the building blocks @@ -165,8 +164,9 @@ Direction is set by the path: path, the outermost state's entries fire first, then the next, then the innermost's. Within a single state, entry actions fire in declaration order. After a state's entries finish, its `during:` - activities start. Then default-descent (rule 2) applies recursively - if a `default` is declared. + activities start. Then, if the state declared a `default(...)`, + it fires as a transition (rule 2) — chains continue until a state + with no default. - **Exits** fire **inner-to-outer**: innermost first, then parent, then grandparent. Within a single state, exit actions fire in declaration order. Before a state's exits begin, its `during:` activities are @@ -228,7 +228,7 @@ Add to `Cargo.toml`: ```toml [dependencies] -hsmc = { version = "0.4", features = ["embassy"] } # or ["tokio"] +hsmc = { version = "0.5", features = ["embassy"] } # or ["tokio"] ``` Minimal timer-only machine: @@ -385,7 +385,7 @@ For `statechart! Foo { ... }` the macro emits: | `fn step(elapsed) -> Option` | One unit of work (test/polling driver). | | `fn send(ev)` | Raw push, non-draining. For tests. | | `sender() -> Sender` | Clone handle for other tasks / ISRs. | -| `current_state()` | The active leaf state. | +| `current_state()` | The innermost active state. | | `is_terminated()` | True after `terminate` event. | | `has_pending_events()` | Queue non-empty. | | `context()` / `context_mut()` | Borrow the root context. | @@ -403,135 +403,6 @@ For `statechart! Foo { ... }` the macro emits: `embassy` and `tokio` are mutually exclusive — enabling both is a compile error. -## Migration from v0.3 - -The 0.4 breaks are in the observability surface area only; chart -syntax and runtime API are unchanged. - -### 1. Trace prefix changed - -Trace lines (when `trace-defmt` / `trace-log` / `trace-tracing` is -enabled) now use `[statechart:Name]` instead of `[Name]`. Update any -log filters or grep patterns. The verb after the prefix is now a -single hyphenated token followed by `key=value` pairs (logfmt). - -### 2. `TraceEvent::TransitionFired` carries `reason` - -Add `reason` to any pattern matches: - -```rust -// before: -TraceEvent::TransitionFired { from, to } => … -// after: -TraceEvent::TransitionFired { from, to, reason } => … -// or, if you don't need it: -TraceEvent::TransitionFired { from, to, .. } => … -``` - -The new field carries `TransitionReason::Event { event }`, -`Timer { state, timer }`, or `Internal` so consumers can see what -triggered the transition. - -### 3. New `TraceEvent` variants - -If you `match` exhaustively on `TraceEvent`, add arms for the new -variants. Otherwise nothing changes: - -- `EnterBegan { state }` — phase begin marker pairs with `Entered`. -- `ExitBegan { state }` — phase begin marker pairs with `Exited`. -- `TransitionComplete { from, to }` — pairs with `TransitionFired`. -- `EventReceived { event }` — fires when an event is popped from the - queue, before handler search. - -These are pure observation — no runtime semantic change. - -### 4. `trace;` keyword is a no-op - -Charts that declared `trace;` continue to compile. The keyword no -longer gates emission — observation is now controlled purely by -which `trace-*` cargo feature you enable. You can leave `trace;` in -or remove it; both work. - -### 5. Trace backends are no longer mutually exclusive - -Previously, enabling more than one of `trace-defmt` / `trace-log` / -`trace-tracing` was a compile error. Now they fan out independently: -turn on whichever you want. - -## Migration from v0.1 - -v0.1 statecharts continue to compile. New features are purely additive: - -### 1. `events:` is now optional - -Previously required; now omit for pure timer-only machines: - -```rust -statechart! { - Blinker { - context: Ctx; - default(On); - state On { on(after Duration::from_millis(500)) => Off; } - state Off { on(after Duration::from_millis(500)) => On; } - } -} -``` - -### 2. `dispatch(ev).await` replaces the push+drain helper - -Before (v0.1, in the dogfood firmware): - -```rust -async fn push(m: &mut M, ev: E) { - m.send(ev).expect("queue full"); - while m.has_pending_events() { - m.step(Duration::ZERO).await; - } -} -push(&mut machine, ev).await; -``` - -After (v0.2): - -```rust -machine.dispatch(ev).await.unwrap(); -``` - -### 3. `during:` replaces the imperative I/O outer loop - -Before — a radio task with per-state match and select: - -```rust -loop { - match machine.current_state() { - RadioState::Receiving => { - match select(rx_once(&mut lora, &cfg, &mut rx_buf), - commands.receive()).await { - Either::First(r) => handle_rx(r, &mut machine, ...).await, - Either::Second(c) => handle_cmd(c, &mut machine, ...).await, - } - } - _ => { ... } - } -} -``` - -After — the statechart owns the loop: - -```rust -state Receiving { - during: next_packet(lora, rx_buf); - on(PacketRx { rssi: i16, snr: i16 }) => record_packet; - on(StopRx) => Idle; -} - -#[embassy_executor::task] -async fn radio_task(lora: LoRaDriver, ch: &'static RadioChan) { - let mut m = Radio::new(RadioCtx { lora, ... }, ch); - m.run().await.unwrap(); -} -``` - ## Examples | Example | Purpose | @@ -563,13 +434,14 @@ spec-rule → proof mapping. Beyond Creusot, the suite includes: -- **159 integration tests** — full chart behavior, byte-equal expected- - vs-actual journals for ~113 deterministic-flow tests, plus 11 trace- - format regression tests pinning every observation verb's exact - textual rendering. -- **0 missed mutants** under `cargo mutants --features +- **Integration tests** — full chart behavior and per-feature + determinism, with byte-equal expected-vs-actual journals on the + `det_*` deterministic-flow tests, plus trace-format regression + tests pinning every observation verb's textual rendering. Run + with `cargo test --workspace --features tokio,journal`. +- **`cargo mutants`** — full coverage under `cargo mutants --features tokio,journal,trace-log`. -- **Miri**: 68 tests, no UB. +- **Miri** — clean, no UB on the runtime crates. ## Observability — one journal, multiple outputs @@ -639,25 +511,16 @@ diffed against expected behavior the same way the journal can. ## Status -- v0.1 spec: fully implemented. -- v0.2: `during:`, optional `events:`, `dispatch()`, `STATE_CHART`, - drain-on-send. Up-transitions no longer exit/re-enter the target. -- v0.3: `journal` feature + deterministic trace + replay; root - state targetable by chart name; Creusot verification of the - runtime data structures; 113-test deterministic-flow suite. -- v0.4: unified observation pipeline (journal + trace share one - vocabulary, fan out to multiple sinks at compile time); logfmt- - style trace format with `[statechart:Name]` prefix; transition - reasons; entry/exit/transition begin/end markers; multiple trace - backends now compose; chart-level `trace;` keyword deprecated. - Breaking on the `TraceEvent` enum shape; chart syntax unchanged. -- Out of scope (deliberate): guard conditions, orthogonal/parallel - regions, history states, deferred events, internal transitions, - state-local context, event priorities beyond FIFO, runtime - statechart modification, multi-threaded tokio. See - [`docs/002. hsmc-semantics-formal.md`](docs/002.%20hsmc-semantics-formal.md) - § "What `hsmc` deliberately does NOT have" for the rationale and - what to use instead. +Pre-1.0. Per-release breaking changes are documented in +[`CHANGELOG.md`](CHANGELOG.md). + +Out of scope (deliberate): guard conditions, orthogonal/parallel +regions, history states, deferred events, internal transitions, +state-local context, event priorities beyond FIFO, runtime +statechart modification, multi-threaded tokio. See +[`docs/002. hsmc-semantics-formal.md`](docs/002.%20hsmc-semantics-formal.md) +§ "What `hsmc` deliberately does NOT have" for the rationale and +what to use instead. ## License diff --git a/docs/002. hsmc-semantics-formal.md b/docs/002. hsmc-semantics-formal.md index 891ccdc..577957e 100644 --- a/docs/002. hsmc-semantics-formal.md +++ b/docs/002. hsmc-semantics-formal.md @@ -93,8 +93,9 @@ and still nothing handles it, the event is silently discarded. That's all. Three other things follow from this rule: -- A handler on a leaf state shadows a handler on its ancestor for the same - event. The leaf wins because the search starts there. +- A handler on the innermost active state shadows a handler on any + ancestor for the same event. The innermost wins because the search + starts there. - If a single state has multiple handlers (actions and/or a transition) for the same trigger, the actions fire in declaration order, then the transition fires last. @@ -115,8 +116,8 @@ in `statechart! { Foo { ... } }`, an `on(Trig) => Foo;` is a valid transition whose target is the root. From any state inside the chart this is an up-transition (root is always on the active path) — exiting only the states strictly between current and root, with no entry actions and -no default-descent on root. Use this when you want to wind everything -back up to the chart's own scope. +no default firing on root (the root wasn't freshly entered). Use this +when you want to wind everything back up to the chart's own scope. To run a transition: @@ -140,8 +141,9 @@ in which steps fire. ### Transitioning to a sibling (or anywhere not on your active path) The standard case. LCA is somewhere strictly above both current and -target. Exit up to LCA, enter down to target, default-descend from the -target if it declares a `default`. Already covered above. +target. Exit up to LCA, enter down to target, then if the target +declares a `default(...)`, fire it as a chained transition. Already +covered above. ### Transitioning to yourself diff --git a/hsmc/Cargo.toml b/hsmc/Cargo.toml index f74415f..7821fa4 100644 --- a/hsmc/Cargo.toml +++ b/hsmc/Cargo.toml @@ -40,7 +40,7 @@ trace-tracing = ["dep:tracing"] journal = [] [dependencies] -hsmc-macros = { path = "../hsmc-macros", version = "0.4.1" } +hsmc-macros = { path = "../hsmc-macros", version = "0.5.0" } heapless = "0.8" tokio = { version = "1", features = ["sync", "time", "rt", "macros"], optional = true } embassy-sync = { version = "0.8", optional = true }