[devin-ai-integration]

What and why

Documentation and manifest only; no runtime behaviour changes.

• Beta 2 constraint names. docs/project/constraint-manifest.json's specifications block now pins the KerML 1.1 Beta 2 and SysML v2.1 Beta 2 PDFs the pinned release ships (doc/1-Kernel_Modeling_Language.pdf, doc/2a-OMG_Systems_Modeling_Language.pdf, "Release 2026-07", SHA-256 recorded) instead of KerML 1.0 formal/26-03-01 / SysML 2.0 formal/26-03-02, and formal-constraints -update re-derived every spec.name and spec-sourced row from those texts. The validation-rule rows of docs/project/spec-compliance.md (the four Xpect-suite sections and the validate* rows elsewhere) show the Beta 2 name first and the pilot validator's name second where they differ (validateFeatureEndMultiplicity (pilot validateFeatureEndFeatureMultiplicity), 32 such names), and a check the Beta 2 text does not state is marked pilot-only check (42 names, mostly the validate…UsageType family, which Beta 2 states only as check…Specialization implied specializations). The four section headers no longer claim the rows came from the reference's validator source alone.
• Rows added for the Beta 2 constraints the map lacked, each probed with bin/sysml -validate and the pinned pilot validator rather than guessed: validateAttributeDefinitionFeatures / validateAttributeUsageFeatures (§8.3.7.2 / §8.3.7.3) and validateControlNodeIsComposite (§8.3.17.6) are satisfied by construction from the notation — §7.7.2 makes an attribute's owned features referential whether or not ref is written (both validators silent on attribute def SensorRecord { part sensor : Sensor; attribute reading : Real; }; api-json exports every such member isComposite: false), and the grammar gives a control node no ref prefix (ref fork f; is a syntax error in both parsers). validateUsageOwningType is not a constraint of either Beta 2 text: the SysML text uses the name only as an example of the naming convention (§8.3.1 "validateUsageOwningType"), neither §8.3 states it and the validation library does not declare it, so no row was added.
• State-machine rows re-grounded. The exit-action parameter row now rests on KerML 1.1 Beta 2 §7.4.11 Feature Values (a bound feature value makes the parameter equivalent to its value expression's result; a default applies when no other value is given), PSSM §8.5.5 as corroboration. The declared-but-not-performed behaviour row (action count : Count; in a part def, started only by an explicit start) now rests on SysML v2.1 Beta 2 §8.4.7.1 Parts Semantics — ownedActions is "a subset of Actions::actions and Objects::ownedPerformances that collects the values of the composite ActionUsages featured by a Part", while performedActions subsets Objects::enactedPerformances — and on Objects.kerml, where ownedPerformances subsets involvingPerformances, timeEnclosedOccurrences and suboccurrences but not enactedPerformances: the declared action is an owned performance within the part's lifetime, not one the part enacts, so creating the part starts nothing and this is not the part as performer until a start is performed; fUML §8.8.1 / §8.10.2 stay as corroboration. The concurrent-region-exit row keeps its 🧩 Extension (UML-derived) status: no Beta 2 clause mandates the order among sibling regions' exits (§7.18.2 says only that the states nested in a parallel state "can be performed concurrently", §8.4.14 says nothing about exit order, and StatePerformances.kerml orders a substate's exit only before its composite's own), so the row now says the SysML v2 specification is silent and PSSM §8.5.5 is the source.
• Real is now stated as a tool decision, not as faithful to the clause: KerML 1.1 Beta 2 §9.3.2.2.9 defines Real as the extended reals, ±∞ included; the implementation holds Real to finite IEEE 754 binary64 values and * is its only unbounded value, in multiplicity and LiteralInfinity positions. The row and the Function Library prose block say so; the row stays ⚠️ Approximate.
• seq#(i) out of range stays a typed error; the row carries no clause number to correct (its cite is the library declaration SequenceFunctions::'#', in index: Positive[1], which matches KerML 1.1 Beta 2 §9.4.14.2), so it is untouched.
• tools/census/formal/formal.go's page-footer pattern admits the Beta 2 footers (Kernel Modeling Language v1.1, Beta 2, Systems Modeling Language v2.1, Beta 2, Part 1) beside the formal ones; the fixture in formal_test.go exercises one.

Specification basis

KerML 1.1 Beta 2 §7.4.11 (Feature Values), §8.3 Constraints subsections, §9.3.2.2.9 (Real), §9.4.14.2 ('#'), Objects.kerml (ownedPerformances vs enactedPerformances); SysML v2.1 Beta 2 §7.7.2 (attribute members referential), §7.18.2 (parallel states performed concurrently — no exit-order mandate), §8.4.7.1 (Parts Semantics, ownedActions), §8.3.7.2 / §8.3.7.3 / §8.3.17.6, §8.3 Constraints subsections. The pinned pilot is treated as an oracle: where its validator name differs from the Beta 2 name the row says so, and where it checks something Beta 2 does not state the row says pilot-only check.

Rows and baselines that moved (every one, by object)

Compliance map (docs/project/spec-compliance.md):

• Region-exit concurrency row: text only (SysML v2 silent, PSSM the source), status 🧩 Extension (UML-derived) unchanged.
• Exit-action parameter row and declared-behaviour row: text only, status ✅ unchanged.
• Real row: text and status cell wording (⚠️ Approximate unchanged in marker).
• 36 validation rows re-keyed (text only; statuses unchanged); two rows added as above.

Census (docs/project/constraint-manifest.json, rendered in validation-constraints.md):

• validateAttributeDefinitionFeatures, validateAttributeUsageFeatures (pilot rows): ❔ unknown → ⛔ deliberate, with implementation semantics/annotations.go:Model.reflectiveFeatureFlags; export/composite.go:usageCompositeByDefault — the same recording as validateEnumerationDefinitionIsVariation, the existing "unobservable in text, derived by the model" row. Census line: 5 ⛔ → 7 ⛔, 49 ❔ → 47 ❔; reported count 163 of 217 unchanged.
• validateControlNodeIsComposite (spec-sourced row): ❔ unknown → ⛔ deliberate, implementation parser/behavior.go:Parser.parseActionMember.
• Pilot rows re-pointed at Beta 2 names: validateAssignmentActionUsageReferentIsTimeVarying (spec.name was the formal validateAssignmentActionUsage; Beta 2 uses the pilot's name) and validateSendActionUsagePayloadArgument (gains spec.name; Beta 2 renamed the formal validateSendActionParameters to the pilot's name).
• Spec-sourced rows renamed by Beta 2: checkIncludeUseCaseSpecialization → checkIncludeUseCaseUsageSpecialization, deriveMetadataAccessExpressionReferencdElement → deriveMetadataAccessExpressionReferencedElement, deriveOwningNamespace → deriveElementOwningNamespace; validateSendActionParameters dropped (it is the pilot row above). 40 spec-sourced rows refresh their checks/ocl text to the Beta 2 wording; no clause, status or implementation moved.
• Coverage table: 623 constraints stated, totals unchanged (258 KerML, 365 SysML); SysML pilot-named 86 → 87, spec-sourced 279 → 278, ❔ 238 → 236, implemented 41 unchanged.

No test, golden, oracle baseline or training_examples_expected.txt row moved.

How it was verified

• make docs-counts (runs doc-counts, doc-counts -check, validation-census -check, transformation-census -check and the census/referee unit tests): current, 217 constraints agree.
• go run -C tools ./cmd/formal-constraints -kerml build/spec-docs/pdf/1-Kernel_Modeling_Language.pdf -sysml build/spec-docs/pdf/2a-OMG_Systems_Modeling_Language.pdf -check: 623 constraints (KerML 258: 80/90/88; SysML 365: 128/145/92), 449 spec-sourced rows current.
• python3 scripts/check-doc-ids.py, scripts/check-doc-links.py (0 broken), scripts/check-doc-figures.py, python3 scripts/changelog.py check: pass. mkdocs build --strict: built.
• go test -C tools -count=1 ./... and go test -count=1 ./tests/hygiene/...: ok. gofmt -l tools empty, go vet clean.
• Probes by hand: bin/sysml -validate and build/pilot-sysml-validator/validate-sysml-batch on an attribute definition and usage with part/item/attribute members (both silent), bin/sysml -convert api-json on the same (six isComposite: false), and ref fork f; in an action (syntax error in both parsers).
• Dry-merge against PR chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529's head 9ca600a (pilot pin 2026-09) in a detached worktree: conflicts in the two section headers that name the pilot tag, the generated census summary lines and one row block (chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529 reworded the neighbouring connection/flow-end row); resolved by taking chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529's pilot tag and row and regenerating the summary (165 of 219 — 158 ✅, 7 ⚠️, 7 ⛔, 47 ❔), after which validation-census -check (219 constraints agree), make docs-counts and formal-constraints -check are green on the merged tree. Dry-merge against origin/develop (e5f9c3fca, which adds one view row to the compliance map) merges clean and make docs-counts is current on the merged tree. (check-doc-links.py reports third-party-notices.md → assets/landing/libavoid-js.LICENSE.txt missing in any fresh worktree, bare origin/develop included; the file is generated by the site build and present in a built checkout, so it is not from this change.)

Checklist

• make test and make lint pass locally — the documentation and tools gates above; the Go suite outside tools/ and tests/hygiene is untouched by this change
• Tests added or updated for the change (formal_test.go fixture footer)
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/compliance-beta2-constraint-names.changed.md
• baselines regenerated and make docs-counts run
• No internal work-item labels in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/bef6a11727134f2fa22bd2a2cbc65c03
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/bef6a11727134f2fa22bd2a2cbc65c03?variant=devin
Requested by: @HuiJun

[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]

✅ Devin Review: No Issues Found

Devin Review analyzed this PR and found no bugs or issues to report.