Differences

This shows you the differences between two versions of the page.

--- language:langs:chp [2021/12/29 15:35]
rajit [Basic statements]
+++ language:langs:chp [2021/12/31 19:18]
rajit
@@ Line 126: / Line 126: @@
 </code>
 A do-while loop can have only one guard. This program executes ''S'', and then evaluates the guard ''G''. If ''G'' is true, then the loop repeats; otherwise, the loop terminates.
+Loop guards can only use local variables. Hence, it is an error if a variable appearing in a loop guard is either (i) a global variable; or (ii) accessible via the port list of the process; or (iii) involves a channel probe. This ensures that loop guards cannot include any shared variables.
 ==== Channels in expressions ====
@@ Line 217: / Line 219: @@
 Essentially every channel variable ''V'' can be translated into ''(#V ? V : ERR)''. Note that this is a different translation compared to guards. Note that since probes are only allowed in guards of selection statements, negated probes are not possible in other contexts.
+==== Exchange channels ====
+Exchange channels are those where data is exchanged between sender and receiver, and this is indicated directly in the channel type. The syntax for exchange channels is:
+   * ''X!e?v'' : exchange send operation, sends ''e'' and receives into variable ''v''
+   * ''X?v!e'' : exchange receive operation, receives into ''v'' and sends the value ''e''
+In this case, we assume that the exchange send will initiate the operation, and hence only the exchange receive can be probed. This doesn't restrict functionality, since the symmetry of the exchange channel means we can simply swap the two ends.
+==== Split synchronization ====
+Four-phase handshake channels involve two synchronizations. If you need to make this explicit in the CHP, the ''!'' (send) and ''?'' (receive) operators can be replaced with ''!+'' (first half of send), ''!-'' (second half of send), or ''?+'' (first half of receive), ''?-'' (second half of receive). The second half is purely synchronization and should not have any data.