Dear Alireza,
The intuition behind the variables that model context is the following:
- "a_c" is *T*rue means that the source end "a" sends a reason for
no-flow *T*o the connector.
- "a_k" is *F*alse means that the sink end "a" gets a reason for
no-flow *F*rom the connector.
Your expression is a conjunction of 3 elements. The first captures
synchronous and data constraints, as you pointed out. The second
$\lnot a_c$ imposes that "a_c" must be False, that is, the LossySync
must always get a reason From the connector for no-flow. Finally, the
last $\lnot a -> b_k$ says that, whenever there is no-flow on "a" (and
consequently also on "b" because of the first part of the
constraints), then "b_k" must be True, i.e., send a reason To the
connector.
Note that these constraints are slightly different from the context
constraints that me and Dave initially proposed. For example, in the
formula from Behnaz's paper the variable "a_c" is always requiring a
reason, independently of data flowing on "a". This kind of
optimisation only works by assuming that all source ports with flow do
not impose any restriction on the context-variables. In my
perspective, a safer approach would be write $\lnot a \to \lnot a_c$.
I hope this helps.
Best,
José
--
Jose Proenca
http://people.cs.kuleuven.be/~jose.proenca
Disclaimer:
http://www.kuleuven.be/cwis/email_disclaimer.htm