1 #define SpinVersion "Spin Version 5.1.6 -- 9 May 2008"
2 #define PanSource "model.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 #if !defined(NOCLAIM) && !defined NP
54 #define endclaim endstate5
56 typedef struct S_F_MAP
{
57 char *fnm
; int from
; int upto
;
60 #define nstates5 15 /* :never: */
61 #define nstates_claim nstates5
64 0, 301, 301, 302, 302, 300, 304, 306,
65 306, 307, 307, 305, 309, 310, 311, 0, };
66 S_F_MAP src_file5
[] = {
71 #define src_claim src_ln5
73 0, 1, 1, 1, 1, 0, 1, 1,
74 1, 1, 1, 0, 1, 1, 0, 0, };
76 #define reached_claim reached5
78 #define nstates4 44 /* :init: */
81 0, 252, 254, 255, 256, 257, 257, 253,
82 260, 253, 260, 262, 264, 265, 266, 267,
83 267, 263, 269, 263, 269, 270, 271, 273,
84 274, 275, 276, 277, 277, 272, 279, 272,
85 279, 281, 282, 283, 284, 285, 285, 280,
86 287, 280, 251, 288, 0, };
87 S_F_MAP src_file4
[] = {
93 0, 1, 1, 0, 0, 1, 1, 0,
94 1, 1, 0, 0, 1, 0, 0, 1,
95 1, 0, 1, 1, 0, 0, 0, 1,
96 0, 0, 0, 1, 1, 0, 1, 1,
97 0, 1, 0, 0, 0, 1, 1, 0,
101 #define nstates3 10 /* cleaner */
104 0, 237, 238, 239, 240, 236, 242, 236,
106 S_F_MAP src_file3
[] = {
111 uchar reached3
[] = {
112 0, 1, 0, 0, 1, 0, 1, 1,
116 #define nstates2 30 /* reader */
119 0, 200, 202, 204, 205, 206, 207, 208,
120 208, 203, 210, 203, 201, 216, 218, 219,
121 220, 221, 221, 217, 223, 217, 223, 215,
122 225, 225, 195, 227, 195, 227, 0, };
123 S_F_MAP src_file2
[] = {
125 { "pan.___", 1, 29 },
128 uchar reached2
[] = {
129 0, 1, 1, 1, 0, 0, 0, 1,
130 1, 0, 1, 1, 0, 1, 1, 0,
131 0, 1, 1, 0, 1, 1, 0, 0,
132 1, 1, 0, 1, 1, 0, 0, };
135 #define nstates1 52 /* tracer */
138 0, 123, 124, 122, 128, 129, 130, 130,
139 127, 132, 126, 135, 135, 136, 136, 134,
140 138, 138, 140, 141, 142, 143, 144, 144,
141 139, 146, 139, 133, 152, 154, 155, 156,
142 157, 157, 153, 159, 153, 159, 161, 164,
143 167, 168, 169, 170, 165, 172, 151, 174,
144 176, 178, 173, 180, 0, };
145 S_F_MAP src_file1
[] = {
147 { "pan.___", 1, 51 },
150 uchar reached1
[] = {
151 0, 1, 0, 0, 1, 1, 1, 0,
152 1, 1, 0, 1, 1, 1, 0, 1,
153 1, 0, 1, 0, 0, 0, 1, 1,
154 0, 1, 1, 0, 1, 1, 0, 0,
155 1, 1, 0, 1, 1, 0, 0, 0,
156 1, 0, 1, 0, 0, 1, 0, 1,
160 #define nstates0 32 /* switcher */
163 0, 72, 73, 74, 77, 78, 79, 80,
164 80, 75, 82, 71, 85, 85, 86, 86,
165 84, 88, 83, 91, 93, 96, 99, 100,
166 101, 102, 97, 104, 104, 90, 107, 108,
168 S_F_MAP src_file0
[] = {
170 { "pan.___", 1, 31 },
173 uchar reached0
[] = {
174 0, 1, 0, 0, 1, 0, 1, 1,
175 0, 0, 1, 0, 1, 1, 1, 0,
176 1, 1, 0, 1, 0, 0, 1, 0,
177 1, 0, 0, 1, 0, 0, 1, 0,
199 #define T_ID unsigned char
222 typedef struct P5
{ /* :never: */
223 unsigned _pid
: 8; /* 0..255 */
224 unsigned _t
: 4; /* proctype */
225 unsigned _p
: 7; /* state */
227 #define Air5 (sizeof(P5) - 3)
228 #define Pinit ((P4 *)this)
229 typedef struct P4
{ /* :init: */
230 unsigned _pid
: 8; /* 0..255 */
231 unsigned _t
: 4; /* proctype */
232 unsigned _p
: 7; /* state */
238 #define Air4 (sizeof(P4) - Offsetof(P4, commit_sum) - 1*sizeof(uchar))
239 #define Pcleaner ((P3 *)this)
240 typedef struct P3
{ /* cleaner */
241 unsigned _pid
: 8; /* 0..255 */
242 unsigned _t
: 4; /* proctype */
243 unsigned _p
: 7; /* state */
245 #define Air3 (sizeof(P3) - 3)
246 #define Preader ((P2 *)this)
247 typedef struct P2
{ /* reader */
248 unsigned _pid
: 8; /* 0..255 */
249 unsigned _t
: 4; /* proctype */
250 unsigned _p
: 7; /* state */
254 #define Air2 (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar))
255 #define Ptracer ((P1 *)this)
256 typedef struct P1
{ /* tracer */
257 unsigned _pid
: 8; /* 0..255 */
258 unsigned _t
: 4; /* proctype */
259 unsigned _p
: 7; /* state */
267 #define Air1 (sizeof(P1) - Offsetof(P1, j) - 1*sizeof(uchar))
268 #define Pswitcher ((P0 *)this)
269 typedef struct P0
{ /* switcher */
270 unsigned _pid
: 8; /* 0..255 */
271 unsigned _t
: 4; /* proctype */
272 unsigned _p
: 7; /* state */
278 #define Air0 (sizeof(P0) - Offsetof(P0, size) - 1*sizeof(uchar))
279 typedef struct P6
{ /* np_ */
280 unsigned _pid
: 8; /* 0..255 */
281 unsigned _t
: 4; /* proctype */
282 unsigned _p
: 7; /* state */
284 #define Air6 (sizeof(P6) - 3)
285 #if defined(BFS) && defined(REACH)
293 typedef struct Trans
{
294 short atom
; /* if &2 = atomic trans; if &8 local */
296 short escp
[HAS_UNLESS
]; /* lists the escape states */
297 short e_trans
; /* if set, this is an escp-trans */
299 short tpe
[2]; /* class of operation (for reduction) */
300 short qu
[6]; /* for conditional selections: qid's */
301 uchar ty
[6]; /* ditto: type's */
303 short om
; /* completion status of preselects */
305 char *tp
; /* src txt of statement */
306 int st
; /* the nextstate */
307 int t_id
; /* transition id, unique within proc */
308 int forw
; /* index forward transition */
309 int back
; /* index return transition */
313 #define qptr(x) (((uchar *)&now)+(int)q_offset[x])
314 #define pptr(x) (((uchar *)&now)+(int)proc_offset[x])
315 extern uchar
*Pptr(int);
316 #define q_sz(x) (((Q0 *)qptr(x))->Qlen)
319 #define VECTORSZ 1024 /* sv size in bytes */
339 #if !defined(SAFETY) && !defined(MA)
344 #if defined(SAFETY) && !defined(HASH64)
357 #if !defined(LC) && defined(SC)
361 #if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
362 /* accept the above for backward compatibility */
385 #if NCORE>1 && !defined(SEP_STATE)
386 unsigned long *ncomps
; /* in shared memory */
388 unsigned long ncomps
[256+2];
393 #define WS sizeof(void *) /* word size in bytes */
394 typedef struct Stack
{ /* for queues and processes */
415 typedef struct Svtack
{ /* for complete state vector */
420 short o_delta
; /* current size of frame */
421 short m_delta
; /* maximum size of frame */
426 #define StackSize (WS)
432 Trans
***trans
; /* 1 ptr per state per proctype */
435 int depthfound
= -1; /* loop detection */
437 int proc_offset
[MAXPROC
];
440 short proc_offset
[MAXPROC
];
441 short q_offset
[MAXQ
];
443 uchar proc_skip
[MAXPROC
];
445 unsigned long vsize
; /* vector size in bytes */
447 int vprefix
=0, svfd
; /* runtime option -pN */
449 char *tprefix
= "trail"; /* runtime option -tsuffix */
450 short boq
= -1; /* blocked_on_queue status */
451 typedef struct State
{
454 uchar _a_t
; /* cycle detection */
456 uchar _cnt
[NFAIR
]; /* counters, weak fairness */
466 uchar _last
; /* pid executed in last step */
469 #if nstates_event<256
472 unsigned short _event
;
477 uchar commit_count
[2];
486 /* hidden variable: */ uchar deliver
;
487 int _
; /* a predefined write-only variable */
489 #define FORWARD_MOVES "pan.m"
490 #define REVERSE_MOVES "pan.b"
491 #define TRANSITIONS "pan.t"
493 uchar reached6
[3]; /* np_ */
494 uchar
*loopstate6
; /* np_ */
495 #define nstates6 3 /* np_ */
496 #define endstate6 2 /* np_ */
498 #define start6 0 /* np_ */
500 #define start_claim 5
507 #define ACCEPT_LAB 1 /* at least 1 in np_ */
509 #define ACCEPT_LAB 1 /* user-defined accept labels */
513 #warning -DMEMLIM takes precedence over -DMEMCNT
517 #warning using minimal value -DMEMCNT=20 (=1MB)
526 #error excessive value for MEMCNT
528 #define MEMLIM (1<<(MEMCNT-20))
534 #if NCORE>1 && !defined(MEMLIM)
535 #define MEMLIM (2048) /* need a default, using 2 GB */
537 #define PROG_LAB 0 /* progress labels */
551 typedef struct Q0
{ /* generic q */
552 uchar Qlen
; /* q_size */
556 /** function prototypes **/
557 char *emalloc(unsigned long);
558 char *Malloc(unsigned long);
559 int Boundcheck(int, int, int, int, Trans
*);
560 int addqueue(int, int);
561 /* int atoi(char *); */
562 /* int abort(void); */
564 int delproc(int, int);
566 int hstore(char *, int);
568 int gstore(char *, int, uchar
);
570 int q_cond(short, Trans
*);
574 int qrecv(int, int, int, int);
576 /* void *sbrk(int); */
578 void assert(int, char *, int, int, Trans
*);
579 void c_chandump(int);
580 void c_globals(void);
581 void c_locals(int, int);
582 void checkcycles(void);
583 void crack(int, int, Trans
*, short *);
584 void d_sfh(const char *, int);
585 void sfh(const char *, int);
586 void d_hash(uchar
*, int);
587 void s_hash(uchar
*, int);
588 void r_hash(uchar
*, int);
594 void imed(Trans
*, int, int, int);
595 void new_state(void);
597 void putpeg(int, int);
600 void retrans(int, int, int, short *, uchar
*, uchar
*);
602 void setq_claim(int, int, char *, int, char *);
603 void sv_restor(void);
605 void tagtable(int, int, int, short *, uchar
*);
606 void do_dfs(int, int, int, short *, uchar
*, uchar
*);
608 void unrecv(int, int, int, int, int);
610 void wrap_stats(void);
611 #if defined(FULLSTACK) && defined(BITSTATE)
612 int onstack_now(void);
613 void onstack_init(void);
614 void onstack_put(void);
615 void onstack_zap(void);
618 int q_S_check(int, int);
619 int q_R_check(int, int);
620 uchar q_claim
[MAXQ
+1];
621 char *q_name
[MAXQ
+1];
622 char *p_name
[MAXPROC
+1];
624 void qsend(int, int, int);
625 #define Addproc(x) addproc(x)
This page took 0.044175 seconds and 4 git commands to generate.