Behavior Annex accepts p'count, p'fresh, and p'updated on an outgoing port 🤖

[lwrage]

Summary

The three D.5 port-status values are accepted on any port the D.3 naming rules make visible, including an outgoing one, and no diagnostic is reported. AS5506/3 Rev. A defines all three only in terms of input freeze, so on an outgoing port none of them has a defined meaning:

• p'updated "returns true if some new values were received in port p since the last freeze of the port" (D.5).
• p'count "returns the number of elements available through the port variable … In the case of an event port or event data port it is the number of frozen elements" (D.5).
• p'fresh "returns true if the port variable contains a new value … In the case of a data port, this means that it has received a new value by the previous dispatch or freeze" (D.5).

The D.7 value_variable production nevertheless spells these three alternatives with port_name, in contrast to the incoming_port_name it spells for a plain port read and for a dequeue:

value_variable ::=
  incoming_port_name
| incoming_port_name ?
| incoming_subprogram_parameter_identifier
| incoming_port_prototype_name
| data_component_reference
| port_name ' count
| port_name ' fresh
| port_name ' updated

Neither the D.5 legality rules nor the D.7 legality rules narrow port_name. The grammar of the document is therefore looser than the semantics of the same section, and the document does not resolve the difference. This issue asks OSATE to adopt the semantics as the rule and reject the outgoing case, rather than to quote a legality rule from the document — there is no such rule to quote, and that should be stated in whatever diagnostic and comment the fix introduces.

The mechanism is simply that no check exists. AadlBaUtils.getDirectionType can supply the direction, but nothing calls it for a port value; PortCountValue, PortFreshValue, and PortUpdatedValue reach the strict-model checkers with the port they name and are never examined for direction.

Reproduction

The existing covering-syntax corpus already contains the case. ba/org.osate.ba.tests/models/covering_syntax/aadlBaTest002.aadl declares

outPortA : out event data port Base_Types::Float ;

and then reads two of the three values off it:

a -[]-> a {tab[outPortA'count] := 1};   -- line 230
a -[]-> a { bool1 := outPortA'fresh } ; -- line 237

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest002.txt is generated with the Behavior Annex validator registered and contains no finding at either line; its 17 entries are all operator-applicability and unused-with findings elsewhere in the model. p'updated behaves the same way now that #3171 is implemented, though no fixture writes that form on an outgoing port.

A smaller model reproducing it is a thread with a single out event port and one transition reading p'count, p'fresh, or p'updated.

Expected behavior

Each of p'count, p'fresh, and p'updated is reported when p is an outgoing port, on the port value as written, with a message that names the port and says the value is defined only for a port that is frozen on input. An incoming port and an in out port are both accepted, since both are frozen on input. A positive control in the same model keeps the incoming forms undiagnosed.

The three values must be treated alike. Enforcing this for one of them and not the others is what makes the current state hard to reason about.

Relevant code

• ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/BehaviorAnnex.xtext — ReferenceExpression and UnindexedReferenceExpression admit the suffixes after any Reference.
• ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java — toReferenceExpression builds PortCountValue, PortFreshValue, or PortUpdatedValue and copies the resolved holder into it without examining the port.
• ba/org.osate.ba/src/org/osate/ba/utils/AadlBaUtils.java — getDirectionType(Element) and getDirectionType(Target) already compute the direction and currently have no callers.
• Two candidate owners for the check. The strict model carries the port on all three classes, so AadlBaLegalityRulesChecker or AadlBaSemanticRulesChecker can reach it through AadlBaRulesCheckersDriver; alternatively BehaviorAnnexValidator can report it on the written reference, which is the idiom checkInternalPortUses and the Support timeout reset ports in Behavior Annex completion-relative timeouts 🤖 #3168 reset-port category check already use. The validator route gives the better source location when the reference does not resolve.

Test consequences

• ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest002.txt gains two entries. Every golden under expected/ is regenerated with -Dosate.ba.tests.regenerate=true; see ba/doc/conformance.md for the two-golden-set convention.
• CoveringSyntaxTest.aadlBaTest002 asserts 2.assertEquals(result.issues.size) but runs under Aadl2InjectorProvider, with no BA validator, so that count is unaffected.
• aadlBaTest002.aadl is a covering-syntax fixture rather than a legality fixture, so the two lines above should stay as they are and become recorded negative cases, with the new rule's positive and negative controls in a fixture of their own.
• The D.5 row of ba/doc/conformance.md and the G07 row both describe this gap and need updating when it closes.

Follow-up to #3171 and #3216, which implemented p'updated and deliberately left this unenforced so that the three values would keep behaving alike. Related to #3181 (G17), which covers direction and category checking for communication actions rather than for port-status values.