Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions ba/doc/conformance.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato
| D.3: behavior specification | Variables, grouped states, state kinds, named/prioritized and multiple-source transitions, execute conditions, and dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions (G01), complete external-condition expressions (G02), naming and otherwise-transition rules (V01 and V02), and complete-state mode binding (G14) were absent and are now implemented; multiple subprogram final states are rejected unconditionally, and several consistency obligations lack demonstrated enforcement. |
| D.4: thread dispatch | Dispatch conjunction/disjunction, `stop`, bare timeout, timeout with a duration, and an unparenthesized frozen-port list. Selected timeout/stop checks exist. | Partial. Required frozen-list parentheses were missing (G03) and timeout reset ports absent (G04), both since fixed. Full protocol/trigger compatibility and core-property consistency are not demonstrated. |
| D.5: component interactions | Port send/dequeue/freeze, count/fresh/updated, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` was absent (G07), internal events were represented incorrectly (G10), and outgoing ports were accepted for the three input-freeze status values, all since fixed; call-signature and remaining communication direction/category checks need additional coverage. Input/output timing consistency is not established. |
| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, explicit-type loops, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers are missing; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. |
| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, loops with a written or an omitted iterator classifier, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers were missing (G09) and are now implemented; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. |
| D.7: expressions | Boolean/numeric/string syntax, arithmetic/relational/logical operators, property references, indexing, and operator applicability checks per operand data representation. | Partial, with semantic preservation defects. Operand consistency between the two operands is not checked, only applicability of the operator to the first one (G18). Short-circuit logical operators, including in external conditions, and `updated` are now supported (#3166, #3169, and G07, since fixed), and value-expression precedence, association, admissible forms, and grouping now follow the document (G13, since fixed); numeric translation differs from the document, unary plus remains accepted as an extension but now produces a compatibility warning (G06), and initialization analysis is not demonstrated. |
| D.8: synchronization | `Behavior_Properties::Subprogram_Call_Protocol` declares HSER/LSER/ASER and defaults to HSER, matching the supplied document. A client/server example exists. | Property definition conforms. Enforcement of the two LSER/ASER legality rules and execution of the protocols are not established. |

Expand All @@ -80,7 +80,7 @@ All ten categories appear in [BehaviorAnnexConformanceTest](../../ba/org.osate.b
| G06 | D.7 `unary_adding_operator` contains only minus. | `UnaryExpression` explicitly accepts plus. **Addressed by [#3170](https://github.com/osate/osate2/issues/3170) with a deliberate compatibility policy:** the declarative validator reports a warning on the unary `+` token while the grammar and strict-model translation continue to accept and preserve the extension. `UnaryPlus.aadl` has an exact validated-diagnostics golden, and the active expectation asserts the warning code, message, severity, and location. | Deliberate warned extension rather than strict grammar rejection. |
| G07 | D.5 port-service table and D.7 `value_variable` include `p'updated`. | `ReferenceExpression` and `UnindexedReferenceExpression` permit only count/fresh suffixes. `PortUpdated.aadl` records a syntax error. | Source-confirmed missing operation. **Addressed by [#3171](https://github.com/osate/osate2/issues/3171):** both rules gained the suffix, the strict model a `PortUpdatedValue` beside `PortCountValue` and `PortFreshValue`, and the type rules the universal Boolean those two already establish, so the value carries no data classifier and applies to a data-less event port. The generated sequencers emit it, so it round-trips. **The follow-up direction gap is addressed by [#3217](https://github.com/osate/osate2/issues/3217):** the validator reports `count`, `fresh`, and `updated` on an outgoing port and accepts incoming and bidirectional ports, which are frozen on input. This deliberately enforces the semantics of the three D.5 definitions; neither the D.5 nor the D.7 legality rules states the restriction, and the diagnostic says so. |
| G08 | D.7 component-element property references include `self`. | The translator now recognizes the text `self`, so the old expected “not found” diagnosis is stale. However, the strict golden for `SelfPropertyReference.aadl` contains `ClassifierFeaturePropertyReference.component : BehaviorVariableHolder element=<null>`. The source returns an empty holder before recording the owner against the complete prefix reference. | Partial syntactic/name recognition, still a source-confirmed translation gap. **Step 1 made it visible:** with the validator registered the fixture reports `resolved behavior annex holder has no element`, so the finding is now asserted rather than hidden behind an empty golden. **Addressed by [#3172](https://github.com/osate/osate2/issues/3172):** the resolver records the containing classifier against the complete prefix reference, so `self#Priority` becomes a `ClassifierPropertyReference` on that classifier, and its property name resolves to the classifier's own association. No holder can carry a classifier, so a bare `self` remains an unresolved holder in the positions that need a value, where D.7 does not admit it. |
| G09 | D.6 `for` and `forall` make `: data_unique_component_classifier_reference` optional. | `ForStatement` requires the colon and classifier. Both optional-classifier fixtures record syntax errors. | Source-confirmed missing syntax; inferred iterator types also need semantic support. |
| G09 | D.6 `for` and `forall` make `: data_unique_component_classifier_reference` optional. | `ForStatement` requires the colon and classifier. Both optional-classifier fixtures record syntax errors. | Source-confirmed missing syntax; inferred iterator types also need semantic support. **Addressed by [#3173](https://github.com/osate/osate2/issues/3173):** the grammar makes the colon and classifier optional, and the iterator then takes the type the D.6 semantics give it: an integer range makes it a universal integer, which no data classifier denotes and which the type holder of an iterator now reports the way a port count value already did, while a port or a data component supplies the classifier of its own elements, which for a Data Model array is the array's base type. Translation resolves the omitted classifier from the iterated values, the way it resolves every other name in the annex, so the strict model carries the iterator's type and no reader has to infer it: `getClassifier`, the type holder, the data representation, and the resolver's own data-element lookup through an iterator all read the one field. The integer range is the exception, having no classifier to resolve, so its universal integer comes from the loop, exactly as a port count value's does. An instance-context resolution was considered and rejected: the answer does not vary with the component that asks, because the properties and the prototype constraint below are read from classifiers and the checker is handed the annex's own owner in every path. The check that the iterator has a resolved data classifier could no longer tell an omitted classifier from a written one of another category, so the requirement that a written classifier be a data classifier moved to the declarative validator, which reports it on the reference as written. What is still outstanding is the part the standard makes instance-dependent, and it is pre-existing: the same lookup already types the iterated values of a loop whose classifier is written, so making the classifier optional inherits it rather than introducing it, and resolving it at translation rather than on demand does not change it. `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, not a different declarative container. |
| G10 | D.5–D.6 allow internal ports as assignment targets and internal-event send actions. | The internal-action diagnostics golden is now empty, but its strict golden maps the event-data target to `DataSubcomponentHolder [EventDataSource]` and the event send to `SubprogramCallAction` with an `EventSource` proxy. `createHolder` has no internal-feature specialization and falls back to a data-subcomponent holder. | Source-confirmed incorrect representation; acceptance is not correct internal-event support. Step 1 confirmed that on `master` the fixture is accepted with zero diagnostics even with the validator registered, so `internalPortActionsAreAcceptedByTheStandard` was left skipped with that reason recorded: it would have passed for the wrong reason, and closing #3174 needed a strict-model assertion. That expectation is active now that the representation is correct. **Addressed by [#3198](https://github.com/osate/osate2/pull/3198):** `InternalPortHolder`, `EventSourceHolder`, `EventDataSourceHolder`, and `InternalPortSendAction` were added. Running the checkers over the fixture on that branch also showed that this row understated the defect: with the validator registered, the resolver rejected the legal actions with `getClassifier : EventDataSourceImpl is not supported yet`. |

Current output evidence is in [expected/diagnostics](../../ba/org.osate.ba.tests/expected/diagnostics) and [expected/resolved-model](../../ba/org.osate.ba.tests/expected/resolved-model), using filenames beginning `org.osate.ba.tests_models_characterization_conformance_`.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +0,0 @@
error | linking | 17 | 15 | 1 | Couldn't resolve reference to BehaviorState 'i'.
error | linking | 17 | 6 | 5 | Couldn't resolve reference to BehaviorState 'value'.
error | syntax | 16 | 12 | 2 | mismatched input 'in' expecting ':'
error | syntax | 17 | 12 | 2 | mismatched input ':=' expecting '-['
error | syntax | 17 | 6 | 5 | mismatched input 'value' expecting '}'
error | syntax | 18 | 5 | 1 | mismatched input '}' expecting '-['
Original file line number Diff line number Diff line change
@@ -1,6 +0,0 @@
error | linking | 17 | 15 | 1 | Couldn't resolve reference to BehaviorState 'i'.
error | linking | 17 | 6 | 5 | Couldn't resolve reference to BehaviorState 'value'.
error | syntax | 16 | 15 | 2 | mismatched input 'in' expecting ':'
error | syntax | 17 | 12 | 2 | mismatched input ':=' expecting '-['
error | syntax | 17 | 6 | 5 | mismatched input 'value' expecting '}'
error | syntax | 18 | 5 | 1 | mismatched input '}' expecting '-['
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
error | semantic | 49 | 29 | 6 | 'helper' is not a data classifier: a for or forall iterator can only name a data component classifier
error | semantic | 54 | 33 | 11 | 'helper.impl' is not a data classifier: a for or forall iterator can only name a data component classifier
Original file line number Diff line number Diff line change
@@ -1,6 +0,0 @@
error | linking | 17 | 15 | 1 | Couldn't resolve reference to BehaviorState 'i'.
error | linking | 17 | 6 | 5 | Couldn't resolve reference to BehaviorState 'value'.
error | syntax | 16 | 12 | 2 | mismatched input 'in' expecting ':'
error | syntax | 17 | 12 | 2 | mismatched input ':=' expecting '-['
error | syntax | 17 | 6 | 5 | mismatched input 'value' expecting '}'
error | syntax | 18 | 5 | 1 | mismatched input '}' expecting '-['
Original file line number Diff line number Diff line change
@@ -1,6 +0,0 @@
error | linking | 17 | 15 | 1 | Couldn't resolve reference to BehaviorState 'i'.
error | linking | 17 | 6 | 5 | Couldn't resolve reference to BehaviorState 'value'.
error | syntax | 16 | 15 | 2 | mismatched input 'in' expecting ':'
error | syntax | 17 | 12 | 2 | mismatched input ':=' expecting '-['
error | syntax | 17 | 6 | 5 | mismatched input 'value' expecting '}'
error | syntax | 18 | 5 | 1 | mismatched input '}' expecting '-['
Original file line number Diff line number Diff line change
@@ -1,13 +1,20 @@
annex[0] owner=OptionalForClassifier::operation
(BehaviorActionBlock, <null>, 352, 25)
(AssignmentAction, <null>, 383, 10)
(BehaviorActionBlock, <null>, 352, 52)
(BehaviorAnnex, behavior_specification, 216, 189)
(BehaviorIntegerLiteral, <null>, 368, 1)
(BehaviorIntegerLiteral, <null>, 373, 1)
(BehaviorState, finish, 294, 6)
(BehaviorState, start, 269, 5)
(BehaviorStateGroup, <null>, 269, 21)
(BehaviorStateGroup, <null>, 294, 20)
(BehaviorTransition, <null>, 332, 45)
(BehaviorTransition, <null>, 383, 8)
(BehaviorTransition, <null>, 392, 13)
(BehaviorTransition, <null>, 332, 73)
(BehaviorVariable, value, 229, 5)
(BehaviorVariableGroup, <null>, 229, 27)
(ForStatement, <null>, 358, 19)
(ElementValues, <null>, 368, 6)
(ForStatement, <null>, 358, 41)
(Reference, <null>, 383, 5)
(Reference, <null>, 392, 1)
(ReferenceExpression, <null>, 392, 1)
(ReferenceSegment, i, 392, 1)
(ReferenceSegment, value, 383, 5)
Original file line number Diff line number Diff line change
@@ -1,13 +1,20 @@
annex[0] owner=OptionalForallClassifier::operation
(BehaviorActionBlock, <null>, 355, 28)
(AssignmentAction, <null>, 389, 10)
(BehaviorActionBlock, <null>, 355, 55)
(BehaviorAnnex, behavior_specification, 219, 192)
(BehaviorIntegerLiteral, <null>, 374, 1)
(BehaviorIntegerLiteral, <null>, 379, 1)
(BehaviorState, finish, 297, 6)
(BehaviorState, start, 272, 5)
(BehaviorStateGroup, <null>, 272, 21)
(BehaviorStateGroup, <null>, 297, 20)
(BehaviorTransition, <null>, 335, 48)
(BehaviorTransition, <null>, 389, 8)
(BehaviorTransition, <null>, 398, 13)
(BehaviorTransition, <null>, 335, 76)
(BehaviorVariable, value, 232, 5)
(BehaviorVariableGroup, <null>, 232, 27)
(ForStatement, <null>, 361, 22)
(ElementValues, <null>, 374, 6)
(ForStatement, <null>, 361, 44)
(Reference, <null>, 389, 5)
(Reference, <null>, 398, 1)
(ReferenceExpression, <null>, 398, 1)
(ReferenceSegment, i, 398, 1)
(ReferenceSegment, value, 389, 5)
Loading
Loading