validate

type Check ¶

type Check interface {
	// Code returns the stable identifier (e.g. "IPMV2.7") used to tag findings.
	Code() string
	// Description returns a one-line description used in --list-checks output.
	Description() string
	// Run inspects g and returns any findings.
	Run(g *model.IpmGraph) []Finding
}

Check is one semantic validation pass over an IpmGraph.

func AllChecks() []Check

IPMV1.1  Self-loop
IPMV1.2  Duplicate edge per unordered node pair
IPMV1.3  SST type-pair conformance against the γ(3,4) table

IPMV2.1  PartOf is a DAG
IPMV2.2  LeadsTo is a DAG
IPMV2.6  Happens-before (LeadsTo + PartOf composition) is acyclic
IPMV2.7  Sibling sub-events should have declared leads-to order
IPMV2.8  Leads-to edge crossing into a container the predecessor is outside of
IPMV2.9  Leads-to must connect whole (outermost) events, not a part-of sub-part
IPMV4.5.3 Stranded thing
IPMV4.5.4 Stranded event

func AllChecksWith(strict bool) []Check

type DuplicatePairCheck ¶

type DuplicatePairCheck struct{}

DuplicatePairCheck implements IPMV1.2 and §1.7: at most one SST edge may connect any unordered pair of nodes. The four SST relations are mutually exclusive per pair.

func (DuplicatePairCheck) Code() string

func (DuplicatePairCheck) Description() string

func (DuplicatePairCheck) Run(g *model.IpmGraph) []Finding

type Finding ¶

type Finding struct {
	Code     string   `json:"code"`     // stable identifier, e.g. "IPMV2.7"
	Severity Severity `json:"severity"` // error / warning / info
	Message  string   `json:"message"`  // human-readable description
	Suggest  string   `json:"suggest,omitempty"`
	// Location in the source ipmt, derived from the parser's byte positions.
	File   string `json:"file,omitempty"`
	Line   int    `json:"line,omitempty"`   // 1-based
	Column int    `json:"column,omitempty"` // 1-based
	// Node / edge identifiers for programmatic consumers.
	NodeIDs []int `json:"nodeIds,omitempty"`
	EdgeID  int   `json:"edgeId,omitempty"`
}

Finding is one semantic issue surfaced by a check.

func Run(g *model.IpmGraph) []Finding

func RunChecks(g *model.IpmGraph, checks []Check) []Finding

func (f Finding) String() string

type HappensBeforeCheck ¶

type HappensBeforeCheck struct{}

HappensBeforeCheck implements IPMV2.6: LeadsTo and PartOf compose into a happens-before partial order whose own cycles are temporal nonsense, even when each relation is individually acyclic.

Propagation rules (from sst-34.md + the validator-ideas doc):

1. x --> y (LeadsTo) ⇒ x happens-before y
2. x --::P--> y AND y --> z (LeadsTo) ⇒ x happens-before z (a sub-event must finish before its parent's successor starts)

Implementation: build a derived edge set under those rules, then run SCC detection. Any non-trivial SCC indicates an inconsistency.

func (HappensBeforeCheck) Code() string

func (HappensBeforeCheck) Description() string

func (HappensBeforeCheck) Run(g *model.IpmGraph) []Finding

type LeadsToContainerCrossCheck ¶

type LeadsToContainerCrossCheck struct{}

LeadsToContainerCrossCheck implements IPMV2.8: a LeadsTo edge `A → B` should not "dip into" a container event P that A is outside of. If B is (transitively) part-of P, then A must either also be part-of P (the cascade stays within P) or have a LeadsTo path to P (A is a predecessor of the whole container). Otherwise the leads-to edge implicitly reaches into a container without explanation; the cleaner model is to lead-to the container itself.

Motivation: the observation/observer asymmetry surfaced by the UC-3 case where `probe-health-9 --> stalled-9` with `stalled-9 --::P--> task-007` puts the *observation* inside task-007 even though the *observer* (probe-health-9) is outside it. The validator's §2.6 happens-before check passes (no cycle), but the modelling is asymmetric.

Detection: for each LeadsTo edge A → B, walk B's transitive PartOf ancestors. For each ancestor P that's not also an ancestor of A and that A doesn't reach via LeadsTo, flag the edge.

func (LeadsToContainerCrossCheck) Code() string

func (LeadsToContainerCrossCheck) Description() string

func (LeadsToContainerCrossCheck) Run(g *model.IpmGraph) []Finding

type LeadsToDagCheck ¶

type LeadsToDagCheck struct{}

LeadsToDagCheck implements IPMV2.2: causal flow must be acyclic. A cycle in LeadsTo implies an event leading temporally back to itself. Loops in process models are expressed as repeated sub-events, not as cyclic edges.

func (LeadsToDagCheck) Code() string

func (LeadsToDagCheck) Description() string

func (LeadsToDagCheck) Run(g *model.IpmGraph) []Finding

type LeadsToWholeEventCheck ¶

type LeadsToWholeEventCheck struct{}

LeadsToWholeEventCheck implements IPMV2.9: a leads-to edge between events must connect WHOLE (outermost) events, never a sub-part.

Leads-to expresses temporal flow between whole events. If an event Y is part-of some event Z (directly or transitively), then Y is a sub-part of Z and a leads-to edge with Y as its source OR target is wrong: the flow should connect Z — the outermost part-of ancestor — not its sub-part Y.

Motivation (abstract late-side-branch fixture): the chain `e1 --> e2 --> e3` is wrong when `e2 --::P--> e8` (e2 is part-of e8). The correct model is `e1 --> e8 --> e3`, because e2 is only a component of the whole event e8.

Detection: for each LeadsTo edge A → B, resolve each endpoint to its outermost whole event. If both resolve to the SAME whole, the edge sequences sibling sub-events inside one container — legitimate (IPMV2.7 recommends it), so it is skipped. Otherwise the edge crosses a container boundary: flag each endpoint that is a sub-part and resolve its outermost part-of ancestor for the message. Applied transitively (sub-sub-parts).

Severity: warning (matches the IPMV2.x temporal-order family).

func (LeadsToWholeEventCheck) Code() string

func (LeadsToWholeEventCheck) Description() string

func (LeadsToWholeEventCheck) Run(g *model.IpmGraph) []Finding

type PartOfDagCheck ¶

type PartOfDagCheck struct{}

PartOfDagCheck implements IPMV2.1: containment must be acyclic. `A --::P--> B --::P--> C --::P--> A` makes A its own ancestor, which is nonsensical in SST.

func (PartOfDagCheck) Code() string

func (PartOfDagCheck) Description() string

func (PartOfDagCheck) Run(g *model.IpmGraph) []Finding

type RedundantParentParticipationCheck ¶

type RedundantParentParticipationCheck struct{}

RedundantParentParticipationCheck implements IPMV1.4: when a thing X is part-of a parent thing Y (X --::P--> Y, both things) and X also participates in event E (X --> E, part-of), then Y's own participation in E (Y --> E) is implicit by SST convention and should not be declared explicitly. Only the most granular thing carries the explicit thing-in-event edge; the parent thing's involvement follows.

See SKILL.md "Implicit Relations via Part-Of":

configured prefix prefix::a --::P--> config file configFile::a
prefix --> Load source-prefix configuration ::e loadPrefix::a

In the model above, configFile --> loadPrefix would be redundant because prefix part-of configFile + prefix in loadPrefix already places configFile inside loadPrefix's involvement by SST convention.

Severity: warning. The graph is not structurally invalid, but the explicit parent-thing edge is noise that obscures which sub-thing actually participates.

func (RedundantParentParticipationCheck) Code() string

func (RedundantParentParticipationCheck) Description() string

func (RedundantParentParticipationCheck) Run(g *model.IpmGraph) []Finding

type SelfLoopCheck ¶

type SelfLoopCheck struct{}

SelfLoopCheck implements IPMV1.1: an edge whose source and target are the same node violates SST locality (an agent cannot relate to itself).

func (SelfLoopCheck) Code() string

func (SelfLoopCheck) Description() string

func (SelfLoopCheck) Run(g *model.IpmGraph) []Finding

type Severity ¶

type Severity string

Severity classifies a finding.

const (
	SeverityError   Severity = "error"
	SeverityWarning Severity = "warning"
	SeverityInfo    Severity = "info"
)

type SiblingOrderingCheck ¶

type SiblingOrderingCheck struct{}

SiblingOrderingCheck implements IPMV2.7: when two or more events are direct sub-events of the same parent event (via PartOf), the graph should declare a leads-to ordering between them — direct, transitive, or via a shared LeadsTo predecessor/successor (fan-out partial order). Otherwise the temporal sequence among siblings is unknown.

Exemption: a NearTo edge between two siblings marks them as intentionally parallel; the pair is skipped.

The rule applies recursively at every level of containment.

func (SiblingOrderingCheck) Code() string

func (SiblingOrderingCheck) Description() string

func (SiblingOrderingCheck) Run(g *model.IpmGraph) []Finding

type StrandedEventCheck ¶

type StrandedEventCheck struct{}

StrandedEventCheck implements IPMV4.5.4: an event with no participants, no sub-events, no LeadsTo edges in/out, and no Expresses to any concept. Such an event doesn't *do* anything in the graph.

func (StrandedEventCheck) Code() string

func (StrandedEventCheck) Description() string

func (StrandedEventCheck) Run(g *model.IpmGraph) []Finding

type StrandedThingCheck ¶

type StrandedThingCheck struct{}

StrandedThingCheck implements IPMV4.5.3: a thing with no part-of edge to any event/thing and no expresses edge to any concept is detached from the model. Usually a typo or an in-progress draft.

func (StrandedThingCheck) Code() string

func (StrandedThingCheck) Description() string

func (StrandedThingCheck) Run(g *model.IpmGraph) []Finding

type TypePairCheck ¶

type TypePairCheck struct{}

TypePairCheck implements IPMV1.3: every SST edge must match the γ(3,4) type-pair table.

LeadsTo:   event   → event
PartOf:    event   → event
           thing   → event
           thing   → thing
Expresses: event   → event
           event   → concept
           thing   → concept
           concept → concept
NearTo:    event   --- event       (undirected, same-type only)
           thing   --- thing
           concept --- concept

Anything else is a type-pair violation.

func (TypePairCheck) Code() string

func (TypePairCheck) Description() string

func (TypePairCheck) Run(g *model.IpmGraph) []Finding

type UndecidedKindCheck ¶

type UndecidedKindCheck struct{ Strict bool }

UndecidedKindCheck flags nodes whose kind is Unresolved (grey — kind not yet pinned down). In the default draft mode each is a warning ("confirm this kind"); in Strict mode — the publish gate — each is an error, since a finished diagram should carry no undecided kinds.

Type-pair validity for edges touching such nodes is handled separately by TypePairCheck, which substitutes the node's primary candidate.

func (UndecidedKindCheck) Code() string

func (UndecidedKindCheck) Description() string

func (c UndecidedKindCheck) Run(g *model.IpmGraph) []Finding