| /* VERSION 1 introduces plumbing |
| 2 increases SNARFSIZE from 4096 to 32000 |
| */ |
| #define VERSION 2 |
| |
| #define TBLOCKSIZE 512 /* largest piece of text sent to terminal */ |
| #define DATASIZE (UTFmax*TBLOCKSIZE+30) /* ... including protocol header stuff */ |
| #define SNARFSIZE 32000 /* maximum length of exchanged snarf buffer, must fit in 15 bits */ |
| /* |
| * Messages originating at the terminal |
| */ |
| typedef enum Tmesg |
| { |
| Tversion, /* version */ |
| Tstartcmdfile, /* terminal just opened command frame */ |
| Tcheck, /* ask host to poke with Hcheck */ |
| Trequest, /* request data to fill a hole */ |
| Torigin, /* gimme an Horigin near here */ |
| Tstartfile, /* terminal just opened a file's frame */ |
| Tworkfile, /* set file to which commands apply */ |
| Ttype, /* add some characters, but terminal already knows */ |
| Tcut, |
| Tpaste, |
| Tsnarf, |
| Tstartnewfile, /* terminal just opened a new frame */ |
| Twrite, /* write file */ |
| Tclose, /* terminal requests file close; check mod. status */ |
| Tlook, /* search for literal current text */ |
| Tsearch, /* search for last regular expression */ |
| Tsend, /* pretend he typed stuff */ |
| Tdclick, /* double click */ |
| Tstartsnarf, /* initiate snarf buffer exchange */ |
| Tsetsnarf, /* remember string in snarf buffer */ |
| Tack, /* acknowledge Hack */ |
| Texit, /* exit */ |
| Tplumb, /* send plumb message */ |
| TMAX |
| }Tmesg; |
| /* |
| * Messages originating at the host |
| */ |
| typedef enum Hmesg |
| { |
| Hversion, /* version */ |
| Hbindname, /* attach name[0] to text in terminal */ |
| Hcurrent, /* make named file the typing file */ |
| Hnewname, /* create "" name in menu */ |
| Hmovname, /* move file name in menu */ |
| Hgrow, /* insert space in rasp */ |
| Hcheck0, /* see below */ |
| Hcheck, /* ask terminal to check whether it needs more data */ |
| Hunlock, /* command is finished; user can do things */ |
| Hdata, /* store this data in previously allocated space */ |
| Horigin, /* set origin of file/frame in terminal */ |
| Hunlockfile, /* unlock file in terminal */ |
| Hsetdot, /* set dot in terminal */ |
| Hgrowdata, /* Hgrow + Hdata folded together */ |
| Hmoveto, /* scrolling, context search, etc. */ |
| Hclean, /* named file is now 'clean' */ |
| Hdirty, /* named file is now 'dirty' */ |
| Hcut, /* remove space from rasp */ |
| Hsetpat, /* set remembered regular expression */ |
| Hdelname, /* delete file name from menu */ |
| Hclose, /* close file and remove from menu */ |
| Hsetsnarf, /* remember string in snarf buffer */ |
| Hsnarflen, /* report length of implicit snarf */ |
| Hack, /* request acknowledgement */ |
| Hexit, |
| Hplumb, /* return plumb message to terminal - version 1 */ |
| HMAX |
| }Hmesg; |
| typedef struct Header{ |
| uchar type; /* one of the above */ |
| uchar count0; /* low bits of data size */ |
| uchar count1; /* high bits of data size */ |
| uchar data[1]; /* variable size */ |
| }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 |
| * :: t?Hgrow -> h!Trequest |
| * :: t?Hdata -> skip |
| * :: t?Hcheck0 -> h!Tcheck |
| * :: t?Hcheck -> |
| * if |
| * :: h!Trequest -> progress: h!Tcheck |
| * :: break |
| * fi |
| * od; |
| * printf("term exits\n") |
| * } |
| * |
| * 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") |
| * |
| */ |
