Node Type — Frontmatter

A document's type is declared in YAML frontmatter:

---
type: spec
---

A type is an identifier ([a-z][a-z0-9_-]*). Valid types must be declared in the trace.types config array. A document with a type not listed in config is an error. Documents without type are untyped — they may be navigation link targets but cannot be trace link sources or targets.

Trace Edges — Markdown Links with Edge Name Prefix

Trace links use standard markdown link syntax with an <edge_name>:: prefix in the link text:

This epic [covers::Login Story](../stories/login.md) and
[covers::Password Reset](../stories/password-reset.md).

• Standard markdown links — render and click in any viewer
• Link text starts with <edge_name>:: where edge name is declared in config
• Text after :: is the display text — it is required
• Plain links without the <identifier>:: pattern are navigation links — no trace semantics
• Edge name is always required — no inference or shorthand

Documents Are Atoms

One document = one node. No heading-level references. Fragment anchors in links are stripped before resolution — documents are atoms.

Structural Guarantee

When an edge kind connects documents of different types (e.g., feature → test), the type system alone prevents reverse cycles within that edge kind. This means hierarchical traceability (theme → epic → story → test) is inherently acyclic without needing the acyclic flag.

module tracegraph

sig Type {}
sig Doc { dtype: one Type }

sig EdgeKind {
  fromType: one Type,
  toType: one Type
}

sig Link {
  kind: one EdgeKind,
  src: one Doc,
  tgt: one Doc
}

-- links are well-typed
fact wellTyped {
  all l: Link |
    l.src.dtype = l.kind.fromType and
    l.tgt.dtype = l.kind.toType
}

-- self-loops are forbidden
fact noSelfLoop {
  no l: Link | l.src = l.tgt
}

-- cross-type edges cannot form reverse pairs
assert crossTypeNoReverse {
  all ek: EdgeKind | ek.fromType != ek.toType implies
    no disj l1, l2: Link | l1.kind = ek and l2.kind = ek and
      l1.src = l2.tgt and l1.tgt = l2.src
}

check crossTypeNoReverse for 5

pred sanityCheck {}
run sanityCheck {} for 5

Count Notation

Format: <source> → <target>, where each side is a UML multiplicity. Both → (U+2192) and -> (ASCII) are accepted.

Source side (left of →): how many sources each target document must be linked from. Target side (right of →): how many targets each source document must link to.

Omitted count defaults to 0..* → 0..* (no constraints).

Cardinality

For each edge type with a count constraint, every document of the relevant type must satisfy both source-side and target-side multiplicity.

Cardinality constraints apply to direct edges only. Transitive edges (computed via transitive: true) do not count toward cardinality — an indirect link A → B → C does not satisfy a "must have at least 1 outgoing edge" constraint on A unless A also has a direct edge.

Cycle Detection

Edges with acyclic: true reject cycles.

Transitive Closure

When transitive: true, specdown computes the transitive closure. If A requires B and B requires C, A transitively requires C. Transitive edges appear in the report graph but do not affect cardinality checks — only direct edges satisfy count constraints.

Strict Mode

With --strict, validation errors cause a non-zero exit code.