From 0b7cb96d23b4d6044251c6b8a883d7c740fb2a55 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 12:33:29 +0200 Subject: [PATCH] fix(analysis): report unmeasurable bus demand instead of silence (REQ-NC-BUS-PAYLOAD-001) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `compute_connection_demand` returned `0.0` for three distinct *unmeasurable* cases — unresolved source subcomponent, no findable `Data_Size`, no findable `Period` — and the caller then dropped every `demand == 0.0` connection. A bus on which nothing resolved left `bound_connections` empty, hit the `continue`, and emitted no diagnostic at all: a saturated bus passed clean. Where only some connections resolved, the utilization silently omitted the rest and was still printed as a bare percentage — a lower bound presented as a verdict. The load-bearing change is at the type level, not in the message text: enum ConnectionDemand { Known(f64), Unknown(Unaccounted) } enum Unaccounted { UnresolvedSource, PayloadSize, SourcePeriod } `compute_connection_demand` no longer returns `f64`, so a caller cannot conflate the two by testing `demand > 0.0` — the old `return 0.0` was a lie the compiler could not see. Any bus with >=1 unaccounted bound connection now emits a Warning naming the count, the total and the grouped reasons — including when nothing resolved — and every utilization verdict computed over an incomplete set carries an explicit `LOWER BOUND: N connections unaccounted` suffix. Reasons render in a fixed order, eliding past `MAX_NAMED_CONNECTIONS = 3`, so diagnostics are stable across runs. No computed bandwidth number changes. Where the input is complete the existing tests are untouched and still pass; that is the evidence for the SCOPE clause. The dominant unmeasurable case has a known root cause, recorded as the successor REQ-NC-BUS-PAYLOAD-002 (v0.37.0): payload size is read only from the source component's own `Data_Size`, never from the port's `data` classifier — the AADL-native place for it, and the one spar's own WIT codegen already follows via `resolve_data_shape`. A model that types its ports properly has no findable `Data_Size` here at all. The blocker is plumbing, not semantics: the analysis path gets a `SystemInstance` without the resolver scope needed to follow a classifier reference. This change makes the gap visible first, because the honesty fix is sound on its own and must not wait on the capability. Oracle: `missing_data_size_no_demand` previously asserted *silence* ("No demand computed, so no diagnostics for this bus.") — the bug was encoded in the oracle itself, which is why it survived. It now asserts exactly one Warning containing the reason and the connection name and, as the falsification edge, that the message does not contain `utilization:` — no verdict may be reported when nothing was measured. New `partial_demand_is_labelled_a_lower_bound` covers the mixed case that previously produced a clean sub-80% Info. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/requirements.yaml | 84 +++++++ artifacts/verification.yaml | 44 ++++ crates/spar-analysis/src/bus_bandwidth.rs | 292 ++++++++++++++++++++-- 3 files changed, 399 insertions(+), 21 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 5590d47..6237bcc 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -4239,6 +4239,90 @@ artifacts: fields: release: v0.23.0 + - id: REQ-NC-BUS-PAYLOAD-001 + type: requirement + title: "Bus bandwidth shall report what it could not measure, not score it as zero" + description: > + The bus bandwidth analysis (`spar-analysis::bus_bandwidth`) shall + distinguish a connection that uses NO bandwidth from a connection whose + bandwidth it COULD NOT DETERMINE, and shall never present a utilization + figure computed over an incomplete connection set as a verdict. + + DEFECT: `compute_connection_demand` returned `0.0` for three distinct + unmeasurable cases — unresolved source subcomponent, no findable + `Data_Size`, no findable `Period` — and the caller then dropped every + `demand == 0.0` connection from `bound_connections`. A bus on which NO + connection's demand could be computed therefore left `bound_connections` + empty, hit the `continue`, and emitted NO DIAGNOSTIC AT ALL. A saturated + bus passed clean. Where some connections did resolve, the reported + utilization silently omitted the rest and was still printed as a bare + percentage. + + This is the same failure direction as REQ-TSN-SVC-MULTIWIN-001 and + REQ-CODEGEN-LAYOUT-CERT-001: an analysis that is OPTIMISTIC when its + input is incomplete. Silence is the worst possible rendering of "I do not + know", because it is indistinguishable from "I checked and it is fine". + + ROOT CAUSE of the dominant case: payload size is read only from the + SOURCE COMPONENT's own `Data_Size` property. The port's `data` classifier + — the AADL-native place to put payload size, and the one spar's OWN WIT + codegen relies on via `resolve_data_shape` — is never consulted. A model + that types its ports properly has no findable `Data_Size` here at all. + Closing that gap is the successor REQ-NC-BUS-PAYLOAD-002; this + requirement makes the analysis HONEST about the gap first, because the + honesty fix is sound on its own and must not wait on the capability. + + SHALL: (a) the demand of a single connection is `Known(bps)` or + `Unknown(reason)` — a type distinction, not a sentinel value, so the two + cannot be conflated by a caller; (b) any bus with at least one + unaccounted bound connection emits a `Warning` naming the count, the + total, and the reasons grouped, EVEN WHEN no connection resolved and the + analysis would otherwise say nothing; (c) every utilization verdict + (Error / Warning / Info) computed over an incomplete set carries an + explicit "LOWER BOUND: N connections unaccounted" suffix. + + SCOPE: reporting honesty only. This requirement does NOT make any + currently-unmeasurable connection measurable, and deliberately does not + change a single computed bandwidth number. Where the input is complete + the output is byte-identical to before. + status: implemented + release: v0.35.0 + tags: [network-calculus, bus, honesty, analysis, diagnostics, v0350] + links: + - type: traces-to + target: REQ-NC-BRIDGE-001 + + - id: REQ-NC-BUS-PAYLOAD-002 + type: requirement + title: "Resolve bus payload size from the port's data classifier" + description: > + Successor to REQ-NC-BUS-PAYLOAD-001, which made the gap visible. The bus + bandwidth analysis shall determine payload size from the connection's + SOURCE PORT `data` classifier — resolving the classifier and reading its + `Data_Size` — falling back to the source component's own `Data_Size` + only when the port is untyped. + + This is the AADL-native placement and the one spar already depends on + elsewhere: `spar_hir_def::resolver::GlobalScope::resolve_data_shape` + performs exactly this resolution today, but is consumed ONLY by codegen. + The blocker is plumbing, not semantics — the analysis path receives a + `SystemInstance` without the resolver scope needed to follow a classifier + reference, so wiring that through is the actual work. + + GATE (executed, not prose): a fixture whose ports are typed with a `data` + classifier carrying `Data_Size`, and whose source components carry NO + `Data_Size` of their own, shall produce a complete utilization figure + with ZERO unaccounted connections — i.e. the REQ-NC-BUS-PAYLOAD-001 + warning must be ABSENT on a model where it currently fires for every + connection. That absence, on a fixture that is red today, is the + acceptance criterion. + status: proposed + release: v0.37.0 + tags: [network-calculus, bus, analysis, resolver, codegen] + links: + - type: traces-to + target: REQ-NC-BUS-PAYLOAD-001 + - id: REQ-TSN-SYNTH-MILP-001 type: requirement title: "TSN schedule synthesis — MIP→VNS-GA scale handoff" diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 2d4ca83..efac4fc 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -4091,3 +4091,47 @@ artifacts: links: - type: satisfies target: REQ-INGEST-DBC-FLOWS-001 + + - id: TEST-NC-BUS-PAYLOAD + type: feature + title: Bus bandwidth reports unmeasurable connections instead of scoring them zero + description: > + Verifies REQ-NC-BUS-PAYLOAD-001 through two spar-analysis unit tests that + are red against the previous implementation. + + (1) `missing_data_size_no_demand` — a bus whose ONLY bound connection has + no findable `Data_Size`. This test previously asserted SILENCE ("no + demand computed, so no diagnostics for this bus"); the bug was encoded in + the oracle itself, which is why it survived. It now asserts exactly one + `Warning`, that the message contains "INCOMPLETE", the reason + "undeterminable payload size" and the connection name `c1`, and — the + falsification edge — that the message does NOT contain "utilization:", + so no verdict may be reported when nothing was measured. + + (2) `partial_demand_is_labelled_a_lower_bound` — two bound connections, + one fully specified (1 KByte / 1 sec = 8192 bps) and one with no findable + `Data_Size`, on a 1 Mbitsps bus. The measured demand alone is a clean + sub-80% figure, so the pre-fix code emitted a bare `Info` verdict that + read as complete. It now asserts a `Warning` quantifying "1 of 2 bound + connections" and naming `c_b`, AND that the `Info` verdict carries + "LOWER BOUND: 1 connections unaccounted". + + The type change is what makes the property hold rather than the message + text: `compute_connection_demand` returns + `ConnectionDemand::{Known(f64), Unknown(Unaccounted)}` instead of `f64`, + so a caller can no longer conflate "uses no bandwidth" with "could not be + measured" by testing `demand > 0.0`. The remaining bus_bandwidth tests + are unchanged and still pass, which is the evidence for the requirement's + SCOPE clause: where the input is complete, no computed number moved. + fields: + method: automated-test + steps: + - run: cargo test -p spar-analysis --lib bus_bandwidth + status: passing + tags: [network-calculus, bus, honesty, analysis, oracle, v0350] + links: + - type: satisfies + target: REQ-NC-BUS-PAYLOAD-001 + + - type: verifies + target: REQ-NC-BUS-PAYLOAD-001 diff --git a/crates/spar-analysis/src/bus_bandwidth.rs b/crates/spar-analysis/src/bus_bandwidth.rs index 7749d22..61849d0 100644 --- a/crates/spar-analysis/src/bus_bandwidth.rs +++ b/crates/spar-analysis/src/bus_bandwidth.rs @@ -10,8 +10,8 @@ //! 1. Find connections whose owning component has `Actual_Connection_Binding` //! pointing to this bus. //! 2. For each bound connection, compute bandwidth demand: -//! - `Data_Size` of the data type being transferred (from the source port's -//! classifier or the source component's `Data_Size` property). +//! - `Data_Size` of the data type being transferred, read from the source +//! component's own `Data_Size` property (or a child thread's). //! - `Period` of the source thread (message rate = 1 / Period). //! - demand = Data_Size / Period (bits per picosecond, converted to bps). //! 3. Sum all demands on the bus. @@ -20,6 +20,23 @@ //! 5. Error if demand > capacity. //! 6. Warning if utilization > 80%. //! 7. Info with utilization summary. +//! +//! # Known limitation: payload size is not read from the port's data classifier +//! +//! Step 2 consults only the *source component's* `Data_Size`. It does NOT +//! resolve the port's `data` classifier, even though that is the AADL-native +//! place to put payload size and the one spar's own WIT codegen requires +//! ([`spar_hir_def::resolver::GlobalScope::resolve_data_shape`] is currently +//! consumed by codegen alone). A model that types its ports properly therefore +//! has no findable `Data_Size` here. +//! +//! Until that gap is closed, such connections are reported as **unaccounted** +//! rather than scored as zero demand, and every utilization figure computed +//! over an incomplete set is labelled a lower bound. Silently treating "size +//! unknown" as "uses no bandwidth" let a saturated bus pass with no diagnostic +//! at all — this analysis is now honest about what it could not measure +//! (REQ-NC-BUS-PAYLOAD-001). Deriving the size from the classifier is the +//! successor requirement; it needs the resolver scope in the analysis path. use rustc_hash::FxHashMap; @@ -110,6 +127,8 @@ impl BusBandwidthAnalysis { // Find all connections bound to this bus and compute demands. let mut total_demand_bps: f64 = 0.0; let mut bound_connections: Vec<(String, f64)> = Vec::new(); + // Bound to this bus but contributing nothing, with the reason. + let mut unaccounted: Vec<(String, Unaccounted)> = Vec::new(); // Walk all components looking for Actual_Connection_Binding referencing this bus. for (comp_idx, _comp) in instance.all_components() { @@ -159,31 +178,67 @@ impl BusBandwidthAnalysis { continue; } - let demand = compute_connection_demand(instance, src_sub_idx, &bus_map); - if demand > 0.0 { - bound_connections.push((conn.name.as_str().to_string(), demand)); - total_demand_bps += demand; + match compute_connection_demand(instance, src_sub_idx, &bus_map) { + ConnectionDemand::Known(demand) => { + bound_connections.push((conn.name.as_str().to_string(), demand)); + total_demand_bps += demand; + } + ConnectionDemand::Unknown(why) => { + unaccounted.push((conn.name.as_str().to_string(), why)); + } } } } + // A connection bound to this bus whose demand could not be computed + // is a hole in the aggregate, and the aggregate is what the verdict + // below rests on. Report it — including when it is the *only* thing + // we found, which is precisely the case that used to pass in + // silence (REQ-NC-BUS-PAYLOAD-001). + if !unaccounted.is_empty() { + diags.push(AnalysisDiagnostic { + severity: Severity::Warning, + message: format!( + "bus '{}' demand is INCOMPLETE: {} of {} bound connections contributed \ + no demand ({}); the reported utilization is a lower bound, not a verdict", + bus_comp.name, + unaccounted.len(), + unaccounted.len() + bound_connections.len(), + summarize_unaccounted(&unaccounted), + ), + path: bus_path.clone(), + analysis: self.name().to_string(), + }); + } + if bound_connections.is_empty() { continue; } let utilization = total_demand_bps / capacity_bps * 100.0; + // Appended to every verdict below so the number is never read as + // complete when it isn't. + let completeness = if unaccounted.is_empty() { + String::new() + } else { + format!( + ", LOWER BOUND: {} connections unaccounted", + unaccounted.len() + ) + }; if total_demand_bps > capacity_bps { diags.push(AnalysisDiagnostic { severity: Severity::Error, message: format!( "bus '{}' bandwidth exceeded: {:.1} bps demand vs {:.1} bps capacity \ - ({:.1}% utilization, {} bound connections)", + ({:.1}% utilization, {} bound connections{})", bus_comp.name, total_demand_bps, capacity_bps, utilization, bound_connections.len(), + completeness, ), path: bus_path.clone(), analysis: self.name().to_string(), @@ -193,12 +248,13 @@ impl BusBandwidthAnalysis { severity: Severity::Warning, message: format!( "bus '{}' bandwidth utilization is high: {:.1} bps demand vs {:.1} bps capacity \ - ({:.1}% utilization, {} bound connections)", + ({:.1}% utilization, {} bound connections{})", bus_comp.name, total_demand_bps, capacity_bps, utilization, bound_connections.len(), + completeness, ), path: bus_path.clone(), analysis: self.name().to_string(), @@ -207,12 +263,13 @@ impl BusBandwidthAnalysis { diags.push(AnalysisDiagnostic { severity: Severity::Info, message: format!( - "bus '{}' bandwidth utilization: {:.1} bps of {:.1} bps ({:.1}%, {} bound connections)", + "bus '{}' bandwidth utilization: {:.1} bps of {:.1} bps ({:.1}%, {} bound connections{})", bus_comp.name, total_demand_bps, capacity_bps, utilization, bound_connections.len(), + completeness, ), path: bus_path, analysis: self.name().to_string(), @@ -224,6 +281,51 @@ impl BusBandwidthAnalysis { } } +/// How many connection names to name explicitly before eliding the rest. +/// A bus can carry many connections; the point of the message is to make the +/// gap actionable, not to reproduce the model. +const MAX_NAMED_CONNECTIONS: usize = 3; + +/// Render the unaccounted connections grouped by reason, e.g. +/// `2 with undeterminable payload size: c1, c2; 1 with undeterminable source +/// period: c3`. Reasons appear in a fixed order so the message is stable +/// across runs (diagnostics are compared in tests and in CI output). +fn summarize_unaccounted(unaccounted: &[(String, Unaccounted)]) -> String { + let mut parts = Vec::new(); + for why in [ + Unaccounted::PayloadSize, + Unaccounted::SourcePeriod, + Unaccounted::UnresolvedSource, + ] { + let names: Vec<&str> = unaccounted + .iter() + .filter(|(_, w)| *w == why) + .map(|(n, _)| n.as_str()) + .collect(); + if names.is_empty() { + continue; + } + let shown = names + .iter() + .take(MAX_NAMED_CONNECTIONS) + .copied() + .collect::>() + .join(", "); + let elided = names.len().saturating_sub(MAX_NAMED_CONNECTIONS); + let tail = if elided > 0 { + format!(", +{elided} more") + } else { + String::new() + }; + parts.push(format!( + "{} with {}: {shown}{tail}", + names.len(), + why.reason() + )); + } + parts.join("; ") +} + /// Extract a data rate value in bps from a typed [`PropertyExpr`]. fn extract_data_rate_bps(expr: &PropertyExpr) -> Option { match expr { @@ -312,40 +414,83 @@ fn get_bandwidth_capacity(props: &spar_hir_def::properties::PropertyMap) -> Opti None } +/// Why a bus-bound connection contributed nothing to the demand sum. +/// +/// Each variant is a *gap in the input model*, not a zero-bandwidth +/// connection — the distinction the aggregate verdict depends on. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Unaccounted { + /// The connection's source subcomponent did not resolve. + UnresolvedSource, + /// No `Data_Size` was findable for the payload (REQ-NC-BUS-PAYLOAD-001): + /// notably, a port typed with a `data` classifier that carries the size + /// is NOT consulted — see [`get_data_size_for_component`]. + PayloadSize, + /// No `Period` was findable for the source, so the message rate is unknown. + SourcePeriod, +} + +impl Unaccounted { + /// Plural noun phrase used when grouping connections by reason. + fn reason(self) -> &'static str { + match self { + Unaccounted::UnresolvedSource => "unresolved source subcomponent", + Unaccounted::PayloadSize => "undeterminable payload size", + Unaccounted::SourcePeriod => "undeterminable source period", + } + } +} + +/// The bandwidth demand of a single connection, or why it could not be computed. +#[derive(Debug, Clone, Copy, PartialEq)] +enum ConnectionDemand { + /// Both payload size and message rate resolved, in bits per second. + Known(f64), + /// Bound to the bus, but its demand is unknown — it must NOT be silently + /// treated as zero, or the aggregate becomes an unsound lower bound + /// presented as a verdict. + Unknown(Unaccounted), +} + /// Compute the bandwidth demand of a single connection in bits per second. /// /// demand = Data_Size (bits) / Period (seconds) /// /// Where Data_Size comes from the source component's data type properties, /// and Period comes from the source thread's timing properties. +/// +/// Returns [`ConnectionDemand::Unknown`] rather than `0.0` when either input is +/// missing: a connection whose payload size is unknown is not a connection that +/// uses no bandwidth, and conflating the two makes a saturated bus pass clean +/// (REQ-NC-BUS-PAYLOAD-001). fn compute_connection_demand( instance: &SystemInstance, src_sub_idx: Option, _bus_map: &FxHashMap, -) -> f64 { +) -> ConnectionDemand { let src_idx = match src_sub_idx { Some(idx) => idx, - None => return 0.0, + None => return ConnectionDemand::Unknown(Unaccounted::UnresolvedSource), }; // Get data size from the source component (bits). // We look for Data_Size on the source or find a thread child. let data_size_bits = get_data_size_for_component(instance, src_idx); if data_size_bits == 0 { - return 0.0; + return ConnectionDemand::Unknown(Unaccounted::PayloadSize); } // Get Period from the source component (picoseconds). // Walk down to find a thread if the source is a process. let period_ps = get_period_for_component(instance, src_idx); if period_ps == 0 { - return 0.0; + return ConnectionDemand::Unknown(Unaccounted::SourcePeriod); } // demand = Data_Size (bits) / Period (seconds) // Period is in picoseconds, so Period_sec = period_ps / 1e12 // demand_bps = data_size_bits / (period_ps / 1e12) = data_size_bits * 1e12 / period_ps - (data_size_bits as f64) * 1e12 / (period_ps as f64) + ConnectionDemand::Known((data_size_bits as f64) * 1e12 / (period_ps as f64)) } /// Get Data_Size for a component in bits. @@ -786,15 +931,106 @@ mod tests { let inst = b.build(root); let diags = BusBandwidthAnalysis.analyze(&inst); - // No demand computed, so no diagnostics for this bus. + // REQ-NC-BUS-PAYLOAD-001 — this test previously asserted SILENCE here + // ("missing Data_Size = no demand"), which is exactly the unsound + // reading: a connection whose payload size we cannot determine is not + // a connection that uses no bandwidth. A bus carrying only such + // connections used to produce no diagnostic at all, so a saturated bus + // passed clean. It must now say what it could not measure. let bus_diags: Vec<_> = diags .iter() .filter(|d| d.analysis == "bus_bandwidth") .collect(); + assert_eq!( + bus_diags.len(), + 1, + "expected exactly one incompleteness warning: {bus_diags:?}" + ); + assert_eq!(bus_diags[0].severity, Severity::Warning); assert!( - bus_diags.is_empty(), - "missing Data_Size = no demand: {:?}", - bus_diags + bus_diags[0].message.contains("INCOMPLETE") + && bus_diags[0].message.contains("undeterminable payload size") + && bus_diags[0].message.contains("c1"), + "warning must name the gap and the connection: {}", + bus_diags[0].message + ); + // And it must NOT claim a utilization verdict off an empty sum. + assert!( + !bus_diags[0].message.contains("utilization:"), + "no verdict may be reported when nothing was measured: {}", + bus_diags[0].message + ); + } + + /// REQ-NC-BUS-PAYLOAD-001 — a bus with SOME measurable and SOME + /// unmeasurable connections must report the utilization as a lower bound, + /// not as a complete verdict. This is the case that silently under-reports + /// on real models: one connection carries a `Data_Size` property, the + /// other types its payload with a data classifier the analysis cannot see. + #[test] + fn partial_demand_is_labelled_a_lower_bound() { + let mut b = TestBuilder::new(); + let root = b.add_component("root", ComponentCategory::System, None); + let bus1 = b.add_component("bus1", ComponentCategory::Bus, Some(root)); + + // Sender A: fully specified -> contributes real demand. + let send_a = b.add_component("send_a", ComponentCategory::Process, Some(root)); + let thread_a = b.add_component("thread_a", ComponentCategory::Thread, Some(send_a)); + b.set_children(send_a, vec![thread_a]); + b.set_property(thread_a, "Memory_Properties", "Data_Size", "1 KByte"); + b.set_property(thread_a, "Timing_Properties", "Period", "1 sec"); + + // Sender B: no findable Data_Size -> unaccounted, NOT zero. + let send_b = b.add_component("send_b", ComponentCategory::Process, Some(root)); + let thread_b = b.add_component("thread_b", ComponentCategory::Thread, Some(send_b)); + b.set_children(send_b, vec![thread_b]); + b.set_property(thread_b, "Timing_Properties", "Period", "1 sec"); + + let receiver = b.add_component("receiver", ComponentCategory::Process, Some(root)); + b.set_children(root, vec![bus1, send_a, send_b, receiver]); + + // Capacity comfortably above the *measured* demand (8192 bps), so the + // bus would otherwise report a clean sub-80% Info verdict. + b.set_property(bus1, "SEI", "Bandwidth", "1 Mbitsps"); + b.add_connection("c_a", root, "send_a", "out_port", "receiver", "in_port"); + b.add_connection("c_b", root, "send_b", "out_port", "receiver", "in_port"); + b.set_property( + root, + "Deployment_Properties", + "Actual_Connection_Binding", + "reference (bus1)", + ); + + let inst = b.build(root); + let diags = BusBandwidthAnalysis.analyze(&inst); + let bus_diags: Vec<_> = diags + .iter() + .filter(|d| d.analysis == "bus_bandwidth") + .collect(); + + let warning = bus_diags + .iter() + .find(|d| d.severity == Severity::Warning) + .unwrap_or_else(|| panic!("expected an incompleteness warning: {bus_diags:?}")); + assert!( + warning.message.contains("1 of 2 bound connections") && warning.message.contains("c_b"), + "warning must quantify the gap and name the connection: {}", + warning.message + ); + + // The utilization verdict is still emitted (we did measure something), + // but it must carry the lower-bound qualifier. Select it by severity: + // the warning above also contains the word "utilization". + let verdict = bus_diags + .iter() + .find(|d| d.severity == Severity::Info) + .unwrap_or_else(|| panic!("expected a utilization verdict: {bus_diags:?}")); + assert!( + verdict + .message + .contains("LOWER BOUND: 1 connections unaccounted"), + "a partial sum must not read as a complete verdict: {}", + verdict.message ); } @@ -824,14 +1060,28 @@ mod tests { let inst = b.build(root); let diags = BusBandwidthAnalysis.analyze(&inst); + // REQ-NC-BUS-PAYLOAD-001 — the Period dual of + // `missing_data_size_no_demand`: an unknown message rate is likewise + // not a zero message rate, and used to vanish from the aggregate in + // silence. It must be reported as unaccounted. let bus_diags: Vec<_> = diags .iter() .filter(|d| d.analysis == "bus_bandwidth") .collect(); + assert_eq!( + bus_diags.len(), + 1, + "expected exactly one incompleteness warning: {bus_diags:?}" + ); + assert_eq!(bus_diags[0].severity, Severity::Warning); assert!( - bus_diags.is_empty(), - "missing Period = no demand: {:?}", - bus_diags + bus_diags[0].message.contains("INCOMPLETE") + && bus_diags[0] + .message + .contains("undeterminable source period") + && bus_diags[0].message.contains("c1"), + "warning must name the gap and the connection: {}", + bus_diags[0].message ); }