1 /***** spin: pangen3.h *****/
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
12 static char *Head0[] = {
13 "#if defined(BFS) && defined(REACH)",
14 "#undef REACH", /* redundant with bfs */
21 "typedef struct Trans {",
22 " short atom; /* if &2 = atomic trans; if &8 local */",
24 " short escp[HAS_UNLESS]; /* lists the escape states */",
25 " short e_trans; /* if set, this is an escp-trans */",
27 " short tpe[2]; /* class of operation (for reduction) */",
28 " short qu[6]; /* for conditional selections: qid's */",
29 " uchar ty[6]; /* ditto: type's */",
31 " short om; /* completion status of preselects */",
33 " char *tp; /* src txt of statement */",
34 " int st; /* the nextstate */",
35 " int t_id; /* transition id, unique within proc */",
36 " int forw; /* index forward transition */",
37 " int back; /* index return transition */",
38 " struct Trans *nxt;",
40 "#define qptr(x) (((uchar *)&now)+(int)q_offset[x])",
41 "#define pptr(x) (((uchar *)&now)+(int)proc_offset[x])",
42 /* "#define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", */
43 "extern uchar *Pptr(int);",
45 "#define q_sz(x) (((Q0 *)qptr(x))->Qlen)\n",
47 "#define VECTORSZ 1024 /* sv size in bytes */",
52 static char *Header[] = {
70 "#if !defined(SAFETY) && !defined(MA)",
75 "#ifdef SAFETY && !defined(HASH64)",
88 "#if !defined(LC) && defined(SC)",
92 "#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)",
93 "/* accept the above for backward compatibility */",
100 "#ifdef HC0", /* 32 bits */
103 "#ifdef HC1", /* 32+8 bits */
106 "#ifdef HC2", /* 32+16 bits */
109 "#ifdef HC3", /* 32+24 bits */
112 "#ifdef HC4", /* 32+32 bits - combine with -DMA=8 */
116 "unsigned long ncomps[256+2];",
120 "#define MAXPROC 255",
121 "#define WS sizeof(long) /* word size in bytes */",
122 "typedef struct Stack { /* for queues and processes */",
123 "#if VECTORSZ>32000",
139 " struct Stack *nxt;",
140 " struct Stack *lst;",
142 "typedef struct Svtack { /* for complete state vector */",
143 "#if VECTORSZ>32000",
147 " short o_delta; /* current size of frame */",
148 " short m_delta; /* maximum size of frame */",
156 static char *Header0[] = {
158 " struct Svtack *nxt;",
159 " struct Svtack *lst;",
161 "Trans ***trans; /* 1 ptr per state per proctype */\n",
162 "#if defined(FULLSTACK) || defined(BFS)",
163 "struct H_el *Lstate;",
165 "int depthfound = -1; /* loop detection */",
166 "#if VECTORSZ>32000",
167 "int proc_offset[MAXPROC];",
168 "int q_offset[MAXQ];",
170 "short proc_offset[MAXPROC];",
171 "short q_offset[MAXQ];",
173 "uchar proc_skip[MAXPROC];",
174 "uchar q_skip[MAXQ];",
175 "unsigned long vsize; /* vector size in bytes */",
177 "int vprefix=0, svfd; /* runtime option -pN */",
179 "char *tprefix = \"trail\"; /* runtime option -tsuffix */",
180 "short boq = -1; /* blocked_on_queue status */",
184 static char *Head1[] = {
185 "typedef struct State {",
188 " uchar _a_t; /* cycle detection */",
190 in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs
191 bit 1 is used as the A-bit for fairness
192 bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance)
195 " uchar _cnt[NFAIR]; /* counters, weak fairness */",
202 * noticed alignment problems with some Solaris
203 * compilers, if widest field isn't wordsized
206 "#if VECTORSZ<65536",
208 " unsigned short _vsz;",
210 " unsigned long _vsz;",
214 "#ifdef HAS_LAST", /* cannot go before _cnt - see hstore() */
215 " uchar _last; /* pid executed in last step */",
217 "#ifdef EVENT_TRACE",
218 "#if nstates_event<256",
221 " unsigned short _event;",
227 static char *Addp0[] = {
228 /* addproc(....parlist... */ ")",
229 "{ int j, h = now._nr_pr;",
233 " uchar *o_this = this;\n",
235 " if (TstOnly) return (h < MAXPROC);",
237 "#ifndef NOBOUNDCHECK",
238 "/* redefine Index only within this procedure */",
240 "#define Index(x, y) Boundcheck(x, y, 0, 0, 0)",
242 " if (h >= MAXPROC)",
243 " Uerror(\"too many processes\");",
245 " case 0: j = sizeof(P0); break;",
249 static char *Addp1[] = {
250 " default: Uerror(\"bad proc - addproc\");",
253 " proc_skip[h] = WS-(vsize%%WS);",
255 " proc_skip[h] = 0;",
257 " for (k = vsize + (int) proc_skip[h]; k > vsize; k--)",
258 " Mask[k-1] = 1; /* align */",
260 " vsize += (int) proc_skip[h];",
261 " proc_offset[h] = vsize;",
265 " write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */",
266 " write(svfd, (uchar *) &h, sizeof(int));",
267 " write(svfd, (uchar *) &n, sizeof(int));",
268 "#if VECTORSZ>32000",
269 " write(svfd, (uchar *) &proc_offset[h], sizeof(int));",
271 " write(svfd, (uchar *) &proc_offset[h], sizeof(short));",
273 " write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
277 " if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))",
278 " { printf(\"pan: error: too many processes -- current\");",
279 " printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",",
280 " (8*NFAIR)/2 - 2, NFAIR);",
281 " printf(\"\\trecompile with -DNFAIR=%%d\\n\",",
288 " now._vsz = vsize;",
291 " for (k = 1; k <= Air[n]; k++)",
292 " Mask[vsize - k] = 1; /* pad */",
293 " Mask[vsize-j] = 1; /* _pid */",
295 " hmax = max(hmax, vsize);",
296 " if (vsize >= VECTORSZ)",
297 " { printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",
298 " printf(\" with -DVECTORSZ=N with N>%%d\\n\", vsize);",
299 " Uerror(\"aborting\");",
301 " memset((char *)pptr(h), 0, j);",
303 " if (BASE > 0 && h > 0)",
304 " ((P0 *)this)->_pid = h-BASE;",
306 " ((P0 *)this)->_pid = h;",
311 static char *Addq0[] = {
313 "addqueue(int n, int is_rv)",
314 "{ int j=0, i = now._nr_qs;",
319 " Uerror(\"too many queues\");",
324 static char *Addq1[] = {
325 " default: Uerror(\"bad queue - addqueue\");",
328 " q_skip[i] = WS-(vsize%%WS);",
334 " if (is_rv) k += j;",
336 " for (k += (int) q_skip[i]; k > vsize; k--)",
339 " vsize += (int) q_skip[i];",
340 " q_offset[i] = vsize;",
344 " now._vsz = vsize;",
346 " hmax = max(hmax, vsize);",
347 " if (vsize >= VECTORSZ)",
348 " Uerror(\"VECTORSZ is too small, edit pan.h\");",
349 " memset((char *)qptr(i), 0, j);",
350 " ((Q0 *)qptr(i))->_t = n;",
356 static char *Addq11[] = {
357 "{ int j; uchar *z;\n",
362 " uerror(\"ref to uninitialized chan name (sending)\");",
363 " if (into >= (int) now._nr_qs || into < 0)",
364 " Uerror(\"qsend bad queue#\");",
366 " j = ((Q0 *)qptr(into))->Qlen;",
367 " switch (((Q0 *)qptr(into))->_t) {",
371 static char *Addq2[] = {
372 " case 0: printf(\"queue %%d was deleted\\n\", into+1);",
373 " default: Uerror(\"bad queue - qsend\");",
375 "#ifdef EVENT_TRACE",
376 " if (in_s_scope(into+1))",
377 " require('s', into);",
385 " { uerror(\"ref to uninitialized chan name (q_zero)\");",
388 " switch(((Q0 *)qptr(from))->_t) {",
392 static char *Addq3[] = {
393 " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
395 " Uerror(\"bad queue q-zero\");",
400 "{ if (q_zero(from))",
401 " { printf(\"==>> a test of the contents of a rv \");",
402 " printf(\"channel always returns FALSE\\n\");",
403 " uerror(\"error to poll rendezvous channel\");",
410 "setq_claim(int x, int m, char *s, int y, char *p)",
412 " uerror(\"x[rs] claim on uninitialized channel\");",
413 " if (x < 0 || x > MAXQ)",
414 " Uerror(\"cannot happen setq_claim\");",
418 " if (m&2) q_S_check(x, y);",
419 " if (m&1) q_R_check(x, y);",
421 "short q_sender[MAXQ+1];",
423 "q_S_check(int x, int who)",
424 "{ if (!q_sender[x])",
425 " { q_sender[x] = who+1;",
428 " { printf(\"chan %%s (%%d), \",",
430 " printf(\"sndr proc %%s (%%d)\\n\",",
431 " p_name[who], who);",
432 " uerror(\"xs chans cannot be used for rv\");",
436 " if (q_sender[x] != who+1)",
437 " { printf(\"pan: xs assertion violated: \");",
438 " printf(\"access to chan <%%s> (%%d)\\npan: by \",",
440 " if (q_sender[x] > 0 && p_name[q_sender[x]-1])",
441 " printf(\"%%s (proc %%d) and by \",",
442 " p_name[q_sender[x]-1], q_sender[x]-1);",
443 " printf(\"%%s (proc %%d)\\n\",",
444 " p_name[who], who);",
445 " uerror(\"error, partial order reduction invalid\");",
449 "short q_recver[MAXQ+1];",
451 "q_R_check(int x, int who)",
452 "{ if (!q_recver[x])",
453 " { q_recver[x] = who+1;",
456 " { printf(\"chan %%s (%%d), \",",
458 " printf(\"recv proc %%s (%%d)\\n\",",
459 " p_name[who], who);",
460 " uerror(\"xr chans cannot be used for rv\");",
464 " if (q_recver[x] != who+1)",
465 " { printf(\"pan: xr assertion violated: \");",
466 " printf(\"access to chan %%s (%%d)\\npan: \",",
468 " if (q_recver[x] > 0 && p_name[q_recver[x]-1])",
469 " printf(\"by %%s (proc %%d) and \",",
470 " p_name[q_recver[x]-1], q_recver[x]-1);",
471 " printf(\"by %%s (proc %%d)\\n\",",
472 " p_name[who], who);",
473 " uerror(\"error, partial order reduction invalid\");",
481 " uerror(\"ref to uninitialized chan name (len)\");",
482 " return ((Q0 *)qptr(x))->Qlen;",
487 " uerror(\"ref to uninitialized chan name (qfull)\");",
488 " switch(((Q0 *)qptr(from))->_t) {",
492 static char *Addq4[] = {
493 " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
495 " Uerror(\"bad queue - q_full\");",
501 "{ /* empty or full */",
502 " return !q_len(from) || q_full(from);",
507 "qrecv(int from, int slot, int fld, int done)",
511 " uerror(\"ref to uninitialized chan name (receiving)\");",
512 " if (from >= (int) now._nr_qs || from < 0)",
513 " Uerror(\"qrecv bad queue#\");",
515 "#ifdef EVENT_TRACE",
516 " if (done && (in_r_scope(from+1)))",
517 " require('r', from);",
519 " switch (((Q0 *)qptr(from))->_t) {",
523 static char *Addq5[] = {
524 " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
525 " default: Uerror(\"bad queue - qrecv\");",
533 "col_q(int i, char *z)",
536 " Q0 *ptr = (Q0 *) qptr(i);",
537 " switch (ptr->_t) {",
541 static char *Code0[] = {
545 " memset((char *)&now, 0, sizeof(State));",
546 " vsize = (unsigned long) (sizeof(State) - VECTORSZ);",
548 " now._vsz = vsize;",
550 "/* optional provisioning statements, e.g. to */",
551 "/* set hidden variables, used as constants */",
559 static char *R0[] = {
560 " Maxbody = max(Maxbody, sizeof(P%d));",
561 " reached[%d] = reached%d;",
562 " accpstate[%d] = (uchar *) emalloc(nstates%d);",
563 " progstate[%d] = (uchar *) emalloc(nstates%d);",
564 " stopstate[%d] = (uchar *) emalloc(nstates%d);",
565 " visstate[%d] = (uchar *) emalloc(nstates%d);",
566 " mapstate[%d] = (short *) emalloc(nstates%d * sizeof(short));",
568 " NrStates[%d] = nstates%d;",
570 " stopstate[%d][endstate%d] = 1;",
574 static char *R0a[] = {
575 " retrans(%d, nstates%d, start%d, src_ln%d, reached%d);",
578 static char *R0b[] = {
579 " if (state_tables)",
580 " { printf(\"\\nTransition Type: \");",
581 " printf(\"A=atomic; D=d_step; L=local; G=global\\n\");",
582 " printf(\"Source-State Labels: \");",
583 " printf(\"p=progress; e=end; a=accept;\\n\");",
585 " printf(\"Note: statement merging was used. Only the first\\n\");",
586 " printf(\" stmnt executed in each merge sequence is shown\\n\");",
587 " printf(\" (use spin -a -o3 to disable statement merging)\\n\");",
594 static char *Code1[] = {
596 "#define ACCEPT_LAB 1 /* at least 1 in np_ */",
598 "#define ACCEPT_LAB %d /* user-defined accept labels */",
603 static char *Code3[] = {
604 "#define PROG_LAB %d /* progress labels */",
608 static char *R2[] = {
609 "uchar *accpstate[%d];",
610 "uchar *progstate[%d];",
611 "uchar *reached[%d];",
612 "uchar *stopstate[%d];",
613 "uchar *visstate[%d];",
614 "short *mapstate[%d];",
620 static char *R3[] = {
621 " Maxbody = max(Maxbody, sizeof(Q%d));",
624 static char *R4[] = {
625 " r_ck(reached%d, nstates%d, %d, src_ln%d, src_file%d);",
628 static char *R5[] = {
629 " case %d: j = sizeof(P%d); break;",
632 static char *R6[] = {
636 "#ifndef NOBOUNDCHECK",
638 "#define Index(x, y) Boundcheck(x, y, II, tt, t)",
641 "#if defined(BITSTATE) && defined(COLLAPSE)",
642 "/* just to allow compilation, to generate the error */",
643 "long col_p(int i, char *z) { return 0; }",
644 "long col_q(int i, char *z) { return 0; }",
649 "col_p(int i, char *z)",
650 "{ int j, k; unsigned long ordinal(char *, long, short);",
652 " P0 *ptr = (P0 *) pptr(i);",
653 " switch (ptr->_t) {",
654 " case 0: j = sizeof(P0); break;",
657 static char *R8a[] = {
658 " default: Uerror(\"bad proctype - collapse\");",
660 " if (z) x = z; else x = scratch;",
661 " y = (char *) ptr; k = proc_offset[i];",
663 " for ( ; j > 0; j--, y++)",
664 " if (!Mask[k++]) *x++ = *y;",
666 " for (j = 0; j < WS-1; j++)",
669 " if (z) return (long) (x - z);",
670 " return ordinal(scratch, x-scratch, (short) (2+ptr->_t));",
676 static char *R8b[] = {
677 " default: Uerror(\"bad qtype - collapse\");",
679 " if (z) x = z; else x = scratch;",
680 " y = (char *) ptr; k = q_offset[i];",
682 " /* no need to store the empty slots at the end */",
683 " j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);",
685 " for ( ; j > 0; j--, y++)",
686 " if (!Mask[k++]) *x++ = *y;",
688 " for (j = 0; j < WS-1; j++)",
691 " if (z) return (long) (x - z);",
692 " return ordinal(scratch, x-scratch, 1); /* chan */",
699 static char *R12[] = {
700 "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
706 "{ int _m=0, j; uchar *z;\n",
711 " uerror(\"ref to uninitialized chan (unsend)\");",
713 " j = ((Q0 *)z)->Qlen;",
714 " ((Q0 *)z)->Qlen = --j;",
715 " switch (((Q0 *)qptr(into))->_t) {",
719 " default: Uerror(\"bad queue - unsend\");",
724 "unrecv(int from, int slot, int fld, int fldvar, int strt)",
725 "{ int j; uchar *z;\n",
727 " uerror(\"ref to uninitialized chan (unrecv)\");",
729 " j = ((Q0 *)z)->Qlen;",
730 " if (strt) ((Q0 *)z)->Qlen = j+1;",
731 " switch (((Q0 *)qptr(from))->_t) {",
735 " default: Uerror(\"bad queue - qrecv\");",
740 static char *Proto[] = {
742 "/** function prototypes **/",
743 "char *emalloc(unsigned long);",
744 "char *Malloc(unsigned long);",
745 "int Boundcheck(int, int, int, int, Trans *);",
746 "int addqueue(int, int);",
747 "/* int atoi(char *); */",
748 "/* int abort(void); */",
749 "int close(int);", /* should probably remove this */
752 "int creat(char *, unsigned short);",
753 "int write(int, void *, unsigned);",
756 "int delproc(int, int);",
757 "int endstate(void);",
758 "int hstore(char *, int);",
760 "int gstore(char *, int, uchar);",
762 "int q_cond(short, Trans *);",
766 "int qrecv(int, int, int, int);",
768 "/* void *sbrk(int); */",
769 "void Uerror(char *);",
770 "void assert(int, char *, int, int, Trans *);",
771 "void c_chandump(int);",
772 "void c_globals(void);",
773 "void c_locals(int, int);",
774 "void checkcycles(void);",
775 "void crack(int, int, Trans *, short *);",
776 "void d_hash(uchar *, int);",
777 "void s_hash(uchar *, int);",
778 "void r_hash(uchar *, int);",
780 "void do_reach(void);",
781 "void pan_exit(int);",
784 "void imed(Trans *, int, int, int);",
785 "void new_state(void);",
786 "void p_restor(int);",
787 "void putpeg(int, int);",
788 "void putrail(void);",
789 "void q_restor(void);",
790 "void retrans(int, int, int, short *, uchar *);",
791 "void settable(void);",
792 "void setq_claim(int, int, char *, int, char *);",
793 "void sv_restor(void);",
794 "void sv_save(void);",
795 "void tagtable(int, int, int, short *, uchar *);",
796 "void uerror(char *);",
797 "void unrecv(int, int, int, int, int);",
798 "void usage(FILE *);",
799 "void wrap_stats(void);",
800 "#if defined(FULLSTACK) && defined(BITSTATE)",
801 "int onstack_now(void);",
802 "void onstack_init(void);",
803 "void onstack_put(void);",
804 "void onstack_zap(void);",
807 "int q_S_check(int, int);",
808 "int q_R_check(int, int);",
809 "uchar q_claim[MAXQ+1];",
810 "char *q_name[MAXQ+1];",
811 "char *p_name[MAXPROC+1];",
816 static char *SvMap[] = {
819 "{ char ctd[1024], carg[64];",
821 " strcpy(ctd, \"-DBITSTATE \");",
823 " strcpy(ctd, \"\");",
826 " strcat(ctd, \"-DNOVSZ \");",
829 " sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);",
830 " strcat(ctd, carg);",
833 " sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);",
834 " strcat(ctd, carg);",
838 " strcat(ctd, \"-DNOCLAIM \");",
841 " strcat(ctd, \"-DSAFETY \");",
844 " strcat(ctd, \"-DNOFAIR \");",
848 " { sprintf(carg, \"-DNFAIR=%%d \", NFAIR);",
849 " strcat(ctd, carg);",
855 " strcat(ctd, \"-DNOREDUCE \");",
858 " strcat(ctd, \"-DXUSAFE \");",
862 " strcat(ctd, \"-DNP \");",
865 " strcat(ctd, \"-DPEG \");",
868 " strcat(ctd, \"-DVAR_RANGES \");",
871 " strcat(ctd, \"-DHC0 \");",
874 " strcat(ctd, \"-DHC1 \");",
877 " strcat(ctd, \"-DHC2 \");",
880 " strcat(ctd, \"-DHC3 \");",
883 " strcat(ctd, \"-DHC4 \");",
886 " strcat(ctd, \"-DCHECK \");",
889 " strcat(ctd, \"-DCTL \");",
892 " strcat(ctd, \"-DNIBIS \");",
894 "#ifdef NOBOUNDCHECK",
895 " strcat(ctd, \"-DNOBOUNDCHECK \");",
898 " strcat(ctd, \"-DNOSTUTTER \");",
901 " strcat(ctd, \"-DREACH \");",
904 " strcat(ctd, \"-DPRINTF \");",
907 " strcat(ctd, \"-DOTIM \");",
910 " strcat(ctd, \"-DCOLLAPSE \");",
913 " sprintf(carg, \"-DMA=%%d \", MA);",
914 " strcat(ctd, carg);",
917 " strcat(ctd, \"-DSVDUMP \");",
920 " if (VECTORSZ != 1024)",
921 " { sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);",
922 " strcat(ctd, carg);",
926 " strcat(ctd, \"-DVERBOSE \");",
929 " strcat(ctd, \"-DCHECK \");",
932 " strcat(ctd, \"-DSDUMP \");",
935 " strcat(ctd, \"-DCOVEST \");",
937 " printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);",