From 6265e23bb2bc9f2f63914162070813dd4c3925ed Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 18 Sep 2026 12:33:00 -0400 Subject: [PATCH 1/2] Add regression test for issue #2804 Check that EMV2 behavior state machines reject zero or multiple initial states, including a machine with no states. Preserve acceptance of exactly one initial state regardless of declaration order using a separate valid model. --- .../models/issue2804/.gitignore | 2 + .../models/issue2804/.project | 18 +++++ .../models/issue2804/Issue2804.aadl | 21 ++++++ .../models/issue2804/ValidInitialStates.aadl | 16 ++++ .../tests/issues/Issue2804Test.java | 74 +++++++++++++++++++ 5 files changed, 131 insertions(+) create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.gitignore create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.project create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2804/Issue2804.aadl create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2804/ValidInitialStates.aadl create mode 100644 emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2804Test.java diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.gitignore b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.gitignore new file mode 100644 index 00000000000..afce51184c6 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.gitignore @@ -0,0 +1,2 @@ +/.aadlbin-gen/ +/instances/ diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.project b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.project new file mode 100644 index 00000000000..e253780d3a6 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/.project @@ -0,0 +1,18 @@ + + + issue2804 + + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + + org.osate.core.aadlnature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/Issue2804.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/Issue2804.aadl new file mode 100644 index 00000000000..85b5a38b3c1 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/Issue2804.aadl @@ -0,0 +1,21 @@ +package Issue2804 +public + annex EMV2 {** + error behavior no_initial + states + one: state; + two: state; + three: state; + end behavior; + + error behavior multiple_initial + states + a: initial state; + b: state; + c: initial state; + end behavior; + + error behavior no_states + end behavior; + **}; +end Issue2804; diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/ValidInitialStates.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/ValidInitialStates.aadl new file mode 100644 index 00000000000..5bbe655097f --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2804/ValidInitialStates.aadl @@ -0,0 +1,16 @@ +package ValidInitialStates +public + annex EMV2 {** + error behavior one_state + states + only: initial state; + end behavior; + + error behavior initial_not_first + states + one: state; + two: initial state; + three: state; + end behavior; + **}; +end ValidInitialStates; diff --git a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2804Test.java b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2804Test.java new file mode 100644 index 00000000000..5e8c3094332 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2804Test.java @@ -0,0 +1,74 @@ +/** + * 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.aadl2.errormodel.tests.issues; + +import java.util.ArrayList; + +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.aadl2.DefaultAnnexLibrary; +import org.osate.aadl2.errormodel.tests.ErrorModelInjectorProvider; +import org.osate.testsupport.AssertHelper; +import org.osate.testsupport.TestHelper; +import org.osate.xtext.aadl2.errormodel.errorModel.ErrorModelLibrary; + +import com.google.inject.Inject; +import com.itemis.xtext.testing.FluentIssueCollection; +import com.itemis.xtext.testing.XtextTest; + +@RunWith(XtextRunner.class) +@InjectWith(ErrorModelInjectorProvider.class) +public class Issue2804Test extends XtextTest { + private static final String PROJECT_LOCATION = "org.osate.aadl2.errormodel.tests/models/issue2804/"; + + @Inject + private TestHelper testHelper; + + @Inject + private ValidationTestHelper validationHelper; + + @Test + public void rejectMissingAndMultipleInitialStates() throws Exception { + var result = issues = testHelper.testFile(PROJECT_LOCATION + "Issue2804.aadl"); + var expected = new FluentIssueCollection(result.getResource(), new ArrayList<>(), new ArrayList<>()); + var pkg = (AadlPackage) result.getResource().getContents().getFirst(); + var library = (ErrorModelLibrary) ((DefaultAnnexLibrary) pkg.getPublicSection().getOwnedAnnexLibraries() + .getFirst()).getParsedAnnexLibrary(); + for (var behavior : library.getBehaviors()) { + AssertHelper.assertError(behavior, result.getIssues(), expected, + "Error behavior state machine must have exactly one initial state"); + } + expected.sizeIs(3); + assertConstraints(expected); + } + + @Test + public void acceptExactlyOneInitialState() { + validationHelper.assertNoIssues(testHelper.parseFile(PROJECT_LOCATION + "ValidInitialStates.aadl")); + } +} From a83851f85901d3b01e69acc1087a6448cda250e1 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 18 Sep 2026 12:37:20 -0400 Subject: [PATCH 2/2] Require one initial EMV2 behavior state Enforce E.8 legality rule L32 by requiring exactly one initial state in each error behavior state machine. Add missing initial declarations in four existing test fixtures so their transition and scoping assertions remain isolated from this new check. --- .../models/Issue2579/emv-transition.aadl | 4 ++-- .../tests/errormodelscopeprovider/EMV2PathElementTest.java | 2 +- .../OtherErrorModelScopeProviderTest.java | 2 ++ .../tests/errormodelscopeprovider/PropertyReferenceTest.java | 2 +- .../aadl2/errormodel/validation/ErrorModelValidator.java | 3 +++ 5 files changed, 9 insertions(+), 4 deletions(-) diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/Issue2579/emv-transition.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/Issue2579/emv-transition.aadl index dd5a2e4fb2a..b2215482891 100644 --- a/emv2/org.osate.aadl2.errormodel.tests/models/Issue2579/emv-transition.aadl +++ b/emv2/org.osate.aadl2.errormodel.tests/models/Issue2579/emv-transition.aadl @@ -5,7 +5,7 @@ public events ev: error event; states - s: state {ErrorLibrary::CommonErrors}; + s: initial state {ErrorLibrary::CommonErrors}; end behavior; **}; @@ -24,4 +24,4 @@ public end component; **}; end S; -end emv::transition; \ No newline at end of file +end emv::transition; diff --git a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/EMV2PathElementTest.java b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/EMV2PathElementTest.java index eefa1d1232e..d5fd060b4ca 100644 --- a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/EMV2PathElementTest.java +++ b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/EMV2PathElementTest.java @@ -1198,7 +1198,7 @@ public void testBasicEMV2PropertyAssociationInErrorBehaviorStateMachine() throws \t\tevents \t\t\tevt1: error event; \t\tstates - \t\t\tstate1: state; + \t\t\tstate1: initial state; \t\ttransitions \t\t\ttrans1: all -[ evt1 ]-> same state; \t\tproperties diff --git a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/OtherErrorModelScopeProviderTest.java b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/OtherErrorModelScopeProviderTest.java index e5cde6b9f17..92f26b696c8 100644 --- a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/OtherErrorModelScopeProviderTest.java +++ b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/OtherErrorModelScopeProviderTest.java @@ -108,6 +108,8 @@ public void testErrorModelLibraryReference() throws Exception { \t\terror behavior b \t\t\tuse types ErrorLibrary; \t\t\tuse transformations t; + \t\tstates + \t\t\tstate1: initial state; \t\tend behavior; \t\t \t\ttype mappings m diff --git a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/PropertyReferenceTest.java b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/PropertyReferenceTest.java index 32ed305c791..e461494df98 100644 --- a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/PropertyReferenceTest.java +++ b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/errormodelscopeprovider/PropertyReferenceTest.java @@ -85,7 +85,7 @@ public void testBranchValue() throws Exception { \t\tevents \t\t\terr_evt1: error event; \t\tstates - \t\t\tbvr_state1: state; + \t\t\tbvr_state1: initial state; \t\t\tbvr_state2: state; \t\ttransitions \t\t\ttransition1: bvr_state1 -[ err_evt1 ]-> (bvr_state2 with 0.2_0, bvr_state2 with ps1::def1); diff --git a/emv2/org.osate.xtext.aadl2.errormodel/src/org/osate/xtext/aadl2/errormodel/validation/ErrorModelValidator.java b/emv2/org.osate.xtext.aadl2.errormodel/src/org/osate/xtext/aadl2/errormodel/validation/ErrorModelValidator.java index b8acd26436b..de4aece7095 100644 --- a/emv2/org.osate.xtext.aadl2.errormodel/src/org/osate/xtext/aadl2/errormodel/validation/ErrorModelValidator.java +++ b/emv2/org.osate.xtext.aadl2.errormodel/src/org/osate/xtext/aadl2/errormodel/validation/ErrorModelValidator.java @@ -354,6 +354,9 @@ public void caseErrorModelLibrary(ErrorModelLibrary errorModelLibrary) { @Check(CheckType.FAST) public void caseErrorBehaviorStateMachine(ErrorBehaviorStateMachine ebsm) { checkUniqueEBSMElements(ebsm); + if (ebsm.getStates().stream().filter(ErrorBehaviorState::isIntial).count() != 1) { + error(ebsm, "Error behavior state machine must have exactly one initial state"); + } } @Check(CheckType.FAST)