ref: a60e9f279604c56fc4c74054bc01f93f3e6debef
dir: /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")
*
*/