Summary
The BA checker does not enforce the AS5506/3 Rev. A D.6 rule that no complete state may be reached while a shared-data resource remains locked.
Lock and unlock actions resolve, but no path-sensitive lock-balance check was found in the active rules or type checker.
Reproduction
This issue comes from the source audit in ba/doc/conformance.md; no additional runtime reproduction was performed. Historical issue #2234 covers resolution/type checking of the operations, not resource lifetime across control-flow paths.
Expected behavior
Track required-data-access locks across sequences, sets, branches, loops, wildcard operations, and transitions. Report every path that can reach a complete state while a resource remains locked without rejecting balanced paths.
Relevant code
Summary
The BA checker does not enforce the AS5506/3 Rev. A D.6 rule that no complete state may be reached while a shared-data resource remains locked.
Lock and unlock actions resolve, but no path-sensitive lock-balance check was found in the active rules or type checker.
Reproduction
This issue comes from the source audit in
ba/doc/conformance.md; no additional runtime reproduction was performed. Historical issue #2234 covers resolution/type checking of the operations, not resource lifetime across control-flow paths.Expected behavior
Track required-data-access locks across sequences, sets, branches, loops, wildcard operations, and transitions. Report every path that can reach a complete state while a resource remains locked without rejecting balanced paths.
Relevant code
ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java.ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaLegalityRulesChecker.java.ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue2372Test.xtend— reference-resolution coverage.