Summary
Behavior Annex transition priorities accept based and exponent-form integer literals without a diagnostic. AS5506/3 Rev. A D.3 defines behavior_transition_priority ::= numeral, which is narrower than the general integer-literal production.
The grammar uses INTEGER_LIT for priorities, and the validator checks numeric representability without checking the permitted numeral spelling.
Audit finding A15, reproduced on ed1e5396486e0b16c55a9bb4cd51ce1f55353b17 during the 2026-09-19 audit against AS5506/3 Rev. A.
Reproduction
Two separately executed fixtures use the following transition prefixes:
Both produce zero diagnostics. The complete model below is the based-literal case; the exponent case has the same declarations and action block.
External AADL fixture used in the audit (license header omitted):
package Audit_BasedPriority
public
with Base_Types;
subprogram routine end routine;
subprogram writer
features result: out parameter Base_Types::Integer;
end writer;
abstract host
features
a: in event port;
b: in event port;
c: in event port;
inp: in event data port Base_Types::Integer;
incoming: in data port Base_Types::Integer;
outp: out event data port Base_Types::Integer;
rpc: provides subprogram access routine;
end host;
abstract implementation host.i
annex behavior_specification {**
variables
v: Base_Types::Integer := 0;
flag: Base_Types::Boolean := true;
arr[2]: Base_Types::Integer;
states st: initial state; done: final state;
transitions t[16#F#]: st -[]-> done { v := 1 & flag := false };
**};
end host.i;
end Audit_BasedPriority;
The audit parsed this external file and validated it with BehaviorAnnexInjectorProvider and ValidationTestHelper. Its companion with the annex removed had zero core-AADL diagnostics. Strict-model observations used BehaviorAnnexUtil.getStrictModel. These are recorded execution results from the audit, not a new test run performed while filing this issue.
Expected behavior
Accept numeral priorities and reject based/exponent spellings, or explicitly diagnose any deliberately retained compatibility extension. Nonstandard forms must not remain silently accepted as standard syntax: issue a warning. Preserve valid decimal numeral priorities and existing numeric-representability diagnostics.
Relevant code
Closed #3175 concerns preserving numeric literal values generally, and #3183 concerns priorities on otherwise transitions. Neither tracks the narrower lexical production for a normal transition priority.
Summary
Behavior Annex transition priorities accept based and exponent-form integer literals without a diagnostic. AS5506/3 Rev. A D.3 defines
behavior_transition_priority ::= numeral, which is narrower than the general integer-literal production.The grammar uses
INTEGER_LITfor priorities, and the validator checks numeric representability without checking the permitted numeral spelling.Audit finding A15, reproduced on
ed1e5396486e0b16c55a9bb4cd51ce1f55353b17during the 2026-09-19 audit against AS5506/3 Rev. A.Reproduction
Two separately executed fixtures use the following transition prefixes:
Both produce zero diagnostics. The complete model below is the based-literal case; the exponent case has the same declarations and action block.
External AADL fixture used in the audit (license header omitted):
The audit parsed this external file and validated it with
BehaviorAnnexInjectorProviderandValidationTestHelper. Its companion with the annex removed had zero core-AADL diagnostics. Strict-model observations usedBehaviorAnnexUtil.getStrictModel. These are recorded execution results from the audit, not a new test run performed while filing this issue.Expected behavior
Accept numeral priorities and reject based/exponent spellings, or explicitly diagnose any deliberately retained compatibility extension. Nonstandard forms must not remain silently accepted as standard syntax: issue a warning. Preserve valid decimal numeral priorities and existing numeric-representability diagnostics.
Relevant code
BehaviorAnnex.xtext:72—BehaviorTransitionusespriority=INTEGER_LIT.BehaviorAnnexValidator.java:1018—checkTransitionPriority/integer-literal checking validates representability.Closed #3175 concerns preserving numeric literal values generally, and #3183 concerns priorities on otherwise transitions. Neither tracks the narrower lexical production for a normal transition priority.