Skip to content

Accept Behavior Annex loops without an iterator classifier 🤖 - #3227

Merged
lwrage merged 5 commits into
masterfrom
3173_optional_loop_iterator_classifier
Sep 15, 2026
Merged

lwrage merged 5 commits into
masterfrom
3173_optional_loop_iterator_classifier

Conversation

@lwrage

@lwrage lwrage commented Sep 14, 2026

Copy link
Copy Markdown
Contributor

Fixes #3173

Cause and correction

AS5506/3 Rev. A D.6 writes the iterator of a for and of a forall construct as
element_identifier [ : data_unique_component_classifier_reference ], and the standard's own BA_example4 omits the
classifier (for(d in int_set)). BehaviorAnnex.xtext required the colon and the classifier, so every loop that left
them out was a syntax error. The colon and classifier are now an optional group.

An iterator without a written classifier takes the type D.6's semantics give it: an integer range makes it an integer,
an input event data port makes it the port's data classifier, and a data component array makes it the classifier of the
array's elements, which for a Data Model array is the array's base type.

Translation resolves that classifier from the iterated values, the way it resolves every other name in the annex, and
before the loop body, because a data element reached through the iterator (entry.left) needs the iterator's own type
to resolve. The strict model carries the type, so getClassifier, the type holder, the data representation, and the
resolver's data-element lookup all read the one field rather than each inferring it. An integer range is the exception,
having no classifier to name: its universal integer comes from the loop, exactly as a port count value's does.

Resolving it on demand against each caller's container was considered and rejected. The answer does not vary with the
component that asks: Data_Representation and Base_Type are read from the data classifier of the iterated element,
the constraining classifier of an unbound prototype is read from the prototype, and every path hands the checker the
annex's own owner. The declarative limits below are the same either way, and are pre-existing.

Two checks moved as a consequence. AadlBaTypeChecker.checkForOrForAll could no longer tell an omitted classifier from
a written one of another category, and resolution would have silently supplied a type for the second; it now reports only
an iterator that ends up with no type at all. The requirement that a written classifier be a data classifier moved to
BehaviorAnnexValidator.checkIteratorClassifiers, which reports it on the reference as written and gates the strict
checkers the way the other unrepresentable spellings do. For that case the diagnostic changes from
iterative variable data classifier is not resolved on the whole loop to
'helper' is not a data classifier: a for or forall iterator can only name a data component classifier on the
classifier reference.

No metamodel change was needed: a single-valued assignment is already optional in the derived Ecore, so the
regeneration touched only the runtime and content-assist parsers, the grammar access, the semantic sequencer, and the
.xtextbin.

Regression model and assertions

ba/org.osate.ba.tests/models/issue3173/Issue3173.aadl writes both constructs without a classifier over each of the
three element_values the production admits — an integer range, an input event data port, and a data component array in
both the AADL core (history : data Base_Types::Integer [3]) and the Data Model (pairs : Pairs) spelling — and keeps a
written classifier as the positive control. Every loop body names its iterator as the first operand of an arithmetic
expression, because the applicable operator is selected by the type of that operand alone; an iterator left untyped is
therefore reported even while the conformance check between the two operand types is disabled (#3199). The pre-fix
baseline of the second fixture records exactly that: There is no applicable operator "+" for type unknown.

Issue3173Test asserts:

  • both constructs parse and validate with no issue;
  • the type of each iterator, as AadlBaUtils.getTypeHolder reports it: step -> Integer <no classifier>,
    sample -> Integer Base_Types::Integer, element -> Integer Base_Types::Integer, entry -> Struct Issue3173::Pair,
    and the written control typed -> Integer Base_Types::Integer;
  • each read of an iterator inside its loop carries that same type, including both reads through entry.left and
    entry.right;
  • a copy of the annex serializes the classifier-free loops through the registered unparser and reparses to the same
    types, which is what exercises the regenerated sequencers rather than the retained node model.

NonDataIteratorClassifier.aadl holds the other side: for (step : helper in 0 .. 2) and
forall (other : helper.impl in 0 .. 2) name a thread type and a thread implementation and must stay rejected, so that
making the classifier optional cannot turn a rejected declaration into one whose type is resolved from the iterated
values instead.

The conformance expectation optionalLoopClassifierIsAcceptedByTheStandard (G09) is activated in the regression commit
and passes with the fix, so OptionalForClassifier.aadl and OptionalForallClassifier.aadl are now clean.

Validation

Run outside the sandbox, from the repository root.

  • Regression before the fix: -Dtest='Issue3173Test,BehaviorAnnexConformanceTest'Issue3173Test 5 tests, 5
    failures, each on the syntax error at the omitted colon or on the pre-fix diagnostics of the second fixture;
    BehaviorAnnexConformanceTest 1 failure on the activated expectation.
  • Same selection after the fix: Issue3173Test 5 tests, 0 failures; BehaviorAnnexConformanceTest 12 tests, 0
    failures, 1 skip (unaryPlusIsRejectedByTheStandard, Reject unary plus in Behavior Annex expressions 🤖 #3170).
  • Goldens refreshed with -Dosate.ba.tests.regenerate=true -Dtest='BehaviorAnnexCharacterizationTest,BehaviorAnnexValidatedDiagnosticsTest',
    then rerun without the flag. Only the four affected fixtures changed, across diagnostics,
    diagnostics-validated, positions, and resolved-model; no unparse golden and no other corpus model moved. A
    second regeneration after the change described above under "considered and rejected" produced no golden churn at all,
    which is the check that where the classifier is resolved is not observable in the recorded models.
  • Clean root reactor, all tests, -Dtycho.localArtifacts=ignore: BUILD SUCCESS in 2:13, no failures or errors anywhere
    in the reactor. git diff --check clean apart from the trailing whitespace the Xtext generator itself emits into
    src-gen, which is left as generated.

Dependencies and merge order

None. The branch is based on 0def9cf962, which is the current tip of master, and it does not depend on any unmerged
PR.

Residual risk

  • The resolution is declarative, and its limits are pre-existing: the same lookup already types the iterated values of a
    loop whose classifier is written, so making the classifier optional inherits them rather than introducing them.
    Data_Representation and Base_Type are looked up on the data classifier of the iterated element, so an association
    on the element itself is not consulted, contained or not. Iterated values typed by a prototype resolve to the
    prototype's constraining classifier: a legal model that declares buffer : data element_type [3] under
    element_type : data Base_Types::Integer and binds element_type => data Base_Types::Float on one subcomponent and
    Base_Types::Integer on another validates with no diagnostic, and the iterator is typed Base_Types::Integer for
    both, because a prototype bound on a subcomponent is not reachable from the classifier the checker is given. Closing
    that needs an instance-context resolution, which is the part of Allow omitted classifiers in Behavior Annex for and forall loops 🤖 #3173's comment that remains open and is recorded in
    the G09 row of ba/doc/conformance.md.
  • Type conformance between the iterator and the iterated values is still not enforced, because
    AdaLikeDataTypeChecker.conformsTo returns true unconditionally (Behavior Annex type conformance is disabled, so no type mismatch is reported 🤖 #3199). The iterator types this PR establishes are
    what that check will compare once it is enabled, so the fixtures are chosen to be correct under it.
  • Iterating an iterator is unaffected and still broken: a nested loop over an array of arrays crashes translation with a
    ClassCastException, which I confirmed at 0def9cf962 with written classifiers and filed as Behavior Annex for and forall crash when the iterated values name a loop iterator 🤖 #3226. It is
    independent of this change and out of scope here.
  • checkIteratorClassifiers gates the strict checkers for a subclause with a non-data iterator classifier, so such a
    subclause now reports that one message instead of the strict findings it used to accumulate. That is the same gating
    the internal-port, timeout-reset-port, and array-size checks already apply.

🤖 Generated with Claude Code

AS5506/3 Rev A D.6 writes the iterator of a for and of a forall construct as
element_identifier [ : data_unique_component_classifier_reference ], so the
classifier is optional, and the standard's own BA_example4 omits it. The
grammar requires it, so every loop that leaves it out is a syntax error.

Issue3173.aadl writes both constructs without a classifier over each of the
three element_values the production admits: an integer range, an input event
data port, and a data component array in both the AADL core and the Data Model
spelling. A written classifier is kept as the positive control. Each loop body
names its iterator as the first operand of an arithmetic expression, because
the applicable operator is selected by the type of that operand alone; an
iterator left without a type is therefore reported even while the conformance
check between the two operand types is disabled. That is what the pre-fix
baseline of NonDataIteratorClassifier.aadl records beside the existing
"iterative variable data classifier is not resolved" finding.

The assertions require the strict model to carry the type the iterated values
determine rather than an unresolved iterator: an integer range makes the
iterator a universal integer with no classifier, the way a port count value is
one, while a port and an array each supply the classifier of their own
elements, which for a Data Model array is the array's base type. Reads of the
iterator inside the loop must carry that same type, and a copy of the annex
must serialize the classifier-free loops and reparse to the same types.

NonDataIteratorClassifier.aadl fixes the other side: a written classifier of a
category other than data must stay rejected, so that making the classifier
optional cannot turn a rejected declaration into one whose type is inferred
from the iterated values instead.

Activate the existing conformance expectation for the two optional-classifier
fixtures while preserving the pre-fix corpus baselines.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
AS5506/3 Rev A D.6 writes the iterator of a for and of a forall construct as
element_identifier [ : data_unique_component_classifier_reference ], and the
standard's own BA_example4 omits the classifier. Make the colon and classifier
optional in the grammar, and give an iterator that has none the type D.6's
semantics give it: an integer range makes it an integer, an input event data
port makes it the port's data classifier, and a data component array makes it
the classifier of the array's elements, which for a Data Model array is the
array's base type.

Translation resolves that classifier from the iterated values, the way it
resolves every other name in the annex, and before the loop body, because a
data element reached through the iterator needs the iterator's own type to
resolve. The strict model therefore carries the type, and getClassifier, the
type holder, the data representation, and the resolver's own data-element
lookup all read the one field instead of each inferring it. An integer range is
the exception, having no classifier to name: its universal integer comes from
the loop, exactly as a port count value's does.

Resolving it on demand against the container of each caller was considered and
rejected. The answer does not vary with the component that asks: the Data Model
values and the constraining classifier of an unbound prototype are read from
classifiers, and every path hands the checker the annex's own owner. The
declarative limits are unchanged either way, and are pre-existing, since the
same lookup already types the iterated values of a loop whose classifier is
written.

The strict type check that the iterator has a resolved data classifier could no
longer distinguish an omitted classifier from a written one of another
category, and resolution would have silently supplied a type for the second.
It now reports only an iterator that ends up with no type, and the requirement
that a written classifier be a data classifier moves to the declarative
validator, which reports it on the reference as written and gates the strict
checkers the way the other unrepresentable spellings do. That replaces
"iterative variable data classifier is not resolved" for this case with a
message naming the classifier and the rule.

Regenerate the runtime and content-assist grammars, refresh the four affected
characterization fixtures across the diagnostics, positions, and resolved-model
goldens, and update the conformance report. No metamodel change was needed: a
single-valued assignment is already optional in the derived Ecore.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@lwrage
lwrage force-pushed the 3173_optional_loop_iterator_classifier branch from a286891 to 8845f3a Compare September 14, 2026 19:53
@lwrage
lwrage merged commit cdf08b0 into master Sep 15, 2026
1 check passed
@lwrage
lwrage deleted the 3173_optional_loop_iterator_classifier branch September 15, 2026 14:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Allow omitted classifiers in Behavior Annex for and forall loops 🤖

2 participants