Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| language:langs:chp [2022/08/02 20:27] – [Conditionals] rajit | language:langs:chp [2025/05/23 11:56] (current) – [Syntactic replication] rajit | ||
|---|---|---|---|
| Line 45: | Line 45: | ||
| This corresponds to setting '' | This corresponds to setting '' | ||
| - | ==== Conditional execution ==== | + | ===== Conditional execution |
| The selection statement uses the guarded command syntax. The statement | The selection statement uses the guarded command syntax. The statement | ||
| Line 87: | Line 87: | ||
| In the published literature, non-deterministic selections are usually written using a thin bar '' | In the published literature, non-deterministic selections are usually written using a thin bar '' | ||
| - | ==== Loops ==== | + | ===== Arrays: dynamic v/s non-dynamic indices ===== |
| + | |||
| + | Suppose an array '' | ||
| + | <code act> | ||
| + | int x[10]; | ||
| + | </ | ||
| + | |||
| + | Now when '' | ||
| + | <code act> | ||
| + | chp { | ||
| + | ... | ||
| + | x[0] := x[0] + 1; | ||
| + | ... | ||
| + | } | ||
| + | </ | ||
| + | uses '' | ||
| + | <code act> | ||
| + | chp { | ||
| + | ... | ||
| + | x[i] := x[i] + 1; | ||
| + | ... | ||
| + | } | ||
| + | </ | ||
| + | uses '' | ||
| + | |||
| + | |||
| + | ===== Loops ===== | ||
| Loops/ | Loops/ | ||
| Line 128: | Line 154: | ||
| 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. | 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 ===== | ||
| + | |||
| + | ==== Bitslice assignment ==== | ||
| + | |||
| + | For integer-valued variables, one can assign to some of the bits. The syntax for this is: | ||
| + | |||
| + | <code act> | ||
| + | | ||
| + | ... | ||
| + | chp { | ||
| + | ... | ||
| + | x{4..2} := 4; | ||
| + | ... | ||
| + | } | ||
| + | </ | ||
| + | This will update three bits of '' | ||
| + | |||
| + | |||
| ==== Channels in expressions ==== | ==== Channels in expressions ==== | ||
| Line 158: | Line 203: | ||
| If '' | If '' | ||
| <code act> | <code act> | ||
| - | *[[A=3 -> X!true; | + | [A=3 -> X!true; |
| - | | + | []A!=3 -> X!false; |
| - | ] | + | ] |
| </ | </ | ||
| Here, '' | Here, '' | ||
| Line 221: | Line 266: | ||
| Essentially every channel variable '' | Essentially every channel variable '' | ||
| + | |||
| + | ===== Advanced channels ===== | ||
| ==== Exchange channels ==== | ==== Exchange channels ==== | ||
| Line 233: | Line 280: | ||
| Four-phase handshake channels involve two synchronizations. If you need to make this explicit in the CHP, the '' | Four-phase handshake channels involve two synchronizations. If you need to make this explicit in the CHP, the '' | ||
| - | === The chp-txt sublanguage === | + | ===== 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: | ||
| + | |||
| + | <code act> | ||
| + | (; i : 4 : x[i] := 0) | ||
| + | </ | ||
| + | |||
| + | corresponds to | ||
| + | |||
| + | <code act> | ||
| + | x[0] := 0; x[1] := 0; x[2] := 0; x[3] := 0 | ||
| + | </ | ||
| + | |||
| + | 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] | ||
| + | </ | ||
| + | |||
| + | Similarly, the semicolon can be replaced with a comma to specify parallel execution. | ||
| + | |||
| + | Syntactic replication is also supported for guarded commands. | ||
| + | |||
| + | <code act> | ||
| + | [ v = 0 -> x := x - v | ||
| + | [] ( [] i : 3 : v = i+2 -> x := x + i ) | ||
| + | ] | ||
| + | </ | ||
| + | |||
| + | 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 | ||
| + | ] | ||
| + | </ | ||
| + | |||
| + | 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 ] | ||
| + | </ | ||
| + | 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, | ||
| + | <code act> | ||
| + | *[ C?c; [ ([] i : N : c = i -> I[i]?d) ]; O!d ] | ||
| + | </ | ||
| + | where '' | ||
| + | |||
| + | ===== Debugging and other support functions for simulation ===== | ||
| + | |||
| + | When running CHP simulations, | ||
| + | |||
| + | <code act> | ||
| + | ... | ||
| + | chp { | ||
| + | ... | ||
| + | log (" | ||
| + | ... | ||
| + | } | ||
| + | </ | ||
| + | The statement above will display '' | ||
| + | |||
| + | <code act> | ||
| + | int x; | ||
| + | ... | ||
| + | chp { | ||
| + | ... | ||
| + | log (" | ||
| + | log ("%x This is hex: ", x+3); | ||
| + | log ("%b This is binary", | ||
| + | ... | ||
| + | } | ||
| + | </ | ||
| + | |||
| + | Booleans are displayed as integers, with '' | ||
| + | |||
| + | Other support functions of this type are: | ||
| + | * '' | ||
| + | * '' | ||
| + | * In the standard '' | ||
| + | * '' | ||
| + | * '' | ||
| + | * '' | ||
| + | |||
| + | |||
| + | |||
| + | ====== The chp-txt sublanguage | ||
| Since the CHP syntax is quite different from commonly used programming languages, we have provided a variation called '' | Since the CHP syntax is quite different from commonly used programming languages, we have provided a variation called '' | ||
| Line 241: | Line 377: | ||
| } | } | ||
| </ | </ | ||
| - | 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. | + | 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 | ||
| + | </ | ||
| + | for a send operation, '' | ||
| + | <code act> | ||
| + | send (X, e) | ||
| + | </ | ||
| + | In addition to the syntax | ||
| + | <code act> | ||
| + | X?v | ||
| + | </ | ||
| + | for a receive operation, '' | ||
| + | <code act> | ||
| + | recv (X, v) | ||
| + | </ | ||
| ==== Conditionals | ==== Conditionals | ||
| Line 259: | Line 414: | ||
| </ | </ | ||
| The '' | The '' | ||
| + | |||
| + | A non-deterministic statement is written the same way, except the keyword '' | ||
| + | |||
| + | Waiting for a condition is a commonly used operation. This was written in chp as '' | ||
| + | <code act> | ||
| + | wait-for (condition) | ||
| + | </ | ||
| + | |||
| + | ==== Loops ==== | ||
| + | |||
| + | A simple while loop written in CHP as | ||
| + | <code act> | ||
| + | *[ G -> S ] | ||
| + | </ | ||
| + | is written in '' | ||
| + | <code act> | ||
| + | while (G) { | ||
| + | S | ||
| + | } | ||
| + | </ | ||
| + | A while loop with multiple guards of the form | ||
| + | <code act> | ||
| + | *[ G1 -> S1 [] G2 -> S2 ... [] Gn -> Sn ] | ||
| + | </ | ||
| + | is written as | ||
| + | <code act> | ||
| + | while { | ||
| + | case G1 : S1; | ||
| + | case G2 : S2; | ||
| + | ... | ||
| + | case Gn : Sn | ||
| + | } | ||
| + | </ | ||
| + | A do-loop is written: | ||
| + | <code act> | ||
| + | do { | ||
| + | S | ||
| + | } while (G) | ||
| + | </ | ||
| + | Finally, an infinite loop is written: | ||
| + | <code act> | ||
| + | forever { | ||
| + | S | ||
| + | } | ||
| + | </ | ||
| + | |||
| + | ==== An example ==== | ||
| + | |||
| + | The CHP program: | ||
| + | <code act> | ||
| + | chp { | ||
| + | *[ L?x; R!x ] | ||
| + | } | ||
| + | </ | ||
| + | would be written in '' | ||
| + | <code act> | ||
| + | chp-txt { | ||
| + | | ||
| + | recv (L, x); send (R, x) | ||
| + | } | ||
| + | } | ||
| + | </ | ||
| + | |||
| + | The CHP program: | ||
| + | <code act> | ||
| + | chp { | ||
| + | *[ L?x; [ x > 0 -> R!x [] else -> skip ] ] | ||
| + | } | ||
| + | </ | ||
| + | would be written | ||
| + | <code act> | ||
| + | chp-txt { | ||
| + | | ||
| + | recv (L, x); | ||
| + | select { | ||
| + | case x > 0 : send (R, x); | ||
| + | else : skip | ||
| + | } | ||
| + | } | ||
| + | } | ||
| + | </ | ||