diff --git a/ba/doc/conformance.md b/ba/doc/conformance.md index b86c0e6397..83e443b12c 100644 --- a/ba/doc/conformance.md +++ b/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. | diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_lr_D3_L6_L7_L8.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_lr_D3_L6_L7_L8.txt index f752f1cb8e..fabaa3d149 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_lr_D3_L6_L7_L8.txt +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_sr_D4_6.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_sr_D4_6.txt index c5892ff7b6..b0aeafe2b4 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_sr_D4_6.txt +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt index 1e62d1b772..ab7cf9c414 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue1884_issue1884.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue1884_issue1884.txt index ef704f78cb..3aa7d27089 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue1884_issue1884.txt +++ b/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 '' 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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt index bb4bb6b8f1..1df1c8feb9 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_FalseConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_FalseConditions.txt new file mode 100644 index 0000000000..3fb8496dea --- /dev/null +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_Issue3185.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_Issue3185.txt new file mode 100644 index 0000000000..3fb8496dea --- /dev/null +++ b/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. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_FalseConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_FalseConditions.txt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_Issue3185.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_Issue3185.txt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt new file mode 100644 index 0000000000..e69de29bb2 diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_FalseConditions.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_FalseConditions.txt new file mode 100644 index 0000000000..9051343241 --- /dev/null +++ b/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, , 2012, 5) + (BehaviorBooleanLiteral, , 2044, 4) + (BehaviorBooleanLiteral, , 2053, 4) + (BehaviorBooleanLiteral, , 2062, 5) + (BehaviorCondition, , 2012, 5) + (BehaviorCondition, , 2040, 28) + (BehaviorState, done, 1942, 4) + (BehaviorState, start, 1898, 5) + (BehaviorState, working, 1923, 7) + (BehaviorStateGroup, , 1898, 21) + (BehaviorStateGroup, , 1923, 15) + (BehaviorStateGroup, , 1942, 18) + (BehaviorTransition, , 1978, 20) + (BehaviorTransition, , 2002, 24) + (BehaviorTransition, , 2030, 47) + (BinaryExpression, , 2040, 28) + (BinaryExpression, , 2053, 14) + (ExecuteCondition, , 2012, 5) + (ExecuteCondition, , 2040, 28) + (ParenthesizedExpression, , 2052, 16) + (UnaryExpression, , 2040, 8) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_Issue3185.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_Issue3185.txt new file mode 100644 index 0000000000..bee6b56bf8 --- /dev/null +++ b/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, , 1892, 21) + (BehaviorStateGroup, , 1917, 15) + (BehaviorTransition, , 1950, 20) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt new file mode 100644 index 0000000000..64b2b18ff0 --- /dev/null +++ b/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, , 2223, 4) + (BehaviorBooleanLiteral, , 2231, 5) + (BehaviorCondition, , 2181, 10) + (BehaviorCondition, , 2223, 13) + (BehaviorCondition, , 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, , 1982, 21) + (BehaviorStateGroup, , 2007, 21) + (BehaviorStateGroup, , 2032, 18) + (BehaviorStateGroup, , 2054, 21) + (BehaviorStateGroup, , 2079, 16) + (BehaviorStateGroup, , 2099, 18) + (BehaviorTransition, , 2135, 26) + (BehaviorTransition, , 2165, 41) + (BehaviorTransition, , 2210, 44) + (BehaviorTransition, , 2258, 29) + (BehaviorTransition, , 2291, 29) + (BinaryExpression, , 2223, 13) + (ExecuteCondition, , 2181, 10) + (ExecuteCondition, , 2223, 13) + (ExecuteCondition, , 2302, 9) + (Reference, , 2181, 10) + (ReferenceExpression, , 2181, 10) + (ReferenceSegment, keep_going, 2181, 10) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt index 1aae906ae3..7985d951c2 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt +++ b/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, , 1927, 24) - (BehaviorStateGroup, , 1953, 16) - (BehaviorTransition, , 1983, 22) + (BehaviorStateGroup, , 1954, 22) + (BehaviorTransition, , 1990, 22) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt index b870059c8b..f6a1c54082 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt +++ b/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, , 2024, 5) - (BehaviorState, running, 1984, 7) + (BehaviorAnnex, behavior_specification, 1950, 98) + (BehaviorCondition, , 2031, 5) + (BehaviorState, running, 1985, 7) (BehaviorState, waiting, 1958, 7) (BehaviorStateGroup, , 1958, 24) - (BehaviorStateGroup, , 1984, 16) - (BehaviorTransition, , 2014, 27) - (ModeSwitchCondition, , 2027, 2) - (ModeSwitchConjunction, , 2027, 2) - (ModeSwitchTrigger, , 2027, 2) - (Reference, , 2027, 2) - (ReferenceSegment, go, 2027, 2) + (BehaviorStateGroup, , 1985, 22) + (BehaviorTransition, , 2021, 27) + (ModeSwitchCondition, , 2034, 2) + (ModeSwitchConjunction, , 2034, 2) + (ModeSwitchTrigger, , 2034, 2) + (Reference, , 2034, 2) + (ReferenceSegment, go, 2034, 2) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Inheritance.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Inheritance.txt index ad70ade26f..1eb55b2ce0 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Inheritance.txt +++ b/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, , 1854, 25) annex[1] owner=Inheritance::base.impl - (BehaviorAnnex, behavior_specification, 1963, 91) - (BehaviorCondition, , 2037, 5) - (BehaviorState, running, 1997, 7) + (BehaviorAnnex, behavior_specification, 1963, 98) + (BehaviorCondition, , 2044, 5) + (BehaviorState, running, 1998, 7) (BehaviorState, waiting, 1971, 7) (BehaviorStateGroup, , 1971, 24) - (BehaviorStateGroup, , 1997, 16) - (BehaviorTransition, , 2027, 27) - (ModeSwitchCondition, , 2040, 2) - (ModeSwitchConjunction, , 2040, 2) - (ModeSwitchTrigger, , 2040, 2) - (Reference, , 2040, 2) - (ReferenceSegment, go, 2040, 2) + (BehaviorStateGroup, , 1998, 22) + (BehaviorTransition, , 2034, 27) + (ModeSwitchCondition, , 2047, 2) + (ModeSwitchConjunction, , 2047, 2) + (ModeSwitchTrigger, , 2047, 2) + (Reference, , 2047, 2) + (ReferenceSegment, go, 2047, 2) annex[2] owner=Inheritance::base.replaced - (BehaviorAnnex, behavior_specification, 2243, 29) - (BehaviorState, only, 2251, 4) - (BehaviorStateGroup, , 2251, 21) + (BehaviorAnnex, behavior_specification, 2250, 29) + (BehaviorState, only, 2258, 4) + (BehaviorStateGroup, , 2258, 21) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Issue3186.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Issue3186.txt index 31096e5d25..cc5beeea32 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3186_Issue3186.txt +++ b/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, , 1979, 5) - (BehaviorState, running, 1939, 7) + (BehaviorAnnex, behavior_specification, 1905, 98) + (BehaviorCondition, , 1986, 5) + (BehaviorState, running, 1940, 7) (BehaviorState, waiting, 1913, 7) (BehaviorStateGroup, , 1913, 24) - (BehaviorStateGroup, , 1939, 16) - (BehaviorTransition, , 1969, 27) - (ModeSwitchCondition, , 1982, 2) - (ModeSwitchConjunction, , 1982, 2) - (ModeSwitchTrigger, , 1982, 2) - (Reference, , 1982, 2) - (ReferenceSegment, go, 1982, 2) + (BehaviorStateGroup, , 1940, 22) + (BehaviorTransition, , 1976, 27) + (ModeSwitchCondition, , 1989, 2) + (ModeSwitchConjunction, , 1989, 2) + (ModeSwitchTrigger, , 1989, 2) + (Reference, , 1989, 2) + (ReferenceSegment, go, 1989, 2) diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_FalseConditions.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_FalseConditions.txt new file mode 100644 index 0000000000..651d602622 --- /dev/null +++ b/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 diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_Issue3185.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_Issue3185.txt new file mode 100644 index 0000000000..102b617c30 --- /dev/null +++ b/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 diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt new file mode 100644 index 0000000000..9d8a05152e --- /dev/null +++ b/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 diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_FalseConditions.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_FalseConditions.txt new file mode 100644 index 0000000000..db7948e50d --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_FalseConditions.txt @@ -0,0 +1,13 @@ +===== annex[0] owner=FalseConditions::controller.impl ===== + +\t\tstates +\t\t\tstart: initial state; +\t\t\tworking: state; +\t\t\tdone: final state; +\t\ttransitions +\t\t\tstart -[]-> working; +\t\t\tworking -[false]-> done; +\t\t\tworking -[not true or (true and false)]-> done; +\t +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_Issue3185.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_Issue3185.txt new file mode 100644 index 0000000000..503a35e24a --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_Issue3185.txt @@ -0,0 +1,10 @@ +===== annex[0] owner=Issue3185::controller.impl ===== + +\t\tstates +\t\t\tstart: initial state; +\t\t\tworking: state; +\t\ttransitions +\t\t\tstart -[]-> working; +\t +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt new file mode 100644 index 0000000000..777df83dec --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt @@ -0,0 +1,18 @@ +===== annex[0] owner=PossiblyTrueConditions::controller.impl ===== + +\t\tstates +\t\t\tstart: initial state; +\t\t\tunknown_guard: state; +\t\t\ttrue_guard: state; +\t\t\tunconditional: state; +\t\t\tfallback: state; +\t\t\tdone: final state; +\t\ttransitions +\t\t\tstart -[]-> unknown_guard; +\t\t\tunknown_guard -[keep_going]-> true_guard; +\t\t\ttrue_guard -[true or false]-> unconditional; +\t\t\tunconditional -[]-> fallback; +\t\t\tfallback -[otherwise]-> done; +\t +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt index a54963c811..a2e53d9abf 100644 --- a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExecuteCondition.txt @@ -2,7 +2,7 @@ states \twaiting : initial state; -\trunning : state; +\t\trunning : final state; transitions \twaiting -[]-> running; ----- Xtext reparse ----- diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt index 2b2eb1b483..f615cb3624 100644 --- a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_InModesExternalCondition.txt @@ -2,7 +2,7 @@ states \twaiting : initial state; -\trunning : state; +\t\trunning : final state; transitions \twaiting -[on go]-> running; ----- Xtext reparse ----- diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Inheritance.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Inheritance.txt index 67b8e53275..a3531cae93 100644 --- a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Inheritance.txt +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Inheritance.txt @@ -8,7 +8,7 @@ reparsed states \twaiting : initial state; -\trunning : state; +\t\trunning : final state; transitions \twaiting -[on go]-> running; ----- Xtext reparse ----- diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Issue3186.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Issue3186.txt index cfc2dfeef2..3efc137c89 100644 --- a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Issue3186.txt +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3186_Issue3186.txt @@ -2,7 +2,7 @@ states \twaiting : initial state; -\trunning : state; +\t\trunning : final state; transitions \twaiting -[on go]-> running; ----- Xtext reparse ----- diff --git a/ba/org.osate.ba.tests/models/issue3185/.gitignore b/ba/org.osate.ba.tests/models/issue3185/.gitignore new file mode 100644 index 0000000000..afce51184c --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3185/.gitignore @@ -0,0 +1,2 @@ +/.aadlbin-gen/ +/instances/ diff --git a/ba/org.osate.ba.tests/models/issue3185/.project b/ba/org.osate.ba.tests/models/issue3185/.project new file mode 100644 index 0000000000..da58f5d8b4 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3185/.project @@ -0,0 +1,8 @@ + + + issue3185 + + + org.eclipse.xtext.ui.shared.xtextBuilder + org.osate.core.aadlnatureorg.eclipse.xtext.ui.shared.xtextNature + diff --git a/ba/org.osate.ba.tests/models/issue3185/FalseConditions.aadl b/ba/org.osate.ba.tests/models/issue3185/FalseConditions.aadl new file mode 100644 index 0000000000..dfc76255d7 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3185/FalseConditions.aadl @@ -0,0 +1,40 @@ +-- Copyright (c) 2004-2026 Carnegie Mellon University and others. (see Contributors file). +-- All Rights Reserved. +-- +-- NO WARRANTY. ALL MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY +-- KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE +-- OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT +-- MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. +-- +-- This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 +-- which is available at https://www.eclipse.org/legal/epl-2.0/ +-- SPDX-License-Identifier: EPL-2.0 +-- +-- Created, in part, with funding and support from the United States Government. (see Acknowledgments file). +-- +-- This program includes and/or can make use of certain third party source code, object code, documentation and other +-- files ("Third Party Software"). The Third Party Software that is used by this program is dependent upon your system +-- configuration. By using this program, You agree to comply with any and all relevant Third Party Software terms and +-- conditions contained in any such Third Party Software or separate license file distributed with such Third Party +-- Software. The parties who own the Third Party Software ("Third Party Licensors") are intended third party benefici- +-- aries to this license with respect to the terms applicable to their Third Party Software. Third Party Software li- +-- censes only apply to the Third Party Software and not any other portion of this program or this program as a whole. + +package FalseConditions +public + abstract controller + end controller; + + abstract implementation controller.impl + annex behavior_specification {** + states + start: initial state; + working: state; + done: final state; + transitions + start -[]-> working; + working -[false]-> done; + working -[not true or (true and false)]-> done; + **}; + end controller.impl; +end FalseConditions; diff --git a/ba/org.osate.ba.tests/models/issue3185/Issue3185.aadl b/ba/org.osate.ba.tests/models/issue3185/Issue3185.aadl new file mode 100644 index 0000000000..5cc2eb677b --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3185/Issue3185.aadl @@ -0,0 +1,37 @@ +-- Copyright (c) 2004-2026 Carnegie Mellon University and others. (see Contributors file). +-- All Rights Reserved. +-- +-- NO WARRANTY. ALL MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY +-- KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE +-- OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT +-- MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. +-- +-- This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 +-- which is available at https://www.eclipse.org/legal/epl-2.0/ +-- SPDX-License-Identifier: EPL-2.0 +-- +-- Created, in part, with funding and support from the United States Government. (see Acknowledgments file). +-- +-- This program includes and/or can make use of certain third party source code, object code, documentation and other +-- files ("Third Party Software"). The Third Party Software that is used by this program is dependent upon your system +-- configuration. By using this program, You agree to comply with any and all relevant Third Party Software terms and +-- conditions contained in any such Third Party Software or separate license file distributed with such Third Party +-- Software. The parties who own the Third Party Software ("Third Party Licensors") are intended third party benefici- +-- aries to this license with respect to the terms applicable to their Third Party Software. Third Party Software li- +-- censes only apply to the Third Party Software and not any other portion of this program or this program as a whole. + +package Issue3185 +public + abstract controller + end controller; + + abstract implementation controller.impl + annex behavior_specification {** + states + start: initial state; + working: state; + transitions + start -[]-> working; + **}; + end controller.impl; +end Issue3185; diff --git a/ba/org.osate.ba.tests/models/issue3185/PossiblyTrueConditions.aadl b/ba/org.osate.ba.tests/models/issue3185/PossiblyTrueConditions.aadl new file mode 100644 index 0000000000..978fd94d44 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3185/PossiblyTrueConditions.aadl @@ -0,0 +1,49 @@ +-- Copyright (c) 2004-2026 Carnegie Mellon University and others. (see Contributors file). +-- All Rights Reserved. +-- +-- NO WARRANTY. ALL MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY +-- KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE +-- OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT +-- MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. +-- +-- This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 +-- which is available at https://www.eclipse.org/legal/epl-2.0/ +-- SPDX-License-Identifier: EPL-2.0 +-- +-- Created, in part, with funding and support from the United States Government. (see Acknowledgments file). +-- +-- This program includes and/or can make use of certain third party source code, object code, documentation and other +-- files ("Third Party Software"). The Third Party Software that is used by this program is dependent upon your system +-- configuration. By using this program, You agree to comply with any and all relevant Third Party Software terms and +-- conditions contained in any such Third Party Software or separate license file distributed with such Third Party +-- Software. The parties who own the Third Party Software ("Third Party Licensors") are intended third party benefici- +-- aries to this license with respect to the terms applicable to their Third Party Software. Third Party Software li- +-- censes only apply to the Third Party Software and not any other portion of this program or this program as a whole. + +package PossiblyTrueConditions +public + with Base_Types; + + abstract controller + features + keep_going: in data port Base_Types::Boolean; + end controller; + + abstract implementation controller.impl + annex behavior_specification {** + states + start: initial state; + unknown_guard: state; + true_guard: state; + unconditional: state; + fallback: state; + done: final state; + transitions + start -[]-> unknown_guard; + unknown_guard -[keep_going]-> true_guard; + true_guard -[true or false]-> unconditional; + unconditional -[]-> fallback; + fallback -[otherwise]-> done; + **}; + end controller.impl; +end PossiblyTrueConditions; diff --git a/ba/org.osate.ba.tests/models/issue3186/InModesExecuteCondition.aadl b/ba/org.osate.ba.tests/models/issue3186/InModesExecuteCondition.aadl index 5e88579921..631beb2297 100644 --- a/ba/org.osate.ba.tests/models/issue3186/InModesExecuteCondition.aadl +++ b/ba/org.osate.ba.tests/models/issue3186/InModesExecuteCondition.aadl @@ -32,7 +32,7 @@ modes annex behavior_specification {** states waiting : initial state; - running : state; + running : final state; transitions waiting -[]-> running; **} in modes (normal); diff --git a/ba/org.osate.ba.tests/models/issue3186/InModesExternalCondition.aadl b/ba/org.osate.ba.tests/models/issue3186/InModesExternalCondition.aadl index 2f7e520991..53a9d594db 100644 --- a/ba/org.osate.ba.tests/models/issue3186/InModesExternalCondition.aadl +++ b/ba/org.osate.ba.tests/models/issue3186/InModesExternalCondition.aadl @@ -34,7 +34,7 @@ modes annex behavior_specification {** states waiting : initial state; - running : state; + running : final state; transitions waiting -[on go]-> running; **} in modes (normal); diff --git a/ba/org.osate.ba.tests/models/issue3186/Inheritance.aadl b/ba/org.osate.ba.tests/models/issue3186/Inheritance.aadl index 8fff9847e9..f15f5e2a39 100644 --- a/ba/org.osate.ba.tests/models/issue3186/Inheritance.aadl +++ b/ba/org.osate.ba.tests/models/issue3186/Inheritance.aadl @@ -36,7 +36,7 @@ abstract implementation base.impl annex behavior_specification {** states waiting : initial state; - running : state; + running : final state; transitions waiting -[on go]-> running; **}; diff --git a/ba/org.osate.ba.tests/models/issue3186/Issue3186.aadl b/ba/org.osate.ba.tests/models/issue3186/Issue3186.aadl index 6b3bd2b24d..479ad63ab5 100644 --- a/ba/org.osate.ba.tests/models/issue3186/Issue3186.aadl +++ b/ba/org.osate.ba.tests/models/issue3186/Issue3186.aadl @@ -32,7 +32,7 @@ process implementation controller.impl annex behavior_specification {** states waiting : initial state; - running : state; + running : final state; transitions waiting -[on go]-> running; **}; diff --git a/ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.java b/ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.java index a9771aebb9..965331904c 100644 --- a/ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.java +++ b/ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.java @@ -74,7 +74,8 @@ public void test_lr_D3_L5() throws Exception { @Test public void test_lr_D3_L6_L7_L8() throws Exception { - assertEquals(4, issues("lr_D3_L6_L7_L8.aadl").size()); + // The unqualified execution state also violates D.3.(C3) because it has no outgoing transition. + assertEquals(5, issues("lr_D3_L6_L7_L8.aadl").size()); } @Test @@ -111,7 +112,8 @@ public void test_sr_D3_18() throws Exception { @Test public void test_sr_D4_6() throws Exception { - assertEquals(3, issues("sr_D4_6.aadl").size()); + // Both unqualified execution states also violate D.3.(C3) because they have no outgoing transitions. + assertEquals(5, issues("sr_D4_6.aadl").size()); } private List issues(String fileName) throws Exception { diff --git a/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3185Test.java b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3185Test.java new file mode 100644 index 0000000000..579655e537 --- /dev/null +++ b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3185Test.java @@ -0,0 +1,81 @@ +/** + * Copyright (c) 2004-2026 Carnegie Mellon University and others. (see Contributors file). + * All Rights Reserved. + * + * NO WARRANTY. ALL MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY + * KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE + * OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT + * MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. + * + * This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0 + * which is available at https://www.eclipse.org/legal/epl-2.0/ + * SPDX-License-Identifier: EPL-2.0 + * + * Created, in part, with funding and support from the United States Government. (see Acknowledgments file). + * + * This program includes and/or can make use of certain third party source code, object code, documentation and other + * files ("Third Party Software"). The Third Party Software that is used by this program is dependent upon your system + * configuration. By using this program, You agree to comply with any and all relevant Third Party Software terms and + * conditions contained in any such Third Party Software or separate license file distributed with such Third Party + * Software. The parties who own the Third Party Software ("Third Party Licensors") are intended third party benefici- + * aries to this license with respect to the terms applicable to their Third Party Software. Third Party Software li- + * censes only apply to the Third Party Software and not any other portion of this program or this program as a whole. + */ +package org.osate.ba.tests; + +import static org.junit.Assert.assertEquals; + +import org.eclipse.xtext.diagnostics.Severity; +import org.eclipse.xtext.nodemodel.util.NodeModelUtils; +import org.eclipse.xtext.testing.InjectWith; +import org.eclipse.xtext.testing.XtextRunner; +import org.eclipse.xtext.testing.validation.ValidationTestHelper; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.osate.aadl2.AadlPackage; +import org.osate.testsupport.TestHelper; + +import com.google.inject.Inject; +import com.itemis.xtext.testing.XtextTest; + +/** Exercises the AS5506/3 Rev. A D.3 nonblocking rule for execution states. */ +@RunWith(XtextRunner.class) +@InjectWith(BehaviorAnnexInjectorProvider.class) +public class Issue3185Test extends XtextTest { + private static final String PATH = "org.osate.ba.tests/models/issue3185/"; + private static final String MESSAGE = "Execution state 'working' has no possibly true outgoing execute condition" + + " and can remain blocked: Behavior Annex D.3 consistency rule failed."; + + @Inject + private TestHelper testHelper; + + @Inject + private ValidationTestHelper validationHelper; + + @Test + public void executionStateWithoutOutgoingTransitionIsRejected() throws Exception { + assertDiagnostic("Issue3185", "working"); + } + + @Test + public void staticallyFalseExecuteConditionsAreRejected() throws Exception { + assertDiagnostic("FalseConditions", "working"); + } + + @Test + public void conditionsThatMayBeTrueAreHandledConservatively() throws Exception { + validationHelper.assertNoIssues(testHelper.parseFile(PATH + "PossiblyTrueConditions.aadl")); + } + + private void assertDiagnostic(String model, String target) throws Exception { + var root = testHelper.parseFile(PATH + model + ".aadl"); + var source = NodeModelUtils.getNode(root).getRootNode().getText(); + var issues = validationHelper.validate(root); + assertEquals(issues.toString(), 1, issues.size()); + var issue = issues.getFirst(); + assertEquals(Severity.ERROR, issue.getSeverity()); + assertEquals("org.osate.xtext.aadl2.ba.checker", issue.getCode()); + assertEquals(target, source.substring(issue.getOffset(), issue.getOffset() + issue.getLength())); + assertEquals(MESSAGE, issue.getMessage()); + } +} diff --git a/ba/org.osate.ba/resources/checking_And_Comments_Rules_AADL_BA_Current_Version.txt b/ba/org.osate.ba/resources/checking_And_Comments_Rules_AADL_BA_Current_Version.txt index 9b0ac623b2..a3889bd813 100644 --- a/ba/org.osate.ba/resources/checking_And_Comments_Rules_AADL_BA_Current_Version.txt +++ b/ba/org.osate.ba/resources/checking_And_Comments_Rules_AADL_BA_Current_Version.txt @@ -84,7 +84,7 @@ Notes: - D.3.(N1) : an empty execute condition is equivalent to a condition that is always true. [IMPLEMENTED] in [PARSER]. - D.3.(18) : only transition out of execution states or states that are intial only may have execute condition. [TODO] too many errors are found in aadlba std's exemples. Is the std wrong ? [IMPLEMENTED] -- D.3.(C3) : the logical disjunction of all the execute conditions associated with the transitions out of an execution state must be true. [NOT IMPLEMENTED] [TODO] : is it statically analyzable ? +- D.3.(C3) : the logical disjunction of all the execute conditions associated with the transitions out of an execution state must be true. [IMPLEMENTED] for an empty disjunction and execute conditions that reduce to Boolean literals; runtime-dependent, non-value, or unsupported conditions are accepted conservatively. -------------------------- diff --git a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java index 8f8648f80a..690cdc2e35 100644 --- a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java +++ b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java @@ -36,6 +36,7 @@ import org.osate.aadl2.modelsupport.errorreporting.AnalysisErrorReporterManager; import org.osate.ba.aadlba.ActualPortHolder; import org.osate.ba.aadlba.BehaviorAnnex; +import org.osate.ba.aadlba.BehaviorBooleanLiteral; import org.osate.ba.aadlba.BehaviorCondition; import org.osate.ba.aadlba.BehaviorElement; import org.osate.ba.aadlba.BehaviorState; @@ -43,10 +44,18 @@ import org.osate.ba.aadlba.DispatchCondition; import org.osate.ba.aadlba.DispatchTrigger; import org.osate.ba.aadlba.DispatchTriggerLogicalExpression; +import org.osate.ba.aadlba.Factor; import org.osate.ba.aadlba.ModeSwitchConjunction; import org.osate.ba.aadlba.ModeSwitchTrigger; import org.osate.ba.aadlba.ModeSwitchTriggerCondition; import org.osate.ba.aadlba.ModeSwitchTriggerLogicalExpression; +import org.osate.ba.aadlba.Otherwise; +import org.osate.ba.aadlba.Relation; +import org.osate.ba.aadlba.SimpleExpression; +import org.osate.ba.aadlba.Term; +import org.osate.ba.aadlba.UnaryBooleanOperator; +import org.osate.ba.aadlba.Value; +import org.osate.ba.aadlba.ValueExpression; import org.osate.ba.utils.AadlBaUtils; import org.osate.ba.utils.AadlBaVisitors; import org.osate.utils.internal.Aadl2Utils; @@ -70,6 +79,129 @@ public AadlBaConsistencyRulesChecker(BehaviorAnnex ba, ComponentClassifier paren _contextsTab = AadlBaVisitors.getBaPackageSections(_ba, _baParentContainer); } + /** + * Document: AS5506/3 Rev A + * Type : Consistency rule + * Section : D.3 Behavior Specification + * Object : The disjunction of the execute conditions on transitions out of an execution state must be true. + * Report only a definite violation: an empty disjunction or one whose conditions reduce to false using Boolean + * literals and operators. A runtime-dependent expression or any non-value condition makes the result unknown and + * is accepted conservatively. + * Keys : execution state execute condition nonblocking + */ + public boolean D_3_C3_Check(BehaviorAnnex ba) { + var result = true; + for (var state : ba.getStates()) { + if (state.isInitial() || state.isComplete() || state.isFinal()) { + continue; + } + var disjunction = StaticTruth.FALSE; + for (var transition : state.getOutgoingTransitions()) { + var condition = transition.getCondition(); + if (condition == null || condition instanceof Otherwise) { + disjunction = StaticTruth.TRUE; + break; + } + if (condition instanceof ValueExpression expression) { + disjunction = disjunction.or(staticTruth(expression)); + } else { + disjunction = disjunction.or(StaticTruth.UNKNOWN); + } + } + if (disjunction == StaticTruth.FALSE) { + result = false; + reportConsistencyError(state, "Execution state '" + state.getName() + + "' has no possibly true outgoing execute condition and can remain blocked: " + + "Behavior Annex D.3 consistency rule failed"); + } + } + return result; + } + + private static StaticTruth staticTruth(ValueExpression expression) { + if (expression.getRelations().isEmpty() + || expression.getLogicalOperators().size() != expression.getRelations().size() - 1) { + return StaticTruth.UNKNOWN; + } + var result = staticTruth(expression.getRelations().getFirst()); + for (var i = 1; i < expression.getRelations().size(); i++) { + var right = staticTruth(expression.getRelations().get(i)); + result = switch (expression.getLogicalOperators().get(i - 1)) { + case AND, AND_THEN -> result.and(right); + case OR, OR_ELSE -> result.or(right); + case XOR -> result.xor(right); + default -> StaticTruth.UNKNOWN; + }; + } + return result; + } + + private static StaticTruth staticTruth(Relation relation) { + return relation.getSecondExpression() == null && !relation.isSetRelationalOperator() + ? staticTruth(relation.getFirstExpression()) + : StaticTruth.UNKNOWN; + } + + private static StaticTruth staticTruth(SimpleExpression expression) { + return !expression.isSetUnaryAddingOperator() && expression.getTerms().size() == 1 + && expression.getBinaryAddingOperators().isEmpty() ? staticTruth(expression.getTerms().getFirst()) + : StaticTruth.UNKNOWN; + } + + private static StaticTruth staticTruth(Term term) { + return term.getFactors().size() == 1 && term.getMultiplyingOperators().isEmpty() + ? staticTruth(term.getFactors().getFirst()) + : StaticTruth.UNKNOWN; + } + + private static StaticTruth staticTruth(Factor factor) { + if (factor.getSecondValue() != null || factor.isSetBinaryNumericOperator() + || factor.isSetUnaryNumericOperator()) { + return StaticTruth.UNKNOWN; + } + var result = staticTruth(factor.getFirstValue()); + if (factor.isSetUnaryBooleanOperator()) { + result = factor.getUnaryBooleanOperator() == UnaryBooleanOperator.NOT ? result.not() : StaticTruth.UNKNOWN; + } + return result; + } + + private static StaticTruth staticTruth(Value value) { + if (value instanceof BehaviorBooleanLiteral literal) { + return literal.isValue() ? StaticTruth.TRUE : StaticTruth.FALSE; + } + return value instanceof ValueExpression expression ? staticTruth(expression) : StaticTruth.UNKNOWN; + } + + private enum StaticTruth { + FALSE, TRUE, UNKNOWN; + + private StaticTruth and(StaticTruth other) { + if (this == FALSE || other == FALSE) { + return FALSE; + } + return this == TRUE && other == TRUE ? TRUE : UNKNOWN; + } + + private StaticTruth or(StaticTruth other) { + if (this == TRUE || other == TRUE) { + return TRUE; + } + return this == FALSE && other == FALSE ? FALSE : UNKNOWN; + } + + private StaticTruth xor(StaticTruth other) { + if (this == UNKNOWN || other == UNKNOWN) { + return UNKNOWN; + } + return this == other ? FALSE : TRUE; + } + + private StaticTruth not() { + return this == TRUE ? FALSE : this == FALSE ? TRUE : UNKNOWN; + } + } + /** * Document: AADL Behavior Annex draft * Version : 0.94 diff --git a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java index e9dff37771..7a07fe1c6d 100644 --- a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java +++ b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java @@ -160,6 +160,7 @@ public Boolean caseAnnexSubclause(AnnexSubclause object) { result &= _legality.D_3_L1_And_L2_Check(initialStates, completeStates, finalStates); result &= _legality.D_3_L3_Check(initialStates, completeStates); result &= _legality.D_3_L4_Check(initialStates, finalStates); + result &= _consistency.D_3_C3_Check(_ba); } // End of first if.