Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions ba/org.osate.xtext.aadl2.ba.tests/models/issue3244/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
/.aadlbin-gen/
/instances/
16 changes: 16 additions & 0 deletions ba/org.osate.xtext.aadl2.ba.tests/models/issue3244/.project
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>issue3244</name>
<comment></comment>
<projects></projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
<arguments></arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.osate.core.aadlnature</nature>
<nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
</natures>
</projectDescription>
64 changes: 64 additions & 0 deletions ba/org.osate.xtext.aadl2.ba.tests/models/issue3244/Issue3244.aadl
Original file line number Diff line number Diff line change
@@ -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 Issue3244
public
with Base_Types;

thread worker
features
outgoing : out event port;
end worker;

thread implementation worker.invalid
annex behavior_specification {**
variables
amount : Base_Types::Integer;
values[amount] : Base_Types::Integer;
flag : Base_Types::Boolean;
states
start : initial state;
done : complete final state;
transitions
start -[]-> done {
for (i : Base_Types::Integer in 0 .. 2) {
i := 1;
forall (j : Base_Types::Integer in 0 .. 2) {
j := 1;
flag := outgoing'fresh;
amount := #Issue3244Properties::Size
}
}
};
**};
end worker.invalid;

thread implementation worker.valid
annex behavior_specification {**
states
start : initial state;
done : complete final state;
transitions
start -[]-> done;
**};
end worker.valid;
end Issue3244;
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
-- 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.

property set Issue3244Properties is
Size : aadlinteger units AADL_Project::Size_Units applies to (all);
end Issue3244Properties;
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
/**
* 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.xtext.aadl2.ba.tests;

import static org.junit.Assert.assertEquals;

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.junit.Test;
import org.junit.runner.RunWith;
import org.osate.aadl2.AadlPackage;
import org.osate.testsupport.TestHelper;
import org.osate.xtext.aadl2.ba.validation.BehaviorAnnexValidator;

import com.google.inject.Inject;

/** Characterizes independent diagnostics and annex isolation while consolidating validator traversals. */
@RunWith(XtextRunner.class)
@InjectWith(BehaviorAnnexEmbeddedInjectorProvider.class)
public class Issue3244Test {
private static final String MODEL_DIRECTORY = "org.osate.xtext.aadl2.ba.tests/models/issue3244/";

@Inject
private TestHelper<AadlPackage> testHelper;

@Test
public void reportsIndependentChecksInNestedActionsAfterAnInvalidArraySize() throws Exception {
var result = testHelper.testFile(MODEL_DIRECTORY + "Issue3244.aadl",
MODEL_DIRECTORY + "Issue3244Properties.aadl");
var source = NodeModelUtils.getNode(result.getResource().getContents().getFirst()).getRootNode().getText();
// The invalid dimension gates the strict analyzers, but all source checks and both property checks must run.
// A second, valid annex in the same file must not inherit the first annex's pending checks.
var expected = List.of(BehaviorAnnexValidator.ARRAY_SIZE + ": amount",
BehaviorAnnexValidator.ITERATIVE_VARIABLE_TARGET + ": i",
BehaviorAnnexValidator.ITERATIVE_VARIABLE_TARGET + ": j",
BehaviorAnnexValidator.PORT_STATUS_DIRECTION + ": outgoing'fresh",
BehaviorAnnexValidator.PROPERTY_REFERENCE_VALUE + ": #Issue3244Properties::Size",
BehaviorAnnexValidator.PROPERTY_REFERENCE_UNITS + ": #Issue3244Properties::Size");
assertEquals(expected.stream().sorted().toList(), result.getIssues().stream().map(issue -> {
assertEquals(result.getSummary(), Severity.ERROR, issue.getSeverity());
return issue.getCode() + ": " + source.substring(issue.getOffset(), issue.getOffset() + issue.getLength());
}).sorted().toList());
}
}
Loading