feat(runtrace): render a run's trace as a state timeline and a message sequence

[devin-ai-integration]

What and why

A running engine can draw a run's behaviour, which a static model view cannot. This PR renders the runtime's structured trace in two ways:

• State timeline: one lane per object machine, showing which state configuration was active over clock time, with transition triggers. Choice and guard records appear as marks.
• Message sequence: sends and accepts between runtime objects, ordered by clock time, with payloads.

Representation: a new view.KindTimeline, and reuse of KindSequence

• Run sequence → KindSequence. A run sequence has the same shape as a model sequence: lifelines plus ordered messages. The new internal/exec/runtrace package builds Roots (one participant per object, plus environment for sends from outside the run) and Edges (messages in clock order). The existing text, Mermaid and PlantUML sequence writers then draw it unchanged, and DOT is refused as it already is for sequences.
• Timeline → new view.KindTimeline. No existing kind carries time-valued data. KindState is the graph of declared states and transitions, not which states one object held between which instants. Rendering gains Run, RunUntil and Lanes (Lane/Span/LaneTransition/Mark).
• Not a model view. KindTimeline is not in Kinds(), is not a pseudo-view (#timeline is refused), is never returned by KindOf, and is refused as a document Diagram kind. The model stays plain SysML v2 and no library vocabulary is added.

Forms

	text	mermaid	plantuml	dot	d2
timeline	per-lane spans, transitions, notes	gantt with displayMode: compact	concise timing diagram	refused	refused
sequence	existing sequence text	sequenceDiagram	sequence diagram	refused	refused

• Mermaid timeline uses gantt in compact mode. Compact mode puts each lane on one row against a shared numeric time axis, with real durations. Mermaid's timeline grammar is a list of categorical periods, with no durations and no shared axis. Choice and guard records become %% comments plus a notice, because gantt has no notes.
• PlantUML timeline uses concise. robust needs a fixed, ordered set of states per lane. Here a lane value is the active configuration of a machine, e.g. parallel leaves waiting | charged, which is free text. Choice and guard records become note top of.
• DOT is refused. It has no time axis, and the model sequence already refuses DOT. The refusal reads a timeline rendering is not written as dot; ask for text, mermaid or plantuml.
• D2 is refused for run renderings. D2, which develop added for model renderings, is not a run form: -render-run and %render-run write text, Mermaid and PlantUML, and a run timeline or sequence asked for as D2 is refused with an error that lists only those forms. Model sequences still render as D2.

Runtime record additions

Entry, exit and do trace records now carry:

• Path: the state qualified by the states written around it.
• Region: the innermost orthogonal region, qualified the same way.

With these, the timeline can rebuild the active configuration and order parallel leaves by region. The printed trace text is unchanged and every existing .trace.golden is byte-identical.

Three helpers moved so the query layer and the renderer share one implementation instead of duplicating it:

• TraceRecord.Machine() and TraceRecord.PayloadTexts() moved from internal/doc/queryexec into runtime.
• StateExecutor.RegionOf now holds the region walk that queryexec used before.

Entry and exit records also carry Source, the origin of the state's declaration, which source links use.

Three further runtime additions keep the renderings correct:

• Message identity. runtime.Message gains Serial, a per-context number assigned when a message is posted. It is never rolled back by snapshots or journal rollback, and imported messages get fresh serials. Send and accept records carry it as TraceRecord.Message, so the sequence pairs an accept with the exact send it took, even when same-named signals from different definitions reach one object. Records without a serial fall back to matching by event and target.
• Termination. A new TraceTerminate kind records a terminate action or the end of the occurrence performing a machine, with the clock instant and origin. Its printed line is the existing one. The timeline closes the lane's occupancy there and marks it, since termination abandons states without exiting them. Because terminate is a documented Events kind, a state run's trace from ExecuteState (gRPC, clients and the browser engine) also reports it.
• Parallel identity. The timeline keys active states by state path plus region path, so same-named leaves in sibling regions stay distinct. Colliding leaf names in one span are labelled by their shortest distinguishing path (left.waiting | right.waiting).

The end instant comes from the clock, so the run_start/run_end records proposed in the observing-a-run design are not needed yet.

Timeline semantics

• Records at one instant are merged, so each instant produces at most one new span per lane.
• States entered and left within one instant are listed as "via" in the text form.
• A self-transition starts a new span.
• A state still active at the end is drawn up to the run's clock instant and marked as held at the end.

Surfaces

• CLI: -render-run <timeline|sequence>=<path>, repeatable, declared next to -trace.
  • The form comes from -render-form or the path's extension (.txt, .mmd/.mermaid, .puml/.plantuml); - writes text to stdout.
  • The run is recorded silently unless -trace also asks for the printed trace.
  • It is refused, with a usage error, without a behavior run, and together with -schedule explore, -engine check|smt|all, -runs, -sweep/-samples, -record-run, model or document rendering, -convert/-migrate or -query.
• REPL: %render-run <timeline|sequence> [text|mermaid|plantuml|dot] [link=<template>] renders the trace recorded since %trace on, up to the current clock instant. Objects are labelled by the path the session reaches them by. The command has help and completion.
• Source links: -render-link <template> (CLI) and link=<template> (REPL) apply to run renderings, following the source-link conventions the model renderings use:
  • Sequence (Mermaid and PlantUML): each object participant links to the declaration of its type or usage; messages are not linked, because the trace records no send or accept site.
  • PlantUML timeline: each lane links to its state machine, and a span showing exactly one state links to that state's declaration. Spans showing a parallel configuration are not linked.
  • Mermaid timeline: not linked. Gantt click targets carry no anchor in mermaid-cli SVG output.
  • Without a template, every output is unchanged.
• Refused combinations added: -json with a -render-run ...=- stdout target (the JSON document would be broken), and -compare-results (it compares many runs, so there is no single trace).
• HTML/PDF documents: not embedded. The document backends do not run behaviors: -render-document refuses -state/-advance, and a document Diagram selects a model rendering. Embedding a run would need a document-level way to describe the run, which would be new model vocabulary. The limitation is documented in docs/project/view-rendering-forms.md.
• LSP: not offered. It holds no live run.

Long and truncated runs

• Long runs are capped and summarised. Each rendering draws at most 200 spans or messages. The timeline is cut at the start of the 201st span, and the sequence keeps its first 200 messages. A not represented: notice reports how much was cut and the time range it covers.
• Truncated traces are drawn with a warning. When the recorder dropped earlier records, the rendering shows what it kept and a notice says how many records up to which instant were lost.

Example

examples/run-timeline/run-timeline.sysml: a controller and an instrument, sibling parts joined by a connector. Each exhibits a state machine. Timers drive the controller to send Ping(seq) and the instrument to answer Ack(seq). A parallel state gives a recorded choice point.

sysml examples/run-timeline/run-timeline.sysml \
  -instantiate RunTimeline::mission \
  -state "RunTimeline::Controller::modes RunTimeline::mission.controller" \
  -state "RunTimeline::Instrument::modes RunTimeline::mission.instrument" \
  -advance 6 \
  -render-run timeline=timeline.mmd \
  -render-run sequence=sequence.puml

Mermaid timeline (gantt, compact):

PlantUML timeline (concise):

Mermaid sequence:

PlantUML sequence:

PlantUML timeline with source links (lanes and single-state spans are links; parallel spans are not):

Specification basis

No specification behaviour changes: this is an output of the execution engine. docs/project/spec-compliance.md gains a "Run renderings" table covering the timeline, the run sequence, and the state-path and region fields on trace records.

How it was verified

• Goldens in internal/exec/runtrace/testdata/, all new files:
  • Example run: both kinds in text, Mermaid and PlantUML.
  • Empty run: both kinds in all three forms.
  • Capped long runs: more than 200 spans and messages.
  • Truncated recorder.
  • An unevaluable-guard mark.
  • Unmatched, environment and broadcast messages.
  • A self-transition.
  • A #<id> label escaped for PlantUML.
  • DOT refusal for both kinds.
  • Parallel regions with same-named leaves, same-named signals from two definitions (serial pairing), and a machine terminating while another advances the clock.
  • Linked output: run sequence (Mermaid, PlantUML), example and parallel-region timelines (PlantUML).
• Other tests:
  • internal/ir/view/run_timeline_test.go: form support for KindTimeline, and that it is neither a model kind nor a pseudo-view.
  • internal/exec/runtime/trace_records_test.go: entry and exit records carry path and region.
  • cmd/sysml/render_run_test.go: CLI artifacts, stdout output and every refusal.
  • internal/frontend/repl/run_render_test.go: REPL output, path labels, the missing-trace error, form refusal and completion.
  • internal/exec/runtime: message serials across snapshot restore, journal rollback and held-image import.
  • The cap keeps exactly 200 spans when many start at one instant, and keeps a lane's gap before the cut.
• No existing golden changed. git diff --diff-filter=M origin/develop -- '*.golden' is empty.
• Pilot validation: the example and the new test models have 0 errors against the pinned OMG pilot validator (validate-sysml-batch with the OpenSysML library path).
• Gates: go build ./..., go vet ./..., gofmt -l . (empty), go test ./..., make docs-check, make docs-counts, make man-check all pass.
• Rendering checked by hand: the Mermaid output was rendered with mermaid-cli 11 and the PlantUML output with PlantUML 1.2026.8; images above.
• Baseline counts moved: the new example adds a file to the pilot differential. The baseline and its derived figures were regenerated by make docs-counts, including the headline lines that TestW6FSkillDocumentCountsMatchBaseline pins.

Checklist

• make test and make lint pass locally (go test ./... passes locally; make lint is left to CI)
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

End-to-end verification against 8300b2b, using the CLI, a real-terminal REPL session, and the Mermaid and PlantUML converters.

Empty recorded run	Timeline extended to t=8

Mermaid timeline	PlantUML timeline

• CLI artifacts: all six match their goldens byte for byte. Extension inference, aliases, explicit forms and stdout work.
• CLI refusals: every incompatible combination returns a usage error, and no partial file is left behind.
• -trace with rendering: the 162 printed trace lines are unchanged.
• REPL:
  • Tab completion of kinds and forms, help, DOT refusal and the missing-trace error behave as documented.
  • %trace on before any run renders the empty notice.
  • Advancing from t=6 to t=8 keeps the earlier history.
• Unreachable object: a displaced object renders the literal label #1.modes in PlantUML.
• Sequence diagrams: both forms show the six Ping/Ack messages carrying seq = 1.
• Known gap: PlantUML's axis shows an empty tick at 7, but every bar stops at the run end, t=6.

[devin-ai-integration]

This branch now conflicts with develop. Conflicting files, and the merged PRs that changed them:

• docs/project/pilot-differential-baseline.json (fix(runtime): explore every order of unordered statements in calc, constraint and case bodies #864)

To resolve: merge current develop into this branch with an ordinary merge commit (no rebase or force-push).
Don't hand-merge generated files: regenerate docs/project/pilot-differential-baseline.json with go run -C tools ./cmd/pilot-diff -update after the merge.

Planned merge order for the view and docs PRs: #889 → #881 → #871 → #882 → #884 → #885 → #886. Each needs these files regenerated again after the one before it merges.

Re-run the full gate (go build ./..., go vet ./..., gofmt -l ., make lint, make docs-check, go test ./...) and wait for green CI before marking ready.

[devin-ai-integration]

Hold on pushes: please don't push to this branch, including develop merges or empty commits to retrigger CI, until a maintainer says the CI runners are free. Prepare the conflict resolution locally and push it then.