Allow multiple final states in Behavior Annex specifications 🤖

ba/doc/conformance.md

@@ -12,7 +12,7 @@ The user directed that the report findings be treated as valid and filed without
 
 | Finding | Issue | Finding | Issue |
 | --- | --- | --- | --- |
-| G01 ✅ | [#3165](https://github.com/osate/osate2/issues/3165) | G15 | [#3179](https://github.com/osate/osate2/issues/3179) |
+| G01 ✅ | [#3165](https://github.com/osate/osate2/issues/3165) | G15 ✅ | [#3179](https://github.com/osate/osate2/issues/3179) |
 | G02 ✅ | [#3166](https://github.com/osate/osate2/issues/3166) | G16 ✅ | [#3180](https://github.com/osate/osate2/issues/3180) |
 | G03 ✅ | [#3167](https://github.com/osate/osate2/issues/3167) | G17 | [#3181](https://github.com/osate/osate2/issues/3181) |
 | G04 ✅ | [#3168](https://github.com/osate/osate2/issues/3168) | V01 ✅ | [#3182](https://github.com/osate/osate2/issues/3182) |
@@ -57,7 +57,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato
 | Section | Implemented capability and evidence | Assessment |
 | --- | --- | --- |
 | D.1–D.2: scope and concepts | Embedded `behavior_specification` parser, linker, serializer, and strict-model translation are registered. | Supports the language-tooling role; execution semantics require separate consumer evidence. |
-| 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.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), complete-state mode binding (G14), and multiple subprogram final states (G15) were absent and are now implemented; 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, 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. |
@@ -144,9 +144,11 @@ The AST precedence error and the strict-model flattening error must be assessed
 
 **Standard:** D.3's description explicitly allows several final states when specifying intended behavior; a deterministic implementation representation is distinguished as requiring one final state.
 
-**Evidence:** [AadlBaLegalityRulesChecker.D_3_L1_And_L2_Check](../../ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java), lines 133–145, reports an error whenever a subprogram has more than one final state. No specification-versus-deterministic-implementation distinction gates that branch. `CoveringSemanticTest.test_lr_D3_L1_L2` and the diagnostic regression tests preserve the multiple-final-state rejection.
+**Review evidence:** [AadlBaLegalityRulesChecker.D_3_L1_And_L2_Check](../../ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java) reported an error whenever a subprogram had more than one final state. No specification-versus-deterministic-implementation distinction gated that branch. `CoveringSemanticTest.test_lr_D3_L1_L2` and the diagnostic regression tests preserved the multiple-final-state rejection.
 
-**Impact:** A documented standard-conforming specification style is rejected. Add a valid subprogram specification with alternative final states before deciding how any deterministic-profile restriction should be expressed.
+**Review impact:** A documented standard-conforming specification style was rejected.
+
+**Implemented for [#3179](https://github.com/osate/osate2/issues/3179):** standard behavior specifications now allow multiple final states in every component category. Subprograms still require at least one final state; an annex on a component implementation does not itself select a deterministic implementation profile. [Issue3179Test](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3179Test.java) validates an external model covering all 14 categories, both types and implementations, and a subprogram with an initial-final state. It asserts that each annex has two final states and that both classifier kinds cover every category. Existing negative state-rule tests and diagnostic goldens retain the missing-final-state, initial-state, complete-state, and outgoing-final-state checks.
 
 ### G16 — Loop-variable target legality is not enforced by its named covering test
 

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_lr_D3_L1_L2.txt

@@ -2,5 +2,3 @@ error | semantic | 47 | 1 | 96 | exemple_lr_D3_L1_L2::sub.error1 has no final st
 error | semantic | 48 | 2 | 10 | exemple_lr_D3_L1_L2::sub.error1 can't have more than one initial state : initState1, initState2 : Behavior Annex D.3.(L1) legality rule failed.
 error | semantic | 49 | 2 | 10 | exemple_lr_D3_L1_L2::sub.error1 can't have more than one initial state : initState1, initState2 : Behavior Annex D.3.(L1) legality rule failed.
 error | semantic | 50 | 2 | 9 | exemple_lr_D3_L1_L2::sub.error1 can't have complete state : compState : Behavior Annex D.3.(L2) legality rule failed.
-error | semantic | 61 | 2 | 11 | exemple_lr_D3_L1_L2::sub.error2 has more than one final state : uniqueState, finalState1 : Behavior Annex D.3.(L1) legality rule failed.
-error | semantic | 62 | 2 | 11 | exemple_lr_D3_L1_L2::sub.error2 has more than one final state : uniqueState, finalState1 : Behavior Annex D.3.(L1) legality rule failed.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3155_Issue3155.txt

@@ -4,8 +4,6 @@ error | semantic | 38 | 5 | 27 | Transitions out of final states are not allowed
 error | semantic | 48 | 19 | 13 | issue3155::subprogramLegality.impl can't have more than one initial state : firstInitial, secondInitial : Behavior Annex D.3.(L1) legality rule failed.
 error | semantic | 48 | 5 | 12 | issue3155::subprogramLegality.impl can't have more than one initial state : firstInitial, secondInitial : Behavior Annex D.3.(L1) legality rule failed.
 error | semantic | 49 | 5 | 9 | issue3155::subprogramLegality.impl can't have complete state : waitState : Behavior Annex D.3.(L2) legality rule failed.
-error | semantic | 50 | 17 | 11 | issue3155::subprogramLegality.impl has more than one final state : firstFinal, secondFinal : Behavior Annex D.3.(L1) legality rule failed.
-error | semantic | 50 | 5 | 10 | issue3155::subprogramLegality.impl has more than one final state : firstFinal, secondFinal : Behavior Annex D.3.(L1) legality rule failed.
 error | semantic | 60 | 5 | 12 | issue3155::threadLegality.impl can't have more than one initial state : firstInitial, secondInitial : Behavior Annex D.3.(L3) legality rule failed.
 error | semantic | 61 | 5 | 13 | issue3155::threadLegality.impl can't have more than one initial state : firstInitial, secondInitial : Behavior Annex D.3.(L3) legality rule failed.
 error | semantic | 75 | 18 | 11 | Only transition out of complete states may have dispatch condition : Behavior Annex D.3.(L6) legality rule failed.

ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_covering_semantic_lr_D3_L1_L2.txt

@@ -3,16 +3,16 @@ annex[0] owner=exemple_lr_D3_L1_L2::sub.good
   (BehaviorState, uniqueState, 953, 11)
   (BehaviorStateGroup, <null>, 953, 35)
 annex[1] owner=exemple_lr_D3_L1_L2::sub.error1
-  (BehaviorAnnex, behavior_specification, 1278, 96)
-  (BehaviorState, compState, 1346, 9)
-  (BehaviorState, initState1, 1286, 10)
-  (BehaviorState, initState2, 1316, 10)
-  (BehaviorStateGroup, <null>, 1286, 28)
-  (BehaviorStateGroup, <null>, 1316, 28)
-  (BehaviorStateGroup, <null>, 1346, 28)
+  (BehaviorAnnex, behavior_specification, 1287, 96)
+  (BehaviorState, compState, 1355, 9)
+  (BehaviorState, initState1, 1295, 10)
+  (BehaviorState, initState2, 1325, 10)
+  (BehaviorStateGroup, <null>, 1295, 28)
+  (BehaviorStateGroup, <null>, 1325, 28)
+  (BehaviorStateGroup, <null>, 1355, 28)
 annex[2] owner=exemple_lr_D3_L1_L2::sub.error2
-  (BehaviorAnnex, behavior_specification, 1573, 72)
-  (BehaviorState, finalState1, 1618, 11)
-  (BehaviorState, uniqueState, 1581, 11)
-  (BehaviorStateGroup, <null>, 1581, 35)
-  (BehaviorStateGroup, <null>, 1618, 27)
+  (BehaviorAnnex, behavior_specification, 1608, 72)
+  (BehaviorState, finalState1, 1653, 11)
+  (BehaviorState, uniqueState, 1616, 11)
+  (BehaviorStateGroup, <null>, 1616, 35)
+  (BehaviorStateGroup, <null>, 1653, 27)