I noticed when trying to look at conformance between Segway example diagrams and the original CSP that the diagrams were permitting extra behaviour in places. For example, consider:
The problem here is that this expansion permits Foo.out - in other words, the opposite direction of the event from the one that is observable on the side of the module. The original Segway CSP instead defined a restricted form of Module::sem_events that only contained the appropriate communications.
I'm not sure whether the CSP (which is used with the existing RoboChart Assertions language) uses any hiding and renaming to clean away the unused communications, or if we would be able to replace Module::sem__events with a filtered version that just contains the events visible to the robotic platform. Either way, it feels like we should technically do something here. There's no soundness issue as I understand it - the sequences are strictly more permissive than they should be? - but it's still unwanted.
This may also come up in an even worse form if we start trying to work out the correct gap semantics for multi-controller sequences.
I noticed when trying to look at conformance between Segway example diagrams and the original CSP that the diagrams were permitting extra behaviour in places. For example, consider:
This expands into CSP similar to
The problem here is that this expansion permits
Foo.out- in other words, the opposite direction of the event from the one that is observable on the side of the module. The original Segway CSP instead defined a restricted form ofModule::sem_eventsthat only contained the appropriate communications.I'm not sure whether the CSP (which is used with the existing RoboChart Assertions language) uses any hiding and renaming to clean away the unused communications, or if we would be able to replace
Module::sem__eventswith a filtered version that just contains the events visible to the robotic platform. Either way, it feels like we should technically do something here. There's no soundness issue as I understand it - the sequences are strictly more permissive than they should be? - but it's still unwanted.This may also come up in an even worse form if we start trying to work out the correct gap semantics for multi-controller sequences.