Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
language:langs:chp [2020/07/09 07:34]
rajit [More on channel expressions and probes]
language:langs:chp [2023/04/09 19:28] (current)
rajit [Arrays: dynamic v/s non-dynamic indices]
Line 2: Line 2:
  
 The CHP sublanguage is an evolution of Dijkstra's guarded commands notation and Hoare's CSP. It is a programming notation augmented with send/receive primitives for communication and parallel composition. A chp program is specified in ACT as follows: The CHP sublanguage is an evolution of Dijkstra's guarded commands notation and Hoare's CSP. It is a programming notation augmented with send/receive primitives for communication and parallel composition. A chp program is specified in ACT as follows:
-<code>+<code act>
 chp {  chp { 
    /* program goes here */    /* program goes here */
Line 14: Line 14:
  
    * ''skip'': does nothing    * ''skip'': does nothing
-   * ''x:=E'': assignment statement; the expression ''E'' is evaluated, and the result is assigned to variable ''x''+   * ''x:=E'': assignment statement; the [[language:expressions|expression]] ''E'' is evaluated, and the result is assigned to variable ''x''
    * ''x+'': short-hand for ''x:=true''    * ''x+'': short-hand for ''x:=true''
    * ''x-'': short-hand for ''x:=false''    * ''x-'': short-hand for ''x:=false''
-   * ''X!e'': communication action (send). The expression ''e'' is evaluated and sent over channel ''X''. Communication is blocking (slack zero). +   * ''X!e'': communication action (send). The expression ''e'' is evaluated and sent over channel ''X''. Communication is blocking (slack zero). ''X!'' is also supported, which means complete the synchronization operation. This is normally used when no data needs to be sent on the channel
-   * ''X?v'': communication action (receive). ''v'' is a variable, and the value received on channel ''X'' is assigned to ''v''+   * ''X?v'': communication action (receive). ''v'' is a variable, and the value received on channel ''X'' is assigned to ''v''. ''X?'' is also supported, which means complete the synchronization operation. This is normally used when no data needs to be sent on the channel. 
 + 
 +==== Typechecking ==== 
 + 
 +Expressions are evaluated using the [[language:expressions|standard expression rules]] for bit-width conversion. All operations are unsigned. Subtraction uses two's complement arithmetic, and unary minus computes the two's complement of the integer. 
 + 
 +Variables can be set via either assignment statements or via receive operations. When an integer variable of bit-width //w1// is set to an integer value of bitwidth //w2//, then 
 +   * If //w1//=//w2//, then a standard bit-wise assignment is performed. 
 +   * If //w1//<//w2//, then the high-order bits of the value being assigned are discarded. 
 +   * If //w1//>//w2//, the value being assigned is zero-extended prior to assignment 
 +An integer cannot be assigned a Boolean value or vice versa. Explicit conversion via ''bool()'' and ''int()'' can be used to support this functionality. 
 + 
 +The same rules outlined above apply to receive operations, where the value being assigned is the value received from the channel. To support int/bool conversion during a receive operation, we also support the following extended syntax: 
 +   * ''X?bool(v)'' : permits the assignment of a Boolean value to an integer variable ''v'' 
 +   * ''X?int(v)'' : permits the assignment of an integer value to a Boolean variable ''v''
  
 ===== Composition operators ===== ===== Composition operators =====
Line 24: Line 38:
 Sequential composition uses the '';'' separator. So ''S;T'' is the statement ''S'' followed by the statement ''T'', like many standard programming languages. Sequential composition uses the '';'' separator. So ''S;T'' is the statement ''S'' followed by the statement ''T'', like many standard programming languages.
  
-Parallel composition uses the ''||'' separator. Since circuit instances implicitly run in parallel, it is entirely possible to design a complex system without using the ''||'' operator. +Since circuit instances implicitly run in parallel, there's no actual requirement for an explicit parallel composition operator at the level of circuit modules. Internal parallelism where the two statements do not write a variable that is read by the other can use the '','' separator. The comma has a higher binding power compared to semicolon.
- +
-Internal parallelism where the two statements do not write a variable that is read by the other can use the ''.'' separator. The comma has a higher binding power compared to semicolon, and semicolon has a higher binding power than ''||''.+
  
-<code>+<code act>
   x+,y+;z-   x+,y+;z-
 </code> </code>
 This corresponds to setting ''x'' and ''y'' to true in parallel. Only after both are complete, ''z'' is set to false. This corresponds to setting ''x'' and ''y'' to true in parallel. Only after both are complete, ''z'' is set to false.
  
-==== Conditional execution ====+===== Conditional execution =====
  
 The selection statement uses the guarded command syntax. The statement The selection statement uses the guarded command syntax. The statement
-<code>+<code act>
  [ g1 -> S1  [ g1 -> S1
  [] g2 -> S2  [] g2 -> S2
Line 49: Line 61:
  
 Often a circuit simply waits for some condition to be true before proceeding. This would be written  Often a circuit simply waits for some condition to be true before proceeding. This would be written 
-<code>+<code act>
 [ cond -> skip ] [ cond -> skip ]
 </code> </code>
 This happens so often that there is syntactic sugar to support this particular construct, shown below: This happens so often that there is syntactic sugar to support this particular construct, shown below:
-<code> +<code act
-[code]+[cond]
 </code> </code>
 For example, For example,
-<code>+<code act>
  [xi];xo+  [xi];xo+
 </code> </code>
Line 65: Line 77:
  
 Sometimes the selection statement can have multiple guards that are true. This requires the use of a non-deterministic circuit (an arbiter) to resolve the choice, and introduces implementation overhead. Hence, the programmer is required to use different syntax for non-deterministic selections to make this overhead explicit and visible. A non-deterministic selection is written as follows: Sometimes the selection statement can have multiple guards that are true. This requires the use of a non-deterministic circuit (an arbiter) to resolve the choice, and introduces implementation overhead. Hence, the programmer is required to use different syntax for non-deterministic selections to make this overhead explicit and visible. A non-deterministic selection is written as follows:
-<code>+<code act>
 [| g1 -> S1 [| g1 -> S1
 [] g2 -> S2  [] g2 -> S2 
Line 75: Line 87:
 In the published literature, non-deterministic selections are usually written using a thin bar ''|'' rather than the thick bar ''[]''. However, this can create some ambiguities in parsing. For example, consider the statement ''[ a -> y:=b | c | d -> skip ]''. This can be parsed in a number of ways, and it is not clear which one was the intended option. In the published literature, non-deterministic selections are usually written using a thin bar ''|'' rather than the thick bar ''[]''. However, this can create some ambiguities in parsing. For example, consider the statement ''[ a -> y:=b | c | d -> skip ]''. This can be parsed in a number of ways, and it is not clear which one was the intended option.
  
-==== Loops ====+===== Arrays: dynamic v/s non-dynamic indices ===== 
 + 
 +Suppose an array ''x'' has been declared as: 
 +<code act> 
 +int x[10]; 
 +</code> 
 + 
 +Now when ''x'' is accessed in CHP, it could be accessed with an array index that is a run-time constant, or an index that is computed at run-time. For example, the CHP program 
 +<code act> 
 +chp { 
 +   ... 
 +   x[0] := x[0] + 1; 
 +   ... 
 +
 +</code> 
 +uses ''x'' with a constant index. As opposed to this, the program 
 +<code act> 
 +chp { 
 +   ... 
 +   x[i] := x[i] + 1; 
 +   ... 
 +
 +</code> 
 +uses ''x'' with an index that is computed using the run-time value of ''i''. This second category of arrays are referred to as //dynamic arrays//---not because the array size is dynamic, but because the element of the array accessed depends on a value that is computed by the circuit.  Such dynamic arrays have to be translated into memory structures, or other circuits where the element being accessed has to be specified at run-time. Arrays with constant references can be directly mapped to circuit implementations of asynchronous registers, since the element to be accessed can be determined statically. 
 + 
 + 
 +===== Loops =====
  
 Loops/repetitions use a syntax similar to selections, with the addition of the Kleene star.  Loops/repetitions use a syntax similar to selections, with the addition of the Kleene star. 
-<code>+<code act>
 *[ g1 -> S1 *[ g1 -> S1
 [] g2 -> S2 [] g2 -> S2
Line 88: Line 126:
  
 One of the most common cases in using loops is the infinite repetition. This is typically the "outer" loop in programs that describe most circuits. This would be written One of the most common cases in using loops is the infinite repetition. This is typically the "outer" loop in programs that describe most circuits. This would be written
-<code>+<code act>
 *[ true -> S ] *[ true -> S ]
 </code> </code>
 Since this is so common, the following syntactic sugar is provided to make this even more compact: Since this is so common, the following syntactic sugar is provided to make this even more compact:
-<code>+<code act>
 *[ S ] *[ S ]
 </code> </code>
  
 Using this, the classic greatest common divisor algorithm can be written as follows: Using this, the classic greatest common divisor algorithm can be written as follows:
-<code>+<code act>
 chp {  chp { 
  *[ X?x,Y?y;  *[ X?x,Y?y;
Line 110: Line 148:
  
 One last supported construct is a do-while loop. The main difference between the standard loop and the do-loop is that we are guaranteed that the loop will execute at least one iteration. This information can be useful during circuit synthesis. The syntax for a do-while loop is: One last supported construct is a do-while loop. The main difference between the standard loop and the do-loop is that we are guaranteed that the loop will execute at least one iteration. This information can be useful during circuit synthesis. The syntax for a do-while loop is:
-<code>+<code act>
 *[ S <- G ] *[ S <- G ]
 </code> </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. 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.
 +
 +===== Advanced expression syntax =====
  
 ==== Channels in expressions ==== ==== Channels in expressions ====
Line 119: Line 161:
 Channels can be used in expressions in two ways: Channels can be used in expressions in two ways:
    * The //explicit probe// of a channel can be used using the syntax ''#A''. The probe is a Boolean expression that indicates that there is a communication action pending/being attempted on the channel. The explicit probe is only permitted in the guards of selection statements.    * The //explicit probe// of a channel can be used using the syntax ''#A''. The probe is a Boolean expression that indicates that there is a communication action pending/being attempted on the channel. The explicit probe is only permitted in the guards of selection statements.
-   * The channel itself can be used within an expression. This is detailed below.+   * The channel itself can be used within an expression. This is detailed below. Channel expressions are not permitted in loop guards.
  
 The following program takes the arriving data on two different input channels, and merges them into a data sequence on its output channel: The following program takes the arriving data on two different input channels, and merges them into a data sequence on its output channel:
-<code>+<code act>
 *[ [| #A -> A?x *[ [| #A -> A?x
    [] #B -> B?x    [] #B -> B?x
Line 130: Line 172:
 </code> </code>
 This is sometimes called a non-deterministic merge. Note that a channel can be probed at either end (i.e. the sender end or the receiver end can probe the channel), but not at both. If we knew that the inputs on ''A'' and ''B'' are guaranteed to be mutually exclusive, then this can be written This is sometimes called a non-deterministic merge. Note that a channel can be probed at either end (i.e. the sender end or the receiver end can probe the channel), but not at both. If we knew that the inputs on ''A'' and ''B'' are guaranteed to be mutually exclusive, then this can be written
-<code>+<code act>
 *[[#A -> A?x *[[#A -> A?x
   []#B -> B?x   []#B -> B?x
Line 143: Line 185:
  
 If ''A'' is an input port, then ''A'' can participate in a //channel expression//. For example, we can write: If ''A'' is an input port, then ''A'' can participate in a //channel expression//. For example, we can write:
-<code> +<code act
-*[[A=3 -> X!true;A?+[A=3 -> X!true;A?
- []A!=3 -> X!false;A?+[]A!=3 -> X!false;A?
- ]+]
 </code> </code>
 Here, ''A=3'' is a channel expression. This has the following meaning: first, wait for a value to be pending on the input channel ''A''; then compare it to 3. In other words, this expression includes an //implicit// probe. It also permits the pending value on ''A'' to be inspected. Note that ''A!=3'' //also includes waiting for a value to be pending on the input channel//, and is not the literal negation of the condition corresponding to ''A=3''. In other words, in the program fragment above, the selection statement should be read: wait for a value to be pending on input channel ''A''; if the value is 3, do the first set of statements; otherwise pick the second set of statements. Here, ''A=3'' is a channel expression. This has the following meaning: first, wait for a value to be pending on the input channel ''A''; then compare it to 3. In other words, this expression includes an //implicit// probe. It also permits the pending value on ''A'' to be inspected. Note that ''A!=3'' //also includes waiting for a value to be pending on the input channel//, and is not the literal negation of the condition corresponding to ''A=3''. In other words, in the program fragment above, the selection statement should be read: wait for a value to be pending on input channel ''A''; if the value is 3, do the first set of statements; otherwise pick the second set of statements.
  
 Channel expressions can be used in any context that includes an expression (e.g. assignment statements, send operations). However, evaluating the expression will result in an error if the probe of the appropriate channels is false; i.e. the assignment statement //must be// non-blocking. So, if ''A'' is an input channel, the statement Channel expressions can be used in any context that includes an expression (e.g. assignment statements, send operations). However, evaluating the expression will result in an error if the probe of the appropriate channels is false; i.e. the assignment statement //must be// non-blocking. So, if ''A'' is an input channel, the statement
-<code>+<code act>
 x:=A x:=A
 </code> </code>
 might fail, the following alternative will not. might fail, the following alternative will not.
-<code>+<code act>
 [#A];x:=A [#A];x:=A
 </code> </code>
  
 +==== Functions in expressions ====
 +
 +The CHP language supports functions in expressions. These  functions can be templated, and must operate on ''int'' or ''bool'' arguments (no array arguments at present). The syntax for functions can be found with general rules for [[language:expressions|expressions]].
 ==== More on channel expressions and probes ==== ==== More on channel expressions and probes ====
  
 The interaction of Boolean expressions, probes, and channel expressions can be a bit tricky. For example, consider the following guards: The interaction of Boolean expressions, probes, and channel expressions can be a bit tricky. For example, consider the following guards:
-<code>+<code act>
 [ #A | #B -> ...  [ #A | #B -> ... 
 [] #C -> ... [] #C -> ...
Line 168: Line 213:
 </code> </code>
 The standard way ORs (and AND) operators are viewed is via short-circuit evaluation. Hence, the first guard can evaluate to true as soon as either ''#A'' or ''#B'' is true. Instead, suppose we had: The standard way ORs (and AND) operators are viewed is via short-circuit evaluation. Hence, the first guard can evaluate to true as soon as either ''#A'' or ''#B'' is true. Instead, suppose we had:
-<code>+<code act>
 [ A=0 | B=0 -> ... [ A=0 | B=0 -> ...
 [] #C -> ... [] #C -> ...
Line 176: Line 221:
  
 What about: What about:
-<code>+<code act>
 [| ~(#A | ~#B) -> ... [| ~(#A | ~#B) -> ...
 [] #C -> ... [] #C -> ...
 |] |]
 </code> </code>
-In the first guard, there is a negated probe on ''A'' and an ordinary probe on ''B''. Hence, to understand negated probes, short circuit evaluation and channel expressions, it is best to first convert the Boolean expression into negation-normal form (this is the form where negations can only appear on literals). Note that since we can mix Boolean and integer expressions, a literal might be say a comparison between two integer expressions. +In the first guard, there is a negated probe on ''A'' and an ordinary probe on ''B''. Hence, to understand negated probes, short circuit evaluation and channel expressions, it is best to first convert the Boolean expression into [[https://en.wikipedia.org/wiki/Negation_normal_form|negation-normal form]] (this is the form where negations can only appear on literals). Note that since we can mix Boolean and integer expressions, a literal might be say a comparison between two integer expressions. 
  
 Channel expressions can be handled using a combination of short-circuit evaluation and the explicit introduction of a probe. For each literal, if the literal involves a channel expression, then the literal is augmented with a conjunction of the probes needed to evaluate the literal. To see how this works, the following shows a number of channel expressions and their modified versions that make all the probes explicit. We use upper-case variables for channels, and lower-case variables for variables. Channel expressions can be handled using a combination of short-circuit evaluation and the explicit introduction of a probe. For each literal, if the literal involves a channel expression, then the literal is augmented with a conjunction of the probes needed to evaluate the literal. To see how this works, the following shows a number of channel expressions and their modified versions that make all the probes explicit. We use upper-case variables for channels, and lower-case variables for variables.
  
 ^ Original expression ^ Elaborated expression ^ Negated probe? ^ ^ Original expression ^ Elaborated expression ^ Negated probe? ^
-| ''~(#A | ~#B)'' | ''~##B'' | On ''A'' |+| ''~(#A | ~#B)'' | ''~##B'' | On ''A'' |
 | ''A = x'' | ''#A & (A = x)'' | N/A |  | ''A = x'' | ''#A & (A = x)'' | N/A | 
 | ''~(A = x)'' | ''#A & (A != x)'' | N/A | | ''~(A = x)'' | ''#A & (A != x)'' | N/A |
Line 193: Line 238:
 | ''~(x = 0 | x = A)'' | ''x != 0 & #A & (x != A)'' | N/A | | ''~(x = 0 | x = A)'' | ''x != 0 & #A & (x != A)'' | N/A |
 | ''~(x = 0 | #A & (x=A))'' | ''x != 0 & (~#A | #A & (x != A))'' | On ''A'' | | ''~(x = 0 | #A & (x=A))'' | ''x != 0 & (~#A | #A & (x != A))'' | On ''A'' |
 +
 +Note that since using a channel variable is an implicit use of the probe, channel variable expressions are disallowed in the guards of loops.
  
 In the case of integer expressions, the situation can be handled as follows. ''ERR'' is used to denote an error. In the case of integer expressions, the situation can be handled as follows. ''ERR'' is used to denote an error.
  
-^ Original expression ^  Elaborated expression ^ +^ Original expression ^ Elaborated expression ^ 
-| x + B | x + (#B ? B : ERR) | +''x + B'' ''x + (#B ? B : ERR)'' 
-| A * B + w | (#A ? A : ERR) * (#B ? B : ERR) + w |+''A * B + w'' ''(#A ? A : ERR) * (#B ? B : ERR) + w''
 +| ''A > B ? w : B + C'' | ''( (#A ? A : ERR) > (#B ? B : ERR) ) ? w : (#B ? B : ERR) + (#C ? C : ERR)'' |
  
 +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. 
  
 +===== Advanced channels =====
  
 +==== 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.
  
 +===== Syntactic replication =====
 +
 +There are three common uses of syntactic replication in CHP, and the language has syntactic support for them. The first two correspond to scenarios where you have a number of items separated by semicolon or comma. The syntax for this follows the generic template for [[language:controlflow|syntactic replication]]:
 +
 +<code act>
 +(; i : 4 : x[i] := 0)
 +</code>
 +
 +corresponds to
 +
 +<code act>
 +x[0] := 0; x[1] := 0; x[2] := 0; x[3] := 0
 +</code>
 +
 +Note the missing trailing semicolon. Following this with another statement in sequence would be written
 +
 +<code act>
 +(; i : 4 : x[i] := 0 );
 +x[0] := 1 - x[1]
 +</code>
 +
 +Similarly, the semicolon can be replaced with a comma to specify parallel execution.
 +
 +Syntactic replication is also supported for guarded commands.  The statement
 +
 +<code act>
 +[ v = 0 -> x := x  - v
 +[] ( [] i : 3 : v = i+2 -> x := x + i
 +]
 +</code>
 +
 +is the same as
 +
 +<code act>
 +[ v = 0 -> x := x - v
 +[] v = 0+2 -> x := x + 0
 +[] v = 1+2 -> x := x + 1
 +[] v = 2+2 -> x := x  + 2
 +]
 +</code>
 +
 +This construct can be used to work around one of the current restrictions of CHP. A natural way to write a merge process in ACT is:
 +<code act>
 +*[ C?c; I[c]?d; O!d ]
 +</code>
 +This will error out because the CHP has a //dynamic// channel access---i.e. the channel accessed is computed at run-time. While this is supported for int arrays, for example, that is because there is an efficient compilation mechanism for large int arrays (via memory macros). To work around this restriction, one can use:
 +<code act>
 +*[ C?c; [ ([] i : N : c = i -> I[i]?d) ]; O!d ]
 +</code>
 +where ''N'' is the number of channels in the ''I'' array. This approach ensures that index for the array ''I[]'' is always a constant.
 +
 +====== The chp-txt sublanguage ======
 +
 +Since the CHP syntax is quite different from commonly used programming languages, we have provided a variation called ''chp-txt'' that uses notation that may be a bit more familiar to programmers. Note that ''chp-txt'' is viewed internally as exactly the same as ''chp'', so only one ''chp''/''chp-txt'' block can be used in a process.
 +<code act>
 +chp-txt { 
 +   /* chp-txt program goes here */
 +}
 +</code>
 +The basic statements, expression syntax, etc. remains unchanged from the CHP language. What is different is the syntax for loops, selection statements, and short-cuts, plus additional syntax for baseline send and receive operations.
 +==== Send and receive ====
 +
 +In addition to the syntax
 +<code act>
 +X!e
 +</code>
 +for a send operation, ''chp-txt'' also supports
 +<code act>
 +send (X, e)
 +</code>
 +In addition to the syntax
 +<code act>
 +X?v
 +</code>
 +for a receive operation, ''chp-txt'' also supports
 +<code act>
 +recv (X, v)
 +</code>
 +
 +
 +==== Conditionals  ====
 +
 +The selection statement
 +<code act>
 + [ g1 -> S1  [] g2 -> S2  [] g3 -> S3  ...  [] gn -> Sn  ]
 +</code>
 +is written as follows in ''chp-txt'':
 +<code act>
 +select {
 +case g1 : S1;
 +case g2 : S2;
 +...
 +case gn: Sn
 +}
 +</code>
 +The ''else'' clause can be written ''else : Sn'' as the last item in the list of cases. 
 +
 +A non-deterministic statement is written the same way, except the keyword ''arb_select'' is used instead of ''select''.
 +
 +Waiting for a condition is a commonly used operation. This was written in chp as ''[cond]''; in ''chp-txt'', this is written
 +<code act>
 +wait-for (condition)
 +</code>
 +
 +==== Loops ====
 +
 +A simple while loop written in CHP as
 +<code act>
 +*[ G -> S ]
 +</code>
 +is written in ''chp-txt'' as:
 +<code act>
 +while (G) {
 +   S
 + }
 +</code>
 +A while loop with multiple guards of the form
 +<code act>
 +*[ G1 -> S1 [] G2 -> S2 ... [] Gn -> Sn ]
 +</code> 
 +is written as 
 +<code act>
 +while { 
 + case G1 : S1;
 + case G2 : S2;
 +  ...
 + case Gn : Sn
 +}
 +</code>
 +A do-loop is written:
 +<code act>
 +do {
 +  S 
 +} while (G)
 +</code>
 +Finally, an infinite loop is written:
 +<code act>
 +forever {
 +   S
 +}
 +</code>
 +
 +==== An example ====
 +
 +The CHP program:
 +<code act>
 +chp {
 +   *[ L?x; R!x ]
 +}
 +</code>
 +would be written in ''chp-txt'' as
 +<code act>
 +chp-txt {
 +   forever {
 +      recv (L, x); send (R, x)
 +   }
 +}
 +</code>
 +
 +The CHP program:
 +<code act>
 +chp {
 +   *[ L?x; [ x > 0 -> R!x [] else -> skip ] ]
 +}
 +</code>
 +would be written
 +<code act>
 +chp-txt {
 +   forever {
 +      recv (L, x);
 +      select {
 +        case x > 0 : send (R, x);
 +        else : skip
 +      }
 +   }
 +}   
 +</code>