123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131 |
- /* 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")
- *
- */
|