Skip to content

Commit 0eb41b5

Browse files
avrabeclaude
andauthored
feat(tsn): Spar_TSN property set + spar-network::tsn skeleton (v0.8.1 c1/5) (#177)
Foundation for Track D Phase 2 TSN-shaped service curves. Adds the Spar_TSN property set (Stream_ID, Class_of_Service, Gate_Control_List, Max_Frame_Size, Frame_Preemption) and a placeholder tsn module in spar-network with GateWindow, ClassOfService, CreditPool types. No TAS / CBS / preemption math in this commit — that's commits 2-4. Total predeclared property count 122 → 127. New requirement: REQ-TSN-001. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent ebbe9af commit 0eb41b5

5 files changed

Lines changed: 541 additions & 3 deletions

File tree

artifacts/requirements.yaml

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1436,4 +1436,27 @@ artifacts:
14361436
status: planned
14371437
tags: [network, wctt, lean, proofs, v080]
14381438

1439+
- id: REQ-TSN-001
1440+
type: requirement
1441+
title: Spar_TSN property surface for Time-Sensitive Networking
1442+
description: >
1443+
Spar_TSN property surface declares stream identification,
1444+
class-of-service, gate-control-list (raw string in v0.8.1,
1445+
structured in v0.9.x), max frame size, and frame preemption
1446+
hooks. Properties are: Stream_ID (aadlinteger 0..2**32-1; port,
1447+
connection), Class_of_Service (aadlinteger 0..7; port,
1448+
connection), Gate_Control_List (aadlstring; bus —
1449+
v0.8.1 raw blob, v0.9.x structured GateWindow record),
1450+
Max_Frame_Size (aadlinteger units Size_Units; port, connection),
1451+
and Frame_Preemption (aadlboolean; port, connection). Foundation
1452+
for Track D Phase 2 TSN-shaped service curves: TAS gate-window
1453+
(802.1Qbv), CBS credit-pool (802.1Qav), and frame preemption
1454+
(802.1Qbu). v0.8.1 commit 1 ships the property surface and the
1455+
spar-network::tsn module skeleton (GateWindow, ClassOfService,
1456+
CreditPool types plus property accessors); subsequent commits
1457+
add the analysis math. Per
1458+
docs/designs/track-d-tsn-wctt-research.md §5.1.
1459+
status: planned
1460+
tags: [network, tsn, wctt, v081]
1461+
14391462
# Research findings tracked separately in research/findings.yaml

artifacts/verification.yaml

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1892,3 +1892,34 @@ artifacts:
18921892
links:
18931893
- type: satisfies
18941894
target: REQ-NETWORK-007
1895+
1896+
- id: TEST-TSN-PROPS
1897+
type: feature
1898+
title: Spar_TSN property-set + spar-network::tsn surface
1899+
description: >
1900+
Verifies that the v0.8.1 commit 1 TSN property surface is
1901+
registered and reachable. Asserts that Spar_TSN appears in
1902+
STANDARD_PROPERTY_SET_NAMES with the expected five properties
1903+
(Stream_ID, Class_of_Service, Gate_Control_List, Max_Frame_Size,
1904+
Frame_Preemption), that each resolves via GlobalScope without
1905+
explicit `with` imports, and that the total predeclared property
1906+
count is 127 (was 122 before this commit). Verifies the
1907+
spar-network::tsn placeholder types (GateWindow, ClassOfService,
1908+
CreditPool) construct, that ClassOfService enforces the 0..=7
1909+
range and orders by 802.1Q priority, and that the property
1910+
accessors (get_stream_id, get_class_of_service,
1911+
get_max_frame_size_bytes, get_frame_preemption,
1912+
get_gate_control_list_raw) read both typed PropertyExpr values
1913+
and string-fallback values from a PropertyMap.
1914+
fields:
1915+
method: automated-test
1916+
steps:
1917+
- run: cargo test -p spar-hir-def --lib -- standard_properties
1918+
- run: cargo test -p spar-network --lib -- tsn
1919+
status: passing
1920+
tags: [v0.8.1, network, tsn, properties]
1921+
links:
1922+
- type: satisfies
1923+
target: REQ-TSN-001
1924+
- type: satisfies
1925+
target: REQ-NETWORK-001

crates/spar-hir-def/src/standard_properties.rs

Lines changed: 143 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ pub const STANDARD_PROPERTY_SET_NAMES: &[&str] = &[
3939
"Spar_Network",
4040
"Spar_Migration",
4141
"Spar_Power",
42+
"Spar_TSN",
4243
];
4344

4445
// ── Timing_Properties ───────────────────────────────────────────────
@@ -457,6 +458,50 @@ const SPAR_POWER: &[(&str, &str)] = &[
457458
("Power_Budget", "Time"),
458459
];
459460

461+
// ── Spar_TSN ────────────────────────────────────────────────────────
462+
//
463+
// Non-standard property set defined by spar itself (not AS5506); used
464+
// for Time-Sensitive Networking (TSN) WCTT analysis (Track D Phase 2,
465+
// v0.8.1+). Provides the AADL vocabulary for TSN-shaped service
466+
// curves: TAS gate-control schedules (802.1Qbv), CBS credit-pool
467+
// classes (802.1Qav), and frame preemption (802.1Qbu). Sits alongside
468+
// `Spar_Network::*` (Phase 1, switch-discriminator + classical
469+
// FIFO/Priority disciplines).
470+
//
471+
// v0.8.1 commit 1 ships the property surface only; subsequent commits
472+
// in the v0.8.1 series add the analysis math (TAS gate-window service
473+
// curves, CBS credit accounting, frame-preemption hooks). See
474+
// `docs/designs/track-d-tsn-wctt-research.md` §5.1 (property design)
475+
// and §5.2 (switch modeling).
476+
477+
const SPAR_TSN: &[(&str, &str)] = &[
478+
// Per-stream identifier required by TAS gate-control lists and
479+
// by stream reservation (802.1Qcc). Applies to port and connection.
480+
("Stream_ID", "aadlinteger 0..2**32-1"),
481+
// 802.1Q priority class (0-7). Drives queue selection at switches
482+
// and gate-mask matching in the TAS gate-control list.
483+
// Applies to port and connection.
484+
("Class_of_Service", "aadlinteger 0..7"),
485+
// Time-aware-shaper gate schedule — 802.1Qbv gate-control list.
486+
// For v0.8.1 commit 1 the value is parsed only as an opaque string
487+
// blob (the structured form lands in v0.8.1 commit 2 once the TAS
488+
// service-curve math is wired up).
489+
//
490+
// Future v0.9.x: structured form via Gate_Window record.
491+
//
492+
// Applies to bus.
493+
("Gate_Control_List", "aadlstring"),
494+
// Maximum frame size in bytes (typed as `aadlinteger units
495+
// Size_Units` so it lowers to bytes via the existing AADL
496+
// size-unit machinery). Frame-preemption (802.1Qbu) and
497+
// serialization-time terms read this. Applies to port and
498+
// connection.
499+
("Max_Frame_Size", "aadlinteger units Size_Units"),
500+
// Whether frames in this class can be pre-empted by Express
501+
// traffic (802.1Qbu). Applies to port and connection.
502+
("Frame_Preemption", "aadlboolean"),
503+
];
504+
460505
/// Helper: collect properties from a table into the result vector.
461506
fn collect_properties(
462507
table: &[(&'static str, &'static str)],
@@ -497,6 +542,7 @@ pub fn all_standard_properties() -> Vec<StandardProperty> {
497542
collect_properties(SPAR_NETWORK, "Spar_Network", &mut result);
498543
collect_properties(SPAR_MIGRATION, "Spar_Migration", &mut result);
499544
collect_properties(SPAR_POWER, "Spar_Power", &mut result);
545+
collect_properties(SPAR_TSN, "Spar_TSN", &mut result);
500546

501547
result
502548
}
@@ -527,6 +573,7 @@ fn lookup_table(set_lower: &str) -> Option<&'static [(&'static str, &'static str
527573
"spar_network" => Some(SPAR_NETWORK),
528574
"spar_migration" => Some(SPAR_MIGRATION),
529575
"spar_power" => Some(SPAR_POWER),
576+
"spar_tsn" => Some(SPAR_TSN),
530577
_ => None,
531578
}
532579
}
@@ -576,6 +623,7 @@ mod tests {
576623
assert!(is_standard_property_set("Spar_Network"));
577624
assert!(is_standard_property_set("Spar_Migration"));
578625
assert!(is_standard_property_set("Spar_Power"));
626+
assert!(is_standard_property_set("Spar_TSN"));
579627

580628
// Case-insensitive
581629
assert!(is_standard_property_set("timing_properties"));
@@ -1027,6 +1075,96 @@ mod tests {
10271075
);
10281076
}
10291077

1078+
#[test]
1079+
fn test_standard_properties_in_spar_tsn() {
1080+
// Spar_TSN is a known property set.
1081+
assert!(is_standard_property_set("Spar_TSN"));
1082+
1083+
let props = standard_properties_in_set("Spar_TSN");
1084+
assert_eq!(props.len(), 5);
1085+
assert!(props.contains(&"Stream_ID"));
1086+
assert!(props.contains(&"Class_of_Service"));
1087+
assert!(props.contains(&"Gate_Control_List"));
1088+
assert!(props.contains(&"Max_Frame_Size"));
1089+
assert!(props.contains(&"Frame_Preemption"));
1090+
1091+
// Each property resolves to its expected type.
1092+
assert_eq!(
1093+
standard_property_type("Spar_TSN", "Stream_ID"),
1094+
Some("aadlinteger 0..2**32-1")
1095+
);
1096+
assert_eq!(
1097+
standard_property_type("Spar_TSN", "Class_of_Service"),
1098+
Some("aadlinteger 0..7")
1099+
);
1100+
assert_eq!(
1101+
standard_property_type("Spar_TSN", "Gate_Control_List"),
1102+
Some("aadlstring")
1103+
);
1104+
assert_eq!(
1105+
standard_property_type("Spar_TSN", "Max_Frame_Size"),
1106+
Some("aadlinteger units Size_Units")
1107+
);
1108+
assert_eq!(
1109+
standard_property_type("Spar_TSN", "Frame_Preemption"),
1110+
Some("aadlboolean")
1111+
);
1112+
1113+
// Deliberately-wrong name returns None.
1114+
assert_eq!(standard_property_type("Spar_TSN", "Nonexistent"), None);
1115+
1116+
// Case-insensitive.
1117+
assert_eq!(
1118+
standard_property_type("spar_tsn", "stream_id"),
1119+
Some("aadlinteger 0..2**32-1")
1120+
);
1121+
assert_eq!(
1122+
standard_property_type("SPAR_TSN", "FRAME_PREEMPTION"),
1123+
Some("aadlboolean")
1124+
);
1125+
}
1126+
1127+
#[test]
1128+
fn test_spar_tsn_property_set_resolved_via_global_scope() {
1129+
use crate::name::Name;
1130+
use crate::resolver::{GlobalScope, ResolvedProperty};
1131+
1132+
let scope = GlobalScope::from_trees(vec![]);
1133+
1134+
// Each Spar_TSN property is resolvable without explicit `with`.
1135+
for prop_name in [
1136+
"Stream_ID",
1137+
"Class_of_Service",
1138+
"Gate_Control_List",
1139+
"Max_Frame_Size",
1140+
"Frame_Preemption",
1141+
] {
1142+
let result = scope.resolve_property(&Name::new("Spar_TSN"), &Name::new(prop_name));
1143+
assert!(
1144+
matches!(result, ResolvedProperty::PropertyDef { .. }),
1145+
"expected PropertyDef for Spar_TSN::{}, got {:?}",
1146+
prop_name,
1147+
result
1148+
);
1149+
}
1150+
1151+
// Deliberately-wrong name inside a known spar set is Unresolved.
1152+
let result = scope.resolve_property(&Name::new("Spar_TSN"), &Name::new("Nonexistent"));
1153+
assert!(
1154+
matches!(result, ResolvedProperty::Unresolved),
1155+
"expected Unresolved for Spar_TSN::Nonexistent, got {:?}",
1156+
result
1157+
);
1158+
1159+
// Case-insensitive resolution.
1160+
let result = scope.resolve_property(&Name::new("spar_tsn"), &Name::new("stream_id"));
1161+
assert!(
1162+
matches!(result, ResolvedProperty::PropertyDef { .. }),
1163+
"expected case-insensitive match for Spar_TSN::Stream_ID, got {:?}",
1164+
result
1165+
);
1166+
}
1167+
10301168
#[test]
10311169
fn test_standard_properties_unknown_set() {
10321170
let props = standard_properties_in_set("Nonexistent_Properties");
@@ -1043,15 +1181,17 @@ mod tests {
10431181
#[test]
10441182
fn test_all_standard_properties_total_count() {
10451183
let all = all_standard_properties();
1046-
// 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 = 122
1184+
// 12 + 13 + 14 + 14 + 8 + 25 + 4 + 13 + 5 + 4 + 5 + 4 + 1 + 5 = 127
10471185
// (Timing + Communication + Memory + Deployment + Thread + Programming
10481186
// + Modeling + AADL_Project + Spar_Timing + Spar_Trace + Spar_Network
1049-
// + Spar_Migration + Spar_Power)
1187+
// + Spar_Migration + Spar_Power + Spar_TSN)
10501188
// Thread_Properties: +1 for Locking_Protocol (v0.7.1 PIP/PCP).
10511189
// Spar_Timing: +1 for Critical_Section_Blocking (v0.7.1 PIP/PCP).
10521190
// Spar_Network: +1 for WCTT_Budget (Track D commit 4).
10531191
// Spar_Power: +1 for Power_Budget (Track E commit 5/8 ranker).
1054-
assert_eq!(all.len(), 122);
1192+
// Spar_TSN: +5 for Stream_ID, Class_of_Service, Gate_Control_List,
1193+
// Max_Frame_Size, Frame_Preemption (Track D Phase 2 v0.8.1 c1).
1194+
assert_eq!(all.len(), 127);
10551195
}
10561196

10571197
#[test]

crates/spar-network/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,10 +46,12 @@
4646

4747
pub mod curves;
4848
pub mod extract;
49+
pub mod tsn;
4950
pub mod types;
5051

5152
pub use curves::{
5253
ArrivalCurve, NcError, ServiceCurve, backlog_bound, delay_bound, output_bound, residual_service,
5354
};
5455
pub use extract::extract_network_graph;
56+
pub use tsn::{ClassOfService, CreditPool, GateWindow};
5557
pub use types::{NetworkGraph, NetworkLink, NetworkNode, NodeKind, SwitchType};

0 commit comments

Comments
 (0)