Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@ jobs:
supply-chain:
name: Supply Chain (cargo-vet)
runs-on: ubuntu-latest
continue-on-error: true
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@nightly
Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -200,9 +200,6 @@ jobs:
name: Publish to Marketplace
needs: [build-vsix, create-release]
runs-on: ubuntu-latest
if: env.VSCE_PAT != ''
env:
VSCE_PAT: ${{ secrets.VSCE_PAT }}
steps:
- uses: actions/download-artifact@v4
with:
Expand All @@ -212,6 +209,9 @@ jobs:
with:
node-version: 20
- name: Publish to VS Code Marketplace
env:
VSCE_PAT: ${{ secrets.VSCE_PAT }}
if: env.VSCE_PAT != ''
run: npx @vscode/vsce publish --packagePath vsix/*.vsix
env:
VSCE_PAT: ${{ secrets.VSCE_PAT }}
Expand Down
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ members = [
]

[workspace.package]
version = "0.1.0"
version = "0.2.0"
edition = "2024"
license = "MIT"
repository = "https://github.com/pulseengine/spar"
Expand Down
20 changes: 20 additions & 0 deletions artifacts/architecture.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,8 @@ artifacts:

- id: ARCH-R1
type: design-decision
status: implemented
satisfies: [RENDER-REQ-002]
title: Port-aware layout
description: >
Graph nodes gain explicit ports with side placement, direction
Expand All @@ -239,6 +241,8 @@ artifacts:

- id: ARCH-R2
type: design-decision
status: implemented
satisfies: [RENDER-REQ-001]
title: Orthogonal edge routing
description: >
A visibility-graph router with obstacle avoidance replaces bezier
Expand All @@ -259,6 +263,8 @@ artifacts:

- id: ARCH-R3
type: design-decision
status: implemented
satisfies: [RENDER-REQ-003]
title: Interactive HTML wrapper
description: >
A self-contained HTML file with embedded JavaScript provides
Expand All @@ -281,6 +287,8 @@ artifacts:

- id: ARCH-R4
type: design-decision
status: implemented
satisfies: [RENDER-REQ-004]
title: GLSP-inspired separation
description: >
Layout computation (GraphLayout) is separated from rendering
Expand All @@ -302,3 +310,15 @@ artifacts:
target: RENDER-REQ-004
- type: satisfies
target: RENDER-REQ-006

- id: ARCH-R5
type: design-decision
status: implemented
title: VS Code extension with native LSP and WASM rendering
description: >
VS Code extension combines native spar binary for LSP editing
intelligence (10 IDE features) with jco-transpiled spar-wasm
for in-process diagram rendering. WASI filesystem calls are
shimmed to read workspace files. Webview panel shows interactive
HTML from etch with ports, orthogonal routing, and pan/zoom.
tags: [architecture, tooling, vscode]
10 changes: 10 additions & 0 deletions artifacts/verification.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -281,6 +281,8 @@ artifacts:

- id: VAL-R1
type: feature
status: implemented
verifies: [RENDER-REQ-004]
title: Layout determinism tests (RENDER-REQ-004)
description: >
Tests verifying that the same AADL model always produces the same
Expand All @@ -298,6 +300,8 @@ artifacts:

- id: VAL-R2
type: feature
status: implemented
verifies: [RENDER-REQ-001]
title: Orthogonal routing tests (RENDER-REQ-001)
description: >
Tests verifying that edge routing produces orthogonal (rectilinear)
Expand All @@ -315,6 +319,8 @@ artifacts:

- id: VAL-R3
type: feature
status: implemented
verifies: [RENDER-REQ-002]
title: Port positioning tests (RENDER-REQ-002)
description: >
Tests verifying that ports are rendered with correct side placement,
Expand All @@ -332,6 +338,8 @@ artifacts:

- id: VAL-R4
type: feature
status: implemented
verifies: [RENDER-REQ-003, RENDER-REQ-005]
title: HTML interactive feature tests (RENDER-REQ-003, RENDER-REQ-005)
description: >
Tests verifying the interactive HTML output supports zoom, pan,
Expand All @@ -351,6 +359,8 @@ artifacts:

- id: VAL-R5
type: feature
status: implemented
verifies: [RENDER-REQ-006]
title: Semantic zoom tests (RENDER-REQ-006)
description: >
Tests verifying that semantic zoom reduces clutter at overview
Expand Down
95 changes: 95 additions & 0 deletions docs/introduction.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
# spar — AADL v2.2 Toolchain

spar is a Rust-based toolchain for the Architecture Analysis & Design Language
(AADL, SAE AS5506C). It provides parsing, semantic analysis, safety analysis,
and interactive architecture visualization for safety-critical system design.

## Architecture

```mermaid
graph TB
subgraph "spar toolchain"
P[spar-parser] --> S[spar-syntax]
S --> A[spar-annex]
S --> BD[spar-base-db]
BD --> HD[spar-hir-def]
HD --> H[spar-hir]
H --> AN[spar-analysis]
HD --> R[spar-render]
R --> CLI[spar-cli]
AN --> CLI
HD --> W[spar-wasm]
AN --> W
R --> W
HD --> T[spar-transform]
end

subgraph "shared"
E[etch] --> R
E --> W
end

subgraph "VS Code"
CLI -->|LSP stdio| VSC[VS Code Extension]
W -->|jco transpile| VSC
end

subgraph "rivet"
W -->|WASM component| RV[rivet dashboard]
end
```

## Crates

| Crate | Purpose |
|-------|---------|
| `spar-parser` | AADL v2.2 lexer and parser |
| `spar-syntax` | Lossless CST via rowan |
| `spar-annex` | EMV2 and behavior annex parsing |
| `spar-base-db` | Salsa incremental computation database |
| `spar-hir-def` | HIR definitions: item tree, instance model, properties |
| `spar-hir` | Public HIR facade with serde serialization |
| `spar-analysis` | 21 analysis passes (scheduling, latency, connectivity, etc.) |
| `spar-render` | SVG/HTML rendering via etch compound layout |
| `spar-transform` | WIT/WAC/Rust crate transforms |
| `spar-cli` | CLI (`spar parse/items/instance/analyze/render/modes/verify/lsp`) |
| `spar-wasm` | WASM component (wasm32-wasip2) for rivet integration |
| `etch` | Shared graph layout + SVG rendering engine (in rivet repo) |

## Key Features

- **Full AADL v2.2 parser** with error recovery and lossless syntax tree
- **21 analysis passes** including RMA scheduling, latency, EMV2 fault trees, mode reachability
- **Port-aware rendering** with orthogonal edge routing and interactive HTML
- **LSP server** with 10 IDE features (diagnostics, hover, completion, go-to-def, rename, etc.)
- **WASM component** for browser-side rendering in rivet dashboard
- **VS Code extension** with syntax highlighting, LSP, and live diagram webview
- **Lean4 formal proofs** for scheduling theory (RTA convergence, RM bound)
- **Requirements verification** via `spar verify` with TOML-based thresholds

## CLI Commands

```
spar parse [--tree] <file...> Parse and report diagnostics
spar items [--format text|json] <file...> Show declarations
spar instance --root Pkg::Type.Impl [--analyze] <file...> Instantiate system
spar analyze --root Pkg::Type.Impl [--format text|json] <file...> Run analyses
spar render --root Pkg::Type.Impl [--format svg|html] [-o out] <file...> Render diagram
spar modes --root Pkg::Type.Impl [--format text|smv|dot] <file...> Mode analysis
spar verify [--format text|json] --root Pkg::Type.Impl req.toml <file...> Check requirements
spar lsp Start LSP server
```

## Safety Traceability

spar uses rivet for lifecycle artifact management:

```
STPA Analysis (analysis.yaml)
→ Safety Requirements (requirements.yaml, rendering-analysis.yaml)
→ Architecture Decisions (architecture.yaml)
→ Verification Evidence (verification.yaml)
```

All safety requirements are traced from hazard analysis through implementation
to test evidence. See `safety/stpa/` and `artifacts/` directories.
2 changes: 1 addition & 1 deletion rivet.yaml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
project:
name: spar
version: "0.1.0"
version: "0.2.0"
description: >
AADL v2.2 toolchain — parser, HIR, analyses, LSP, WASM.
Tracks requirements derived from SAE AS5506C, architecture decisions,
Expand Down
21 changes: 20 additions & 1 deletion safety/stpa/rendering-analysis.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -111,54 +111,73 @@ artifacts:
- id: RENDER-REQ-001
type: safety-requirement
title: Orthogonal edge routing
status: implemented
description: >
Edges must use orthogonal (rectilinear) routing to minimize
visual crossings. The routing algorithm must avoid overlapping
edges and route around component obstacles.
hazards: [H-R1]
satisfies: [ARCH-R2]
verified-by: [VAL-R2]

- id: RENDER-REQ-002
type: safety-requirement
title: Visible ports with directional indicators
status: implemented
description: >
Ports must be rendered as visible elements on component
boundaries with directional indicators (arrows for in/out/in-out)
and type-based coloring (distinct colors for data, event, event
data, bus access, etc.).
hazards: [H-R2]
satisfies: [ARCH-R1]
verified-by: [VAL-R3]

- id: RENDER-REQ-003
type: safety-requirement
title: Interactive HTML with zoom/pan/minimap/search
status: partial
description: >
The interactive HTML output must support zoom, pan, a minimap
for orientation in large models, and text search to locate
components by name.
components by name. Phase 3a (zoom/pan/selection) is implemented;
Phase 3b (minimap/search) is deferred.
hazards: [H-R3]
satisfies: [ARCH-R3]
verified-by: [VAL-R4]

- id: RENDER-REQ-004
type: safety-requirement
title: Deterministic layout
status: implemented
description: >
Layout must be deterministic — the same AADL model must always
produce the same rendered layout. No randomized placement or
non-deterministic ordering.
hazards: [H-R4]
satisfies: [ARCH-R4]
verified-by: [VAL-R1]

- id: RENDER-REQ-005
type: safety-requirement
title: Selection and group highlighting
status: implemented
description: >
Interactive output must support selecting a component or
connection and highlighting its connected neighbors, ports,
and edges to isolate subsystems for focused review.
hazards: [H-R5]
satisfies: [ARCH-R3]
verified-by: [VAL-R4]

- id: RENDER-REQ-006
type: safety-requirement
title: Semantic zoom
status: implemented
description: >
At overview zoom levels, rendering must reduce visual clutter
by collapsing internal details and showing only component
boundaries and inter-component connections.
hazards: [H-R3]
satisfies: [ARCH-R4]
verified-by: [VAL-R5]
Loading