Talk:Event Model Decomposition

From Event-B
Revision as of 12:20, 10 April 2012 by imported>Neoser
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Dear the author of the article,

I do not clearly understand why shared variables and events must have a restriction that they cannot be refined in a sub-model. Suppose, we have a shared variable 's' of type BOOL. After the decomposition, this variable is data-refined with three new variables 's1', 's2' and 's3' such that 's' disappears. In this case we provide a gluing invariant, e.g. s = bool(s1=TRUE or s2=TRUE and s3=TRUE). Although 's' vanishes, we still can use it as the interface between sub-models since we have defined it as a shared variable and it still exists as the communication channel between the sub-models. Furthermore, the glueing invariant forms the precise interface between these sub-models such that it can be used to provide the required value and, therefore, no rule is broken.

Best regards, Sergey

Retrieved from ‘https://wiki.event-b.org/index.php?title=Talk:Event_Model_Decomposition&oldid=10662’