From 8d57adefa660a325c01c2dd14043588a0b18e774 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Sat, 12 Sep 2026 14:35:42 -0400 Subject: [PATCH 1/2] Add regression test for issue #3178 Model mode-refining Behavior Annex subclauses through ordinary embedded AADL input. Assert same-name source and destination bindings, matching and mismatching triggers, multi-source transitions, the all-or-none rule, and the in-modes boundary without mutating the strict model. --- ...sate.ba.tests_models_issue3178_InModes.txt | 0 ...te.ba.tests_models_issue3178_Issue3178.txt | 0 ...s_models_issue3178_MixedCompleteStates.txt | 1 + ...tests_models_issue3178_MultipleSources.txt | 1 + ...ba.tests_models_issue3178_WrongTrigger.txt | 1 + ...sate.ba.tests_models_issue3178_InModes.txt | 0 ...te.ba.tests_models_issue3178_Issue3178.txt | 0 ...s_models_issue3178_MixedCompleteStates.txt | 0 ...tests_models_issue3178_MultipleSources.txt | 0 ...ba.tests_models_issue3178_WrongTrigger.txt | 0 ...sate.ba.tests_models_issue3178_InModes.txt | 4 + ...te.ba.tests_models_issue3178_Issue3178.txt | 14 ++ ...s_models_issue3178_MixedCompleteStates.txt | 6 + ...tests_models_issue3178_MultipleSources.txt | 15 ++ ...ba.tests_models_issue3178_WrongTrigger.txt | 14 ++ ...sate.ba.tests_models_issue3178_InModes.txt | 3 + ...te.ba.tests_models_issue3178_Issue3178.txt | 9 ++ ...s_models_issue3178_MixedCompleteStates.txt | 4 + ...tests_models_issue3178_MultipleSources.txt | 15 ++ ...ba.tests_models_issue3178_WrongTrigger.txt | 9 ++ ...sate.ba.tests_models_issue3178_InModes.txt | 6 + ...te.ba.tests_models_issue3178_Issue3178.txt | 9 ++ ...s_models_issue3178_MixedCompleteStates.txt | 7 + ...tests_models_issue3178_MultipleSources.txt | 9 ++ ...ba.tests_models_issue3178_WrongTrigger.txt | 9 ++ .../models/issue3178/.gitignore | 2 + .../models/issue3178/.project | 8 + .../models/issue3178/InModes.aadl | 37 +++++ .../models/issue3178/Issue3178.aadl | 44 ++++++ .../models/issue3178/MixedCompleteStates.aadl | 39 +++++ .../models/issue3178/MultipleSources.aadl | 47 ++++++ .../models/issue3178/WrongTrigger.aadl | 45 ++++++ .../src/org/osate/ba/tests/Issue3178Test.java | 147 ++++++++++++++++++ 33 files changed, 505 insertions(+) create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_InModes.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_Issue3178.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_WrongTrigger.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_InModes.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_Issue3178.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_WrongTrigger.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_InModes.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_Issue3178.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_WrongTrigger.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_InModes.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_Issue3178.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_WrongTrigger.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_InModes.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_Issue3178.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MultipleSources.txt create mode 100644 ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_WrongTrigger.txt create mode 100644 ba/org.osate.ba.tests/models/issue3178/.gitignore create mode 100644 ba/org.osate.ba.tests/models/issue3178/.project create mode 100644 ba/org.osate.ba.tests/models/issue3178/InModes.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3178/Issue3178.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3178/MixedCompleteStates.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3178/MultipleSources.aadl create mode 100644 ba/org.osate.ba.tests/models/issue3178/WrongTrigger.aadl create mode 100644 ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3178Test.java diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_InModes.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_InModes.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_Issue3178.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_Issue3178.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt new file mode 100644 index 00000000000..a03a598357f --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt @@ -0,0 +1 @@ +error | semantic | 36 | 2 | 7 | Complete state 'waiting' must be a mode identifier because complete state 'idle' is a mode identifier: Behavior Annex D.3 legality rule failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MultipleSources.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MultipleSources.txt new file mode 100644 index 00000000000..a5d65d5b464 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_MultipleSources.txt @@ -0,0 +1 @@ +error | semantic | 44 | 30 | 5 | The behavior transition tries to refine a transition mode but it is not consisting with any transition mode of MultipleSources::worker.impl component: Behavior Annex D.3.(C4) consistency rule failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_WrongTrigger.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_WrongTrigger.txt new file mode 100644 index 00000000000..09554352dd5 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3178_WrongTrigger.txt @@ -0,0 +1 @@ +error | semantic | 42 | 21 | 5 | The behavior transition tries to refine a transition mode but it is not consisting with any transition mode of WrongTrigger::worker.impl component: Behavior Annex D.3.(C4) consistency rule failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_InModes.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_InModes.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_Issue3178.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_Issue3178.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MultipleSources.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_MultipleSources.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_WrongTrigger.txt b/ba/org.osate.ba.tests/expected/diagnostics/org.osate.ba.tests_models_issue3178_WrongTrigger.txt new file mode 100644 index 00000000000..e69de29bb2d diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_InModes.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_InModes.txt new file mode 100644 index 00000000000..b61c1847614 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_InModes.txt @@ -0,0 +1,4 @@ +annex[0] owner=InModes::worker.impl + (BehaviorAnnex, behavior_specification, 1889, 40) + (BehaviorState, active, 1897, 6) + (BehaviorStateGroup, , 1897, 32) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_Issue3178.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_Issue3178.txt new file mode 100644 index 00000000000..b281e9b5457 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_Issue3178.txt @@ -0,0 +1,14 @@ +annex[0] owner=Issue3178::worker.impl + (BehaviorAnnex, behavior_specification, 1957, 110) + (BehaviorCondition, , 2042, 14) + (BehaviorState, active, 1997, 6) + (BehaviorState, idle, 1965, 4) + (BehaviorStateGroup, , 1965, 30) + (BehaviorStateGroup, , 1997, 24) + (BehaviorTransition, , 2035, 32) + (DispatchCondition, , 2045, 11) + (DispatchConjunction, , 2054, 2) + (DispatchTriggerCondition, , 2054, 2) + (DispatchTriggerLogicalExpression, , 2054, 2) + (Reference, , 2054, 2) + (ReferenceSegment, go, 2054, 2) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt new file mode 100644 index 00000000000..5ddb5e65c71 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt @@ -0,0 +1,6 @@ +annex[0] owner=MixedCompleteStates::worker.impl + (BehaviorAnnex, behavior_specification, 1915, 65) + (BehaviorState, idle, 1923, 4) + (BehaviorState, waiting, 1955, 7) + (BehaviorStateGroup, , 1923, 30) + (BehaviorStateGroup, , 1955, 25) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MultipleSources.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MultipleSources.txt new file mode 100644 index 00000000000..4e7a7520342 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_MultipleSources.txt @@ -0,0 +1,15 @@ +annex[0] owner=MultipleSources::worker.impl + (BehaviorAnnex, behavior_specification, 2023, 127) + (BehaviorCondition, , 2124, 17) + (BehaviorState, done, 2072, 4) + (BehaviorState, first, 2031, 5) + (BehaviorState, second, 2064, 6) + (BehaviorStateGroup, , 2031, 31) + (BehaviorStateGroup, , 2064, 30) + (BehaviorTransition, , 2108, 42) + (DispatchCondition, , 2127, 14) + (DispatchConjunction, , 2136, 5) + (DispatchTriggerCondition, , 2136, 5) + (DispatchTriggerLogicalExpression, , 2136, 5) + (Reference, , 2136, 5) + (ReferenceSegment, wrong, 2136, 5) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_WrongTrigger.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_WrongTrigger.txt new file mode 100644 index 00000000000..3a94f58ca43 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3178_WrongTrigger.txt @@ -0,0 +1,14 @@ +annex[0] owner=WrongTrigger::worker.impl + (BehaviorAnnex, behavior_specification, 1984, 113) + (BehaviorCondition, , 2069, 17) + (BehaviorState, active, 2024, 6) + (BehaviorState, idle, 1992, 4) + (BehaviorStateGroup, , 1992, 30) + (BehaviorStateGroup, , 2024, 24) + (BehaviorTransition, , 2062, 35) + (DispatchCondition, , 2072, 14) + (DispatchConjunction, , 2081, 5) + (DispatchTriggerCondition, , 2081, 5) + (DispatchTriggerLogicalExpression, , 2081, 5) + (Reference, , 2081, 5) + (ReferenceSegment, wrong, 2081, 5) diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_InModes.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_InModes.txt new file mode 100644 index 00000000000..d445d0ff947 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_InModes.txt @@ -0,0 +1,3 @@ +annex[0] owner=InModes::worker.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=active diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_Issue3178.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_Issue3178.txt new file mode 100644 index 00000000000..2b6631a7c20 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_Issue3178.txt @@ -0,0 +1,9 @@ +annex[0] owner=Issue3178::worker.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=idle + states[1] : BehaviorState name=active + transitions[0] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : DispatchTriggerLogicalExpression + dispatchConjunctions[0] : DispatchConjunction + dispatchTriggers[0] : EventPortHolder element=Issue3178::worker.go [EventPort] diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt new file mode 100644 index 00000000000..3abf7761ce2 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt @@ -0,0 +1,4 @@ +annex[0] owner=MixedCompleteStates::worker.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=idle + states[1] : BehaviorState name=waiting diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MultipleSources.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MultipleSources.txt new file mode 100644 index 00000000000..db6df58b514 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_MultipleSources.txt @@ -0,0 +1,15 @@ +annex[0] owner=MultipleSources::worker.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=first + states[1] : BehaviorState name=second + states[2] : BehaviorState name=done + transitions[0] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : DispatchTriggerLogicalExpression + dispatchConjunctions[0] : DispatchConjunction + dispatchTriggers[0] : EventPortHolder element=MultipleSources::worker.wrong [EventPort] + transitions[1] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : DispatchTriggerLogicalExpression + dispatchConjunctions[0] : DispatchConjunction + dispatchTriggers[0] : EventPortHolder element=MultipleSources::worker.wrong [EventPort] diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_WrongTrigger.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_WrongTrigger.txt new file mode 100644 index 00000000000..d3a3dd2d608 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_issue3178_WrongTrigger.txt @@ -0,0 +1,9 @@ +annex[0] owner=WrongTrigger::worker.impl + parsedAnnexSubclause : BehaviorAnnex name=behavior_specification + states[0] : BehaviorState name=idle + states[1] : BehaviorState name=active + transitions[0] : BehaviorTransition + condition : DispatchCondition + dispatchTriggerCondition : DispatchTriggerLogicalExpression + dispatchConjunctions[0] : DispatchConjunction + dispatchTriggers[0] : EventPortHolder element=WrongTrigger::worker.wrong [EventPort] diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_InModes.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_InModes.txt new file mode 100644 index 00000000000..2f14245efd5 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_InModes.txt @@ -0,0 +1,6 @@ +===== annex[0] owner=InModes::worker.impl ===== + +states +\tactive : initial complete state; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_Issue3178.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_Issue3178.txt new file mode 100644 index 00000000000..58f218996ae --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_Issue3178.txt @@ -0,0 +1,9 @@ +===== annex[0] owner=Issue3178::worker.impl ===== + +states +\tidle : initial complete state; +\tactive : complete state; +transitions +\tidle -[on dispatch go]-> active; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt new file mode 100644 index 00000000000..4f73012f67e --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MixedCompleteStates.txt @@ -0,0 +1,7 @@ +===== annex[0] owner=MixedCompleteStates::worker.impl ===== + +states +\tidle : initial complete state; +\twaiting : complete state; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MultipleSources.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MultipleSources.txt new file mode 100644 index 00000000000..77439805674 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_MultipleSources.txt @@ -0,0 +1,9 @@ +===== annex[0] owner=MultipleSources::worker.impl ===== + +states +\tfirst : initial complete state; +\tsecond, done : complete state; +transitions +\tfirst, second -[on dispatch wrong]-> done; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_WrongTrigger.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_WrongTrigger.txt new file mode 100644 index 00000000000..875f51cf243 --- /dev/null +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_issue3178_WrongTrigger.txt @@ -0,0 +1,9 @@ +===== annex[0] owner=WrongTrigger::worker.impl ===== + +states +\tidle : initial complete state; +\tactive : complete state; +transitions +\tidle -[on dispatch wrong]-> active; +----- Xtext reparse ----- +reparsed diff --git a/ba/org.osate.ba.tests/models/issue3178/.gitignore b/ba/org.osate.ba.tests/models/issue3178/.gitignore new file mode 100644 index 00000000000..afce51184c6 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/.gitignore @@ -0,0 +1,2 @@ +/.aadlbin-gen/ +/instances/ diff --git a/ba/org.osate.ba.tests/models/issue3178/.project b/ba/org.osate.ba.tests/models/issue3178/.project new file mode 100644 index 00000000000..e8856f1d7df --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/.project @@ -0,0 +1,8 @@ + + + issue3178 + + + org.eclipse.xtext.ui.shared.xtextBuilder + org.osate.core.aadlnatureorg.eclipse.xtext.ui.shared.xtextNature + diff --git a/ba/org.osate.ba.tests/models/issue3178/InModes.aadl b/ba/org.osate.ba.tests/models/issue3178/InModes.aadl new file mode 100644 index 00000000000..fb311f1f488 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/InModes.aadl @@ -0,0 +1,37 @@ +-- 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 InModes +public + +thread worker +end worker; + +thread implementation worker.impl +modes + active : initial mode; +annex behavior_specification {** +states + active : initial complete state; +**} in modes (active); +end worker.impl; +end InModes; diff --git a/ba/org.osate.ba.tests/models/issue3178/Issue3178.aadl b/ba/org.osate.ba.tests/models/issue3178/Issue3178.aadl new file mode 100644 index 00000000000..995298b88d3 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/Issue3178.aadl @@ -0,0 +1,44 @@ +-- 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 Issue3178 +public + +thread worker +features + go : in event port; +end worker; + +thread implementation worker.impl +modes + idle : initial mode; + active : mode; + idle -[go]-> active; +annex behavior_specification {** +states + idle : initial complete state; + active : complete state; +transitions + idle -[on dispatch go]-> active; +**}; +end worker.impl; +end Issue3178; diff --git a/ba/org.osate.ba.tests/models/issue3178/MixedCompleteStates.aadl b/ba/org.osate.ba.tests/models/issue3178/MixedCompleteStates.aadl new file mode 100644 index 00000000000..c8ad5bc32f5 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/MixedCompleteStates.aadl @@ -0,0 +1,39 @@ +-- 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 MixedCompleteStates +public + +thread worker +end worker; + +thread implementation worker.impl +modes + idle : initial mode; + active : mode; +annex behavior_specification {** +states + idle : initial complete state; + waiting : complete state; +**}; +end worker.impl; +end MixedCompleteStates; diff --git a/ba/org.osate.ba.tests/models/issue3178/MultipleSources.aadl b/ba/org.osate.ba.tests/models/issue3178/MultipleSources.aadl new file mode 100644 index 00000000000..46a0d06df70 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/MultipleSources.aadl @@ -0,0 +1,47 @@ +-- 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 MultipleSources +public + +thread worker +features + go : in event port; + wrong : in event port; +end worker; + +thread implementation worker.impl +modes + first : initial mode; + second : mode; + done : mode; + first -[go]-> done; + second -[go]-> done; +annex behavior_specification {** +states + first : initial complete state; + second, done : complete state; +transitions + first, second -[on dispatch wrong]-> done; +**}; +end worker.impl; +end MultipleSources; diff --git a/ba/org.osate.ba.tests/models/issue3178/WrongTrigger.aadl b/ba/org.osate.ba.tests/models/issue3178/WrongTrigger.aadl new file mode 100644 index 00000000000..97a6a5fb7d7 --- /dev/null +++ b/ba/org.osate.ba.tests/models/issue3178/WrongTrigger.aadl @@ -0,0 +1,45 @@ +-- 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 WrongTrigger +public + +thread worker +features + go : in event port; + wrong : in event port; +end worker; + +thread implementation worker.impl +modes + idle : initial mode; + active : mode; + idle -[go]-> active; +annex behavior_specification {** +states + idle : initial complete state; + active : complete state; +transitions + idle -[on dispatch wrong]-> active; +**}; +end worker.impl; +end WrongTrigger; diff --git a/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3178Test.java b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3178Test.java new file mode 100644 index 00000000000..dc93711d7fc --- /dev/null +++ b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3178Test.java @@ -0,0 +1,147 @@ +/** + * 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.ba.tests; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNull; +import static org.junit.Assert.assertSame; +import static org.junit.Assert.assertTrue; + +import java.util.Comparator; +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.eclipse.xtext.testing.validation.ValidationTestHelper; +import org.eclipse.xtext.validation.Issue; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.osate.aadl2.AadlPackage; +import org.osate.aadl2.ComponentClassifier; +import org.osate.aadl2.Mode; +import org.osate.annexsupport.AnnexUtil; +import org.osate.ba.aadlba.BehaviorState; +import org.osate.testsupport.TestHelper; +import org.osate.xtext.aadl2.ba.util.BehaviorAnnexUtil; + +import com.google.inject.Inject; +import com.itemis.xtext.testing.XtextTest; + +/** Exercises AS5506/3 Rev. A D.3 mode-state refinement through ordinary embedded AADL validation. */ +@RunWith(XtextRunner.class) +@InjectWith(BehaviorAnnexInjectorProvider.class) +public class Issue3178Test extends XtextTest { + private static final String PATH = "org.osate.ba.tests/models/issue3178/"; + private static final String CHECKER = "org.osate.xtext.aadl2.ba.checker"; + private static final String MODE_REFINEMENT = "org.osate.xtext.aadl2.ba.modeRefinement"; + + @Inject + private TestHelper testHelper; + + @Inject + private ValidationTestHelper validationHelper; + + @Test + public void sameNamedCompleteStatesBindToSourceAndDestinationModes() throws Exception { + var root = testHelper.parseFile(PATH + "Issue3178.aadl"); + validationHelper.assertNoIssues(root); + var annex = AnnexUtil.getAllDefaultAnnexSubclauses(root).getFirst(); + var owner = (ComponentClassifier) annex.getContainingClassifier(); + var strict = BehaviorAnnexUtil.getStrictModel(annex); + assertSame(mode(owner, "idle"), state(strict, "idle").getBindedMode()); + assertSame(mode(owner, "active"), state(strict, "active").getBindedMode()); + assertSame(mode(owner, "idle"), strict.getTransitions().getFirst().getSourceState().getBindedMode()); + assertSame(mode(owner, "active"), strict.getTransitions().getFirst().getDestinationState().getBindedMode()); + } + + @Test + public void mismatchedTriggerIsCheckedThroughEmbeddedValidation() throws Exception { + assertDiagnostics("WrongTrigger", List.of(new Expected("wrong", CHECKER, + "The behavior transition tries to refine a transition mode but it is not consisting with any " + + "transition mode of WrongTrigger::worker.impl component: Behavior Annex D.3.(C4) " + + "consistency rule failed."))); + } + + @Test + public void everyModeSourceOfExpandedTransitionIsChecked() throws Exception { + var root = testHelper.parseFile(PATH + "MultipleSources.aadl"); + var annex = AnnexUtil.getAllDefaultAnnexSubclauses(root).getFirst(); + var strict = BehaviorAnnexUtil.getStrictModel(annex); + assertEquals(List.of("first", "second"), strict.getTransitions().stream() + .map(transition -> transition.getSourceState().getBindedMode().getName()).toList()); + assertDiagnostics(root, List.of(new Expected("wrong", CHECKER, + "The behavior transition tries to refine a transition mode but it is not consisting with any " + + "transition mode of MultipleSources::worker.impl component: Behavior Annex D.3.(C4) " + + "consistency rule failed."))); + } + + @Test + public void everyCompleteStateMustRepresentAModeOnceOneDoes() throws Exception { + assertDiagnostics("MixedCompleteStates", List.of(new Expected("waiting", MODE_REFINEMENT, + "Complete state 'waiting' must be a mode identifier because complete state 'idle' is a mode " + + "identifier: Behavior Annex D.3 legality rule failed."))); + } + + @Test + public void inModesSubclauseDoesNotBindCompleteStates() throws Exception { + var root = testHelper.parseFile(PATH + "InModes.aadl"); + var annex = AnnexUtil.getAllDefaultAnnexSubclauses(root).getFirst(); + assertEquals(1, annex.getInModes().size()); + assertNull(BehaviorAnnexUtil.getStrictModel(annex).getStates().getFirst().getBindedMode()); + } + + private void assertDiagnostics(String model, List expected) throws Exception { + assertDiagnostics(testHelper.parseFile(PATH + model + ".aadl"), expected); + } + + private void assertDiagnostics(AadlPackage root, List expected) { + var source = NodeModelUtils.getNode(root).getRootNode().getText(); + var issues = validationHelper.validate(root).stream().sorted(Comparator.comparing(Issue::getOffset)).toList(); + assertEquals(issues.toString(), expected.size(), issues.size()); + assertEquals(expected, issues.stream().map(issue -> { + assertEquals(Severity.ERROR, issue.getSeverity()); + var target = source.substring(issue.getOffset(), issue.getOffset() + issue.getLength()); + return new Expected(target, issue.getCode(), issue.getMessage()); + }).toList()); + } + + private static Mode mode(ComponentClassifier owner, String name) { + return owner.getAllModes().stream() + .filter(mode -> name.equalsIgnoreCase(mode.getName())) + .findFirst() + .orElseThrow(); + } + + private static BehaviorState state(org.osate.ba.aadlba.BehaviorAnnex annex, String name) { + return annex.getStates().stream() + .filter(state -> name.equalsIgnoreCase(state.getName())) + .findFirst() + .orElseThrow(); + } + + private record Expected(String target, String code, String message) { + } +} From 5e23e684a8a1b3707dd95e84ee9902351e0e94f3 Mon Sep 17 00:00:00 2001 From: Lutz Wrage Date: Sat, 12 Sep 2026 14:36:08 -0400 Subject: [PATCH 2/2] Bind complete states to corresponding modes Bind complete Behavior Annex states to visible same-named AADL modes only when the subclause has no in-modes applicability. Enforce the AS5506/3 all-or-none legality rule before strict checking, refresh affected characterization fixtures, and mark G14 implemented in the conformance report. --- ba/doc/conformance.md | 24 +-- ...ests_models_covering_semantic_cr_D3_C4.txt | 2 +- ...s_models_covering_syntax_aadlBaTest001.txt | 1 - ...te.ba.tests_models_issue2147_issue2147.txt | 1 - ...ests_models_covering_semantic_cr_D3_C4.txt | 40 +++-- ...te.ba.tests_models_issue3182_Issue3182.txt | 146 +++++++++--------- ...ests_models_covering_semantic_cr_D3_C4.txt | 14 +- ...ests_models_covering_semantic_cr_D3_C4.txt | 2 +- .../models/covering_semantic/cr_D3_C4.aadl | 6 +- .../models/issue3182/Issue3182.aadl | 2 + .../src/org/osate/ba/tests/Issue3154Test.java | 4 +- .../DeclarativeToStrictTranslator.java | 36 ++++- .../ba/validation/BehaviorAnnexValidator.java | 35 ++++- 13 files changed, 187 insertions(+), 126 deletions(-) diff --git a/ba/doc/conformance.md b/ba/doc/conformance.md index fb01e1390bd..bb40d454678 100644 --- a/ba/doc/conformance.md +++ b/ba/doc/conformance.md @@ -1,10 +1,10 @@ # Behavior Annex conformance and gap report -Review date: 2026-09-09. Repository: `osate/osate2`, local `master`, commit `01911d359378a4481ae2109ec2c61ac3a42537b7`. Tracking status updated 2026-09-10 against `master` at commit `32233c796b`. +Review date: 2026-09-09. Repository: `osate/osate2`, local `master`, commit `01911d359378a4481ae2109ec2c61ac3a42537b7`. Tracking status updated 2026-09-12 against `master` at commit `638ec7cbc0`. -The current implementation provides substantial Behavior Annex syntax, model construction, and selected semantic checks, but **does not fully conform to the supplied AS5506/3 Rev. A document**. Gaps include required syntax, preservation of expression and literal meaning, internal features, mode binding, and enforcement of several legality and consistency rules. Existing tests document some of these limitations, but their passing expectations do not establish conformance. +The current implementation provides substantial Behavior Annex syntax, model construction, and selected semantic checks, but **does not fully conform to the supplied AS5506/3 Rev. A document**. Remaining gaps include syntax acceptance, preservation of some strict-model meaning, and enforcement of several legality, consistency, and execution rules. Existing tests document some of these limitations, but their passing expectations do not establish conformance. -The most urgent findings are loss of information during translation to the strict BA model, type conformance being disabled outright (G18), absent mode bindings, and weaknesses in the conformance tests themselves. Fixing only the missing grammar productions would leave significant semantic gaps. +The most urgent remaining findings are type conformance being disabled outright (G18), other losses of information during translation to the strict BA model, and weaknesses in the conformance tests themselves. Fixing only the missing grammar productions would leave significant semantic gaps. ## GitHub tracking @@ -25,7 +25,7 @@ The user directed that the report findings be treated as valid and filed without | G11 ✅ | [#3175](https://github.com/osate/osate2/issues/3175) | V08 | [#3189](https://github.com/osate/osate2/issues/3189) | | G12 ✅ | [#3176](https://github.com/osate/osate2/issues/3176) | V09 | [#3190](https://github.com/osate/osate2/issues/3190) | | G13 ✅ | [#3177](https://github.com/osate/osate2/issues/3177) | V10 | [#3191](https://github.com/osate/osate2/issues/3191) | -| G14 | [#3178](https://github.com/osate/osate2/issues/3178) | V11 | [#3192](https://github.com/osate/osate2/issues/3192) | +| G14 ✅ | [#3178](https://github.com/osate/osate2/issues/3178) | V11 | [#3192](https://github.com/osate/osate2/issues/3192) | | G18 | [#3199](https://github.com/osate/osate2/issues/3199) | | | Closed since the review: G01 ([#3165](https://github.com/osate/osate2/issues/3165), internal conditions), G02 ([#3166](https://github.com/osate/osate2/issues/3166), external-condition expressions), G03 ([#3167](https://github.com/osate/osate2/issues/3167), frozen-port parentheses), G04 ([#3168](https://github.com/osate/osate2/issues/3168), timeout reset ports), G05 ([#3169](https://github.com/osate/osate2/issues/3169), short-circuit logical operators), G07 ([#3171](https://github.com/osate/osate2/issues/3171), the port `updated` value), G08 ([#3172](https://github.com/osate/osate2/issues/3172), `self` property references), G10 ([#3174](https://github.com/osate/osate2/issues/3174), internal port actions), G11 ([#3175](https://github.com/osate/osate2/issues/3175), numeric literals), G12 ([#3176](https://github.com/osate/osate2/issues/3176), array extents) together with its follow-ups [#3208](https://github.com/osate/osate2/issues/3208) and [#3210](https://github.com/osate/osate2/issues/3210), G13 ([#3177](https://github.com/osate/osate2/issues/3177), expression precedence and grouping), G16 ([#3180](https://github.com/osate/osate2/issues/3180), loop-variable assignment targets), V01 ([#3182](https://github.com/osate/osate2/issues/3182), declaration naming rules), V02 ([#3183](https://github.com/osate/osate2/issues/3183), otherwise-transition rules), and V03 ([#3184](https://github.com/osate/osate2/issues/3184), action timeout legality rules). @@ -57,7 +57,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato | Section | Implemented capability and evidence | Assessment | | --- | --- | --- | | D.1–D.2: scope and concepts | Embedded `behavior_specification` parser, linker, serializer, and strict-model translation are registered. | Supports the language-tooling role; execution semantics require separate consumer evidence. | -| D.3: behavior specification | Variables, grouped states, state kinds, named/prioritized and multiple-source transitions, execute conditions, and dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions (G01) and complete external-condition expressions (G02) were absent, both since fixed, and the naming and otherwise-transition rules were unenforced (V01 and V02, since fixed); mode binding is explicitly missing; multiple subprogram final states are rejected unconditionally; several consistency obligations lack demonstrated enforcement. | +| D.3: behavior specification | Variables, grouped states, state kinds, named/prioritized and multiple-source transitions, execute conditions, and dispatch/external conditions. State and transition legality checks have dedicated tests. | Partial. Internal conditions (G01), complete external-condition expressions (G02), naming and otherwise-transition rules (V01 and V02), and complete-state mode binding (G14) were absent and are now implemented; multiple subprogram final states are rejected unconditionally, and several consistency obligations lack demonstrated enforcement. | | D.4: thread dispatch | Dispatch conjunction/disjunction, `stop`, bare timeout, timeout with a duration, and an unparenthesized frozen-port list. Selected timeout/stop checks exist. | Partial. Required frozen-list parentheses were missing (G03) and timeout reset ports absent (G04), both since fixed. Full protocol/trigger compatibility and core-property consistency are not demonstrated. | | D.5: component interactions | Port send/dequeue/freeze, count/fresh/updated, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` was absent (G07) and internal events were represented incorrectly (G10), both since fixed; call-signature and direction/category checks need additional coverage. Input/output timing consistency is not established. | | D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, explicit-type loops, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers are missing; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. | @@ -132,12 +132,14 @@ The AST precedence error and the strict-model flattening error must be assessed **Standard:** D.3 allows complete states to represent same-named modes and requires consistency with the corresponding mode transitions. It also constrains mixtures of complete states that do and do not represent modes. -**Evidence:** `translateStates`, translator line 335, copies names and initial/complete/final flags but never sets `bindedMode`. [Issue3154Test.eachBoundSourceChecksModeConsistency](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java) explicitly documents this at line 135 and supplies bindings through the strict API before invoking the checker. [AadlBaConsistencyRulesChecker.D_3_C4_Check](../../ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java) returns immediately when a source state has no bound mode. +**Review evidence:** At the review date, `translateStates` copied names and initial/complete/final flags but never set `bindedMode`. [Issue3154Test.eachBoundSourceChecksModeConsistency](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java) supplied bindings through the strict API before invoking the checker. [AadlBaConsistencyRulesChecker.D_3_C4_Check](../../ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java) returns immediately when a source state has no bound mode. -**Impact:** The C4 unit-level regression exercises a checker that ordinary translated source does not activate through that binding path. This is an explicitly documented implementation gap, not merely missing test coverage. +**Review impact:** Before #3178, the C4 unit-level regression exercised a checker that ordinary translated source did not activate through that binding path. This was an implementation gap, not merely missing test coverage. **Required coverage:** Parse and validate an external model with matching state/mode names without manually editing the strict model; verify positive and negative trigger cases, destination modes, multiple source states, and the all-or-none mode-state rule. The checker itself currently compares flattened trigger-name lists against transitions from the source mode; destination and Boolean structure also warrant focused tests. +**Implemented for [#3178](https://github.com/osate/osate2/issues/3178):** for a subclause without an `in modes` statement, translation now binds each complete state to a visible same-named mode case-insensitively. A subclause with an `in modes` statement does not create those bindings. The validator enforces D.3's all-or-none rule before strict checking, so a non-mode complete state is reported when another complete state represents a mode. `Issue3178Test` exercises source and destination bindings, matching and mismatching transition triggers, every source of a multi-source transition, the all-or-none diagnostic, and the `in modes` boundary through embedded AADL models without mutating the strict model. + ### G15 — Multiple final states in subprogram behavior are always rejected **Standard:** D.3's description explicitly allows several final states when specifying intended behavior; a deterministic implementation representation is distinguished as requiring one final state. @@ -190,7 +192,7 @@ These are bounded findings from the inspected grammar/translator/checker path. E | V02 | D.3 otherwise rules: no assigned priority and at most one otherwise transition per source state. | Implemented for [#3183](https://github.com/osate/osate2/issues/3183): report every conflicting otherwise transition as an error identifying its source state, including overlapping multi-source declarations. Explicit priorities produce a warning once per declaration, reflecting the standard's “should not” wording. `Issue3183Test` covers duplicates, source overlap, explicit zero and positive priorities, and valid otherwise transitions. | | V03 | D.3 and D.6 action timeouts: a matching simple timeout transition from the same source; restrictions on combining an action timeout with timeout conditions. | Implemented for [#3184](https://github.com/osate/osate2/issues/3184): every top-level or nested action timeout is checked against each source of its transition for a same-source simple timeout catch. Action timeouts on execution-timeout, dispatch-relative-timeout, and completion-relative-timeout transitions are rejected. Diagnostics mark the behavior time and name a missing source state; `Issue3184Test` covers positive, missing, wrong-source, nested, expanded multi-source, and all three prohibited timeout-condition forms. | | V04 | D.3 nonblocking execution-state behavior. | The only consistency-checker method is the mode-related C4 check; no guard-exhaustiveness analysis is present there. The driver also comments out the call to the older `D_3_18_Checker`; that method's existence does not establish coverage. Distinguish general symbolic proof from simple detectable dead ends and clearly document any analysis limit. | -| V05 | D.3 component-category/mode restrictions on external/internal conditions; behavior inheritance and replacement. | Conditions can be parsed generically, while type checking dispatches only execute conditions and the rules driver primarily dispatch conditions. Mode bindings are absent (G14), and the builder does not copy an in-modes context into the strict annex. Core AADL may retain mode applicability on the enclosing annex. Verify the complete consumer path before declaring inheritance or mode-specific selection unsupported. Cover thread/subprogram external-condition rejection and device condition mixing. | +| V05 | D.3 component-category/mode restrictions on external/internal conditions; behavior inheritance and replacement. | Conditions can be parsed generically, while type checking dispatches only execute conditions and the rules driver primarily dispatch conditions. Same-named complete states are now bound for no-`in modes` refinements (G14), but the builder does not copy an in-modes context into the strict annex. Core AADL may retain mode applicability on the enclosing annex. Verify the complete consumer path before declaring inheritance or mode-specific selection unsupported. Cover thread/subprogram external-condition rejection and device condition mixing. | | V06 | D.4 protocol/trigger compatibility, legal trigger/frozen-port categories, and consistency with core dispatch/freeze properties. | The checker has dedicated timeout branches and a stop check, but no complete implementation of the document's protocol/trigger table was found. Dispatch references use generic `Reference` syntax. A rule implementing one timeout form is not evidence for all rows of the table. Test the matrix and invalid trigger direction/category through embedded source. | | V07 | D.5 C1/C2: BA freeze/send operations agree with `Input_Time`/`Output_Time`, or are absent where required. | No BA check referring to these properties was found in the active BA checker/translator/validator code. Core property validation alone does not establish agreement with BA actions. Use models that are individually legal on each side but inconsistent together. | | V08 | D.6: a complete state cannot be reached while shared data remains locked. | Lock/unlock syntax and holders exist; `Issue2372Test` checks resolved lock references. No path-sensitive lock-balance check was found. Cover a balanced path, an unreleased resource, alternative branches, loops, and wildcard lock/unlock. Parsing a lock operation does not establish this rule. | @@ -210,11 +212,11 @@ Some checker comments identify their source as **AADL Behavior Annex draft 0.94* 4. **Model goldens omit the attributes most relevant to G11–G13.** `BehaviorAnnexCharacterizationTest.appendModel`, line 260, records EClass, names, holder targets, and containment structure, but not general scalar attributes such as literal values, array sizes, or operator enum values. The translator test uses this representation and adds selected checks for property associations and freeze actions. It does not establish numeric or operator-value preservation. -5. **The mode-consistency test deliberately supplies missing production state.** `Issue3154Test.eachBoundSourceChecksModeConsistency` is valuable per-source checker coverage, but its manual mode bindings are an explicit qualification on the end-to-end coverage claim. +5. ~~**The mode-consistency test deliberately supplies missing production state.**~~ `Issue3154Test.eachBoundSourceChecksModeConsistency` remains checker-level coverage using explicit bindings for differently named states. **Addressed end to end by #3178:** `Issue3178Test` obtains same-name bindings from ordinary embedded AADL translation and validates the resulting C4 diagnostics without mutating the strict model. 6. **Some legacy fixtures retain errors while tests now expect no diagnostics.** The loop-variable assignment example in G16 was a concrete instance until #3180 made that covering test require its diagnostic; the corresponding dequeue fixture shape is still accepted and is tracked as #3205. Other issue tests frequently assert only issue counts and successful parse. Counts should not substitute for the intended rule, severity, location, and positive control. -7. **Validator registration and gating matter.** At the review date the conformance and characterization classes used the generic AADL injector, unlike `CoveringSemanticTest` and the recent diagnostic regressions, so their goldens showed core-AADL findings only. **Step 1 made both states explicit** rather than choosing one: `BehaviorAnnexValidatedDiagnosticsTest` records the corpus with the validator registered under `expected/diagnostics-validated`, `BehaviorAnnexCharacterizationTest` keeps the plain-AADL baseline, and each asserts the presence or absence of BA rule diagnostics so the two cannot be confused. 29 of the 100 corpus models reported findings only the validated run saw at that point; each BA check added since raises that share, and at this update it is 50 of 127. `BehaviorAnnexValidator` still skips all later rule checking when the type checker fails, so an absent secondary diagnostic remains uninformative. G08 was the case in point — its validated golden held the null-element holder error and therefore no D.3 rule result at all — and that golden is empty now that #3172 has landed, which removes the example without removing the gating behavior. +7. **Validator registration and gating matter.** At the review date the conformance and characterization classes used the generic AADL injector, unlike `CoveringSemanticTest` and the recent diagnostic regressions, so their goldens showed core-AADL findings only. **Step 1 made both states explicit** rather than choosing one: `BehaviorAnnexValidatedDiagnosticsTest` records the corpus with the validator registered under `expected/diagnostics-validated`, `BehaviorAnnexCharacterizationTest` keeps the plain-AADL baseline, and each asserts the presence or absence of BA rule diagnostics so the two cannot be confused. 29 of the 100 corpus models reported findings only the validated run saw at that point; each BA check added since raises that share, and at this update it is 63 of 156. `BehaviorAnnexValidator` still skips all later rule checking when the type checker fails, so an absent secondary diagnostic remains uninformative. G08 was the case in point — its validated golden held the null-element holder error and therefore no D.3 rule result at all — and that golden is empty now that #3172 has landed, which removes the example without removing the gating behavior. 8. **No test establishes that BA types are checked.** Every type-mismatch expectation in the suite passes because `conformsTo` accepts every pair (G18), not because the compared types agree. `Issue3174Test.internalEventWithoutDataCarriesNoValue` documents that for one construct. @@ -225,7 +227,7 @@ These are proposed follow-up changes, not changes made by this review. | Order | Work | Concrete evidence needed to close it | | --- | --- | --- | | 1 | ~~Repair the conformance test oracle and ensure deterministic BA validator registration. Separate legacy characterization from standard expectations.~~ **Done**, branch `repair_conformance_test_oracle` (commit `Repair the Behavior Annex conformance test oracle`). | Exact diagnostics are compared, by `expected/diagnostics` and the new `expected/diagnostics-validated`; registration is proved end to end by requiring at least one BA rule diagnostic in the validated suite and none in the plain baseline; both suites and the conformance class assert nonzero executed cases; the nine skips it left were listed in `TRACKED_SKIPS` against their own issues and enforced by reflection, and that list has shrunk to five as those issues closed; `SelfPropertyReference.aadl` no longer carries an unrelated D.3 error. Each repaired expectation was confirmed to fail for its intended reason by temporarily removing its `@Ignore`. | -| 2 | Preserve strict-model meaning: numeric literals, array extents, logical grouping, `self`, internal events, and mode bindings (G08, G10–G14). **Under way:** G08, G10, G11, G12, and G13 are closed; mode bindings (G14) remain. | External AADL input produces correct literal values, extents, references, operation kinds, and mode links; no test-only model mutation is needed. Assert attributes and semantic structure directly. | +| 2 | Preserve strict-model meaning: numeric literals, array extents, logical grouping, `self`, internal events, and mode bindings (G08, G10–G14). **Done:** G08 and G10–G14 are implemented. | External AADL input produces correct literal values, extents, references, operation kinds, and mode links; no test-only model mutation is needed. Assert attributes and semantic structure directly. | | 3 | Implement the missing standard syntax and remove unwanted overacceptance (G01–G07, G09, G13). **Under way:** G01–G05, G07, and G13 are closed; G06 and G09 remain. | Each standard form parses and translates; nonstandard forms have deliberate rejection/extension policy. Enable corrected standard acceptance tests and add AST/strict-model expression tests. | | 4 | Correct the explicit validation mismatches and add the remaining static legality checks (G15–G18, V01–V03, V06–V07, V10–V11). G18 belongs first in this step: with type conformance disabled, several of the others cannot be demonstrated. **Under way:** G16 and V01–V03 are addressed; G15, G17, G18, V06, V07, V10, and V11 remain, and the G16 dequeue form (#3205) is open. | Each negative model has an exact rule diagnostic and a nearby positive control. For G18, every diagnostic that appears in the existing corpus is triaged and its golden updated deliberately. Reproduce independently before opening an issue; use one independently reviewable defect per issue/fix. | | 5 | Establish behavioral/dataflow coverage and consumer boundaries (V04–V05, V08–V09, D.5 and D.8 runtime semantics). | State which obligations the front end can prove, which are warnings/approximations, and which belong to a simulator, analyzer, or generator. Validate queue behavior, timeouts, lock lifetimes, initialization, and call synchronization in the responsible consumer. | diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt index add0b02819b..1d0d5c0b0f0 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt @@ -1 +1 @@ -error | semantic | 45 | 3 | 66 | Transitions out of complete states must have dispatch condition : Behavior Annex D.3.(L7) legality rule failed. +error | semantic | 45 | 20 | 30 | The behavior transition tries to refine a transition mode but it is not consisting with any transition mode of exemple_cr_D3_C4::proc component: Behavior Annex D.3.(C4) consistency rule failed. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt index ff921edb018..3184f90aca5 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_covering_syntax_aadlBaTest001.txt @@ -1,6 +1,5 @@ error | semantic | 165 | 2 | 2 | NamesResolutionTest::thread1.impl can't have more than one initial state : a5, a6 : Behavior Annex D.3.(L3) legality rule failed. error | semantic | 166 | 2 | 2 | NamesResolutionTest::thread1.impl can't have more than one initial state : a5, a6 : Behavior Annex D.3.(L3) legality rule failed. error | semantic | 199 | 19 | 14 | The completion relative timeout condition and catch statement must have a value greater or equal to the Period of the thread it is defined in (otherwise) timeout condition can never occur. -error | semantic | 97 | 3 | 32 | Transitions out of complete states must have dispatch condition : Behavior Annex D.3.(L7) legality rule failed. warning | semantic | 25 | 33 | 21 | AadlBaTestPropertySet in 'with' clause of public package section is not used. warning | semantic | 25 | 75 | 20 | AadlBaTestSubprogram in 'with' clause of public package section is not used. diff --git a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt index 7dd749c71a0..e69de29bb2d 100644 --- a/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt +++ b/ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue2147_issue2147.txt @@ -1 +0,0 @@ -error | semantic | 35 | 5 | 21 | Transitions out of complete states must have dispatch condition : Behavior Annex D.3.(L7) legality rule failed. diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt index 5cc2e281033..e05a9823434 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt @@ -1,23 +1,19 @@ annex[0] owner=exemple_cr_D3_C4::proc - (BehaviorAnnex, behavior_specification, 1190, 152) - (BehaviorCondition, , 1281, 45) - (BehaviorState, finalState, 1231, 10) - (BehaviorState, m1, 1199, 2) - (BehaviorStateGroup, , 1199, 29) - (BehaviorStateGroup, , 1231, 26) - (BehaviorTransition, , 1276, 66) - (ModeSwitchCondition, , 1284, 42) - (ModeSwitchConjunction, , 1284, 19) - (ModeSwitchConjunction, , 1307, 19) - (ModeSwitchTrigger, , 1284, 7) - (ModeSwitchTrigger, , 1296, 7) - (ModeSwitchTrigger, , 1307, 7) - (ModeSwitchTrigger, , 1319, 7) - (Reference, , 1284, 7) - (Reference, , 1296, 7) - (Reference, , 1307, 7) - (Reference, , 1319, 7) - (ReferenceSegment, inPortA, 1319, 7) - (ReferenceSegment, inPortB, 1296, 7) - (ReferenceSegment, inPorta, 1284, 7) - (ReferenceSegment, inPortc, 1307, 7) + (BehaviorAnnex, behavior_specification, 1189, 149) + (BehaviorCondition, , 1280, 42) + (BehaviorState, finalState, 1230, 10) + (BehaviorState, m1, 1198, 2) + (BehaviorStateGroup, , 1198, 29) + (BehaviorStateGroup, , 1230, 26) + (BehaviorTransition, , 1275, 63) + (DispatchCondition, , 1283, 39) + (DispatchConjunction, , 1292, 19) + (DispatchConjunction, , 1315, 7) + (DispatchTriggerCondition, , 1292, 30) + (DispatchTriggerLogicalExpression, , 1292, 30) + (Reference, , 1292, 7) + (Reference, , 1304, 7) + (Reference, , 1315, 7) + (ReferenceSegment, inPortA, 1292, 7) + (ReferenceSegment, inPortB, 1304, 7) + (ReferenceSegment, inPortC, 1315, 7) diff --git a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3182_Issue3182.txt b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3182_Issue3182.txt index 04c1c76c6e3..898bfc02645 100644 --- a/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3182_Issue3182.txt +++ b/ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_issue3182_Issue3182.txt @@ -1,76 +1,76 @@ annex[0] owner=Issue3182::derived - (AssignmentAction, , 2232, 10) - (BehaviorActionBlock, , 2231, 12) - (BehaviorAnnex, behavior_specification, 2057, 271) - (BehaviorCondition, , 2258, 17) - (BehaviorCondition, , 2300, 17) - (BehaviorIntegerLiteral, , 2241, 1) - (BehaviorState, ACTIVE, 2138, 6) - (BehaviorState, finish, 2167, 6) - (BehaviorState, start, 2111, 5) - (BehaviorStateGroup, , 2111, 22) - (BehaviorStateGroup, , 2138, 24) - (BehaviorStateGroup, , 2167, 21) - (BehaviorTransition, , 2249, 37) - (BehaviorTransition, , 2291, 37) - (BehaviorTransition, begin, 2205, 39) - (BehaviorVariable, local, 2071, 5) - (BehaviorVariableGroup, , 2071, 28) - (DispatchCondition, , 2261, 14) - (DispatchCondition, , 2303, 14) - (DispatchConjunction, , 2270, 5) - (DispatchConjunction, , 2312, 5) - (DispatchTriggerCondition, , 2270, 5) - (DispatchTriggerCondition, , 2312, 5) - (DispatchTriggerLogicalExpression, , 2270, 5) - (DispatchTriggerLogicalExpression, , 2312, 5) - (Reference, , 2232, 5) - (Reference, , 2270, 5) - (Reference, , 2312, 5) - (ReferenceSegment, input, 2270, 5) - (ReferenceSegment, input, 2312, 5) - (ReferenceSegment, local, 2232, 5) + (AssignmentAction, , 2283, 10) + (BehaviorActionBlock, , 2282, 12) + (BehaviorAnnex, behavior_specification, 2108, 271) + (BehaviorCondition, , 2309, 17) + (BehaviorCondition, , 2351, 17) + (BehaviorIntegerLiteral, , 2292, 1) + (BehaviorState, ACTIVE, 2189, 6) + (BehaviorState, finish, 2218, 6) + (BehaviorState, start, 2162, 5) + (BehaviorStateGroup, , 2162, 22) + (BehaviorStateGroup, , 2189, 24) + (BehaviorStateGroup, , 2218, 21) + (BehaviorTransition, , 2300, 37) + (BehaviorTransition, , 2342, 37) + (BehaviorTransition, begin, 2256, 39) + (BehaviorVariable, local, 2122, 5) + (BehaviorVariableGroup, , 2122, 28) + (DispatchCondition, , 2312, 14) + (DispatchCondition, , 2354, 14) + (DispatchConjunction, , 2321, 5) + (DispatchConjunction, , 2363, 5) + (DispatchTriggerCondition, , 2321, 5) + (DispatchTriggerCondition, , 2363, 5) + (DispatchTriggerLogicalExpression, , 2321, 5) + (DispatchTriggerLogicalExpression, , 2363, 5) + (Reference, , 2283, 5) + (Reference, , 2321, 5) + (Reference, , 2363, 5) + (ReferenceSegment, input, 2321, 5) + (ReferenceSegment, input, 2363, 5) + (ReferenceSegment, local, 2283, 5) annex[1] owner=Issue3182::derived.impl - (AssignmentAction, , 2614, 10) - (BehaviorActionBlock, , 2613, 12) - (BehaviorAnnex, behavior_specification, 2433, 277) - (BehaviorCondition, , 2640, 17) - (BehaviorCondition, , 2682, 17) - (BehaviorIntegerLiteral, , 2623, 1) - (BehaviorState, ACTIVE, 2520, 6) - (BehaviorState, finish, 2549, 6) - (BehaviorState, start, 2493, 5) - (BehaviorStateGroup, , 2493, 22) - (BehaviorStateGroup, , 2520, 24) - (BehaviorStateGroup, , 2549, 21) - (BehaviorTransition, , 2631, 37) - (BehaviorTransition, , 2673, 37) - (BehaviorTransition, begin, 2587, 39) - (BehaviorVariable, TASK, 2454, 4) - (BehaviorVariable, local, 2447, 5) - (BehaviorVariableGroup, , 2447, 34) - (DispatchCondition, , 2643, 14) - (DispatchCondition, , 2685, 14) - (DispatchConjunction, , 2652, 5) - (DispatchConjunction, , 2694, 5) - (DispatchTriggerCondition, , 2652, 5) - (DispatchTriggerCondition, , 2694, 5) - (DispatchTriggerLogicalExpression, , 2652, 5) - (DispatchTriggerLogicalExpression, , 2694, 5) - (Reference, , 2614, 5) - (Reference, , 2652, 5) - (Reference, , 2694, 5) - (ReferenceSegment, input, 2652, 5) - (ReferenceSegment, input, 2694, 5) - (ReferenceSegment, local, 2614, 5) + (AssignmentAction, , 2665, 10) + (BehaviorActionBlock, , 2664, 12) + (BehaviorAnnex, behavior_specification, 2484, 277) + (BehaviorCondition, , 2691, 17) + (BehaviorCondition, , 2733, 17) + (BehaviorIntegerLiteral, , 2674, 1) + (BehaviorState, ACTIVE, 2571, 6) + (BehaviorState, finish, 2600, 6) + (BehaviorState, start, 2544, 5) + (BehaviorStateGroup, , 2544, 22) + (BehaviorStateGroup, , 2571, 24) + (BehaviorStateGroup, , 2600, 21) + (BehaviorTransition, , 2682, 37) + (BehaviorTransition, , 2724, 37) + (BehaviorTransition, begin, 2638, 39) + (BehaviorVariable, TASK, 2505, 4) + (BehaviorVariable, local, 2498, 5) + (BehaviorVariableGroup, , 2498, 34) + (DispatchCondition, , 2694, 14) + (DispatchCondition, , 2736, 14) + (DispatchConjunction, , 2703, 5) + (DispatchConjunction, , 2745, 5) + (DispatchTriggerCondition, , 2703, 5) + (DispatchTriggerCondition, , 2745, 5) + (DispatchTriggerLogicalExpression, , 2703, 5) + (DispatchTriggerLogicalExpression, , 2745, 5) + (Reference, , 2665, 5) + (Reference, , 2703, 5) + (Reference, , 2745, 5) + (ReferenceSegment, input, 2703, 5) + (ReferenceSegment, input, 2745, 5) + (ReferenceSegment, local, 2665, 5) annex[2] owner=Issue3182::typed - (BehaviorAnnex, behavior_specification, 2857, 185) - (BehaviorState, finish, 2979, 6) - (BehaviorState, ready, 2951, 5) - (BehaviorState, start, 2924, 5) - (BehaviorStateGroup, , 2924, 22) - (BehaviorStateGroup, , 2951, 23) - (BehaviorStateGroup, , 2979, 21) - (BehaviorTransition, begin, 3017, 25) - (BehaviorVariable, implementationData, 2871, 18) - (BehaviorVariableGroup, , 2871, 41) + (BehaviorAnnex, behavior_specification, 2908, 185) + (BehaviorState, finish, 3030, 6) + (BehaviorState, ready, 3002, 5) + (BehaviorState, start, 2975, 5) + (BehaviorStateGroup, , 2975, 22) + (BehaviorStateGroup, , 3002, 23) + (BehaviorStateGroup, , 3030, 21) + (BehaviorTransition, begin, 3068, 25) + (BehaviorVariable, implementationData, 2922, 18) + (BehaviorVariableGroup, , 2922, 41) diff --git a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt index 5d97f4f2b98..24c99cdb6f6 100644 --- a/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt +++ b/ba/org.osate.ba.tests/expected/resolved-model/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt @@ -3,10 +3,10 @@ annex[0] owner=exemple_cr_D3_C4::proc states[0] : BehaviorState name=m1 states[1] : BehaviorState name=finalState transitions[0] : BehaviorTransition - condition : ModeSwitchTriggerLogicalExpression - modeSwitchConjunctions[0] : ModeSwitchConjunction - modeSwitchTriggers[0] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortA [EventDataPort] - modeSwitchTriggers[1] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortB [EventDataPort] - modeSwitchConjunctions[1] : ModeSwitchConjunction - modeSwitchTriggers[0] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortC [EventDataPort] - modeSwitchTriggers[1] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortA [EventDataPort] + condition : DispatchCondition + dispatchTriggerCondition : DispatchTriggerLogicalExpression + dispatchConjunctions[0] : DispatchConjunction + dispatchTriggers[0] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortA [EventDataPort] + dispatchTriggers[1] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortB [EventDataPort] + dispatchConjunctions[1] : DispatchConjunction + dispatchTriggers[0] : EventDataPortHolder element=exemple_cr_D3_C4::proc.inPortC [EventDataPort] diff --git a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt index 133f665a53c..93e38f5bc9c 100644 --- a/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt +++ b/ba/org.osate.ba.tests/expected/unparse/org.osate.ba.tests_models_covering_semantic_cr_D3_C4.txt @@ -6,7 +6,7 @@ states finalState : final state ; \s\s\s transitions - m1 -[on inPorta and inPortB or inPortc and inPortA]-> finalState ; + m1 -[on dispatch inPortA and inPortB or inPortC]-> finalState ; \s\s ----- Xtext reparse ----- reparsed diff --git a/ba/org.osate.ba.tests/models/covering_semantic/cr_D3_C4.aadl b/ba/org.osate.ba.tests/models/covering_semantic/cr_D3_C4.aadl index ceb8dfb0db5..8e6833d84e4 100644 --- a/ba/org.osate.ba.tests/models/covering_semantic/cr_D3_C4.aadl +++ b/ba/org.osate.ba.tests/models/covering_semantic/cr_D3_C4.aadl @@ -23,7 +23,7 @@ package exemple_cr_D3_C4 public with Base_Types ; -process proc +thread proc features inPortA : in event data port Base_Types::Integer ; @@ -42,9 +42,9 @@ states finalState : final state ; transitions - m1 -[on inPorta and inPortB or inPortc and inPortA]-> finalState ; + m1 -[on dispatch inPortA and inPortB or inPortC]-> finalState ; **}; end proc ; -end exemple_cr_D3_C4 ; \ No newline at end of file +end exemple_cr_D3_C4 ; diff --git a/ba/org.osate.ba.tests/models/issue3182/Issue3182.aadl b/ba/org.osate.ba.tests/models/issue3182/Issue3182.aadl index 953b8c32eaf..0200d81f354 100644 --- a/ba/org.osate.ba.tests/models/issue3182/Issue3182.aadl +++ b/ba/org.osate.ba.tests/models/issue3182/Issue3182.aadl @@ -31,6 +31,8 @@ features input : in event port; modes active : initial mode; + standby : mode; + active -[input]-> standby; end base; thread implementation base.impl subcomponents diff --git a/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java index 51b903910a6..5f218b9d088 100644 --- a/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java +++ b/ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java @@ -132,8 +132,8 @@ public void eachBoundSourceChecksModeConsistency() throws Exception { resource.getContents().add(strict); var first = strict.getTransitions().get(1); var second = strict.getTransitions().get(2); - // Mode binding is not populated by the translator yet. Supply bindings through the public strict API - // to isolate C4's per-source checks from that independent limitation. + // This checker-level test intentionally binds differently named states through the public strict API. + // Issue3178Test covers production same-name binding through embedded AADL validation. first.getSourceState().setBindedMode(owner.getOwnedModes().get(0)); second.getSourceState().setBindedMode(owner.getOwnedModes().get(1)); var manager = new AnalysisErrorReporterManager(QueuingAnalysisErrorReporter.factory); diff --git a/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java b/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java index ecfa67c247c..f41149df64f 100644 --- a/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java +++ b/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java @@ -45,6 +45,7 @@ import org.osate.aadl2.DataClassifier; import org.osate.aadl2.DataPort; import org.osate.aadl2.DataSubcomponent; +import org.osate.aadl2.DefaultAnnexSubclause; import org.osate.aadl2.DirectionType; import org.osate.aadl2.Element; import org.osate.aadl2.EnumerationLiteral; @@ -58,6 +59,7 @@ import org.osate.aadl2.FeaturePrototype; import org.osate.aadl2.FeaturePrototypeBinding; import org.osate.aadl2.ListValue; +import org.osate.aadl2.Mode; import org.osate.aadl2.NamedElement; import org.osate.aadl2.NumberValue; import org.osate.aadl2.Parameter; @@ -187,21 +189,37 @@ public TranslationResult translate( final ComponentClassifier owner) { Objects.requireNonNull(source, "source"); Objects.requireNonNull(owner, "owner"); + final var modeRefinement = canRefineModes(source); var cache = (TranslationCache) EcoreUtil.getExistingAdapter(source, TranslationCache.class); if (cache == null) { cache = new TranslationCache(); source.eAdapters().add(cache); } - if (cache.result != null && cache.owner == owner) { + if (cache.result != null && cache.owner == owner && cache.modeRefinement == modeRefinement) { return cache.result; } - final var builder = new Builder(source, owner); + final var builder = new Builder(source, owner, modeRefinement); cache.owner = owner; + cache.modeRefinement = modeRefinement; cache.result = builder.translate(); return cache.result; } + /** + * Returns whether a subclause may refine the containing classifier's modes. Embedded parsing normally retains the + * modal context on the enclosing default annex; standalone callers may instead supply it on the parsed annex. + */ + public static boolean canRefineModes( + final org.osate.xtext.aadl2.ba.behaviorAnnex.BehaviorAnnex source) { + Objects.requireNonNull(source, "source"); + if (!source.getInModes().isEmpty()) { + return false; + } + return !(source.eContainer() instanceof DefaultAnnexSubclause defaultAnnex) + || defaultAnnex.getInModes().isEmpty(); + } + /** Translation output and immutable identity maps in both directions. */ public static final class TranslationResult { private final BehaviorAnnex strictAnnex; @@ -253,6 +271,7 @@ public EObject getResolvedReference(final EObject sourceSegment) { private static final class TranslationCache extends EContentAdapter { private ComponentClassifier owner; + private boolean modeRefinement; private TranslationResult result; @Override @@ -270,6 +289,7 @@ public boolean isAdapterForType(final Object type) { private static final class Builder { private final org.osate.xtext.aadl2.ba.behaviorAnnex.BehaviorAnnex source; private final ComponentClassifier owner; + private final boolean modeRefinement; private final IdentityHashMap declarativeToStrict = new IdentityHashMap<>(); private final IdentityHashMap strictToDeclarative = new IdentityHashMap<>(); private final IdentityHashMap states = @@ -280,9 +300,10 @@ private static final class Builder { private final IdentityHashMap resolvedReferences = new IdentityHashMap<>(); private Builder(final org.osate.xtext.aadl2.ba.behaviorAnnex.BehaviorAnnex source, - final ComponentClassifier owner) { + final ComponentClassifier owner, final boolean modeRefinement) { this.source = source; this.owner = owner; + this.modeRefinement = modeRefinement; } private TranslationResult translate() { @@ -361,6 +382,12 @@ private PropertyAssociation toPropertyAssociation(final BehaviorPropertyAssociat } private void translateStates(final BehaviorAnnex strict) { + Map modes = new java.util.TreeMap<>(String.CASE_INSENSITIVE_ORDER); + if (modeRefinement) { + for (final var mode : owner.getAllModes()) { + modes.put(mode.getName(), mode); + } + } for (final var group : source.getStateGroups()) { for (final var state : group.getStates()) { final var result = trace(FACTORY.createBehaviorState(), state); @@ -368,6 +395,9 @@ private void translateStates(final BehaviorAnnex strict) { result.setInitial(group.isInitial()); result.setComplete(group.isComplete()); result.setFinal(group.isFinal()); + if (group.isComplete() && state.getName() != null) { + result.setBindedMode(modes.get(state.getName())); + } strict.getStates().add(result); states.put(state, result); if (group.isInitial() && strict.getInitialState() == null) { diff --git a/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/validation/BehaviorAnnexValidator.java b/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/validation/BehaviorAnnexValidator.java index 61501f44d22..a280ea224f5 100644 --- a/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/validation/BehaviorAnnexValidator.java +++ b/ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/validation/BehaviorAnnexValidator.java @@ -92,6 +92,7 @@ public final class BehaviorAnnexValidator extends AbstractBehaviorAnnexValidator public static final String ITERATIVE_VARIABLE_TARGET = "org.osate.xtext.aadl2.ba.iterativeVariableTarget"; public static final String ARRAY_SIZE = "org.osate.xtext.aadl2.ba.arraySize"; public static final String PROPERTY_REFERENCE_VALUE = "org.osate.xtext.aadl2.ba.propertyReferenceValue"; + public static final String MODE_REFINEMENT = "org.osate.xtext.aadl2.ba.modeRefinement"; private static final URI VALIDATION_RESOURCE_URI = URI.createURI("validation:/behavior-annex.aadlba"); @Inject @@ -111,7 +112,8 @@ public boolean isLanguageSpecific() { @Check(CheckType.NORMAL) public void checkBehaviorAnnex(final BehaviorAnnex source) { if (!(source.getContainingClassifier() instanceof ComponentClassifier owner) - || !checkDeclarationNames(source, owner) || hasSyntaxOrLinkingErrors(source)) { + || !checkDeclarationNames(source, owner) || hasSyntaxOrLinkingErrors(source) + || !checkCompleteModeStates(source, owner)) { return; } @@ -415,6 +417,37 @@ private boolean checkDeclarationNames(final BehaviorAnnex source, final Componen return valid; } + /** + * In a subclause without an {@code in modes} statement, one complete state that names a mode makes the subclause a + * mode refinement. D.3 then requires every complete state in that subclause to name a mode. + */ + private boolean checkCompleteModeStates(final BehaviorAnnex source, final ComponentClassifier owner) { + if (!DeclarativeToStrictTranslator.canRefineModes(source)) { + return true; + } + var modeNames = new TreeSet(String.CASE_INSENSITIVE_ORDER); + for (var mode : owner.getAllModes()) { + modeNames.add(mode.getName()); + } + var completeStates = source.getStateGroups().stream().filter(group -> group.isComplete()) + .flatMap(group -> group.getStates().stream()).toList(); + var firstModeState = completeStates.stream().filter(state -> modeNames.contains(state.getName())).findFirst(); + if (firstModeState.isEmpty()) { + return true; + } + var modeStateName = firstModeState.orElseThrow().getName(); + var valid = true; + for (var state : completeStates) { + if (!modeNames.contains(state.getName())) { + valid = false; + error("Complete state '" + state.getName() + "' must be a mode identifier because complete state '" + + modeStateName + "' is a mode identifier: Behavior Annex D.3 legality rule failed.", state, + BehaviorAnnexPackage.eINSTANCE.getBehaviorState_Name(), MODE_REFINEMENT); + } + } + return valid; + } + private record Declaration(String name, EObject source, EStructuralFeature feature, boolean complete) { }