1 /***** spin: pangen1.h *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
9 static const char *Code2a[] = { /* the tail of procedure run() */
11 " { if (dodot) exit(0);",
12 " printf(\"\\nTransition Type: \");",
13 " printf(\"A=atomic; D=d_step; L=local; G=global\\n\");",
14 " printf(\"Source-State Labels: \");",
15 " printf(\"p=progress; e=end; a=accept;\\n\");",
17 " printf(\"Note: statement merging was used. Only the first\\n\");",
18 " printf(\" stmnt executed in each merge sequence is shown\\n\");",
19 " printf(\" (use spin -a -o3 to disable statement merging)\\n\");",
23 "#if defined(BFS) && defined(TRIX)", /* before iniglobals */
25 " for (i = 0; i < MAXPROC+1; i++)",
26 " { processes[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
27 " processes[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
29 " for (i = 0; i < MAXQ+1; i++)",
30 " { channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
31 " channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
37 " /* this must be the very first allocation from the shared heap */",
38 " #ifdef BFS_SEP_HASH",
39 " ncomps = (ulong *) emalloc((ulong)((256+2) * sizeof(ulong)));",
41 " ncomps = (ulong *) sh_pre_malloc((ulong)((256+2) * sizeof(ulong)));",
45 " iniglobals(258); /* arg outside range of pids */",
46 "#if defined(VERI) && !defined(NOREDUCE) && !defined(NP) && !defined(BFS) && !defined(HAS_LTL)",
55 " { printf(\"warning: for p.o. reduction to be valid \");",
56 " printf(\"the never claim must be stutter-invariant\\n\");",
57 " printf(\"(never claims generated from LTL \");",
58 " printf(\"formulae are stutter-invariant)\\n\");",
61 " UnBlock; /* disable rendez-vous */",
67 "#if defined(FULLSTACK) && defined(BITSTATE)",
70 "#if defined(CNTRSTACK) && !defined(BFS)",
71 " LL = (uchar *) emalloc(ONE_L<<(ssize-3));",
73 " stack = (_Stack *) emalloc(sizeof(_Stack));",
74 " svtack = (Svtack *) emalloc(sizeof(Svtack));",
75 " /* a place to point for Pptr of non-running procs: */",
76 " noqptr = noptr = (uchar *) emalloc(Maxbody * sizeof(char));",
77 "#if defined(SVDUMP) && defined(VERBOSE)",
79 " (void) write(svfd, (uchar *) &vprefix, sizeof(int));",
82 " Addproc(VERI,1); /* pid = 0, priority 1 */",
84 " if (claimname != NULL)",
85 " { whichclaim = find_claim(claimname);",
86 " select_claim(whichclaim);",
90 " active_procs(); /* started after never */",
92 " now._event = start_event;",
93 " reached[EVENT_TRACE][start_event] = 1;",
104 " if (--Nrun > 0 && HASH_CONST[++HASH_NR])", /* last entry is 0 */
105 " { printf(\"Run %%d:\\n\", HASH_NR);",
108 " if (udmem) /* Dillinger 3/2/09 */",
109 " { memset(SS, 0, udmem);",
111 " { memset(SS, 0, ONE_L<<(ssize-3));",
114 " memset(LL, 0, ONE_L<<(ssize-3));",
117 " memset((uchar *) S_Tab, 0, ",
118 " maxdepth*sizeof(H_el *));",
120 " nstates=nlinks=truncs=truncs2=ngrabs = 0;",
121 " nlost=nShadow=hcmp = 0;",
123 " PUT=PROBE=ZAPS=Ccheck=Cholds = 0;",
128 "#ifdef HAS_PRIORITY",
129 "extern int highest_priority(int, short, Trans *);",
130 "extern int get_priority(int);",
131 "extern int set_priority(int, int);",
135 "spin_malloc(int n) /* reserved for use by Modex generated models */",
136 "{ char *spin_heap_ptr = &(now.spin_heap[now.spin_heap_n]);",
137 " if (now.spin_heap_n + n >= sizeof(now.spin_heap))",
138 " { Uerror(\"spin_heap limit reached\");",
140 " now.spin_heap_n += n;",
141 " return spin_heap_ptr;",
144 "spin_free(void *unused)",
145 "{ unused; /* ignore */",
149 "spin_join(int p, void **unused)",
150 "{ /* fprintf(stderr, \"join %%d when %%d\\n \", p, now._nr_pr); */",
151 " return (now._nr_pr <= p); /* process *p has stopped */",
155 "spin_mutex_free(int *m)",
156 "{ return (*m == 0);",
160 "spin_mutex_lock(int *m)",
165 "spin_mutex_destroy(int *m)",
169 "spin_mutex_unlock(int *m)",
173 "spin_mutex_init(int *m, void *val)",
175 " if (!val)", /* the 2nd arg must be NULL, for now */
178 " { Uerror(\"pthread_mutex_init: unsupported non-default init\");",
183 "spin_cond_wait(int *cond, int *lck)", /*release and re-acquire lock *lck */
184 "{ /* this version does not scale very far alas */",
185 " if (((P0 *)this)->_pid + 1 >= WS*8)", /* 32 or 64 */
186 " { Uerror(\"pid exceeds range supported by pthread_cond_wait\");",
188 " if (((*cond)&1) == 0)", /* repeatedly tested, so: */
189 " { spin_mutex_unlock(lck);", /* avoid double counting */
190 " *cond |= (1<<(((P0 *)this)->_pid + 1));",
191 " return 0;", /* blocked, must test again */
193 " { /* if other processes are already waiting */",
194 " /* while our wait flag is 0, then they should go first */",
195 " if (((*cond)&(~(1 | (1<<(((P0 *)this)->_pid + 1))))) != 0)",
196 " { spin_mutex_unlock(lck);",
197 " return 0;", /* wait for the others to go first */
199 " *cond &= ~1;", /* clear the 'go' bit andy wait flag */
200 " *cond &= ~(1<<(((P0 *)this)->_pid + 1));",
201 " return 1;", /* okay to proceed */
205 "spin_cond_signal(int *cond)",
207 " if ( ((*cond)&(~1)) != 0 )", /* procs are waiting */
208 " { *cond |= 1;", /* set the 'go' bit */
212 "#ifdef HAS_PROVIDED",
213 " int provided(int, uchar, int, Trans *);",
216 " extern void bfs_shutdown(const char *);",
220 " #define GLOBAL_LOCK (0)",
222 " #define CS_N (256*NCORE)", /* must be a power of 2 */
225 " #ifdef NGQ", /* no global queue */
226 " #define NR_QS (NCORE)",
227 " #define CS_NR (CS_N+1) /* 2^N + 1, nr critical sections */",
228 " #define GQ_RD GLOBAL_LOCK", /* not really used in this mode */
229 " #define GQ_WR GLOBAL_LOCK", /* but just in case... */
230 " #define CS_ID (1 + (int) (j1_spin & (CS_N-1))) /* mask: 2^N - 1, zero reserved */",
231 " #define QLOCK(n) (1+n)", /* overlaps first n zones of hashtable */
233 " #define NR_QS (NCORE+1)", /* add a global queue */
234 " #define CS_NR (CS_N+3)", /* 2 extra locks for global q */
235 " #define GQ_RD (1)", /* read access to global q */
236 " #define GQ_WR (2)", /* write access to global q */
237 " #define CS_ID (3 + (int) (j1_spin & (CS_N-1)))",
238 " #define QLOCK(n) (3+n)",/* overlaps first n zones of hashtable */
241 " #ifndef SEP_STATE",
242 " #define enter_critical(w) e_critical(w)",
243 " #define leave_critical(w) x_critical(w)",
246 " #define enter_critical(w) { if (w < 1+NCORE) e_critical(w); }",
247 " #define leave_critical(w) { if (w < 1+NCORE) x_critical(w); }",
249 " #define enter_critical(w) { if (w < 3+NCORE) e_critical(w); }",
250 " #define leave_critical(w) { if (w < 3+NCORE) x_critical(w); }",
255 " cpu_printf(const char *fmt, ...)", /* only used with VERBOSE/CHECK/DEBUG */
257 " enter_critical(GLOBAL_LOCK); /* printing */",
258 " printf(\"cpu%%d: \", core_id);",
260 " va_start(args, fmt);",
261 " vprintf(fmt, args);",
264 " leave_critical(GLOBAL_LOCK);",
268 " #define enter_critical(w) /* none */",
269 " #define leave_critical(w) /* none */",
272 " cpu_printf(const char *fmt, ...)",
274 " va_start(args, fmt);",
275 " vprintf(fmt, args);",
283 "Printf(const char *fmt, ...)",
284 "{ /* Make sure the args to Printf",
285 " * are always evaluated (e.g., they",
286 " * could contain a run stmnt)",
287 " * but do not generate the output",
288 " * during verification runs",
289 " * unless explicitly wanted",
290 " * If this fails on your system",
291 " * compile SPIN itself -DPRINTF",
292 " * and this code is not generated",
297 " va_start(args, fmt);",
298 " vprintf(fmt, args);",
305 " va_start(args, fmt);",
306 " vprintf(fmt, args);",
312 "extern void printm(int);",
315 "#define getframe(i) &trail[i];",
317 "static long HHH, DDD, hiwater;",
318 "static long CNT1, CNT2;",
319 "static int stackwrite;",
320 "static int stackread;",
321 "static Trail frameptr;",
325 " if (CNT1 == CNT2)",
326 " return &trail[d];",
328 " if (d >= (CNT1-CNT2)*DDD)",
329 " return &trail[d - (CNT1-CNT2)*DDD];",
332 " && (stackread = open(stackfile, 0)) < 0)",
333 " { printf(\"getframe: cannot open %%s\\n\", stackfile);",
336 " if (lseek(stackread, d* (off_t) sizeof(Trail), SEEK_SET) == -1",
337 " || read(stackread, &frameptr, sizeof(Trail)) != sizeof(Trail))",
338 " { printf(\"getframe: frame read error\\n\");",
341 " return &frameptr;",
345 "extern void cleanup_shm(int);",
346 "volatile uint *search_terminated; /* to signal early termination */",
348 * Meaning of bitflags in search_terminated:
352 * 8 set by sudden_stop -- called after someone_crashed and [Uu]error
353 * 16 set by cleanup_shm
354 * 32 set by give_up -- called on signal
355 * 64 set by proxy_exit
356 * 128 set by proxy on write port failure
357 * 256 set by proxy on someone_crashed
359 * Flags 8|32|128|256 indicate abnormal termination
361 * The flags are checked in 4 functions in the code:
363 * someone_crashed() (proxy and pan version)
369 "{ void stop_timer(int);",
371 " extern void bfs_mark_done(int);",
372 " extern void bfs_drop_shared_memory(void);",
375 " { printf(\"--end of output--\\n\");",
378 " if (search_terminated != NULL)",
379 " { *search_terminated |= 1; /* pan_exit */",
382 " { void dsk_stats(void);",
386 " if (!state_tables && !readtrail)",
387 " { cleanup_shm(1);",
391 " if (who_am_i != 0)",
392 " { bfs_mark_done(3); /* stopped */",
394 " bfs_drop_shared_memory();",
400 " if (who_am_i == 0)",
405 " C_EXIT; /* trust that it defines a fct */",
410 "static char tbuf[2][2048];",
413 "transmognify(char *s)",
415 " int i, toggle = 0;",
416 " if (!s || strlen(s) > 2047) return s;",
417 " memset(tbuf[0], 0, 2048);",
418 " memset(tbuf[1], 0, 2048);",
419 " strcpy(tbuf[toggle], s);",
420 " while ((v = strstr(tbuf[toggle], \"{c_code\")))", /* assign v */
421 " { *v = '\\0'; v++;",
422 " strcpy(tbuf[1-toggle], tbuf[toggle]);",
423 " for (w = v; *w != '}' && *w != '\\0'; w++) /* skip */;",
424 " if (*w != '}') return s;",
426 " for (i = 0; code_lookup[i].c; i++)",
427 " if (strcmp(v, code_lookup[i].c) == 0",
428 " && strlen(v) == strlen(code_lookup[i].c))",
429 " { if (strlen(tbuf[1-toggle])",
430 " + strlen(code_lookup[i].t)",
431 " + strlen(w) > 2047)",
433 " strcat(tbuf[1-toggle], code_lookup[i].t);",
436 " strcat(tbuf[1-toggle], w);",
437 " toggle = 1 - toggle;",
439 " tbuf[toggle][2047] = '\\0';",
440 " return tbuf[toggle];",
443 "char * transmognify(char *s) { return s; }",
448 "add_src_txt(int ot, int tt)",
452 " for (t = trans[ot][tt]; t; t = t->nxt)",
453 " { printf(\"\\t\\t\");",
454 " q = transmognify(t->tp);",
455 " for ( ; q && *q; q++)",
457 " printf(\"\\\\n\");",
465 "find_source(int tp, int s)",
467 " if (s >= flref[tp]->from",
468 " && s <= flref[tp]->upto)",
469 " { return flref[tp]->fnm;",
471 " return PanSource; /* i.e., don't know */",
476 "{ static int wrap_in_progress = 0;",
480 " if (wrap_in_progress++) return;",
482 " printf(\"spin: trail ends after %%ld steps\\n\", depth);",
483 " if (onlyproc >= 0)",
484 " { if (onlyproc >= now._nr_pr) { pan_exit(0); }",
486 " z = (P0 *)pptr(II);",
487 " printf(\"%%3ld:\tproc %%d (%%s) \",",
488 " depth, II, procname[z->_t]);",
489 " for (i = 0; src_all[i].src; i++)",
490 " if (src_all[i].tp == (int) z->_t)",
491 " { printf(\" %%s:%%d\",",
492 " find_source((int) z->_t, (int) z->_p),",
493 " src_all[i].src[z->_p]);",
496 " printf(\" (state %%2d)\", z->_p);",
497 " if (!stopstate[z->_t][z->_p])",
498 " printf(\" (invalid end state)\");",
500 " add_src_txt(z->_t, z->_p);",
503 " printf(\"#processes %%d:\\n\", now._nr_pr);",
504 " if (depth < 0) depth = 0;",
505 " for (II = 0; II < now._nr_pr; II++)",
506 " { z = (P0 *)pptr(II);",
507 " printf(\"%%3ld:\tproc %%d (%%s) \",",
508 " depth, II, procname[z->_t]);",
509 " for (i = 0; src_all[i].src; i++)",
510 " if (src_all[i].tp == (int) z->_t)",
511 " { printf(\" %%s:%%d\",",
512 " find_source((int) z->_t, (int) z->_p),",
513 " src_all[i].src[z->_p]);",
516 " printf(\" (state %%2d)\", z->_p);",
517 " if (!stopstate[z->_t][z->_p])",
518 " printf(\" (invalid end state)\");",
520 " add_src_txt(z->_t, z->_p);",
523 " for (II = 0; II < now._nr_pr; II++)",
524 " { z = (P0 *)pptr(II);",
525 " c_locals(II, z->_t);",
535 " char fnm[512], *q;",
536 " char MyFile[512];", /* avoid using a non-writable string */
537 " char MySuffix[16];",
539 " int candidate_files;",
541 " if (trailfilename != NULL)",
542 " { fd = fopen(trailfilename, \"r\");",
544 " { printf(\"pan: cannot find %%s\\n\", trailfilename);",
551 " candidate_files = 0;",
552 " tprefix = \"trail\";",
553 " strcpy(MyFile, TrailFile);",
554 " do { /* see if there's more than one possible trailfile */",
556 " { sprintf(fnm, \"%%s%%d.%%s\",",
557 " MyFile, whichtrail, tprefix);",
558 " fd = fopen(fnm, \"r\");",
560 " { candidate_files++;",
561 " if (verbose==100)",
562 " printf(\"trail%%d: %%s\\n\",",
563 " candidate_files, fnm);",
566 " if ((q = strchr(MyFile, \'.\')) != NULL)",
567 " { *q = \'\\0\';", /* e.g., strip .pml */
568 " sprintf(fnm, \"%%s%%d.%%s\",",
569 " MyFile, whichtrail, tprefix);",
571 " fd = fopen(fnm, \"r\");",
573 " { candidate_files++;",
574 " if (verbose==100)",
575 " printf(\"trail%%d: %%s\\n\",",
576 " candidate_files, fnm);",
580 " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
581 " fd = fopen(fnm, \"r\");",
583 " { candidate_files++;",
584 " if (verbose==100)",
585 " printf(\"trail%%d: %%s\\n\",",
586 " candidate_files, fnm);",
589 " if ((q = strchr(MyFile, \'.\')) != NULL)",
590 " { *q = \'\\0\';", /* e.g., strip .pml */
591 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
593 " fd = fopen(fnm, \"r\");",
595 " { candidate_files++;",
596 " if (verbose==100)",
597 " printf(\"trail%%d: %%s\\n\",",
598 " candidate_files, fnm);",
601 " tprefix = MySuffix;",
602 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
603 " } while (try_core <= NCORE);",
605 " if (candidate_files != 1)",
606 " { if (verbose != 100)",
607 " { printf(\"error: there are %%d trail files:\\n\",",
608 " candidate_files);",
612 " { printf(\"pan: rm or mv all except one\\n\");",
617 " strcpy(MyFile, TrailFile); /* restore */",
618 " tprefix = \"trail\";",
621 " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);",
622 " fd = fopen(fnm, \"r\");",
623 " if (fd == NULL && (q = strchr(MyFile, \'.\')))",
624 " { *q = \'\\0\';", /* e.g., strip .pml on original file */
625 " sprintf(fnm, \"%%s%%d.%%s\",",
626 " MyFile, whichtrail, tprefix);",
628 " fd = fopen(fnm, \"r\");",
631 " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
632 " fd = fopen(fnm, \"r\");",
633 " if (fd == NULL && (q = strchr(MyFile, \'.\')))",
634 " { *q = \'\\0\';", /* e.g., strip .pml on original file */
635 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
637 " fd = fopen(fnm, \"r\");",
640 " { if (try_core < NCORE)",
641 " { tprefix = MySuffix;",
642 " sprintf(tprefix, \"cpu%%d_trail\", try_core++);",
645 " printf(\"pan: cannot find trailfile %%s\\n\", fnm);",
649 "#if NCORE>1 && defined(SEP_STATE)",
650 " { void set_root(void); /* for partial traces from local root */",
657 "uchar do_transit(Trans *, short);",
659 "void set_permuted(int);",
660 "void set_reversed(int);",
661 "void set_rotated(int);",
662 "void set_randrot(int);",
663 "void (*p_reorder)(int) = set_permuted;",
671 " int i, t_id, lastnever = -1; short II;",
676 " memset(sbuf, 0, sizeof(sbuf));",
678 " fd = findtrail(); /* exits if unsuccessful */",
679 " while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)",
680 " { if (depth == -1)",
681 " { printf(\"<<<<<START OF CYCLE>>>>>\\n\");",
685 " { switch (depth) {",
687 " if (i && !t_reverse)",
688 " { strcat(sbuf, \"-t_reverse \");",
692 " if (i && p_reorder != set_permuted)",
693 " { strcat(sbuf, \"-p_permute \");",
695 " if (t_id && p_reorder != set_reversed)",
696 " { strcat(sbuf, \"-p_reverse \");",
701 " && (p_reorder != set_rotated || p_rotate != t_id))",
703 " sprintf(tmp, \"-p_rotate%%d \", t_id);",
704 " strcat(sbuf, tmp);",
708 " if (i && p_reorder != set_randrot)",
709 " { strcat(sbuf, \"-p_randrot \");",
711 " if (s_rand != ++t_id)",
713 " sprintf(tmp, \"-RS%%u \", (uint) t_id-1);",
714 " strcat(sbuf, tmp);",
726 " if (strlen(sbuf) > 0)",
727 " { fprintf(efd, \"add: %%s\\n\", sbuf);",
731 " if (i > now._nr_pr)",
732 " { printf(\"pan: Error, proc %%d invalid pid \", i);",
733 " printf(\"transition %%d\\n\", t_id);",
737 " z = (P0 *)pptr(II);",
738 " for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
739 " if (t->t_id == (T_ID) t_id)",
742 " { for (i = 0; i < NrStates[z->_t]; i++)",
743 " { t = trans[z->_t][i];",
744 " if (t && t->t_id == (T_ID) t_id)",
745 " { printf(\"\\tRecovered at state %%d\\n\", i);",
749 " printf(\"pan: Error, proc %%d type %%d state %%d: \",",
750 " II, z->_t, z->_p);",
751 " printf(\"transition %%d not found\\n\", t_id);",
752 " printf(\"pan: list of possible transitions in this process:\\n\");",
753 " if (z->_t >= 0 && z->_t <= _NP_)",
754 " for (t = trans[z->_t][z->_p]; t; t = t->nxt)",
755 " printf(\" t_id %%d -- case %%d, [%%s]\\n\",",
756 " t->t_id, t->forw, t->tp);",
757 " break; /* pan_exit(1); */",
760 " q = transmognify(t->tp);",
761 " if (gui) simvals[0] = \'\\0\';",
763 " pnm = procname[z->_t];",
765 " trpt->tau |= 1;", /* timeout always possible */
766 " if (!do_transit(t, II))",
767 " { if (onlyproc >= 0 && II != onlyproc)",
769 " if (!verbose) break;",
770 " printf(\"pan: error, next transition UNEXECUTABLE on replay\\n\");",
771 " printf(\" most likely causes: missing c_track statements\\n\");",
772 " printf(\" or illegal side-effects in c_expr statements\\n\");",
775 " if (onlyproc >= 0 && II != onlyproc)",
779 " { printf(\"%%3ld: proc %%2d (%%s) \", depth, II, pnm);",
781 " for (i = 0; src_all[i].src; i++)",
782 " if (src_all[i].tp == (int) z->_t)",
783 " { printf(\" %%s:%%d \",",
784 " find_source((int) z->_t, (int) z->_p),",
785 " src_all[i].src[z->_p]);",
789 " printf(\"(state %%d) trans {%%d,%%d} [%%s]\\n\",",
790 " z->_p, t_id, t->forw, q?q:\"\");",
793 " for (i = 0; i < now._nr_pr; i++)",
794 " { c_locals(i, ((P0 *)pptr(i))->_t);",
796 " } else if (Btypes[z->_t] == N_CLAIM)",
797 " { if (lastnever != (int) z->_p)",
798 " { for (i = 0; src_all[i].src; i++)",
799 " if (src_all[i].tp == (int) z->_t)",
800 " { printf(\"MSC: ~G %%d\\n\",",
801 " src_all[i].src[z->_p]);",
804 " if (!src_all[i].src)",
805 " printf(\"MSC: ~R %%d\\n\", z->_p);",
807 " lastnever = z->_p;",
809 " } else if (Btypes[z->_t] != 0) /* not :np_: */",
811 "sameas: if (no_rck) goto moveon;",
813 " { printf(\"%%ld: \", depth);",
814 " for (i = 0; i < II; i++)",
815 " printf(\"\\t\\t\");",
816 " printf(\"%%s(%%d):\", pnm, II);",
817 " printf(\"[%%s]\\n\", q?q:\"\");",
818 " } else if (!silent)",
819 " { if (strlen(simvals) > 0) {",
820 " printf(\"%%3ld: proc %%2d (%%s)\", ",
822 " for (i = 0; src_all[i].src; i++)",
823 " if (src_all[i].tp == (int) z->_t)",
824 " { printf(\" %%s:%%d \",",
825 " find_source((int) z->_t, (int) z->_p),",
826 " src_all[i].src[z->_p]);",
829 " printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);",
831 " printf(\"%%3ld: proc %%2d (%%s)\", ",
833 " for (i = 0; src_all[i].src; i++)",
834 " if (src_all[i].tp == (int) z->_t)",
835 " { printf(\" %%s:%%d \",",
836 " find_source((int) z->_t, (int) z->_p),",
837 " src_all[i].src[z->_p]);",
840 " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");",
841 " /* printf(\"\\n\"); */",
843 "moveon: z->_p = t->st;",
852 " for (i = 0; i < now._nr_pr; i++)",
853 " { z = (P0 *)pptr(i);",
854 " if (z->_t == (unsigned) pt)",
855 " return BASE+z->_pid;",
860 "#if NCORE>1 && !defined(GLOB_HEAP)",
861 " #define SEP_HEAP /* version 5.1.2 */",
866 "bstore_mod(char *v, int n) /* hasharray size not a power of two */",
869 "#if defined(MURMUR) && (WS==8)",
870 " m_hash((uchar *) v, n); /* bstore_mod - sets j3_spin, j4_spin, K1, K2 */",
872 " d_hash((uchar *) v, n); /* bstore_mod - sets j3_spin, j4_spin, K1, K2 */",
874 " x = K1; y = j3_spin;", /* was K2 before 5.1.1 */
876 " { if (!(SS[x%%udmem]&(1<<y))) break;", /* take the hit in speed */
879 " printf(\"Old bitstate\\n\");",
883 " x = (x + K2 + i);", /* no mask, using mod - was K1 before 5.1.1 */
884 " y = (y + j4_spin) & 7;",
888 " if (rand()%%100 > RANDSTOR) return 0;",
891 " { SS[x%%udmem] |= (1<<y);",
892 " if (i == hfns) break;", /* done */
893 " x = (x + K2 + i);", /* no mask - was K1 before 5.1.1 */
894 " y = (y + j4_spin) & 7;",
898 " printf(\"New bitstate\\n\");",
906 "bstore_reg(char *v, int n) /* extended hashing, Peter Dillinger, 2004 */",
909 "#if defined(MURMUR) && (WS==8)",
910 " m_hash((uchar *) v, n); /* bstore_reg - sets j1_spin-j4_spin */",
912 " d_hash((uchar *) v, n); /* bstore_reg - sets j1_spin-j4_spin */",
914 " x = j2_spin; y = j3_spin;",
916 " { if (!(SS[x]&(1<<y))) break;", /* at least one bit not set */
919 " printf(\"Old bitstate\\n\");",
923 " x = (x + j1_spin + i) & nmask;",
924 " y = (y + j4_spin) & 7;",
928 " if (rand()%%100 > RANDSTOR) return 0;",
931 " { SS[x] |= (1<<y);",
932 " if (i == hfns) break;", /* done */
933 " x = (x + j1_spin + i) & nmask;",
934 " y = (y + j4_spin) & 7;",
938 " printf(\"New bitstate\\n\");",
945 "#endif", /* BITSTATE */
946 "ulong TMODE = 0666; /* file permission bits for trail files */",
949 "char snap[64], fnm[512];",
955 " char MyFile[512];",
956 " int w_flags = O_CREAT|O_WRONLY|O_TRUNC;",
958 " if (exclusive == 1 && iterative == 0)",
959 " { w_flags |= O_EXCL;",
962 " q = strrchr(TrailFile, \'/\');",
963 " if (q == NULL) q = TrailFile; else q++;",
964 " strcpy(MyFile, q); /* TrailFile is not a writable string */",
966 " if (iterative == 0 && Nr_Trails++ > 0)",
969 " sprintf(fnm, \"%%s_%%s_%%d_%%d.%%s\",",
970 " MyFile, progname, getpid(), Nr_Trails-1, tprefix);",
972 " sprintf(fnm, \"%%s%%d.%%s\",",
973 " MyFile, Nr_Trails-1, tprefix);",
978 " sprintf(fnm, \"%%s_%%s_%%d.%%s\", MyFile, progname, getpid(), tprefix);",
980 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
983 " if ((fd = open(fnm, w_flags, TMODE)) < 0)",
984 " { if ((q = strchr(MyFile, \'.\')))",
985 " { *q = \'\\0\';", /* strip .pml */
986 " if (iterative == 0 && Nr_Trails-1 > 0)",
987 " sprintf(fnm, \"%%s%%d.%%s\",",
988 " MyFile, Nr_Trails-1, tprefix);",
990 " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);",
992 " fd = open(fnm, w_flags, TMODE);",
995 " { printf(\"pan: cannot create %%s\\n\", fnm);",
996 " perror(\"cause\");",
999 "#if NCORE>1 && (defined(SEP_STATE) || !defined(FULL_TRAIL))",
1000 " void write_root(void); ",
1003 " printf(\"pan: wrote %%s\\n\", fnm);",
1010 "#define FREQ (1000000)",
1012 "double freq = (double) FREQ;\n",
1015 "void sv_populate(void);",
1018 "re_populate(void) /* restore procs and chans from now._ids_ */",
1019 "{ int i, cnt = 0;",
1022 " printf(\"%%4d: re_populate\\n\", depth);",
1024 " for (i = 0; i < now._nr_pr; i++, cnt++)",
1025 " { b = now._ids_[cnt];",
1026 " processes[i]->psize = what_p_size( ((P0 *)b)->_t );",
1027 " memcpy(processes[i]->body, b, processes[i]->psize);",
1029 " ((P0 *)pptr(i))->_pid = i;",
1030 " if (BASE > 0 && h > 0)",
1031 " { ((P0 *)pptr(i))->_pid -= BASE;",
1035 " processes[i]->modified = 1; /* re-populate */",
1038 " for (i = 0; i < now._nr_qs; i++, cnt++)",
1039 " { b = now._ids_[cnt];",
1040 " channels[i]->psize = what_q_size( ((Q0 *)b)->_t );",
1041 " memcpy(channels[i]->body, b, channels[i]->psize);",
1043 " channels[i]->modified = 1; /* re-populate */",
1049 "#ifdef BFS", /* breadth-first search */
1051 " BFS_State *bfs_trail, *bfs_bot, *bfs_free;",
1052 " SV_Hold *svfree;",
1054 " static ulong bfs_pre_allocated;",
1057 " #ifndef BFS_LIMIT",
1058 " #define BFS_LIMIT 100000",
1060 " #ifndef BFS_DSK_LIMIT",
1061 " #define BFS_DSK_LIMIT 1000000",
1063 " #if defined(WIN32) || defined(WIN64)",
1064 " #define RFLAGS (O_RDONLY|O_BINARY)",
1065 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC|O_BINARY)",
1066 " #define RWFLAGS (O_RDWR|O_BINARY)",
1068 " #define RFLAGS (O_RDONLY)",
1069 " #define WFLAGS (O_CREAT|O_WRONLY|O_TRUNC)",
1070 " #define RWFLAGS (O_RDWR)",
1073 " long bfs_size_limit;",
1074 " int bfs_dsk_write = -1;",
1075 " int bfs_dsk_read = -1;",
1076 " long bfs_dsk_writes, bfs_dsk_reads;",
1077 " int bfs_dsk_seqno_w, bfs_dsk_seqno_r;",
1080 "uchar do_reverse(Trans *, short, uchar);",
1081 "void snapshot(void);",
1084 "select_claim(int x) /* ignored in BFS mode */",
1086 " { printf(\"select %%d (ignored)\\n\", x);",
1097 " if (svfree && n <= svfree->sz)",
1099 " svfree = h->nxt;",
1100 " h->nxt = (SV_Hold *) 0;",
1102 " { h = (SV_Hold *) emalloc(sizeof(SV_Hold));",
1105 " if (bfs_size_limit >= BFS_LIMIT)",
1106 " { h->sv = (State *) 0; /* means: read disk */",
1107 " bfs_dsk_writes++; /* count */",
1108 " if (bfs_dsk_write < 0 /* file descriptor */",
1109 " || bfs_dsk_writes%%BFS_DSK_LIMIT == 0)",
1110 " { char dsk_nm[32];",
1111 " if (bfs_dsk_write >= 0)",
1112 " { (void) close(bfs_dsk_write);",
1114 " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_w++);",
1115 " bfs_dsk_write = open(dsk_nm, WFLAGS, 0644);",
1116 " if (bfs_dsk_write < 0)",
1117 " { Uerror(\"could not create tmp disk file\");",
1119 " printf(\"pan: created disk file %%s\\n\", dsk_nm);",
1121 " if (write(bfs_dsk_write, (char *) &now, n) != n)",
1122 " { Uerror(\"aborting -- disk write failed (disk full?)\");",
1124 " return h; /* no memcpy */",
1126 " bfs_size_limit++;",
1128 " h->sv = (State *) emalloc(sizeof(State) - VECTORSZ + n);",
1131 " memcpy((char *)h->sv, (char *)&now, n);",
1136 "getsv_mask(int n)",
1138 " static EV_Hold *kept = (EV_Hold *) 0;",
1140 " for (h = kept; h; h = h->nxt)",
1142 "#if !defined(NOCOMP) && !defined(HC)",
1143 " && (memcmp((char *) Mask, (char *) h->sv, n) == 0)",
1145 " && (now._nr_pr == h->nrpr)",
1146 " && (now._nr_qs == h->nrqs)",
1150 " #if VECTORSZ>32000",
1151 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
1152 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
1154 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
1155 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
1157 " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
1158 " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
1162 " { h = (EV_Hold *) emalloc(sizeof(EV_Hold));",
1164 " h->nrpr = now._nr_pr;",
1165 " h->nrqs = now._nr_qs;",
1167 " h->sv = (char *) emalloc(n * sizeof(char));",
1168 "#if !defined(NOCOMP) && !defined(HC)",
1169 " memcpy((char *) h->sv, (char *) Mask, n);",
1172 " if (now._nr_pr > 0)",
1173 " { h->ps = (char *) emalloc(now._nr_pr * sizeof(int));",
1174 " memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(uchar));",
1175 " #if VECTORSZ>32000",
1176 " h->po = (char *) emalloc(now._nr_pr * sizeof(int));",
1177 " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));",
1179 " h->po = (char *) emalloc(now._nr_pr * sizeof(short));",
1180 " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));",
1183 " if (now._nr_qs > 0)",
1184 " { h->qs = (char *) emalloc(now._nr_qs * sizeof(int));",
1185 " memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(uchar));",
1186 " #if VECTORSZ>32000",
1187 " h->qo = (char *) emalloc(now._nr_qs * sizeof(int));",
1188 " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));",
1190 " h->qo = (char *) emalloc(now._nr_qs * sizeof(short));",
1191 " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));",
1202 "freesv(SV_Hold *p)",
1203 "{ SV_Hold *h, *oh;",
1205 " oh = (SV_Hold *) 0;",
1206 " for (h = svfree; h; oh = h, h = h->nxt)",
1207 " { if (p->sz >= h->sz)",
1211 " { p->nxt = svfree;",
1220 "get_bfs_frame(void)",
1225 " bfs_free = bfs_free->nxt;",
1226 " t->nxt = (BFS_State *) 0;",
1228 " { t = (BFS_State *) emalloc(sizeof(BFS_State));",
1230 " t->frame = (Trail *) emalloc(sizeof(Trail));", /* always new */
1231 " /* new because we keep a ptr to the frame of parent states */",
1232 " /* used for reconstructing path and recovering failed rvs etc */",
1237 "push_bfs(Trail *f, int d)",
1240 " t = get_bfs_frame();",
1241 " memcpy((char *)t->frame, (char *)f, sizeof(Trail));",
1242 " t->frame->o_tt = d; /* depth */",
1248 " t->onow = getsv(vsize);",
1249 " t->omask = getsv_mask(vsize);",
1250 " #if defined(FULLSTACK) && defined(Q_PROVISO)",
1251 " t->lstate = Lstate; /* bfs */",
1254 " { bfs_bot = bfs_trail = t;",
1256 " { bfs_bot->nxt = t;",
1260 " t->nr = nstates;",
1264 " printf(\"PUSH %%lu (depth %%d, nr %%lu)\\n\", (ulong) t->frame, d, t->nr);",
1266 " printf(\"PUSH %%lu (depth %%d)\\n\", (ulong) t->frame, d);",
1276 " { return (Trail *) 0;",
1279 " bfs_trail = t->nxt;",
1281 " { bfs_bot = (BFS_State *) 0;",
1283 " #if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
1284 " if (t->lstate) /* bfs */",
1285 " { t->lstate->tagged = 0; /* bfs */",
1288 " t->nxt = bfs_free;",
1291 " vsize = t->onow->sz;",
1294 " if (t->onow->sv == (State *) 0)",
1295 " { char dsk_nm[32];",
1296 " bfs_dsk_reads++; /* count */",
1297 " if (bfs_dsk_read >= 0 /* file descriptor */",
1298 " && bfs_dsk_reads%%BFS_DSK_LIMIT == 0)",
1299 " { (void) close(bfs_dsk_read);",
1300 " sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r-1);",
1301 " (void) unlink(dsk_nm);",
1302 " bfs_dsk_read = -1;",
1304 " if (bfs_dsk_read < 0)",
1305 " { sprintf(dsk_nm, \"pan_bfs_%%d.tmp\", bfs_dsk_seqno_r++);",
1306 " bfs_dsk_read = open(dsk_nm, RFLAGS);",
1307 " if (bfs_dsk_read < 0)",
1308 " { Uerror(\"could not open temp disk file\");",
1310 " if (read(bfs_dsk_read, (char *) &now, vsize) != vsize)",
1311 " { Uerror(\"bad bfs disk file read\");",
1314 " if (now._vsz != vsize)",
1315 " { Uerror(\"disk read vsz mismatch\");",
1320 " { memcpy((uchar *) &now, (uchar *) t->onow->sv, vsize);",
1322 " vsize = now._vsz;",
1325 "#if !defined(NOCOMP) && !defined(HC)",
1326 " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);",
1331 " if (now._nr_pr > 0)",
1332 " #if VECTORSZ>32000",
1333 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));",
1335 " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));",
1337 " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));",
1339 " if (now._nr_qs > 0)",
1340 " #if VECTORSZ>32000",
1341 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));",
1343 " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));",
1345 " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));",
1349 " if (t->onow->sv != (State *) 0)",
1351 " { freesv(t->onow); /* omask not freed */",
1355 " printf(\"POP %%lu (depth %%d, nr %%lu)\\n\", (ulong) t->frame, t->frame->o_tt, t->nr);",
1357 " printf(\"POP %%lu (depth %%d)\\n\", (ulong) t->frame, t->frame->o_tt);",
1360 " return t->frame;",
1364 "store_state(Trail *ntrpt, int shortcut, short oboq)",
1367 " Trans *t2 = (Trans *) 0;",
1368 " uchar ot; int tt, E_state;",
1369 " uchar o_opm = trpt->o_pm, *othis = this;",
1374 " printf(\"claim: shortcut\\n\");",
1376 " goto store_it; /* no claim move */",
1379 " this = pptr(0); /* 0 = never claim */",
1380 " trpt->o_pm = 0;", /* to interpret else in never claim */
1382 " tt = (int) ((P0 *)this)->_p;",
1383 " ot = (uchar) ((P0 *)this)->_t;",
1385 " #ifdef HAS_UNLESS",
1388 " for (t2 = trans[ot][tt]; t2; t2 = t2?t2->nxt:(Trans *)0)",
1390 " #ifdef HAS_UNLESS",
1391 " if (E_state > 0 && E_state != t2->e_trans)",
1395 " if (do_transit(t2, 0))",
1398 " if (!reached[ot][t2->st])",
1399 " printf(\"depth: %%d -- claim move from %%d -> %%d\\n\",",
1400 " trpt->o_tt, ((P0 *)this)->_p, t2->st);",
1402 " #ifdef HAS_UNLESS",
1403 " E_state = t2->e_trans;",
1406 " { ((P0 *)this)->_p = t2->st;",
1407 " reached[ot][t2->st] = 1;",
1409 " if (stopstate[ot][t2->st])",
1410 " { uerror(\"end state in claim reached\");",
1414 " if (now._nr_pr == 0) /* claim terminated */",
1415 " uerror(\"end state in claim reached\");",
1418 " peg[t2->forw]++;",
1420 " trpt->o_pm |= 1;",
1422 " { Uerror(\"atomic in claim not supported in BFS\");",
1426 " #endif", /* VERI */
1428 " #if defined(BITSTATE)",
1429 " if (!b_store((char *)&now, vsize))",
1430 " #elif defined(MA)",
1431 " if (!g_store((char *)&now, vsize, 0))",
1433 " if (!h_store((char *)&now, vsize))",
1435 " { static long sdone = (long) 0; long ndone;",
1437 " #ifndef NOREDUCE",
1438 " trpt->tau |= 64;", /* bfs: succ definitely outside stack */
1440 " ndone = (ulong) (nstates/(freq));",
1441 " if (ndone != sdone && mreached%%10 != 0)",
1444 " #if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
1445 " if (nstates > ((double)(1<<(ssize+1))))",
1446 " { void resize_hashtable(void);",
1447 " resize_hashtable();",
1454 " else if (oboq != -1)",
1456 " x = (Trail *) trpt->ostate; /* pre-rv state */",
1457 " if (x) x->o_pm |= 4; /* mark success */",
1460 " push_bfs(ntrpt, trpt->o_tt+1);",
1464 " #if defined(Q_PROVISO) && !defined(NOREDUCE) && defined(FULLSTACK)",
1465 " #if !defined(BITSTATE)",
1466 " if (Lstate && Lstate->tagged)",
1467 " { trpt->tau |= 64;",
1470 " if (trpt->tau&32)",
1471 " { BFS_State *tprov;",
1472 " for (tprov = bfs_trail; tprov; tprov = tprov->nxt)",
1473 " if (tprov->onow->sv != (State *) 0",
1474 " && memcmp((uchar *)&now, (uchar *)tprov->onow->sv, vsize) == 0)",
1475 " { trpt->tau |= 64;",
1476 " break; /* state is in queue */",
1482 " ((P0 *)this)->_p = tt; /* reset claim */",
1484 " do_reverse(t2, 0, 0);",
1489 " trpt->o_pm = o_opm;",
1495 "{ Trans *t; Trail *otrpt, *x;",
1496 " uchar _n, _m, ot, nps = 0;",
1497 " int tt, E_state;",
1498 " short II, From = (short) (now._nr_pr-1), To = BASE;",
1499 " short oboq = boq;",
1501 " ntrpt = (Trail *) emalloc(sizeof(Trail));",
1502 " trpt->ostate = (H_el *) 0;",
1505 " trpt->o_tt = -1;",
1506 " store_state(ntrpt, 0, oboq); /* initial state */",
1508 " while ((otrpt = pop_bfs())) /* also restores now */",
1509 " { memcpy((char *) trpt, (char *) otrpt, sizeof(Trail));",
1510 " #if defined(C_States) && (HAS_TRACK==1)",
1511 " c_revert((uchar *) &(now.c_state[0]));",
1513 " if (trpt->o_pm & 4)",
1516 " printf(\"Revisit of atomic not needed (%%d)\\n\",",
1517 " trpt->o_pm);", /* at least 1 rv succeeded */
1521 " #ifndef NOREDUCE",
1524 " if (trpt->o_pm == 8)",
1526 " if (trpt->tau&8)",
1529 " printf(\"Break atomic (pm:%%d,tau:%%d)\\n\",",
1530 " trpt->o_pm, trpt->tau);",
1532 " trpt->tau &= ~8;",
1534 " #ifndef NOREDUCE",
1535 " else if (trpt->tau&32)", /* was a preselected move */
1538 " printf(\"Void preselection (pm:%%d,tau:%%d)\\n\",",
1539 " trpt->o_pm, trpt->tau);",
1541 " trpt->tau &= ~32;",
1542 " nps = 1; /* no preselection in repeat */",
1546 " trpt->o_pm &= ~(4|8);",
1547 " if (trpt->o_tt > mreached)",
1548 " { mreached = trpt->o_tt;",
1549 " if (mreached%%10 == 0)",
1552 " depth = trpt->o_tt;",
1554 " if (depth >= maxdepth)",
1559 " { x = (Trail *) trpt->ostate;",
1560 " if (x) x->o_pm |= 4; /* not failing */",
1566 " printf(\"error: max search depth too small\\n\");",
1569 " { uerror(\"depth limit reached\");",
1573 " #ifndef NOREDUCE",
1574 " if (boq == -1 && !(trpt->tau&8) && nps == 0)",
1575 " for (II = now._nr_pr-1; II >= BASE; II -= 1)",
1577 "Pickup: this = pptr(II);",
1578 " tt = (int) ((P0 *)this)->_p;",
1579 " ot = (uchar) ((P0 *)this)->_t;",
1580 " if (trans[ot][tt]->atom & 8)", /* safe */
1581 " { t = trans[ot][tt];",
1582 " if (t->qu[0] != 0)",
1584 " if (!q_cond(II, t))",
1589 " trpt->tau |= 32; /* preselect marker */",
1591 " printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
1592 " depth, II, trpt->tau);",
1596 " trpt->tau &= ~32;", /* not preselected */
1597 " #endif", /* if !NOREDUCE */
1599 " if (trpt->tau&8) /* atomic */",
1600 " { From = To = (short ) trpt->pr;",
1603 " { From = now._nr_pr-1;",
1608 " for (II = From; II >= To; II -= 1)",
1610 " this = pptr(II);",
1611 " tt = (int) ((P0 *)this)->_p;",
1612 " ot = (uchar) ((P0 *)this)->_t;",
1614 " /* no rendezvous with same proc */",
1615 " if (boq != -1 && trpt->pr == II)",
1619 " ntrpt->pr = (uchar) II;",
1620 " ntrpt->st = tt; ",
1621 " trpt->o_pm &= ~1; /* no move yet */",
1622 " #ifdef EVENT_TRACE",
1623 " trpt->o_event = now._event;",
1626 " #ifdef HAS_PRIORITY",
1627 " if (!highest_priority(((P0 *)this)->_pid, II, t))",
1631 " #ifdef HAS_PROVIDED",
1632 " if (!provided(II, ot, tt, t))",
1638 " #ifdef HAS_UNLESS",
1641 " for (t = trans[ot][tt]; t; t = t->nxt)",
1643 " #ifdef HAS_UNLESS",
1645 " && E_state != t->e_trans)",
1652 " if (!(_m = do_transit(t, II)))",
1655 " trpt->o_pm |= 1; /* we moved */",
1656 " (trpt+1)->o_m = _m; /* for unsend */",
1661 " printf(\"%%3ld: proc %%d exec %%d, \",",
1662 " depth, II, t->forw);",
1663 " printf(\"%%d to %%d, %%s %%s %%s\",",
1664 " tt, t->st, t->tp,",
1665 " (t->atom&2)?\"atomic\":\"\",",
1666 " (boq != -1)?\"rendez-vous\":\"\");",
1667 " #ifdef HAS_UNLESS",
1669 " printf(\" (escapes to state %%d)\", t->st);",
1671 " printf(\" %%saccepting [tau=%%d]\\n\",",
1672 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
1674 " #ifdef HAS_UNLESS",
1675 " E_state = t->e_trans;",
1677 " if (t->e_trans > 0 && (boq != -1 /* || oboq != -1 */))",
1678 " { fprintf(efd, \"error:\ta rendezvous stmnt in the escape clause\\n\");",
1679 " fprintf(efd, \"\tof an unless stmnt is not compatible with -DBFS\\n\");",
1685 " { ((P0 *)this)->_p = t->st;",
1688 " /* ptr to pred: */ ntrpt->ostate = (H_el *) otrpt;",
1690 " if (boq == -1 && (t->atom&2)) /* atomic */",
1691 " ntrpt->tau = 8; /* record for next move */",
1694 " store_state(ntrpt, (boq != -1 || (t->atom&2)), oboq);",
1695 " #ifdef EVENT_TRACE",
1696 " now._event = trpt->o_event;",
1698 " /* undo move and continue */",
1699 " trpt++; /* this is where ovals and ipt are set */",
1700 " do_reverse(t, II, _m); /* restore now. */",
1703 " enter_critical(GLOBAL_LOCK); /* verbose mode */",
1705 " printf(\"cpu%%d: \", core_id);",
1707 " printf(\"%%3lu: proc %%d \", depth, II);",
1708 " printf(\"reverses %%d, %%d to %%d,\",",
1709 " t->forw, tt, t->st);",
1710 " printf(\" %%s [abit=%%d,adepth=%%ld,\",",
1711 " t->tp, now._a_t, A_depth);",
1712 " printf(\"tau=%%d,%%d]\\n\",",
1713 " trpt->tau, (trpt-1)->tau);",
1714 " leave_critical(GLOBAL_LOCK);",
1716 " reached[ot][t->st] = 1;",
1717 " reached[ot][tt] = 1;",
1719 " ((P0 *)this)->_p = tt;",
1722 " #ifndef NOREDUCE", /* with PO */
1723 " /* preselected - no succ definitely outside stack */",
1724 " if ((trpt->tau&32) && !(trpt->tau&64))",
1725 " { From = now._nr_pr-1; To = BASE;",
1727 " cpu_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
1728 " depth, II+1, (int) _n, trpt->tau);",
1730 " _n = 0; trpt->tau &= ~32;",
1736 " trpt->tau &= ~(32|64);",
1742 " printf(\"%%3ld: no move [II=%%d, tau=%%d, boq=%%d, _nr_pr=%%d]\\n\",",
1743 " depth, II, trpt->tau, boq, now._nr_pr);",
1747 " x = (Trail *) trpt->ostate; /* pre-rv state */",
1749 " { continue; /* root state */",
1751 " if ((x->tau&8) || (x->tau&32)) /* break atomic or preselect at parent */",
1752 " { x->o_pm |= 8; /* mark failure */",
1753 " this = pptr(otrpt->pr);",
1755 " printf(\"\\treset state of %%d from %%d to %%d\\n\",",
1756 " otrpt->pr, ((P0 *)this)->_p, otrpt->st);",
1758 " ((P0 *)this)->_p = otrpt->st;",
1759 " unsend(boq); /* retract rv offer */",
1762 " push_bfs(x, x->o_tt);",
1764 " printf(\"failed rv, repush with %%d\\n\", x->o_pm);",
1769 " { printf(\"failed rv, tau at parent: %%d\\n\", x->tau);",
1772 " } else if (now._nr_pr > 0)",
1774 " if ((trpt->tau&8)) /* atomic */",
1775 " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */",
1777 " printf(\"%%3ld: atomic step proc %%d blocks\\n\",",
1783 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
1784 " { trpt->tau |= 1;",
1786 " printf(\"%%ld: timeout\\n\", depth);",
1791 " if (!noends && !a_cycles && !endstate())",
1792 " { uerror(\"invalid end state\");",
1797 "#endif", /* !BFS_PAR */
1800 "putter(Trail *trpt, int fd)",
1803 " if (!trpt) return;",
1805 " if (trpt != (Trail *) trpt->ostate)",
1806 " putter((Trail *) trpt->ostate, fd);",
1809 " { sprintf(snap, \"%%d:%%d:%%d\\n\",",
1810 " trcnt++, trpt->pr, trpt->o_t->t_id);",
1811 " j = strlen(snap);",
1812 " if (write(fd, snap, j) != j)",
1813 " { printf(\"pan: error writing %%s\\n\", fnm);",
1819 "n_ewrite(int fd, char *s, int n)",
1820 "{ if (write(fd, s, strlen(s)) != strlen(s))",
1821 " { printf(\"pan: error writing %%s\\n\", fnm);",
1828 "{ int fd = make_trail();",
1831 " if (fd < 0) return;",
1833 " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
1834 " n_ewrite(fd, snap, strlen(snap));",
1837 " sprintf(snap, \"-4:-4:-4\\n\");",
1838 " n_ewrite(fd, snap, strlen(snap));",
1841 " putter(trpt, fd);",
1842 " if (ntrpt->o_t)", /* 4.2.8 -- Alex example, missing last transition */
1843 " { sprintf(snap, \"%%d:%%d:%%d\\n\",",
1844 " trcnt++, ntrpt->pr, ntrpt->o_t->t_id);",
1845 " j = strlen(snap);",
1846 " n_ewrite(fd, snap, j);",
1849 " if (errors >= upto && upto != 0)",
1857 static const char *Code2d[] = {
1858 "clock_t start_time;",
1860 "clock_t crash_stamp;",
1862 "#if !defined(WIN32) && !defined(WIN64)",
1863 "struct tms start_tm;",
1867 "extern int q_zero(int);",
1868 "extern int not_RV(int);",
1872 "start_timer(void)",
1874 "#if defined(WIN32) || defined(WIN64)",
1875 " start_time = clock();",
1877 " start_time = times(&start_tm);",
1881 "double delta_time;",
1884 "report_time(void)",
1886 " printf(\"\\npan: elapsed time %%.3g seconds\\n\", delta_time);",
1887 " if (delta_time > 0.01)",
1888 " { printf(\"pan: rate %%9.8g states/second\\n\", nstates/delta_time);",
1890 " { printf(\"pan: avg transition delay %%.5g usec\\n\",",
1891 " delta_time/(nstates+truncs));",
1896 "stop_timer(int report)",
1897 "{ clock_t stop_time;",
1898 "#if !defined(WIN32) && !defined(WIN64)",
1899 " struct tms stop_tm;",
1900 " stop_time = times(&stop_tm);",
1901 " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
1903 " stop_time = clock();",
1904 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
1906 " if (readtrail || delta_time < 0.00) return;",
1908 " if (core_id == 0 && nstates > (double) 0)",
1909 " { printf(\"\\ncpu%%d: elapsed time %%.3g seconds (%%g states visited)\\n\",",
1910 " core_id, delta_time, nstates);",
1911 " if (delta_time > 0.01)",
1912 " { printf(\"cpu%%d: rate %%g states/second\\n\", core_id, nstates/delta_time);",
1914 " { void check_overkill(void);",
1915 " check_overkill();",
1919 " { report_time();",
1926 "double t_alerts[17];",
1929 "crash_report(void)",
1931 " printf(\"crash alert intervals:\\n\");",
1932 " for (i = 0; i < 17; i++)",
1933 " { printf(\"%%d\\t%%g\\n\", i, t_alerts[i]);",
1938 "crash_reset(void)",
1939 "{ /* false alarm */",
1940 " if (crash_stamp != (clock_t) 0)",
1943 " double delta_time;",
1945 "#if defined(WIN32) || defined(WIN64)",
1946 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1948 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1950 " for (i = 0; i < 16; i++)",
1951 " { if (delta_time <= (i*30))",
1952 " { t_alerts[i] = delta_time;",
1955 " if (i == 16) t_alerts[i] = delta_time;",
1958 " printf(\"cpu%%d: crash alert off\\n\", core_id);",
1960 " crash_stamp = (clock_t) 0;",
1964 "crash_test(double maxtime)",
1965 "{ double delta_time;",
1966 " if (crash_stamp == (clock_t) 0)",
1967 " { /* start timing */",
1968 "#if defined(WIN32) || defined(WIN64)",
1969 " crash_stamp = clock();",
1971 " crash_stamp = times(&start_tm);",
1974 " { printf(\"cpu%%d: crash detection\\n\", core_id);",
1978 "#if defined(WIN32) || defined(WIN64)",
1979 " delta_time = ((double) (clock() - crash_stamp)) / ((double) CLOCKS_PER_SEC);",
1981 " delta_time = ((double) (times(&start_tm) - crash_stamp)) / ((double) sysconf(_SC_CLK_TCK));",
1983 " return (delta_time >= maxtime);",
1992 "do_the_search(void)",
1994 " depth = mreached = 0;",
1995 " trpt = &trail[0];",
1997 " trpt->tau |= 4; /* the claim moves first */",
1999 " for (i = 0; i < (int) now._nr_pr; i++)",
2000 " { P0 *ptr = (P0 *) pptr(i);",
2002 " if (!(trpt->o_pm&2)",
2003 " && accpstate[ptr->_t][ptr->_p])",
2004 " { trpt->o_pm |= 2;",
2008 " if (!(trpt->o_pm&4)",
2009 " && progstate[ptr->_t][ptr->_p])",
2010 " { trpt->o_pm |= 4;",
2015 "#ifdef EVENT_TRACE",
2017 " if (accpstate[EVENT_TRACE][now._event])",
2018 " { trpt->o_pm |= 2;",
2021 " if (progstate[EVENT_TRACE][now._event])",
2022 " { trpt->o_pm |= 4;",
2026 "#if !defined(NOCOMP) && !defined(HC)",
2027 " Mask[0] = Mask[1] = 1; /* _nr_pr, _nr_qs */",
2029 " { i = &(now._a_t) - (uchar *) &now;",
2030 " Mask[i] = 1; /* _a_t */",
2035 " i = &(now._cnt[0]) - (uchar *) &now;",
2036 " while (j++ < NFAIR)",
2037 " Mask[i++] = 1; /* _cnt[] */",
2043 " && (a_cycles && (trpt->o_pm&2)))",
2044 " { now._a_t = 2; /* set the A-bit */",
2045 " now._cnt[0] = now._nr_pr + 1;", /* NEW: +1 */
2047 " printf(\"%%3ld: fairness Rule 1, cnt=%%d, _a_t=%%d\\n\",",
2048 " depth, now._cnt[now._a_t&1], now._a_t);",
2053 " c_stack_start = (char *) &i; /* meant to be read-only */",
2055 "#if defined(HAS_CODE) && defined (C_INIT)",
2056 " C_INIT; /* initialization of data that must precede fork() */",
2060 "#if defined(C_States) && (HAS_TRACK==1)",
2061 " /* capture initial state of tracked C objects */",
2062 " c_update((uchar *) &(now.c_state[0]));",
2066 " if (readtrail) getrail(); /* no return */",
2073 " bfs_main(ncores,0);",
2078 " #if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
2079 " /* initial state of tracked & unmatched objects */",
2080 " c_stack((uchar *) &(svtack->c_stack[0]));",
2083 " #if defined(P_RAND) || defined(T_RAND)",
2084 " srand(s_rand+HASH_NR);", /* do_the_search */
2090 " new_state(); /* start 1st DFS */",
2095 "#ifdef INLINE_REV",
2097 "do_reverse(Trans *t, short II, uchar M)",
2099 " int tt = (int) ((P0 *)this)->_p;",
2100 "#include BACKWARD_MOVES",
2106 " #ifdef EVENT_TRACE",
2107 "static char _tp = 'n'; static int _qid = 0;",
2110 "do_transit(Trans *t, short II)",
2112 " int tt = (int) ((P0 *)this)->_p;",
2114 " uchar delta_m = 0;",
2116 " #ifdef EVENT_TRACE",
2117 " short oboq = boq;",
2118 " uchar ot = (uchar) ((P0 *)this)->_t;",
2119 " if (II == -EVENT_TRACE) boq = -1;",
2120 "#define continue { boq = oboq; return 0; }",
2122 "#define continue return 0",
2124 " uchar ot = (uchar) ((P0 *)this)->_t;",
2127 "#include FORWARD_MOVES",
2129 " #ifdef EVENT_TRACE",
2130 " if (II == -EVENT_TRACE) boq = oboq;",
2135 "#ifdef EVENT_TRACE",
2137 "require(char tp, int qid)",
2139 " _tp = tp; _qid = qid;",
2141 " if (now._event != endevent)",
2142 " for (t = trans[EVENT_TRACE][now._event]; t; t = t->nxt)",
2143 " { if (do_transit(t, -EVENT_TRACE))",
2144 " { now._event = t->st;",
2145 " reached[EVENT_TRACE][t->st] = 1;",
2147 " printf(\" event_trace move to -> %%d\\n\", t->st);",
2151 " if (accpstate[EVENT_TRACE][now._event])",
2152 " (trpt+1)->o_pm |= 2;",
2154 " if (progstate[EVENT_TRACE][now._event])",
2155 " (trpt+1)->o_pm |= 4;",
2158 " #ifdef NEGATED_TRACE",
2159 " if (now._event == endevent)",
2162 " depth++; trpt++;",
2164 " uerror(\"event_trace error (all events matched)\");",
2166 " trpt--; depth--;",
2171 " for (t = t->nxt; t; t = t->nxt)",
2172 " { if (do_transit(t, -EVENT_TRACE))",
2173 " Uerror(\"non-determinism in event-trace\");",
2179 " printf(\" event_trace miss '%%c' -- %%d, %%d, %%d\\n\",",
2180 " tp, qid, now._event, t->forw);",
2183 " #ifdef NEGATED_TRACE",
2184 " now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */",
2187 " depth++; trpt++;",
2189 " uerror(\"event_trace error (no matching event)\");",
2191 " trpt--; depth--;",
2197 "enabled(int iam, int pid)",
2198 "{ Trans *t; uchar *othis = this;",
2199 " int res = 0; int tt; uchar ot;",
2203 " Uerror(\"used: enabled(pid=thisproc)\");",
2204 " if (pid < 0 || pid >= (int) now._nr_pr)",
2206 " this = pptr(pid);",
2208 " tt = (int) ((P0 *)this)->_p;",
2209 " ot = (uchar) ((P0 *)this)->_t;",
2210 " for (t = trans[ot][tt]; t; t = t->nxt)",
2211 " if (do_transit(t, (short) pid))",
2221 "#ifdef HAS_PRIORITY",
2223 "highest_priority(int pid, short nII, Trans *t)",
2224 "{ int i = pid; uchar *othis = this;",
2228 " { return 1;", /* never claim */
2231 "#ifdef HAS_PROVIDED",
2232 " i = pid+BASE;", /* uncorrected process number */
2235 " || i >= (int) now._nr_pr",
2236 "#ifdef HAS_PROVIDED",
2237 " || !provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, t)",
2243 " for (i = BASE; i < now._nr_pr; i++)", /* all except never, if present */
2244 " { this = pptr(i);",
2245 " if (i != pid+BASE",
2246 " && ((P0 *)this)->_priority > ((P0 *)pptr(pid+BASE))->_priority",
2247 "#ifdef HAS_PROVIDED",
2248 " && provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, 0)",
2250 " && enabled(i+1, i-BASE))", /* enabled adds back BASE in 2nd arg */
2258 "get_priority(int pid)",
2259 "{ pid += BASE; /* 6.2.7 */",
2260 " if (pid < 0 || pid >= (int) now._nr_pr)",
2262 " return ((P0 *)pptr(pid))->_priority;",
2265 "set_priority(int pid, int pr)",
2266 "{ pid += BASE; /* 6.2.7 */",
2267 " if (pid < 0 || pid >= (int) now._nr_pr)",
2270 " printf(\"warning: bad pid %%d, no such process (set_priority)\\n\", pid);",
2274 " if (pr < 1 || pr > 255)",
2275 " { Uerror(\"priority is out of range\");",
2279 " { (trpt+1)->o_priority = ",
2280 " (((P0 *)pptr(pid))->_priority & 255) | (pid << 8);",
2281 " ((P0 *)pptr(pid))->_priority = pr;",
2284 " return 1;", /* always executable */
2290 "{ clock_t stop_time;",
2291 " double delta_time;",
2292 "#if !defined(WIN32) && !defined(WIN64)",
2293 " struct tms stop_tm;",
2294 " stop_time = times(&stop_tm);",
2295 " delta_time = ((double) (stop_time - start_time)) / ((double) sysconf(_SC_CLK_TCK));",
2297 " stop_time = clock();",
2298 " delta_time = ((double) (stop_time - start_time)) / ((double) CLOCKS_PER_SEC);",
2300 " if (delta_time > 0.01)",
2301 " { printf(\"t= %%8.3g \", delta_time);",
2302 " printf(\"R= %%7.0g\", nstates/delta_time);",
2304 " printf(\"\\n\");",
2305 " if (quota > 0.1 && delta_time > quota)",
2306 " { printf(\"Time limit of %%6.3g minutes exceeded\\n\", quota/60.0);",
2309 " leave_critical(GLOBAL_LOCK);",
2310 " sudden_stop(\"time-limit\");",
2320 " e_critical(BFS_GLOB); /* bfs_par / snapshot */",
2321 " printf(\"cpu%%d: \", who_am_i);",
2324 " enter_critical(GLOBAL_LOCK); /* ncore / snapshot */",
2325 " printf(\"cpu%%d: \", core_id);",
2327 " printf(\"Depth= %%7ld States= %%8.3g \",",
2329 " (long) (nr_handoffs * z_handoff) +",
2331 " mreached, nstates);",
2332 " printf(\"Transitions= %%8.3g \", nstates+truncs);",
2334 " printf(\"Nodes= %%7lu \", nr_states);",
2336 " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
2340 " leave_critical(GLOBAL_LOCK);",
2343 " x_critical(BFS_GLOB);",
2351 " && (stackwrite = creat(stackfile, TMODE)) < 0)",
2352 " Uerror(\"cannot create stackfile\");",
2354 " if (write(stackwrite, trail, DDD*sizeof(Trail))",
2355 " != DDD*sizeof(Trail))",
2356 " Uerror(\"stackfile write error -- disk is full?\");",
2358 " memmove(trail, &trail[DDD], (HHH-DDD+2)*sizeof(Trail));",
2359 " memset(&trail[HHH-DDD+2], 0, (omaxdepth - HHH + DDD - 2)*sizeof(Trail));",
2367 " memmove(&trail[DDD], trail, (HHH-DDD+2)*sizeof(Trail));",
2370 " || lseek(stackwrite, -DDD* (off_t) sizeof(Trail), SEEK_CUR) == -1)",
2371 " Uerror(\"disk2stack lseek error\");",
2374 " && (stackread = open(stackfile, 0)) < 0)",
2375 " Uerror(\"cannot open stackfile\");",
2377 " if (lseek(stackread, (CNT1-CNT2)*DDD* (off_t) sizeof(Trail), SEEK_SET) == -1)",
2378 " Uerror(\"disk2stack lseek error\");",
2380 " have = read(stackread, trail, DDD*sizeof(Trail));",
2381 " if (have != DDD*sizeof(Trail))",
2382 " Uerror(\"stackfile read error\");",
2388 "{ if (x < 0 || x >= MAXPROC", /* does not exist */
2390 " || !processes[x])",
2392 " || !proc_offset[x])",
2396 " return (uchar *) pptr(x);",
2400 "{ if (x < 0 || x >= MAXQ",
2402 " || !channels[x])",
2404 " || !q_offset[x])",
2408 " return (uchar *) qptr(x);",
2413 "select_claim(int n)",
2415 " if (n < 0 || n >= NCLAIMS)",
2416 " { uerror(\"non-existing claim\");",
2418 " { m = ((Pclaim *)pptr(0))->_n;",
2420 " { printf(\"%%d: Claim %%s (%%d), from state %%d\\n\",",
2421 " (int) depth, procname[spin_c_typ[n]],",
2422 " n, ((Pclaim *)pptr(0))->c_cur[n]);",
2424 " { printf(\"pan: ltl formula %%s\\n\",",
2425 " procname[spin_c_typ[n]]);",
2427 " ((Pclaim *)pptr(0))->c_cur[m] = ((Pclaim *)pptr(0))->_p;",
2428 " ((Pclaim *)pptr(0))->_t = spin_c_typ[n];",
2429 " ((Pclaim *)pptr(0))->_p = ((Pclaim *)pptr(0))->c_cur[n];",
2430 " ((Pclaim *)pptr(0))->_n = n;",
2431 " for (i = 0; src_all[i].src != (short *) 0; i++)",
2432 " { if (src_all[i].tp == spin_c_typ[n])",
2433 " { src_claim = src_all[i].src;",
2436 " if (src_all[i].src == (short *) 0)",
2437 " { uerror(\"cannot happen: src_ln ref\");",
2442 "select_claim(int n)",
2443 "{ if (n != 0) uerror(\"non-existing claim\");",
2447 "int qs_empty(void);",
2448 "#if !defined(BFS) && (!defined(BITSTATE) || !defined(MA))",
2452 "tally_succ(int cnt)",
2453 "{ if (cnt < 512) N_succ[cnt]++;",
2454 " else printf(\"tally_succ: cnt %%d exceeds range\\n\", cnt);",
2459 "{ int i; double sum = 0.0;",
2460 " double w_avg = 0.0;",
2461 " printf(\"Successor counts:\\n\");",
2462 " for (i = 0; i < 512; i++)",
2463 " { sum += (double) N_succ[i];",
2465 " for (i = 0; i < 512; i++)",
2466 " { if (N_succ[i] > 0)",
2467 " { printf(\"%%3d\t%%10d\t(%%.4g %%%% of total)\\n\",",
2468 " i, N_succ[i], (100.0 * (double) N_succ[i])/sum);",
2469 " w_avg += (double) i * (double) N_succ[i];",
2471 " if (sum > N_succ[0])",
2472 " printf(\"mean %%.4g (without 0: %%.4g)\\n\", w_avg / sum, w_avg / (sum - (double) N_succ[0]));",
2477 " #define FROM_P (BASE)",
2478 " #define UPTO_P (now._nr_pr-1)",
2479 " #define MORE_P (II <= To)", /* p.o. only */
2480 " #define INI_P (From-1)", /* fairness only */
2481 " #define CNT_P (1 + (To - From))", /* P_RAND start */
2482 " #define NDONE_P (From <= To)", /* P_RAND continue */
2483 " #define ALL_P (II = From; II <= To; II++)",
2485 " #define FROM_P (now._nr_pr-1)",
2486 " #define UPTO_P (BASE)",
2487 " #define MORE_P (II >= BASE)",
2488 " #define INI_P (From+1)",
2489 " #define CNT_P (1 + (From - To))",
2490 " #define NDONE_P (From >= To)",
2491 " #define ALL_P (II = From; II >= To; II--)",
2495 " #define CONTINUE0 { if (reversing&2) { II = oII; } continue; }",
2496 " #define CONTINUE { if (reversing&2) { p_reorder(seed); II = oII; } continue; }",
2498 " #define CONTINUE0 { continue; }",
2499 " #define CONTINUE { continue; }",
2503 "uchar _permutation_[256];",
2505 "set_reversed(int unused)",
2506 "{ int i, n = now._nr_pr;",
2508 " printf(\"%%ld: Set_reversed\\n\", depth);",
2510 " #if defined(VERI) && !defined(NOCLAIM)",
2511 " for (i = 1; i < n; i++)",
2512 " { _permutation_[i] = n-i;",
2515 " for (i = 0; i < n; i++)",
2516 " { _permutation_[i] = n-1-i;",
2521 "set_rotated(int unused)",
2522 "{ int i, n = now._nr_pr;",
2524 " printf(\"%%ld: Set_rotated %%d\\n\", depth, p_rotate);",
2526 " #if defined(VERI) && !defined(NOCLAIM)",
2527 " for (i = 1; i < n; i++)",
2528 " { _permutation_[i] = 1+(i-1+p_rotate)%%(n-1);",
2531 " for (i = 0; i < n; i++)",
2532 " { _permutation_[i] = (i+p_rotate)%%n;",
2537 "set_randrot(int unused)",
2539 " if (now._nr_pr > 1)",
2540 " { p_rotate = 1+rand()%%(now._nr_pr-1);",
2547 "set_permuted(int T)",
2548 "{ /* permute nrs 1..n-1, leave 0 in place */",
2549 " int i, j, k, n = now._nr_pr;",
2550 " char tmp, *in = &(_permutation_[0]);",
2552 " printf(\"%%ld: Set_permuted %%d\\n\", depth, T);",
2554 " srand(T);", /* set_permuted */
2555 " for (i = 0; i < n; i++)",
2559 " { for (i = 0; i < n; i++)",
2561 " #if defined(VERI) && !defined(NOCLAIM)",
2562 " j = 1 + rand()%%(n-1);",
2563 " k = 1 + rand()%%(n-1);",
2565 " j = rand()%%(n);",
2566 " k = rand()%%(n);",
2576 " get_permuted(int x)",
2577 " { printf(\"%%ld: Get_permuted %%d -> %%d\\n\",",
2578 " depth, x, _permutation_[x]);",
2579 " return (short) _permutation_[x];",
2582 " #define get_permuted(x) (short) _permutation_[x]",
2587 " * new_state() is the main DFS search routine in the verifier",
2588 " * it has a lot of code ifdef-ed together to support",
2589 " * different search modes, which makes it quite unreadable.",
2590 " * if you are studying the code, use the C preprocessor",
2591 " * to generate a specific version from the pan.c source,",
2592 " * e.g. by saying:",
2593 " * gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c",
2594 " * and then study the resulting file, instead of this version",
2600 " uchar _n, _m, ot;",
2605 " short oII; uint seed;",
2608 " uchar delta_m = 0;",
2610 " short II, JJ = 0, kk;",
2612 " short From = FROM_P, To = UPTO_P;",
2614 " trpt->sched_limit = 0; /* at depth=0 only */",
2618 " cpu_printf(\"%%d: Down - %%s %%saccepting [pids %%d-%%d]\\n\",",
2619 " depth, (trpt->tau&4)?\"claim\":\"program\",",
2620 " (trpt->o_pm&2)?\"\":\"non-\", From, To);",
2624 " trpt->p_skip = -1;",
2628 " if (depth > hiwater)",
2630 " maxdepth += DDD;",
2634 " printf(\"zap %%ld: %%ld (maxdepth now %%ld)\\n\",",
2635 " CNT1, hiwater, maxdepth);",
2639 " trpt->tau &= ~(16|32|64); /* make sure these are off */",
2640 "#if defined(FULLSTACK) && defined(MA)",
2641 " trpt->proviso = 0;",
2644 " trpt->n_succ = 0;",
2647 " if (mem_hand_off())",
2650 " (trpt+1)->o_n = 1; /* not a deadlock: as below */",
2652 "#ifndef LOOPSTATE",
2653 " (trpt-1)->tau |= 16; /* worstcase guess: as below */",
2655 "#if NCORE>1 && defined(FULL_TRAIL)",
2657 " { Pop_Stack_Tree();",
2664 " if (depth >= maxdepth)",
2667 " printf(\"error: max search depth too small\\n\");",
2670 " { uerror(\"depth limit reached\");",
2674 " (trpt+1)->o_n = 1; /* not a deadlock */",
2676 "#ifndef LOOPSTATE",
2677 " (trpt-1)->tau |= 16; /* worstcase guess */",
2680 "#if NCORE>1 && defined(FULL_TRAIL)",
2682 " { Pop_Stack_Tree();",
2688 "#if (defined(FULLSTACK) && !defined(MA)) || NCORE>1",
2689 " /* if atomic or rv move, carry forward previous state */",
2690 " trpt->ostate = (trpt-1)->ostate;",
2693 " if ((trpt->tau&4) || ((trpt-1)->tau&128))",
2695 " if (boq == -1) { /* if not mid-rv */",
2698 we want to skip nrpr, nrqs, _a_t and cnt[NFAIR] (in the case of fairness)
2699 this is calculated in S_A, but S_A subtracts 2 bytes,
2700 because nrpr and nrqs are masked in the default state comparisons
2701 so we add those two bytes back here
2702 -- in default comparisons (h_store) we skip _a_t and cnt in the
2703 -- first comparison to find a match on the base-state
2704 -- the _a_t and cnt fields are then separately updated if there was
2705 -- a match on the base state
2707 " if ((now._a_t&1) && depth > A_depth)",
2708 " { int delta = S_A + 2;",
2709 " if (!memcmp((char *)&A_Root + delta, ",
2710 " (char *)&now + delta, vsize - delta))",
2713 " if (fairness && now._cnt[1] != 1) /* was > 1 */",
2716 " printf(\"\tfairness count non-zero\\n\");",
2718 " /* treat as new state */",
2721 " { depthfound = A_depth;",
2723 " printf(\"matches seed\\n\");",
2726 " uerror(\"non-progress cycle\");",
2728 " uerror(\"acceptance cycle\");",
2730 " #if NCORE>1 && defined(FULL_TRAIL)",
2732 " { Pop_Stack_Tree();",
2740 " printf(\"not seed\\n\");",
2745 " if (!(trpt->tau&8)) /* if no atomic move */",
2747 "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
2748 " uchar was_last = now._last;",
2749 " now._last = 0; /* value not stored */",
2752 "#ifdef CNTRSTACK", /* -> bitstate, reduced, safety */
2753 " #if defined(BCS) && defined(STORE_CTX)",
2755 " for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
2756 " { now._ctx = xj;",
2757 " II = b_store((char *)&now, vsize);",
2758 " trpt->j6 = j1_spin; trpt->j7 = j2_spin;",
2759 " JJ = LL[j1_spin] && LL[j2_spin];",
2760 " if (II != 0) { break; }",
2762 " now._ctx = 0; /* just in case */",
2765 " II = b_store((char *)&now, vsize);",
2766 " trpt->j6 = j1_spin; trpt->j7 = j2_spin;",
2767 " JJ = LL[j1_spin] && LL[j2_spin];",
2770 " #ifdef FULLSTACK", /* b_store after onstack_now, to preserve j1-j4 */
2771 " #if defined(BCS) && defined(STORE_CTX)",
2774 " JJ = onstack_now();", /* mangles j1 */
2775 " for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
2776 " { now._ctx = xj;",
2777 " II = b_store((char *)&now, vsize);", /* sets j1-j4 */
2778 " if (II != 0) { break; }",
2783 " JJ = onstack_now();", /* mangles j1 */
2784 " II = b_store((char *)&now, vsize);", /* sets j1-j4 */
2787 " #if defined(BCS) && defined(STORE_CTX)",
2789 " for (xj = trpt->sched_limit; xj <= sched_max; xj++)",
2790 " { now._ctx = xj;",
2791 " II = b_store((char *)&now, vsize);", /* sets j1-j4 */
2792 " JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */",
2793 " if (II != 0) { break; }",
2798 " II = b_store((char *)&now, vsize);", /* sets j1-j4 */
2799 " JJ = II; /* worstcase guess for p.o. - order corrected in 5.2.1 */",
2805 " II = g_store((char *)&now, vsize, 0);",
2806 "#ifndef FULLSTACK",
2809 " JJ = (II == 2)?1:0;",
2812 " II = h_store((char *)&now, vsize);",
2813 " /* @hash j1_spin II */",
2815 " JJ = (II == 2)?1:0;",
2819 " kk = (II == 1 || II == 2);",
2820 /* actually, BCS implies HAS_LAST */
2821 "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
2822 " now._last = was_last; /* restore value */",
2825 /* II==0 new state */
2826 /* II==1 old state */
2827 /* II==2 on current dfs stack */
2828 /* II==3 on 1st dfs stack */
2830 /* with multicore we don't know which stack its on */
2831 /* with HC there's a small chance of a false match - example fifoq 2012 */
2832 "#if !defined(HC) && (NCORE==1 || defined (SEP_STATE))",
2833 " if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))",
2835 " if (a_cycles && !fairness) /* 5.1.6 -- example by Hirofumi Watanabe */",
2837 " if (depth > A_depth) /* forum example by adl */",
2839 " II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */",
2841 " printf(\"state match on dfs stack\\n\");",
2847 "#if defined(FULLSTACK) && defined(BITSTATE)",
2848 " if (!JJ && (now._a_t&1) && depth > A_depth)",
2849 " { int oj1 = j1_spin;",
2850 " uchar o_a_t = now._a_t;",
2851 " now._a_t &= ~(1|16|32);", /* 1st stack */
2852 " if (onstack_now())", /* changes j1_spin */
2855 " printf(\"state match on 1st dfs stack\\n\");",
2858 " now._a_t = o_a_t;", /* restore */
2862 " if (II == 3 && a_cycles && (now._a_t&1))",
2865 " if (fairness && now._cnt[1] != 1) /* was > 1 */",
2868 " printf(\"\tfairness count non-zero\\n\");",
2870 " II = 0;", /* treat as new state */
2877 "same_case: if (Lstate) depthfound = Lstate->D;",
2879 " uerror(\"non-progress cycle\");",
2881 " uerror(\"acceptance cycle\");",
2883 "#if NCORE>1 && defined(FULL_TRAIL)",
2885 " { Pop_Stack_Tree();",
2895 " #if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
2896 " if (II != 0 && (!Lstate || Lstate->cpu_id < core_id))",
2897 " { (trpt-1)->tau |= 16;", /* treat as a stack state */
2900 " if ((II && JJ) || (II == 3))",
2901 " { /* marker for liveness proviso */",
2902 " #ifndef LOOPSTATE",
2903 " (trpt-1)->tau |= 16;", /* truncated on stack */
2908 " #if NCORE>1 && !defined(SEP_STATE) && defined(V_PROVISO)",
2909 " if (!(II != 0 && (!Lstate || Lstate->cpu_id < core_id)))",
2910 " { /* treat as stack state */",
2911 " (trpt-1)->tau |= 16;",
2913 " { /* treat as non-stack state */",
2914 " (trpt-1)->tau |= 64;",
2918 " { /* successor outside stack */",
2919 " (trpt-1)->tau |= 64;",
2923 "#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))",
2924 /* needed for BCS - cover cases where it would not otherwise be set */
2926 " { (trpt-1)->tau |= 64;",
2931 "#if NCORE>1 && defined(FULL_TRAIL)",
2933 " { Pop_Stack_Tree();",
2941 " { static long sdone = (long) 0; long ndone;",
2943 "#if defined(ZAPH) && defined(BITSTATE)",
2944 " zstates += (double) hfns;",
2946 " ndone = (ulong) (nstates/(freq));",
2947 " if (ndone != sdone)",
2950 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
2951 " if (nstates > ((double)(ONE_L<<(ssize+1))))",
2952 " { void resize_hashtable(void);",
2953 " resize_hashtable();",
2956 "#if defined(ZAPH) && defined(BITSTATE)",
2957 " if (zstates > ((double)(ONE_L<<(ssize-2))))",
2958 " { /* more than half the bits set */",
2959 " void zap_hashtable(void);",
2960 " zap_hashtable();",
2966 " if (vprefix > 0)",
2967 " #ifdef SHO", /* Store Hash Only */
2968 " /* always use the same hashfunction, for consistency across runs */",
2969 " if (HASH_NR != 0)",
2970 " { int oh = HASH_NR;",
2972 " d_hash((uchar *) &now, vsize); /* SHO - set K1 */",
2975 " if (write(svfd, (uchar *) &K1, sizeof(ulong)) != sizeof(ulong))",
2977 " if (write(svfd, (uchar *) &now, vprefix) != vprefix)",
2979 " { fprintf(efd, \"writing %%s.svd failed\\n\", PanSource);",
2983 "#if defined(MA) && defined(W_XPT)",
2984 " if ((ulong) nstates%%W_XPT == 0)",
2985 " { void w_xpoint(void);",
2991 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
2994 "#if defined(FULLSTACK) && !defined(MA)",
2995 " printf(\"%%d: putting %%u (%%d)\\n\", depth,",
2997 " (trpt->ostate)?trpt->ostate->tagged:0);",
2999 " printf(\"%%d: putting\\n\", depth);",
3004 " trpt->ostate = Lstate;",
3009 " if (depth > mreached)",
3010 " mreached = depth;",
3012 " if (trpt->tau&4)",
3014 " trpt->tau &= ~(1|2); /* timeout and -request off */",
3017 " (trpt+1)->o_n = 0;",
3020 " if (now._nr_pr == 0) /* claim terminated */",
3021 " { uerror(\"end state in claim reached\");",
3023 " if (stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])",
3024 " { uerror(\"end state in claim reached\");",
3027 " if (trpt->tau&4) /* must make a claimmove */",
3030 " if ((now._a_t&2) /* A-bit set */",
3031 " && now._cnt[now._a_t&1] == 1)",
3032 " { now._a_t &= ~2;",
3033 " now._cnt[now._a_t&1] = 0;",
3034 " trpt->o_pm |= 16;",
3036 " printf(\"%%3d: fairness Rule 3.: _a_t = %%d\\n\",",
3037 " (int) depth, now._a_t);",
3041 " II = 0; /* never */",
3046 " if (reversing&2)",
3047 " { seed = rand();",
3048 " p_reorder(seed);",
3052 " /* Look for a process with only safe transitions */",
3053 " /* (special rules apply in the 2nd dfs) */",
3054 " if (boq == -1 && From != To",
3058 " && (depth < z_handoff)", /* not for border states */
3063 " && ((a_cycles) || (!a_cycles && depth < z_handoff))",
3066 " && (sched_max > 0 || depth > BASE)", /* no po in initial state if -L0 */
3068 " && (!(now._a_t&1)",
3070 " #ifndef BITSTATE",
3073 " !((trpt-1)->proviso))",
3075 " !(trpt->proviso))",
3079 " (trpt-1)->ostate &&",
3080 " !(((char *)&((trpt-1)->ostate->state))[0] & 128))", /* proviso bit in _a_t */
3082 " !(((char *)&(trpt->ostate->state))[0] & 128))",
3087 " (trpt-1)->ostate &&",
3088 " (trpt-1)->ostate->proviso == 0)",
3090 " trpt->ostate->proviso == 0)",
3094 "#endif", /* SAFETY */
3095 " /* attempt Partial Order Reduction as preselect moves */",
3097 " if (trpt->sched_limit < sched_max)", /* po only if we can switch */
3099 " { for ALL_P {", /* PO preselect */
3100 "Resume: /* pick up here if preselect fails */",
3101 " this = pptr(II);",
3102 " tt = (int) ((P0 *)this)->_p;",
3103 " ot = (uchar) ((P0 *)this)->_t;",
3104 " if (trans[ot][tt]->atom & 8)",
3105 " { t = trans[ot][tt];",
3106 " if (t->qu[0] != 0)",
3108 " if (!q_cond(II, t))",
3113 " From = To = II; /* preselect process */",
3117 " trpt->tau |= 32; /* preselect marker */",
3119 " printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
3120 " depth, II, trpt->tau);",
3126 " trpt->tau &= ~32;",
3128 "#if !defined(NOREDUCE) || (defined(ETIM) && !defined(VERI))",
3131 " trpt->o_pm &= ~(8|16|32|64); /* clear fairness-marks */",
3133 " if (fairness && boq == -1",
3135 " && (!(trpt->tau&4) && !((trpt-1)->tau&128))",
3137 " && !(trpt->tau&8))",
3138 " { /* A_bit = 1; Cnt = N in acc states with A_bit 0 */",
3139 " if (!(now._a_t&2))", /* A-bit not set */
3140 " { if (a_cycles && (trpt->o_pm&2))",
3141 " { /* Accepting state */",
3143 " now._cnt[now._a_t&1] = now._nr_pr + 1;",
3144 " trpt->o_pm |= 8;",
3146 " printf(\"%%3ld: fairness Rule 1: cnt=%%d, _a_t=%%d\\n\",",
3147 " depth, now._cnt[now._a_t&1], now._a_t);",
3150 " } else", /* A-bit set */
3151 " { /* A_bit = 0 when Cnt 0 */",
3152 " if (now._cnt[now._a_t&1] == 1)",
3153 " { now._a_t &= ~2;", /* reset a-bit */
3154 " now._cnt[now._a_t&1] = 0;",
3155 " trpt->o_pm |= 16;",
3157 " printf(\"%%3ld: fairness Rule 3: _a_t = %%d\\n\",",
3158 " depth, now._a_t);",
3163 "#ifdef BCS", /* bounded context switching */
3164 " trpt->bcs = trpt->b_pno = 0; /* initial */",
3165 " if (From != To /* not a PO or atomic move */",
3166 " && depth > BASE) /* there is a prior move */",
3167 " { trpt->b_pno = now._last + BASE;",
3168 " trpt->bcs = B_PHASE1;",
3170 " printf(\"%%3ld: BCS phase 1 proc %%d limit %%d\\n\",",
3171 " depth, trpt->b_pno, trpt->sched_limit);",
3173 " /* allow only process b_pno to move in this phase */",
3175 "c_switch: /* jumps here with bcs == B_PHASE2 with or wo B_FORCED added */",
3177 " printf(\"%%3ld: BCS c_switch phase=%%d pno=%%d [forced %%d]\\n\",",
3178 " depth, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
3183 " trpt->p_left = CNT_P;",
3184 " if (trpt->p_left > 1)",
3185 " { trpt->p_skip = rand() %% (trpt->p_left);",
3187 " { trpt->p_skip = -1;",
3191 " printf(\"%%3ld: P_RAND r_switch p_skip=%%d p_left=%%d\\n\",",
3192 " depth, trpt->p_skip, trpt->p_left);",
3196 " for ALL_P {", /* Main Loop */
3198 " if (reversing&2)",
3200 " if (From != To)", /* not atomic or preselected */
3201 " { II = get_permuted(II);",
3205 " if (trpt->p_skip >= 0)",
3206 " { trpt->p_skip--; /* skip random nr of procs */",
3208 " printf(\"%%3ld: P_RAND skipping %%d [new p_skip=%%d p_left=%%d]\\n\",",
3209 " depth, II, trpt->p_skip, trpt->p_left);",
3213 " if (trpt->p_left == 0)",
3216 " printf(\"%%3ld: P_RAND done at %%d\\n\", depth, II);",
3218 " break; /* done */",
3221 " printf(\"%%3ld: P_RAND explore %%d [p_left=%%d]\\n\",",
3222 " depth, II, trpt->p_left);",
3228 " /* no rendezvous with same proc */",
3229 " if (boq != -1 && trpt->pr == II)",
3234 "#ifdef BCS", /* never claim with II==0 cannot get here */
3235 " if ((trpt->bcs & B_PHASE1)",
3236 " && trpt->b_pno != II)",
3239 " printf(\"%%3ld: BCS NotPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
3240 " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
3242 " CONTINUE0;", /* avoid context switch */
3245 " else if ((trpt->bcs & B_PHASE1) && trpt->b_pno == II)",
3246 " printf(\"%%3ld: BCS IsPre II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
3247 " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
3250 " if (trpt->bcs & B_PHASE2) /* 2nd phase */",
3251 " { if (trpt->b_pno == II) /* was already done in phase 1 */",
3254 " printf(\"%%3ld: BCS NoRepeat II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
3255 " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
3259 " if (!(trpt->bcs & B_FORCED) /* unless forced */",
3260 " && trpt->sched_limit >= sched_max)",
3263 " printf(\"%%3ld: BCS Bound II=%%d bcs=%%d pno=%%d [forced %%d]\\n\",",
3264 " depth, II, trpt->bcs, trpt->b_pno, (trpt->bcs&B_FORCED)?1:0);",
3266 " CONTINUE0; /* enforce bound */",
3273 " this = pptr(II);",
3274 " tt = (int) ((P0 *)this)->_p;",
3275 " ot = (uchar) ((P0 *)this)->_t;",
3278 " /* don't repeat a previous preselected expansion */",
3279 " /* could hit this if reduction proviso was false */",
3280 " t = trans[ot][tt];",
3281 " if (!(trpt->tau&4)", /* not claim */
3282 " && !(trpt->tau&1)", /* not timeout */
3283 " && !(trpt->tau&32)", /* not preselected */
3284 " && (t->atom & 8)", /* local */
3285 " && boq == -1", /* not inside rendezvous */
3286 " && From != To)", /* not inside atomic seq */
3287 " { if (t->qu[0] == 0", /* unconditional */
3288 " || q_cond(II, t))", /* true condition */
3290 " if (_m>_n||(_n>3&&_m!=0))",
3293 " CONTINUE0; /* did it before */",
3296 " trpt->o_pm &= ~1; /* no move in this pid yet */",
3297 "#ifdef EVENT_TRACE",
3298 " (trpt+1)->o_event = now._event;",
3300 " /* Fairness: Cnt++ when Cnt == II */",
3302 " trpt->o_pm &= ~64; /* didn't apply rule 2 */",
3304 " && boq == -1", /* not mid rv - except rcv - NEW 3.0.8 */
3305 " && !(trpt->o_pm&32)", /* Rule 2 not in effect */
3306 " && (now._a_t&2)", /* A-bit is set */
3307 " && now._cnt[now._a_t&1] == II+2)",
3308 " { now._cnt[now._a_t&1] -= 1;",
3310 " /* claim need not participate */",
3312 " now._cnt[now._a_t&1] = 1;",
3315 " printf(\"%%3ld: proc %%d fairness \", depth, II);",
3316 " printf(\"Rule 2: --cnt to %%d (%%d)\\n\",",
3317 " now._cnt[now._a_t&1], now._a_t);",
3319 " trpt->o_pm |= (32|64);",
3323 "#ifdef HAS_PRIORITY",
3324 " if (!highest_priority(((P0 *)this)->_pid, II, t))",
3328 " #ifdef HAS_PROVIDED",
3329 " if (!provided(II, ot, tt, t))",
3335 " /* check all trans of proc II - escapes first */",
3336 "#ifdef HAS_UNLESS",
3337 " trpt->e_state = 0;",
3339 " (trpt+1)->pr = (uchar) II;", /* for uerror */
3340 " (trpt+1)->st = tt;",
3343 " for (ooi = eoi = 0, t = trans[ot][tt]; t; t = t->nxt, ooi++)",
3344 " { if (strcmp(t->tp, \"else\") == 0",
3345 " #ifdef HAS_UNLESS",
3346 " || t->e_trans != 0",
3349 " { eoi++;", /* no break, must count ooi */
3352 " { t = trans[ot][tt];",
3354 " printf(\"randomizer: suppressed, saw else or escape\\n\");",
3356 " } else if (ooi > 0)",
3357 " { eoi = rand()%%ooi;",
3359 " printf(\"randomizer: skip %%d in %%d\\n\", eoi, ooi);",
3361 " for (t = trans[ot][tt]; t; t = t->nxt)",
3362 " if (eoi-- <= 0) break;",
3365 " for ( ; t && ooi > 0; t = t->nxt, ooi--)",
3366 "#else", /* ie dont randomize */
3367 " for (t = trans[ot][tt]; t; t = t->nxt)",
3370 "#ifdef HAS_UNLESS",
3371 " /* exploring all transitions from",
3372 " * a single escape state suffices",
3374 " if (trpt->e_state > 0",
3375 " && trpt->e_state != t->e_trans)",
3378 " printf(\"skip 2nd escape %%d (did %%d before)\\n\",",
3379 " t->e_trans, trpt->e_state);",
3384 " #if defined(TRIX) && !defined(TRIX_ORIG) && !defined(BFS)",
3385 " (trpt+1)->p_bup = now._ids_[II];",
3387 " (trpt+1)->o_t = t;", /* for uerror */
3389 "#include FORWARD_MOVES",
3390 "P999: /* jumps here when move succeeds */",
3392 " if (!(_m = do_transit(t, II)))",
3397 " if (depth > BASE", /* has prior move */
3398 " && II >= BASE", /* not claim */
3399 " && From != To", /* not atomic or po */
3400 " #ifndef BCS_NOFIX",
3401 " /* added 5.2.5: prior move was not po */",
3402 " && !((trpt-(BASE+1))->tau & 32)",
3404 " && boq == -1", /* not rv */
3405 " && (trpt->bcs & B_PHASE2)",
3406 " && trpt->b_pno != II /* context switch */", /* redundant */
3407 " && !(trpt->bcs & B_FORCED)) /* unless forced */",
3408 " { (trpt+1)->sched_limit = 1 + trpt->sched_limit;",
3410 " printf(\"%%3ld: up sched count to %%d\\n\", depth, (trpt+1)->sched_limit);",
3413 " { (trpt+1)->sched_limit = trpt->sched_limit;",
3415 " printf(\"%%3ld: keep sched count at %%d\\n\", depth, (trpt+1)->sched_limit);",
3421 " /* for branching-time, can accept reduction only if */",
3422 " /* the persistent set contains just 1 transition */",
3423 " { if ((trpt->tau&32) && (trpt->o_pm&1))",
3424 " trpt->tau |= 16;", /* CTL */
3425 " trpt->o_pm |= 1; /* we moved */",
3428 " trpt->o_pm |= 1; /* we moved */",
3432 " if (loopstate[ot][tt])",
3435 " printf(\"exiting from loopstate:\\n\");",
3437 " trpt->tau |= 16;", /* exiting loopstate */
3445 "#if defined(VERBOSE) || defined(CHECK)",
3446 "#if defined(SVDUMP)",
3447 " cpu_printf(\"%%3ld: proc %%d exec %%d \\n\", depth, II, t->t_id);",
3449 " cpu_printf(\"%%3ld: proc %%d exec %%d, %%d to %%d, %%s %%s %%s %%saccepting [tau=%%d]\\n\", ",
3450 " depth, II, t->forw, tt, t->st, t->tp,",
3451 " (t->atom&2)?\"atomic\":\"\",",
3452 " (boq != -1)?\"rendez-vous\":\"\",",
3453 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
3454 "#ifdef HAS_UNLESS",
3456 " cpu_printf(\"\\t(escape to state %%d)\\n\", t->st);",
3460 " cpu_printf(\"\\t(randomizer %%d)\\n\", ooi);",
3468 " now._last = II - BASE;",
3470 "#ifdef HAS_UNLESS",
3471 " trpt->e_state = t->e_trans;",
3474 " depth++; trpt++;",
3475 " trpt->pr = (uchar) II;",
3477 " trpt->o_pm &= ~(2|4);",
3479 " { ((P0 *)this)->_p = t->st;",
3480 "/* moved down reached[ot][t->st] = 1; */",
3485 "#if (ACCEPT_LAB>0 && !defined(NP)) || (PROG_LAB>0 && defined(HAS_NP))",
3488 "#define P__Q ((P0 *)pptr(ii))",
3491 " /* state 1 of np_ claim is accepting */",
3492 " if (((P0 *)pptr(0))->_p == 1)",
3493 " trpt->o_pm |= 2;",
3495 " for (ii = 0; ii < (int) now._nr_pr; ii++)",
3496 " { if (accpstate[P__Q->_t][P__Q->_p])",
3497 " { trpt->o_pm |= 2;",
3502 "#if defined(HAS_NP) && PROG_LAB>0",
3503 " for (ii = 0; ii < (int) now._nr_pr; ii++)",
3504 " { if (progstate[P__Q->_t][P__Q->_p])",
3505 " { trpt->o_pm |= 4;",
3512 " trpt->o_t = t; trpt->o_n = _n;",
3513 " trpt->o_ot = ot; trpt->o_tt = tt;",
3514 " trpt->o_To = To; trpt->o_m = _m;",
3517 " if (reversing&2)",
3518 " { trpt->seed = seed;",
3519 " trpt->oII = oII;",
3523 "#if defined(T_RAND) && !defined(BFS)",
3524 " trpt->oo_i = ooi;",
3526 " if (boq != -1 || (t->atom&2))",
3527 " { trpt->tau |= 8;",
3529 " /* atomic sequence in claim */",
3530 " if((trpt-1)->tau&4)",
3533 " trpt->tau &= ~4;",
3535 " { if ((trpt-1)->tau&4)",
3536 " trpt->tau &= ~4;",
3540 " /* if claim allowed timeout, so */",
3541 " /* does the next program-step: */",
3542 " if (((trpt-1)->tau&1) && !(trpt->tau&4))",
3546 " trpt->tau &= ~8;",
3548 " if (boq == -1 && (t->atom&2))",
3549 " { From = To = II; nlinks++;",
3551 " { From = FROM_P; To = UPTO_P;",
3553 "#if NCORE>1 && defined(FULL_TRAIL)",
3555 " { Push_Stack_Tree(II, t->t_id);",
3559 " if (processes[II])", /* last move could have been a delproc */
3560 " { processes[II]->modified = 1; /* transition in II */",
3562 " printf(\"%%4d: process %%d modified\\n\", depth, II);",
3564 " { printf(\"%%4d: process %%d modified but gone (%%p)\\n\",",
3565 " depth, II, trpt);",
3569 " goto Down; /* pseudo-recursion */",
3572 " #ifndef TRIX_ORIG",
3574 " now._ids_[trpt->pr] = trpt->p_bup;",
3577 " if (processes[trpt->pr])",
3579 " processes[trpt->pr]->modified = 1; /* reverse move */",
3581 " printf(\"%%4d: unmodify pr %%d (%%p)\\n\",",
3582 " depth, trpt->pr, trpt);",
3584 " { printf(\"%%4d: unmodify pr %%d (gone) (%%p)\\n\",",
3585 " depth, trpt->pr, trpt);",
3591 " cpu_printf(\"%%d: Up - %%s\\n\", depth,",
3592 " (trpt->tau&4)?\"claim\":\"program\");",
3600 "#if defined(MA) || NCORE>1",
3601 " if (depth <= 0) return;",
3602 " /* e.g., if first state is old, after a restart */",
3607 " && depth < hiwater - (HHH-DDD) - 2)", /* 5.1.6: was + 2 */
3611 " maxdepth -= DDD;",
3614 " printf(\"unzap %%ld: %%ld\\n\", CNT2, hiwater);",
3618 "#ifndef SAFETY", /* moved earlier in version 5.2.5 */
3619 " if ((now._a_t&1) && depth <= A_depth)",
3620 " return; /* to checkcycles() */",
3624 " if (trpt->o_pm&128) /* fairness alg */",
3625 " { now._cnt[now._a_t&1] = trpt->bup.oval;",
3626 " _n = 1; trpt->o_pm &= ~128;",
3627 " depth--; trpt--;",
3628 "#if defined(VERBOSE) || defined(CHECK)",
3629 " printf(\"%%3ld: reversed fairness default move\\n\", depth);",
3637 " { long d; Trail *trl;",
3639 " for (d = 1; d < depth; d++)",
3640 " { trl = getframe(depth-d); /* was (trpt-d) */",
3641 " if (trl->pr != 0)",
3642 " { now._last = trl->pr - BASE;",
3646 " now._last = (depth<1)?0:(trpt-1)->pr;",
3649 "#ifdef EVENT_TRACE",
3650 " now._event = trpt->o_event;",
3652 " t = trpt->o_t; _n = trpt->o_n;",
3653 " ot = trpt->o_ot; II = trpt->pr;",
3654 " tt = trpt->o_tt; this = Pptr(II);",
3655 " To = trpt->o_To; _m = trpt->o_m;",
3657 " if (reversing&2)",
3658 " { seed = trpt->seed;",
3659 " oII = trpt->oII;",
3662 "#if defined(T_RAND) && !defined(BFS)",
3663 " ooi = trpt->oo_i;",
3665 "#ifdef INLINE_REV",
3666 " _m = do_reverse(t, II, _m);",
3668 "#include BACKWARD_MOVES",
3669 "R999: /* jumps here when done */",
3673 " cpu_printf(\"%%3ld: proc %%d reverses %%d, %%d to %%d\\n\",",
3674 " depth, II, t->forw, tt, t->st);",
3675 " cpu_printf(\"\\t%%s [abit=%%d,adepth=%%ld,tau=%%d,%%d]\\n\", ",
3676 " t->tp, now._a_t, A_depth, trpt->tau, (trpt-1)->tau);",
3679 " /* pass the proviso tags */",
3680 " if ((trpt->tau&8) /* rv or atomic */",
3681 " && (trpt->tau&16))",
3682 " (trpt-1)->tau |= 16;", /* pass upward */
3684 " if ((trpt->tau&8) /* rv or atomic */",
3685 " && (trpt->tau&64))",
3686 " (trpt-1)->tau |= 64;",
3690 "#if defined(BCS) && (defined(NOREDUCE) || !defined(SAFETY))",
3691 /* for BCS, cover cases where 64 is otherwise not handled */
3692 " if ((trpt->tau&8)",
3693 " && (trpt->tau&64))",
3694 " (trpt-1)->tau |= 64;",
3697 " depth--; trpt--;",
3703 " (trans[ot][tt])->om = _m; /* head of list */",
3706 " /* i.e., not set if rv fails */",
3708 " { reached[ot][t->st] = 1;",
3709 " reached[ot][tt] = 1;",
3711 "#ifdef HAS_UNLESS",
3712 " else trpt->e_state = 0; /* undo */",
3715 " if (_m>_n||(_n>3&&_m!=0)) _n=_m;",
3716 " ((P0 *)this)->_p = tt;",
3717 " } /* all options */",
3720 " if (!t && ooi > 0)", /* means we skipped some initial options */
3721 " { t = trans[ot][tt];",
3723 " printf(\"randomizer: continue for %%d more\\n\", ooi);",
3729 " printf(\"randomizer: done\\n\");",
3734 " /* Fairness: undo Rule 2 */",
3735 " if ((trpt->o_pm&32)",/* rule 2 was applied */
3736 " && (trpt->o_pm&64))",/* by this process II */
3737 " { if (trpt->o_pm&1)",/* it didn't block */
3740 " if (now._cnt[now._a_t&1] == 1)",
3741 " now._cnt[now._a_t&1] = 2;",
3743 " now._cnt[now._a_t&1] += 1;",
3745 " printf(\"%%3ld: proc %%d fairness \", depth, II);",
3746 " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
3747 " now._cnt[now._a_t&1], now._a_t);",
3749 " trpt->o_pm &= ~(32|64);",
3750 " } else", /* process blocked */
3751 " { if (_n > 0)", /* a prev proc didn't */
3752 " {", /* start over */
3753 " trpt->o_pm &= ~64;",
3754 " II = INI_P;", /* after loop incr II == From */
3759 " { break; /* never claim */",
3766 " tally_succ(trpt->n_succ);",
3770 " if (trpt->p_left > 0 && NDONE_P)",
3771 " { trpt->p_skip = -1; /* probably rendundant */",
3773 " printf(\"%%3ld: P_RAND -- explore remainder\\n\", depth);",
3775 " goto r_switch; /* explore the remaining procs */",
3779 " printf(\"%%3ld: P_RAND -- none left\\n\", depth);",
3785 " if (trpt->bcs & B_PHASE1)",
3786 " { trpt->bcs = B_PHASE2; /* start 2nd phase */",
3787 " if (_n == 0 || !(trpt->tau&64)) /* pre-move unexecutable or led to stackstate */",
3788 " { trpt->bcs |= B_FORCED; /* forced switch */",
3791 " printf(\"%%3ld: BCS move to phase 2, _n=%%d %%s\\n\", depth, _n,",
3792 " (trpt->bcs & B_FORCED)?\"forced\":\"free\");",
3794 " From = FROM_P; To = UPTO_P;",
3798 " if (_n == 0 /* no process could move */",
3799 " && II >= BASE /* not the never claim */",
3800 " && trpt->sched_limit >= sched_max)",
3803 " printf(\"%%3ld: BCS not a deadlock\\n\", depth);",
3809 " /* Fairness: undo Rule 2 */",
3810 " if (trpt->o_pm&32) /* remains if proc blocked */",
3813 " if (now._cnt[now._a_t&1] == 1)",
3814 " now._cnt[now._a_t&1] = 2;",
3816 " now._cnt[now._a_t&1] += 1;",
3818 " printf(\"%%3ld: proc -- fairness \", depth);",
3819 " printf(\"undo Rule 2, cnt=%%d, _a_t=%%d\\n\",",
3820 " now._cnt[now._a_t&1], now._a_t);",
3822 " trpt->o_pm &= ~32;",
3825 /* 12/97 non-progress cycles cannot be created
3826 * by stuttering extension, here or elsewhere
3829 " && _n == 0 /* nobody moved */",
3831 " && !(trpt->tau&4) /* in program move */",
3833 " && !(trpt->tau&8) /* not an atomic one */",
3835 " && (trpt->tau&1) /* already tried timeout */",
3839 " && !((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3841 " && now._cnt[now._a_t&1] > 0) /* needed more procs */",
3842 " { depth++; trpt++;",
3843 " trpt->o_pm |= 128 | ((trpt-1)->o_pm&(2|4));",
3844 " trpt->bup.oval = now._cnt[now._a_t&1];",
3845 " now._cnt[now._a_t&1] = 1;",
3851 " From = FROM_P; To = UPTO_P;",
3852 "#if defined(VERBOSE) || defined(CHECK)",
3853 " printf(\"%%3ld: fairness default move \", depth);",
3854 " printf(\"(all procs block)\\n\");",
3859 "Q999: /* returns here with _n>0 when done */;",
3861 " if (trpt->o_pm&8)",
3862 " { now._a_t &= ~2;",
3863 " now._cnt[now._a_t&1] = 0;",
3864 " trpt->o_pm &= ~8;",
3866 " printf(\"%%3ld: fairness undo Rule 1, _a_t=%%d\\n\",",
3867 " depth, now._a_t);",
3870 " if (trpt->o_pm&16)",
3871 " { now._a_t |= 2;", /* restore a-bit */
3872 " now._cnt[now._a_t&1] = 1;", /* NEW: restore cnt */
3873 " trpt->o_pm &= ~16;",
3875 " printf(\"%%3ld: fairness undo Rule 3, _a_t=%%d\\n\",",
3876 " depth, now._a_t);",
3883 " #ifdef LOOPSTATE",
3884 " /* at least one move that was preselected at this */",
3885 " /* level, blocked or was a loop control flow point */",
3886 " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3888 " /* preselected move - no successors outside stack */",
3889 " if ((trpt->tau&32) && !(trpt->tau&64))",
3891 " { From = FROM_P; To = UPTO_P; /* undo From == To */",
3893 " printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3894 " depth, II+1, _n, trpt->tau);",
3896 " _n = 0; trpt->tau &= ~(16|32|64);",
3898 " if (MORE_P) /* II already restored and updated */",
3904 " /* at least one move that was preselected at this */",
3905 " /* level, blocked or truncated at the next level */",
3906 " if ((trpt->tau&32) && (_n == 0 || (trpt->tau&16)))",
3909 " printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
3910 " depth, II+1, (int) _n, trpt->tau);",
3912 " if (a_cycles && (trpt->tau&16))",
3913 " { if (!(now._a_t&1))",
3916 " printf(\"%%3ld: setting proviso bit\\n\", depth);",
3921 " (trpt-1)->proviso = 1;",
3923 " trpt->proviso = 1;",
3927 " if ((trpt-1)->ostate)",
3928 " ((char *)&((trpt-1)->ostate->state))[0] |= 128;",
3930 " ((char *)&(trpt->ostate->state))[0] |= 128;",
3935 " if ((trpt-1)->ostate)",
3936 " (trpt-1)->ostate->proviso = 1;",
3938 " trpt->ostate->proviso = 1;",
3941 " From = FROM_P; To = UPTO_P;",
3942 " _n = 0; trpt->tau &= ~(16|32|64);",
3943 " goto Again; /* do full search */",
3944 " } /* else accept reduction */",
3946 " { From = FROM_P; To = UPTO_P;",
3947 " _n = 0; trpt->tau &= ~(16|32|64);",
3948 " if (MORE_P) /* II already updated */",
3956 " if (_n == 0 || ((trpt->tau&4) && (trpt->tau&2)))",
3959 " cpu_printf(\"%%3ld: no move [II=%%d, tau=%%d, boq=%%d]\\n\",",
3960 " depth, II, trpt->tau, boq);",
3963 " /* ok if a rendez-vous fails: */",
3964 " if (boq != -1) goto Done;",
3966 " /* ok if no procs or we're at maxdepth */",
3967 " if ((now._nr_pr == 0 && (!strict || qs_empty()))",
3968 " || depth >= maxdepth-1) goto Done; /* undo change from 5.2.3 */",
3970 " if ((trpt->tau&8) && !(trpt->tau&4))",
3971 " { trpt->tau &= ~(1|8);",
3972 " /* 1=timeout, 8=atomic */",
3973 " From = FROM_P; To = UPTO_P;",
3975 " cpu_printf(\"%%3ld: atomic step proc %%d unexecutable\\n\", depth, II+1);",
3978 " trpt->tau |= 4; /* switch to claim */",
3984 " if (!(trpt->tau&1)) /* didn't try timeout yet */",
3987 " if (trpt->tau&4)",
3990 " if (trpt->tau&2) /* requested */",
3992 " { trpt->tau |= 1;",
3993 " trpt->tau &= ~2;",
3995 " cpu_printf(\"%%d: timeout\\n\", depth);",
4000 " { /* only claim can enable timeout */",
4001 " if ((trpt->tau&8)",
4002 " && !((trpt-1)->tau&4))",
4003 "/* blocks inside an atomic */ goto BreakOut;",
4005 " cpu_printf(\"%%d: req timeout\\n\",",
4008 " (trpt-1)->tau |= 2; /* request */",
4009 " #if NCORE>1 && defined(FULL_TRAIL)",
4011 " { Pop_Stack_Tree();",
4018 " cpu_printf(\"%%d: timeout\\n\", depth);",
4026 /* old location of atomic block code */
4029 "#ifndef NOSTUTTER",
4030 " if (!(trpt->tau&4))",
4031 " { trpt->tau |= 4; /* claim stuttering */",
4032 " trpt->tau |= 128; /* stutter mark */",
4034 " cpu_printf(\"%%d: claim stutter\\n\", depth);",
4042 " if (!noends && !a_cycles && !endstate())",
4043 " { depth--; trpt--; /* new 4.2.3 */",
4044 " uerror(\"invalid end state\");",
4045 " depth++; trpt++;",
4047 "#ifndef NOSTUTTER",
4048 " else if (a_cycles && (trpt->o_pm&2)) /* new 4.2.4 */",
4049 " { depth--; trpt--;",
4050 " uerror(\"accept stutter\");",
4051 " depth++; trpt++;",
4057 " if (!(trpt->tau&8)) /* not in atomic seqs */",
4061 "#if defined(FULLSTACK) || defined(CNTRSTACK)",
4064 " && (((trpt->tau&4) && !(trpt->tau&128))",
4065 " || ( (trpt-1)->tau&128)))",
4071 "#if defined(FULLSTACK)",
4072 " printf(\"%%ld: zapping %%u (%%d)\\n\",",
4073 " depth, trpt->ostate,",
4074 " (trpt->ostate)?trpt->ostate->tagged:0);",
4083 " && (((trpt->tau&4) && !(trpt->tau&128))",
4084 " || ( (trpt-1)->tau&128)))",
4090 " printf(\"%%ld: zapping\\n\", depth);",
4094 " if (trpt->proviso)",
4095 " g_store((char *) &now, vsize, 1);",
4101 " if (_n != 0", /* we made a move */
4103 " /* --after-- a program-step, i.e., */",
4104 " /* after backtracking a claim-step */",
4105 " && (trpt->tau&4)",
4106 " /* with at least one running process */",
4107 " /* unless in a stuttered accept state */",
4108 " && ((now._nr_pr > 1) || (trpt->o_pm&2))",
4110 " && !(now._a_t&1))", /* not in 2nd DFS */
4113 " if (fairness)", /* implies a_cycles */
4116 " cpu_printf(\"Consider check %%d %%d...\\n\",",
4117 " now._a_t, now._cnt[0]);",
4120 the a-bit is set, which means that the fairness
4121 counter is running -- it was started in an accepting state.
4122 we check that the counter reached 1, which means that all
4123 processes moved least once.
4124 this means we can start the search for cycles -
4125 to be able to return to this state, we should be able to
4126 run down the counter to 1 again -- which implies a visit to
4127 the accepting state -- even though the Seed state for this
4128 search is itself not necessarily accepting
4130 " if ((now._a_t&2) /* A-bit */",
4131 " && (now._cnt[0] == 1))",
4135 " if (a_cycles && (trpt->o_pm&2))",
4142 "#if NCORE>1 && defined(FULL_TRAIL)",
4144 " { Pop_Stack_Tree();",
4151 "void new_state(void) { /* place holder */ }",
4155 "spin_assert(int a, char *s, int ii, int tt, Trans *t)",
4157 " if (!a && !noasserts)",
4158 " { char bad[1024];",
4159 " strcpy(bad, \"assertion violated \");",
4160 " if (strlen(s) > 1000)",
4161 " { strncpy(&bad[19], (const char *) s, 1000);",
4162 " bad[1019] = '\\0';",
4164 " strcpy(&bad[19], s);",
4168 "#ifndef NOBOUNDCHECK",
4170 "Boundcheck(int x, int y, int a1, int a2, Trans *a3)",
4172 " spin_assert((x >= 0 && x < y), \"- invalid array index\",",
4177 "int do_hashgen = 0;",
4182 " printf(\"%%9.8g states, stored (%%g visited)\\n\",",
4183 " nstates - nShadow, nstates);",
4185 " printf(\"%%9.8g states, stored\\n\", nstates);",
4187 " if (bfs_punt > 0)",
4188 " printf(\"%%9.8g states lost (lack of queue memory)\\n\", (double) bfs_punt);",
4192 " printf(\" %%8g nominal states (- rv and atomic)\\n\", nstates-midrv-nlinks+revrv);",
4193 " printf(\" %%8g rvs succeeded\\n\", midrv-failedrv);",
4195 " printf(\" %%8g nominal states (stored-atomic)\\n\", nstates-nlinks);",
4198 " printf(\" %%8g midrv\\n\", midrv);",
4199 " printf(\" %%8g failedrv\\n\", failedrv);",
4200 " printf(\" %%8g revrv\\n\", revrv);",
4203 " printf(\"%%9.8g states, matched\\n\", truncs);",
4205 " printf(\"%%9.8g matches within stack\\n\",truncs2);",
4208 " printf(\"%%9.8g transitions (= visited+matched)\\n\",",
4209 " nstates+truncs);",
4211 " printf(\"%%9.8g transitions (= stored+matched)\\n\",",
4212 " nstates+truncs);",
4213 " printf(\"%%9.8g atomic steps\\n\", nlinks);",
4214 " if (nlost) printf(\"%%g lost messages\\n\", (double) nlost);",
4218 " printf(\"hash conflicts: %%9.8g (resolved)\\n\", hcmp);",
4219 " #if !defined(AUTO_RESIZE) && !defined(BFS_PAR)",
4220 " if (hcmp > (double) (1<<ssize))",
4221 " { printf(\"hint: increase hashtable-size (-w) to reduce runtime\\n\");",
4224 " #if defined(BFS_PAR) && defined(HC)",
4225 " { double fp = (100. * (double) nstates)/((double) ((ulong) (1<<ssize)));",
4227 " printf(\"the hash table is %%3.3g %%%% filled\", fp);",
4229 " { fp = 100. / fp;",
4230 " while (fp > 2.) { fi++; fp /= 2.; }",
4232 " { printf(\" (hint: rerun with -w%%d to reduce runtime)\",",
4235 " printf(\"\\n\");",
4241 " printf(\"%%8g states allocated for dfs stack\\n\", ngrabs);",
4244 " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
4245 " (double)(((double) udmem) * 8.0) / (double) nstates);",
4247 " printf(\"\\nhash factor: %%4g (best if > 100.)\\n\\n\",",
4248 " ((double)(((ulong)1)<<(ssize-10)) / (double) nstates) * 1024.0);",
4249 /* the -10 and *1024 stuff is to avoid overflow */
4250 " printf(\"bits set per state: %%u (-k%%u)\\n\", hfns, hfns);",
4252 " printf(\"hash polynomial used: 0x%%.8x\\n\", HASH_CONST[HASH_NR]);",
4253 " if (s_rand != 12345)",
4254 " printf(\"random seed used: %%u\\n\", (uint) (s_rand-1));",
4256 "#if defined(BFS_DISK) && !defined(BFS_PAR)",
4257 " printf(\"bfs disk reads: %%ld writes %%ld -- diff %%ld\\n\",",
4258 " bfs_dsk_reads, bfs_dsk_writes, bfs_dsk_writes-bfs_dsk_reads);",
4259 " if (bfs_dsk_read >= 0) (void) close(bfs_dsk_read);",
4260 " if (bfs_dsk_write >= 0) (void) close(bfs_dsk_write);",
4261 " (void) unlink(\"pan_bfs_dsk.tmp\");",
4267 "{ double nr1, nr2, nr3 = 0.0, nr4, nr5 = 0.0;",
4269 " if (who_am_i != 0)",
4274 " if (verbose) cpu_printf(\"wrapup -- %%d error(s)\\n\", errors);",
4275 " if (core_id != 0)",
4278 " void dsk_stats(void);",
4281 " if (search_terminated != NULL)",
4282 " { *search_terminated |= 2; /* wrapup */",
4284 " exit(0); /* normal termination, not an error */",
4287 "#if !defined(WIN32) && !defined(WIN64)",
4288 " signal(SIGINT, SIG_DFL);",
4290 " printf(\"\\n(%%s)\\n\", SpinVersion);",
4291 " if (!done) printf(\"Warning: Search not completed\\n\");",
4292 "#if defined(BFS_PAR) && !defined(BITSTATE)",
4293 " if (bfs_punt > 0) printf(\"Warning: Search incomplete\\n\");",
4296 " (void) unlink((const char *)stackfile);",
4299 " printf(\" + Multi-Core (using %%d cores)\\n\", Cores);",
4300 " #ifdef BFS_SEP_HASH",
4301 " printf(\" + Separate Hash Tables\\n\");",
4304 " printf(\" + Disk storage\\n\");",
4309 " { printf(\" + Multi-Core (NCORE=%%d)\\n\", NCORE);",
4311 " { printf(\" + Multi-Core (NCORE=%%d -z%%ld)\\n\", NCORE, z_handoff);",
4315 " printf(\" + Breadth-First Search\\n\");",
4318 " printf(\" + Partial Order Reduction\\n\");",
4321 " printf(\" + Process Scheduling Permutation\\n\");",
4324 " printf(\" + Reverse Depth-First Search Order\\n\");",
4327 " printf(\" + Reverse Transition Ordering\\n\");",
4329 " printf(\" + Randomized Transition Ordering\\n\");",
4332 " printf(\" + Randomized Process Ordering\\n\");",
4335 " printf(\" + Scheduling Restriction (-L%%d)\\n\", sched_max);",
4338 " printf(\" + Tree Index Compression\\n\");",
4341 " printf(\" + Compression\\n\");",
4344 " printf(\" + Graph Encoding (-DMA=%%d)\\n\", MA);",
4346 " printf(\" Restarted from checkpoint %%s.xpt\\n\", PanSource);",
4350 " #ifdef FULLSTACK",
4351 " printf(\" + FullStack Matching\\n\");",
4353 " #ifdef CNTRSTACK",
4354 " printf(\" + CntrStack Matching\\n\");",
4358 " if (reversing & 2)",
4359 " { if (p_reorder == set_permuted)",
4360 " { printf(\" + Permuted\\n\");",
4362 " if (p_reorder == set_reversed)",
4363 " { printf(\" + Reversed\\n\");",
4365 " if (p_reorder == set_rotated)",
4366 " { printf(\" + Rotated %%d\\n\", p_rotate);",
4368 " if (p_reorder == set_randrot)",
4369 " { printf(\" + RandRotated\\n\");",
4373 " printf(\"\\nBit statespace search for:\\n\");",
4376 " printf(\"\\nHash-Compact %%d search for:\\n\", HC);",
4378 " printf(\"\\nFull statespace search for:\\n\");",
4381 "#ifdef EVENT_TRACE",
4382 "#ifdef NEGATED_TRACE",
4383 " printf(\"\tnotrace assertion \t+\\n\");",
4385 " printf(\"\ttrace assertion \t+\\n\");",
4389 " printf(\"\tnever claim \t+\");",
4390 " printf(\" (%%s)\\n\", procname[((Pclaim *)pptr(0))->_t]);",
4391 " printf(\"\tassertion violations\t\");",
4393 " printf(\"- (disabled by -A flag)\\n\");",
4395 " printf(\"+ (if within scope of claim)\\n\");",
4398 " printf(\"\tnever claim \t- (not selected)\\n\");",
4400 " printf(\"\tnever claim \t- (none specified)\\n\");",
4402 " printf(\"\tassertion violations\t\");",
4404 " printf(\"- (disabled by -A flag)\\n\");",
4406 " printf(\"+\\n\");",
4410 " printf(\"\tnon-progress cycles \t\");",
4412 " printf(\"\tacceptance cycles \t\");",
4415 " printf(\"+ (fairness %%sabled)\\n\",",
4416 " fairness?\"en\":\"dis\");",
4417 " else printf(\"- (not selected)\\n\");",
4419 " #if !defined(BFS_PAR) || !defined(L_BOUND)",
4420 " printf(\"\tcycle checks \t- (disabled by -DSAFETY)\\n\");",
4422 " printf(\"\tcycle checks \t+ (bound %%d)\\n\", L_bound);",
4426 " printf(\"\tinvalid end states\t- \");",
4427 " printf(\"(disabled by \");",
4429 " printf(\"-E flag)\\n\\n\");",
4431 " printf(\"never claim)\\n\\n\");",
4433 " printf(\"\tinvalid end states\t\");",
4435 " printf(\"- (disabled by -E flag)\\n\\n\");",
4437 " printf(\"+\\n\\n\");",
4439 " printf(\"State-vector %%d byte, depth reached %%ld\", hmax,",
4441 " (nr_handoffs * z_handoff) +",
4444 " printf(\", errors: %%d\\n\", errors);",
4448 " { extern void dfa_stats(void);",
4449 " if (maxgs+a_cycles+2 < MA)",
4450 " printf(\"MA stats: -DMA=%%d is sufficient\\n\",",
4451 " maxgs+a_cycles+2);",
4457 " printf(\"stackframes: %%d/%%d\\n\\n\", smax, svmax);",
4458 " printf(\"stats: fa %%ld, fh %%ld, zh %%ld, zn %%ld - \",",
4459 " Fa, Fh, Zh, Zn);",
4460 " printf(\"check %%ld holds %%ld\\n\", Ccheck, Cholds);",
4461 " printf(\"stack stats: puts %%ld, probes %%ld, zaps %%ld\\n\",",
4462 " PUT, PROBE, ZAPS);",
4464 " printf(\"\\n\");",
4467 "#if !defined(BITSTATE) && defined(NOCOMP)",
4468 " if (!verbose) { goto jump_here; }", /* added 5.2.0 */
4471 "#if 1", /* omitted 5.2.0: defined(BITSTATE) || !defined(NOCOMP) */
4472 " nr1 = (nstates-nShadow)*",
4473 " (double)(hmax+sizeof(H_el)-sizeof(unsigned));",
4477 " nr2 = (double) ((maxdepth+3)*sizeof(Trail));",
4480 " #ifndef BITSTATE",
4481 "#if !defined(MA) || defined(COLLAPSE)",
4482 " nr3 = (double) (ONE_L<<ssize)*sizeof(H_el *);",
4486 " nr3 = (double) (udmem);",
4488 " nr3 = (double) (ONE_L<<(ssize-3));",
4490 " nr5 = (double) (ONE_L<<(ssize-3));",
4493 " nr5 = (double) (maxdepth*sizeof(H_el *));",
4497 " nr4 = (double) (svmax * (sizeof(Svtack) + hmax))",
4498 " + (double) (smax * (sizeof(_Stack) + Maxbody * sizeof(char)));",
4500 " if (1 /* verbose || memcnt < nr1+nr2+nr3+nr4+nr5 */)",
4502 " { double remainder = memcnt;",
4503 " double tmp_nr = memcnt-nr3-nr4-(nr2-fragment)-nr5;",
4505 " #if NCORE>1 && !defined(SEP_STATE)",
4506 " tmp_nr -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
4508 " if (tmp_nr < 0.0) tmp_nr = 0.;",
4509 " printf(\"Stats on memory usage (in Megabytes):\\n\");",
4510 " printf(\"%%9.3f\tequivalent memory usage for states\",",
4511 " nr1/1048576.); /* 1024*1024=1048576 */",
4512 " printf(\" (stored*(State-vector + overhead))\\n\");",
4513 " #if NCORE>1 && !defined(WIN32) && !defined(WIN64)",
4514 " printf(\"%%9.3f\tshared memory reserved for state storage\\n\",",
4515 " mem_reserved/1048576.);",
4517 " printf(\"\t\tin %%d local heaps of %%7.3f MB each\\n\",",
4518 " NCORE, mem_reserved/(NCORE*1048576.));",
4520 " printf(\"\\n\");",
4524 " printf(\"%%9.3f\tmemory used for hash array (-M%%ld)\\n\",",
4525 " nr3/1048576., udmem/(1024L*1024L));",
4527 " printf(\"%%9.3f\tmemory used for hash array (-w%%d)\\n\",",
4528 " nr3/1048576., ssize);",
4530 " printf(\"%%9.3f\tmemory used for bit stack\\n\",",
4532 " remainder = remainder - nr3 - nr5;",
4535 " printf(\"%%9.3f\tactual memory usage for states\",",
4536 " tmp_nr/1048576.);",
4537 " remainder -= tmp_nr;",
4538 " if (tmp_nr > 0.)",
4539 " { if (tmp_nr < nr1) ",
4540 " { printf(\" (compression: %%.2f%%%%)\\n\",",
4541 " (100.0*tmp_nr)/nr1);",
4543 " { printf(\"\\n\");",
4546 " { printf(\" (less than 1k)\\n\");",
4549 " if (tmp_nr > 0. && tmp_nr < nr1)",
4550 " { printf(\" \tstate-vector as stored = %%.0f byte\",",
4551 " (tmp_nr)/(nstates-nShadow) -",
4552 " (double) (sizeof(H_el) - sizeof(unsigned)));",
4553 " printf(\" + %%ld byte overhead\\n\",",
4554 " (long int) sizeof(H_el)-sizeof(unsigned));",
4558 " #if !defined(MA) || defined(COLLAPSE)",
4560 " printf(\"%%9.3f\tshared memory used for hash table (-w%%d)\\n\",",
4561 " ((double) bfs_pre_allocated)/1048576., ssize);",
4563 " printf(\"%%9.3f\tmemory used for hash table (-w%%d)\\n\",",
4564 " nr3/1048576., ssize);",
4565 " remainder -= nr3;",
4570 " printf(\"%%9.3f\tmemory used for DFS stack (-m%%ld)\\n\",",
4571 " nr2/1048576., maxdepth);",
4572 " remainder -= nr2;",
4575 " remainder -= ((double) NCORE * LWQ_SIZE) + GWQ_SIZE;",
4576 " printf(\"%%9.3f\tshared memory used for work-queues\\n\",",
4577 " (GWQ_SIZE + (double) NCORE * LWQ_SIZE) /1048576.);",
4578 " printf(\"\t\tin %%d queues of %%7.3f MB each\",",
4579 " NCORE, (double) LWQ_SIZE /1048576.);",
4581 " printf(\" + a global q of %%7.3f MB\\n\",",
4582 " (double) GWQ_SIZE / 1048576.);",
4584 " printf(\"\\n\");",
4587 " if (remainder - fragment > 1048576.)",
4588 " { printf(\"%%9.3f\tother (proc and chan stacks)\\n\",",
4589 " (remainder-fragment)/1048576.);",
4591 " if (fragment > 1048576.)",
4592 " { printf(\"%%9.3f\tmemory lost to fragmentation\\n\",",
4593 " fragment/1048576.);",
4596 " printf(\"%%9.3f\ttotal non-shared memory usage\\n\\n\",",
4597 " memcnt/1048576.);",
4599 " printf(\"%%9.3f\ttotal actual memory usage\\n\\n\",",
4600 " memcnt/1048576.);",
4608 "#if !defined(BITSTATE) && defined(NOCOMP)",
4612 " printf(\"%%9.3f\tmemory usage (Mbyte)\\n\",",
4613 " memcnt/1048576.);",
4616 " bfs_report_mem();",
4618 " printf(\"\\n\");",
4621 " printf(\"nr of templates: [ 0:globals 1:chans 2:procs ]\\n\");",
4622 " printf(\"collapse counts: [ \");",
4623 " { int i; for (i = 0; i < 256+2; i++)",
4624 " if (ncomps[i] != 0)",
4625 " printf(\"%%d:%%lu \", i, ncomps[i]);",
4626 " printf(\"]\\n\");",
4632 " printf(\"TRIX counts:\\n\");",
4633 " printf(\" processes: \");",
4634 " for (i = 0; i < MAXPROC; i++)",
4635 " if (_p_count[i] != 0)",
4636 " { printf(\"%%3d:%%ld \",",
4637 " i, _p_count[i]);",
4639 " printf(\"\\n channels : \");",
4640 " for (i = 0; i < MAXQ; i++)",
4641 " if (_c_count[i] != 0)",
4642 " { printf(\"%%3d:%%ld \",",
4643 " i, _c_count[i]);",
4645 " printf(\"\\n\\n\");",
4649 " if ((done || verbose) && !no_rck) do_reach();",
4652 " printf(\"\\nPeg Counts (transitions executed):\\n\");",
4653 " for (i = 1; i < NTRANS; i++)",
4654 " { if (peg[i]) putpeg(i, peg[i]);",
4657 "#ifdef VAR_RANGES",
4661 " if (vprefix > 0) close(svfd);",
4664 " printf(\"%%g loopstates hit\\n\", cnt_loops);",
4669 "#if NCORE>1 && defined(T_ALERT)",
4680 " bfs_shutdown(\"interrupted\");",
4682 " printf(\"Interrupted\\n\");",
4684 " was_interrupted = 1;",
4691 " * super fast hash, based on Paul Hsieh's function",
4692 " * http://www.azillionmonkeys.com/qed/hash.html",
4694 "#include <stdint.h>", /* for uint32_t etc */
4695 " #undef get16bits",
4696 " #if defined(__GNUC__) && defined(__i386__)",
4697 " #define get16bits(d) (*((const uint16_t *) (d)))",
4699 " #define get16bits(d) ((((uint32_t)(((const uint8_t *)(d))[1])) << 8)\\",
4700 " +(uint32_t)(((const uint8_t *)(d))[0]) )",
4704 "d_sfh(uchar *s, int len)", /* sets one 32-bit number, in K1 */
4705 "{ uint32_t h = len, tmp;",
4711 " for ( ; len > 0; len--)",
4712 " { h += get16bits(s);",
4713 " tmp = (get16bits(s+2) << 11) ^ h;",
4714 " h = (h << 16) ^ tmp;",
4715 " s += 2*sizeof(uint16_t);",
4719 " case 3: h += get16bits(s);",
4721 " h ^= s[sizeof(uint16_t)] << 18;",
4724 " case 2: h += get16bits(s);",
4728 " case 1: h += *s;",
4744 "/* 64-bit Jenkins hash, 1997",
4745 " * http://burtleburtle.net/bob/c/lookup8.c",
4747 "#define mix(a,b,c) \\",
4748 "{ a -= b; a -= c; a ^= (c>>43); \\",
4749 " b -= c; b -= a; b ^= (a<<9); \\",
4750 " c -= a; c -= b; c ^= (b>>8); \\",
4751 " a -= b; a -= c; a ^= (c>>38); \\",
4752 " b -= c; b -= a; b ^= (a<<23); \\",
4753 " c -= a; c -= b; c ^= (b>>5); \\",
4754 " a -= b; a -= c; a ^= (c>>35); \\",
4755 " b -= c; b -= a; b ^= (a<<49); \\",
4756 " c -= a; c -= b; c ^= (b>>11); \\",
4757 " a -= b; a -= c; a ^= (c>>12); \\",
4758 " b -= c; b -= a; b ^= (a<<18); \\",
4759 " c -= a; c -= b; c ^= (b>>22); \\",
4762 "/* 32-bit Jenkins hash, 2006",
4763 " * http://burtleburtle.net/bob/c/lookup3.c",
4765 "#define rot(x,k) (((x)<<(k))|((x)>>(32-(k))))",
4767 "#define mix(a,b,c) \\",
4768 "{ a -= c; a ^= rot(c, 4); c += b; \\",
4769 " b -= a; b ^= rot(a, 6); a += c; \\",
4770 " c -= b; c ^= rot(b, 8); b += a; \\",
4771 " a -= c; a ^= rot(c,16); c += b; \\",
4772 " b -= a; b ^= rot(a,19); a += c; \\",
4773 " c -= b; c ^= rot(b, 4); b += a; \\",
4776 "#define final(a,b,c) \\",
4777 "{ c ^= b; c -= rot(b,14); \\",
4778 " a ^= c; a -= rot(c,11); \\",
4779 " b ^= a; b -= rot(a,25); \\",
4780 " c ^= b; c -= rot(b,16); \\",
4781 " a ^= c; a -= rot(c,4); \\",
4782 " b ^= a; b -= rot(a,14); \\",
4783 " c ^= b; c -= rot(b,24); \\",
4788 "d_hash(uchar *kb, int nbytes)", /* sets two 64-bit or 32-bit nrs, depending on WS */
4791 " uint64_t a = 0, b, c, n;",
4792 " const uint64_t *k = (uint64_t *) kb;",
4794 " uint32_t a = 0, b, c, n;",
4795 " const uint32_t *k = (uint32_t *) kb;",
4797 " n = nbytes/WS; /* nr of words */",
4798 " /* extend to multiple of words, if needed */",
4799 " a = WS - (nbytes %% WS);",
4800 " if (a > 0 && a < WS)",
4802 " bp = kb + nbytes;",
4805 " case 7: *bp++ = 0; /* fall thru */",
4806 " case 6: *bp++ = 0; /* fall thru */",
4807 " case 5: *bp++ = 0; /* fall thru */",
4808 " case 4: *bp++ = 0; /* fall thru */",
4810 " case 3: *bp++ = 0; /* fall thru */",
4811 " case 2: *bp++ = 0; /* fall thru */",
4812 " case 1: *bp = 0;",
4816 " b = HASH_CONST[HASH_NR];",
4817 " c = 0x9e3779b97f4a7c13LL; /* arbitrary value */",
4826 " c += (((uint64_t) nbytes)<<3);",
4828 " case 2: b += k[1];",
4829 " case 1: a += k[0];",
4833 "#else", /* 32 bit version: */
4834 " a = c = 0xdeadbeef + (n<<2);",
4835 " b = HASH_CONST[HASH_NR];",
4845 " case 3: c += k[2];",
4846 " case 2: b += k[1];",
4847 " case 1: a += k[0];",
4852 " j1_spin = c&nmask; j3_spin = a&7; /* 1st bit */",
4853 " j2_spin = b&nmask; j4_spin = (a>>3)&7; /* 2nd bit */",
4857 "#if defined(MURMUR) && (WS==8)",
4858 "/* public-domain, 64-bit MurmurHash3, by Austin Appleby */",
4859 "/* https://code.google.com/p/smhasher/wiki/MurmurHash3 */",
4861 "m_hash(uchar *v, int len)",
4862 "{ uint8_t *bp, *data = (uint8_t*) v;",
4863 " int i, nblocks = len / 16;",
4865 " uint64_t h1 = HASH_CONST[HASH_NR];",
4866 " uint64_t h2 = 0x9e3779b97f4a7c13LL;",
4868 " uint64_t c1 = 0x87c37b91114253d5;",
4869 " uint64_t c2 = 0x4cf5ad432745937f;",
4871 " uint64_t *blocks = (uint64_t *)(data);",
4873 " /* guarantee a multiple of 16 bytes */",
4874 " i = 16 - (len %% 16);",
4875 " if (i > 0 && i < 16)",
4879 " case 15: *bp++ = 0; /* fall thru */",
4880 " case 14: *bp++ = 0;",
4881 " case 13: *bp++ = 0;",
4882 " case 12: *bp++ = 0;",
4883 " case 11: *bp++ = 0;",
4884 " case 10: *bp++ = 0;",
4885 " case 9: *bp++ = 0;",
4886 " case 8: *bp++ = 0;",
4887 " case 7: *bp++ = 0;",
4888 " case 6: *bp++ = 0;",
4889 " case 5: *bp++ = 0;",
4890 " case 4: *bp++ = 0;",
4891 " case 3: *bp++ = 0;",
4892 " case 2: *bp++ = 0;",
4893 " case 1: *bp = 0;",
4897 " for (i = 0; i < nblocks; i++)",
4898 " { uint64_t k1 = blocks[i*2];",
4899 " uint64_t k2 = blocks[i*2+1];",
4902 " k1 = (k1 << 31) | (k1 >> 33);",
4906 " h1 = (h1 << 27) | (h1 >> 37);",
4908 " h1 = h1 * 5 + 0x52dce729;",
4911 " k2 = (k2 << 33) | (k2 >> 31);",
4915 " h2 = (h2 << 31) | (h2 >> 33);",
4917 " h2 = h2 * 5 + 0x38495ab5;",
4920 " uint8_t *tail = (uint8_t*)(data + (nblocks * 16));",
4922 " uint64_t k1 = 0;",
4923 " uint64_t k2 = 0;",
4925 " switch(len & 15) {",
4926 " case 15: k2 ^= ((uint64_t) tail[14]) << 48; break;",
4927 " case 14: k2 ^= ((uint64_t) tail[13]) << 40; break;",
4928 " case 13: k2 ^= ((uint64_t) tail[12]) << 32; break;",
4929 " case 12: k2 ^= ((uint64_t) tail[11]) << 24; break;",
4930 " case 11: k2 ^= ((uint64_t) tail[10]) << 16; break;",
4931 " case 10: k2 ^= ((uint64_t) tail[ 9]) << 8; break;",
4932 " case 9: k2 ^= ((uint64_t) tail[ 8]) << 0; break;",
4934 " k2 = (k2 << 33) | (k2 >> 31);",
4936 " h2 ^= k2; break;",
4937 " case 8: k1 ^= ((uint64_t) tail[7]) << 56; break;",
4938 " case 7: k1 ^= ((uint64_t) tail[6]) << 48; break;",
4939 " case 6: k1 ^= ((uint64_t) tail[5]) << 40; break;",
4940 " case 5: k1 ^= ((uint64_t) tail[4]) << 32; break;",
4941 " case 4: k1 ^= ((uint64_t) tail[3]) << 24; break;",
4942 " case 3: k1 ^= ((uint64_t) tail[2]) << 16; break;",
4943 " case 2: k1 ^= ((uint64_t) tail[1]) << 8; break;",
4944 " case 1: k1 ^= ((uint64_t) tail[0]) << 0; break;",
4946 " k1 = (k1 << 31) | (k1 >> 33);",
4951 " h1 ^= len; h2 ^= len;",
4955 " h1 *= 0xff51afd7ed558ccd;",
4957 " h1 *= 0xc4ceb9fe1a85ec53;",
4960 " h2 *= 0xff51afd7ed558ccd;",
4962 " h2 *= 0xc4ceb9fe1a85ec53;",
4967 " j1_spin = h1&nmask; j3_spin = (h1>>48)&7;",
4968 " j2_spin = h2&nmask; j4_spin = (h2>>48)&7;",
4969 " K1 = h1; K2 = h2;",
4974 "s_hash(uchar *cp, int om)", /* uses either d_sfh (1x32bit), or d_hash (2x64bit) */
4975 "{", /* depending on ssize ie the -w parameter */
4976 " hasher(cp, om); /* sets K1 */",
4978 " if (S_Tab == H_tab)", /* state stack in bitstate search */
4979 " j1_spin = K1 %% omaxdepth;",
4982 " if (ssize < 8*WS)",
4983 " j1_spin = K1&mask;",
4992 " srand(s_rand+HASH_NR);", /* inirand */
4993 " prerand = (int *) emalloc((omaxdepth+3)*sizeof(int));",
4994 " for (i = 0; i < omaxdepth+3; i++)",
4995 " { prerand[i] = rand();",
5000 "{ if (!prerand) inirand();",
5001 " return prerand[depth];",
5008 " if (WS == 4 && ssize >= 32)",
5009 " { mask = 0xffffffff;",
5011 " switch (ssize) {",
5012 " case 34: nmask = (mask>>1); break;",
5013 " case 33: nmask = (mask>>2); break;",
5014 " default: nmask = (mask>>3); break;",
5019 " } else if (WS == 8)",
5020 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
5022 " nmask = mask>>3;",
5026 " } else if (WS != 4)",
5027 " { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", (long int) WS);",
5029 " } else /* WS == 4 and ssize < 32 */",
5030 " { mask = ((ONE_L<<ssize)-1); /* hash init */",
5031 " nmask = (mask>>3);",
5035 "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
5037 " #error cannot combine AUTO_RESIZE with NCORE>1",
5039 "static long reclaim_size;",
5040 "static char *reclaim_mem;",
5041 "static H_el **N_tab;",
5043 "reverse_capture(H_el *p)",
5044 "{ if (!p) return;",
5045 " reverse_capture(p->nxt);",
5046 " /* last element of list moves first */",
5047 " /* to preserve list-order */",
5048 " j2_spin = p->m_K1;",
5049 " if (ssize < 8*WS) /* probably always true */",
5050 " { j2_spin &= mask;",
5052 " p->nxt = N_tab[j2_spin];",
5053 " N_tab[j2_spin] = p;",
5056 "resize_hashtable(void)",
5058 "#ifndef BFS_PAR", /* ssize and mask/nmask are not in shared mem */
5059 " if (WS == 4 && ssize >= 27 - 1)",
5061 " { return; /* cannot increase further */",
5064 " ssize += 2; /* 4x size @htable ssize */",
5066 " printf(\"pan: resizing hashtable to -w%%d.. \", ssize);",
5068 " N_tab = (H_el **) emalloc((ONE_L<<ssize)*sizeof(H_el *));",
5069 " set_masks(); /* they changed */",
5071 " for (j1_spin = 0; j1_spin < (ONE_L << (ssize - 2)); j1_spin++)",
5072 " { reverse_capture(H_tab[j1_spin]);",
5074 " reclaim_mem = (char *) H_tab;",
5075 " reclaim_size = (ONE_L << (ssize - 2));",
5078 " printf(\" done\\n\");",
5081 "#if defined(ZAPH) && defined(BITSTATE)",
5083 "zap_hashtable(void)",
5084 "{ cpu_printf(\"pan: resetting hashtable\\n\");",
5086 " { memset(SS, 0, udmem);",
5088 " { memset(SS, 0, ONE_L<<(ssize-3));",
5095 "find_claim(char *s)",
5097 " for (i = 0; strncmp(procname[i], \":np_:\", 5) != 0; i++)",
5098 " { if (strcmp(s, procname[i]) == 0)",
5099 " { for (j = 0; j < NCLAIMS; j++)",
5100 " { if (spin_c_typ[j] == i)",
5105 " printf(\"pan: error: cannot find claim '%%s'\\n\", s);",
5107 " return -1; /* unreachable */",
5111 "#if defined(BFS_PAR) && defined(BFS_SEP_HASH)",
5112 "int /* to avoid having to include <math.h> and compile with -lm */",
5113 "blog2(int n) /* n >= 1 */",
5115 " if (n == 1) { return 0; }",
5116 " if (n == 2) { return 1; }",
5117 " while (n > r) { m++; r *= 2; }",
5125 "mul(uint a, uint b, uint p)",
5133 " if (b & 0x80000000)",
5143 "ppow(int n, uint p)",
5144 "{ uint t = 1; int i;",
5145 " for (i = 0; i < 32; i++)",
5146 " { if (n & (1<<i))",
5147 " { t = mul(t, pp[i], p);",
5153 "hashgen(void) /* courtesy Jim Reeds, 1995 */",
5154 "{ uint x, y, p; int i, cnt;",
5155 " int ff[5] = { 3, 5, 17, 257, 65537 };",
5158 " srand(s_rand); /* was: srandom(s_rand) */",
5159 " nn[0] = ff[1]*ff[2]*ff[3]*ff[4];",
5160 " nn[1] = ff[0]*ff[2]*ff[3]*ff[4];",
5161 " nn[2] = ff[0]*ff[1]*ff[3]*ff[4];",
5162 " nn[3] = ff[0]*ff[1]*ff[2]*ff[4];",
5163 " nn[4] = ff[0]*ff[1]*ff[2]*ff[3];",
5164 " for (cnt = 0; cnt < 5000; cnt++)",
5166 " p = ((rand()<<13)^rand()) | 1; /* used random() before */",
5168 " for (i = 0; i < 32; i++)",
5169 " { pp[i+1] = mul(pp[i], pp[i], p);",
5171 " if (pp[32] == x)",
5172 " { for (i = 0; i < 5; i++)",
5173 " { y = ppow(nn[i], p);",
5178 " { HASH_CONST[0] = p;", /* 32 bit */
5180 " { printf(\"polynomial: 0x%%.8x (%%d tries)\\n\",",
5183 " return;", /* success */
5185 " fprintf(efd, \"pan: could not find a polynomial in %%d tries\\n\", cnt);",
5186 " fprintf(efd, \"pan: try a different seed with -RSn\\n\");",
5191 "main(int argc, char *argv[])",
5192 "{ void to_compile(void);\n",
5193 " efd = stderr; /* default */",
5194 "#if defined(BFS_PAR) && defined(BFS_SEP_HASH)",
5195 " uchar used_w = 0;",
5197 " if (G_long != sizeof(long)",
5198 " || G_int != sizeof(int))",
5199 " { printf(\"spin: error, the version of spin \");",
5200 " printf(\"that generated this pan.c assumed a different \");",
5201 " printf(\"wordsize (%%d iso %%d)\\n\", G_long, (int) sizeof(long));",
5205 "#if defined(T_RAND) && (T_RAND>0)",
5206 " s_rand = T_RAND;", /* so that -RS can override */
5207 "#elif defined(P_RAND) && (P_RAND>0)",
5208 " s_rand = P_RAND;",
5212 " { char *ptr = strrchr(argv[0], '/');",
5213 " if (ptr == NULL)",
5214 " { ptr = argv[0];",
5218 " progname = emalloc(strlen(ptr));",
5219 " strcpy(progname, ptr);",
5220 " /* printf(\"progname: %%s\\n\", progname); */",
5225 " b_store = bstore_reg; /* default */",
5229 " strcpy(o_cmdline, \"\");",
5230 " for (j = 1; j < argc; j++)",
5231 " { strcat(o_cmdline, argv[j]);",
5232 " strcat(o_cmdline, \" \");",
5234 " /* printf(\"Command Line: %%s\\n\", o_cmdline); */",
5235 " if (strlen(o_cmdline) >= sizeof(o_cmdline))",
5236 " { Uerror(\"option list too long\");",
5239 " while (argc > 1 && argv[1][0] == '-')",
5240 " { switch (argv[1][1]) {",
5243 " case 'a': fprintf(efd, \"warning: -a is disabled by -DNP, ignored\");",
5246 " case 'a': a_cycles = 1; break;",
5249 " #if defined(BFS_PAR) && defined(L_BOUND)",
5250 " case 'a': if (isdigit(argv[1][2]))",
5251 " { L_bound = atoi(&argv[1][2]);",
5252 " if (L_bound < 1 || L_bound > 255)",
5253 " { printf(\"usage: -aN with 0<N<256\\n\");",
5259 " case 'A': noasserts = 1; break;",
5260 " case 'b': bounded = 1; break;",
5263 " case 'C': coltrace = 1; goto samething;",
5266 " case 'c': upto = atoi(&argv[1][2]); break;",
5267 " case 'D': dodot++; state_tables++; break;",
5268 " case 'd': state_tables++; break;",
5269 " case 'e': every_error = 1; upto = 0; Nr_Trails = 1; break;",
5270 " case 'E': noends = 1; break;",
5272 " case 'F': if (strlen(argv[1]) > 2)",
5273 " stackfile = &argv[1][2];",
5276 "#if !defined(SAFETY) && !defined(NOFAIR)",
5277 " case 'f': fairness = 1; break;",
5281 " case 'g': gui = 1; goto samething;",
5285 " if (strncmp(&argv[1][1], \"hash\", strlen(\"hash\")) == 0)",
5286 " { do_hashgen = 1;",
5289 " if (!argv[1][2] || !isdigit((int) argv[1][2]))",
5290 " { usage(efd); /* exits */",
5292 " HASH_NR = atoi(&argv[1][2])%%(sizeof(HASH_CONST)/sizeof(uint));",
5294 " case 'I': iterative = 2; every_error = 1; break;",
5296 " if (strncmp(&argv[1][1], \"i_reverse\", strlen(\"i_reverse\")) == 0)",
5297 " { reversing |= 1;",
5299 " { iterative = 1;",
5300 " every_error = 1;",
5303 " case 'J': like_java = 1; break; /* Klaus Havelund */",
5305 " case 'k': hfns = atoi(&argv[1][2]); break;",
5309 " sched_max = atoi(&argv[1][2]);",
5310 " if (sched_max > 255) /* stored as one byte */",
5311 " { fprintf(efd, \"warning: using max bound (255)\\n\");",
5312 " sched_max = 255;",
5314 " #ifndef NOREDUCE",
5315 " if (sched_max == 0)",
5316 " { fprintf(efd, \"warning: with (default) bound -L0, \");",
5317 " fprintf(efd, \"using -DNOREDUCE performs better\\n\");",
5324 " case 'l': a_cycles = 1; break;",
5326 " case 'l': fprintf(efd, \"error: -l not available (compile with -DNP)\");",
5327 " usage(efd); break;",
5331 " case 'M': udmem = atoi(&argv[1][2]); break;",
5332 " case 'G': udmem = atoi(&argv[1][2]); udmem *= 1024; break;",
5334 " case 'M': case 'G':",
5335 " fprintf(stderr, \"-M and -G affect only -DBITSTATE\\n\");",
5338 " case 'm': maxdepth = atoi(&argv[1][2]); break;",
5342 " if (isdigit((int)argv[1][2]))",
5343 " { whichclaim = atoi(&argv[1][2]);",
5344 " } else if (isalpha((int)argv[1][2]))",
5345 " { claimname = &argv[1][2];",
5346 " } else if (argc > 2 && argv[2][0] != '-') /* check next arg */",
5347 " { claimname = argv[2];",
5348 " argc--; argv++; /* skip next arg */",
5352 " fprintf(stderr, \"warning: only one claim defined, -N ignored\\n\");",
5354 " fprintf(stderr, \"warning: no claims defined, -N ignored\\n\");",
5356 " if (!isdigit((int)argv[1][2]) && argc > 2 && argv[2][0] != '-')",
5357 " { argc--; argv++;",
5362 " case 'n': no_rck = 1; break;",
5366 " && isdigit((int) argv[1][2]))", /* was argv[1][2] == '_' */
5367 " { int x = atoi(&argv[1][2]);",
5368 " if (x != 0 && x != 1)",
5369 " { fprintf(efd, \"pan: bad option -P[01], ignored\\n\");",
5372 " { reversing &= ~1;",
5376 " { reversing |= 1;",
5380 " fprintf(efd, \"pan: reversed *active* process creation %%s\\n\",",
5381 " reversing&1?\"on\":\"off\");",
5386 " readtrail = 1; onlyproc = atoi(&argv[1][2]);",
5387 " if (argc > 2 && argv[2][0] != '-') /* check next arg */",
5388 " { trailfilename = argv[2];",
5389 " argc--; argv++; /* skip next arg */",
5392 " fprintf(efd, \"pan: option -P not recognized, ignored\\n\");",
5395 " fprintf(efd, \"pan: option -P not recognized, ignored\\n\");",
5400 " #if !defined(BFS) && !defined(BFS_PAR)",
5402 " if (strncmp(&argv[1][1], \"p_normal\", strlen(\"p_normal\")) == 0)",
5403 " { reversing &= ~2;",
5407 " if (strncmp(&argv[1][1], \"p_permute\", strlen(\"p_permute\")) == 0)",
5408 " { p_reorder = set_permuted;",
5411 " if (strncmp(&argv[1][1], \"p_rotate\", strlen(\"p_rotate\")) == 0)",
5412 " { p_reorder = set_rotated;",
5413 " if (isdigit((int) argv[1][9]))",
5414 " { p_rotate = atoi(&argv[1][9]);",
5420 " if (strncmp(&argv[1][1], \"p_randrot\", strlen(\"p_randrot\")) == 0)",
5421 " { p_reorder = set_randrot;",
5424 " if (strncmp(&argv[1][1], \"p_reverse\", strlen(\"p_reverse\")) == 0)",
5425 " { p_reorder = set_reversed;",
5429 " if (strncmp(&argv[1][1], \"p_permute\", strlen(\"p_permute\")) == 0",
5430 " || strncmp(&argv[1][1], \"p_rotate\", strlen(\"p_rotate\")) == 0",
5431 " || strncmp(&argv[1][1], \"p_randrot\", strlen(\"p_randrot\")) == 0",
5432 " || strncmp(&argv[1][1], \"p_reverse\", strlen(\"p_reverse\")) == 0)",
5433 " { fprintf(efd, \"option %%s required compilation with -DPERMUTED\\n\",",
5440 " vprefix = atoi(&argv[1][2]);",
5442 " fprintf(efd, \"invalid option '%%s' -- ignored\\n\", argv[1]);",
5446 " case 'Q': quota = (double) 60.0 * (double) atoi(&argv[1][2]);",
5448 " freq /= 10.; /* for better resolution */",
5452 " case 'q': strict = 1; break;",
5454 " if (argv[1][2] == 'S') /* e.g., -RS76842 */",
5455 " { s_rand = atoi(&argv[1][3]);", /* RS */
5459 " Nrun = atoi(&argv[1][2]);",
5462 " } else if (Nrun < 1)",
5470 " if (strncmp(&argv[1][1], \"rhash\", strlen(\"rhash\")) == 0)",
5471 " { if (s_rand == 12345) /* default seed */",
5473 "#if defined(WIN32) || defined(WIN64)",
5474 " s_rand = (uint) clock();",
5476 " struct tms dummy_tm;",
5477 " s_rand = (uint) times(&dummy_tm);",
5480 " srand(s_rand++);",
5482 " do_hashgen = 1;", /* + randomize p_rotate, p_reverse, p_permute */
5483 " switch (rand()%%5) {",
5484 " case 0: p_reorder = set_permuted;",
5487 " case 1: p_reorder = set_reversed;",
5490 " /* fully randomize p_rotate: */",
5491 " case 2: p_reorder = set_randrot;",
5494 " /* choose once, then keep p_rotate fixed: */",
5495 " case 3: p_reorder = set_rotated;",
5496 " p_rotate = rand()%%3;",
5499 " default: /* standard search */ break;",
5501 " if (rand()%%2 == 0)",
5502 " { t_reverse = 1;",
5506 " fprintf(efd, \"option -rhash requires compilation with -DPERMUTED\\n\");",
5510 "#if defined(HAS_CODE) && HAS_CODE>0",
5511 "samething: readtrail = 1;",
5512 " if (isdigit((int)argv[1][2]))",
5513 " whichtrail = atoi(&argv[1][2]);",
5514 " else if (argc > 2 && argv[2][0] != '-') /* check next arg */",
5515 " { trailfilename = argv[2];",
5516 " argc--; argv++; /* skip next arg */",
5519 " case 'S': silent = 1; goto samething;",
5521 " fprintf(efd, \"options -r is for models with embedded C code\\n\");",
5525 " if (isdigit((int) argv[1][2]))", /* was argv[1][2] == '_' */
5526 " { t_reverse = atoi(&argv[1][2]);",
5528 " printf(\"pan: reverse transition ordering %%s\\n\",",
5529 " t_reverse?\"on\":\"off\");",
5535 " if (strncmp(&argv[1][1], \"t_reverse\", strlen(\"t_reverse\")) == 0)",
5536 " { t_reverse = 1;",
5538 " }", /* i.e., a trail prefix cannot be '_reverse' */
5540 " { tprefix = &argv[1][2];",
5545 " ncores = atoi(&argv[1][2]);",
5548 " case 'V': start_timer(); printf(\"Generated by %%s\\n\", SpinVersion);",
5549 " to_compile(); pan_exit(2); break;",
5550 " case 'v': verbose++; break;",
5551 " case 'w': ssize = atoi(&argv[1][2]);",
5552 " #if defined(BFS_PAR) && defined(BFS_SEP_HASH)",
5556 " case 'Y': signoff = 1; break;",
5557 " case 'X': efd = stdout; break;",
5558 " case 'x': exclusive = 1; break;",
5560 " /* -B ip is passthru to proxy of remote ip address: */",
5561 " case 'B': argc--; argv++; break;",
5562 " case 'Q': worker_pids[0] = atoi(&argv[1][2]); break;",
5563 " /* -Un means that the nth worker should be instantiated as a proxy */",
5564 " case 'U': proxy_pid = atoi(&argv[1][2]); break;",
5565 " /* -W means this copy is started by a cluster-server as a remote */",
5566 " /* this flag is passed to ./pan_proxy, which interprets it */",
5567 " case 'W': remote_party++; break;",
5568 " case 'Z': core_id = atoi(&argv[1][2]);",
5570 " { printf(\"cpu%%d: pid %%d parent %%d\\n\",",
5571 " core_id, getpid(), worker_pids[0]);",
5574 " case 'z': z_handoff = atoi(&argv[1][2]); break;",
5576 " case 'z': break; /* ignored for single-core */",
5578 " default : fprintf(efd, \"saw option -%%c\\n\",",
5579 " argv[1][1]); usage(efd); break;",
5583 "#if defined(BFS_PAR) && defined(BFS_SEP_HASH)",
5584 " if (used_w == 0)",
5585 " { if (ncores == 0) /* all cores used, by default */",
5586 " { ssize -= blog2(BFS_MAXPROCS - 1);",
5588 " { ssize -= blog2(ncores);",
5592 " { hashgen();", /* placed here so that -RSn can appear after -hash */
5595 " if (fairness && !a_cycles)",
5596 " { fprintf(efd, \"error: -f requires the use of -a or -l\\n\");",
5599 " #if ACCEPT_LAB==0",
5601 " { fprintf(efd, \"warning: no accept labels are defined, \");",
5602 " fprintf(efd, \"so option -a has no effect (ignored)\\n\");",
5609 " uerror = bfs_uerror;",
5610 " Uerror = bfs_Uerror;",
5612 " uerror = dfs_uerror;",
5613 " Uerror = dfs_Uerror;",
5615 " if (ssize <= 32) /* 6.2.0 */",
5616 " { hasher = d_sfh;",
5617 "#if !defined(BITSTATE) && defined(USE_TDH)",
5618 " o_hash = o_hash32;",
5621 " { hasher = d_hash;",
5622 "#if !defined(BITSTATE) && defined(USE_TDH)",
5623 " o_hash = o_hash64;",
5626 " if (iterative && TMODE != 0666)",
5628 " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");",
5630 "#if defined(WIN32) || defined(WIN64)",
5631 " #ifndef _S_IWRITE",
5632 " #define S_IWRITE 0000200 /* write permission, owner */",
5634 " #ifndef _S_IREAD",
5635 " #define S_IREAD 0000400 /* read permission, owner */",
5637 " if (TMODE == 0666)",
5638 " TMODE = S_IWRITE | S_IREAD;",
5640 " TMODE = S_IREAD;",
5643 " store_proxy_pid = proxy_pid; /* for checks in mem_file() and someone_crashed() */",
5644 " if (core_id != 0) { proxy_pid = 0; }",
5645 " #ifndef SEP_STATE",
5646 " if (core_id == 0 && a_cycles)",
5647 " { fprintf(efd, \"hint: this search may be more efficient \");",
5648 " fprintf(efd, \"if pan.c is compiled -DSEP_STATE\\n\");",
5651 " if (z_handoff < 0)",
5652 " { z_handoff = 20; /* conservative default - for non-liveness checks */",
5654 "#if defined(NGQ) || defined(LWQ_FIXED)",
5655 " LWQ_SIZE = (double) (128.*1048576.);",
5657 " LWQ_SIZE = (double) ( z_handoff + 2.) * (double) sizeof(SM_frame);",
5658 /* the added margin of +2 is not really necessary */
5662 " { fprintf(efd, \"warning: the intended nr of cores to be used in liveness mode is 2\\n\");",
5663 " #ifndef SEP_STATE",
5664 " fprintf(efd, \"warning: without -DSEP_STATE there is no guarantee that all liveness violations are found\\n\");",
5666 " }", /* it still works though, the later cores get states from the global q */
5668 " #ifdef HAS_HIDDEN",
5669 " #error cannot use hidden variables when compiling multi-core",
5672 "#if defined(T_RAND) && defined(ELSE_IN_GUARD)",
5673 " #error cannot hide 'else' as guard in d_step, when using -DT_RAND",
5678 " fprintf(efd, \"warning: using -k%%d as minimal usable value\\n\", hfns);",
5681 " omaxdepth = maxdepth;",
5683 " if (WS == 4 && ssize > 34)", /* 32-bit word size */
5685 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
5687 " * -w35 would not work: 35-3 = 32 but 1^31 is the largest",
5688 " * power of 2 that can be represented in an ulong",
5692 " if (WS == 4 && ssize > 27)",
5694 " fprintf(efd, \"warning: using -w%%d as max usable value\\n\", ssize);",
5696 " * for emalloc, the lookup table size multiplies by 4 for the pointers",
5697 " * the largest power of 2 that can be represented in a ulong is 1^31",
5698 " * hence the largest number of lookup table slots is 31-4 = 27",
5704 " hiwater = HHH = maxdepth-10;",
5707 " { stackfile = (char *) emalloc(strlen(PanSource)+4+1);",
5708 " sprintf(stackfile, \"%%s._s_\", PanSource);",
5711 " { fprintf(efd, \"error: cannot use -i or -I with -DSC\\n\");",
5716 "#if (defined(R_XPT) || defined(W_XPT)) && !defined(MA)",
5717 " #warning -DR_XPT and -DW_XPT assume -DMA (ignored)",
5720 " if (iterative && a_cycles)",
5721 " fprintf(efd, \"warning: -i or -I work for safety properties only\\n\");",
5725 " #error -DBFS not compatible with -DSC",
5728 " #error -DBFS not compatible with _last",
5730 " #ifdef HAS_STACK",
5731 " #error cannot use c_track UnMatched with BFS",
5734 " #error -DBFS not compatible with -DBCS",
5737 " #warning -DREACH is redundant when -DBFS is used",
5743 " #error cannot combine -DTRIX and -DBITSTATE",
5746 " #error cannot combine -DTRIX and -DCOLLAPSE",
5749 " #error cannot combine -DTRIX and -DMA",
5751 " #if defined(BFS_PAR) && defined(BFS_SEP_HEAP)",
5752 " #error cannot combined -DBFS_SEP_HEAP with -DTRIX",
5758 " #error cannot combine -DBFS_PAR and -DNP",
5765 " #warning using -DNP overrides -DNOCLAIM",
5772 " #error cannot combine -DBCS and -DP_RAND",
5775 " #error cannot combine -DBCS and -DBFS",
5779 "#if defined(MERGED) && defined(PEG)",
5780 " #error to use -DPEG use: spin -o3 -a",
5782 "#if defined(HC) && !defined(BFS_PAR)",
5784 " #error cannot combine -DHC and -DNOCOMP",
5787 " #error cannot combine -DHC and -DBITSTATE",
5790 "#if defined(SAFETY) && defined(NP)",
5791 " #error cannot combine -DNP and -DBFS or -DSAFETY",
5795 " #error cannot combine -DMA and -DBITSTATE",
5798 " #error usage: -DMA=N with N > 0 and N < VECTORSZ",
5803 " #error cannot combine -DBITSTATE and -DCOLLAPSE",
5806 " #error cannot combine -DCOLLAPSE and -DNOCOMP",
5809 " if (maxdepth <= 0 || ssize <= 1) usage(efd);",
5810 "#if SYNC>0 && !defined(NOREDUCE)",
5811 " if (a_cycles && fairness)",
5812 " { fprintf(efd, \"error: p.o. reduction not compatible with \");",
5813 " fprintf(efd, \"fairness (-f) in models\\n\");",
5814 " fprintf(efd, \" with rendezvous operations: \");",
5815 " fprintf(efd, \"recompile with -DNOREDUCE\\n\");",
5819 "#if defined(REM_VARS) && !defined(NOREDUCE)",
5820 " #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)",
5822 "#if defined(NOCOMP) && !defined(BITSTATE)",
5824 " { fprintf(efd, \"error: use of -DNOCOMP voids -l and -a\\n\");",
5829 " memlim = ((double) MEMLIM) * (double) (1<<20); /* size in Mbyte */",
5832 " #ifdef HAS_PRIORITY",
5833 " #error use of priorities cannot be combined with rendezvous",
5834 " #elif HAS_ENABLED",
5835 " #error use of enabled() cannot be combined with rendezvous",
5839 " #ifdef HAS_PRIORITY",
5840 " #warning use of priorities requires -DNOREDUCE",
5841 " #elif HAS_ENABLED",
5842 " #error use of enabled() requires -DNOREDUCE",
5844 " #ifdef HAS_PCVALUE",
5845 " #error use of pcvalue() requires -DNOREDUCE",
5847 " #ifdef HAS_BADELSE",
5848 " #error use of 'else' combined with i/o stmnts requires -DNOREDUCE",
5850 " #if defined(HAS_LAST) && !defined(BCS)",
5851 " #error use of _last requires -DNOREDUCE",
5855 "#if SYNC>0 && !defined(NOREDUCE)",
5856 " #ifdef HAS_UNLESS",
5857 " fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");",
5858 " fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");",
5859 " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");",
5861 " fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");",
5865 "#if SYNC>0 && defined(BFS)",
5867 " fprintf(efd, \"warning: use of rendezvous with BFS does not preserve all invalid endstates\\n\");",
5869 "#if !defined(REACH) && !defined(BITSTATE)",
5870 " if (iterative != 0 && a_cycles == 0)",
5871 " { fprintf(efd, \"warning: -i and -I need -DREACH to work accurately\\n\");",
5874 "#if defined(BITSTATE) && defined(REACH)",
5875 " #warning -DREACH is voided by -DBITSTATE",
5877 "#if defined(MA) && defined(REACH)",
5878 " #warning -DREACH is voided by -DMA",
5880 "#if defined(FULLSTACK) && defined(CNTRSTACK)",
5881 " #error cannot combine -DFULLSTACK and -DCNTRSTACK",
5883 "#if defined(VERI)",
5884 " #if ACCEPT_LAB>0",
5893 " && !state_tables)",
5894 " { fprintf(efd, \"warning: never claim + accept labels \");",
5895 " fprintf(efd, \"requires -a flag to fully verify\\n\");",
5898 " if (verbose && !state_tables",
5903 " { fprintf(efd, \"warning: verification in BFS mode \");",
5904 " fprintf(efd, \"is restricted to safety properties\\n\");",
5918 " && !state_tables)",
5919 " { fprintf(efd, \"hint: this search is more efficient \");",
5920 " fprintf(efd, \"if pan.c is compiled -DSAFETY\\n\");",
5927 " { if (!fairness)",
5928 " { S_A = 1; /* _a_t */",
5930 " } else /* _a_t and _cnt[NFAIR] */",
5931 " { S_A = (&(now._cnt[0]) - (uchar *) &now) + NFAIR - 2;",
5932 " /* -2 because first two uchars in now are masked */",
5937 " signal(SIGINT, stopped);",
5939 "#if defined(BFS) || defined(BFS_PAR)",
5940 " trail = (Trail *) emalloc(6*sizeof(Trail));",
5943 " trail = (Trail *) emalloc((maxdepth+3)*sizeof(Trail));",
5944 " trail++; /* protect trpt-1 refs at depth 0 */",
5946 " trpt = &trail[0]; /* precaution -- in case uerror is called early */",
5951 " if (vprefix > 0)",
5953 " sprintf(nm, \"%%s.svd\", PanSource);",
5954 " if ((svfd = creat(nm, TMODE)) < 0)",
5955 " { fprintf(efd, \"couldn't create %%s\\n\", nm);",
5960 " srand(s_rand+HASH_NR);", /* main - RANDSTOR */
5962 "#if SYNC>0 && ASYNC==0",
5969 "}", /* end of main() */
5974 " fprintf(fd, \"%%s\\n\", SpinVersion);",
5975 " fprintf(fd, \"Valid Options are:\\n\");",
5978 " fprintf(fd, \"\t-a -> is disabled by -DNP \");",
5979 " fprintf(fd, \"(-DNP compiles for -l only)\\n\");",
5981 " fprintf(fd, \"\t-a find acceptance cycles\\n\");",
5984 " fprintf(fd, \"\t-a,-l,-f -> are disabled by -DSAFETY\\n\");",
5986 " fprintf(fd, \"\t-A ignore assert() violations\\n\");",
5987 " fprintf(fd, \"\t-b consider it an error to exceed the depth-limit\\n\");",
5988 " fprintf(fd, \"\t-cN stop at Nth error \");",
5989 " fprintf(fd, \"(defaults to -c1)\\n\");",
5990 " fprintf(fd, \"\t-D print state tables in dot-format and stop\\n\");",
5991 " fprintf(fd, \"\t-d print state tables and stop\\n\");",
5992 " fprintf(fd, \"\t-e create trails for all errors\\n\");",
5993 " fprintf(fd, \"\t-E ignore invalid end states\\n\");",
5995 " fprintf(fd, \"\t-Ffile use 'file' to store disk-stack\\n\");",
5998 " fprintf(fd, \"\t-f add weak fairness (to -a or -l)\\n\");",
6000 " fprintf(fd, \"\t-hN use different hash-seed N:0..499 (defaults to -h0)\\n\");",
6001 " fprintf(fd, \"\t-hash generate a random hash-polynomial for -h0 (see also -rhash)\\n\");",
6002 " fprintf(fd, \"\t using a seed set with -RSn (default %%u)\\n\", s_rand);",
6003 " fprintf(fd, \"\t-i search for shortest path to error\\n\");",
6004 " fprintf(fd, \"\t-I like -i, but approximate and faster\\n\");",
6005 " fprintf(fd, \"\t-J reverse eval order of nested unlesses\\n\");",
6007 " fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
6010 " fprintf(fd, \"\t-LN set scheduling restriction to N (default 0)\\n\");",
6014 " fprintf(fd, \"\t-l find non-progress cycles\\n\");",
6016 " fprintf(fd, \"\t-l find non-progress cycles -> \");",
6017 " fprintf(fd, \"disabled, requires \");",
6018 " fprintf(fd, \"compilation with -DNP\\n\");",
6022 " fprintf(fd, \"\t-MN use N Megabytes for bitstate hash array\\n\");",
6023 " fprintf(fd, \"\t-GN use N Gigabytes for bitstate hash array\\n\");",
6025 " fprintf(fd, \"\t-mN max depth N steps (default=10k)\\n\");",
6027 " fprintf(fd, \"\t-N cn -- use the claim named cn\\n\");",
6028 " fprintf(fd, \"\t-Nn -- use claim number n\\n\");",
6030 " fprintf(fd, \"\t-n no listing of unreached states\\n\");",
6032 " fprintf(fd, \"\t-p_permute randomize order in which processes are scheduled (see also -rhash)\\n\");",
6033 " fprintf(fd, \"\t-p_reverse reverse order in which processes are scheduled (see also -rhash)\\n\");",
6034 " fprintf(fd, \"\t-p_rotateN rotate by N the process scheduling order (see also -rhash)\\n\");",
6037 " fprintf(fd, \"\t-pN create svfile (save N bytes per state)\\n\");",
6039 " fprintf(fd, \"\t-QN set time-limit on execution of N minutes\\n\");",
6040 " fprintf(fd, \"\t-q require empty chans in valid end states\\n\");",
6042 " fprintf(fd, \"\t-r read and execute trail - can add -v,-n,-PN,-g,-C\\n\");",
6043 " fprintf(fd, \"\t-r trailfilename read and execute trail in file\\n\");",
6044 " fprintf(fd, \"\t-rN read and execute N-th error trail\\n\");",
6045 " fprintf(fd, \"\t-C read and execute trail - columnated output (can add -v,-n)\\n\");",
6046 " fprintf(fd, \"\t-r -PN read and execute trail - restrict trail output to proc N\\n\");",
6047 " fprintf(fd, \"\t-g read and execute trail + msc gui support\\n\");",
6048 " fprintf(fd, \"\t-S silent replay: only user defined printfs show\\n\");",
6050 " fprintf(fd, \"\t-RSn use randomization seed n\\n\");",
6051 " fprintf(fd, \"\t-rhash use random hash-polynomial and randomly choose -p_rotateN, -p_permute, or p_reverse\\n\");",
6053 " fprintf(fd, \"\t-Rn run n times n: [1..100] using n \");",
6054 " fprintf(fd, \" different hash functions\\n\");",
6056 " fprintf(fd, \"\t-T create trail files in read-only mode\\n\");",
6057 " fprintf(fd, \"\t-t_reverse reverse order in which transitions are explored\\n\");",
6058 " fprintf(fd, \"\t-tsuf replace .trail with .suf on trailfiles\\n\");",
6059 " fprintf(fd, \"\t-V print SPIN version number\\n\");",
6060 " fprintf(fd, \"\t-v verbose -- filenames in unreached state listing\\n\");",
6061 " fprintf(fd, \"\t-wN hashtable of 2^N entries \");",
6062 " fprintf(fd, \"(defaults to -w%%d)\\n\", ssize);",
6063 " fprintf(fd, \"\t-x do not overwrite an existing trail file\\n\");",
6065 " fprintf(fd, \"\t-zN handoff states below depth N to 2nd cpu (multi_core)\\n\");",
6068 " fprintf(fd, \"\\n\toptions -r, -C, -PN, -g, and -S can optionally be followed by\\n\");",
6069 " fprintf(fd, \"\ta filename argument, as in \'-r filename\', naming the trailfile\\n\");",
6072 " multi_usage(fd);",
6081 " if (memcnt + (double) n > memlim)",
6082 " { printf(\"pan: reached -DMEMLIM bound\\n\");",
6086 " tmp = (char *) malloc(n);",
6090 " Uerror(\"out of non-shared memory\");",
6092 " printf(\"pan: out of memory\\n\");",
6095 " printf(\"\t%%g bytes used\\n\", memcnt);",
6096 " printf(\"\t%%g bytes more needed\\n\", (double) n);",
6097 " printf(\"\t%%g bytes limit\\n\", memlim);",
6100 " printf(\"hint: to reduce memory, recompile with\\n\");",
6102 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
6104 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
6107 " printf(\"hint: to reduce memory, recompile with\\n\");",
6109 " printf(\" -DCOLLAPSE # good, fast compression, or\\n\");",
6111 " printf(\" -DMA=%%d # better/slower compression, or\\n\", hmax);",
6113 " printf(\" -DHC # hash-compaction, approximation\\n\");",
6115 " printf(\" -DBITSTATE # supertrace, approximation\\n\");",
6119 " #ifdef FULL_TRAIL",
6120 " printf(\" omit -DFULL_TRAIL or use pan -c0 to reduce memory\\n\");",
6122 " #ifdef SEP_STATE",
6123 " printf(\"hint: to reduce memory, recompile without\\n\");",
6124 " printf(\" -DSEP_STATE # may be faster, but uses more memory\\n\");",
6129 " memcnt += (double) n;",
6133 "#define CHUNK (100*VECTORSZ)",
6136 "emalloc(ulong n) /* never released or reallocated */",
6139 " return (char *) NULL;",
6140 " if (n&(sizeof(void *)-1)) /* for proper alignment */",
6141 " n += sizeof(void *)-(n&(sizeof(void *)-1));",
6142 " if ((ulong) left < n)", /* was: (left < (long)n) */
6143 " { grow = (n < CHUNK) ? CHUNK : n;",
6145 " have = Malloc(grow);",
6147 " /* gcc's sbrk can give non-aligned result */",
6148 " grow += sizeof(void *); /* allow realignment */",
6149 " have = Malloc(grow);",
6150 " if (((unsigned) have)&(sizeof(void *)-1))",
6151 " { have += (long) (sizeof(void *) ",
6152 " - (((unsigned) have)&(sizeof(void *)-1)));",
6153 " grow -= sizeof(void *);",
6156 " fragment += (double) left;",
6160 " have += (long) n;",
6161 " left -= (long) n;",
6162 " memset(tmp, 0, n);",
6167 "dfs_Uerror(char *str)",
6168 "{ /* always fatal */",
6171 " sudden_stop(\"Uerror\");",
6174 " bfs_shutdown(\"Uerror\");",
6178 "#if defined(MA) && !defined(SAFETY)",
6181 "{ Trans *t; uchar ot, _m; int tt; short II;",
6185 " uchar oat = now._a_t;",
6186 " now._a_t &= ~(1|16|32);",
6187 " memcpy((char *) &comp_now, (char *) &now, vsize);",
6191 " trpt = getframe(depth);",
6194 " printf(\"%%ld State: \", depth);",
6195 "#if !defined(NOCOMP) && !defined(HC)",
6196 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
6197 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
6199 " for (i = 0; i < vsize; i++)",
6200 " printf(\"%%d,\", ((char *)&now)[i]);",
6202 " printf(\"\\n\");",
6205 " if (trpt->o_pm&128) /* fairness alg */",
6206 " { now._cnt[now._a_t&1] = trpt->bup.oval;",
6209 " trpt = getframe(depth);",
6218 " { long d; Trail *trl;",
6220 " for (d = 1; d < depth; d++)",
6221 " { trl = getframe(depth-d); /* was trl = (trpt-d); */",
6222 " if (trl->pr != 0)",
6223 " { now._last = trl->pr - BASE;",
6227 " now._last = (depth<1)?0:(trpt-1)->pr;",
6230 "#ifdef EVENT_TRACE",
6231 " now._event = trpt->o_event;",
6233 " if ((now._a_t&1) && depth <= A_depth)",
6234 " { now._a_t &= ~(1|16|32);",
6235 " if (fairness) now._a_t |= 2; /* ? */",
6237 " goto CameFromHere; /* checkcycles() */",
6240 " ot = trpt->o_ot; II = trpt->pr;",
6241 " tt = trpt->o_tt; this = pptr(II);",
6242 " _m = do_reverse(t, II, trpt->o_m);",
6244 " printf(\"%%3ld: proc %%d \", depth, II);",
6245 " printf(\"reverses %%d, %%d to %%d,\",",
6246 " t->forw, tt, t->st);",
6247 " printf(\" %%s [abit=%%d,adepth=%%ld,\", ",
6248 " t->tp, now._a_t, A_depth);",
6249 " printf(\"tau=%%d,%%d] <unwind>\\n\", ",
6250 " trpt->tau, (trpt-1)->tau);",
6254 " trpt = getframe(depth);",
6258 " /* reached[ot][t->st] = 1; 3.4.13 */",
6259 " ((P0 *)this)->_p = tt;",
6261 " if ((trpt->o_pm&32))",
6264 " if (now._cnt[now._a_t&1] == 0)",
6265 " now._cnt[now._a_t&1] = 1;",
6267 " now._cnt[now._a_t&1] += 1;",
6270 " if (trpt->o_pm&8)",
6271 " { now._a_t &= ~2;",
6272 " now._cnt[now._a_t&1] = 0;",
6274 " if (trpt->o_pm&16)",
6278 " if (memcmp((char *) &now, (char *) &comp_now, vsize) == 0)",
6280 " if (depth > 0) goto Up;",
6284 "static char unwinding;",
6286 "dfs_uerror(char *str)",
6287 "{ static char laststr[256];",
6290 " if (unwinding) return; /* 1.4.2 */",
6291 " if (strncmp(str, laststr, 254))",
6293 " cpu_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,",
6295 " printf(\"pan:%%d: %%s (at depth %%ld)\\n\", errors+1, str,",
6298 " (nr_handoffs * z_handoff) + ",
6300 " ((depthfound == -1)?depth:depthfound));",
6301 " strncpy(laststr, str, 254);",
6304 " if (readtrail) { wrap_trail(); return; }",
6306 " is_cycle = (strstr(str, \" cycle\") != (char *) 0);",
6308 " { depth++; trpt++;", /* include failed step */
6310 " if ((every_error != 0)",
6311 " || errors == upto)",
6313 "#if defined(MA) && !defined(SAFETY)",
6315 " { int od = depth;",
6317 " depthfound = Unwind();",
6323 " writing_trail = 1;",
6326 " if (depth > 1) trpt--;",
6328 " if (depth > 1) trpt++;",
6332 "#if defined(MA) && !defined(SAFETY)",
6333 " if (strstr(str, \" cycle\"))",
6334 " { if (every_error)",
6335 " printf(\"sorry: MA writes 1 trail max\\n\");",
6336 " wrapup(); /* no recovery from unwind */",
6340 " if (search_terminated != NULL)",
6341 " { *search_terminated |= 4; /* uerror */",
6343 " writing_trail = 0;",
6347 " { depth--; trpt--; /* undo */",
6350 " if (iterative != 0 && maxdepth > 0)",
6351 " { if (maxdepth > depth)",
6352 " { maxdepth = (iterative == 1)?(depth+1):(depth/2);",
6355 " printf(\"pan: reducing search depth to %%ld\\n\",",
6359 " if (errors >= upto && upto != 0)",
6362 " bfs_shutdown(\"uerror\"); /* no return */",
6365 " sudden_stop(\"uerror\");",
6369 " depthfound = -1;",
6372 "xrefsrc(int lno, S_F_MAP *mp, int M, int i)",
6373 "{ Trans *T; int j, retval=1;",
6374 " for (T = trans[M][i]; T; T = T->nxt)",
6376 " { if (strcmp(T->tp, \".(goto)\") == 0",
6377 " || strncmp(T->tp, \"goto :\", 6) == 0)",
6378 " return 1; /* not reported */",
6380 " for (j = 0; j < sizeof(mp); j++)",
6381 " if (i >= mp[j].from && i <= mp[j].upto)",
6382 " { printf(\"\\t%%s:%%d\", mp[j].fnm, lno);",
6385 " if (j >= sizeof(mp)) /* fnm not found in list */",
6386 " { printf(\"\\t%%s:%%d\", PanSource, lno); /* use default */",
6388 " printf(\", state %%d\", i);",
6389 " if (strcmp(T->tp, \"\") != 0)",
6391 " q = transmognify(T->tp);",
6392 " printf(\", \\\"%%s\\\"\", q?q:\"\");",
6393 " } else if (stopstate[M][i])",
6394 " printf(\", -end state-\");",
6395 " printf(\"\\n\");",
6396 " retval = 0; /* reported */",
6401 "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)",
6404 " if ((enum btypes) Btypes[M] == N_CLAIM",
6405 " && claimname != NULL && strcmp(claimname, procname[M]) != 0)",
6409 " switch ((enum btypes) Btypes[M]) {",
6412 " printf(\"unreached in proctype %%s\\n\", procname[M]);",
6415 " printf(\"unreached in init\\n\");",
6421 " printf(\"unreached in claim %%s\\n\", procname[M]);",
6424 " for (i = 1; i < N; i++)",
6425 " { if (which[i] == 0",
6426 " && (mapstate[M][i] == 0",
6427 " || which[mapstate[M][i]] == 0))",
6428 " { m += xrefsrc((int) src[i], mp, M, i);",
6432 " printf(\"\t(%%d of %%d states)\\n\", N-1-m, N-1);",
6434 "#if NCORE>1 && !defined(SEP_STATE)",
6435 "static long rev_trail_cnt;",
6437 "#ifdef FULL_TRAIL",
6439 "rev_trail(int fd, volatile Stack_Tree *st_tr)",
6440 "{ long j; char snap[64];",
6445 " rev_trail(fd, st_tr->prv);",
6447 " printf(\"%%d (%%d) LRT [%%d,%%d] -- %%9u (root %%9u)\\n\",",
6448 " depth, rev_trail_cnt, st_tr->pr, st_tr->t_id, st_tr, stack_last[core_id]);",
6450 " if (st_tr->pr != 255)", /* still needed? */
6451 " { sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
6452 " rev_trail_cnt++, st_tr->pr, st_tr->t_id);",
6453 " j = strlen(snap);",
6454 " if (write(fd, snap, j) != j)",
6455 " { printf(\"pan: error writing trailfile\\n\");",
6460 " } else /* handoff point */",
6462 " { (void) write(fd, \"-1:-1:-1\\n\", 9);",
6465 "#endif", /* FULL_TRAIL */
6466 "#endif", /* NCORE>1 */
6471 "#if defined VERI || defined(MERGED)",
6474 "#if NCORE==1 || defined(SEP_STATE) || !defined(FULL_TRAIL)",
6478 " fd = make_trail();",
6479 " if (fd < 0) return;",
6481 " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
6482 " if (write(fd, snap, strlen(snap)) < 0) return;",
6485 " sprintf(snap, \"-4:-4:-4\\n\");",
6486 " if (write(fd, snap, strlen(snap)) < 0) return;",
6489 " sprintf(snap, \"-5:%%d:%%d\\n\", t_reverse, reversing&2);",
6490 " if (write(fd, snap, strlen(snap)) < 0) return;",
6492 " sprintf(snap, \"-6:%%d:%%d\\n\", p_reorder==set_permuted, p_reorder==set_reversed);",
6493 " if (write(fd, snap, strlen(snap)) < 0) return;",
6495 " sprintf(snap, \"-7:%%d:%%d\\n\", p_reorder==set_rotated, p_rotate);",
6496 " if (write(fd, snap, strlen(snap)) < 0) return;",
6498 " sprintf(snap, \"-8:%%d:%%d\\n\", p_reorder==set_randrot, --s_rand);",
6499 " if (write(fd, snap, strlen(snap)) < 0) return;",
6501 "#if NCORE>1 && !defined(SEP_STATE) && defined(FULL_TRAIL)",
6502 " rev_trail_cnt = 1;",
6503 " enter_critical(GLOBAL_LOCK);",
6504 " rev_trail(fd, stack_last[core_id]);",
6505 " leave_critical(GLOBAL_LOCK);",
6507 " i = 1; /* trail starts at position 1 */",
6508 " #if NCORE>1 && defined(SEP_STATE)",
6509 " if (cur_Root.m_vsize > 0) { i++; depth++; }",
6511 " for ( ; i <= depth; i++)",
6512 " { if (i == depthfound+1)",
6513 " { if (write(fd, \"-1:-1:-1\\n\", 9) != 9)",
6516 " trl = getframe(i);",
6517 " if (!trl->o_t) continue;",
6518 " if (trl->o_pm&128) continue;",
6519 " sprintf(snap, \"%%ld:%%d:%%d\\n\", ",
6520 " i, trl->pr, trl->o_t->t_id);",
6521 " j = strlen(snap);",
6522 " if (write(fd, snap, j) != j)",
6524 "notgood: printf(\"pan: error writing trailfile\\n\");",
6531 " cpu_printf(\"pan: wrote trailfile\\n\");",
6535 "sv_save(void) /* push state vector onto save stack */",
6536 "{ if (!svtack->nxt)",
6537 " { svtack->nxt = (Svtack *) emalloc(sizeof(Svtack));",
6538 " svtack->nxt->body = emalloc(vsize*sizeof(char));",
6539 " svtack->nxt->lst = svtack;",
6540 " svtack->nxt->m_delta = vsize;",
6542 " } else if (vsize > svtack->nxt->m_delta)",
6543 " { svtack->nxt->body = emalloc(vsize*sizeof(char));",
6544 " svtack->nxt->lst = svtack;",
6545 " svtack->nxt->m_delta = vsize;",
6548 " svtack = svtack->nxt;",
6550 " svtack->o_boq = boq;",
6555 " svtack->o_delta = vsize; /* don't compress */",
6556 " memcpy((char *)(svtack->body), (char *) &now, vsize);",
6557 "#if defined(C_States) && defined(HAS_STACK) && (HAS_TRACK==1)",
6558 " c_stack((uchar *) &(svtack->c_stack[0]));",
6561 " cpu_printf(\"%%d: sv_save\\n\", depth);",
6565 "sv_restor(void) /* pop state vector from save stack */",
6567 " memcpy((char *)&now, svtack->body, svtack->o_delta);",
6569 " boq = svtack->o_boq;",
6574 "#if defined(C_States) && (HAS_TRACK==1)",
6576 " c_unstack((uchar *) &(svtack->c_stack[0]));",
6578 " c_revert((uchar *) &(now.c_state[0]));",
6581 " if (vsize != svtack->o_delta)",
6582 " Uerror(\"sv_restor\");",
6583 " if (!svtack->lst)",
6584 " Uerror(\"error: sv_restor\");",
6585 " svtack = svtack->lst;",
6587 " cpu_printf(\" sv_restor\\n\");",
6594 " char *z = (char *) &now;\n",
6597 " bfs_prepmask(1); /* p_restor */",
6600 " proc_offset[h] = stack->o_offset;",
6601 " proc_skip[h] = (uchar) stack->o_skip;",
6605 " printf(\"%%4d: p_restor %%d\\n\", depth, h);",
6609 " p_name[h] = stack->o_name;",
6612 " vsize += sizeof(char *);",
6614 " if (processes[h] != NULL || freebodies == NULL)",
6615 " { Uerror(\"processes error\");",
6617 " processes[h] = freebodies;",
6618 " freebodies = freebodies->nxt;",
6619 " processes[h]->nxt = (TRIX_v6 *) 0;",
6620 " processes[h]->modified = 1; /* p_restor */",
6622 " processes[h]->parent_pid = stack->parent;",
6623 " processes[h]->psize = stack->o_delta;",
6624 " memcpy((char *)pptr(h), stack->b_ptr, stack->o_delta);",
6625 " oi = stack->b_ptr;",
6627 " #if !defined(NOCOMP) && !defined(HC)",
6628 " for (i = vsize + stack->o_skip; i > vsize; i--)",
6629 " Mask[i-1] = 1; /* align */",
6631 " vsize += stack->o_skip;",
6632 " memcpy(z+vsize, stack->body, stack->o_delta);",
6633 " vsize += stack->o_delta;",
6634 " #if !defined(NOCOMP) && !defined(HC)",
6635 " for (i = 1; i <= Air[((P0 *)pptr(h))->_t]; i++)",
6636 " Mask[vsize - i] = 1; /* pad */",
6637 " Mask[proc_offset[h]] = 1; /* _pid */",
6639 " if (BASE > 0 && h > 0)",
6640 " ((P0 *)pptr(h))->_pid = h-BASE;",
6642 " ((P0 *)pptr(h))->_pid = h;",
6644 " bfs_fixmask(1); /* p_restor */",
6647 " now._nr_pr += 1;",
6649 " now._vsz = vsize;",
6651 " i = stack->o_delqs;",
6652 " if (!stack->lst)",
6653 " Uerror(\"error: p_restor\");",
6654 " stack = stack->lst;",
6659 " re_mark_all(1); /* p_restor - all chans move up in _ids_ */",
6660 " now._ids_[h] = oi; /* restor the original contents */",
6665 "{ int h = now._nr_qs;",
6668 " printf(\"%%4d: q_restor %%d\\n\", depth, h);",
6670 " vsize += sizeof(char *);",
6672 " if (channels[h] != NULL || freebodies == NULL)",
6673 " { Uerror(\"channels error\");",
6675 " channels[h] = freebodies;",
6676 " freebodies = freebodies->nxt;",
6677 " channels[h]->nxt = (TRIX_v6 *) 0;",
6678 " channels[h]->modified = 1; /* q_restor */",
6680 " channels[h]->parent_pid = stack->parent;",
6681 " channels[h]->psize = stack->o_delta;",
6682 " memcpy((char *)qptr(h), stack->b_ptr, stack->o_delta);",
6683 " now._ids_[now._nr_pr + h] = stack->b_ptr;",
6685 " char *z = (char *) &now;",
6690 " bfs_prepmask(2); /* q_restor */",
6692 " q_offset[h] = stack->o_offset;",
6693 " q_skip[h] = (uchar) stack->o_skip;",
6694 " vsize += stack->o_skip;",
6695 " memcpy(z+vsize, stack->body, stack->o_delta);",
6696 " vsize += stack->o_delta;",
6699 " q_name[h] = stack->o_name;",
6702 " now._vsz = vsize;",
6704 " now._nr_qs += 1;",
6706 " #if !defined(NOCOMP) && !defined(HC)",
6707 " k_end = stack->o_offset;",
6708 " k = k_end - stack->o_skip;",
6711 " if (q_zero(now._nr_qs)) k_end += stack->o_delta;",
6714 " for ( ; k < k_end; k++)",
6718 " bfs_fixmask(2); /* q_restor */",
6721 " if (!stack->lst)",
6722 " Uerror(\"error: q_restor\");",
6723 " stack = stack->lst;",
6726 "typedef struct IntChunks {",
6728 " struct IntChunks *nxt;",
6730 "IntChunks *filled_chunks[512];",
6731 "IntChunks *empty_chunks[512];",
6734 "grab_ints(int nr)",
6736 " if (nr >= 512) Uerror(\"cannot happen grab_int\");",
6737 " if (filled_chunks[nr])",
6738 " { z = filled_chunks[nr];",
6739 " filled_chunks[nr] = filled_chunks[nr]->nxt;",
6741 " { z = (IntChunks *) emalloc(sizeof(IntChunks));",
6742 " z->ptr = (int *) emalloc(nr * sizeof(int));",
6744 " z->nxt = empty_chunks[nr];",
6745 " empty_chunks[nr] = z;",
6749 "ungrab_ints(int *p, int nr)",
6751 " if (!empty_chunks[nr]) Uerror(\"cannot happen ungrab_int\");",
6752 " z = empty_chunks[nr];",
6753 " empty_chunks[nr] = empty_chunks[nr]->nxt;",
6755 " z->nxt = filled_chunks[nr];",
6756 " filled_chunks[nr] = z;",
6759 "delproc(int sav, int h)",
6762 " int o_vsize = vsize;",
6764 " if (h+1 != (int) now._nr_pr)",
6769 " printf(\"%%4d: delproc %%d -- parent %%d\\n\", depth, h, processes[h]->parent_pid);",
6770 " if (now._nr_qs > 0)",
6771 " printf(\" top channel: %%d -- parent %%d\\n\", now._nr_qs-1, channels[now._nr_qs-1]->parent_pid);",
6773 " while (now._nr_qs > 0",
6774 " && channels[now._nr_qs-1]->parent_pid == processes[h]->parent_pid)",
6778 " d = processes[h]->psize;",
6780 " { if (!stack->nxt)",
6781 " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
6782 " stack->nxt->lst = stack;",
6785 " stack = stack->nxt;",
6787 " stack->o_name = p_name[h];",
6789 " stack->parent = processes[h]->parent_pid;",
6790 " stack->o_delta = d;",
6791 " stack->o_delqs = i;",
6792 " stack->b_ptr = now._ids_[h];", /* new 6.1 */
6794 " memset((char *)pptr(h), 0, d);",
6796 " processes[h]->nxt = freebodies;",
6797 " freebodies = processes[h];",
6798 " processes[h] = (TRIX_v6 *) 0;",
6800 " vsize -= sizeof(char *);",
6801 " now._nr_pr -= 1;",
6802 " re_mark_all(-1); /* delproc - all chans move down in _ids_ */",
6804 " while (now._nr_qs",
6805 " && q_offset[now._nr_qs-1] > proc_offset[h])",
6809 " d = vsize - proc_offset[h];",
6811 " { if (!stack->nxt)",
6812 " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
6813 " stack->nxt->body = emalloc(Maxbody * sizeof(char));",
6814 " stack->nxt->lst = stack;",
6817 " stack = stack->nxt;",
6818 " stack->o_offset = proc_offset[h];",
6819 " #if VECTORSZ>32000",
6820 " stack->o_skip = (int) proc_skip[h];",
6822 " stack->o_skip = (short) proc_skip[h];",
6825 " stack->o_name = p_name[h];",
6827 " stack->o_delta = d;",
6828 " stack->o_delqs = i;",
6829 " memcpy(stack->body, (char *)pptr(h), d);",
6831 " vsize = proc_offset[h];",
6832 " now._nr_pr -= 1;",
6833 " memset((char *)pptr(h), 0, d);",
6834 " vsize -= (int) proc_skip[h];",
6835 " #if !defined(NOCOMP) && !defined(HC)",
6837 " bfs_prepmask(3); /* delproc - no chance in proc_offset or proc_skip */",
6839 " for (i = vsize; i < o_vsize; i++)",
6840 " Mask[i] = 0; /* reset */",
6842 " bfs_fixmask(3); /* delproc */",
6847 " now._vsz = vsize;",
6853 "{ int h = now._nr_qs - 1;",
6855 " int d = channels[now._nr_qs - 1]->psize;",
6857 " int d = vsize - q_offset[now._nr_qs - 1];",
6860 " int k, o_vsize = vsize;",
6863 " { if (!stack->nxt)",
6864 " { stack->nxt = (_Stack *) emalloc(sizeof(_Stack));",
6866 " stack->nxt->body = emalloc(Maxbody * sizeof(char));",
6868 " stack->nxt->lst = stack;",
6871 " stack = stack->nxt;",
6873 " stack->parent = channels[h]->parent_pid;",
6874 " stack->b_ptr = now._ids_[h];", /* new 6.1 */
6876 " stack->o_offset = q_offset[h];",
6877 " #if VECTORSZ>32000",
6878 " stack->o_skip = (int) q_skip[h];",
6880 " stack->o_skip = (short) q_skip[h];",
6884 " stack->o_name = q_name[h];",
6886 " stack->o_delta = d;",
6888 " memcpy(stack->body, (char *)qptr(h), d);",
6892 " vsize -= sizeof(char *);",
6894 " printf(\"%%4d: delq %%d parent %%d\\n\", depth, h, channels[h]->parent_pid);",
6897 " vsize = q_offset[h];",
6898 " vsize -= (int) q_skip[h];",
6899 " #if !defined(NOCOMP) && !defined(HC)",
6901 " bfs_prepmask(3); /* delq - no change in q_offset or q_skip */",
6903 " for (k = vsize; k < o_vsize; k++)",
6904 " Mask[k] = 0; /* reset */",
6906 " bfs_fixmask(3); /* delq */",
6910 " now._nr_qs -= 1;",
6911 " memset((char *)qptr(h), 0, d);",
6914 " channels[h]->nxt = freebodies;",
6915 " freebodies = channels[h];",
6916 " channels[h] = (TRIX_v6 *) 0;",
6920 " now._vsz = vsize;",
6926 " for (i = 0; i < (int) now._nr_qs; i++)",
6927 " { if (q_sz(i) > 0)",
6934 "{ int i; P0 *ptr;",
6935 " for (i = BASE; i < (int) now._nr_pr; i++)",
6936 " { ptr = (P0 *) pptr(i);",
6937 " if (!stopstate[ptr->_t][ptr->_p])",
6940 " if (strict) return qs_empty();",
6941 "#if defined(EVENT_TRACE)",
6942 " if (!stopstate[EVENT_TRACE][now._event] && !a_cycles)",
6943 " { printf(\"pan: event_trace not completed\\n\");",
6949 "#if !defined(SAFETY) && !defined(BFS)",
6951 "checkcycles(void)",
6952 "{ uchar o_a_t = now._a_t;",
6954 " uchar o_cnt = now._cnt[1];",
6956 " #ifdef FULLSTACK",
6958 " H_el *sv = trpt->ostate; /* save */",
6960 " uchar prov = trpt->proviso; /* save */",
6964 " { int i; uchar *v = (uchar *) &now;",
6965 " printf(\" set Seed state \");",
6968 " printf(\"(cnt = %%d:%%d, nrpr=%%d) \",",
6969 " now._cnt[0], now._cnt[1], now._nr_pr);",
6971 " /* for (i = 0; i < n; i++) printf(\"%%d,\", v[i]); */",
6972 " printf(\"\\n\");",
6974 " printf(\"%%ld: cycle check starts\\n\", depth);",
6976 " now._a_t |= (1|16|32);",
6977 " /* 1 = 2nd DFS; (16|32) to improve hashing */",
6979 " now._cnt[1] = now._cnt[0];",
6981 " memcpy((char *)&A_Root, (char *)&now, vsize);",
6982 " A_depth = depthfound = depth;",
6985 " mem_put_acc();", /* handoff accept states */
6987 " new_state(); /* start 2nd DFS */",
6990 " now._a_t = o_a_t;",
6992 " now._cnt[1] = o_cnt;",
6994 " A_depth = 0; depthfound = -1;",
6996 " printf(\"%%ld: cycle check returns\\n\", depth);",
7000 " trpt->ostate = sv; /* restore */",
7002 " trpt->proviso = prov;",
7008 "#if defined(FULLSTACK) && defined(BITSTATE)",
7009 "H_el *Free_list = (H_el *) 0;",
7011 "onstack_init(void) /* to store stack states in a bitstate search */",
7012 "{ S_Tab = (H_el **) emalloc(maxdepth*sizeof(H_el *));",
7016 "#if !defined(BFS_PAR)",
7017 " #if defined(FULLSTACK) && defined(BITSTATE)",
7019 "grab_state(int n)",
7020 "{ H_el *v, *last = 0;",
7021 " if (H_tab == S_Tab)",
7022 " { for (v = Free_list; v && ((int) v->tagged >= n); v=v->nxt)",
7023 " { if ((int) v->tagged == n)",
7025 " last->nxt = v->nxt;",
7027 "gotcha: Free_list = v->nxt;",
7037 " /* new: second try */",
7038 " v = Free_list;", /* try to avoid emalloc */
7039 " if (v && ((int) v->tagged >= n))",
7043 " return (H_el *) emalloc(sizeof(H_el)+n-sizeof(unsigned));",
7045 " #else", /* !FULLSTACK || !BITSTATE */
7048 "grab_state(int n)",
7049 "{ H_el *grab_shared(int);",
7050 " return grab_shared(sizeof(H_el)+n-sizeof(unsigned));",
7052 "#else", /* ! NCORE>1 */
7053 "#ifndef AUTO_RESIZE",
7054 " #define grab_state(n) (H_el *) \\",
7055 " emalloc(sizeof(H_el)+n-sizeof(ulong));",
7056 "#else", /* AUTO_RESIZE */
7058 "grab_state(int n)",
7060 " int cnt = sizeof(H_el)+n-sizeof(ulong);",
7062 " if (reclaim_size >= cnt+WS)",
7063 " { if ((cnt & (WS-1)) != 0) /* alignment */",
7064 " { cnt += WS - (cnt & (WS-1));",
7066 " p = (H_el *) reclaim_mem;",
7067 " reclaim_mem += cnt;",
7068 " reclaim_size -= cnt;",
7069 " memset(p, 0, cnt);",
7072 " { p = (H_el *) emalloc(cnt);",
7076 "#endif", /* AUTO_RESIZE */
7077 "#endif", /* NCORE>1 */
7078 " #endif", /* FULLSTACK && !BITSTATE */
7079 "#else", /* BFS_PAR */
7080 " extern volatile uchar *sh_pre_malloc(ulong);",
7081 " extern volatile uchar *sh_malloc(ulong);",
7083 " grab_state(int n) /* bfs_par */",
7084 " { volatile uchar *rval = NULL;",
7085 " int m = sizeof(H_el) + n - sizeof(unsigned);",
7087 " if (n == 0) m = m/n;",
7088 " #ifdef BFS_SEP_HASH",
7089 " rval = emalloc((ulong) m);",
7091 " rval = sh_malloc((ulong) m);",
7093 " memset((void *) rval, 0, (size_t) m);",
7095 " return (H_el *) rval;",
7097 "#endif", /* BFS_PAR */
7101 "ordinal(char *v, long n, short tp)",
7102 "{ H_el *tmp, *ntmp; long m;",
7103 " H_el *olst = (H_el *) 0;",
7104 " s_hash((uchar *)v, n);",
7106 "#if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7107 " e_critical(BFS_ID); /* bfs_par / collapse */",
7109 "#if NCORE>1 && !defined(SEP_STATE)",
7110 " enter_critical(CS_ID); /* uses spinlock - 1..128 */",
7112 " tmp = H_tab[j1_spin];",
7114 " { tmp = grab_state(n);",
7115 " H_tab[j1_spin] = tmp;",
7117 " for ( ;; olst = tmp, tmp = tmp->nxt)",
7118 " { if (n == tmp->ln)",
7119 " { m = memcmp(((char *)&(tmp->state)), v, n);",
7124 "Insert: ntmp = grab_state(n);",
7125 " ntmp->nxt = tmp;",
7127 " H_tab[j1_spin] = ntmp;",
7129 " olst->nxt = ntmp;",
7132 " } else if (!tmp->nxt)",
7134 "Append: tmp->nxt = grab_state(n);",
7140 " if (n < tmp->ln)",
7142 " else if (!tmp->nxt)",
7145 "#if NCORE>1 && !defined(SEP_STATE)",
7146 " enter_critical(GLOBAL_LOCK);",
7149 " e_critical(BFS_ORD); /* bfs_par */",
7151 " m = ++ncomps[tp];",
7153 " x_critical(BFS_ORD);",
7155 "#if NCORE>1 && !defined(SEP_STATE)",
7156 " leave_critical(GLOBAL_LOCK);",
7159 " tmp->tagged = m;",
7163 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
7166 " memcpy(((char *)&(tmp->state)), v, n);",
7170 "#if NCORE>1 && !defined(SEP_STATE)",
7171 " leave_critical(CS_ID);",
7173 "#if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7174 " x_critical(BFS_ID);",
7178 " return tmp->tagged;",
7180 " return tmp->st_id;",
7185 "compress(char *vin, int nin) /* collapse compression */",
7186 "{ char *w, *v = (char *) &comp_now;",
7190 " static uchar nbytes[513]; /* 1 + 256 + 256 */",
7191 " static unsigned short nbytelen;",
7192 " long col_q(int, char *);",
7193 " long col_p(int, char *);",
7196 " *v++ = now._a_t;",
7199 " for (i = 0; i < NFAIR; i++)",
7200 " *v++ = now._cnt[i];",
7205 "#ifndef JOINPROCS",
7206 " for (i = 0; i < (int) now._nr_pr; i++)",
7207 " { n = col_p(i, (char *) 0);",
7209 " nbytes[nbytelen] = 0;",
7211 " nbytes[nbytelen] = 1;",
7212 " *v++ = ((P0 *) pptr(i))->_t;",
7215 " if (n >= (1<<8))",
7216 " { nbytes[nbytelen]++;",
7217 " *v++ = (n>>8)&255;",
7219 " if (n >= (1<<16))",
7220 " { nbytes[nbytelen]++;",
7221 " *v++ = (n>>16)&255;",
7223 " if (n >= (1<<24))",
7224 " { nbytes[nbytelen]++;",
7225 " *v++ = (n>>24)&255;",
7231 " for (i = 0; i < (int) now._nr_pr; i++)",
7232 " x += col_p(i, x);",
7233 " n = ordinal(scratch, x-scratch, 2); /* procs */",
7235 " nbytes[nbytelen] = 0;",
7236 " if (n >= (1<<8))",
7237 " { nbytes[nbytelen]++;",
7238 " *v++ = (n>>8)&255;",
7240 " if (n >= (1<<16))",
7241 " { nbytes[nbytelen]++;",
7242 " *v++ = (n>>16)&255;",
7244 " if (n >= (1<<24))",
7245 " { nbytes[nbytelen]++;",
7246 " *v++ = (n>>24)&255;",
7251 " for (i = 0; i < (int) now._nr_qs; i++)",
7252 " { n = col_q(i, (char *) 0);",
7253 " nbytes[nbytelen] = 0;",
7255 " if (n >= (1<<8))",
7256 " { nbytes[nbytelen]++;",
7257 " *v++ = (n>>8)&255;",
7259 " if (n >= (1<<16))",
7260 " { nbytes[nbytelen]++;",
7261 " *v++ = (n>>16)&255;",
7263 " if (n >= (1<<24))",
7264 " { nbytes[nbytelen]++;",
7265 " *v++ = (n>>24)&255;",
7272 " /* 3 = _a_t, _nr_pr, _nr_qs */",
7273 " w = (char *) &now + 3 * sizeof(uchar);",
7278 "#if VECTORSZ<65536",
7279 " w = (char *) &(now._vsz) + sizeof(unsigned short);",
7281 " w = (char *) &(now._vsz) + sizeof(ulong);",
7285 " *x++ = now._nr_pr;",
7286 " *x++ = now._nr_qs;",
7288 " if (now._nr_qs > 0 && qptr(0) < pptr(0))",
7289 " n = qptr(0) - (uchar *) w;",
7291 " n = pptr(0) - (uchar *) w;",
7292 " j = w - (char *) &now;",
7294 "#if !defined(NOCOMP) && !defined(HC)",
7295 " for (i = 0; i < (int) n; i++, w++)",
7296 " if (!Mask[j++]) *x++ = *w;",
7298 " memcpy(x, w, n); x += n;",
7302 " for (i = 0; i < (int) now._nr_qs; i++)",
7303 " x += col_q(i, x);",
7307 " for (i = 0, j = 6; i < nbytelen; i++)",
7313 " *x |= (nbytes[i] << j);",
7316 " for (j = 0; j < WS-1; j++)",
7319 " n = ordinal(scratch, x-scratch, 0); /* globals */",
7321 " if (n >= (1<< 8)) { *v++ = (n>> 8)&255; j++; }",
7322 " if (n >= (1<<16)) { *v++ = (n>>16)&255; j++; }",
7323 " if (n >= (1<<24)) { *v++ = (n>>24)&255; j++; }",
7324 " *v++ = j; /* add last count as a byte */",
7326 " for (i = 0; i < WS-1; i++)",
7330 " printf(\"collapse %%d -> %%d\\n\",",
7331 " vsize, v - (char *)&comp_now);",
7333 " return v - (char *)&comp_now;",
7336 "#else", /* !COLLAPSE */
7337 "#if !defined(NOCOMP)",
7339 "compress(char *vin, int n) /* default compression */",
7343 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
7346 " { delta++; /* _a_t */",
7348 " if (S_A > NFAIR)",
7349 " delta += NFAIR; /* _cnt[] */",
7353 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
7356 " memcpy((char *) &comp_now + delta, (char *) &K2, HC);",
7362 " char *v = (char *) &comp_now;",
7364 " #ifndef NO_FAST_C", /* disable faster compress */
7365 " int r = 0, unroll = n/8;", /* most sv are much longer */
7368 " while (r++ < unroll)",
7369 " { /* unroll 8 times, avoid ifs */",
7370 " /* 1 */ *v = *vv++; v += 1 - Mask[i++];",
7371 " /* 2 */ *v = *vv++; v += 1 - Mask[i++];",
7372 " /* 3 */ *v = *vv++; v += 1 - Mask[i++];",
7373 " /* 4 */ *v = *vv++; v += 1 - Mask[i++];",
7374 " /* 5 */ *v = *vv++; v += 1 - Mask[i++];",
7375 " /* 6 */ *v = *vv++; v += 1 - Mask[i++];",
7376 " /* 7 */ *v = *vv++; v += 1 - Mask[i++];",
7377 " /* 8 */ *v = *vv++; v += 1 - Mask[i++];",
7379 " r = n - i; /* the rest, at most 7 */",
7381 " case 7: *v = *vv++; v += 1 - Mask[i++];",
7382 " case 6: *v = *vv++; v += 1 - Mask[i++];",
7383 " case 5: *v = *vv++; v += 1 - Mask[i++];",
7384 " case 4: *v = *vv++; v += 1 - Mask[i++];",
7385 " case 3: *v = *vv++; v += 1 - Mask[i++];",
7386 " case 2: *v = *vv++; v += 1 - Mask[i++];",
7387 " case 1: *v = *vv++; v += 1 - Mask[i++];",
7390 " n = i = v - (char *)&comp_now; /* bytes written so far */",
7391 " r = (n+WS-1)/WS; /* in words, rounded up */",
7392 " r *= WS; /* total bytes to fill */",
7393 " i = r - i; /* remaining bytes */",
7394 " switch (i) {", /* fill word */
7395 " case 7: *v++ = 0; /* fall thru */",
7396 " case 6: *v++ = 0;",
7397 " case 5: *v++ = 0;",
7398 " case 4: *v++ = 0;",
7399 " case 3: *v++ = 0;",
7400 " case 2: *v++ = 0;",
7401 " case 1: *v++ = 0;",
7403 " default: Uerror(\"unexpected wordsize\");",
7408 " { for (i = 0; i < n; i++, vv++)",
7409 " if (!Mask[i]) *v++ = *vv;",
7410 " for (i = 0; i < WS-1; i++)",
7415 " printf(\"compress %%d -> %%d\\n\",",
7416 " n, v - (char *)&comp_now);",
7418 " return v - (char *)&comp_now;",
7422 "#endif", /* COLLAPSE */
7423 "#if defined(FULLSTACK) && defined(BITSTATE)",
7425 "#if !defined(onstack_now)",
7426 "int onstack_now(void) {}", /* to suppress compiler errors */
7428 "#if !defined(onstack_put)",
7429 "void onstack_put(void) {}", /* for this invalid combination */
7431 "#if !defined(onstack_zap)",
7432 "void onstack_zap(void) {}", /* of directives */
7436 "onstack_zap(void)",
7437 "{ H_el *v, *w, *last = 0;",
7438 " H_el **tmp = H_tab;",
7439 " char *nv; int n, m;",
7440 " static char warned = 0;",
7441 "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7442 " uchar was_last = now._last;",
7448 " nv = (char *) &comp_now;",
7449 " n = compress((char *)&now, vsize);",
7451 "#if defined(BITSTATE) && defined(LC)",
7452 " nv = (char *) &comp_now;",
7453 " n = compact_stack((char *)&now, vsize);",
7455 " nv = (char *) &now;",
7459 "#if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
7460 " s_hash((uchar *)nv, n);",
7463 " for (v = S_Tab[j1_spin]; v; Zh++, last=v, v=v->nxt)",
7464 " { m = memcmp(&(v->state), nv, n);",
7472 " /* seen this happen, likely harmless in multicore */",
7473 " if (warned == 0)",
7474 " { /* Uerror(\"stack out of wack - zap\"); */",
7475 " cpu_printf(\"pan: warning, stack incomplete\\n\");",
7483 " last->nxt = v->nxt;",
7485 " S_Tab[j1_spin] = v->nxt;",
7486 " v->tagged = (unsigned) n;",
7487 "#if !defined(NOREDUCE) && !defined(SAFETY)",
7490 " v->nxt = last = (H_el *) 0;",
7491 " for (w = Free_list; w; Fa++, last=w, w = w->nxt)",
7492 " { if ((int) w->tagged <= n)",
7497 " { v->nxt = Free_list;",
7508 "#if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7509 " now._last = was_last;",
7516 " onstack_put(void)",
7517 " { H_el **tmp = H_tab;",
7518 " #if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7519 " uchar was_last = now._last;",
7523 " if (h_store((char *)&now, vsize) != 0)",
7524 " #if defined(BITSTATE) && defined(LC)",
7525 " printf(\"pan: warning, double stack entry\\n\");",
7528 " Uerror(\"cannot happen - unstack_put\");",
7532 " trpt->ostate = Lstate;",
7534 " #if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7535 " now._last = was_last;",
7539 " onstack_now(void)",
7541 " H_el **tmp2 = H_tab;",
7542 " char *v; int n, m = 1;\n",
7543 " #if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7544 " uchar was_last = now._last;",
7549 " #if defined(BITSTATE) && defined(LC)",
7550 " v = (char *) &comp_now;",
7551 " n = compact_stack((char *)&now, vsize);",
7553 " v = (char *) &now;",
7557 " v = (char *) &comp_now;",
7558 " n = compress((char *)&now, vsize);",
7560 " #if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
7561 " s_hash((uchar *)v, n);",
7564 " for (tmp = S_Tab[j1_spin]; tmp; Zn++, tmp = tmp->nxt)",
7565 " { m = memcmp(((char *)&(tmp->state)),v,n);",
7567 " { Lstate = (H_el *) tmp; /* onstack_now */",
7571 " #if defined(BCS) && defined(NO_LAST) && defined(HAS_LAST)",
7572 " now._last = was_last;",
7574 " return (m == 0);",
7576 "#endif", /* !BFS_PAR */
7578 "#endif", /* FULLSTACK && BITSTATE */
7581 "void init_SS(ulong);",
7587 " { udmem *= 1024L*1024L;",
7590 " { init_SS((ulong) udmem);",
7593 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7594 " SS = (uchar *) sh_pre_malloc((ulong) udmem);",
7596 " SS = (uchar *) emalloc(udmem);",
7598 " b_store = bstore_mod;",
7602 " init_SS(ONE_L<<(ssize-3));",
7604 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7605 " SS = (uchar *) sh_pre_malloc((ulong)(ONE_L<<(ssize-3)));",
7607 " SS = (uchar *) emalloc(ONE_L<<(ssize-3));",
7613 " #if !defined(MA) || defined(COLLAPSE)",
7617 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7618 " H_tab = (H_el **) sh_pre_malloc((ulong)((ONE_L<<ssize)*sizeof(H_el *)));",
7620 " H_tab = (H_el **) emalloc((ONE_L<<ssize)*sizeof(H_el *));",
7629 " { void r_xpoint(void);",
7633 " dfa_init((unsigned short) (MA+a_cycles));",
7634 " #if NCORE>1 && !defined(COLLAPSE)",
7636 " { void init_HT(ulong);",
7642 " #if !defined(MA) || defined(COLLAPSE)",
7643 " #if NCORE>1 || (defined(BFS_PAR) && defined(USE_TDH) && !defined(WIN32) && !defined(WIN64))",
7645 " { void init_HT(ulong);",
7646 " init_HT((ulong) (ONE_L<<ssize)*sizeof(H_el *));",
7647 " #if defined(TRIX) || (defined(BFS_PAR) && defined(COLLAPSE))",
7648 " set_H_tab(); /* need both */",
7652 " { set_H_tab(); /* @htable ssize */",
7654 " #endif", /* !defined(MA) || defined(COLLAPSE) */
7658 "#if !defined(BITSTATE) || defined(FULLSTACK)",
7662 "dumpstate(int wasnew, char *v, int n, int tag)",
7666 " { printf(\"\tstate tags %%d (%%d::%%d): \",",
7667 " V_A, wasnew, v[0]);",
7669 " printf(\" %%d \", tag);",
7671 " printf(\"\\n\");",
7675 " printf(\"\t State: \");",
7676 "#if !defined(NOCOMP) && !defined(HC)",
7677 " for (i = 0; i < vsize; i++) printf(\"%%d%%s,\",",
7678 " ((char *)&now)[i], Mask[i]?\"*\":\"\");",
7680 " for (i = 0; i < vsize; i++)",
7681 " printf(\"%%d,\", ((char *)&now)[i]);",
7683 " printf(\"\\n\tVector: \");",
7684 " for (i = 0; i < n; i++)",
7685 " printf(\"%%d,\", v[i]);",
7686 " printf(\"\\n\");",
7693 "g_store(char *vin, int nin, uchar pbit)",
7695 " int ret_val = 1;",
7697 " static uchar Info[MA+1];",
7699 " n = compress(vin, nin);",
7700 " v = (uchar *) &comp_now;",
7703 " v = (uchar *) vin;",
7706 " { printf(\"pan: error, MA too small, recompile pan.c\");",
7707 " printf(\" with -DMA=N with N>%%d\\n\", n);",
7708 " Uerror(\"aborting\");",
7710 " if (n > (int) maxgs)",
7711 " { maxgs = (uint) n;",
7713 " for (i = 0; i < n; i++)",
7714 " { Info[i] = v[i];",
7716 " for ( ; i < MA-1; i++)",
7719 " Info[MA-1] = pbit;",
7720 " if (a_cycles) /* place _a_t at the end */",
7721 " { Info[MA] = Info[0];",
7726 " e_critical(BFS_STATE); /* bfs_par / g_store */",
7728 "#if NCORE>1 && !defined(SEP_STATE)",
7729 " enter_critical(GLOBAL_LOCK); /* crude, but necessary */",
7730 " /* to make this mode work, also replace emalloc with grab_shared inside store MA routines */",
7733 " if (!dfa_store(Info))",
7736 " && depth > A_depth)",
7737 " { Info[MA] &= ~(1|16|32); /* _a_t */",
7738 " if (dfa_member(MA))", /* was !dfa_member(MA) */
7739 " { Info[MA-1] = 4; /* off-stack bit */",
7741 " if (!dfa_member(MA-1))",
7744 " printf(\"intersected 1st dfs stack\\n\");",
7750 " printf(\"new state\\n\");",
7756 " { Info[MA-1] = 1; /* proviso bit */",
7758 " trpt->proviso = dfa_member(MA-1);",
7760 " Info[MA-1] = 4; /* off-stack bit */",
7761 " if (dfa_member(MA-1))",
7762 " { ret_val = 1; /* off-stack */",
7764 " printf(\"old state\\n\");",
7767 " { ret_val = 2; /* on-stack */",
7769 " printf(\"on-stack\\n\");",
7777 " printf(\"old state\\n\");",
7781 " x_critical(BFS_STATE);",
7783 "#if NCORE>1 && !defined(SEP_STATE)",
7784 " leave_critical(GLOBAL_LOCK);",
7786 " return ret_val; /* old state */",
7790 "#if defined(BITSTATE) && defined(LC)",
7792 "compact_stack(char *vin, int n)", /* special case of HC4 */
7794 " s_hash((uchar *)vin, n); /* sets K1 and K2 */",
7796 " delta++; /* room for state[0] |= 128 */",
7798 " memcpy((char *) &comp_now + delta, (char *) &K1, WS);",
7800 " memcpy((char *) &comp_now + delta, (char *) &K2, WS);",
7801 " delta += WS; /* use all available bits */",
7808 "sv_populate(void)",
7809 "{ int i, cnt = 0;",
7810 " TRIX_v6 **base = processes;",
7811 " int bound = now._nr_pr; /* MAXPROC+1; */",
7813 " printf(\"%%4d: sv_populate\\n\", depth);",
7816 " for (i = 0; i < bound; i++)",
7817 " { if (base[i] != NULL)",
7819 " int m, n; uchar *v;",
7821 " if (base[i]->modified == 0)",
7824 " printf(\"%%4d: %%s %%d not modified\\n\",",
7825 " depth, (base == processes)?\"proc\":\"chan\", i);",
7830 " base[i]->modified = 0;",
7834 " if (base == processes)",
7835 " { ((P0 *)pptr(i))->_pid = 0;",
7838 " n = base[i]->psize;",
7839 " v = base[i]->body;",
7840 " s_hash(v, n); /* sets j1_spin */",
7841 " tmp = H_tab[j1_spin];",
7842 " if (!tmp) /* new */",
7843 " { tmp = grab_state(n);",
7844 " H_tab[j1_spin] = tmp;",
7845 " m = 1; /* non-zero */",
7847 " { H_el *ntmp, *olst = (H_el *) 0;",
7848 " for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
7849 " { m = memcmp(((char *)&(tmp->state)), v, n);",
7850 " if (m == 0) /* match */",
7852 " } else if (m < 0) /* insert */",
7853 " { ntmp = grab_state(n);",
7854 " ntmp->nxt = tmp;",
7856 " H_tab[j1_spin] = ntmp;",
7858 " olst->nxt = ntmp;",
7861 " } else if (!tmp->nxt) /* append */",
7862 " { tmp->nxt = grab_state(n);",
7867 " { memcpy((char *)&(tmp->state), v, n);",
7868 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)",
7869 " tmp->m_K1 = K1; /* set via s_hash */",
7872 " { if (base == processes)",
7873 " { _p_count[i]++;",
7875 " { _c_count[i]++;",
7877 " now._ids_[cnt++] = (char *)&(tmp->state);",
7879 " if (base == processes)",
7880 " { ((P0 *)pptr(i))->_pid = i;",
7881 " if (BASE > 0 && i > 0)",
7882 " { ((P0 *)pptr(i))->_pid -= BASE;",
7887 if a process appears or disappears: always secure a full sv_populate
7888 (channels come and go only with a process)
7890 only one process can disappear per step
7891 but any nr of channels can be removed at the same time
7892 if a process disappears, all subsequent entries
7893 are then in the wrong place in the _ids_ list
7894 and need to be recomputed
7895 but we do not need to fill out with zeros
7896 because vsize prevents them being used
7898 " /* do the same for all channels */",
7899 " if (base == processes)",
7900 " { base = channels;",
7901 " bound = now._nr_qs; /* MAXQ+1; */",
7906 "#if !defined(BFS_PAR) || (!defined(BITSTATE) && !defined(USE_TDH))",
7908 "h_store(char *vin, int nin) /* hash table storage */",
7910 " H_el *tmp, *olst = (H_el *) 0;",
7911 " char *v; int n, m=0;",
7916 " sv_populate(); /* update proc and chan ids */",
7918 " #ifdef NOCOMP", /* defined by BITSTATE */
7919 " #if defined(BITSTATE) && defined(LC)",
7920 " if (S_Tab == H_tab)",
7921 " { v = (char *) &comp_now;",
7922 " n = compact_stack(vin, nin);",
7924 " { v = vin; n = nin;",
7927 " v = vin; n = nin;",
7930 " v = (char *) &comp_now;",
7932 " rem_a = now._a_t;", /* new 5.0 */
7933 " now._a_t = 0;", /* for hashing/state matching to work right */
7935 " n = compress(vin, nin);", /* with HC, this calls s_hash -- but on vin, not on v... */
7937 " now._a_t = rem_a;", /* new 5.0 */
7939 /* with HC4 -a, compress copies K1 and K2 into v[], leaving v[0] free for the a-bit */
7942 " { v[0] = 0; /* _a_t */",
7944 " if (S_A > NFAIR)",
7945 " for (m = 0; m < NFAIR; m++)",
7946 " v[m+1] = 0; /* _cnt[] */",
7952 " #if !defined(HC) && !(defined(BITSTATE) && defined(LC))",
7953 " s_hash((uchar *)v, n);",
7955 " /* for BFS_PAR we can only get here in BITSTATE mode */",
7956 " /* and in that case we don't use locks */",
7957 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
7958 " e_critical(BFS_ID); /* bfs_par / h_store */",
7960 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
7961 " enter_critical(CS_ID);",
7963 " tmp = H_tab[j1_spin];",
7965 " { tmp = grab_state(n);", /* no zero-returns with bfs_par */
7968 " { /* if we get here -- we've already issued a warning */",
7969 " /* but we want to allow the normal distributed termination */",
7970 " /* to collect the stats on all cpus in the wrapup */",
7971 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
7972 " leave_critical(CS_ID);",
7974 " return 1; /* allow normal termination */",
7977 " H_tab[j1_spin] = tmp;",
7979 " { for (;; hcmp++, olst = tmp, tmp = tmp->nxt)",
7980 " { /* skip the _a_t and the _cnt bytes */",
7982 " if (tmp->ln != 0)",
7983 " { if (!tmp->nxt) goto Append;",
7987 " m = memcmp(((char *)&(tmp->state)) + S_A, ",
7988 " v + S_A, n - S_A);",
7996 " #if !defined(SAFETY) && !defined(NOCOMP)",
7998 " { if ((((char *)&(tmp->state))[0] & V_A) != V_A)",
7999 " { wasnew = 1; nShadow++;",
8000 " ((char *)&(tmp->state))[0] |= V_A;",
8003 " if (S_A > NFAIR)",
8004 " { /* 0 <= now._cnt[now._a_t&1] < MAXPROC */",
8005 " uint ci, bp; /* index, bit pos */",
8006 " ci = (now._cnt[now._a_t&1] / 8);",
8007 " bp = (now._cnt[now._a_t&1] - 8*ci);",
8008 " if (now._a_t&1) /* use tail-bits in _cnt */",
8009 " { ci = (NFAIR - 1) - ci;",
8010 " bp = 7 - bp; /* bp = 0..7 */",
8012 " ci++; /* skip over _a_t */",
8013 " bp = 1 << bp; /* the bit mask */",
8014 " if ((((char *)&(tmp->state))[ci] & bp)==0)",
8019 " ((char *)&(tmp->state))[ci] |= bp;",
8022 " /* else: wasnew == 0, i.e., old state */",
8028 " Lstate = (H_el *) tmp; /* h_store */",
8032 "#ifndef SAFETY", /* or else wasnew == 0 */
8034 " { Lstate = (H_el *) tmp; /* h_store */",
8035 " tmp->tagged |= V_A;",
8036 " if ((now._a_t&1)",
8037 " && (tmp->tagged&A_V)",
8038 " && depth > A_depth)",
8043 " printf(\"cpu%%d: \", core_id);",
8045 " printf(\"1st dfs-stack intersected on state %%d+\\n\",",
8046 " (int) tmp->st_id);",
8049 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8050 " x_critical(BFS_ID);",
8052 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8053 " leave_critical(CS_ID);",
8060 " printf(\"cpu%%d: \", core_id);",
8062 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
8065 " dumpstate(1, (char *)&(tmp->state),n,tmp->tagged);",
8067 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8068 " x_critical(BFS_ID);",
8070 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8071 " leave_critical(CS_ID);",
8076 " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)",
8077 " { Lstate = (H_el *) tmp; /* h_store */",
8079 " /* already on current dfs stack */",
8080 " /* but may also be on 1st dfs stack */",
8081 " if ((now._a_t&1)",
8082 " && (tmp->tagged&A_V)",
8084 " && depth > A_depth",
8085 /* new (Zhang's example) */
8087 " && (!fairness || now._cnt[1] <= 1)",
8095 " printf(\"cpu%%d: \", core_id);",
8097 " printf(\"\tStack state %%d\\n\", (int) tmp->st_id);",
8100 " dumpstate(0, (char *)&(tmp->state),n,tmp->tagged);",
8102 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8103 " x_critical(BFS_ID);",
8105 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8106 " leave_critical(CS_ID);",
8108 " return 2; /* match on stack */",
8115 " printf(\"cpu%%d: \", core_id);",
8117 " printf(\"\tNew state %%d+\\n\", (int) tmp->st_id);",
8120 " dumpstate(1, (char *)&(tmp->state), n, 0);",
8122 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8123 " x_critical(BFS_ID);",
8125 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8126 " leave_critical(CS_ID);",
8133 " printf(\"cpu%%d: \", core_id);",
8135 " printf(\"\tOld state %%d\\n\", (int) tmp->st_id);",
8138 " dumpstate(0, (char *)&(tmp->state), n, 0);",
8141 " #ifdef CONSERVATIVE",
8142 " if (tmp->ctx_low > trpt->sched_limit)",
8143 " { tmp->ctx_low = trpt->sched_limit;",
8144 " tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%%8); /* new */",
8147 " printf(\"cpu%%d: \", core_id);",
8149 " printf(\"\t\tRevisit with fewer context switches\\n\");",
8152 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8153 " x_critical(BFS_ID);",
8155 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8156 " leave_critical(CS_ID);",
8159 " } else if ((tmp->ctx_low == trpt->sched_limit",
8160 " && (tmp->ctx_pid[(now._last)/8] & ( 1 << ((now._last)%%8) )) == 0 ))",
8161 " { tmp->ctx_pid[(now._last)/8] |= 1 << ((now._last)%%8); /* add */",
8164 " printf(\"cpu%%d: \", core_id);",
8166 " printf(\"\t\tRevisit with same nr of context switches\\n\");",
8169 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8170 " x_critical(BFS_ID);",
8172 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8173 " leave_critical(CS_ID);",
8180 " if (tmp->D > depth)",
8181 " { tmp->D = depth;",
8184 " printf(\"cpu%%d: \", core_id);",
8186 " printf(\"\t\tReVisiting (from smaller depth)\\n\");",
8189 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8190 " x_critical(BFS_ID);",
8192 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8193 " leave_critical(CS_ID);",
8196 a possible variation of iterative search for shortest counter-example
8197 (pan -i and pan -I) suggested by Pierre Moro (for safety properties):
8198 state revisits on shorter depths do not start until after
8199 the first counter-example is found. this assumes that the max search
8200 depth is set large enough that a first (possibly long) counter-example
8202 if set too short, this variant can miss the counter-example, even if
8203 it would otherwise be shorter than the depth-limit.
8204 (p.m. unsure if this preserves the guarantee of finding the
8205 shortest counter-example - so not enabled by default)
8206 " if (errors > 0 && iterative)", /* Moro */
8211 " #if (defined(BFS) && defined(Q_PROVISO)) || NCORE>1",
8212 " Lstate = (H_el *) tmp; /* h_store */",
8214 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8215 " x_critical(BFS_ID);",
8217 " #if NCORE>1 && !defined(SEP_STATE) && !defined(BITSTATE)",
8218 " leave_critical(CS_ID);",
8220 " return 1; /* match outside stack */",
8221 " } else if (m < 0)",
8222 " { /* insert state before tmp */",
8223 " ntmp = grab_state(n);",
8227 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
8228 " leave_critical(CS_ID);",
8230 " return 1; /* allow normal termination */",
8233 " ntmp->nxt = tmp;",
8235 " H_tab[j1_spin] = ntmp;",
8237 " olst->nxt = ntmp;",
8240 " } else if (!tmp->nxt)",
8241 " { /* append after tmp */",
8245 " tmp->nxt = grab_state(n);",
8249 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
8250 " leave_critical(CS_ID);",
8252 " return 1; /* allow normal termination */",
8260 " tmp->st_id = (unsigned) nstates;",
8262 " printf(\"cpu%%d: \", core_id);",
8265 " printf(\" Push state %%d\\n\", ((int) nstates) - 1);",
8267 " printf(\" New state %%d\\n\", (int) nstates);",
8270 " #if defined(BCS)",
8271 " tmp->ctx_low = trpt->sched_limit;",
8272 " #ifdef CONSERVATIVE",
8273 " tmp->ctx_pid[(now._last)/8] = 1 << ((now._last)%%8); /* new limit */",
8276 " #if !defined(SAFETY) || defined(REACH)",
8279 " #if !defined(SAFETY) && !defined(NOCOMP)",
8283 " if (S_A > NFAIR)",
8284 " { uint ci, bp; /* as above */",
8285 " ci = (now._cnt[now._a_t&1] / 8);",
8286 " bp = (now._cnt[now._a_t&1] - 8*ci);",
8288 " { ci = (NFAIR - 1) - ci;",
8289 " bp = 7 - bp; /* bp = 0..7 */",
8291 " v[1+ci] = 1 << bp;",
8296 " #if defined(AUTO_RESIZE) && !defined(BITSTATE)",
8299 " memcpy(((char *)&(tmp->state)), v, n);",
8300 " #ifdef FULLSTACK",
8301 " tmp->tagged = (S_A)?V_A:(depth+1);",
8303 " dumpstate(-1, v, n, tmp->tagged);",
8305 " Lstate = (H_el *) tmp; /* end of h_store */",
8308 " dumpstate(-1, v, n, 0);",
8311 " Lstate = (H_el *) tmp; /* end of h_store */",
8315 " #if defined(BFS_PAR) && !defined(BFS_SEP_HASH)",
8316 " x_critical(BFS_ID);",
8319 " #ifdef V_PROVISO",
8320 " tmp->cpu_id = core_id;",
8322 " #if !defined(SEP_STATE) && !defined(BITSTATE)",
8323 " leave_critical(CS_ID);",
8328 "}", /* end of h_store */
8329 "#endif", /* !BFS_PAR || !USE_TDH */
8332 "o_hash32(uchar *s, int len, int h) /* 32-bit, like d_sfh, but with seed */",
8339 " for ( ; len > 0; len--)",
8340 " { h += get16bits(s);",
8341 " tmp = (get16bits(s+2) << 11) ^ h;",
8342 " h = (h << 16) ^ tmp;",
8343 " s += 2*sizeof(uint16_t);",
8347 " case 3: h += get16bits(s);",
8349 " h ^= s[sizeof(uint16_t)] << 18;",
8352 " case 2: h += get16bits(s);",
8356 " case 1: h += *s;",
8371 "o_hash64(uchar *kb, int nbytes, int seed)", /* 64-bit hash */
8373 " uint64_t a, b, c, n;",
8374 " const uint64_t *k = (uint64_t *) kb;",
8375 " n = nbytes/WS; /* nr of 8-byte chunks */",
8376 " /* extend to multiple of words, if needed */",
8377 " a = WS - (nbytes %% WS);",
8378 " if (a > 0 && a < WS)",
8380 " bp = kb + nbytes;",
8382 " case 7: *bp++ = 0; /* fall thru */",
8383 " case 6: *bp++ = 0; /* fall thru */",
8384 " case 5: *bp++ = 0; /* fall thru */",
8385 " case 4: *bp++ = 0; /* fall thru */",
8386 " case 3: *bp++ = 0; /* fall thru */",
8387 " case 2: *bp++ = 0; /* fall thru */",
8388 " case 1: *bp = 0;",
8391 " a = (uint64_t) seed;",
8392 " b = HASH_CONST[HASH_NR];",
8393 " c = 0x9e3779b97f4a7c13LL; /* arbitrary */",
8402 " c += (((uint64_t) nbytes)<<3);",
8404 " case 2: b += k[1];",
8405 " case 1: a += k[0];",
8413 "#if defined(USE_TDH) && !defined(WIN32) && !defined(WIN64)",
8415 some problems with this storage mode:
8417 0. pre-allocates full hash-table with slots equal to max statevector size
8418 e.g. with -w26 we allocate 2^26 (64 M) slots of VECTORSZ large
8419 which can accomodate up to 64 M states
8420 once you get close to or exceed the max, the search aborts
8421 with a 'hashtable full' message
8422 in HC mode the max storage needed per state is more modest and independent
8423 of the maximum vectorsize; which makes this mode attractive as a default
8425 1. does not support PO reduction through the Lstate->ostate->tagged
8426 to distinguish open from closed states - this can reduce states by 50%
8427 could add this as another bit from the hash value
8428 e.g., could add it in HC mode to the first hash?
8430 2. the same state may be stored multiple times
8435 " #define T_HC BFS_HC",
8440 " #if T_HC<1 || T_HC>4",
8441 " #error \"BFS_HC must be 1, 2, 3, or 4 (default is 2)\"",
8445 "#define T_ROW 6", /* related to cache line size */
8446 "#define T_ROW_SIZE (1<<T_ROW)",
8447 "#define T_ROW_MASK -(1<<T_ROW)",
8449 "#define T_STAT 1 /* status bit */",
8451 " #define T_VSZ VECTORSZ/4 /* compressed vectorsize */",
8454 "static volatile char *ohash_sd; /* state data */",
8455 "static volatile uint32_t *ohash_hv; /* hash values */",
8456 "static ulong ohash_max;",
8457 "static ulong ohash_mask;",
8459 "#if defined(USE_TDH) && defined(Q_PROVISO)",
8460 " static volatile uchar *ohash_inq; /* open/closed flag BFS_INQ */",
8463 " static uint32_t ohash_hc[T_HC];",
8464 " static ulong ohash_hc_sz;",
8468 "init_HT(ulong x) /* USE_TDH cygwin/linux */",
8469 "{ x = x / (ulong) sizeof(H_el *); /* room for x pointers */",
8471 " printf(\"prealloc x %%lu v %%d x*v %%lu\\n\",",
8472 " x, T_VSZ, (ulong) (x * (ulong)T_VSZ));",
8475 " if (!(x * (ulong) T_VSZ > x))",
8476 " { Uerror(\"assertion x * (ulong) T_VSZ > x fails\");",
8478 " #ifdef BFS_SEP_HASH",
8479 " ohash_sd = (char *) emalloc(x * (ulong) T_VSZ);",
8481 " ohash_sd = (volatile char *) sh_pre_malloc(x * (ulong) T_VSZ);",
8483 "#else", /* assume T_HC >= 1, and normally 2 */
8484 " ohash_hc_sz = (ulong) (T_HC * (ulong) sizeof(uint32_t));",
8485 " if (!(x * ohash_hc_sz > x))", /* watch for overflow */
8486 " { Uerror(\"assertion x * ohash_hc_sz > x fails\");",
8488 " #ifdef BFS_SEP_HASH",
8489 " ohash_sd = (char *) emalloc(x * ohash_hc_sz);",
8491 " ohash_sd = (volatile char *) sh_pre_malloc(x * ohash_hc_sz);",
8494 "#ifdef BFS_SEP_HASH",
8495 " ohash_hv = (uint32_t *) emalloc(x * (ulong) sizeof(uint32_t));",
8497 " ohash_hv = (volatile uint32_t *) sh_pre_malloc(x * (ulong) sizeof(uint32_t));",
8499 " ohash_mask = (((ulong)1)<<ssize)-1;",
8500 " ohash_max = (((ulong)1)<<ssize)/100;",
8501 "#if defined(USE_TDH) && defined(Q_PROVISO)",
8502 " #ifdef BFS_SEP_HASH",
8503 " ohash_inq = (uchar *) emalloc(x * (ulong) sizeof(uchar));",
8505 " ohash_inq = (volatile uchar *) sh_pre_malloc(x * (ulong) sizeof(uchar));",
8510 "static int h_table_full;",
8513 "bfs_mark_live(void)",
8516 " trpt->o_pm &= ~2;",
8518 " bfs_printf(\"check to mark\\n\");",
8520 " for (i = 0; i < (int) now._nr_pr; i++)",
8521 " { P0 *ptr = (P0 *) pptr(i);",
8522 " if (accpstate[ptr->_t][ptr->_p])",
8523 " { trpt->o_pm |= 2;",
8524 " now._l_bnd = L_bound;",
8525 " now._l_sds = (uchar *) 0;",
8527 " bfs_printf(\"mark state live\\n\");",
8533 "bfs_check_live(uchar b, uchar *s)",
8534 "{ /* assert(b>0); */",
8535 " now._l_bnd = b-1; /* decrease bound */",
8537 " bfs_printf(\"check live %%d\\n\", b);",
8539 " if (b == L_bound && boq == -1)", /* never mid rv */
8540 " { now._l_sds = (uchar *) Lstate; /* new target */",
8542 " { now._l_sds = s; /* restore target */",
8543 " if (s == (uchar *) Lstate)",
8544 " { depthfound = depth - (BASE+1)*(L_bound - now._l_bnd - 1);",
8545 " uerror(\"accept cycle found\");",
8546 " depthfound = -1;",
8548 " now._l_sds = (uchar *) 0;",
8551 " bfs_printf(\"set l_bound to %%d -- sds %%p\\n\", b-1, (void *) now._l_sds);",
8555 "/* closed hashing with locality - similar to ltsmin */",
8557 "o_store(const char *vin, int nin)",
8558 "{ int i, seed = 0;",
8559 " ulong hash_v, ix, ex;",
8560 " uint32_t T_BUSY, T_DONE;",
8561 " volatile uint32_t *t_entry;",
8563 " ulong vs = ohash_hc_sz;",
8565 " ulong vs = (ulong) T_VSZ;",
8568 " uchar o_bnd, *o_sds;",
8570 "#ifndef STOP_ON_FULL",
8571 " if (h_table_full)",
8576 " if (now._l_bnd == 0)",
8577 " { bfs_mark_live();",
8581 " { bfs_printf(\"non-markable state %%d\\n\", now._l_bnd);",
8584 " o_bnd = now._l_bnd;",
8585 " o_sds = now._l_sds;",
8586 " now._l_bnd = (o_bnd)?1:0; /* mark nested phase of bounded search */",
8587 " now._l_sds = (uchar *) 0;",
8589 "#if !defined(HC) && !defined(T_NOCOMP)",
8590 " nin = compress((char *)vin, nin);",
8591 " vin = (char *) &comp_now;",
8593 " do { o_hash((uchar *)vin, nin, seed++);",
8595 " } while (hash_v == T_FREE || hash_v == T_STAT); /* unlikely, hash_v 0 or 1 */",
8597 " T_BUSY = ((uint32_t) hash_v & ~((uint32_t) T_STAT)); /* hash with status bit 0 */",
8598 " T_DONE = ((uint32_t) hash_v | ((uint32_t) T_STAT)); /* hash with status bit 1 */",
8600 " d_hash((uchar *)vin, nin);", /* HC */
8601 " ohash_hc[0] = (uint32_t) K1;",
8603 " ohash_hc[1] = (uint32_t) (K1>>32);", /* assumes ulong = 64 bits */
8606 " ohash_hc[2] = (uint32_t) K2;",
8609 " ohash_hc[3] = (uint32_t) (K2>>32);",
8612 " while (seed < ohash_max)",
8613 " { ix = hash_v & ohash_mask;",
8614 " ex = (ix & T_ROW_MASK) + T_ROW_SIZE;",
8615 " for (i = 0; i < T_ROW_SIZE; i++)",
8616 " { t_entry = (uint32_t *) &ohash_hv[ix];",
8617 " if (*t_entry == T_FREE && cas(t_entry, T_FREE, T_BUSY))",
8620 " memcpy((char *) &ohash_sd[ix * vs], vin, nin);",
8622 " memcpy((char *) &ohash_sd[ix * vs], (char *) ohash_hc, vs);",
8624 "#if defined(USE_TDH) && defined(Q_PROVISO)",
8625 " ohash_inq[ix] = (uchar) BFS_INQ;",
8626 " Lstate = (H_el *) &ohash_inq[ix];",
8628 " *t_entry = T_DONE;",
8631 " bfs_printf(\"New state %%p [%%p]\\n\",",
8632 " (void *) Lstate, (void *) o_sds);",
8634 " bfs_printf(\"New state %%p\\n\", (void *) Lstate);",
8638 " if (o_bnd) { bfs_check_live(o_bnd, o_sds); }",
8640 " return 0; /* New State */",
8642 " while (*t_entry == T_BUSY)",
8643 " { usleep(2); /* wait */",
8645 " if (*t_entry == T_DONE /* (first) hash matches, check data */",
8647 " && memcmp((char *) &ohash_sd[ix * vs], vin, nin) == 0)",
8649 " && memcmp((char *) &ohash_sd[ix * vs], (char *) ohash_hc, vs) == 0)",
8652 "#if defined(USE_TDH) && defined(Q_PROVISO)",
8653 " Lstate = (H_el *) &ohash_inq[ix];",
8657 " bfs_printf(\"Old state %%p [%%p]\\n\",",
8658 " (void *) Lstate, (void *) o_sds);",
8660 " bfs_printf(\"Old state %%p\\n\", (void *) Lstate);",
8664 " if (o_bnd) { bfs_check_live(o_bnd, o_sds); }",
8666 " return 1; /* Old State */",
8669 " ix = (ix==ex) ? ex - T_ROW_SIZE : ix;",
8671 " /* find a new slot: */",
8672 " do { o_hash((uchar *)vin, nin, (int) (hash_v + seed++));",
8674 " } while (hash_v == T_FREE || hash_v == T_STAT);",
8675 " T_BUSY = ((uint32_t) hash_v & ~((uint32_t) T_STAT));",
8676 " T_DONE = ((uint32_t) hash_v | ((uint32_t) T_STAT));",
8678 "#ifdef STOP_ON_FULL",
8679 " Uerror(\"hash table full\");",
8680 " /* no return from Uerror */",
8682 " if (!h_table_full)",
8683 " { h_table_full++;",
8684 " if (who_am_i == 0)",
8685 " { bfs_printf(\"hash table is full\\n\");",
8688 " bfs_punt++; /* counts this as a lost state */",
8691 " now._l_bnd = 0; /* no more checking */",
8692 " now._l_sds = (uchar *) 0;",
8694 " return 1; /* technically should be 0, but we want to throttle down */",
8696 "#endif", /* USE_TDH && !WIN32 && !WIN64 */
8697 "#endif", /* !BITSTATE || FULLSTACK */
8698 "#include TRANSITIONS",