Talk:Event Model Decomposition - Revision history

imported>Neoser at 06:27, 11 April 2012

2012-04-11T06:27:03Z

← Older revision		Revision as of 06:27, 11 April 2012
Line 18:		Line 18:
	Best regards,		Best regards,
	Son		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

imported>Son at 13:15, 10 April 2012

2012-04-10T13:15:06Z

← Older revision		Revision as of 13:15, 10 April 2012
Line 7:		Line 7:
	Best regards,		Best regards,
	Sergey		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

imported>Neoser at 12:25, 10 April 2012

2012-04-10T12:25:35Z

← Older revision		Revision as of 12:25, 10 April 2012
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\|center]]		[[Image:Decomposition.jpg\|thumb\|center\|270px]]

	Best regards,		Best regards,
	Sergey		Sergey

imported>Neoser at 12:23, 10 April 2012

2012-04-10T12:23:14Z

← Older revision		Revision as of 12:23, 10 April 2012
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

imported>Neoser at 12:21, 10 April 2012

2012-04-10T12:21:57Z

← Older revision		Revision as of 12:21, 10 April 2012
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]]		[[Image:Decomposition.jpg\|thumb]]

	Best regards,		Best regards,
	Sergey		Sergey

imported>Neoser at 12:20, 10 April 2012

2012-04-10T12:20:01Z

← Older revision		Revision as of 12:20, 10 April 2012
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:~~f:\!Work_Papers\~~Decomposition.jpg]]		[[Image:Decomposition.jpg]]

	Best regards,		Best regards,
	Sergey		Sergey

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...

2012-04-10T12:19:08Z

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...

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 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:f:\!Work_Papers\Decomposition.jpg]]

Best regards,
Sergey