From 0c96f262033e8b8f47638a450cd6de03f315f994 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Thu, 17 Sep 2026 09:24:23 -0400 Subject: [PATCH 1/2] Add regression test for issue #3185 Model execution states with no outgoing transition and with only statically false execute conditions, and assert the missing D.3 diagnostics. Include positive controls for runtime-dependent, true, unconditional, and otherwise conditions to keep the analysis conservative. --- ...tests_models_issue3185_FalseConditions.txt | 1 + ...te.ba.tests_models_issue3185_Issue3185.txt | 1 + ...odels_issue3185_PossiblyTrueConditions.txt | 0 ...tests_models_issue3185_FalseConditions.txt | 0 ...te.ba.tests_models_issue3185_Issue3185.txt | 0 ...odels_issue3185_PossiblyTrueConditions.txt | 0 ...tests_models_issue3185_FalseConditions.txt | 23 ++++++ ...te.ba.tests_models_issue3185_Issue3185.txt | 7 ++ ...odels_issue3185_PossiblyTrueConditions.txt | 31 +++++++ ...tests_models_issue3185_FalseConditions.txt | 35 ++++++++ ...te.ba.tests_models_issue3185_Issue3185.txt | 5 ++ ...odels_issue3185_PossiblyTrueConditions.txt | 31 +++++++ ...tests_models_issue3185_FalseConditions.txt | 13 +++ ...te.ba.tests_models_issue3185_Issue3185.txt | 10 +++ ...odels_issue3185_PossiblyTrueConditions.txt | 18 +++++ .../models/issue3185/.gitignore | 2 + .../models/issue3185/.project | 8 ++ .../models/issue3185/FalseConditions.aadl | 40 +++++++++ .../models/issue3185/Issue3185.aadl | 37 +++++++++ .../issue3185/PossiblyTrueConditions.aadl | 49 +++++++++++ .../src/org/osate/ba/tests/Issue3185Test.java | 81 +++++++++++++++++++ 21 files changed, 392 insertions(+) create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_FalseConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_Issue3185.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_FalseConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_Issue3185.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_FalseConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_Issue3185.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_FalseConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_Issue3185.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_FalseConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_Issue3185.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3185_PossiblyTrueConditions.txt create mode 100644 ba/org.osate.ba.tests/models/issue3185/.gitignore create mode 100644 ba/org.osate.ba.tests/models/issue3185/.project create mode 100644 ba/org.osate.ba.tests/models/issue3185/FalseConditions.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3185/Issue3185.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3185/PossiblyTrueConditions.aadl create mode 100644 ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3185Test.java 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 00000000000..3fb8496dead --- /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 00000000000..3fb8496dead --- /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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..e69de29bb2d 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 00000000000..90513432416 --- /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 00000000000..bee6b56bf8e --- /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 00000000000..64b2b18ff03 --- /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/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 00000000000..651d6026220 --- /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 00000000000..102b617c309 --- /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 00000000000..9d8a05152e6 --- /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 00000000000..db7948e50d3 --- /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 00000000000..503a35e24a6 --- /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 00000000000..777df83decf --- /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/models/issue3185/.gitignore b/ba/org.osate.ba.tests/models/issue3185/.gitignore new file mode 100644 index 00000000000..afce51184c6 --- /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 00000000000..da58f5d8b42 --- /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 00000000000..dfc76255d79 --- /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 00000000000..5cc2eb677b5 --- /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 00000000000..978fd94d44a --- /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/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 00000000000..579655e5371 --- /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()); + } +} From 42c3f8b64923baae1750a10298b7ff36e1c65bcd Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Thu, 17 Sep 2026 09:33:32 -0400 Subject: [PATCH 2/2] Detect blocked Behavior Annex execution states Implement the D.3 consistency check for execution states whose outgoing condition disjunction is definitely false. Fold Boolean literal guards conservatively, accepting runtime-dependent and unsupported conditions when blocking cannot be proven. Update conformance documentation, characterization baselines, and existing positive fixtures so the broader Behavior Annex suite reflects the new diagnostic without obscuring their original intent. --- ba/doc/conformance.md | 2 +- ...odels_covering_semantic_lr_D3_L6_L7_L8.txt | 1 + ...tests_models_covering_semantic_sr_D4_6.txt | 2 + ...s_models_covering_syntax_aadlBaTest001.txt | 1 + ...te.ba.tests_models_issue1884_issue1884.txt | 1 + ...te.ba.tests_models_issue2147_issue2147.txt | 1 + ...dels_issue3186_InModesExecuteCondition.txt | 8 +- ...els_issue3186_InModesExternalCondition.txt | 20 +-- ....ba.tests_models_issue3186_Inheritance.txt | 26 ++-- ...te.ba.tests_models_issue3186_Issue3186.txt | 20 +-- ...dels_issue3186_InModesExecuteCondition.txt | 2 +- ...els_issue3186_InModesExternalCondition.txt | 2 +- ....ba.tests_models_issue3186_Inheritance.txt | 2 +- ...te.ba.tests_models_issue3186_Issue3186.txt | 2 +- .../issue3186/InModesExecuteCondition.aadl | 2 +- .../issue3186/InModesExternalCondition.aadl | 2 +- .../models/issue3186/Inheritance.aadl | 2 +- .../models/issue3186/Issue3186.aadl | 2 +- .../osate/ba/tests/CoveringSemanticTest.java | 6 +- ...Comments_Rules_AADL_BA_Current_Version.txt | 2 +- .../AadlBaConsistencyRulesChecker.java | 132 ++++++++++++++++++ .../analyzers/AadlBaRulesCheckersDriver.java | 1 + 22 files changed, 190 insertions(+), 49 deletions(-) diff --git a/ba/doc/conformance.md b/ba/doc/conformance.md index b86c0e6397d..83e443b12cb 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 f752f1cb8e5..fabaa3d1498 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 c5892ff7b69..b0aeafe2b48 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 1e62d1b7720..ab7cf9c4145 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 ef704f78cb6..3aa7d270893 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 bb4bb6b8f17..1df1c8feb9b 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/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 1aae906ae30..7985d951c2a 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 b870059c8b0..f6a1c54082a 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 ad70ade26f0..1eb55b2ce01 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 31096e5d25d..cc5beeea32c 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/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 a54963c811a..a2e53d9abf5 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 2b2eb1b4839..f615cb36244 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 67b8e532750..a3531cae934 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 cfc2dfeef2b..3efc137c89a 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/issue3186/InModesExecuteCondition.aadl b/ba/org.osate.ba.tests/models/issue3186/InModesExecuteCondition.aadl index 5e88579921e..631beb22976 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 2f7e5209919..53a9d594db4 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 8fff9847e9d..f15f5e2a39a 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 6b3bd2b24d9..479ad63ab56 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 a9771aebb97..965331904cc 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/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 9b0ac623b2d..a3889bd8135 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 8f8648f80aa..690cdc2e355 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 e9dff377719..7a07fe1c6d4 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.