Menu
▾
▴
#11 Refined CD and SM - mark the inheritance
In the event-b code it is not possible to change, for instance, a guard of an event that has been refined. It is shown in soft blue and it is read only.
But in the diagrams, for instance, the inherited guards of a refined state machine can be modified.
It should be read-only and somehow mark in the diagram as inherited properties.
In Event-B this is called 'Extends'. While no abstract guards or actions have been altered, it is not necessary to replicate them in the refinement. (the abstract guards and actions are shown in soft blue/grey). A similar facility could be provided for state-machine transitions and class methods. (An extends attribute already exists in the meta-models for this functionality to be added in the future).
I think this issue can be removed since I thought that in a refined state-machine diagram the inherited guards are seen and can be modified. I have checked it again and it does not happen.