diff options
| author | Petter Rodhelind <petter.rodhelind@gmail.com> | 2020-01-14 11:41:08 +0100 |
|---|---|---|
| committer | Petter Rodhelind <petter.rodhelind@gmail.com> | 2020-01-14 11:41:08 +0100 |
| commit | 02d7aa8915f9c3a3288dab01f321eb94ba219e3b (patch) | |
| tree | f053238978479e408a2b83571443e132f30586ab /src/cmd/sam/mesg.h | |
| parent | c0c9d8f883dfd3a7f5a74499d91bb95884b15873 (diff) | |
| parent | 3d1382b98a502d0c34d5ba2c462396acc515016e (diff) | |
| download | plan9port-02d7aa8915f9c3a3288dab01f321eb94ba219e3b.tar.gz plan9port-02d7aa8915f9c3a3288dab01f321eb94ba219e3b.tar.bz2 plan9port-02d7aa8915f9c3a3288dab01f321eb94ba219e3b.zip | |
Merge remote-tracking branch 'upstream/master'
Diffstat (limited to 'src/cmd/sam/mesg.h')
| -rw-r--r-- | src/cmd/sam/mesg.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/cmd/sam/mesg.h b/src/cmd/sam/mesg.h index 23441499..0acf861c 100644 --- a/src/cmd/sam/mesg.h +++ b/src/cmd/sam/mesg.h @@ -79,27 +79,27 @@ typedef struct Header{ /* * File transfer protocol schematic, a la Holzmann * #define N 6 - * + * * chan h = [4] of { mtype }; * chan t = [4] of { mtype }; - * + * * mtype = { Hgrow, Hdata, * Hcheck, Hcheck0, * Trequest, Tcheck, * }; - * + * * active proctype host() * { byte n; - * + * * do * :: n < N -> n++; t!Hgrow * :: n == N -> n++; t!Hcheck0 - * + * * :: h?Trequest -> t!Hdata * :: h?Tcheck -> t!Hcheck * od * } - * + * * active proctype term() * { * do @@ -118,14 +118,14 @@ typedef struct Header{ * From: gerard@research.bell-labs.com * Date: Tue Jul 17 13:47:23 EDT 2001 * To: rob@research.bell-labs.com - * + * * spin -c (or -a) spec * pcc -DNP -o pan pan.c * pan -l - * + * * proves that there are no non-progress cycles * (infinite executions *not* passing through * the statement marked with a label starting * with the prefix "progress") - * + * */ |