/***** spin: pangen2.h *****/ /* Copyright (c) 1989-2007 by Lucent Technologies, Bell Laboratories. *//* All Rights Reserved. This software is for educational purposes only. *//* No guarantee whatsoever is expressed or implied by the distribution of *//* this code. Permission is given to distribute this code provided that *//* this introductory message is not removed and no monies are exchanged. *//* Software written by Gerard J. Holzmann. For tool documentation see: *//* http://spinroot.com/ *//* Send all bug-reports and/or questions to: bugs@spinroot.com *//* (c) 2007: small additions for V5.0 to support multi-core verifications */ static char *Pre0[] = {"#ifdef SC", "#define _FILE_OFFSET_BITS 64", /* to allow file sizes greater than 2Gb */"#endif", "#include <stdio.h>", "#include <signal.h>", "#include <stdlib.h>", "#include <stdarg.h>", "#include <string.h>", "#include <ctype.h>", "#include <errno.h>", "#if defined(WIN32) || defined(WIN64)", "#include <time.h>", "#else", "#include <unistd.h>", "#include <sys/times.h>", "#endif", "#include <sys/types.h>", /* defines off_t */ "#include <sys/stat.h>", "#include <fcntl.h>", "#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))", "#ifndef max", "#define max(a,b) (((a)<(b)) ? (b) : (a))", "#endif", "#ifndef PRINTF", "int Printf(const char *fmt, ...); /* prototype only */", "#endif", 0,}; static char *Preamble[] = { "#ifdef RANDOMIZE", " #define T_RAND RANDOMIZE", "#endif", "#ifdef CNTRSTACK", " #define onstack_now() (LL[trpt->j6] && LL[trpt->j7])", " #define onstack_put() LL[trpt->j6]++; LL[trpt->j7]++", " #define onstack_zap() LL[trpt->j6]--; LL[trpt->j7]--", "#endif", "#if !defined(SAFETY) && !defined(NOCOMP)", /* * V_A identifies states in the current statespace * A_V identifies states in the 'other' statespace * S_A remembers how many leading bytes in the sv * are used for these markers + fairness bits */ " #define V_A (((now._a_t&1)?2:1) << (now._a_t&2))", " #define A_V (((now._a_t&1)?1:2) << (now._a_t&2))", " int S_A = 0;", "#else", " #define V_A 0", " #define A_V 0", " #define S_A 0", "#endif", "#ifdef MA", "#undef onstack_now", "#undef onstack_put", "#undef onstack_zap", "#define onstack_put() ;", "#define onstack_zap() gstore((char *) &now, vsize, 4)","#else", "#if defined(FULLSTACK) && !defined(BITSTATE)", "#define onstack_put() trpt->ostate = Lstate", "#define onstack_zap() { \\", " if (trpt->ostate) \\", " trpt->ostate->tagged = \\", " (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\", " }", "#endif","#endif", "#ifndef NO_V_PROVISO", "#define V_PROVISO", "#endif", "#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && NCORE==1", " #define AUTO_RESIZE", "#endif", "", "struct H_el {", " struct H_el *nxt;", "#ifdef FULLSTACK", " unsigned int tagged;", " #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)", " unsigned int proviso;", /* uses just 1 bit 0/1 */ " #endif", "#endif", "#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))", " unsigned long st_id;", "#endif", "#if !defined(SAFETY) || defined(REACH)", " unsigned int D;", "#endif", "#ifdef BCS", " #ifndef CONSERVATIVE", " #define CONSERVATIVE 1 /* good for up to 8 processes */", " #endif", " #ifdef CONSERVATIVE", " #if CONSERVATIVE <= 0 || CONSERVATIVE>32", " #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)", " #endif", " uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */ " #endif", " uchar ctx_low;", /* lowest nr of context switches seen so far */ "#endif", "#if NCORE>1", " /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */", " #ifdef V_PROVISO", " uchar cpu_id; /* id of cpu that created the state */", " #endif", "#endif", "#ifdef COLLAPSE", " #if VECTORSZ<65536", " unsigned short ln;", /* length of vector */ " #else", " unsigned long ln;", /* length of vector */ " #endif", "#endif", "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", " unsigned long m_K1;", "#endif", " unsigned long state;", "} **H_tab, **S_Tab;\n", "typedef struct Trail {", " int st; /* current state */", " int o_tt;", " uchar pr; /* process id */", " uchar tau; /* 8 bit-flags */", " uchar o_pm; /* 8 more bit-flags */", "#if 0", " Meaning of bit-flags:", " tau&1 -> timeout enabled", " tau&2 -> request to enable timeout 1 level up (in claim)", " tau&4 -> current transition is a claim move", " tau&8 -> current transition is an atomic move", " tau&16 -> last move was truncated on stack", " tau&32 -> current transition is a preselected move", " tau&64 -> at least one next state is not on the stack", " tau&128 -> current transition is a stutter move", " o_pm&1 -> the current pid moved -- implements else", " o_pm&2 -> this is an acceptance state", " o_pm&4 -> this is a progress state", " o_pm&8 -> fairness alg rule 1 undo mark", " o_pm&16 -> fairness alg rule 3 undo mark", " o_pm&32 -> fairness alg rule 2 undo mark", " o_pm&64 -> the current proc applied rule2", " o_pm&128 -> a fairness, dummy move - all procs blocked", "#endif", "#ifdef NSUCC", " uchar n_succ; /* nr of successor states */", "#endif", "#if defined(FULLSTACK) && defined(MA) && !defined(BFS)", " uchar proviso;", "#endif", "#ifndef BFS", " uchar o_n, o_ot; /* to save locals */", "#endif", " uchar o_m;", "#ifdef EVENT_TRACE", " #if nstates_event<256", " uchar o_event;", " #else", " unsigned short o_event;", " #endif", "#endif", "#ifndef BFS", " short o_To;", " #ifdef T_RAND", " short oo_i;", " #endif", "#endif", "#if defined(HAS_UNLESS) && !defined(BFS)", " int e_state; /* if escape trans - state of origin */", "#endif", "#if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)", " struct H_el *ostate; /* pointer to stored state */", "#endif", /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY, uses LL[] */ "#if defined(CNTRSTACK) && !defined(BFS)", " long j6, j7;", "#endif", " Trans *o_t;", /* transition fct, next state */ "#if !defined(BFS) && !defined(TRIX_ORIG)", " char *p_bup;", " char *q_bup;", "#endif", "#ifdef BCS", " unsigned short sched_limit;", " unsigned char bcs; /* phase 1 or 2, or forced 4 */", " unsigned char b_pno; /* preferred pid */", "#endif", "#ifdef P_RAND", /* process scheduling randomization */ " unsigned char p_left; /* nr of procs left to explore */", " short p_skip; /* to find starting point in list */", "#endif", "#ifdef HAS_SORTED", " short ipt;", /* insertion slot in q */ "#endif", " union {", " int oval;", /* single backup value of variable */ " int *ovals;", /* ptr to multiple values */ " } bup;", "} Trail;", "Trail *trail, *trpt;", "FILE *efd;", "uchar *this;", "long maxdepth=10000;", "long omaxdepth=10000;", "#ifdef BCS", " /* bitflags in trpt->bcs */", " #define B_PHASE1 1", " #define B_PHASE2 2", " #define B_FORCED 4", "int sched_max = 0;", "#endif", "#ifdef PERMUTED", " uchar permuted = 1;", "#else", " uchar permuted = 0;", "#endif", "double quota; /* time limit */", "#if NCORE>1", "long z_handoff = -1;", "#endif", "#ifdef SC", /* stack cycling */ "char *stackfile;", "#endif", "uchar *SS, *LL;", "uchar HASH_NR = 0;", "", "double memcnt = (double) 0;", "double memlim = (double) (1<<30); /* 1 GB */", "#if NCORE>1", "double mem_reserved = (double) 0;", "#endif", "", "/* for emalloc: */", "static char *have;", "static long left = 0L;", "static double fragment = (double) 0;", "static unsigned long grow;", "",#if 1 "unsigned int HASH_CONST[] = {", " /* asuming 4 bytes per int */", " 0x100d4e63, 0x0fc22f87,", " 0x3ff0c3ff, 0x38e84cd7,", " 0x02b148e9, 0x98b2e49d,", " 0xb616d379, 0xa5247fd9,", " 0xbae92a15, 0xb91c8bc5,", " 0x8e5880f3, 0xacd7c069,", " 0xb4c44bb3, 0x2ead1fb7,", " 0x8e428171, 0xdbebd459,", " 0x00400007, 0x04c11db7,", " 0x828ae611, 0x6cb25933,", " 0x86cdd651, 0x9e8f5f21,", " 0xd5f8d8e7, 0x9c4e956f,", " 0xb5cf2c71, 0x2e805a6d,", " 0x33fc3a55, 0xaf203ed1,", " 0xe31f5909, 0x5276db35,", " 0x0c565ef7, 0x273d1aa5,", " 0x8923b1dd, 0xa9acaac5,", " 0xd1f69207, 0xedfd944b,", " 0x9a68e46b, 0x5355e13f,", " 0x7eeb44f9, 0x932beea9,", " 0x330c4cd3, 0x87f34e5f,", " 0x1b5851b7, 0xb9ca6447,", " 0x58f96a8f, 0x1b3b5307,", " 0x31c387b3, 0xf35f0f35,", " 0xa0acc4df, 0xf3140303,", " 0x2446245d, 0xe4b8f4ef,", " 0x5c007383, 0x68e648af,", " 0x1814fba7, 0xcdf731b5,", " 0xd09ccb4b, 0xb92d0eff,", " 0xcc3c6b67, 0xd3af6a57,", " 0xf44fc3f5, 0x5bb67623,", " 0xaeb9c953, 0x5e0ac739,", " 0x3a7fda09, 0x5edf39eb,", " 0x661eefd9, 0x6423f0d1,", " 0x910fe413, 0x9ec92297,", " 0x4bd8159d, 0xa7b16ee1,", " 0x89d484e9, 0x7f305cb3,", " 0xc5f303e7, 0x415deeef,", " 0x09986f89, 0x7e9c4117,", " 0x0b7cbedb, 0xf9ed7561,", " 0x7a20ac99, 0xf05adef3,", " 0x5893d75b, 0x44d73327,", " 0xb583c873, 0x324d2145,", " 0x7fa3829b, 0xe4b47a23,", " 0xe256d94f, 0xb1fd8959,", " 0xe561a321, 0x1435ac09,", " 0xdd62408b, 0x02ec0bcb,", " 0x5469b785, 0x2f4f50bb,", " 0x20f19395, 0xf96ba085,", " 0x2381f937, 0x768e2a11,", " 0", "};",#else "unsigned int HASH_CONST[] = {", " /* asuming 4 bytes per int */", " 0x88888EEF, 0x00400007,", " 0x04c11db7, 0x100d4e63,", " 0x0fc22f87, 0x3ff0c3ff,", " 0x38e84cd7, 0x02b148e9,", " 0x98b2e49d, 0xb616d379,", " 0xa5247fd9, 0xbae92a15,", " 0xb91c8bc5, 0x8e5880f3,", " 0xacd7c069, 0xb4c44bb3,", " 0x2ead1fb7, 0x8e428171,", " 0xdbebd459, 0x828ae611,", " 0x6cb25933, 0x86cdd651,", " 0x9e8f5f21, 0xd5f8d8e7,", " 0x9c4e956f, 0xb5cf2c71,", " 0x2e805a6d, 0x33fc3a55,", " 0xaf203ed1, 0xe31f5909,", " 0x5276db35, 0x0c565ef7,", " 0x273d1aa5, 0x8923b1dd,", " 0", "};",#endif "#if NCORE>1", "extern int core_id;", "#endif", "long mreached=0;", "int done=0, errors=0, Nrun=1;", "int c_init_done=0;", "char *c_stack_start = (char *) 0;", "double nstates=0, nlinks=0, truncs=0, truncs2=0;", "double nlost=0, nShadow=0, hcmp=0, ngrabs=0;", "#ifdef PUTPID", "char *progname;", "#endif", "#if defined(ZAPH) && defined(BITSTATE)", "double zstates = 0;", "#endif", "int c_init_run;", "#ifdef BFS", "double midrv=0, failedrv=0, revrv=0;", "#endif", "unsigned long nr_states=0; /* nodes in DFA */", "long Fa=0, Fh=0, Zh=0, Zn=0;", "long PUT=0, PROBE=0, ZAPS=0;", "long Ccheck=0, Cholds=0;", "int a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;", "#ifdef HAS_CODE", "int gui = 0, coltrace = 0, readtrail = 0;", "int whichtrail = 0, whichclaim = -1, onlyproc = -1, silent = 0;", "char *claimname;", "#endif", "int state_tables=0, fairness=0, no_rck=0, Nr_Trails=0, dodot=0;", "char simvals[128];", "#ifndef INLINE", "int TstOnly=0;", "#endif", "unsigned long mask, nmask;", "#ifdef BITSTATE", "int ssize=23; /* 1 Mb */", "#else", "int ssize=19; /* 512K slots */", "#endif", "int hmax=0, svmax=0, smax=0;", "int Maxbody=0, XX;", "uchar *noptr, *noqptr; /* used by Pptr(x) and Qptr(x) */", "#ifdef VAR_RANGES", "void logval(char *, int);", "void dumpranges(void);", "#endif", "#ifdef MA", "#define INLINE_REV", "extern void dfa_init(unsigned short);", "extern int dfa_member(unsigned long);", "extern int dfa_store(uchar *);", "unsigned int maxgs = 0;", "#endif", "", "#ifdef ALIGNED", " State comp_now __attribute__ ((aligned (8)));", " /* gcc 64-bit aligned for Itanium2 systems */", " /* MAJOR runtime penalty if not used on those systems */", "#else", " State comp_now; /* compressed state vector */", "#endif", "", "State comp_msk;", "uchar *Mask = (uchar *) &comp_msk;", "#ifdef COLLAPSE", "State comp_tmp;", "static char *scratch = (char *) &comp_tmp;", "#endif", "_Stack *stack; /* for queues, processes */", "Svtack *svtack; /* for old state vectors */", "#ifdef BITSTATE", "static unsigned int hfns = 3; /* new default */", "#endif", "static unsigned long j1_spin; /* 5.2.1: avoid nameclash with math.h */", "static unsigned long K1, K2;", "static unsigned long j2, j3, j4;", "#ifdef BITSTATE", "static long udmem;", "#endif", "static long A_depth = 0;", "long depth = 0;", /* depth: not static to support -S2, but possible clash with embedded code */ "#if NCORE>1", "long nr_handoffs = 0;", "#endif", "static uchar warned = 0, iterative = 0, exclusive = 0, like_java = 0, every_error = 0;", "static uchar noasserts = 0, noends = 0, bounded = 0;", "#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)", "unsigned int s_rand = 123; /* default seed */", "#endif", "#if SYNC>0 && ASYNC==0", "void set_recvs(void);", "int no_recvs(int);", "#endif", "#if SYNC", "#define IfNotBlocked if (boq != -1) continue;", "#define UnBlock boq = -1", "#else", "#define IfNotBlocked /* cannot block */", "#define UnBlock /* don't bother */", "#endif\n", "#ifdef BITSTATE", "int (*bstore)(char *, int);", "int bstore_reg(char *, int);", "int bstore_mod(char *, int);", "#endif", "void active_procs(void);", "void cleanup(void);", "void do_the_search(void);", "void find_shorter(int);", "void iniglobals(int);", "void stopped(int);", "void wrapup(void);", "int *grab_ints(int);", "void ungrab_ints(int *, int);", 0,}; static char *Tail[] = { "Trans *", "settr( int t_id, int a, int b, int c, int d,", " char *t, int g, int tpe0, int tpe1)", "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", " tmp->atom = a&(6|32); /* only (2|8|32) have meaning */", " if (!g) tmp->atom |= 8; /* no global references */", " tmp->st = b;", " tmp->tpe[0] = tpe0;", " tmp->tpe[1] = tpe1;", " tmp->tp = t;", " tmp->t_id = t_id;", " tmp->forw = c;", " tmp->back = d;", " return tmp;", "}\n", "Trans *", "cpytr(Trans *a)", "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", " int i;", " tmp->atom = a->atom;", " tmp->st = a->st;", "#ifdef HAS_UNLESS", " tmp->e_trans = a->e_trans;", " for (i = 0; i < HAS_UNLESS; i++)", " tmp->escp[i] = a->escp[i];", "#endif", " tmp->tpe[0] = a->tpe[0];", " tmp->tpe[1] = a->tpe[1];", " for (i = 0; i < 6; i++)", " { tmp->qu[i] = a->qu[i];", " tmp->ty[i] = a->ty[i];", " }", " tmp->tp = (char *) emalloc(strlen(a->tp)+1);", " strcpy(tmp->tp, a->tp);",Lines 1–500 of 1153. Load more
/***** spin: pangen2.h *****/ /* Copyright (c) 1989-2007 by Lucent Technologies, Bell Laboratories. */ /* All Rights Reserved. This software is for educational purposes only. */ /* No guarantee whatsoever is expressed or implied by the distribution of */ /* this code. Permission is given to distribute this code provided that */ /* this introductory message is not removed and no monies are exchanged. */ /* Software written by Gerard J. Holzmann. For tool documentation see: */ /* http://spinroot.com/ */ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ /* (c) 2007: small additions for V5.0 to support multi-core verifications */ static char *Pre0[] = { "#ifdef SC", "#define _FILE_OFFSET_BITS 64", /* to allow file sizes greater than 2Gb */ "#endif", "#include <stdio.h>", "#include <signal.h>", "#include <stdlib.h>", "#include <stdarg.h>", "#include <string.h>", "#include <ctype.h>", "#include <errno.h>", "#if defined(WIN32) || defined(WIN64)", "#include <time.h>", "#else", "#include <unistd.h>", "#include <sys/times.h>", "#endif", "#include <sys/types.h>", /* defines off_t */ "#include <sys/stat.h>", "#include <fcntl.h>", "#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))", "#ifndef max", "#define max(a,b) (((a)<(b)) ? (b) : (a))", "#endif", "#ifndef PRINTF", "int Printf(const char *fmt, ...); /* prototype only */", "#endif", 0, }; static char *Preamble[] = { "#ifdef RANDOMIZE", " #define T_RAND RANDOMIZE", "#endif", "#ifdef CNTRSTACK", " #define onstack_now() (LL[trpt->j6] && LL[trpt->j7])", " #define onstack_put() LL[trpt->j6]++; LL[trpt->j7]++", " #define onstack_zap() LL[trpt->j6]--; LL[trpt->j7]--", "#endif", "#if !defined(SAFETY) && !defined(NOCOMP)", /* * V_A identifies states in the current statespace * A_V identifies states in the 'other' statespace * S_A remembers how many leading bytes in the sv * are used for these markers + fairness bits */ " #define V_A (((now._a_t&1)?2:1) << (now._a_t&2))", " #define A_V (((now._a_t&1)?1:2) << (now._a_t&2))", " int S_A = 0;", "#else", " #define V_A 0", " #define A_V 0", " #define S_A 0", "#endif", "#ifdef MA", "#undef onstack_now", "#undef onstack_put", "#undef onstack_zap", "#define onstack_put() ;", "#define onstack_zap() gstore((char *) &now, vsize, 4)", "#else", "#if defined(FULLSTACK) && !defined(BITSTATE)", "#define onstack_put() trpt->ostate = Lstate", "#define onstack_zap() { \\", " if (trpt->ostate) \\", " trpt->ostate->tagged = \\", " (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\", " }", "#endif", "#endif", "#ifndef NO_V_PROVISO", "#define V_PROVISO", "#endif", "#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && NCORE==1", " #define AUTO_RESIZE", "#endif", "", "struct H_el {", " struct H_el *nxt;", "#ifdef FULLSTACK", " unsigned int tagged;", " #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)", " unsigned int proviso;", /* uses just 1 bit 0/1 */ " #endif", "#endif", "#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))", " unsigned long st_id;", "#endif", "#if !defined(SAFETY) || defined(REACH)", " unsigned int D;", "#endif", "#ifdef BCS", " #ifndef CONSERVATIVE", " #define CONSERVATIVE 1 /* good for up to 8 processes */", " #endif", " #ifdef CONSERVATIVE", " #if CONSERVATIVE <= 0 || CONSERVATIVE>32", " #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)", " #endif", " uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */ " #endif", " uchar ctx_low;", /* lowest nr of context switches seen so far */ "#endif", "#if NCORE>1", " /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */", " #ifdef V_PROVISO", " uchar cpu_id; /* id of cpu that created the state */", " #endif", "#endif", "#ifdef COLLAPSE", " #if VECTORSZ<65536", " unsigned short ln;", /* length of vector */ " #else", " unsigned long ln;", /* length of vector */ " #endif", "#endif", "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", " unsigned long m_K1;", "#endif", " unsigned long state;", "} **H_tab, **S_Tab;\n", "typedef struct Trail {", " int st; /* current state */", " int o_tt;", " uchar pr; /* process id */", " uchar tau; /* 8 bit-flags */", " uchar o_pm; /* 8 more bit-flags */", "#if 0", " Meaning of bit-flags:", " tau&1 -> timeout enabled", " tau&2 -> request to enable timeout 1 level up (in claim)", " tau&4 -> current transition is a claim move", " tau&8 -> current transition is an atomic move", " tau&16 -> last move was truncated on stack", " tau&32 -> current transition is a preselected move", " tau&64 -> at least one next state is not on the stack", " tau&128 -> current transition is a stutter move", " o_pm&1 -> the current pid moved -- implements else", " o_pm&2 -> this is an acceptance state", " o_pm&4 -> this is a progress state", " o_pm&8 -> fairness alg rule 1 undo mark", " o_pm&16 -> fairness alg rule 3 undo mark", " o_pm&32 -> fairness alg rule 2 undo mark", " o_pm&64 -> the current proc applied rule2", " o_pm&128 -> a fairness, dummy move - all procs blocked", "#endif", "#ifdef NSUCC", " uchar n_succ; /* nr of successor states */", "#endif", "#if defined(FULLSTACK) && defined(MA) && !defined(BFS)", " uchar proviso;", "#endif", "#ifndef BFS", " uchar o_n, o_ot; /* to save locals */", "#endif", " uchar o_m;", "#ifdef EVENT_TRACE", " #if nstates_event<256", " uchar o_event;", " #else", " unsigned short o_event;", " #endif", "#endif", "#ifndef BFS", " short o_To;", " #ifdef T_RAND", " short oo_i;", " #endif", "#endif", "#if defined(HAS_UNLESS) && !defined(BFS)", " int e_state; /* if escape trans - state of origin */", "#endif", "#if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)", " struct H_el *ostate; /* pointer to stored state */", "#endif", /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY, uses LL[] */ "#if defined(CNTRSTACK) && !defined(BFS)", " long j6, j7;", "#endif", " Trans *o_t;", /* transition fct, next state */ "#if !defined(BFS) && !defined(TRIX_ORIG)", " char *p_bup;", " char *q_bup;", "#endif", "#ifdef BCS", " unsigned short sched_limit;", " unsigned char bcs; /* phase 1 or 2, or forced 4 */", " unsigned char b_pno; /* preferred pid */", "#endif", "#ifdef P_RAND", /* process scheduling randomization */ " unsigned char p_left; /* nr of procs left to explore */", " short p_skip; /* to find starting point in list */", "#endif", "#ifdef HAS_SORTED", " short ipt;", /* insertion slot in q */ "#endif", " union {", " int oval;", /* single backup value of variable */ " int *ovals;", /* ptr to multiple values */ " } bup;", "} Trail;", "Trail *trail, *trpt;", "FILE *efd;", "uchar *this;", "long maxdepth=10000;", "long omaxdepth=10000;", "#ifdef BCS", " /* bitflags in trpt->bcs */", " #define B_PHASE1 1", " #define B_PHASE2 2", " #define B_FORCED 4", "int sched_max = 0;", "#endif", "#ifdef PERMUTED", " uchar permuted = 1;", "#else", " uchar permuted = 0;", "#endif", "double quota; /* time limit */", "#if NCORE>1", "long z_handoff = -1;", "#endif", "#ifdef SC", /* stack cycling */ "char *stackfile;", "#endif", "uchar *SS, *LL;", "uchar HASH_NR = 0;", "", "double memcnt = (double) 0;", "double memlim = (double) (1<<30); /* 1 GB */", "#if NCORE>1", "double mem_reserved = (double) 0;", "#endif", "", "/* for emalloc: */", "static char *have;", "static long left = 0L;", "static double fragment = (double) 0;", "static unsigned long grow;", "", #if 1 "unsigned int HASH_CONST[] = {", " /* asuming 4 bytes per int */", " 0x100d4e63, 0x0fc22f87,", " 0x3ff0c3ff, 0x38e84cd7,", " 0x02b148e9, 0x98b2e49d,", " 0xb616d379, 0xa5247fd9,", " 0xbae92a15, 0xb91c8bc5,", " 0x8e5880f3, 0xacd7c069,", " 0xb4c44bb3, 0x2ead1fb7,", " 0x8e428171, 0xdbebd459,", " 0x00400007, 0x04c11db7,", " 0x828ae611, 0x6cb25933,", " 0x86cdd651, 0x9e8f5f21,", " 0xd5f8d8e7, 0x9c4e956f,", " 0xb5cf2c71, 0x2e805a6d,", " 0x33fc3a55, 0xaf203ed1,", " 0xe31f5909, 0x5276db35,", " 0x0c565ef7, 0x273d1aa5,", " 0x8923b1dd, 0xa9acaac5,", " 0xd1f69207, 0xedfd944b,", " 0x9a68e46b, 0x5355e13f,", " 0x7eeb44f9, 0x932beea9,", " 0x330c4cd3, 0x87f34e5f,", " 0x1b5851b7, 0xb9ca6447,", " 0x58f96a8f, 0x1b3b5307,", " 0x31c387b3, 0xf35f0f35,", " 0xa0acc4df, 0xf3140303,", " 0x2446245d, 0xe4b8f4ef,", " 0x5c007383, 0x68e648af,", " 0x1814fba7, 0xcdf731b5,", " 0xd09ccb4b, 0xb92d0eff,", " 0xcc3c6b67, 0xd3af6a57,", " 0xf44fc3f5, 0x5bb67623,", " 0xaeb9c953, 0x5e0ac739,", " 0x3a7fda09, 0x5edf39eb,", " 0x661eefd9, 0x6423f0d1,", " 0x910fe413, 0x9ec92297,", " 0x4bd8159d, 0xa7b16ee1,", " 0x89d484e9, 0x7f305cb3,", " 0xc5f303e7, 0x415deeef,", " 0x09986f89, 0x7e9c4117,", " 0x0b7cbedb, 0xf9ed7561,", " 0x7a20ac99, 0xf05adef3,", " 0x5893d75b, 0x44d73327,", " 0xb583c873, 0x324d2145,", " 0x7fa3829b, 0xe4b47a23,", " 0xe256d94f, 0xb1fd8959,", " 0xe561a321, 0x1435ac09,", " 0xdd62408b, 0x02ec0bcb,", " 0x5469b785, 0x2f4f50bb,", " 0x20f19395, 0xf96ba085,", " 0x2381f937, 0x768e2a11,", " 0", "};", #else "unsigned int HASH_CONST[] = {", " /* asuming 4 bytes per int */", " 0x88888EEF, 0x00400007,", " 0x04c11db7, 0x100d4e63,", " 0x0fc22f87, 0x3ff0c3ff,", " 0x38e84cd7, 0x02b148e9,", " 0x98b2e49d, 0xb616d379,", " 0xa5247fd9, 0xbae92a15,", " 0xb91c8bc5, 0x8e5880f3,", " 0xacd7c069, 0xb4c44bb3,", " 0x2ead1fb7, 0x8e428171,", " 0xdbebd459, 0x828ae611,", " 0x6cb25933, 0x86cdd651,", " 0x9e8f5f21, 0xd5f8d8e7,", " 0x9c4e956f, 0xb5cf2c71,", " 0x2e805a6d, 0x33fc3a55,", " 0xaf203ed1, 0xe31f5909,", " 0x5276db35, 0x0c565ef7,", " 0x273d1aa5, 0x8923b1dd,", " 0", "};", #endif "#if NCORE>1", "extern int core_id;", "#endif", "long mreached=0;", "int done=0, errors=0, Nrun=1;", "int c_init_done=0;", "char *c_stack_start = (char *) 0;", "double nstates=0, nlinks=0, truncs=0, truncs2=0;", "double nlost=0, nShadow=0, hcmp=0, ngrabs=0;", "#ifdef PUTPID", "char *progname;", "#endif", "#if defined(ZAPH) && defined(BITSTATE)", "double zstates = 0;", "#endif", "int c_init_run;", "#ifdef BFS", "double midrv=0, failedrv=0, revrv=0;", "#endif", "unsigned long nr_states=0; /* nodes in DFA */", "long Fa=0, Fh=0, Zh=0, Zn=0;", "long PUT=0, PROBE=0, ZAPS=0;", "long Ccheck=0, Cholds=0;", "int a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;", "#ifdef HAS_CODE", "int gui = 0, coltrace = 0, readtrail = 0;", "int whichtrail = 0, whichclaim = -1, onlyproc = -1, silent = 0;", "char *claimname;", "#endif", "int state_tables=0, fairness=0, no_rck=0, Nr_Trails=0, dodot=0;", "char simvals[128];", "#ifndef INLINE", "int TstOnly=0;", "#endif", "unsigned long mask, nmask;", "#ifdef BITSTATE", "int ssize=23; /* 1 Mb */", "#else", "int ssize=19; /* 512K slots */", "#endif", "int hmax=0, svmax=0, smax=0;", "int Maxbody=0, XX;", "uchar *noptr, *noqptr; /* used by Pptr(x) and Qptr(x) */", "#ifdef VAR_RANGES", "void logval(char *, int);", "void dumpranges(void);", "#endif", "#ifdef MA", "#define INLINE_REV", "extern void dfa_init(unsigned short);", "extern int dfa_member(unsigned long);", "extern int dfa_store(uchar *);", "unsigned int maxgs = 0;", "#endif", "", "#ifdef ALIGNED", " State comp_now __attribute__ ((aligned (8)));", " /* gcc 64-bit aligned for Itanium2 systems */", " /* MAJOR runtime penalty if not used on those systems */", "#else", " State comp_now; /* compressed state vector */", "#endif", "", "State comp_msk;", "uchar *Mask = (uchar *) &comp_msk;", "#ifdef COLLAPSE", "State comp_tmp;", "static char *scratch = (char *) &comp_tmp;", "#endif", "_Stack *stack; /* for queues, processes */", "Svtack *svtack; /* for old state vectors */", "#ifdef BITSTATE", "static unsigned int hfns = 3; /* new default */", "#endif", "static unsigned long j1_spin; /* 5.2.1: avoid nameclash with math.h */", "static unsigned long K1, K2;", "static unsigned long j2, j3, j4;", "#ifdef BITSTATE", "static long udmem;", "#endif", "static long A_depth = 0;", "long depth = 0;", /* depth: not static to support -S2, but possible clash with embedded code */ "#if NCORE>1", "long nr_handoffs = 0;", "#endif", "static uchar warned = 0, iterative = 0, exclusive = 0, like_java = 0, every_error = 0;", "static uchar noasserts = 0, noends = 0, bounded = 0;", "#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)", "unsigned int s_rand = 123; /* default seed */", "#endif", "#if SYNC>0 && ASYNC==0", "void set_recvs(void);", "int no_recvs(int);", "#endif", "#if SYNC", "#define IfNotBlocked if (boq != -1) continue;", "#define UnBlock boq = -1", "#else", "#define IfNotBlocked /* cannot block */", "#define UnBlock /* don't bother */", "#endif\n", "#ifdef BITSTATE", "int (*bstore)(char *, int);", "int bstore_reg(char *, int);", "int bstore_mod(char *, int);", "#endif", "void active_procs(void);", "void cleanup(void);", "void do_the_search(void);", "void find_shorter(int);", "void iniglobals(int);", "void stopped(int);", "void wrapup(void);", "int *grab_ints(int);", "void ungrab_ints(int *, int);", 0, }; static char *Tail[] = { "Trans *", "settr( int t_id, int a, int b, int c, int d,", " char *t, int g, int tpe0, int tpe1)", "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", " tmp->atom = a&(6|32); /* only (2|8|32) have meaning */", " if (!g) tmp->atom |= 8; /* no global references */", " tmp->st = b;", " tmp->tpe[0] = tpe0;", " tmp->tpe[1] = tpe1;", " tmp->tp = t;", " tmp->t_id = t_id;", " tmp->forw = c;", " tmp->back = d;", " return tmp;", "}\n", "Trans *", "cpytr(Trans *a)", "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", " int i;", " tmp->atom = a->atom;", " tmp->st = a->st;", "#ifdef HAS_UNLESS", " tmp->e_trans = a->e_trans;", " for (i = 0; i < HAS_UNLESS; i++)", " tmp->escp[i] = a->escp[i];", "#endif", " tmp->tpe[0] = a->tpe[0];", " tmp->tpe[1] = a->tpe[1];", " for (i = 0; i < 6; i++)", " { tmp->qu[i] = a->qu[i];", " tmp->ty[i] = a->ty[i];", " }", " tmp->tp = (char *) emalloc(strlen(a->tp)+1);", " strcpy(tmp->tp, a->tp);",