Detect Behavior Annex execution states that can remain blocked 🤖

ba/doc/conformance.md

@@ -191,7 +191,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. | 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. |
+| V04 | D.3 nonblocking execution-state behavior. | **Addressed by [#3185](https://github.com/osate/osate2/issues/3185):** the consistency checker reports an execution state whose outgoing execute-condition disjunction is definitely false. This includes states with no outgoing transitions and execute conditions that reduce to false using Boolean literals, `not`, `and`/`and then`, `or`/`or else`, and `xor`. An unconditional or `otherwise` transition makes the disjunction true. Conditions that depend on runtime values, non-value conditions such as events and timeouts, relations, or unsupported expressions are not reported because the checker cannot prove that the state remains blocked; this conservative limit avoids rejecting a state whose transitions may be enabled at runtime. `Issue3185Test` covers definite dead ends and the accepted cases. |
 | 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. Same-named complete states are now bound for no-`in modes` refinements (G14), but 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. **Addressed by [#3186](https://github.com/osate/osate2/issues/3186):** the consistency checker rejects an external condition in a thread or a subprogram and rejects a mixture of external and dispatch conditions out of one complete state of a device; the validator rejects an external condition in a subclause with an `in modes` statement, which is where in-modes rules already live because core AADL keeps that statement on the enclosing subclause rather than in the strict annex. D.3 states no per-category restriction on internal conditions beyond the execution-state rule closed with [#3165](https://github.com/osate/osate2/issues/3165). C4 now reads the triggers of an external condition as well, so the mode-transition comparison covers the way a component of any other category than thread and subprogram describes a mode transition; that made `issue2147` report the missing-mode-transition finding its dispatch equivalent already produced. Mode applicability is not duplicated into the strict annex: core AADL keeps it on the `DefaultAnnexSubclause` that every consumer of `BehaviorAnnexUtil.getStrictModel` already holds. `BehaviorAnnexUtil.getBehaviorAnnexSubclauses` implements the ancestor/descendant rule on that access path, with a mode-selecting overload. `Issue3186Test` covers each rejection, a positive control for each, and the inheritance, replacement, type-fallback, and mode-selection cases. The subcomponent override rule is not enforced: it selects which subclause a consumer interprets for an instance rather than constraining a declaration, so it belongs to the consumer that walks the instance hierarchy. |
 | 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. |
 | V07 | D.5 C1/C2: BA freeze/send operations agree with `Input_Time`/`Output_Time`, or are absent where required. | No BA check referring to these properties was found in the active BA checker/translator/validator code. Core property validation alone does not establish agreement with BA actions. Use models that are individually legal on each side but inconsistent together. |

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

@@ -1,3 +1,4 @@
+error | semantic | 49 | 2 | 8 | Execution state 'exeState' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
 error | semantic | 58 | 3 | 28 | Transitions out of complete states must have dispatch condition : Behavior Annex D.3.(L7) legality rule failed.
 error | semantic | 63 | 16 | 11 | Only transition out of complete states may have dispatch condition : Behavior Annex D.3.(L6) legality rule failed.
 error | semantic | 63 | 3 | 40 | Transitions out of final states are not allowed : Behavior Annex D.3.(L8) legality rule failed.

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

@@ -1,3 +1,5 @@
+error | semantic | 56 | 2 | 9 | Execution state 'exeState1' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
+error | semantic | 57 | 2 | 9 | Execution state 'exeState2' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
 error | semantic | 64 | 14 | 16 | Only transition out of complete states may have dispatch condition : Behavior Annex D.3.(L6) legality rule failed.
 error | semantic | 64 | 26 | 4 | The stop dispatch trigger statement must be declared in a transition that ends to final state possibly via one or more execution states: Behavior Annex D.4.(6) semantic rule failed.
 error | semantic | 64 | 26 | 4 | The stop dispatch trigger statement must be declared in an outgoing transition of a complete state: Behavior Annex D.4.(6) semantic rule failed.

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

@@ -1,3 +1,4 @@
+error | semantic | 161 | 8 | 1 | Execution state 'c' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
 error | semantic | 165 | 2 | 2 | NamesResolutionTest::thread1.impl can't have more than one initial state : a5, a6 : Behavior Annex D.3.(L3) legality rule failed.
 error | semantic | 166 | 2 | 2 | NamesResolutionTest::thread1.impl can't have more than one initial state : a5, a6 : Behavior Annex D.3.(L3) legality rule failed.
 error | semantic | 199 | 19 | 14 | The completion relative timeout condition and catch statement must have a value greater or equal to the Period of the thread it is defined in (otherwise) timeout condition can never occur.

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

@@ -1,4 +1,5 @@
 error | linking | 17 | 27 | 13 | Couldn't resolve reference to BehaviorState 'bad_reference'.
+error | semantic | 25 | 5 | 2 | Execution state 's1' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
 error | semantic | 27 | 23 | 7 | The dispatch relative timeout and catch statement must only be declared for timed thread: Behavior Annex D.4.(L1) legality rule failed.
 error | syntax | 7 | 14 | 3 | mismatched input '<EOF>' expecting ';'
 warning | semantic | 27 | 11 | 19 | Using a dispatch condition in an abstract component means this component can only be refined into a component category on which the Dispatch_Protocol property can be applied.

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

@@ -1 +1,2 @@
+error | semantic | 31 | 5 | 2 | Execution state 's1' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.
 error | semantic | 35 | 11 | 8 | The behavior transition tries to refine a transition mode while issue2147::threadA.impl component hasn't got any transition mode: Behavior Annex D.3.(C4) consistency rule failed.

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

@@ -0,0 +1 @@
+error | semantic | 32 | 4 | 7 | Execution state 'working' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.

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

@@ -0,0 +1 @@
+error | semantic | 32 | 4 | 7 | Execution state 'working' has no possibly true outgoing execute condition and can remain blocked: Behavior Annex D.3 consistency rule failed.

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

@@ -0,0 +1,23 @@
+annex[0] owner=FalseConditions::controller.impl
+  (BehaviorAnnex, behavior_specification, 1888, 189)
+  (BehaviorBooleanLiteral, <null>, 2012, 5)
+  (BehaviorBooleanLiteral, <null>, 2044, 4)
+  (BehaviorBooleanLiteral, <null>, 2053, 4)
+  (BehaviorBooleanLiteral, <null>, 2062, 5)
+  (BehaviorCondition, <null>, 2012, 5)
+  (BehaviorCondition, <null>, 2040, 28)
+  (BehaviorState, done, 1942, 4)
+  (BehaviorState, start, 1898, 5)
+  (BehaviorState, working, 1923, 7)
+  (BehaviorStateGroup, <null>, 1898, 21)
+  (BehaviorStateGroup, <null>, 1923, 15)
+  (BehaviorStateGroup, <null>, 1942, 18)
+  (BehaviorTransition, <null>, 1978, 20)
+  (BehaviorTransition, <null>, 2002, 24)
+  (BehaviorTransition, <null>, 2030, 47)
+  (BinaryExpression, <null>, 2040, 28)
+  (BinaryExpression, <null>, 2053, 14)
+  (ExecuteCondition, <null>, 2012, 5)
+  (ExecuteCondition, <null>, 2040, 28)
+  (ParenthesizedExpression, <null>, 2052, 16)
+  (UnaryExpression, <null>, 2040, 8)

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

@@ -0,0 +1,7 @@
+annex[0] owner=Issue3185::controller.impl
+  (BehaviorAnnex, behavior_specification, 1882, 88)
+  (BehaviorState, start, 1892, 5)
+  (BehaviorState, working, 1917, 7)
+  (BehaviorStateGroup, <null>, 1892, 21)
+  (BehaviorStateGroup, <null>, 1917, 15)
+  (BehaviorTransition, <null>, 1950, 20)

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

@@ -0,0 +1,31 @@
+annex[0] owner=PossiblyTrueConditions::controller.impl
+  (BehaviorAnnex, behavior_specification, 1972, 348)
+  (BehaviorBooleanLiteral, <null>, 2223, 4)
+  (BehaviorBooleanLiteral, <null>, 2231, 5)
+  (BehaviorCondition, <null>, 2181, 10)
+  (BehaviorCondition, <null>, 2223, 13)
+  (BehaviorCondition, <null>, 2302, 9)
+  (BehaviorState, done, 2099, 4)
+  (BehaviorState, fallback, 2079, 8)
+  (BehaviorState, start, 1982, 5)
+  (BehaviorState, true_guard, 2032, 10)
+  (BehaviorState, unconditional, 2054, 13)
+  (BehaviorState, unknown_guard, 2007, 13)
+  (BehaviorStateGroup, <null>, 1982, 21)
+  (BehaviorStateGroup, <null>, 2007, 21)
+  (BehaviorStateGroup, <null>, 2032, 18)
+  (BehaviorStateGroup, <null>, 2054, 21)
+  (BehaviorStateGroup, <null>, 2079, 16)
+  (BehaviorStateGroup, <null>, 2099, 18)
+  (BehaviorTransition, <null>, 2135, 26)
+  (BehaviorTransition, <null>, 2165, 41)
+  (BehaviorTransition, <null>, 2210, 44)
+  (BehaviorTransition, <null>, 2258, 29)
+  (BehaviorTransition, <null>, 2291, 29)
+  (BinaryExpression, <null>, 2223, 13)
+  (ExecuteCondition, <null>, 2181, 10)
+  (ExecuteCondition, <null>, 2223, 13)
+  (ExecuteCondition, <null>, 2302, 9)
+  (Reference, <null>, 2181, 10)
+  (ReferenceExpression, <null>, 2181, 10)
+  (ReferenceSegment, keep_going, 2181, 10)

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

@@ -1,7 +1,7 @@
 annex[0] owner=InModesExecuteCondition::controller.impl
-  (BehaviorAnnex, behavior_specification, 1919, 86)
-  (BehaviorState, running, 1953, 7)
+  (BehaviorAnnex, behavior_specification, 1919, 93)
+  (BehaviorState, running, 1954, 7)
   (BehaviorState, waiting, 1927, 7)
   (BehaviorStateGroup, <null>, 1927, 24)
-  (BehaviorStateGroup, <null>, 1953, 16)
-  (BehaviorTransition, <null>, 1983, 22)
+  (BehaviorStateGroup, <null>, 1954, 22)
+  (BehaviorTransition, <null>, 1990, 22)

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

@@ -1,13 +1,13 @@
 annex[0] owner=InModesExternalCondition::controller.impl
-  (BehaviorAnnex, behavior_specification, 1950, 91)
-  (BehaviorCondition, <null>, 2024, 5)
-  (BehaviorState, running, 1984, 7)
+  (BehaviorAnnex, behavior_specification, 1950, 98)
+  (BehaviorCondition, <null>, 2031, 5)
+  (BehaviorState, running, 1985, 7)
   (BehaviorState, waiting, 1958, 7)
   (BehaviorStateGroup, <null>, 1958, 24)
-  (BehaviorStateGroup, <null>, 1984, 16)
-  (BehaviorTransition, <null>, 2014, 27)
-  (ModeSwitchCondition, <null>, 2027, 2)
-  (ModeSwitchConjunction, <null>, 2027, 2)
-  (ModeSwitchTrigger, <null>, 2027, 2)
-  (Reference, <null>, 2027, 2)
-  (ReferenceSegment, go, 2027, 2)
+  (BehaviorStateGroup, <null>, 1985, 22)
+  (BehaviorTransition, <null>, 2021, 27)
+  (ModeSwitchCondition, <null>, 2034, 2)
+  (ModeSwitchConjunction, <null>, 2034, 2)
+  (ModeSwitchTrigger, <null>, 2034, 2)
+  (Reference, <null>, 2034, 2)
+  (ReferenceSegment, go, 2034, 2)

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

@@ -3,19 +3,19 @@ annex[0] owner=Inheritance::base
   (BehaviorState, fromtype, 1854, 8)
   (BehaviorStateGroup, <null>, 1854, 25)
 annex[1] owner=Inheritance::base.impl
-  (BehaviorAnnex, behavior_specification, 1963, 91)
-  (BehaviorCondition, <null>, 2037, 5)
-  (BehaviorState, running, 1997, 7)
+  (BehaviorAnnex, behavior_specification, 1963, 98)
+  (BehaviorCondition, <null>, 2044, 5)
+  (BehaviorState, running, 1998, 7)
   (BehaviorState, waiting, 1971, 7)
   (BehaviorStateGroup, <null>, 1971, 24)
-  (BehaviorStateGroup, <null>, 1997, 16)
-  (BehaviorTransition, <null>, 2027, 27)
-  (ModeSwitchCondition, <null>, 2040, 2)
-  (ModeSwitchConjunction, <null>, 2040, 2)
-  (ModeSwitchTrigger, <null>, 2040, 2)
-  (Reference, <null>, 2040, 2)
-  (ReferenceSegment, go, 2040, 2)
+  (BehaviorStateGroup, <null>, 1998, 22)
+  (BehaviorTransition, <null>, 2034, 27)
+  (ModeSwitchCondition, <null>, 2047, 2)
+  (ModeSwitchConjunction, <null>, 2047, 2)
+  (ModeSwitchTrigger, <null>, 2047, 2)
+  (Reference, <null>, 2047, 2)
+  (ReferenceSegment, go, 2047, 2)
 annex[2] owner=Inheritance::base.replaced
-  (BehaviorAnnex, behavior_specification, 2243, 29)
-  (BehaviorState, only, 2251, 4)
-  (BehaviorStateGroup, <null>, 2251, 21)
+  (BehaviorAnnex, behavior_specification, 2250, 29)
+  (BehaviorState, only, 2258, 4)
+  (BehaviorStateGroup, <null>, 2258, 21)

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

@@ -1,13 +1,13 @@
 annex[0] owner=Issue3186::controller.impl
-  (BehaviorAnnex, behavior_specification, 1905, 91)
-  (BehaviorCondition, <null>, 1979, 5)
-  (BehaviorState, running, 1939, 7)
+  (BehaviorAnnex, behavior_specification, 1905, 98)
+  (BehaviorCondition, <null>, 1986, 5)
+  (BehaviorState, running, 1940, 7)
   (BehaviorState, waiting, 1913, 7)
   (BehaviorStateGroup, <null>, 1913, 24)
-  (BehaviorStateGroup, <null>, 1939, 16)
-  (BehaviorTransition, <null>, 1969, 27)
-  (ModeSwitchCondition, <null>, 1982, 2)
-  (ModeSwitchConjunction, <null>, 1982, 2)
-  (ModeSwitchTrigger, <null>, 1982, 2)
-  (Reference, <null>, 1982, 2)
-  (ReferenceSegment, go, 1982, 2)
+  (BehaviorStateGroup, <null>, 1940, 22)
+  (BehaviorTransition, <null>, 1976, 27)
+  (ModeSwitchCondition, <null>, 1989, 2)
+  (ModeSwitchConjunction, <null>, 1989, 2)
+  (ModeSwitchTrigger, <null>, 1989, 2)
+  (Reference, <null>, 1989, 2)
+  (ReferenceSegment, go, 1989, 2)

ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_FalseConditions.txt

@@ -0,0 +1,35 @@
+annex[0] owner=FalseConditions::controller.impl
+  parsedAnnexSubclause : BehaviorAnnex name=behavior_specification
+    states[0] : BehaviorState name=start
+    states[1] : BehaviorState name=working
+    states[2] : BehaviorState name=done
+    transitions[0] : BehaviorTransition
+    transitions[1] : BehaviorTransition
+      condition : ValueExpression
+        relations[0] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : BehaviorBooleanLiteral
+    transitions[2] : BehaviorTransition
+      condition : ValueExpression
+        relations[0] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : BehaviorBooleanLiteral
+        relations[1] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : ValueExpression
+                  relations[0] : Relation
+                    firstExpression : SimpleExpression
+                      terms[0] : Term
+                        factors[0] : Factor
+                          firstValue : BehaviorBooleanLiteral
+                  relations[1] : Relation
+                    firstExpression : SimpleExpression
+                      terms[0] : Term
+                        factors[0] : Factor
+                          firstValue : BehaviorBooleanLiteral

ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_Issue3185.txt

@@ -0,0 +1,5 @@
+annex[0] owner=Issue3185::controller.impl
+  parsedAnnexSubclause : BehaviorAnnex name=behavior_specification
+    states[0] : BehaviorState name=start
+    states[1] : BehaviorState name=working
+    transitions[0] : BehaviorTransition

ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt

@@ -0,0 +1,31 @@
+annex[0] owner=PossiblyTrueConditions::controller.impl
+  parsedAnnexSubclause : BehaviorAnnex name=behavior_specification
+    states[0] : BehaviorState name=start
+    states[1] : BehaviorState name=unknown_guard
+    states[2] : BehaviorState name=true_guard
+    states[3] : BehaviorState name=unconditional
+    states[4] : BehaviorState name=fallback
+    states[5] : BehaviorState name=done
+    transitions[0] : BehaviorTransition
+    transitions[1] : BehaviorTransition
+      condition : ValueExpression
+        relations[0] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : DataPortHolder element=PossiblyTrueConditions::controller.keep_going [DataPort]
+    transitions[2] : BehaviorTransition
+      condition : ValueExpression
+        relations[0] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : BehaviorBooleanLiteral
+        relations[1] : Relation
+          firstExpression : SimpleExpression
+            terms[0] : Term
+              factors[0] : Factor
+                firstValue : BehaviorBooleanLiteral
+    transitions[3] : BehaviorTransition
+    transitions[4] : BehaviorTransition
+      condition : Otherwise