1 #define SpinVersion "Spin Version 5.1.6 -- 9 May 2008"
2 #define PanSource "buffer.spin"
5 #define ONE_L ((unsigned long) 1)
10 char *TrailFile
= PanSource
; /* default */
21 #define uchar unsigned char
24 #define uint unsigned int
28 #if NCORE>1 && !defined(SEP_STATE)
43 #define NFAIR 2 /* must be >= 2 */
47 #ifdef NP /* includes np_ demon */
50 #define endclaim 3 /* none */
52 typedef struct S_F_MAP
{
53 char *fnm
; int from
; int upto
;
56 #define nstates4 59 /* :init: */
59 0, 225, 227, 228, 229, 230, 231, 231,
60 226, 233, 226, 233, 235, 236, 237, 238,
61 238, 234, 240, 234, 240, 241, 242, 244,
62 245, 246, 247, 248, 248, 243, 250, 243,
63 250, 252, 253, 254, 255, 256, 256, 251,
64 258, 251, 224, 262, 263, 264, 266, 267,
65 271, 272, 273, 273, 265, 278, 265, 278,
67 S_F_MAP src_file4
[] = {
69 { "buffer.spin", 1, 58 },
73 0, 1, 1, 0, 0, 0, 1, 1,
74 0, 1, 1, 0, 1, 0, 0, 1,
75 1, 0, 1, 1, 0, 0, 0, 1,
76 0, 0, 0, 1, 1, 0, 1, 1,
77 0, 1, 0, 0, 0, 1, 1, 0,
78 1, 1, 0, 1, 0, 0, 1, 0,
79 0, 0, 1, 1, 0, 1, 1, 0,
83 #define nstates3 10 /* cleaner */
86 0, 210, 211, 212, 213, 209, 215, 209,
88 S_F_MAP src_file3
[] = {
90 { "buffer.spin", 1, 9 },
94 0, 1, 0, 0, 1, 0, 1, 1,
98 #define nstates2 32 /* reader */
101 0, 169, 171, 173, 174, 175, 176, 177,
102 177, 172, 179, 172, 170, 187, 189, 190,
103 191, 192, 192, 188, 194, 188, 194, 196,
104 197, 186, 199, 199, 164, 201, 164, 201,
106 S_F_MAP src_file2
[] = {
108 { "buffer.spin", 1, 31 },
111 uchar reached2
[] = {
112 0, 1, 1, 1, 0, 0, 0, 1,
113 1, 0, 1, 1, 0, 1, 1, 0,
114 0, 1, 1, 0, 1, 1, 0, 0,
115 0, 0, 1, 1, 0, 1, 1, 0,
119 #define nstates1 51 /* tracer */
122 0, 99, 100, 98, 104, 105, 106, 106,
123 103, 108, 102, 111, 111, 112, 112, 110,
124 114, 114, 116, 117, 118, 119, 120, 120,
125 115, 122, 115, 109, 127, 129, 130, 131,
126 132, 132, 128, 134, 128, 134, 135, 137,
127 137, 138, 138, 136, 140, 126, 142, 144,
129 S_F_MAP src_file1
[] = {
131 { "buffer.spin", 1, 50 },
134 uchar reached1
[] = {
135 0, 1, 0, 0, 1, 1, 1, 0,
136 1, 1, 0, 1, 1, 1, 0, 1,
137 1, 0, 1, 0, 0, 0, 1, 1,
138 0, 1, 1, 0, 1, 1, 0, 0,
139 1, 1, 0, 1, 1, 0, 0, 1,
140 0, 1, 0, 0, 1, 0, 1, 0,
144 #define nstates0 31 /* switcher */
147 0, 56, 57, 58, 61, 62, 63, 64,
148 64, 59, 66, 55, 69, 69, 70, 70,
149 68, 72, 67, 75, 76, 78, 78, 79,
150 79, 77, 81, 81, 74, 84, 85, 0, };
151 S_F_MAP src_file0
[] = {
153 { "buffer.spin", 1, 30 },
156 uchar reached0
[] = {
157 0, 1, 0, 0, 1, 0, 1, 1,
158 0, 0, 1, 0, 1, 1, 1, 0,
159 1, 1, 0, 1, 0, 1, 0, 1,
160 0, 0, 1, 0, 0, 1, 0, 0, };
180 #define T_ID unsigned char
202 #define Pinit ((P4 *)this)
203 typedef struct P4
{ /* :init: */
204 unsigned _pid
: 8; /* 0..255 */
205 unsigned _t
: 4; /* proctype */
206 unsigned _p
: 7; /* state */
212 #define Air4 (sizeof(P4) - Offsetof(P4, commit_sum) - 1*sizeof(uchar))
213 #define Pcleaner ((P3 *)this)
214 typedef struct P3
{ /* cleaner */
215 unsigned _pid
: 8; /* 0..255 */
216 unsigned _t
: 4; /* proctype */
217 unsigned _p
: 7; /* state */
219 #define Air3 (sizeof(P3) - 3)
220 #define Preader ((P2 *)this)
221 typedef struct P2
{ /* reader */
222 unsigned _pid
: 8; /* 0..255 */
223 unsigned _t
: 4; /* proctype */
224 unsigned _p
: 7; /* state */
231 #define Air2 (sizeof(P2) - Offsetof(P2, lcommit_count) - 1*sizeof(uchar))
232 #define Ptracer ((P1 *)this)
233 typedef struct P1
{ /* tracer */
234 unsigned _pid
: 8; /* 0..255 */
235 unsigned _t
: 4; /* proctype */
236 unsigned _p
: 7; /* state */
244 #define Air1 (sizeof(P1) - Offsetof(P1, j) - 1*sizeof(uchar))
245 #define Pswitcher ((P0 *)this)
246 typedef struct P0
{ /* switcher */
247 unsigned _pid
: 8; /* 0..255 */
248 unsigned _t
: 4; /* proctype */
249 unsigned _p
: 7; /* state */
255 #define Air0 (sizeof(P0) - Offsetof(P0, size) - 1*sizeof(uchar))
256 typedef struct P5
{ /* np_ */
257 unsigned _pid
: 8; /* 0..255 */
258 unsigned _t
: 4; /* proctype */
259 unsigned _p
: 7; /* state */
261 #define Air5 (sizeof(P5) - 3)
262 #if defined(BFS) && defined(REACH)
270 typedef struct Trans
{
271 short atom
; /* if &2 = atomic trans; if &8 local */
273 short escp
[HAS_UNLESS
]; /* lists the escape states */
274 short e_trans
; /* if set, this is an escp-trans */
276 short tpe
[2]; /* class of operation (for reduction) */
277 short qu
[6]; /* for conditional selections: qid's */
278 uchar ty
[6]; /* ditto: type's */
280 short om
; /* completion status of preselects */
282 char *tp
; /* src txt of statement */
283 int st
; /* the nextstate */
284 int t_id
; /* transition id, unique within proc */
285 int forw
; /* index forward transition */
286 int back
; /* index return transition */
290 #define qptr(x) (((uchar *)&now)+(int)q_offset[x])
291 #define pptr(x) (((uchar *)&now)+(int)proc_offset[x])
292 extern uchar
*Pptr(int);
293 #define q_sz(x) (((Q0 *)qptr(x))->Qlen)
296 #define VECTORSZ 1024 /* sv size in bytes */
316 #if !defined(SAFETY) && !defined(MA)
321 #if defined(SAFETY) && !defined(HASH64)
334 #if !defined(LC) && defined(SC)
338 #if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
339 /* accept the above for backward compatibility */
362 #if NCORE>1 && !defined(SEP_STATE)
363 unsigned long *ncomps
; /* in shared memory */
365 unsigned long ncomps
[256+2];
370 #define WS sizeof(void *) /* word size in bytes */
371 typedef struct Stack
{ /* for queues and processes */
392 typedef struct Svtack
{ /* for complete state vector */
397 short o_delta
; /* current size of frame */
398 short m_delta
; /* maximum size of frame */
403 #define StackSize (WS)
409 Trans
***trans
; /* 1 ptr per state per proctype */
412 int depthfound
= -1; /* loop detection */
414 int proc_offset
[MAXPROC
];
417 short proc_offset
[MAXPROC
];
418 short q_offset
[MAXQ
];
420 uchar proc_skip
[MAXPROC
];
422 unsigned long vsize
; /* vector size in bytes */
424 int vprefix
=0, svfd
; /* runtime option -pN */
426 char *tprefix
= "trail"; /* runtime option -tsuffix */
427 short boq
= -1; /* blocked_on_queue status */
428 typedef struct State
{
431 uchar _a_t
; /* cycle detection */
433 uchar _cnt
[NFAIR
]; /* counters, weak fairness */
443 uchar _last
; /* pid executed in last step */
446 #if nstates_event<256
449 unsigned short _event
;
454 uchar commit_count
[2];
456 uchar retrieve_count
[2];
463 /* hidden variable: */ uchar deliver
;
464 int _
; /* a predefined write-only variable */
466 #define FORWARD_MOVES "pan.m"
467 #define REVERSE_MOVES "pan.b"
468 #define TRANSITIONS "pan.t"
470 uchar reached5
[3]; /* np_ */
471 uchar
*loopstate5
; /* np_ */
472 #define nstates5 3 /* np_ */
473 #define endstate5 2 /* np_ */
475 #define start5 0 /* np_ */
482 #define ACCEPT_LAB 1 /* at least 1 in np_ */
484 #define ACCEPT_LAB 0 /* user-defined accept labels */
488 #warning -DMEMLIM takes precedence over -DMEMCNT
492 #warning using minimal value -DMEMCNT=20 (=1MB)
501 #error excessive value for MEMCNT
503 #define MEMLIM (1<<(MEMCNT-20))
509 #if NCORE>1 && !defined(MEMLIM)
510 #define MEMLIM (2048) /* need a default, using 2 GB */
512 #define PROG_LAB 0 /* progress labels */
526 typedef struct Q0
{ /* generic q */
527 uchar Qlen
; /* q_size */
531 /** function prototypes **/
532 char *emalloc(unsigned long);
533 char *Malloc(unsigned long);
534 int Boundcheck(int, int, int, int, Trans
*);
535 int addqueue(int, int);
536 /* int atoi(char *); */
537 /* int abort(void); */
539 int delproc(int, int);
541 int hstore(char *, int);
543 int gstore(char *, int, uchar
);
545 int q_cond(short, Trans
*);
549 int qrecv(int, int, int, int);
551 /* void *sbrk(int); */
553 void assert(int, char *, int, int, Trans
*);
554 void c_chandump(int);
555 void c_globals(void);
556 void c_locals(int, int);
557 void checkcycles(void);
558 void crack(int, int, Trans
*, short *);
559 void d_sfh(const char *, int);
560 void sfh(const char *, int);
561 void d_hash(uchar
*, int);
562 void s_hash(uchar
*, int);
563 void r_hash(uchar
*, int);
569 void imed(Trans
*, int, int, int);
570 void new_state(void);
572 void putpeg(int, int);
575 void retrans(int, int, int, short *, uchar
*, uchar
*);
577 void setq_claim(int, int, char *, int, char *);
578 void sv_restor(void);
580 void tagtable(int, int, int, short *, uchar
*);
581 void do_dfs(int, int, int, short *, uchar
*, uchar
*);
583 void unrecv(int, int, int, int, int);
585 void wrap_stats(void);
586 #if defined(FULLSTACK) && defined(BITSTATE)
587 int onstack_now(void);
588 void onstack_init(void);
589 void onstack_put(void);
590 void onstack_zap(void);
593 int q_S_check(int, int);
594 int q_R_check(int, int);
595 uchar q_claim
[MAXQ
+1];
596 char *q_name
[MAXQ
+1];
597 char *p_name
[MAXPROC
+1];
599 void qsend(int, int, int);
600 #define Addproc(x) addproc(x)
This page took 0.041131 seconds and 4 git commands to generate.