ref: c4ecd0fee0f0cef485a223d6e638a56bafd5bbda
dir: /sys/src/cmd/sam/mesg.h/
/* 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") * */