From d9e527270a5f00c2957cb7d577acef5717206878 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 11 Sep 2026 10:21:56 -0400 Subject: [PATCH 1/2] Add regression test for issue #3184 Model valid action timeouts with same-source catches and invalid cases with missing, wrong-source, and timeout-conditioned transitions. Assert exact diagnostics and source ranges, including nested and expanded multi-source action blocks. --- .../models/issue3184/.gitignore | 2 + .../models/issue3184/.project | 8 ++ .../models/issue3184/Issue3184.aadl | 42 +++++++ .../models/issue3184/MissingCatch.aadl | 38 +++++++ .../models/issue3184/MultipleSources.aadl | 41 +++++++ .../models/issue3184/TimeoutConditions.aadl | 64 +++++++++++ .../models/issue3184/WrongSourceCatch.aadl | 40 +++++++ .../src/org/osate/ba/tests/Issue3184Test.java | 106 ++++++++++++++++++ 8 files changed, 341 insertions(+) create mode 100644 ba/org.osate.ba.tests/models/issue3184/.gitignore create mode 100644 ba/org.osate.ba.tests/models/issue3184/.project create mode 100644 ba/org.osate.ba.tests/models/issue3184/Issue3184.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3184/MissingCatch.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3184/MultipleSources.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3184/TimeoutConditions.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3184/WrongSourceCatch.aadl create mode 100644 ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3184Test.java diff --git a/ba/org.osate.ba.tests/models/issue3184/.gitignore b/ba/org.osate.ba.tests/models/issue3184/.gitignore new file mode 100644 index 00000000000..afce51184c6 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/.gitignore @@ -0,0 +1,2 @@ +/.aadlbin-gen/ +/instances/ diff --git a/ba/org.osate.ba.tests/models/issue3184/.project b/ba/org.osate.ba.tests/models/issue3184/.project new file mode 100644 index 00000000000..3da143fa0ed --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/.project @@ -0,0 +1,8 @@ + + + issue3184 + + + org.eclipse.xtext.ui.shared.xtextBuilder + org.osate.core.aadlnatureorg.eclipse.xtext.ui.shared.xtextNature + diff --git a/ba/org.osate.ba.tests/models/issue3184/Issue3184.aadl b/ba/org.osate.ba.tests/models/issue3184/Issue3184.aadl new file mode 100644 index 00000000000..020dfc3db26 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/Issue3184.aadl @@ -0,0 +1,42 @@ +-- 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 Issue3184 +public + +subprogram example +end example; + +subprogram implementation example.impl +annex behavior_specification {** +states + start : initial state; + nested : state; + done : final state; +transitions + start -[true]-> nested {computation (1 ms)} timeout 2 ms; + start -[timeout]-> done; + nested -[true]-> done {{computation (1 ms)} timeout 3 ms}; + nested -[timeout]-> done; +**}; +end example.impl; +end Issue3184; diff --git a/ba/org.osate.ba.tests/models/issue3184/MissingCatch.aadl b/ba/org.osate.ba.tests/models/issue3184/MissingCatch.aadl new file mode 100644 index 00000000000..39bb9bd8b3b --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/MissingCatch.aadl @@ -0,0 +1,38 @@ +-- 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 MissingCatch +public + +subprogram example +end example; + +subprogram implementation example.impl +annex behavior_specification {** +states + start : initial state; + done : final state; +transitions + start -[true]-> done {{computation (1 ms)} timeout 3 ms} timeout 2 ms; +**}; +end example.impl; +end MissingCatch; diff --git a/ba/org.osate.ba.tests/models/issue3184/MultipleSources.aadl b/ba/org.osate.ba.tests/models/issue3184/MultipleSources.aadl new file mode 100644 index 00000000000..f08ec7de1cb --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/MultipleSources.aadl @@ -0,0 +1,41 @@ +-- 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 MultipleSources +public + +subprogram example +end example; + +subprogram implementation example.impl +annex behavior_specification {** +states + start : initial state; + first, second : state; + done : final state; +transitions + start -[]-> first; + first, second -[true]-> done {computation (1 ms)} timeout 2 ms; + first -[timeout]-> done; +**}; +end example.impl; +end MultipleSources; diff --git a/ba/org.osate.ba.tests/models/issue3184/TimeoutConditions.aadl b/ba/org.osate.ba.tests/models/issue3184/TimeoutConditions.aadl new file mode 100644 index 00000000000..fb94d533605 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/TimeoutConditions.aadl @@ -0,0 +1,64 @@ +-- 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 TimeoutConditions +public + +subprogram operation +end operation; + +subprogram implementation operation.impl +annex behavior_specification {** +states + start : initial state; + done : final state; +transitions + start -[timeout]-> done {computation (1 ms)} timeout 2 ms; +**}; +end operation.impl; + +thread worker +properties + Dispatch_Protocol => Timed; + Period => 10 ms; +end worker; + +thread implementation worker.dispatch_relative +annex behavior_specification {** +states + waiting : initial complete state; + done : complete final state; +transitions + waiting -[on dispatch timeout]-> done {computation (1 ms)} timeout 3 ms; +**}; +end worker.dispatch_relative; + +thread implementation worker.completion_relative +annex behavior_specification {** +states + waiting : initial complete state; + done : complete final state; +transitions + waiting -[on dispatch timeout 5 ms]-> done {computation (1 ms)} timeout 4 ms; +**}; +end worker.completion_relative; +end TimeoutConditions; diff --git a/ba/org.osate.ba.tests/models/issue3184/WrongSourceCatch.aadl b/ba/org.osate.ba.tests/models/issue3184/WrongSourceCatch.aadl new file mode 100644 index 00000000000..1bfb3660795 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3184/WrongSourceCatch.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 WrongSourceCatch +public + +subprogram example +end example; + +subprogram implementation example.impl +annex behavior_specification {** +states + start : initial state; + running : state; + done : final state; +transitions + start -[true]-> running {computation (1 ms)} timeout 2 ms; + running -[timeout]-> done; +**}; +end example.impl; +end WrongSourceCatch; diff --git a/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3184Test.java b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3184Test.java new file mode 100644 index 00000000000..446f5c8556f --- /dev/null +++ b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3184Test.java @@ -0,0 +1,106 @@ +/** + * 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 java.util.Comparator; +import java.util.List; + +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.eclipse.xtext.validation.Issue; +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 and D.6 action-timeout rules through embedded AADL validation. */ +@RunWith(XtextRunner.class) +@InjectWith(BehaviorAnnexInjectorProvider.class) +public class Issue3184Test extends XtextTest { + private static final String PATH = "org.osate.ba.tests/models/issue3184/"; + private static final String TIMEOUT_CONDITION = "A behavior action timeout is not allowed on a transition with a " + + "timeout condition : Behavior Annex D.3 and D.6 legality rules failed."; + + @Inject + private TestHelper testHelper; + + @Inject + private ValidationTestHelper validationHelper; + + @Test + public void simpleCatchFromSameSourceAcceptsTopLevelAndNestedTimeouts() throws Exception { + var root = testHelper.parseFile(PATH + "Issue3184.aadl"); + validationHelper.assertNoIssues(root); + } + + @Test + public void actionTimeoutRequiresCatchTransition() throws Exception { + assertDiagnostics("MissingCatch", List.of(new Expected("3 ms", missingCatch("start")), + new Expected("2 ms", missingCatch("start")))); + } + + @Test + public void catchTransitionMustHaveSameSource() throws Exception { + assertDiagnostics("WrongSourceCatch", List.of(new Expected("2 ms", missingCatch("start")))); + } + + @Test + public void everySourceOfExpandedTransitionRequiresCatch() throws Exception { + assertDiagnostics("MultipleSources", List.of(new Expected("2 ms", missingCatch("second")))); + } + + @Test + public void timeoutConditionsRejectActionTimeouts() throws Exception { + assertDiagnostics("TimeoutConditions", List.of(new Expected("2 ms", TIMEOUT_CONDITION), + new Expected("3 ms", TIMEOUT_CONDITION), new Expected("4 ms", TIMEOUT_CONDITION))); + } + + private static String missingCatch(String state) { + return "A behavior action timeout must have a transition from source state '" + state + + "' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed."; + } + + private void assertDiagnostics(String model, List expected) throws Exception { + var root = testHelper.parseFile(PATH + model + ".aadl"); + var source = NodeModelUtils.getNode(root).getRootNode().getText(); + var issues = validationHelper.validate(root).stream().sorted(Comparator.comparing(Issue::getOffset)).toList(); + assertEquals(issues.toString(), expected.size(), issues.size()); + assertEquals(expected, issues.stream().map(issue -> { + assertEquals(Severity.ERROR, issue.getSeverity()); + var target = source.substring(issue.getOffset(), issue.getOffset() + issue.getLength()); + return new Expected(target, issue.getMessage()); + }).toList()); + } + + private record Expected(String target, String message) { + } +} From 992f3908efaec0c2200f155267b38f4255b279b0 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 11 Sep 2026 10:36:54 -0400 Subject: [PATCH 2/2] Enforce Behavior Annex action timeout rules Check every timeout-bearing action block for a simple timeout transition from the same source state. Reject action timeouts on execution, dispatch-relative, and completion-relative timeout conditions, including every source created from a multi-source declaration. Update the Behavior Annex conformance record and corpus goldens for the new diagnostics. --- ba/doc/conformance.md | 6 +- ...te.ba.tests_models_issue3184_Issue3184.txt | 0 ...ba.tests_models_issue3184_MissingCatch.txt | 2 + ...tests_models_issue3184_MultipleSources.txt | 1 + ...sts_models_issue3184_TimeoutConditions.txt | 3 + ...ests_models_issue3184_WrongSourceCatch.txt | 1 + ...te.ba.tests_models_issue3184_Issue3184.txt | 0 ...ba.tests_models_issue3184_MissingCatch.txt | 0 ...tests_models_issue3184_MultipleSources.txt | 0 ...sts_models_issue3184_TimeoutConditions.txt | 0 ...ests_models_issue3184_WrongSourceCatch.txt | 0 ...te.ba.tests_models_issue3184_Issue3184.txt | 35 ++++++++++ ...ba.tests_models_issue3184_MissingCatch.txt | 19 +++++ ...tests_models_issue3184_MultipleSources.txt | 23 ++++++ ...sts_models_issue3184_TimeoutConditions.txt | 49 +++++++++++++ ...ests_models_issue3184_WrongSourceCatch.txt | 21 ++++++ ...te.ba.tests_models_issue3184_Issue3184.txt | 36 ++++++++++ ...ba.tests_models_issue3184_MissingCatch.txt | 20 ++++++ ...tests_models_issue3184_MultipleSources.txt | 29 ++++++++ ...sts_models_issue3184_TimeoutConditions.txt | 39 +++++++++++ ...ests_models_issue3184_WrongSourceCatch.txt | 20 ++++++ ...te.ba.tests_models_issue3184_Issue3184.txt | 13 ++++ ...ba.tests_models_issue3184_MissingCatch.txt | 9 +++ ...tests_models_issue3184_MultipleSources.txt | 12 ++++ ...sts_models_issue3184_TimeoutConditions.txt | 27 +++++++ ...ests_models_issue3184_WrongSourceCatch.txt | 11 +++ .../analyzers/AadlBaLegalityRulesChecker.java | 70 +++++++++++++++++++ .../analyzers/AadlBaRulesCheckersDriver.java | 10 ++- 28 files changed, 450 insertions(+), 6 deletions(-) create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_Issue3184.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MissingCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_Issue3184.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MissingCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_Issue3184.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MissingCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_Issue3184.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MissingCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_Issue3184.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MissingCatch.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt diff --git a/ba/doc/conformance.md b/ba/doc/conformance.md index b1144f209dd..e0c10c50407 100644 --- a/ba/doc/conformance.md +++ b/ba/doc/conformance.md @@ -60,7 +60,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato | D.3: behavior specification | Variables, grouped states, state kinds, named/prioritized and multiple-source transitions, execute conditions, and a subset of dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions were absent (G01, since fixed) and the naming and otherwise-transition rules unenforced (V01 and V02, since fixed); mode binding is explicitly missing; multiple subprogram final states are rejected unconditionally; several consistency obligations lack demonstrated enforcement. | | D.4: thread dispatch | Dispatch conjunction/disjunction, `stop`, bare timeout, timeout with a duration, and an unparenthesized frozen-port list. Selected timeout/stop checks exist. | Partial. Required frozen-list parentheses were missing (G03) and timeout reset ports absent (G04), both since fixed. Full protocol/trigger compatibility and core-property consistency are not demonstrated. | | D.5: component interactions | Port send/dequeue/freeze, count/fresh, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` is absent; internal events were represented incorrectly (G10, since fixed); call-signature and direction/category checks need additional coverage. Input/output timing consistency is not established. | -| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, explicit-type loops, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers are missing; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); timeout, resource-release, and signature obligations are incomplete or unverified. | +| D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, explicit-type loops, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers are missing; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. | | D.7: expressions | Boolean/numeric/string syntax, arithmetic/relational/logical operators, property references, indexing, and operator applicability checks per operand data representation. | Partial, with semantic preservation defects. Operand consistency between the two operands is not checked, only applicability of the operator to the first one (G18). Short circuits and `updated` are missing; expression grouping/precedence and numeric translation differ from the document; initialization analysis is not demonstrated. | | D.8: synchronization | `Behavior_Properties::Subprogram_Call_Protocol` declares HSER/LSER/ASER and defaults to HSER, matching the supplied document. A client/server example exists. | Property definition conforms. Enforcement of the two LSER/ASER legality rules and execution of the protocols are not established. | @@ -186,7 +186,7 @@ These are bounded findings from the inspected grammar/translator/checker path. E | --- | --- | --- | | V01 | D.3 naming: variables, states, and transitions share uniqueness restrictions and must not conflict with relevant enclosing declarations, with the mode exception. | The Xtext validator has no explicit BA naming check; the translator's case-insensitive variable map overwrites duplicate keys. Its superclass validates properties, not the complete BA namespace rule. Verify ordinary AADL/core checks before assigning ownership of the missing diagnostics. Add duplicates across declaration kinds and enclosing feature/data/mode conflicts. **Implemented for [#3182](https://github.com/osate/osate2/issues/3182):** the validator checks the shared declaration namespace case-insensitively, including inherited features, data subcomponents, and modes, reports an error on each offending identifier, preserves the complete-state/mode exception, and checks names even when the classifier is unresolved. Translation keeps duplicate declarations but leaves an ambiguous reference unresolved instead of silently selecting the last one. `Issue3182Test` covers grouped and cross-kind duplicates, inherited declarations, component-type annexes, legal scope boundaries, unnamed transitions, and complete states representing modes. | | V02 | D.3 otherwise rules: no assigned priority and at most one otherwise transition per source state. | Implemented for [#3183](https://github.com/osate/osate2/issues/3183): report every conflicting otherwise transition as an error identifying its source state, including overlapping multi-source declarations. Explicit priorities produce a warning once per declaration, reflecting the standard's “should not” wording. `Issue3183Test` covers duplicates, source overlap, explicit zero and positive priorities, and valid otherwise transitions. | -| V03 | D.3 and D.6 action timeouts: a matching simple timeout transition from the same source; restrictions on combining an action timeout with timeout conditions. | Timeouts are stored by the translator, but `caseBehaviorActionBlock` processes only its content. No corresponding timeout/catch-pair analysis was found in the current driver/type checker. Test positive and negative pairs and dispatch-timeout/action-timeout combinations. | +| V03 | D.3 and D.6 action timeouts: a matching simple timeout transition from the same source; restrictions on combining an action timeout with timeout conditions. | Implemented for [#3184](https://github.com/osate/osate2/issues/3184): every top-level or nested action timeout is checked against each source of its transition for a same-source simple timeout catch. Action timeouts on execution-timeout, dispatch-relative-timeout, and completion-relative-timeout transitions are rejected. Diagnostics mark the behavior time and name a missing source state; `Issue3184Test` covers positive, missing, wrong-source, nested, expanded multi-source, and all three prohibited timeout-condition forms. | | V04 | D.3 nonblocking execution-state behavior. | The only consistency-checker method is the mode-related C4 check; no guard-exhaustiveness analysis is present there. The driver also comments out the call to the older `D_3_18_Checker`; that method's existence does not establish coverage. Distinguish general symbolic proof from simple detectable dead ends and clearly document any analysis limit. | | V05 | D.3 component-category/mode restrictions on external/internal conditions; behavior inheritance and replacement. | Conditions can be parsed generically, while type checking dispatches only execute conditions and the rules driver primarily dispatch conditions. Mode bindings are absent (G14), and the builder does not copy an in-modes context into the strict annex. Core AADL may retain mode applicability on the enclosing annex. Verify the complete consumer path before declaring inheritance or mode-specific selection unsupported. Cover thread/subprogram external-condition rejection and device condition mixing. | | V06 | D.4 protocol/trigger compatibility, legal trigger/frozen-port categories, and consistency with core dispatch/freeze properties. | The checker has dedicated timeout branches and a stop check, but no complete implementation of the document's protocol/trigger table was found. Dispatch references use generic `Reference` syntax. A rule implementing one timeout form is not evidence for all rows of the table. Test the matrix and invalid trigger direction/category through embedded source. | @@ -225,7 +225,7 @@ These are proposed follow-up changes, not changes made by this review. | 1 | ~~Repair the conformance test oracle and ensure deterministic BA validator registration. Separate legacy characterization from standard expectations.~~ **Done**, branch `repair_conformance_test_oracle` (commit `Repair the Behavior Annex conformance test oracle`). | Exact diagnostics are compared, by `expected/diagnostics` and the new `expected/diagnostics-validated`; registration is proved end to end by requiring at least one BA rule diagnostic in the validated suite and none in the plain baseline; both suites and the conformance class assert nonzero executed cases; the nine skips it left were listed in `TRACKED_SKIPS` against their own issues and enforced by reflection, and that list has shrunk to five as those issues closed; `SelfPropertyReference.aadl` no longer carries an unrelated D.3 error. Each repaired expectation was confirmed to fail for its intended reason by temporarily removing its `@Ignore`. | | 2 | Preserve strict-model meaning: numeric literals, array extents, logical grouping, `self`, internal events, and mode bindings (G08, G10–G14). **Under way:** G08, G10, and G11 are closed and G12's pull request is open; logical grouping (G13) and mode bindings (G14) remain. | External AADL input produces correct literal values, extents, references, operation kinds, and mode links; no test-only model mutation is needed. Assert attributes and semantic structure directly. | | 3 | Implement the missing standard syntax and remove unwanted overacceptance (G01–G07, G09, G13). **Under way:** G01, G03, and G04 are closed; G02, G05, G06, G07, G09, and G13 remain. | Each standard form parses and translates; nonstandard forms have deliberate rejection/extension policy. Enable corrected standard acceptance tests and add AST/strict-model expression tests. | -| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16, V01, and V02 are closed; G15, G17, G18, V03, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. | +| 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16 and V01–V03 are addressed; G15, G17, G18, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. | | 5 | Establish behavioral/dataflow coverage and consumer boundaries (V04–V05, V08–V09, D.5 and D.8 runtime semantics). | State which obligations the front end can prove, which are warnings/approximations, and which belong to a simulator, analyzer, or generator. Validate queue behavior, timeouts, lock lifetimes, initialization, and call synchronization in the responsible consumer. | There is no basis here for a numerical conformance percentage: the suite is not a clause-complete standard test suite, some assertions are ineffective, and operational semantics were outside the executed scope. A defensible future claim should distinguish syntax acceptance, valid strict-model construction, legality/consistency enforcement, and downstream execution semantics. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_Issue3184.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_Issue3184.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MissingCatch.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MissingCatch.txt new file mode 100644 index 00000000000..44e1f9640e9 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MissingCatch.txt @@ -0,0 +1,2 @@ +error | semantic | 35 | 53 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed. +error | semantic | 35 | 67 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MultipleSources.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MultipleSources.txt new file mode 100644 index 00000000000..839e2297474 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_MultipleSources.txt @@ -0,0 +1 @@ +error | semantic | 37 | 60 | 4 | A behavior action timeout must have a transition from source state 'second' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt new file mode 100644 index 00000000000..9d980ab8556 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt @@ -0,0 +1,3 @@ +error | semantic | 35 | 55 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed. +error | semantic | 51 | 69 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed. +error | semantic | 61 | 74 | 4 | A behavior action timeout is not allowed on a transition with a timeout condition : Behavior Annex D.3 and D.6 legality rules failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt new file mode 100644 index 00000000000..632aea485c8 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt @@ -0,0 +1 @@ +error | semantic | 36 | 55 | 4 | A behavior action timeout must have a transition from source state 'start' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_Issue3184.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_Issue3184.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MissingCatch.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MissingCatch.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MultipleSources.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_MultipleSources.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_Issue3184.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_Issue3184.txt new file mode 100644 index 00000000000..1bd3b074851 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_Issue3184.txt @@ -0,0 +1,35 @@ +annex[0] owner=Issue3184::example.impl + (BehaviorActionBlock, , 1977, 33) + (BehaviorActionBlock, , 2061, 35) + (BehaviorActionBlock, , 2062, 33) + (BehaviorAnnex, behavior_specification, 1872, 252) + (BehaviorBooleanLiteral, , 1962, 4) + (BehaviorBooleanLiteral, , 2048, 4) + (BehaviorCondition, , 1962, 4) + (BehaviorCondition, , 2021, 7) + (BehaviorCondition, , 2048, 4) + (BehaviorCondition, , 2108, 7) + (BehaviorIntegerLiteral, , 1991, 1) + (BehaviorIntegerLiteral, , 2006, 1) + (BehaviorIntegerLiteral, , 2076, 1) + (BehaviorIntegerLiteral, , 2091, 1) + (BehaviorState, done, 1921, 4) + (BehaviorState, nested, 1904, 6) + (BehaviorState, start, 1880, 5) + (BehaviorStateGroup, , 1880, 22) + (BehaviorStateGroup, , 1904, 15) + (BehaviorStateGroup, , 1921, 19) + (BehaviorTime, , 1991, 4) + (BehaviorTime, , 2006, 4) + (BehaviorTime, , 2076, 4) + (BehaviorTime, , 2091, 4) + (BehaviorTransition, , 1954, 57) + (BehaviorTransition, , 2013, 24) + (BehaviorTransition, , 2039, 58) + (BehaviorTransition, , 2099, 25) + (ExecuteCondition, , 1962, 4) + (ExecuteCondition, , 2021, 7) + (ExecuteCondition, , 2048, 4) + (ExecuteCondition, , 2108, 7) + (TimedAction, , 1978, 18) + (TimedAction, , 2063, 18) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MissingCatch.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MissingCatch.txt new file mode 100644 index 00000000000..dbda293f51e --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MissingCatch.txt @@ -0,0 +1,19 @@ +annex[0] owner=MissingCatch::example.impl + (BehaviorActionBlock, , 1961, 48) + (BehaviorActionBlock, , 1962, 33) + (BehaviorAnnex, behavior_specification, 1875, 135) + (BehaviorBooleanLiteral, , 1948, 4) + (BehaviorCondition, , 1948, 4) + (BehaviorIntegerLiteral, , 1976, 1) + (BehaviorIntegerLiteral, , 1991, 1) + (BehaviorIntegerLiteral, , 2005, 1) + (BehaviorState, done, 1907, 4) + (BehaviorState, start, 1883, 5) + (BehaviorStateGroup, , 1883, 22) + (BehaviorStateGroup, , 1907, 19) + (BehaviorTime, , 1976, 4) + (BehaviorTime, , 1991, 4) + (BehaviorTime, , 2005, 4) + (BehaviorTransition, , 1940, 70) + (ExecuteCondition, , 1948, 4) + (TimedAction, , 1963, 18) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MultipleSources.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MultipleSources.txt new file mode 100644 index 00000000000..752bc5b176a --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_MultipleSources.txt @@ -0,0 +1,23 @@ +annex[0] owner=MultipleSources::example.impl + (BehaviorActionBlock, , 2016, 33) + (BehaviorAnnex, behavior_specification, 1878, 198) + (BehaviorBooleanLiteral, , 2003, 4) + (BehaviorCondition, , 2003, 4) + (BehaviorCondition, , 2060, 7) + (BehaviorIntegerLiteral, , 2030, 1) + (BehaviorIntegerLiteral, , 2045, 1) + (BehaviorState, done, 1934, 4) + (BehaviorState, first, 1910, 5) + (BehaviorState, second, 1917, 6) + (BehaviorState, start, 1886, 5) + (BehaviorStateGroup, , 1886, 22) + (BehaviorStateGroup, , 1910, 22) + (BehaviorStateGroup, , 1934, 19) + (BehaviorTime, , 2030, 4) + (BehaviorTime, , 2045, 4) + (BehaviorTransition, , 1967, 18) + (BehaviorTransition, , 1987, 63) + (BehaviorTransition, , 2052, 24) + (ExecuteCondition, , 2003, 4) + (ExecuteCondition, , 2060, 7) + (TimedAction, , 2017, 18) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt new file mode 100644 index 00000000000..67e85916009 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt @@ -0,0 +1,49 @@ +annex[0] owner=TimeoutConditions::operation.impl + (BehaviorActionBlock, , 1975, 33) + (BehaviorAnnex, behavior_specification, 1886, 123) + (BehaviorCondition, , 1959, 7) + (BehaviorIntegerLiteral, , 1989, 1) + (BehaviorIntegerLiteral, , 2004, 1) + (BehaviorState, done, 1918, 4) + (BehaviorState, start, 1894, 5) + (BehaviorStateGroup, , 1894, 22) + (BehaviorStateGroup, , 1918, 19) + (BehaviorTime, , 1989, 4) + (BehaviorTime, , 2004, 4) + (BehaviorTransition, , 1951, 58) + (ExecuteCondition, , 1959, 7) + (TimedAction, , 1976, 18) +annex[1] owner=TimeoutConditions::worker.dispatch_relative + (BehaviorActionBlock, , 2324, 33) + (BehaviorAnnex, behavior_specification, 2201, 157) + (BehaviorCondition, , 2296, 19) + (BehaviorIntegerLiteral, , 2338, 1) + (BehaviorIntegerLiteral, , 2353, 1) + (BehaviorState, done, 2244, 4) + (BehaviorState, waiting, 2209, 7) + (BehaviorStateGroup, , 2209, 33) + (BehaviorStateGroup, , 2244, 28) + (BehaviorTime, , 2338, 4) + (BehaviorTime, , 2353, 4) + (BehaviorTransition, , 2286, 72) + (DispatchCondition, , 2299, 16) + (DispatchTriggerCondition, , 2308, 7) + (TimedAction, , 2325, 18) +annex[2] owner=TimeoutConditions::worker.completion_relative + (BehaviorActionBlock, , 2605, 33) + (BehaviorAnnex, behavior_specification, 2477, 162) + (BehaviorCondition, , 2572, 24) + (BehaviorIntegerLiteral, , 2592, 1) + (BehaviorIntegerLiteral, , 2619, 1) + (BehaviorIntegerLiteral, , 2634, 1) + (BehaviorState, done, 2520, 4) + (BehaviorState, waiting, 2485, 7) + (BehaviorStateGroup, , 2485, 33) + (BehaviorStateGroup, , 2520, 28) + (BehaviorTime, , 2592, 4) + (BehaviorTime, , 2619, 4) + (BehaviorTime, , 2634, 4) + (BehaviorTransition, , 2562, 77) + (DispatchCondition, , 2575, 21) + (DispatchTriggerCondition, , 2584, 12) + (TimedAction, , 2606, 18) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt new file mode 100644 index 00000000000..1c29232efaa --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt @@ -0,0 +1,21 @@ +annex[0] owner=WrongSourceCatch::example.impl + (BehaviorActionBlock, , 1986, 33) + (BehaviorAnnex, behavior_specification, 1879, 169) + (BehaviorBooleanLiteral, , 1970, 4) + (BehaviorCondition, , 1970, 4) + (BehaviorCondition, , 2032, 7) + (BehaviorIntegerLiteral, , 2000, 1) + (BehaviorIntegerLiteral, , 2015, 1) + (BehaviorState, done, 1929, 4) + (BehaviorState, running, 1911, 7) + (BehaviorState, start, 1887, 5) + (BehaviorStateGroup, , 1887, 22) + (BehaviorStateGroup, , 1911, 16) + (BehaviorStateGroup, , 1929, 19) + (BehaviorTime, , 2000, 4) + (BehaviorTime, , 2015, 4) + (BehaviorTransition, , 1962, 58) + (BehaviorTransition, , 2022, 26) + (ExecuteCondition, , 1970, 4) + (ExecuteCondition, , 2032, 7) + (TimedAction, , 1987, 18) diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_Issue3184.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_Issue3184.txt new file mode 100644 index 00000000000..829e211cb69 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_Issue3184.txt @@ -0,0 +1,36 @@ +annex[0] owner=Issue3184::example.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=start + states[1] : BehaviorState name=nested + states[2] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : ValueExpression + relations[0] : Relation + firstExpression : SimpleExpression + terms[0] : Term + factors[0] : Factor + firstValue : BehaviorBooleanLiteral + transitions[1] : BehaviorTransition + condition : ExecutionTimeoutCatch + transitions[2] : BehaviorTransition + condition : ValueExpression + relations[0] : Relation + firstExpression : SimpleExpression + terms[0] : Term + factors[0] : Factor + firstValue : BehaviorBooleanLiteral + transitions[3] : BehaviorTransition + condition : ExecutionTimeoutCatch + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral + actions[1] : BehaviorActionBlock + content : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MissingCatch.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MissingCatch.txt new file mode 100644 index 00000000000..a6e1b8ce654 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MissingCatch.txt @@ -0,0 +1,20 @@ +annex[0] owner=MissingCatch::example.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=start + states[1] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : ValueExpression + relations[0] : Relation + firstExpression : SimpleExpression + terms[0] : Term + factors[0] : Factor + firstValue : BehaviorBooleanLiteral + actions[0] : BehaviorActionBlock + content : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MultipleSources.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MultipleSources.txt new file mode 100644 index 00000000000..1747afb6e22 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_MultipleSources.txt @@ -0,0 +1,29 @@ +annex[0] owner=MultipleSources::example.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=start + states[1] : BehaviorState name=first + states[2] : BehaviorState name=second + states[3] : 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 + transitions[3] : BehaviorTransition + condition : ExecutionTimeoutCatch + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt new file mode 100644 index 00000000000..f9d120a9dbd --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt @@ -0,0 +1,39 @@ +annex[0] owner=TimeoutConditions::operation.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=start + states[1] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : ExecutionTimeoutCatch + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral +annex[1] owner=TimeoutConditions::worker.dispatch_relative + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=waiting + states[1] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : DispatchRelativeTimeout + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral +annex[2] owner=TimeoutConditions::worker.completion_relative + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=waiting + states[1] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : CompletionRelativeTimeout + integerValue : BehaviorIntegerLiteral + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt new file mode 100644 index 00000000000..ceb35378cd1 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt @@ -0,0 +1,20 @@ +annex[0] owner=WrongSourceCatch::example.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=start + states[1] : BehaviorState name=running + states[2] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : ValueExpression + relations[0] : Relation + firstExpression : SimpleExpression + terms[0] : Term + factors[0] : Factor + firstValue : BehaviorBooleanLiteral + transitions[1] : BehaviorTransition + condition : ExecutionTimeoutCatch + actions[0] : BehaviorActionBlock + content : TimedAction + lowerTime : BehaviorTime + integerValue : BehaviorIntegerLiteral + timeout : BehaviorTime + integerValue : BehaviorIntegerLiteral diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_Issue3184.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_Issue3184.txt new file mode 100644 index 00000000000..55a6bde9fd6 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_Issue3184.txt @@ -0,0 +1,13 @@ +===== annex[0] owner=Issue3184::example.impl ===== + +states +\tstart : initial state; +\tnested : state; +\tdone : final state; +transitions +\tstart -[true]-> nested {computation (1 ms)} timeout 2 ms; +\tstart -[timeout]-> done; +\tnested -[true]-> done {{computation (1 ms)} timeout 3 ms}; +\tnested -[timeout]-> done; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MissingCatch.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MissingCatch.txt new file mode 100644 index 00000000000..4ace867cb12 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MissingCatch.txt @@ -0,0 +1,9 @@ +===== annex[0] owner=MissingCatch::example.impl ===== + +states +\tstart : initial state; +\tdone : final state; +transitions +\tstart -[true]-> done {{computation (1 ms)} timeout 3 ms} timeout 2 ms; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MultipleSources.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MultipleSources.txt new file mode 100644 index 00000000000..9b2bd5cd86c --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_MultipleSources.txt @@ -0,0 +1,12 @@ +===== annex[0] owner=MultipleSources::example.impl ===== + +states +\tstart : initial state; +\tfirst, second : state; +\tdone : final state; +transitions +\tstart -[]-> first; +\tfirst, second -[true]-> done {computation (1 ms)} timeout 2 ms; +\tfirst -[timeout]-> done; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt new file mode 100644 index 00000000000..11624289ea5 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_TimeoutConditions.txt @@ -0,0 +1,27 @@ +===== annex[0] owner=TimeoutConditions::operation.impl ===== + +states +\tstart : initial state; +\tdone : final state; +transitions +\tstart -[timeout]-> done {computation (1 ms)} timeout 2 ms; +----- Xtext reparse ----- +reparsed +===== annex[1] owner=TimeoutConditions::worker.dispatch_relative ===== + +states +\twaiting : initial complete state; +\tdone : complete final state; +transitions +\twaiting -[on dispatch timeout]-> done {computation (1 ms)} timeout 3 ms; +----- Xtext reparse ----- +reparsed +===== annex[2] owner=TimeoutConditions::worker.completion_relative ===== + +states +\twaiting : initial complete state; +\tdone : complete final state; +transitions +\twaiting -[on dispatch timeout 5 ms]-> done {computation (1 ms)} timeout 4 ms; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt new file mode 100644 index 00000000000..5db24b877e7 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3184_WrongSourceCatch.txt @@ -0,0 +1,11 @@ +===== annex[0] owner=WrongSourceCatch::example.impl ===== + +states +\tstart : initial state; +\trunning : state; +\tdone : final state; +transitions +\tstart -[true]-> running {computation (1 ms)} timeout 2 ms; +\trunning -[timeout]-> done; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java index bd66888c563..a6e49a5888c 100644 --- a/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java +++ b/ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java @@ -63,6 +63,7 @@ import org.osate.ba.aadlba.DispatchCondition; import org.osate.ba.aadlba.DispatchRelativeTimeout; import org.osate.ba.aadlba.ElseStatement; +import org.osate.ba.aadlba.ExecutionTimeoutCatch; import org.osate.ba.aadlba.IfStatement; import org.osate.ba.aadlba.IntegerValue; import org.osate.ba.aadlba.InternalCondition; @@ -690,6 +691,75 @@ public boolean D_6_L3_And_L4_Check(BehaviorActionBlock bab) { return lDuplicates.isEmpty(); } + /** + * Document: AS5506/3 Rev A + * Type : Legality rule + * Sections: D.3 Behavior Specification, D.6 Behavior Action Language + * Object : Check action timeout catch and transition-condition rules + * Keys : action timeout simple timeout condition source state + * + * Every timeout-bearing action block is checked against the transition that contains it. The translator expands a + * declarative multi-source transition into one strict transition per source while sharing the action block, so the + * driver calls this method for every expanded transition. This ensures that every source has its own timeout-catch + * transition. + */ + public boolean D_3_And_D_6_Action_Timeout_Check(BehaviorTransition transition) { + var actionBlock = transition.getActionBlock(); + if (actionBlock == null) { + return true; + } + + var timedBlocks = new ArrayList(); + if (actionBlock.getTimeout() != null) { + timedBlocks.add(actionBlock); + } + for (var contents = EcoreUtil.getAllContents(actionBlock, true); contents.hasNext();) { + if (contents.next() instanceof BehaviorActionBlock nestedBlock && nestedBlock.getTimeout() != null) { + timedBlocks.add(nestedBlock); + } + } + if (timedBlocks.isEmpty()) { + return true; + } + + if (hasTimeoutCondition(transition)) { + for (var timedBlock : timedBlocks) { + reportLegalityError(timedBlock.getTimeout(), + "A behavior action timeout is not allowed on a transition with a timeout condition : " + + "Behavior Annex D.3 and D.6 legality rules failed"); + } + return false; + } + + var source = transition.getSourceState(); + var hasCatch = source != null && _ba.getTransitions() + .stream() + .anyMatch(candidate -> candidate.getSourceState() == source + && candidate.getCondition() instanceof ExecutionTimeoutCatch); + if (hasCatch) { + return true; + } + + var sourceName = source == null ? "" : source.getName(); + for (var timedBlock : timedBlocks) { + reportLegalityError(timedBlock.getTimeout(), + "A behavior action timeout must have a transition from source state '" + sourceName + + "' with a simple timeout condition : Behavior Annex D.3 and D.6 legality rules failed"); + } + return false; + } + + private static boolean hasTimeoutCondition(BehaviorTransition transition) { + if (transition.getCondition() instanceof ExecutionTimeoutCatch) { + return true; + } + if (transition.getCondition() instanceof DispatchCondition dispatch) { + var trigger = dispatch.getDispatchTriggerCondition(); + return trigger instanceof DispatchRelativeTimeout || trigger instanceof CompletionRelativeTimeout; + } + return false; + } + /** * Recursively builds a list of assigned target contained * in a given BehaviorActions tree and checks for duplicated targets every time 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 404fdd3954f..5602a436834 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 @@ -248,10 +248,14 @@ private boolean checkBehaviorTransition(BehaviorTransition tmp, Set