Talk:Event Model Decomposition: Difference between revisions
imported>Neoser New page: 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 v... |
imported>Neoser No edit summary |
||
(5 intermediate revisions by 2 users not shown) | |||
Line 3: | Line 3: | ||
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. | 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. | ||
[[Image: | [[Image:Decomposition.jpg|thumb|center|270px]] | ||
Best regards, | |||
Sergey | |||
---- | |||
Dear Sergey | |||
The restriction is there to ensure that the shared variables are not being refined differently in sub-models. This ensures the compositionality of the sub-models. Recently, there is a proposal to encapsulate the shared variables in a separate module, allowing the shared variables to be refined. | |||
Best regards, | |||
Son | |||
---- | |||
Dear Son, | |||
Thank you! That would be nice to allow for refining the shared variables since many (less formal) languages support refinement of the interface. | |||
Best regards, | Best regards, | ||
Sergey | Sergey |
Latest revision as of 06:27, 11 April 2012
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
Dear Sergey
The restriction is there to ensure that the shared variables are not being refined differently in sub-models. This ensures the compositionality of the sub-models. Recently, there is a proposal to encapsulate the shared variables in a separate module, allowing the shared variables to be refined.
Best regards, Son
Dear Son,
Thank you! That would be nice to allow for refining the shared variables since many (less formal) languages support refinement of the interface.
Best regards, Sergey