Enforce Behavior Annex condition restrictions across component categories and modes 🤖

[lwrage]

Fixes #3186

Cause and correction

AS5506/3 Rev. A D.3 restricts external conditions by component category and by in modes context, and defines how a descendant classifier inherits or replaces the Behavior Annex subclauses of an ancestor. None of that was enforced, and the one C4 mode-related consistency check read only dispatch conditions.

• AadlBaConsistencyRulesChecker gains the two D.3 condition rules the rules driver can decide from the strict model. The first rejects an external condition in a thread or a subprogram, naming the conditions that category uses instead; AadlBaRulesCheckersDriver checks it once per declaration, so a multi-source transition reports once. The second rejects a mixture of external and dispatch conditions out of one complete state of a device, reporting each condition of that state; the driver checks it once for the subclause because the rule compares the conditions of several transitions.
• D.3.(C4) now reads the triggers of an external condition as well as those of a dispatch condition. D.3 lets a component of any category other than thread and subprogram describe a mode transition with an external condition, and C4 exists to compare such a transition with the corresponding mode transition triggers; it previously returned false without a diagnostic for every condition that was not a dispatch condition. The comparison reads triggers without their logical operators, as it already did for dispatch conditions.
• BehaviorAnnexValidator rejects an external condition in a subclause with an in modes statement. Core AADL keeps that statement on the enclosing DefaultAnnexSubclause and the strict model does not carry it, so this rule is checked on the declarative model, where the complete-state mode-refinement rule already is. DeclarativeToStrictTranslator exposes hasInModes for it and defines canRefineModes as its negation, which changes no behavior.
• BehaviorAnnexUtil.getBehaviorAnnexSubclauses puts the D.3 inheritance and replacement rule on the public access path: the nearest classifier in the extends order that declares a subclause supplies all of them, and an implementation falls back to its type. A mode-selecting overload uses the in modes statement core AADL retains, matching mode names case insensitively because an applicable subclause can be declared by an ancestor. Mode applicability is not duplicated into the strict model: every consumer of getStrictModel already holds the subclause that carries it.
• Both new rules are cited by section, not by number. The numbered rule list these classes follow comes from the 0.94 draft, which orders the D.3 rules differently.

Not enforced: the subcomponent override rule. It selects which subclause a consumer interprets for an instance rather than constraining a declaration, so it belongs to the consumer that walks the instance hierarchy; ba/doc/conformance.md records that, along with the V05 row update.

Regression model and assertions

ba/org.osate.ba.tests/models/issue3186/ is a separate OSATE project with one fixture per restriction and one per access-path case. Issue3186Test (15 tests) parses each through ordinary embedded AADL validation, asserts no unrelated issues, and then asserts the exact diagnostic, with a positive control beside each rejection:

• threadCannotUseAnExternalCondition, subprogramCannotUseAnExternalCondition, and the control externalConditionIsAcceptedOutOfAnExecutionState (a process leaving an execution state on an event).
• deviceCannotMixExternalAndDispatchConditionsOutOfOneCompleteState and the control deviceMayLeaveACompleteStateOnExternalConditionsAlone.
• externalConditionTriggersMustMatchTheModeTransition, the C4 comparison for a mode-representing complete state.
• inModesSubclauseCannotUseAnExternalCondition and the control inModesSubclauseMayUseAnExecuteCondition.
• Access path: classifierSubclauseAppliesToItself, ancestorSubclauseAppliesToADescendantThatDeclaresNone, descendantSubclauseReplacesTheAncestorOne, typeSubclauseAppliesToAnImplementationThatDeclaresNone, everyModalSubclauseOfTheClassifierApplies, modalSubclausesAreSelectedByMode, subclauseWithoutInModesIsSelectedInEveryMode.

The subprogram fixture triggers on an outgoing event port because core AADL admits no other event port on a subprogram, so no subprogram can name the incoming port the D.3 event_trigger production asks for; the rule constrains the form of the condition rather than its triggers.

Two existing tests are touched:

• BehaviorAnnexGrammarTest.parseAcceptedBehaviorAnnexCorpus matched a subclause by its annex text followed by a semicolon, so it silently skipped every subclause with an in modes statement, and where another subclause followed one it paired their delimiters across the two. The pattern now accepts the statement, which brings the new ModalSubclauses.aadl and the existing InModes.aadl under that test.
• The corpus goldens record the new fixtures in both BA-validator registration states. The one existing golden that changes is issue2147, whose thread group leaves a mode-representing complete state on an external condition while declaring no mode transition: with C4 now reading external condition triggers, that model reports the finding its dispatch equivalent already produced.

Validation

Tests were run from the repository root with the local profile before the branch was pushed; all results below are from that run.

• ba/org.osate.ba.tests: 174 tests, 0 failures, 0 errors, 0 skipped (Issue3186Test contributes 15).
• ba/org.osate.xtext.aadl2.ba.tests: 15 tests, 0 failures, 0 errors.
• core/org.osate.core.tests: 876 tests, 0 failures, 0 errors.

The clean root-reactor build documented in CLAUDE.md was not carried through to completion on this branch at the user's direction; CI on this PR is the first complete build of it.

Dependencies and merge order

None. The branch is based on 537f7ed139, already on master, and does not depend on any unmerged PR.

Residual risk

• issue2147's golden change is a behavior change for existing models: any component of a category other than thread or subprogram that leaves a mode-representing complete state on an external condition without a corresponding mode transition now reports the C4 finding. That is the intended effect of the rule, but it can surface new diagnostics in existing user models.
• The device condition-mixing rule is checked once per subclause and reports each condition of the offending complete state, so a model with several offending states reports several diagnostics per subclause.
• The mode-selecting overload of getBehaviorAnnexSubclauses is new API on BehaviorAnnexUtil; no existing consumer calls it yet, so it is exercised only by the regression test.
• The subcomponent override rule remains unenforced by design, recorded in ba/doc/conformance.md.
• External condition triggers that are not incoming event ports are silently dropped or accepted 🤖 #3232, opened while implementing this, covers an external-condition trigger that is not an incoming event or event data port being dropped in translation or kept despite its direction, in either case without a diagnostic. It is out of scope here.

🤖 Generated with Claude Code