Require exactly one initial EMV2 behavior state 馃 - #3253
Merged
Merged
Conversation
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #2804
EMV2 error behavior state machines now require exactly one initial state, as specified by E.8 legality rule L32. The state-machine validator previously checked identifier uniqueness without checking the number of initial states.
Issue2804Testchecks the diagnostics for a machine without an initial state, one with two initial states, and one with no states. A separate model verifies that one initial state is valid whether it is the only state or appears after a noninitial state. The regression failed before the fix because the expected diagnostic was absent; both tests pass afterward.The EMV2 suite exposed four existing fixtures that omitted an initial state. Add the missing initial declarations so the transition, property-reference, and scope tests retain their original assertions.
Validation:
clean verifywith-Dtest=Issue2804Test: 2 tests passed.clean install: 1,682 tests, 0 failures/errors/skips; all reactor projects passed. This includes all 300 EMV2 tests and the four repaired fixtures.git diff --checkpassed.Build flags:
mvn -o -T5 -s releng/osate.releng/settings.xml -Plocal -Dpr.build=true -Dsign=false -Dspotbugs=false -Dcodecoverage=false -Djavadoc=false -DfailIfNoTests=false. The focused run uses-pl :org.osate.xtext.aadl2.errormodel,:org.osate.aadl2.errormodel.tests,:org.osate.xtext.aadl2.errormodel.feature -Dtycho.localArtifacts=default; the root run uses-Dtycho.localArtifacts=ignore clean install.No dependency on another PR. Existing models with zero or multiple initial states will now receive the required validation error; parsing and instantiation are unchanged.