feat(wctt): per-stream WCTT analysis pass (Track D commit 4/6)#168
Merged
feat(wctt): per-stream WCTT analysis pass (Track D commit 4/6)#168
Conversation
Wires together NetworkGraph extraction (commit 2) and NC primitives (commit 3) into a new spar-analysis::WcttAnalysis pass that walks extracted streams and composes per-hop delay bounds end-to-end. Phase 1 covers FIFO + Priority switches with classical residual-service splitting. TSN-shaped service curves (TAS/CBS/preemption) are deferred to Phase 2 as documented in the research doc. New diagnostics: WcttBound (Info per stream), WcttExceedsBudget (Error when Spar_Network::WCTT_Budget is set and exceeded), WcttUnservable (Error when competing flows exhaust server rate), WcttSwitchOverloaded (Error when port utilization > 1). New property: Spar_Network::WCTT_Budget (Time). Total predeclared property count 120 -> 121. Non-regression: models without Spar_Network::Switch_Type produce zero Wctt* diagnostics (no_switched_buses_emits_no_diagnostics test). New requirement: REQ-NETWORK-006. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Track D commit 4/6 (of 6 for v0.8.0): wires together the network graph extraction (commit 2) and NC primitives (commit 3) into a new
spar-analysis::WcttAnalysispass that walks extracted streams and composes per-hop delay bounds end-to-end.spar-network::curves. Streams are inferred from AADL data-port connections that bind to one or more switched buses viaDeployment_Properties::Actual_Connection_Binding. Per-stream end-to-end WCTT = sum of per-hop delays.Spar_TSNproperty set.latency.rsintegration is the closeout commit 6. Lean theorems are commit 5.Spar_Network::WCTT_Budget(Time). Predeclared-property total goes 120 -> 121 (Spar_Network grew by 1).What's new
crates/spar-analysis/src/wctt.rs— new pass with 10 unit tests covering: non-regression (zeroWctt*on unswitched models), single-hop / multi-hop chain bounds, two-stream residual-service split, competing-flow exhaustion, budget exceed/within, Priority switch (treated like FIFO in Phase 1), TSN switch deferral, unannotated bus skip.crates/spar-analysis/tests/fixtures/wctt/classical_ethernet.aadl+.expected.jsonsnapshot, driven bytests/wctt_fixtures.rs.WcttBound(Info per stream),WcttExceedsBudget(Error),WcttUnservable(Error),WcttSwitchOverloaded(Error),WcttDeferred(Info Phase-2 note).WCTT_Budget => Time); per-set test bumped 4 -> 5; total-count test bumped to 121 reconciled with the v0.7.1 PIP/PCP additions already on main.register_allcount bumped 29 -> 30.requirements.yaml; TEST-WCTT linked to REQ-NETWORK-{004,005,006} appended toverification.yaml.Test plan
cargo build --workspacecleancargo test -p spar-analysis— 824 lib + 3 rta_fixtures + 1 wctt_fixtures passcargo test -p spar-network— 26 lib + 6 integration passcargo test -p spar-hir-def— 448 lib pass (including the bumped property-count assertion)cargo clippy --workspace --all-targets -- -D warningscleancargo fmt --all -- --checkcleanrivet validatePASSOut of scope
latency.rsintegration with WctttCache (commit 6)Track Asurfaces🤖 Generated with Claude Code