Enforce Behavior Annex action timeout legality rules 🤖

ba/doc/conformance.md

@@ -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 a subset of dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions were absent (G01, since fixed) and the naming and otherwise-transition rules unenforced (V01 and V02, since fixed); mode binding is explicitly missing; multiple subprogram final states are rejected unconditionally; 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, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` is absent; internal events were represented incorrectly (G10, since fixed); call-signature and 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)); timeout, resource-release, and signature obligations are incomplete or unverified. |
+| 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.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 circuits and `updated` are missing; expression grouping/precedence and numeric translation differ from the document; 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. |
 
@@ -186,7 +186,7 @@ These are bounded findings from the inspected grammar/translator/checker path. E
 | --- | --- | --- |
 | V01 | D.3 naming: variables, states, and transitions share uniqueness restrictions and must not conflict with relevant enclosing declarations, with the mode exception. | The Xtext validator has no explicit BA naming check; the translator's case-insensitive variable map overwrites duplicate keys. Its superclass validates properties, not the complete BA namespace rule. Verify ordinary AADL/core checks before assigning ownership of the missing diagnostics. Add duplicates across declaration kinds and enclosing feature/data/mode conflicts. **Implemented for [#3182](https://github.com/osate/osate2/issues/3182):** the validator checks the shared declaration namespace case-insensitively, including inherited features, data subcomponents, and modes, reports an error on each offending identifier, preserves the complete-state/mode exception, and checks names even when the classifier is unresolved. Translation keeps duplicate declarations but leaves an ambiguous reference unresolved instead of silently selecting the last one. `Issue3182Test` covers grouped and cross-kind duplicates, inherited declarations, component-type annexes, legal scope boundaries, unnamed transitions, and complete states representing modes. |
 | V02 | D.3 otherwise rules: no assigned priority and at most one otherwise transition per source state. | Implemented for [#3183](https://github.com/osate/osate2/issues/3183): report every conflicting otherwise transition as an error identifying its source state, including overlapping multi-source declarations. Explicit priorities produce a warning once per declaration, reflecting the standard's “should not” wording. `Issue3183Test` covers duplicates, source overlap, explicit zero and positive priorities, and valid otherwise transitions. |
-| V03 | D.3 and D.6 action timeouts: a matching simple timeout transition from the same source; restrictions on combining an action timeout with timeout conditions. | Timeouts are stored by the translator, but `caseBehaviorActionBlock` processes only its content. No corresponding timeout/catch-pair analysis was found in the current driver/type checker. Test positive and negative pairs and dispatch-timeout/action-timeout combinations. |
+| V03 | D.3 and D.6 action timeouts: a matching simple timeout transition from the same source; restrictions on combining an action timeout with timeout conditions. | Implemented for [#3184](https://github.com/osate/osate2/issues/3184): every top-level or nested action timeout is checked against each source of its transition for a same-source simple timeout catch. Action timeouts on execution-timeout, dispatch-relative-timeout, and completion-relative-timeout transitions are rejected. Diagnostics mark the behavior time and name a missing source state; `Issue3184Test` covers positive, missing, wrong-source, nested, expanded multi-source, and all three prohibited timeout-condition forms. |
 | V04 | D.3 nonblocking execution-state behavior. | The only consistency-checker method is the mode-related C4 check; no guard-exhaustiveness analysis is present there. The driver also comments out the call to the older `D_3_18_Checker`; that method's existence does not establish coverage. Distinguish general symbolic proof from simple detectable dead ends and clearly document any analysis limit. |
 | V05 | D.3 component-category/mode restrictions on external/internal conditions; behavior inheritance and replacement. | Conditions can be parsed generically, while type checking dispatches only execute conditions and the rules driver primarily dispatch conditions. Mode bindings are absent (G14), and the builder does not copy an in-modes context into the strict annex. Core AADL may retain mode applicability on the enclosing annex. Verify the complete consumer path before declaring inheritance or mode-specific selection unsupported. Cover thread/subprogram external-condition rejection and device condition mixing. |
 | V06 | D.4 protocol/trigger compatibility, legal trigger/frozen-port categories, and consistency with core dispatch/freeze properties. | The checker has dedicated timeout branches and a stop check, but no complete implementation of the document's protocol/trigger table was found. Dispatch references use generic `Reference` syntax. A rule implementing one timeout form is not evidence for all rows of the table. Test the matrix and invalid trigger direction/category through embedded source. |
@@ -225,7 +225,7 @@ These are proposed follow-up changes, not changes made by this review.
 | 1 | ~~Repair the conformance test oracle and ensure deterministic BA validator registration. Separate legacy characterization from standard expectations.~~ **Done**, branch `repair_conformance_test_oracle` (commit `Repair the Behavior Annex conformance test oracle`). | Exact diagnostics are compared, by `expected/diagnostics` and the new `expected/diagnostics-validated`; registration is proved end to end by requiring at least one BA rule diagnostic in the validated suite and none in the plain baseline; both suites and the conformance class assert nonzero executed cases; the nine skips it left were listed in `TRACKED_SKIPS` against their own issues and enforced by reflection, and that list has shrunk to five as those issues closed; `SelfPropertyReference.aadl` no longer carries an unrelated D.3 error. Each repaired expectation was confirmed to fail for its intended reason by temporarily removing its `@Ignore`. |
 | 2 | Preserve strict-model meaning: numeric literals, array extents, logical grouping, `self`, internal events, and mode bindings (G08, G10–G14). **Under way:** G08, G10, and G11 are closed and G12's pull request is open; logical grouping (G13) and mode bindings (G14) remain. | External AADL input produces correct literal values, extents, references, operation kinds, and mode links; no test-only model mutation is needed. Assert attributes and semantic structure directly. |
 | 3 | Implement the missing standard syntax and remove unwanted overacceptance (G01–G07, G09, G13). **Under way:** G01, G03, and G04 are closed; G02, G05, G06, G07, G09, and G13 remain. | Each standard form parses and translates; nonstandard forms have deliberate rejection/extension policy. Enable corrected standard acceptance tests and add AST/strict-model expression tests. |
-| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16, V01, and V02 are closed; G15, G17, G18, V03, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. |
+| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16 and V01–V03 are addressed; G15, G17, G18, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. |
 | 5 | Establish behavioral/dataflow coverage and consumer boundaries (V04–V05, V08–V09, D.5 and D.8 runtime semantics). | State which obligations the front end can prove, which are warnings/approximations, and which belong to a simulator, analyzer, or generator. Validate queue behavior, timeouts, lock lifetimes, initialization, and call synchronization in the responsible consumer. |
 
 There is no basis here for a numerical conformance percentage: the suite is not a clause-complete standard test suite, some assertions are ineffective, and operational semantics were outside the executed scope. A defensible future claim should distinguish syntax acceptance, valid strict-model construction, legality/consistency enforcement, and downstream execution semantics.

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

@@ -0,0 +1,2 @@
+error | semantic | 35 | 53 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed.
+error | semantic | 35 | 67 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed.

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

@@ -0,0 +1 @@
+error | semantic | 37 | 60 | 4 | A behavior action timeout must have a transition from source state 'second' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed.

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

@@ -0,0 +1,3 @@
+error | semantic | 35 | 55 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed.
+error | semantic | 51 | 69 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed.
+error | semantic | 61 | 74 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed.

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

@@ -0,0 +1 @@
+error | semantic | 36 | 55 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed.

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

@@ -0,0 +1,35 @@
+annex[0] owner=Issue3184::example.impl
+  (BehaviorActionBlock, <null>, 1977, 33)
+  (BehaviorActionBlock, <null>, 2061, 35)
+  (BehaviorActionBlock, <null>, 2062, 33)
+  (BehaviorAnnex, behavior_specification, 1872, 252)
+  (BehaviorBooleanLiteral, <null>, 1962, 4)
+  (BehaviorBooleanLiteral, <null>, 2048, 4)
+  (BehaviorCondition, <null>, 1962, 4)
+  (BehaviorCondition, <null>, 2021, 7)
+  (BehaviorCondition, <null>, 2048, 4)
+  (BehaviorCondition, <null>, 2108, 7)
+  (BehaviorIntegerLiteral, <null>, 1991, 1)
+  (BehaviorIntegerLiteral, <null>, 2006, 1)
+  (BehaviorIntegerLiteral, <null>, 2076, 1)
+  (BehaviorIntegerLiteral, <null>, 2091, 1)
+  (BehaviorState, done, 1921, 4)
+  (BehaviorState, nested, 1904, 6)
+  (BehaviorState, start, 1880, 5)
+  (BehaviorStateGroup, <null>, 1880, 22)
+  (BehaviorStateGroup, <null>, 1904, 15)
+  (BehaviorStateGroup, <null>, 1921, 19)
+  (BehaviorTime, <null>, 1991, 4)
+  (BehaviorTime, <null>, 2006, 4)
+  (BehaviorTime, <null>, 2076, 4)
+  (BehaviorTime, <null>, 2091, 4)
+  (BehaviorTransition, <null>, 1954, 57)
+  (BehaviorTransition, <null>, 2013, 24)
+  (BehaviorTransition, <null>, 2039, 58)
+  (BehaviorTransition, <null>, 2099, 25)
+  (ExecuteCondition, <null>, 1962, 4)
+  (ExecuteCondition, <null>, 2021, 7)
+  (ExecuteCondition, <null>, 2048, 4)
+  (ExecuteCondition, <null>, 2108, 7)
+  (TimedAction, <null>, 1978, 18)
+  (TimedAction, <null>, 2063, 18)

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

@@ -0,0 +1,19 @@
+annex[0] owner=MissingCatch::example.impl
+  (BehaviorActionBlock, <null>, 1961, 48)
+  (BehaviorActionBlock, <null>, 1962, 33)
+  (BehaviorAnnex, behavior_specification, 1875, 135)
+  (BehaviorBooleanLiteral, <null>, 1948, 4)
+  (BehaviorCondition, <null>, 1948, 4)
+  (BehaviorIntegerLiteral, <null>, 1976, 1)
+  (BehaviorIntegerLiteral, <null>, 1991, 1)
+  (BehaviorIntegerLiteral, <null>, 2005, 1)
+  (BehaviorState, done, 1907, 4)
+  (BehaviorState, start, 1883, 5)
+  (BehaviorStateGroup, <null>, 1883, 22)
+  (BehaviorStateGroup, <null>, 1907, 19)
+  (BehaviorTime, <null>, 1976, 4)
+  (BehaviorTime, <null>, 1991, 4)
+  (BehaviorTime, <null>, 2005, 4)
+  (BehaviorTransition, <null>, 1940, 70)
+  (ExecuteCondition, <null>, 1948, 4)
+  (TimedAction, <null>, 1963, 18)

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

@@ -0,0 +1,23 @@
+annex[0] owner=MultipleSources::example.impl
+  (BehaviorActionBlock, <null>, 2016, 33)
+  (BehaviorAnnex, behavior_specification, 1878, 198)
+  (BehaviorBooleanLiteral, <null>, 2003, 4)
+  (BehaviorCondition, <null>, 2003, 4)
+  (BehaviorCondition, <null>, 2060, 7)
+  (BehaviorIntegerLiteral, <null>, 2030, 1)
+  (BehaviorIntegerLiteral, <null>, 2045, 1)
+  (BehaviorState, done, 1934, 4)
+  (BehaviorState, first, 1910, 5)
+  (BehaviorState, second, 1917, 6)
+  (BehaviorState, start, 1886, 5)
+  (BehaviorStateGroup, <null>, 1886, 22)
+  (BehaviorStateGroup, <null>, 1910, 22)
+  (BehaviorStateGroup, <null>, 1934, 19)
+  (BehaviorTime, <null>, 2030, 4)
+  (BehaviorTime, <null>, 2045, 4)
+  (BehaviorTransition, <null>, 1967, 18)
+  (BehaviorTransition, <null>, 1987, 63)
+  (BehaviorTransition, <null>, 2052, 24)
+  (ExecuteCondition, <null>, 2003, 4)
+  (ExecuteCondition, <null>, 2060, 7)
+  (TimedAction, <null>, 2017, 18)

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

@@ -0,0 +1,49 @@
+annex[0] owner=TimeoutConditions::operation.impl
+  (BehaviorActionBlock, <null>, 1975, 33)
+  (BehaviorAnnex, behavior_specification, 1886, 123)
+  (BehaviorCondition, <null>, 1959, 7)
+  (BehaviorIntegerLiteral, <null>, 1989, 1)
+  (BehaviorIntegerLiteral, <null>, 2004, 1)
+  (BehaviorState, done, 1918, 4)
+  (BehaviorState, start, 1894, 5)
+  (BehaviorStateGroup, <null>, 1894, 22)
+  (BehaviorStateGroup, <null>, 1918, 19)
+  (BehaviorTime, <null>, 1989, 4)
+  (BehaviorTime, <null>, 2004, 4)
+  (BehaviorTransition, <null>, 1951, 58)
+  (ExecuteCondition, <null>, 1959, 7)
+  (TimedAction, <null>, 1976, 18)
+annex[1] owner=TimeoutConditions::worker.dispatch_relative
+  (BehaviorActionBlock, <null>, 2324, 33)
+  (BehaviorAnnex, behavior_specification, 2201, 157)
+  (BehaviorCondition, <null>, 2296, 19)
+  (BehaviorIntegerLiteral, <null>, 2338, 1)
+  (BehaviorIntegerLiteral, <null>, 2353, 1)
+  (BehaviorState, done, 2244, 4)
+  (BehaviorState, waiting, 2209, 7)
+  (BehaviorStateGroup, <null>, 2209, 33)
+  (BehaviorStateGroup, <null>, 2244, 28)
+  (BehaviorTime, <null>, 2338, 4)
+  (BehaviorTime, <null>, 2353, 4)
+  (BehaviorTransition, <null>, 2286, 72)
+  (DispatchCondition, <null>, 2299, 16)
+  (DispatchTriggerCondition, <null>, 2308, 7)
+  (TimedAction, <null>, 2325, 18)
+annex[2] owner=TimeoutConditions::worker.completion_relative
+  (BehaviorActionBlock, <null>, 2605, 33)
+  (BehaviorAnnex, behavior_specification, 2477, 162)
+  (BehaviorCondition, <null>, 2572, 24)
+  (BehaviorIntegerLiteral, <null>, 2592, 1)
+  (BehaviorIntegerLiteral, <null>, 2619, 1)
+  (BehaviorIntegerLiteral, <null>, 2634, 1)
+  (BehaviorState, done, 2520, 4)
+  (BehaviorState, waiting, 2485, 7)
+  (BehaviorStateGroup, <null>, 2485, 33)
+  (BehaviorStateGroup, <null>, 2520, 28)
+  (BehaviorTime, <null>, 2592, 4)
+  (BehaviorTime, <null>, 2619, 4)
+  (BehaviorTime, <null>, 2634, 4)
+  (BehaviorTransition, <null>, 2562, 77)
+  (DispatchCondition, <null>, 2575, 21)
+  (DispatchTriggerCondition, <null>, 2584, 12)
+  (TimedAction, <null>, 2606, 18)

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

@@ -0,0 +1,21 @@
+annex[0] owner=WrongSourceCatch::example.impl
+  (BehaviorActionBlock, <null>, 1986, 33)
+  (BehaviorAnnex, behavior_specification, 1879, 169)
+  (BehaviorBooleanLiteral, <null>, 1970, 4)
+  (BehaviorCondition, <null>, 1970, 4)
+  (BehaviorCondition, <null>, 2032, 7)
+  (BehaviorIntegerLiteral, <null>, 2000, 1)
+  (BehaviorIntegerLiteral, <null>, 2015, 1)
+  (BehaviorState, done, 1929, 4)
+  (BehaviorState, running, 1911, 7)
+  (BehaviorState, start, 1887, 5)
+  (BehaviorStateGroup, <null>, 1887, 22)
+  (BehaviorStateGroup, <null>, 1911, 16)
+  (BehaviorStateGroup, <null>, 1929, 19)
+  (BehaviorTime, <null>, 2000, 4)
+  (BehaviorTime, <null>, 2015, 4)
+  (BehaviorTransition, <null>, 1962, 58)
+  (BehaviorTransition, <null>, 2022, 26)
+  (ExecuteCondition, <null>, 1970, 4)
+  (ExecuteCondition, <null>, 2032, 7)
+  (TimedAction, <null>, 1987, 18)