1 /***** spin: pangen7.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 *pan_par[] = { /* generates pan.p */
10 "#include <sys/ipc.h>",
11 "#include <sys/shm.h>",
12 "#include <time.h>", /* for nanosleep */
13 "#include <assert.h>",
14 "#include <limits.h>",
16 "#include <unistd.h>", /* for rmdir */
17 "#include <sys/stat.h>", /* for mkdir */
18 "#include <sys/types.h>",
19 "#include <fcntl.h>", /* for open */
22 "#define Max(a,b) (((a)>(b))?(a):(b))",
24 " #define WAIT_MAX 2 /* seconds */",
26 "#define BFS_GEN 2 /* current and next generation */",
28 "typedef struct BFS_Slot BFS_Slot;",
29 "typedef struct BFS_shared BFS_shared;",
30 "typedef struct BFS_data BFS_data;",
34 " enum bfs_types type; /* message type */",
36 " BFS_State *s_data; /* state data */",
38 " BFS_Slot *nxt; /* linked list */",
49 " ulong memory_left;",
52 " int override; /* after crash, if another proc clears locks */",
55 "struct BFS_shared { /* about 13K for BFS_MAXPROCS=16 and BFS_MAXLOCKS=1028 */",
56 " volatile ulong quit; /* set to signal termination -- one word */",
57 " volatile ulong started;",
59 " volatile uchar sh_owner[BFS_MAXLOCKS]; /* optional */",
61 " volatile uchar in_count[BFS_MAXLOCKS]; /* optional */",
63 " volatile int sh_locks[BFS_MAXLOCKS];",
64 " volatile ulong wait_count[BFS_MAXLOCKS]; /* optional */",
66 " volatile BFS_data bfs_data[BFS_MAXPROCS];",
67 " volatile uchar bfs_flag[BFS_MAXPROCS]; /* running 0, normal exit 1, abnormal 2 */",
68 " volatile uchar bfs_idle[BFS_MAXPROCS]; /* set when all input queues are empty */",
70 " volatile uchar bfs_out_cnt[BFS_MAXPROCS]; /* set when core writes a state */",
74 " #define BFS_NORECYCLE",
76 " #error BFS_QSZ must be positive",
79 " #error BFS_QSZ cannot be combined with BFS_FIFO",
82 " #error BFS_QSZ cannot be combined with BFS_DISK",
84 " volatile BFS_Slot bfsq[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS][BFS_QSZ];",
85 " volatile uint bfs_ix[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
87 " volatile BFS_Slot *head[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
91 " volatile BFS_Slot *tail[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
92 " volatile BFS_Slot *dels[BFS_GEN][BFS_MAXPROCS][BFS_MAXPROCS];",
95 " volatile ulong logmem[1024];",
97 " volatile ulong mem_left;",
98 " volatile uchar *allocator; /* start of shared heap, must be last */",
101 "enum bfs_types { EMPTY = 0, STATE, DELETED };",
103 "extern volatile uchar *bfs_get_shared_mem(key_t, size_t);",
104 "extern BFS_Slot * bfs_new_slot(BFS_Trail *);",
105 "extern BFS_Slot * bfs_prep_slot(BFS_Trail *, BFS_Slot *);",
106 "extern BFS_Slot * bfs_next(void);",
107 "extern BFS_Slot * bfs_pack_state(Trail *, BFS_Trail *, int, BFS_Slot *);",
108 "extern SV_Hold * bfs_new_sv(int);",
110 "extern EV_Hold * bfs_new_sv_mask(int);",
112 "extern BFS_Trail * bfs_grab_trail(void);",
113 "extern BFS_Trail * bfs_unpack_state(BFS_Slot *);",
114 "extern int bfs_all_empty(void);",
115 "extern int bfs_all_idle(void);",
116 "extern int bfs_all_running(void);",
117 "extern int bfs_idle_and_empty(void);",
118 "extern size_t bfs_find_largest(key_t);",
120 "extern void bfs_clear_locks(void);",
121 "extern void bfs_drop_shared_memory(void);",
122 "extern void bfs_explore_state(BFS_Slot *);",
123 "extern void bfs_initial_state(void);",
124 "extern void bfs_mark_done(int);",
125 "extern void bfs_printf(const char *fmt, ...);",
126 "extern void bfs_push_state(Trail *, BFS_Trail *, int);",
127 "extern void bfs_recycle(BFS_Slot *);",
128 "extern void bfs_release_trail(BFS_Trail *);",
129 "extern void bfs_run(void);",
130 "extern void bfs_setup_mem(void);",
131 "extern void bfs_setup(void);",
132 "extern void bfs_shutdown(const char *);",
133 "extern void bfs_statistics(void);",
134 "extern void bfs_store_state(Trail *, short);",
135 "extern void bfs_set_toggle(void);",
136 "extern void bfs_update(void);",
139 " #error cannot combine -DMA with -DBFS_PAR",
140 " /* would require us to parallelize g_store */",
143 " #error cannot combine -DBCS with -DBFS_PAR",
147 " #error cannot combine BFS_DISK and BFS_FIFO",
149 " extern void bfs_disk_start(void);",
150 " extern void bfs_disk_stop(void);",
151 " extern void bfs_disk_out(void);",
152 " extern void bfs_disk_inp(void);",
153 " extern void bfs_disk_iclose(void);",
154 " extern void bfs_disk_oclose(void);",
155 " int bfs_out_fd[BFS_MAXPROCS];",
156 " int bfs_inp_fd[BFS_MAXPROCS];",
159 "static BFS_shared *shared_memory;",
161 "static BFS_Slot *bfs_free_slot; /* local free list */",
163 "static BFS_Slot bfs_null;",
164 "static SV_Hold *bfs_svfree[VECTORSZ];",
165 "static uchar *bfs_heap; /* local pointer into heap */",
166 "static ulong bfs_left; /* local part of shared heap */",
168 "static void bfs_keep(EV_Hold *);",
170 "static long bfs_sent; /* nr msgs sent -- local to each process */",
171 "static long bfs_rcvd; /* nr msgs rcvd */",
172 "static long bfs_sleep_cnt; /* stats */",
173 "static long bfs_wcount;",
174 "static long bfs_gcount;",
175 "static ulong bfs_total_shared;",
176 "#ifdef BFS_STAGGER",
177 " static int bfs_stage_cnt = 0;",
178 " static void bfs_stagger_flush(void);",
180 "static int bfs_toggle; /* local variable, 0 or 1 */",
181 "static int bfs_qscan; /* scan input queues in order */",
182 "static ulong bfs_snapped;",
183 "static int shared_mem_id;",
185 "static int bfs_nps; /* no preselection */",
187 "ulong bfs_punt; /* states dropped for lack of memory */",
188 "#if defined(VERBOSE) || defined(BFS_CHECK)",
189 "static const char *bfs_sname[] = {",
190 " \"EMPTY\", /* 0 */",
191 " \"STATE\", /* 1 */",
192 " \"STATE\", /* 2 = DELETED */",
196 "static const char *bfs_lname[] = { /* match values defined in pangen2.c */",
197 " \"global lock\", /* BFS_GLOB */",
198 " \"ordinal\", /* BFS_ORD */",
199 " \"shared memory\", /* BFS_MEM */",
200 " \"print to stdout\", /* BFS_PRINT */",
201 " \"hashtable\", /* BFS_STATE */",
205 "static ulong bfs_count[DELETED+1]; /* indexed with bfs_types: EMPTY=0, STATE=1, DELETED=2 */",
207 "static int bfs_keep_state;",
210 "int who_am_i = 0; /* root */",
213 " int L_bound = L_BOUND;",
218 "bfs_dump_now(char *s)",
219 "{ int i; char *p = (char *) &now;",
221 " e_critical(BFS_PRINT);",
222 " printf(\"%%s\\t\", s);",
223 " printf(\"%%3lu: \", vsize);",
224 " for (i = 0; i < vsize; i++)",
225 " { printf(\"%%3d \", *p++);",
227 " printf(\" %%s\\noffsets:\\t\", s);",
228 " for (i = 0; i < now._nr_pr; i++)",
229 " { printf(\"%%3d \", proc_offset[i]);",
232 " x_critical(BFS_PRINT);",
236 "view_state(char *s) /* debugging */",
239 " e_critical(BFS_PRINT);",
240 " printf(\"cpu%%02d %%s: \", who_am_i, s);",
241 " p = (char *)&now;",
242 " for (i = 0; i < vsize; i++)",
243 " printf(\"%%3d, \", *p++);",
244 " printf(\"\\n\"); fflush(stdout);",
245 " x_critical(BFS_PRINT);",
250 "bfs_main(int ncores, int cycles)",
253 " { fprintf(stderr, \"pan: cycle detection is not supported in this mode\\n\");",
257 " if (ncores == 0) /* i.e., find out */",
260 " if ((fd = fopen(\"/proc/cpuinfo\", \"r\")) == NULL)",
261 " { /* cannot tell */",
262 " ncores = Cores; /* use the default */",
264 " { while (fgets(buf, sizeof(buf), fd))",
265 " { if (strncmp(buf, \"processor\", strlen(\"processor\")) == 0)",
271 " { printf(\"pan: %%d available cores\\n\", ncores+1);",
273 " if (ncores >= BFS_MAXPROCS)",
274 " { Cores = BFS_MAXPROCS-1; /* why -1? */",
275 " } else if (ncores < 1)",
278 " { Cores = ncores;",
280 " printf(\"pan: using %%d core%%s\\n\", Cores, (Cores>1)?\"s\":\"\");",
283 " bfs_disk_start();", /* create .spin */
285 " bfs_setup(); /* shared memory segments and fork */",
287 " if (who_am_i == 0)",
290 " bfs_statistics();",
291 " bfs_mark_done(1);",
292 " if (who_am_i == 0)",
299 " C_EXIT; /* trust that it defines a fct */",
301 " bfs_drop_shared_memory();",
306 "bfs_setup_mem(void)",
310 " bfs_null.type = EMPTY;",
312 " ntrpt = (Trail *) emalloc(sizeof(Trail));", /* just once */
314 " if ((key = ftok(\".\", (int) 'L')) == -1)",
315 " { perror(\"ftok shared memory\");",
318 " n = bfs_find_largest(key);",
319 " bfs_total_shared = (ulong) n;",
321 " shared_memory = (BFS_shared *) bfs_get_shared_mem(key, n); /* root */",
322 " shared_memory->allocator = (uchar *) shared_memory + sizeof(BFS_shared);",
323 " shared_memory->mem_left = (ulong) (n - sizeof(BFS_shared));",
327 "#ifndef BFS_RESERVE",
328 " #define BFS_RESERVE 5",
329 /* keep memory on global heap in reserve for first few cores */
330 /* that run out of their local allocation of shared mem */
331 /* 1~50 percent, 2~30 percent, 5~20 percent, >Cores=none */
333 " #if BFS_RESERVE<1",
334 " #error BFS_RESERVE must be at least 1",
339 "bfs_setup(void) /* executed by root */",
341 " ulong n; /* share of shared memory allocated to each core */",
343 " n = shared_memory->mem_left / (Cores + Cores/(BFS_RESERVE)); /* keep some reserve */",
345 " if ((n%%sizeof(void *)) != 0)",
346 " { n -= (n%%sizeof(void *)); /* align, without exceeding total */",
348 " for (i = 0; i < Cores-1; i++)",
351 " { bfs_printf(\"fork failed\\n\");",
355 " { who_am_i = i+1; /* 1..Cores-1 */",
359 " e_critical(BFS_MEM);",
360 " bfs_heap = (uchar *) shared_memory->allocator;",
361 " shared_memory->allocator += n;",
362 " shared_memory->mem_left -= n;",
363 " x_critical(BFS_MEM);",
367 " bfs_LowLim = n / (2 * (ulong) Cores);", /* 50% */
375 " bfs_disk_out();", /* create outqs */
377 " if (who_am_i == 0)",
378 " { bfs_initial_state();",
381 " #ifdef BFS_STAGGER",
382 " bfs_stagger_flush();",
384 " bfs_disk_oclose();", /* sync and close outqs */
387 " static int i_count;",
390 " srand(s_rand+HASH_NR);",
392 " bfs_toggle = 1 - bfs_toggle; /* after initial state */",
393 " e_critical(BFS_GLOB);",
394 " shared_memory->started++;",
395 " x_critical(BFS_GLOB);",
397 " while (shared_memory->started != Cores) /* wait for all cores to connect */",
407 " while (shared_memory->quit == 0)",
408 " { v = bfs_next(); /* get next message from current generation */",
409 " if (v->s_data) /* v->type == STATE || v->type == DELETED */",
410 " { bfs_count[STATE]++;",
412 " bfs_printf(\"GOT STATE (depth %%d, nr %%u)\\n\",",
413 " v->s_data->t_info->o_tt, v->s_data->nr);",
415 " /* last resort: start dropping states when out of memory */",
416 " if (bfs_left > 1024 || shared_memory->mem_left > 1024)",
417 " { bfs_explore_state(v);",
419 " { static int warned_loss = 0;",
420 " if (warned_loss == 0 && who_am_i == 0)",
422 " bfs_printf(\"out of shared memory - losing states\\n\");",
426 "#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)",
433 " { bfs_count[EMPTY]++;",
434 "#if defined(BFS_FIFO) && defined(BFS_CHECK)",
435 " assert(v->type == EMPTY);",
438 " if (who_am_i == 0)",
439 " { if (bfs_idle_and_empty())",
440 " { if (i_count++ > 10)",
441 " { shared_memory->quit = 1;",
445 " } else if (!bfs_all_running())",
446 " { bfs_shutdown(\"early termination\");",
449 " if (who_am_i == 0)",
450 " { if (bfs_all_idle()) /* wait for it */",
451 " { if (!bfs_all_empty()) /* more states to process */",
452 " { bfs_set_toggle();",
454 " } else /* done */",
455 " { shared_memory->quit = 1; /* step 4 */",
458 " { bfs_sleep_cnt++;",
461 " { /* wait for quit or idle bit to be reset by root */",
462 " while (shared_memory->bfs_idle[who_am_i] == 1",
463 " && shared_memory->quit == 0)",
464 " { if (bfs_all_running())",
465 " { bfs_sleep_cnt++;",
466 " usleep(10); /* new 6.2.3 */",
468 " { bfs_shutdown(\"early termination\");",
471 "do_toggle: bfs_qscan = 0;",
473 " bfs_disk_iclose();",
474 " bfs_disk_oclose();",
476 " bfs_toggle = 1 - bfs_toggle;",
482 " bfs_printf(\"toggle: recv from %%d, send to %%d\\n\",",
483 " bfs_toggle, 1 - bfs_toggle);",
489 " bfs_printf(\"done, sent %%5ld recvd %%5ld punt %%5lu sleep: %%ld\\n\",",
490 " bfs_sent, bfs_rcvd, bfs_punt, bfs_sleep_cnt);",
495 "bfs_report_mem(void) /* called from within wrapup() */",
497 " printf(\"%%9.3f total shared memory usage\\n\\n\",",
498 " ((double) bfs_total_shared - (double) bfs_left)/(1024.*1024.));",
502 "bfs_statistics(void)",
505 " enum bfs_types i;",
508 " bfs_printf(\"states sent %%7ld recvd %%7ld stored %%8g sleeps: %%4ld, %%4ld, %%ld\\n\",",
509 " bfs_sent, bfs_rcvd, nstates, bfs_wcount, bfs_gcount, bfs_sleep_cnt);",
510 " if (0) bfs_printf(\"states punted %%7lu\\n\", bfs_punt);",
512 " for (i = EMPTY; i <= DELETED; i++)",
513 " { if (bfs_count[i] > 0)",
514 " { bfs_printf(\"%%6s %%8lu\\n\",",
515 " bfs_sname[i], bfs_count[i]);",
520 " if (who_am_i == 0 && shared_memory)",
521 " { int i; ulong count = 0L;",
524 " e_critical(BFS_PRINT);",
527 " { printf(\"\\nlock-wait counts:\\n\");",
528 " for (i = 0; i < BFS_STATE; i++)",
529 " printf(\"%%16s %%9lu\\n\",",
530 " bfs_lname[i], shared_memory->wait_count[i]);",
532 " for (i = BFS_STATE; i < BFS_MAXLOCKS; i++)",
534 " printf(\" [%%6d] %%9lu\\n\",",
535 " i, shared_memory->wait_count[i]);",
536 " count += shared_memory->wait_count[i];",
538 " printf(\"%%16s %%9lu (avg per region)\\n\",",
539 " bfs_lname[BFS_STATE], count/(BFS_MAXLOCKS - BFS_STATE));",
543 " x_critical(BFS_PRINT);",
548 "bfs_snapshot(void)",
549 "{ clock_t stop_time;",
550 " double delta_time;",
551 " struct tms stop_tm;",
552 " volatile BFS_data *s;",
554 " e_critical(BFS_PRINT);",
555 " printf(\"cpu%%02d Depth= %%7lu States= %%8.3g Transitions= %%8.3g \",",
556 " who_am_i, mreached, nstates, nstates+truncs);",
557 " printf(\"Memory= %%9.3f\\t\", memcnt/1048576.);",
558 " printf(\"SharedMLeft= %%4lu \", bfs_left/1048576);",
559 " stop_time = times(&stop_tm);",
560 " delta_time = ((double) (stop_time - start_time))/((double) sysconf(_SC_CLK_TCK));",
561 " if (delta_time > 0.01)",
562 " { printf(\"t= %%6.3g R= %%6.0g\\n\", delta_time, nstates/delta_time);",
564 " { printf(\"t= %%6.3g R= %%6.0g\\n\", 0., 0.);",
567 " x_critical(BFS_PRINT);",
569 " s = &shared_memory->bfs_data[who_am_i];",
570 " s->mreached = (ulong) mreached;",
571 " s->vsize = (ulong) vsize;",
572 " s->errors = (int) errors;",
573 " s->memcnt = (double) memcnt;",
574 " s->nstates = (double) nstates;",
575 " s->nlinks = (double) nlinks;",
576 " s->truncs = (double) truncs;",
577 " s->memory_left = (ulong) bfs_left;",
578 " s->punted = (ulong) bfs_punt;",
579 " bfs_snapped++; /* for bfs_best */",
583 "bfs_shutdown(const char *s)",
585 " bfs_clear_locks(); /* in case we interrupted at a bad point */",
586 " if (!strstr(s, \"early \") || verbose)",
587 " { bfs_printf(\"stop (%%s)\\n\", s);",
590 " if (who_am_i == 0)",
596 " bfs_mark_done(2);",
600 "SV_Hold *bfs_free_hold;",
603 "bfs_get_hold(void)",
605 " if (bfs_free_hold)",
606 " { x = bfs_free_hold;",
607 " bfs_free_hold = bfs_free_hold->nxt;",
609 " { x = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));",
615 "bfs_unpack_state(BFS_Slot *n) /* called in bfs_explore_state */",
616 "{ BFS_Trail *otrpt;",
617 " BFS_State *bfs_t;",
620 " if (!n || !n->s_data || !n->s_data->t_info)",
621 " { bfs_Uerror(\"internal error\");",
623 " otrpt = (BFS_Trail *) ((BFS_State *) n->s_data)->t_info;",
625 " trpt->ostate = otrpt->ostate;",
626 " trpt->st = otrpt->st;",
627 " trpt->o_tt = otrpt->o_tt;",
628 " trpt->pr = otrpt->pr;",
629 " trpt->tau = otrpt->tau;",
630 " trpt->o_pm = otrpt->o_pm;",
631 " if (trpt->ostate)",
632 " trpt->o_t = t_id_lkup[otrpt->t_id];",
633 "#if defined(C_States) && (HAS_TRACK==1)",
634 " c_revert((uchar *) &(now.c_state[0]));",
636 " if (trpt->o_pm & 4) /* rv succeeded */",
637 " { return (BFS_Trail *) 0; /* revisit not needed */",
642 " if (trpt->o_pm & 8) /* rv attempt failed */",
645 " { trpt->tau &= ~8; /* break atomic */",
647 " } else if (trpt->tau&32) /* void preselection */",
648 " { trpt->tau &= ~32;",
649 " bfs_nps = 1; /* no preselection in repeat */",
652 " trpt->o_pm &= ~(4|8);",
653 " if (trpt->o_tt > mreached)",
654 " { static ulong nr = 0L, nc;",
655 " mreached = trpt->o_tt;",
656 " nc = (long) nstates/FREQ;",
661 " depth = trpt->o_tt;",
662 " if (depth >= maxdepth)",
666 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate;",
667 " if (x) x->o_pm |= 4; /* rv not failing */",
673 " bfs_printf(\"error: max search depth too small\\n\");",
676 " { bfs_uerror(\"depth limit reached\");",
678 " return (BFS_Trail *) 0;",
681 " bfs_t = n->s_data;",
683 " vsize = bfs_t->omask->sz;",
685 " vsize = ((State *) (bfs_t->osv))->_vsz;",
688 " boq = bfs_t->boq;",
691 "#if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
693 " if (((uchar *)(bfs_t->lstate))) /* if BFS_INQ is set */",
694 " { *((uchar *) bfs_t->lstate) = 0; /* turn it off */",
697 " if (bfs_t->lstate) /* bfs_par */",
698 " { bfs_t->lstate->tagged = 0; /* bfs_par state removed from q */",
702 " memcpy((char *) &now, (uchar *) bfs_t->osv, vsize);",
703 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
704 " Mask = (uchar *) bfs_t->omask->sv; /* in shared memory */",
707 " if (0) bfs_dump_now(\"got1\");",
713 " if (now._nr_pr > 0)",
715 " #if VECTORSZ>32000",
716 " proc_offset = (int *) bfs_t->omask->po;",
718 " proc_offset = (short *) bfs_t->omask->po;",
720 " proc_skip = (uchar *) bfs_t->omask->ps;",
722 " if (now._nr_qs > 0)",
724 " #if VECTORSZ>32000",
725 " q_offset = (int *) bfs_t->omask->qo;",
727 " q_offset = (short *) bfs_t->omask->qo;",
729 " q_skip = (uchar *) bfs_t->omask->qs;",
733 " vecsz = ((State *) bfs_t->osv)->_vsz;",
735 " assert(vecsz > 0 && vecsz < VECTORSZ);",
737 " { SV_Hold *x = bfs_get_hold();",
738 " x->sv = bfs_t->osv;",
739 " x->nxt = bfs_svfree[vecsz];",
740 " bfs_svfree[vecsz] = x;",
741 " bfs_t->osv = (State *) 0;",
744 " bfs_keep(bfs_t->omask);",
748 " if (0) bfs_dump_now(\"got2\");",
749 " if (0) view_state(\"after\");",
751 " return (BFS_Trail *) bfs_t->t_info;",
754 "bfs_initial_state(void)",
757 " assert(trpt != NULL);",
759 " trpt->ostate = (H_el *) 0;",
763 " trpt->tau |= 4; /* claim moves first */",
765 " bfs_store_state(trpt, boq); /* initial state : bfs_lib.c */",
769 " #define bfs_do_store(v, n) b_store(v, n)",
772 " #define bfs_do_store(v, n) o_store(v, n)",
774 " #define bfs_do_store(v, n) h_store(v, n)",
778 "#ifdef BFS_SEP_HASH",
780 "bfs_seen_before(void)",
781 "{ /* cannot set trpt->tau |= 64 to mark successors outside stack */",
782 " /* since the check is done remotely and the trpt value is gone */",
784 " if (!trpt->ostate /* initial state */",
785 " || ((trpt->tau&4) /* starting claim moves(s) */",
786 " && !(((BFS_Trail *)trpt->ostate)->tau&4))) /* prev move: prog */",
787 " { return 0; /* claim move: mid-state not stored */",
790 " if (!bfs_do_store((char *)&now, vsize)) /* sep_hash */",
791 " { nstates++; /* local count */",
792 " return 0; /* new state */",
795 " bfs_printf(\"seen before\\n\");",
798 " return 1; /* old state */",
803 "bfs_explore_state(BFS_Slot *v) /* generate all successors of v */",
804 "{ BFS_Trail *otrpt;",
810 " short II, To = BASE, From = (short) (now._nr_pr-1);",
811 " short oboq = boq;",
812 " uchar _n, _m, ot;",
814 " memset(ntrpt, 0, sizeof(Trail));",
815 " otrpt = bfs_unpack_state(v); /* BFS_Trail */",
817 " if (!otrpt) { return; } /* e.g., depth limit reached */",
819 " #if defined(VERBOSE)",
820 " bfs_printf(\"Unpacked state with l_bound %%d -- sds %%p\\n\",",
821 " now._l_bnd, now._l_sds);",
825 "#if defined(C_States) && (HAS_TRACK==1)",
826 " c_revert((uchar *) &(now.c_state[0]));",
829 "#ifdef BFS_SEP_HASH",
830 " if (bfs_seen_before()) return;",
833 "#ifdef VERI", /* could move to just before store_state */
834 " if (now._nr_pr == 0 /* claim terminated */",
835 " || stopstate[((Pclaim *)pptr(0))->_t][((Pclaim *)pptr(0))->_p])",
836 " { bfs_uerror(\"end state in claim reached\");",
839 " trpt->tau &= ~1; /* timeout off */",
841 " if (trpt->tau&4) /* claim move */",
842 " { trpt->tau |= (otrpt->tau)&1; /* inherit from prog move */",
843 " From = To = 0; /* claim */",
848 " if (boq == -1 && !(trpt->tau&8) && bfs_nps == 0)",
849 " for (II = now._nr_pr-1; II >= BASE; II -= 1)",
851 "Pickup: this = pptr(II);",
852 " tt = (int) ((P0 *)this)->_p;",
853 " ot = (uchar) ((P0 *)this)->_t;",
854 " if (trans[ot][tt]->atom & 8)",
855 " { t = trans[ot][tt];",
856 " if (t->qu[0] != 0)",
857 " { if (!q_cond(II, t))",
861 " trpt->tau |= 32; /* preselect marker */",
863 " bfs_printf(\"%%3ld: proc %%d PreSelected (tau=%%d)\\n\", ",
864 " depth, II, trpt->tau);",
868 " trpt->tau &= ~32;",
873 " { From = To = (short ) trpt->pr; /* atomic */",
875 " { From = now._nr_pr-1;",
878 "#if defined(VERI) || !defined(NOREDUCE) || defined(ETIM)",
879 "Repeat_two: /* MainLoop */",
882 " for (II = From; II >= To; II -= 1) /* all processes */",
885 " bfs_printf(\"proc %%d (%%d - %%d)\\n\", II, From, To);",
888 " if (boq != -1 && trpt->pr == II)",
889 " { continue; /* no rendezvous with same proc */",
893 " tt = (int) ((P0 *)this)->_p;",
894 " ot = (uchar) ((P0 *)this)->_t;",
895 " ntrpt->pr = (uchar) II;",
897 " trpt->o_pm &= ~1; /* no move yet */",
898 "#ifdef EVENT_TRACE",
899 " trpt->o_event = now._event;",
901 "#ifdef HAS_PRIORITY",
902 " if (!highest_priority(((P0 *)this)->_pid, II, t))",
906 " #ifdef HAS_PROVIDED",
907 " if (!provided(II, ot, tt, t))",
915 " for (t = trans[ot][tt]; t; t = t->nxt) /* all process transitions */",
918 " assert(t_id_lkup[t->t_id] == t); /* for reverse lookup in bfs_unpack_state */",
921 " if (0) bfs_printf(\"\\tproc %%d tr %%d\\n\", II, t->forw);",
925 " && E_state != t->e_trans)",
928 " /* trpt->o_t = */ ntrpt->o_t = t;",
931 " if (!(_m = do_transit(t, II)))",
934 " trpt->o_pm |= 1; /* we moved */",
935 " (trpt+1)->o_m = _m; /* for unsend */",
940 " e_critical(BFS_PRINT);",
941 " printf(\"%%3ld: proc %%d exec %%d, \",",
942 " depth, II, t->forw);",
943 " printf(\"%%d to %%d, %%s %%s %%s\",",
944 " tt, t->st, t->tp,",
945 " (t->atom&2)?\"atomic\":\"\",",
946 " (boq != -1)?\"rendez-vous\":\"\");",
947 " #ifdef HAS_UNLESS",
949 " printf(\" (escapes to state %%d)\", t->st);",
951 " printf(\" %%saccepting [tau=%%d]\\n\",",
952 " (trpt->o_pm&2)?\"\":\"non-\", trpt->tau);",
953 " x_critical(BFS_PRINT);",
956 " E_state = t->e_trans;",
958 " if (t->e_trans > 0 && boq != -1)",
959 " { fprintf(efd, \"error: rendezvous stmnt in the escape clause\\n\");",
960 " fprintf(efd, \" of unless stmnt not compatible with -DBFS\\n\");",
966 " { ((P0 *)this)->_p = t->st;",
968 " /* use the ostate ptr, with type *H_el, to temporarily store *BFS_Trail */",
969 "#ifdef BFS_NOTRAIL",
970 " ntrpt->ostate = (H_el *) 0; /* no error-traces in this mode */",
972 " ntrpt->ostate = (H_el *) otrpt; /* parent stackframe */",
974 " /* ntrpt->st = tt; * was already set above */",
976 " if (boq == -1 && (t->atom&2)) /* atomic */",
977 " { ntrpt->tau = 8; /* record for next move */",
979 " { ntrpt->tau = 0; /* no timeout or preselect etc */",
982 " ntrpt->tau |= trpt->tau&4; /* if claim, inherit */",
983 " if (boq == -1 && !(ntrpt->tau&8)) /* unless rv or atomic */",
984 " { if (ntrpt->tau&4) /* claim */",
985 " { ntrpt->tau &= ~4; /* switch to prog */",
987 " { ntrpt->tau |= 4; /* switch to claim */",
991 " { uchar obnd = now._l_bnd;",
992 " uchar *os = now._l_sds;",
994 " bfs_printf(\"saving bound %%d -- sds %%p\\n\", obnd, (void *) os);",
998 " bfs_store_state(ntrpt, oboq);",
999 "#ifdef EVENT_TRACE",
1000 " now._event = trpt->o_event;",
1002 " /* undo move and generate other successor states */",
1003 " trpt++; /* this is where ovals and ipt are set */",
1004 " do_reverse(t, II, _m); /* restore now. */",
1007 " bfs_printf(\"restoring bound %%d -- sds %%p\\n\", obnd, (void *) os);",
1009 " now._l_bnd = obnd;",
1010 " now._l_sds = os;",
1015 " e_critical(BFS_PRINT);",
1016 " printf(\"%%3ld: proc %%d \", depth, II);",
1017 " printf(\"reverses %%d, %%d to %%d,\", t->forw, tt, t->st);",
1018 " printf(\" %%s [abit=%%d,adepth=%%d,\", t->tp, now._a_t, 0);",
1019 " printf(\"tau=%%d,%%d]\\n\", trpt->tau, (trpt-1)->tau);",
1020 " x_critical(BFS_PRINT);",
1022 " reached[ot][t->st] = 1;",
1023 " reached[ot][tt] = 1;",
1025 " ((P0 *)this)->_p = tt;",
1029 " bfs_printf(\"done _n = %%d\\n\", _n);",
1033 " /* preselected - no succ definitely outside stack */",
1034 " if ((trpt->tau&32) && !(trpt->tau&64))",
1035 " { From = now._nr_pr-1; To = BASE;",
1037 " bfs_printf(\"%%3ld: proc %%d UnSelected (_n=%%d, tau=%%d)\\n\", ",
1038 " depth, II+1, (int) _n, trpt->tau);",
1040 " _n = 0; trpt->tau &= ~32;",
1044 " goto Repeat_two;",
1046 " trpt->tau &= ~(32|64);",
1050 " && !(trpt->tau&4)",
1053 " { /* no successor states generated */",
1054 " if (boq != -1) /* was rv move */",
1055 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */",
1056 " if (x && ((x->tau&8) || (x->tau&32))) /* break atomic or preselect */",
1057 " { x->o_pm |= 8; /* mark failure */",
1058 " this = pptr(otrpt->pr);",
1059 " ((P0 *) this)->_p = otrpt->st; /* reset state */",
1060 " unsend(boq); /* retract rv offer */",
1063 " printf(\"repush state\\n\");",
1065 " bfs_push_state(NULL, x, x->o_tt); /* repush rv fail */",
1066 " } /* else the rv need not be retried */",
1067 " } else if (now._nr_pr > BASE) /* possible deadlock */",
1068 " { if ((trpt->tau&8)) /* atomic step blocked */",
1069 " { trpt->tau &= ~(1|8); /* 1=timeout, 8=atomic */",
1070 " goto Repeat_one;",
1073 " /* if timeouts were used in the model */",
1074 " if (!(trpt->tau&1))",
1075 " { trpt->tau |= 1; /* enable timeout */",
1076 " goto Repeat_two;",
1079 " if (!noends && !endstate())",
1080 " { bfs_uerror(\"invalid end state.\");",
1084 " else /* boq == -1 && now._nr_pr == BASE && trpt->tau != 4 */",
1085 " { trpt->tau |= 4; /* switch to claim for stutter moves */",
1087 " printf(\"%%3ld: proc -1 exec -1, (stutter move)\\n\", depth, II);",
1089 " bfs_store_state(trpt, boq);", /* doesn't store it but queues it */
1091 " printf(\"%%3ld: proc -1 reverses -1, (stutter move)\\n\", depth, II);",
1093 " trpt->tau &= ~4; /* undo, probably not needed */",
1097 "#ifdef BFS_NOTRAIL",
1098 " bfs_release_trail(otrpt);",
1101 "#if !defined(BFS_FIFO) && !defined(BFS_NORECYCLE)",
1103 "bfs_recycle(BFS_Slot *n)",
1105 " #ifdef BFS_CHECK",
1106 " assert(n != &bfs_null);",
1108 " n->nxt = bfs_free_slot;",
1109 " bfs_free_slot = n;",
1111 " #ifdef BFS_CHECK",
1112 " bfs_printf(\"recycles %%s -- %%p\\n\",",
1113 " n->s_data?\"STATE\":\"EMPTY\", (void *) n);",
1119 "bfs_empty(int p)", /* return Cores if all empty or index of first non-empty q of p */
1121 " const int dst = 0;",
1122 " for (i = 0; i < Cores; i++)",
1123 " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)",
1125 " volatile BFS_Slot *x = shared_memory->head[dst][p][i];",
1126 " while (x && x->type == DELETED)",
1132 " if (p == who_am_i)",
1133 " { shared_memory->head[dst][p][i] = x;",
1135 " #ifdef BFS_CHECK",
1136 " bfs_printf(\"input q [%%d][%%d][%%d] !empty\\n\",",
1141 " #ifdef BFS_CHECK",
1142 " bfs_printf(\"all input qs [%%d][%%d][0..max] empty\\n\",",
1150 "bfs_ewrite(int fd, const void *p, size_t count)",
1152 " if (write(fd, p, count) != count)",
1153 " { perror(\"diskwrite\");",
1154 " Uerror(\"aborting\");",
1159 "bfs_eread(int fd, void *p, size_t count)",
1161 " if (read(fd, p, count) != count)",
1162 " { perror(\"diskread\");",
1163 " Uerror(\"aborting\");",
1168 "bfs_sink_disk(int who_are_you, BFS_Slot *n)",
1171 " bfs_printf(\"sink_disk -> %%d\\n\", who_are_you);",
1173 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) n->s_data->t_info, sizeof(BFS_Trail));",
1174 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &vsize, sizeof(ulong));",
1175 " bfs_ewrite(bfs_out_fd[who_are_you], &now, vsize);",
1177 " bfs_release_trail(n->s_data->t_info);",
1178 " n->s_data->t_info = (BFS_Trail *) 0;",
1181 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->omask), sizeof(EV_Hold *));",
1184 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->lstate), sizeof(H_el *));",
1187 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->boq), sizeof(short));",
1190 " bfs_ewrite(bfs_out_fd[who_are_you], (const void *) &(n->s_data->nr), sizeof(ulong));",
1192 " shared_memory->bfs_out_cnt[who_am_i] = 1;", /* wrote at least one state */
1195 "bfs_source_disk(int fd, volatile BFS_Slot *n)",
1196 "{ ulong nb; /* local temporary */",
1199 " bfs_printf(\"source_disk <- %%d\\n\", who_am_i);",
1201 " n->s_data->t_info = bfs_grab_trail();",
1202 " bfs_eread(fd, (void *) n->s_data->t_info, sizeof(BFS_Trail));",
1203 " bfs_eread(fd, (void *) &nb, sizeof(ulong));",
1205 " x = bfs_new_sv(nb); /* space for osv isn't already allocated */",
1206 " n->s_data->osv = x->sv;",
1207 " x->sv = (State *) 0;",
1208 " x->nxt = bfs_free_hold;",
1209 " bfs_free_hold = x;",
1211 " bfs_eread(fd, (void *) n->s_data->osv, (size_t) nb);",
1213 " bfs_eread(fd, (void *) &(n->s_data->omask), sizeof(EV_Hold *));",
1216 " bfs_eread(fd, (void *) &(n->s_data->lstate), sizeof(H_el *));",
1219 " bfs_eread(fd, (void *) &(n->s_data->boq), sizeof(short));",
1222 " bfs_eread(fd, (void *) &(n->s_data->nr), sizeof(ulong));",
1228 " #ifdef BFS_STAGGER",
1229 "static BFS_Slot *bfs_stage[BFS_STAGGER];",
1232 "bfs_stagger_flush(void)",
1233 "{ int i, who_are_you;",
1234 " int dst = 1 - bfs_toggle;",
1236 " who_are_you = (rand()%%Cores);", /* important: all to the same cpu, but reversed */
1237 " for (i = bfs_stage_cnt-1; i >= 0; i--)",
1238 " { n = bfs_stage[i];",
1240 " bfs_sink_disk(who_are_you, n);",
1241 " bfs_stage[i] = (BFS_Slot *) 0;",
1243 " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];",
1244 " shared_memory->head[dst][who_are_you][who_am_i] = n;",
1245 " /* bfs_sent++; */",
1248 " bfs_printf(\"stagger flush %%d states to %%d\\n\",",
1249 " bfs_stage_cnt, who_are_you);",
1251 " bfs_stage_cnt = 0;",
1255 "bfs_stagger_add(BFS_Slot *n)",
1257 " if (bfs_stage_cnt == BFS_STAGGER)",
1258 " { bfs_stagger_flush();",
1260 " bfs_stage[bfs_stage_cnt++] = n;",
1266 "bfs_push_state(Trail *x, BFS_Trail *y, int tt)",
1267 "{ int who_are_you;",
1269 " const int dst = 0;",
1271 " int dst = 1 - bfs_toggle;",
1275 " if (bfs_keep_state > 0)",
1276 " { who_are_you = bfs_keep_state - 1;",
1278 " { who_are_you = (rand()%%Cores);",
1280 " z = shared_memory->bfs_ix[dst][who_are_you][who_am_i];",
1281 " if (z >= BFS_QSZ)",
1282 " { static int warned_qloss = 0;",
1283 " if (warned_qloss == 0 && who_am_i == 0)",
1284 " { warned_qloss++;",
1285 " bfs_printf(\"BFS_QSZ too small - losing states\\n\");",
1290 " shared_memory->bfs_ix[dst][who_are_you][who_am_i] = z+1;",
1291 " BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_prep_slot(y, ",
1292 " (BFS_Slot *) &(shared_memory->bfsq[dst][who_are_you][who_am_i][z])));",
1294 " BFS_Slot *n = bfs_pack_state(x, y, tt, bfs_new_slot(y));",
1296 " #ifdef BFS_GREEDY",
1297 " who_are_you = who_am_i; /* for testing only */",
1299 " if (bfs_keep_state > 0)",
1300 " { who_are_you = bfs_keep_state - 1;",
1303 " #ifdef BFS_STAGGER",
1304 " who_are_you = -1;",
1305 " bfs_stagger_add(n);",
1308 " who_are_you = (rand()%%Cores);",
1313 " if (!shared_memory->tail[dst][who_are_you][who_am_i])",
1314 " { shared_memory->dels[dst][who_are_you][who_am_i] =",
1315 " shared_memory->tail[dst][who_are_you][who_am_i] =",
1316 " shared_memory->head[dst][who_are_you][who_am_i] = n;",
1318 " { shared_memory->tail[dst][who_are_you][who_am_i]->nxt = n;",
1319 " shared_memory->tail[dst][who_are_you][who_am_i] = n;",
1321 " shared_memory->bfs_idle[who_are_you] = 0;",
1324 " bfs_sink_disk(who_are_you, n);",
1326 " n->nxt = (BFS_Slot *) shared_memory->head[dst][who_are_you][who_am_i];",
1327 " shared_memory->head[dst][who_are_you][who_am_i] = n;",
1329 " #ifdef BFS_STAGGER",
1332 "#endif", /* BFS_QSZ */
1334 " bfs_printf(\"PUT STATE (depth %%ld, nr %%u) to %%d -- s_data: %%p\\n\",",
1335 " tt, n->s_data->nr, who_are_you, n->s_data);",
1342 "{ volatile BFS_Slot *n = &bfs_null;",
1344 " const int src = 0;",
1345 " bfs_qscan = bfs_empty(who_am_i);",
1347 " const int src = bfs_toggle;",
1349 " while (bfs_qscan < Cores",
1350 " && shared_memory->bfs_ix[src][who_am_i][bfs_qscan] == 0)",
1354 " while (bfs_qscan < Cores",
1355 " && shared_memory->head[src][who_am_i][bfs_qscan] == (BFS_Slot *) 0)",
1360 " if (bfs_qscan < Cores)",
1362 " #ifdef BFS_FIFO", /* no wait for toggles */
1363 " shared_memory->bfs_idle[who_am_i] = 0;",
1364 " for (n = shared_memory->head[src][who_am_i][bfs_qscan]; n; n = n->nxt)",
1365 " { if (n->type != DELETED)",
1368 " #ifdef BFS_CHECK",
1369 " assert(n && n->type == STATE); /* q cannot be empty */",
1372 " { shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;",
1373 " }", /* else, do not remove it - yet - avoid empty queues */
1374 " n->type = DELETED;",
1377 " uint x = --shared_memory->bfs_ix[src][who_am_i][bfs_qscan];",
1378 " n = &(shared_memory->bfsq[src][who_am_i][bfs_qscan][x]);",
1380 " n = shared_memory->head[src][who_am_i][bfs_qscan];",
1381 " shared_memory->head[src][who_am_i][bfs_qscan] = n->nxt;",
1382 " #if defined(BFS_FIFO) && defined(BFS_CHECK)",
1383 " assert(n->type == STATE);",
1385 " n->nxt = (BFS_Slot *) 0;",
1388 " /* the states actually show up in reverse order (FIFO iso LIFO) here */",
1389 " /* but that doesnt really matter as long as the count is right */",
1390 " bfs_source_disk(bfs_inp_fd[bfs_qscan], n); /* get the data */",
1394 " #ifdef BFS_CHECK",
1395 " bfs_printf(\"rcv STATE from [%%d][%%d][%%d]\\n\",",
1396 " src, who_am_i, bfs_qscan);",
1401 " #if defined(BFS_STAGGER) && !defined(BFS_QSZ)",
1402 " if (bfs_stage_cnt > 0)",
1403 " { bfs_stagger_flush();",
1406 " shared_memory->bfs_idle[who_am_i] = 1;",
1407 " #if defined(BFS_FIFO) && defined(BFS_CHECK)",
1408 " assert(n->type == EMPTY);",
1411 " return (BFS_Slot *) n;",
1415 "bfs_all_empty(void)",
1418 " for (i = 0; i < Cores; i++)",
1419 " { if (shared_memory->bfs_out_cnt[i] != 0)",
1422 " bfs_printf(\"bfs_all_empty %%d not empty\\n\", i);",
1429 " const int dst = 0;",
1431 " int dst = 1 - bfs_toggle; /* next generation */",
1433 " for (p = 0; p < Cores; p++)",
1434 " for (i = 0; i < Cores; i++)",
1436 " { if (shared_memory->bfs_ix[dst][p][i] > 0)",
1438 " { if (shared_memory->head[dst][p][i] != (BFS_Slot *) 0)",
1444 " bfs_printf(\"bfs_all_empty\\n\");",
1454 " for (i = 0; i < Cores; i++)",
1455 " for (n = (BFS_Slot *) shared_memory->dels[0][who_am_i][i];",
1456 " n && n != shared_memory->head[0][who_am_i][i];",
1458 " { if (n->type == DELETED && n->nxt)",
1459 " { shared_memory->dels[0][who_am_i][i] = n->nxt;",
1460 " n->nxt = (BFS_Slot *) 0;",
1463 " return (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));",
1467 "typedef struct BFS_T_Hold BFS_T_Hold;",
1468 "struct BFS_T_Hold {",
1469 " volatile BFS_Trail *t;",
1470 " BFS_T_Hold *nxt;",
1472 "BFS_T_Hold *bfs_t_held, *bfs_t_free;",
1475 "bfs_grab_trail(void)", /* call in bfs_source_disk and bfs_new_slot */
1480 " bfs_printf(\"grab trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);",
1483 " { h = bfs_t_held;",
1484 " bfs_t_held = bfs_t_held->nxt;",
1485 " t = (BFS_Trail *) h->t;",
1486 " h->t = (BFS_Trail *) 0; /* make sure it cannot be reused */",
1487 " h->nxt = bfs_t_free;",
1491 " { t = (BFS_Trail *) sh_malloc((ulong) sizeof(BFS_Trail));",
1496 " t->ostate = (H_el *) 0;",
1498 " bfs_printf(\"grab trail %%p\\n\", (void *) t);",
1503 "#if defined(BFS_DISK) || defined(BFS_NOTRAIL)",
1505 "bfs_release_trail(BFS_Trail *t)", /* call in bfs_sink_disk (not bfs_recycle) */
1507 " #ifdef BFS_CHECK",
1511 " bfs_printf(\"release trail %%p\\n\", (void *) t);",
1514 " { h = bfs_t_free;",
1515 " bfs_t_free = bfs_t_free->nxt;",
1517 " { h = (BFS_T_Hold *) emalloc(sizeof(BFS_T_Hold));",
1520 " h->nxt = bfs_t_held;",
1523 " bfs_printf(\"release trail - bfs_t_held %%p\\n\", (void *) bfs_t_held);",
1530 "bfs_new_slot(BFS_Trail *f)",
1534 " t = bfs_sweep();",
1536 " if (bfs_free_slot) /* local */",
1537 " { t = bfs_free_slot;",
1538 " bfs_free_slot = bfs_free_slot->nxt;",
1539 " t->nxt = (BFS_Slot *) 0;",
1541 " { t = (BFS_Slot *) sh_malloc((ulong) sizeof(BFS_Slot));",
1545 " { memset(t->s_data, 0, sizeof(BFS_State));",
1547 " { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));",
1550 " /* we keep a ptr to the frame of parent states, which is */",
1551 " /* used for reconstructing path and recovering failed rvs etc */",
1552 " /* we should not overwrite the data at this address with a memset */",
1555 " { t->s_data->t_info = f;",
1557 " { t->s_data->t_info = bfs_grab_trail();",
1563 "bfs_prep_slot(BFS_Trail *f, BFS_Slot *t)",
1566 " { memset(t->s_data, 0, sizeof(BFS_State));",
1568 " { t->s_data = (BFS_State *) sh_malloc((ulong) sizeof(BFS_State));",
1571 " { t->s_data->t_info = f;",
1573 " { t->s_data->t_info = bfs_grab_trail();",
1580 "bfs_new_sv(int n)",
1583 " if (bfs_svfree[n])",
1584 " { h = bfs_svfree[n];",
1585 " bfs_svfree[n] = h->nxt;",
1586 " h->nxt = (SV_Hold *) 0;",
1588 " { h = (SV_Hold *) sh_malloc((ulong) sizeof(SV_Hold));",
1592 " h->sv = (State *) sh_malloc((ulong)(sizeof(State) - VECTORSZ + n));",
1594 " memcpy((char *)h->sv, (char *)&now, n);",
1598 "static EV_Hold *kept[VECTORSZ]; /* local */",
1601 "bfs_keep(EV_Hold *v)",
1604 " for (h = kept[v->sz]; h; h = h->nxt) /* check local list */",
1605 " { if (v->nrpr == h->nrpr",
1606 " && v->nrqs == h->nrqs",
1607 "#if !defined(NOCOMP) && !defined(HC)",
1608 " && (v->sv == h->sv || memcmp((char *) v->sv, (char *) h->sv, v->sz) == 0)",
1614 " #if VECTORSZ>32000",
1615 " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(int)) == 0)",
1616 " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(int)) == 0)",
1618 " && (memcmp((char *) v->po, (char *) h->po, v->nrpr * sizeof(short)) == 0)",
1619 " && (memcmp((char *) v->qo, (char *) h->qo, v->nrqs * sizeof(short)) == 0)",
1621 " && (memcmp((char *) v->ps, (char *) h->ps, v->nrpr * sizeof(uchar)) == 0)",
1622 " && (memcmp((char *) v->qs, (char *) h->qs, v->nrqs * sizeof(uchar)) == 0))",
1630 " if (!h) /* we don't have one like it yet */",
1631 " { v->nxt = kept[v->sz]; /* keep the original owner field */",
1632 " kept[v->sz] = v;",
1633 " /* all ptrs inside are to shared memory, but nxt is local */",
1638 "bfs_new_sv_mask(int n)",
1641 " for (h = kept[n]; h; h = h->nxt)",
1642 " { if ((now._nr_pr == h->nrpr)",
1643 " && (now._nr_qs == h->nrqs)",
1644 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
1645 " && ((char *) Mask == h->sv || (memcmp((char *) Mask, h->sv, n) == 0))",
1651 " #if VECTORSZ>32000",
1652 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)",
1653 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)",
1655 " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)",
1656 " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)",
1658 " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)",
1659 " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))",
1668 " { /* once created, the contents are never modified */",
1669 " h = (EV_Hold *) sh_malloc((ulong)sizeof(EV_Hold));",
1670 " h->owner = who_am_i;",
1672 " h->nrpr = now._nr_pr;",
1673 " h->nrqs = now._nr_qs;",
1674 "#if !defined(NOCOMP) && !defined(HC) && NRUNS>0",
1675 " h->sv = (char *) Mask; /* in shared memory, and never modified */",
1677 "#if NRUNS>0 && !defined(TRIX)",
1678 " if (now._nr_pr > 0)",
1679 " { h->ps = (char *) proc_skip;",
1680 " h->po = (char *) proc_offset;",
1682 " if (now._nr_qs > 0)",
1683 " { h->qs = (char *) q_skip;",
1684 " h->qo = (char *) q_offset;",
1687 " h->nxt = kept[n];",
1692 "#endif", /* NRUNS>0 */
1694 "bfs_pack_state(Trail *f, BFS_Trail *g, int search_depth, BFS_Slot *t)",
1697 " assert(t->s_data != NULL);",
1698 " assert(t->s_data->t_info != NULL);",
1702 " { t->s_data->t_info->ostate = f->ostate;",
1703 " t->s_data->t_info->st = f->st;",
1704 " t->s_data->t_info->o_tt = search_depth;",
1705 " t->s_data->t_info->pr = f->pr;",
1706 " t->s_data->t_info->tau = f->tau;",
1707 " t->s_data->t_info->o_pm = f->o_pm;",
1709 " { t->s_data->t_info->t_id = f->o_t->t_id;",
1711 " { t->s_data->t_info->t_id = -1;",
1712 " t->s_data->t_info->ostate = NULL;",
1714 " } /* else t->s_data->t_info == g */",
1716 " t->s_data->boq = boq;",
1719 " { static ulong u_cnt;",
1720 " t->s_data->nr = u_cnt++;",
1724 " sv_populate(); /* make sure now is up to date */",
1727 " { SV_Hold *x = bfs_new_sv(vsize);",
1728 " t->s_data->osv = x->sv;",
1729 " x->sv = (State *) 0;",
1730 " x->nxt = bfs_free_hold;",
1731 " bfs_free_hold = x;",
1735 " t->s_data->omask = bfs_new_sv_mask(vsize);",
1738 "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)",
1739 " t->s_data->lstate = Lstate; /* Lstate is set in o_store or h_store */",
1742 " t->type = STATE;",
1748 "bfs_store_state(Trail *t, short oboq)",
1753 "#if defined(VERI) && defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
1754 " if (!(t->tau&4)", /* prog move */
1755 " && t->ostate)", /* not initial state */
1756 " { t->tau |= ((BFS_Trail *) t->ostate)->tau&64;",
1757 " } /* lift 64 across claim moves */",
1760 "#ifdef BFS_SEP_HASH",
1762 " if (boq == -1 && oboq != -1) /* post-rv */",
1763 " { BFS_Trail *x = (BFS_Trail *) trpt->ostate; /* pre-rv state */",
1765 " { x->o_pm |= 4; /* rv complete */",
1768 " d_sfh((uchar *)&now, (int) vsize); /* sep-hash -- sets K1 -- overkill */",
1769 " bfs_keep_state = K1%%Cores + 1;",
1770 " bfs_push_state(t, NULL, trpt->o_tt+1); /* bfs_store_state - sep_hash */",
1771 " bfs_keep_state = 0;",
1775 in VERI mode store the state when
1776 (!t->ostate || (t->tau&4)) in initial state and after each program move
1778 i.e., dont store when !(!t->ostate || (t->tau&4)) = (t->ostate && !(t->tau&4))
1779 the *first* time that the tau flag is not set:
1780 possibly after a series of claim moves in an atomic sequence
1782 " if (!(t->tau&4) && t->ostate && (((BFS_Trail *)t->ostate)->tau&4))",
1783 " { /* do not store intermediate state */",
1784 " #if defined(VERBOSE) && defined(L_BOUND)",
1785 " bfs_printf(\"Un-Stored state bnd %%d -- sds %%p\\n\",",
1786 " now._l_bnd, now._l_sds);",
1788 " bfs_push_state(t, NULL, trpt->o_tt+1); /* claim move */",
1791 " if (!bfs_do_store((char *)&now, vsize)) /* includes bfs_visited */",
1792 " { nstates++; /* local count */",
1793 " trpt->tau |= 64; /* bfs: succ outside stack */",
1795 " if (boq == -1 && oboq != -1) /* post-rv */",
1796 " { BFS_Trail *x = ",
1797 " (BFS_Trail *) trpt->ostate; /* pre-rv state */",
1799 " { x->o_pm |= 4; /* rv complete */",
1802 " bfs_push_state(t, NULL, trpt->o_tt+1); /* successor */",
1805 " #ifdef BFS_CHECK",
1806 " bfs_printf(\"seen before\\n\");",
1808 " #if defined(Q_PROVISO) && !defined(BITSTATE) && defined(FULLSTACK)",
1810 " if (Lstate)", /* if BFS_INQ is set */
1811 " { trpt->tau |= 64;",
1814 " if (Lstate && Lstate->tagged) /* bfs_store_state */",
1815 " { trpt->tau |= 64;",
1823 "/*** support routines ***/",
1826 "bfs_clear_locks(void)",
1829 " /* clear any locks held by this process only */",
1830 " if (shared_memory)",
1831 " for (i = 0; i < BFS_MAXLOCKS; i++)",
1832 " { if (shared_memory->sh_owner[i] == who_am_i + 1)",
1833 " { shared_memory->sh_locks[i] = 0;",
1835 " shared_memory->in_count[i] = 0;",
1837 " shared_memory->sh_owner[i] = 0;",
1842 "e_critical(int which)",
1845 " assert(which >= 0 && which < BFS_MAXLOCKS);",
1847 " if (shared_memory == NULL) return;",
1848 " while (tas(&(shared_memory->sh_locks[which])) != 0)",
1849 " { w = shared_memory->sh_owner[which]; /* sh_locks[which] could be 0 by now */",
1850 " assert(w >= 0 && w <= BFS_MAXPROCS);",
1851 " if (w > 0 && shared_memory->bfs_flag[w-1] == 2)",
1852 " { /* multiple processes can get here; only one should do this: */",
1853 " if (tas(&(shared_memory->bfs_data[w - 1].override)) == 0)",
1854 " { fprintf(stderr, \"cpu%%02d: override lock %%d - held by %%d\\n\",",
1855 " who_am_i, which, shared_memory->sh_owner[which]);",
1857 " shared_memory->in_count[which] = 0;",
1859 " shared_memory->sh_locks[which] = 0;",
1860 " shared_memory->sh_owner[which] = 0;",
1862 " shared_memory->wait_count[which]++; /* not atomic of course */",
1865 " if (shared_memory->in_count[which] != 0)",
1866 " { fprintf(stderr, \"cpu%%02d: cannot happen lock %%d count %%d\\n\", who_am_i,",
1867 " which, shared_memory->in_count[which]);",
1869 " shared_memory->in_count[which]++;",
1871 " shared_memory->sh_owner[which] = who_am_i+1;",
1875 "x_critical(int which)",
1877 " if (shared_memory == NULL) return;",
1879 " assert(shared_memory->in_count[which] == 1);",
1880 " shared_memory->in_count[which] = 0;",
1882 " shared_memory->sh_locks[which] = 0;",
1883 " shared_memory->sh_owner[which] = 0;",
1887 "bfs_printf(const char *fmt, ...)",
1890 " e_critical(BFS_PRINT);",
1892 " if (1) { int i=who_am_i; while (i-- > 0) printf(\" \"); }",
1894 " printf(\"cpu%%02d: \", who_am_i);",
1895 " va_start(args, fmt);",
1896 " vprintf(fmt, args);",
1899 " x_critical(BFS_PRINT);",
1903 "bfs_all_idle(void)",
1906 " if (shared_memory)",
1907 " for (i = 0; i < Cores; i++)",
1908 " { if (shared_memory->bfs_flag[i] == 0",
1909 " && shared_memory->bfs_idle[i] == 0)",
1917 "bfs_idle_and_empty(void)",
1918 "{ int p; /* read-only */",
1919 " for (p = 0; p < Cores; p++)",
1920 " { if (shared_memory->bfs_flag[p] == 0",
1921 " && shared_memory->bfs_idle[p] == 0)",
1924 " for (p = 0; p < Cores; p++)",
1925 " { if (bfs_empty(p) < Cores)",
1933 "bfs_set_toggle(void) /* executed by root */",
1936 " if (shared_memory)",
1937 " for (i = 0; i < Cores; i++)",
1938 " { shared_memory->bfs_idle[i] = 0;",
1943 "bfs_all_running(void) /* crash detection */",
1945 " for (i = 0; i < Cores; i++)",
1946 " { if (!shared_memory || shared_memory->bfs_flag[i] > 1)",
1953 "bfs_mark_done(int code)",
1955 " if (shared_memory)",
1956 " { shared_memory->bfs_flag[who_am_i] = (int) code;",
1957 " shared_memory->quit = 1;",
1962 "bfs_offset(int c)",
1965 " uchar *q = (uchar *) ncomps; /* it is the first object allocated */",
1966 " q += (256+2) * sizeof(ulong); /* preserve contents of ncomps */",
1968 " uchar *q = (uchar *) &(shared_memory->allocator);",
1970 " /* _NP_+1 proctypes, reachability info:",
1971 " * reached[x : 0 .. _NP_+1][ 0 .. NrStates[x] ]",
1973 " for (p = N = 0; p <= _NP_; p++)",
1974 " { N += NrStates[p]; /* sum for all proctypes */",
1977 " /* space needed per proctype: N bytes */",
1978 " /* rounded up to a multiple of the word size */",
1979 " if ((N%%sizeof(void *)) != 0) /* aligned */",
1980 " { N += sizeof(void *) - (N%%sizeof(void *));",
1983 " q += ((c - 1) * (_NP_ + 1) * N);",
1988 "bfs_putreached(void)",
1992 " assert(who_am_i > 0);",
1994 " q = bfs_offset(who_am_i);",
1995 " for (p = 0; p <= _NP_; p++)",
1996 " { memcpy((void *) q, (const void *) reached[p], (size_t) NrStates[p]);",
1997 " q += NrStates[p];",
2002 "bfs_getreached(int c)",
2006 " assert(who_am_i == 0 && c >= 1 && c < Cores);",
2008 " q = (uchar *) bfs_offset(c);",
2009 " for (p = 0; p <= _NP_; p++)",
2010 " for (i = 0; i < NrStates[p]; i++)",
2011 " { reached[p][i] += *q++; /* update local copy */",
2018 " volatile BFS_data *s;",
2020 " if (!shared_memory) return;",
2022 " s = &shared_memory->bfs_data[who_am_i];",
2023 " if (who_am_i == 0)",
2024 " { shared_memory->bfs_flag[who_am_i] = 3; /* or else others dont stop */",
2026 " for (i = 1; i < Cores; i++) /* start at 1 not 0 */",
2027 " { while (shared_memory->bfs_flag[i] == 0)",
2029 " if (bfs_gcount++ > WAIT_MAX) /* excessively long wait */",
2030 " { printf(\"cpu00: give up waiting for cpu%%2d (%%d cores)\\n\", i, Cores);",
2034 " s = &shared_memory->bfs_data[i];",
2035 " mreached = Max(mreached, s->mreached);",
2036 " hmax = vsize = Max(vsize, s->vsize);",
2037 " errors += s->errors;",
2038 " memcnt += s->memcnt;",
2039 " nstates += s->nstates;",
2040 " nlinks += s->nlinks;",
2041 " truncs += s->truncs;",
2042 " bfs_left += s->memory_left;",
2043 " bfs_punt += s->punted;",
2044 " bfs_getreached(i);",
2047 " { s->mreached = (ulong) mreached;",
2048 " s->vsize = (ulong) vsize;",
2049 " s->errors = (int) errors;",
2050 " s->memcnt = (double) memcnt;",
2051 " s->nstates = (double) nstates;",
2052 " s->nlinks = (double) nlinks;",
2053 " s->truncs = (double) truncs;",
2054 " s->memory_left = (ulong) bfs_left;",
2055 " s->punted = (ulong) bfs_punt;",
2056 " bfs_putreached();",
2061 "sh_pre_malloc(ulong n) /* used before the local heaps are populated */",
2062 "{ volatile uchar *ptr = NULL;",
2064 " assert(!bfs_runs);",
2065 " if ((n%%sizeof(void *)) != 0)",
2066 " { n += sizeof(void *) - (n%%sizeof(void *));",
2067 " assert((n%%sizeof(void *)) == 0);",
2070 " e_critical(BFS_MEM); /* needed? */",
2071 " if (shared_memory->mem_left < n + 7)", /* 7 for possible alignment */
2072 " { x_critical(BFS_MEM);",
2073 " bfs_printf(\"want %%lu, have %%lu\\n\",",
2074 " n, shared_memory->mem_left);",
2075 " bfs_shutdown(\"out of shared memory\");",
2076 " assert(0); /* should be unreachable */",
2078 " ptr = shared_memory->allocator;",
2079 "#if WS>4", /* align to 8 byte boundary */
2080 " { int b = (int) ((uint64_t) ptr)&7;",
2083 " shared_memory->allocator = ptr;",
2086 " shared_memory->allocator += n;",
2087 " shared_memory->mem_left -= n;",
2088 " x_critical(BFS_MEM);",
2090 " bfs_pre_allocated += n;",
2096 "sh_malloc(ulong n)",
2097 "{ volatile uchar *ptr = NULL;",
2099 " assert(bfs_runs);",
2101 " if ((n%%sizeof(void *)) != 0)",
2102 " { n += sizeof(void *) - (n%%sizeof(void *));",
2104 " assert((n%%sizeof(void *)) == 0);",
2108 " /* local heap -- no locks needed */",
2109 " if (bfs_left < n)",
2110 " { e_critical(BFS_MEM);",
2111 " if (shared_memory->mem_left >= n)",
2112 " { ptr = (uchar *) shared_memory->allocator;",
2113 " shared_memory->allocator += n;",
2114 " shared_memory->mem_left -= n;",
2115 " x_critical(BFS_MEM);",
2118 " x_critical(BFS_MEM);",
2119 "#ifdef BFS_LOGMEM",
2121 " e_critical(BFS_MEM);",
2122 " for (i = 0; i < 1024; i++)",
2123 " { if (shared_memory->logmem[i] > 0)",
2124 " { bfs_printf(\"\tlog[%%d]\t%%d\\n\", i, shared_memory->logmem[i]);",
2126 " x_critical(BFS_MEM);",
2128 " bfs_shutdown(\"out of shared memory\"); /* no return */",
2130 "#ifdef BFS_LOGMEM",
2131 " e_critical(BFS_MEM);",
2133 " { shared_memory->logmem[n]++;",
2135 " { shared_memory->logmem[1023]++;",
2137 " x_critical(BFS_MEM);",
2139 " ptr = (uchar *) bfs_heap;",
2143 " if (0) printf(\"sh_malloc %%ld\\n\", n);",
2148 "bfs_get_shared_mem(key_t key, size_t n)",
2151 " assert(who_am_i == 0);",
2153 " shared_mem_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create */",
2154 " if (shared_mem_id == -1)",
2155 " { fprintf(stderr, \"cpu%%02d: tried to get %%d MB of shared memory\\n\",",
2156 " who_am_i, (int) n/(1024*1024));",
2157 " perror(\"shmget\");",
2160 " if ((rval = (char *) shmat(shared_mem_id, (void *) 0, 0)) == (char *) -1) /* attach */",
2161 " { perror(\"shmat\");",
2164 " return (uchar *) rval;",
2168 "bfs_drop_shared_memory(void)",
2170 " if (who_am_i == 0)",
2171 " { printf(\"pan: releasing shared memory...\");",
2174 " if (shared_memory)",
2175 " { shmdt(shared_memory); /* detach */",
2176 " if (who_am_i == 0)",
2177 " { shmctl(shared_mem_id, IPC_RMID, (void *) 0); /* remove */",
2179 " if (who_am_i == 0)",
2180 " { printf(\"done\\n\");",
2186 "bfs_find_largest(key_t key)",
2188 " const size_t delta = 32*1024*1024;",
2189 " int temp_id = -1;",
2190 " int atleastonce = 0;",
2192 " for (n = delta; ; n += delta)",
2193 " { if (WS <= 4 && n >= 1024*1024*1024)", /* was n >= INT_MAX */
2194 " { n = 1024*1024*1024;",
2198 " if ((double) n > memlim)",
2199 " { n = (size_t) memlim;",
2203 " temp_id = shmget(key, n, 0600); /* check for stale copy */",
2204 " if (temp_id != -1)",
2205 " { if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0) /* remove */",
2206 " { perror(\"remove_segment_fails 2\");",
2210 " temp_id = shmget(key, n, 0600 | IPC_CREAT | IPC_EXCL); /* create new */",
2211 " if (temp_id == -1)",
2215 " { atleastonce++;",
2216 " if (shmctl(temp_id, IPC_RMID, ((void *) 0)) < 0)",
2217 " { perror(\"remove_segment_fails 0\");",
2221 " if (!atleastonce)",
2222 " { printf(\"cpu%%02d: no shared memory n=%%d\\n\", who_am_i, (int) n);",
2226 " printf(\"cpu%%02d: largest shared memory segment: %%lu MB\\n\",",
2227 " who_am_i, (ulong) n/(1024*1024));",
2229 " #ifdef BFS_SEP_HASH",
2230 " n /= 2; /* not n /= Cores because the queues take most memory */",
2231 " printf(\"cpu%%02d: using %%lu MB\\n\", who_am_i, (ulong) n/(1024*1024));",
2236 " if ((n/(1024*1024)) == 32)",
2237 " { if (sizeof(void *) == 4) /* a 32 bit machine */",
2238 " { fprintf(stderr, \"\\t32MB is the default; increase it to 1 GB with:\\n\");",
2239 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=%%d\\n\", (1<<30));",
2240 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=%%d\\n\", (1<<30)/8192);",
2241 " } else if (sizeof(void *) == 8) /* a 64 bit machine */",
2242 " { fprintf(stderr, \"\\t32MB is the default; increase it to 30 GB with:\\n\");",
2243 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=32212254720\\n\");",
2244 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=7864320\\n\");",
2245 " fprintf(stderr, \"\\tor for 60 GB:\\n\");",
2246 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmmax=60000000000\\n\");",
2247 " fprintf(stderr, \"\\tsudo /sbin/sysctl kernel.shmall=30000000\\n\");",
2249 " { fprintf(stderr, \"\\tweird wordsize %%d\\n\", (int) sizeof(void *));",
2256 "bfs_disk_start(void)", /* setup .spin*/
2257 "{ int unused = system(\"rm -fr .spin\");",
2258 " if (mkdir(\".spin\", 0777) != 0)",
2259 " { perror(\"mkdir\");",
2260 " Uerror(\"aborting\");",
2264 "bfs_disk_stop(void)", /* remove .spin */
2266 " if (system(\"rm -fr .spin\") < 0)",
2267 " { perror(\"rm -fr .spin/\");",
2271 "bfs_disk_inp(void)", /* this core only */
2272 "{ int i; char fnm[16];",
2274 " bfs_printf(\"inp %%d %%d 0..%%d\\n\", bfs_toggle, who_am_i, Cores);",
2276 " for (i = 0; i < Cores; i++)",
2277 " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", bfs_toggle, who_am_i, i);",
2278 " if ((bfs_inp_fd[i] = open(fnm, 0444)) < 0)",
2279 " { perror(\"open\");",
2284 "bfs_disk_out(void)", /* this core only */
2285 "{ int i; char fnm[16];",
2287 " bfs_printf(\"out %%d 0..%%d %%d\\n\", 1-bfs_toggle, Cores, who_am_i);",
2289 " shared_memory->bfs_out_cnt[who_am_i] = 0;",
2290 " for (i = 0; i < Cores; i++)",
2291 " { sprintf(fnm, \".spin/q%%d_%%d_%%d\", 1-bfs_toggle, i, who_am_i);",
2292 " if ((bfs_out_fd[i] = creat(fnm, 0666)) < 0)",
2293 " { perror(\"creat\");",
2298 "bfs_disk_iclose(void)",
2301 " bfs_printf(\"close_inp\\n\");",
2303 " for (i = 0; i < Cores; i++)",
2304 " { if (close(bfs_inp_fd[i]) < 0)",
2305 " { perror(\"iclose\");",
2309 "bfs_disk_oclose(void)",
2312 " bfs_printf(\"close_out\\n\");",
2314 " for (i = 0; i < Cores; i++)",
2315 " { if (fsync(bfs_out_fd[i]) < 0)",
2316 " { perror(\"fsync\");",
2318 " if (close(bfs_out_fd[i]) < 0)",
2319 " { perror(\"oclose\");",
2324 "bfs_write_snap(int fd)",
2325 "{ if (write(fd, snap, strlen(snap)) != strlen(snap))",
2326 " { printf(\"pan: error writing %%s\\n\", fnm);",
2327 " bfs_shutdown(\"file system error\");",
2332 "bfs_one_step(BFS_Trail *t, int fd)",
2333 "{ if (t && t->t_id != (T_ID) -1)",
2334 " { sprintf(snap, \"%%d:%%d:%%d\\n\",",
2335 " trcnt++, t->pr, t->t_id);",
2336 " bfs_write_snap(fd);",
2341 "bfs_putter(BFS_Trail *t, int fd)",
2342 "{ if (t && t != (BFS_Trail *) t->ostate)",
2343 " bfs_putter((BFS_Trail *) t->ostate, fd);",
2345 " if (depthfound == trcnt)",
2346 " { strcpy(snap, \"-1:-1:-1\\n\");",
2347 " bfs_write_snap(fd);",
2348 " depthfound = -1;",
2351 " bfs_one_step(t, fd);",
2355 "bfs_nuerror(char *str)",
2356 "{ int fd = make_trail();",
2358 " if (fd < 0) return;",
2360 " sprintf(snap, \"-2:%%d:-2\\n\", (uchar) ((P0 *)pptr(0))->_t);",
2361 " bfs_write_snap(fd);",
2364 " sprintf(snap, \"-4:-4:-4\\n\");",
2365 " bfs_write_snap(fd);",
2368 " if (strstr(str, \"invalid\"))",
2369 " { bfs_putter((BFS_Trail *) trpt->ostate, fd);",
2372 " memset((char *) &x, 0, sizeof(BFS_Trail));",
2373 " x.pr = trpt->pr;",
2374 " x.t_id = (trpt->o_t)?trpt->o_t->t_id:0;",
2375 " x.ostate = trpt->ostate;",
2376 " bfs_putter(&x, fd);",
2379 " if (errors >= upto && upto != 0)",
2380 " { bfs_shutdown(str);",
2385 "bfs_uerror(char *str)",
2386 "{ static char laststr[256];",
2389 " if (strncmp(str, laststr, 254) != 0)",
2390 " { bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\",",
2391 " errors, str, ((depthfound == -1)?depth:depthfound));",
2392 " strncpy(laststr, str, 254);",
2395 " if (readtrail) { wrap_trail(); return; }",
2397 " if (every_error != 0 || errors == upto)",
2398 " { bfs_nuerror(str);",
2400 " if (errors >= upto && upto != 0)",
2401 " { bfs_shutdown(\"bfs_uerror\");",
2403 " depthfound = -1;",
2406 "bfs_Uerror(char *str)",
2407 "{ /* bfs_uerror(str); */",
2408 " bfs_printf(\"pan:%%d: %%s (at depth %%ld)\\n\", ++errors, str,",
2409 " ((depthfound == -1)?depth:depthfound));",
2410 " bfs_shutdown(\"bfs_Uerror\");",