In the compositional semantics entered events of a State's children are not visible. So sinceEntry(S) should only refer to states in the same NodeContainer as the transition whose guard uses sinceEntry(S). This should be addressed to prevent erroneous models from being considered. Need to check that the test-suite also addresses this in robochart-csp-gen.
Note that for the extended model with OpenStateMachine's, and for practical reasons, such a WFC should not apply. Although the state may be at the same level in the hierarchy it can most likely be in a different NodeContainer due to CompOpenStateMachine's being used.
In the compositional semantics
entered
events of a State's children are not visible. SosinceEntry(S)
should only refer to states in the sameNodeContainer
as the transition whose guard usessinceEntry(S)
. This should be addressed to prevent erroneous models from being considered. Need to check that the test-suite also addresses this in robochart-csp-gen.Note that for the extended model with OpenStateMachine's, and for practical reasons, such a WFC should not apply. Although the state may be at the same level in the hierarchy it can most likely be in a different
NodeContainer
due toCompOpenStateMachine
's being used.