Summary
The current validation path does not enforce the AS5506/3 Rev. A D.3 consistency rule that a behavior annex must not remain blocked in an execution state: the disjunction of its outgoing execute conditions must be true.
The consistency checker contains only the mode-related C4 check, and the driver has the older execute-condition semantic check commented out.
Reproduction
This issue comes from the source audit in ba/doc/conformance.md; no additional runtime reproduction was performed.
Expected behavior
Detect execution states with no possible outgoing transition when that is statically decidable. Define and document conservative behavior for conditions that cannot be proved exhaustive, rather than silently treating the rule as implemented.
Relevant code
ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java.ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java — commented D_3_18_Checker call.ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaSemanticRulesChecker.java.
Summary
The current validation path does not enforce the AS5506/3 Rev. A D.3 consistency rule that a behavior annex must not remain blocked in an execution state: the disjunction of its outgoing execute conditions must be true.
The consistency checker contains only the mode-related C4 check, and the driver has the older execute-condition semantic check commented out.
Reproduction
This issue comes from the source audit in
ba/doc/conformance.md; no additional runtime reproduction was performed.Expected behavior
Detect execution states with no possible outgoing transition when that is statically decidable. Define and document conservative behavior for conditions that cannot be proved exhaustive, rather than silently treating the rule as implemented.
Relevant code
ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java.ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java— commentedD_3_18_Checkercall.ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaSemanticRulesChecker.java.