141 lines
4.1 KiB
C
141 lines
4.1 KiB
C
|
/*
|
||
|
* This file is part of the UCB release of Plan 9. It is subject to the license
|
||
|
* terms in the LICENSE file found in the top-level directory of this
|
||
|
* distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
|
||
|
* part of the UCB release of Plan 9, including this file, may be copied,
|
||
|
* modified, propagated, or distributed except according to the terms contained
|
||
|
* in the LICENSE file.
|
||
|
*/
|
||
|
|
||
|
/* 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{
|
||
|
uint8_t type; /* one of the above */
|
||
|
uint8_t count0; /* low bits of data size */
|
||
|
uint8_t count1; /* high bits of data size */
|
||
|
uint8_t 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")
|
||
|
*
|
||
|
*/
|