From 7bb4893144e5364dac2d49d804dd19f5585f8251 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 18 Sep 2026 13:01:29 -0400 Subject: [PATCH 1/2] Add regression test for issue #2821 Cover undefined branch probability properties supplied through extension or containment and deferred library-state-machine probabilities. Require structural duplicate-branch diagnostics and fully known sum checks to remain active. --- .../models/issue2821/.gitignore | 2 + .../models/issue2821/.project | 18 +++++ .../models/issue2821/InvalidBranches.aadl | 57 +++++++++++++ .../models/issue2821/Issue2821.aadl | 79 ++++++++++++++++++ .../issue2821/ProbabilityProperties.aadl | 3 + .../tests/issues/Issue2821Test.java | 81 +++++++++++++++++++ 6 files changed, 240 insertions(+) create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.gitignore create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.project create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2821/InvalidBranches.aadl create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2821/Issue2821.aadl create mode 100644 emv2/org.osate.aadl2.errormodel.tests/models/issue2821/ProbabilityProperties.aadl create mode 100644 emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2821Test.java diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.gitignore b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.gitignore new file mode 100644 index 00000000000..afce51184c6 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.gitignore @@ -0,0 +1,2 @@ +/.aadlbin-gen/ +/instances/ diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.project b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.project new file mode 100644 index 00000000000..a79a1d80a57 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/.project @@ -0,0 +1,18 @@ + + + issue2821 + + + + + + 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/issue2821/InvalidBranches.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/InvalidBranches.aadl new file mode 100644 index 00000000000..c6be4d0fee7 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/InvalidBranches.aadl @@ -0,0 +1,57 @@ +package InvalidBranches +public + with ProbabilityProperties, Issue2821; + + system duplicate_same + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (same state with ProbabilityProperties::probability, same state with 0.125); + end component; + **}; + end duplicate_same; + + system duplicate_others + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with ProbabilityProperties::probability, same state with others, state3 with others); + end component; + **}; + end duplicate_others; + + system known_property + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 0.125, state3 with ProbabilityProperties::probability); + end component; + properties + ProbabilityProperties::probability => 0.5 applies to t; + **}; + end known_property; + + system known_literals + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 0.125, state3 with 0.5); + end component; + **}; + end known_literals; + + system exhausted_remainder + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 1.0, same state with others); + end component; + **}; + end exhausted_remainder; + +end InvalidBranches; diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/Issue2821.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/Issue2821.aadl new file mode 100644 index 00000000000..56bd0a87755 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/Issue2821.aadl @@ -0,0 +1,79 @@ +package Issue2821 +public + with ProbabilityProperties; + + system s + end s; + + system implementation s.base + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 0.125, state3 with ProbabilityProperties::probability); + end component; + **}; + end s.base; + + system implementation s.extended extends s.base + annex EMV2 {** + properties + ProbabilityProperties::probability => 0.875 applies to t; + **}; + end s.extended; + + system container + end container; + + system implementation container.i + subcomponents + child: system s.base; + annex EMV2 {** + properties + ProbabilityProperties::probability => 0.875 applies to ^child@t; + **}; + end container.i; + + system known_value + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 0.125, state3 with ProbabilityProperties::probability); + end component; + properties + ProbabilityProperties::probability => 0.875 applies to t; + **}; + end known_value; + + system unknown_with_others + annex EMV2 {** + use behavior Issue2821::machine; + component error behavior + transitions + t: state1 -[event1]-> (state2 with 0.125, state3 with ProbabilityProperties::probability, same state with others); + end component; + **}; + end unknown_with_others; + + annex EMV2 {** + error behavior machine + events + event1: error event; + states + state1: initial state; + state2: state; + state3: state; + end behavior; + + error behavior deferred + events + event1: error event; + states + state1: initial state; + state2: state; + transitions + t: state1 -[event1]-> (state2 with 0.125, same state with ProbabilityProperties::probability); + end behavior; + **}; +end Issue2821; diff --git a/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/ProbabilityProperties.aadl b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/ProbabilityProperties.aadl new file mode 100644 index 00000000000..419ecc2aae4 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/models/issue2821/ProbabilityProperties.aadl @@ -0,0 +1,3 @@ +property set ProbabilityProperties is + probability: aadlreal applies to (all); +end ProbabilityProperties; diff --git a/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2821Test.java b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2821Test.java new file mode 100644 index 00000000000..90394083663 --- /dev/null +++ b/emv2/org.osate.aadl2.errormodel.tests/src/org/osate/aadl2/errormodel/tests/issues/Issue2821Test.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.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.DefaultAnnexSubclause; +import org.osate.aadl2.errormodel.tests.ErrorModelInjectorProvider; +import org.osate.testsupport.AssertHelper; +import org.osate.testsupport.TestHelper; +import org.osate.xtext.aadl2.errormodel.errorModel.ErrorModelSubclause; + +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 Issue2821Test extends XtextTest { + private static final String PROJECT_LOCATION = "org.osate.aadl2.errormodel.tests/models/issue2821/"; + private static final String PROPERTIES = PROJECT_LOCATION + "ProbabilityProperties.aadl"; + + @Inject + private TestHelper testHelper; + + @Inject + private ValidationTestHelper validationHelper; + + @Test + public void allowProbabilitiesSuppliedInLaterContexts() { + validationHelper.assertNoIssues(testHelper.parseFile(PROJECT_LOCATION + "Issue2821.aadl", PROPERTIES)); + } + + @Test + public void preserveStructuralChecksAndKnownProbabilitySums() throws Exception { + var result = issues = testHelper.testFile(PROJECT_LOCATION + "InvalidBranches.aadl", PROPERTIES, + PROJECT_LOCATION + "Issue2821.aadl"); + var expected = new FluentIssueCollection(result.getResource(), new ArrayList<>(), new ArrayList<>()); + var pkg = (AadlPackage) result.getResource().getContents().getFirst(); + for (var classifier : pkg.getPublicSection().getOwnedClassifiers()) { + var annex = (ErrorModelSubclause) ((DefaultAnnexSubclause) classifier.getOwnedAnnexSubclauses().getFirst()) + .getParsedAnnexSubclause(); + var message = switch (classifier.getName()) { + case "duplicate_same" -> "More than one same state branch"; + case "duplicate_others" -> "More than one other branch"; + case "exhausted_remainder" -> "Sum of branch probabilities must be less than 1 due to 'others'"; + default -> "Sum of branch probabilities must be 1"; + }; + AssertHelper.assertError(annex.getTransitions().getFirst(), result.getIssues(), expected, message); + } + expected.sizeIs(5); + assertConstraints(expected); + } +} From dddaed4c59d448aba5b35261d9bc6a565884a881 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Fri, 18 Sep 2026 13:07:10 -0400 Subject: [PATCH 2/2] Defer sums for undefined branch probabilities Skip probability-total checks when a referenced property has no value in the current context, allowing extension and containment to supply it later. Continue structural branch checks and known sums, and update the scope test that expected the old false diagnostic. --- .../errormodelscopeprovider/PropertyReferenceTest.java | 3 +-- .../aadl2/errormodel/validation/ErrorModelValidator.java | 7 +++++++ 2 files changed, 8 insertions(+), 2 deletions(-) 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 e461494df98..3d1301d5ff7 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 @@ -253,8 +253,7 @@ public void testBranchValue() throws Exception { Assert.assertEquals("bvr", errorBehaviorStateMachine.getName()); var errorBehaviorTransition = (errorBehaviorStateMachine.getTransitions()).getFirst(); Assert.assertEquals("transition1", errorBehaviorTransition.getName()); - AssertHelper.assertError(errorBehaviorTransition, lib1TestResult.getIssues(), lib1IssueCollection, - "Sum of branch probabilities must be 1"); + // The library leaves the probability undefined so a using classifier can supply it. this.assertHelper.assertScope(errorBehaviorTransition.getDestinationBranches().get(1).getValue(), ErrorModelPackage.eINSTANCE.getBranchValue_Symboliclabel(), expectedScope); 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 e00cc0c909d..0e73d130bad 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 @@ -1096,6 +1096,7 @@ private void checkBranches(ErrorBehaviorTransition ebt) { EList branches = ebt.getDestinationBranches(); boolean foundsteady = false; boolean foundothers = false; + boolean allProbabilitiesKnown = true; BigDecimal prob = new BigDecimal(0.0, MathContext.UNLIMITED); if (branches.isEmpty()) { return; @@ -1122,12 +1123,18 @@ private void checkBranches(ErrorBehaviorTransition ebt) { } else if (sl != null) { Classifier cl = EMV2Util.getAssociatedClassifier(ebt); List pa = EMV2Properties.getProperty(sl.getQualifiedName(), cl, ebt, null); + if (pa.isEmpty()) { + allProbabilitiesKnown = false; + } for (EMV2PropertyAssociation emv2PropertyAssociation : pa) { prob = prob.add(new BigDecimal(EMV2Properties.getRealValue(emv2PropertyAssociation), MathContext.UNLIMITED)); } } } + if (!allProbabilitiesKnown) { + return; + } if (!foundothers && prob.compareTo(new BigDecimal(1.0)) != 0) { error(ebt, "Sum of branch probabilities must be 1"); }