Talk:Event Model Decomposition: Difference between revisions
imported>Neoser No edit summary |
imported>Neoser No edit summary |
||
| 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:Decomposition.jpg|thumb]] | [[Image:Decomposition.jpg|thumb|center]] | ||
Best regards, | Best regards, | ||
Sergey | Sergey | ||
Revision as of 12:23, 10 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
