Summary
The BA legality checker rejects every subprogram behavior with more than one final state. AS5506/3 Rev. A D.3 allows several final states when the annex specifies intended, potentially nondeterministic behavior; a single final state applies to deterministic implementation representations.
Reproduction
This issue comes from the source audit in ba/doc/conformance.md; no additional runtime reproduction was performed. D_3_L1_And_L2_Check reports an error whenever a subprogram has more than one final state, with no profile or intent distinction.
Expected behavior
Allow multiple final states in standard behavior specifications. If OSATE provides an explicitly selected deterministic implementation profile, enforce a single final state only in that profile.
Relevant code
ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java — D_3_L1_And_L2_Check.ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.xtend — current multiple-final-state expectation.
Summary
The BA legality checker rejects every subprogram behavior with more than one final state. AS5506/3 Rev. A D.3 allows several final states when the annex specifies intended, potentially nondeterministic behavior; a single final state applies to deterministic implementation representations.
Reproduction
This issue comes from the source audit in
ba/doc/conformance.md; no additional runtime reproduction was performed.D_3_L1_And_L2_Checkreports an error whenever a subprogram has more than one final state, with no profile or intent distinction.Expected behavior
Allow multiple final states in standard behavior specifications. If OSATE provides an explicitly selected deterministic implementation profile, enforce a single final state only in that profile.
Relevant code
ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java—D_3_L1_And_L2_Check.ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.xtend— current multiple-final-state expectation.