+++ /dev/null
-#define SpinVersion "Spin Version 5.1.6 -- 9 May 2008"
-#define PanSource "model.spin"
-
-#ifdef WIN64
-#define ONE_L ((unsigned long) 1)
-#define long long long
-#else
-#define ONE_L (1L)
-#endif
-char *TrailFile = PanSource; /* default */
-char *trailfilename;
-#if defined(BFS)
-#ifndef SAFETY
-#define SAFETY
-#endif
-#ifndef XUSAFE
-#define XUSAFE
-#endif
-#endif
-#ifndef uchar
-#define uchar unsigned char
-#endif
-#ifndef uint
-#define uint unsigned int
-#endif
-#define DELTA 500
-#ifdef MA
- #if NCORE>1 && !defined(SEP_STATE)
- #define SEP_STATE
- #endif
-#if MA==1
-#undef MA
-#define MA 100
-#endif
-#endif
-#ifdef W_XPT
-#if W_XPT==1
-#undef W_XPT
-#define W_XPT 1000000
-#endif
-#endif
-#ifndef NFAIR
-#define NFAIR 2 /* must be >= 2 */
-#endif
-#define HAS_CODE
-#define MERGED 1
-#ifdef NP /* includes np_ demon */
-#define HAS_NP 2
-#define VERI 6
-#define endclaim 3 /* none */
-#endif
-#if !defined(NOCLAIM) && !defined NP
-#define VERI 5
-#define endclaim endstate5
-#endif
-typedef struct S_F_MAP {
- char *fnm; int from; int upto;
-} S_F_MAP;
-
-#define nstates5 15 /* :never: */
-#define nstates_claim nstates5
-#define endstate5 14
-short src_ln5 [] = {
- 0, 301, 301, 302, 302, 300, 304, 306,
- 306, 307, 307, 305, 309, 310, 311, 0, };
-S_F_MAP src_file5 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 14 },
- { "-", 15, 16 }
-};
-#define src_claim src_ln5
-uchar reached5 [] = {
- 0, 1, 1, 1, 1, 0, 1, 1,
- 1, 1, 1, 0, 1, 1, 0, 0, };
-uchar *loopstate5;
-#define reached_claim reached5
-
-#define nstates4 44 /* :init: */
-#define endstate4 43
-short src_ln4 [] = {
- 0, 252, 254, 255, 256, 257, 257, 253,
- 260, 253, 260, 262, 264, 265, 266, 267,
- 267, 263, 269, 263, 269, 270, 271, 273,
- 274, 275, 276, 277, 277, 272, 279, 272,
- 279, 281, 282, 283, 284, 285, 285, 280,
- 287, 280, 251, 288, 0, };
-S_F_MAP src_file4 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 43 },
- { "-", 44, 45 }
-};
-uchar reached4 [] = {
- 0, 1, 1, 0, 0, 1, 1, 0,
- 1, 1, 0, 0, 1, 0, 0, 1,
- 1, 0, 1, 1, 0, 0, 0, 1,
- 0, 0, 0, 1, 1, 0, 1, 1,
- 0, 1, 0, 0, 0, 1, 1, 0,
- 1, 1, 0, 0, 0, };
-uchar *loopstate4;
-
-#define nstates3 10 /* cleaner */
-#define endstate3 9
-short src_ln3 [] = {
- 0, 237, 238, 239, 240, 236, 242, 236,
- 235, 243, 0, };
-S_F_MAP src_file3 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 9 },
- { "-", 10, 11 }
-};
-uchar reached3 [] = {
- 0, 1, 0, 0, 1, 0, 1, 1,
- 0, 0, 0, };
-uchar *loopstate3;
-
-#define nstates2 30 /* reader */
-#define endstate2 29
-short src_ln2 [] = {
- 0, 200, 202, 204, 205, 206, 207, 208,
- 208, 203, 210, 203, 201, 216, 218, 219,
- 220, 221, 221, 217, 223, 217, 223, 215,
- 225, 225, 195, 227, 195, 227, 0, };
-S_F_MAP src_file2 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 29 },
- { "-", 30, 31 }
-};
-uchar reached2 [] = {
- 0, 1, 1, 1, 0, 0, 0, 1,
- 1, 0, 1, 1, 0, 1, 1, 0,
- 0, 1, 1, 0, 1, 1, 0, 0,
- 1, 1, 0, 1, 1, 0, 0, };
-uchar *loopstate2;
-
-#define nstates1 52 /* tracer */
-#define endstate1 51
-short src_ln1 [] = {
- 0, 123, 124, 122, 128, 129, 130, 130,
- 127, 132, 126, 135, 135, 136, 136, 134,
- 138, 138, 140, 141, 142, 143, 144, 144,
- 139, 146, 139, 133, 152, 154, 155, 156,
- 157, 157, 153, 159, 153, 159, 161, 164,
- 167, 168, 169, 170, 165, 172, 151, 174,
- 176, 178, 173, 180, 0, };
-S_F_MAP src_file1 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 51 },
- { "-", 52, 53 }
-};
-uchar reached1 [] = {
- 0, 1, 0, 0, 1, 1, 1, 0,
- 1, 1, 0, 1, 1, 1, 0, 1,
- 1, 0, 1, 0, 0, 0, 1, 1,
- 0, 1, 1, 0, 1, 1, 0, 0,
- 1, 1, 0, 1, 1, 0, 0, 0,
- 1, 0, 1, 0, 0, 1, 0, 1,
- 0, 0, 0, 0, 0, };
-uchar *loopstate1;
-
-#define nstates0 32 /* switcher */
-#define endstate0 31
-short src_ln0 [] = {
- 0, 72, 73, 74, 77, 78, 79, 80,
- 80, 75, 82, 71, 85, 85, 86, 86,
- 84, 88, 83, 91, 93, 96, 99, 100,
- 101, 102, 97, 104, 104, 90, 107, 108,
- 0, };
-S_F_MAP src_file0 [] = {
- { "-", 0, 0 },
- { "pan.___", 1, 31 },
- { "-", 32, 33 }
-};
-uchar reached0 [] = {
- 0, 1, 0, 0, 1, 0, 1, 1,
- 0, 0, 1, 0, 1, 1, 1, 0,
- 1, 1, 0, 1, 0, 0, 1, 0,
- 1, 0, 0, 1, 0, 0, 1, 0,
- 0, };
-uchar *loopstate0;
-struct {
- int tp; short *src;
-} src_all[] = {
- { 5, &src_ln5[0] },
- { 4, &src_ln4[0] },
- { 3, &src_ln3[0] },
- { 2, &src_ln2[0] },
- { 1, &src_ln1[0] },
- { 0, &src_ln0[0] },
- { 0, (short *) 0 }
-};
-short *frm_st0;
-struct {
- char *c; char *t;
-} code_lookup[] = {
- { (char *) 0, "" }
-};
-#define _T5 64
-#define _T2 65
-#define T_ID unsigned char
-#define SYNC 0
-#define ASYNC 0
-
-#ifndef NCORE
- #ifdef DUAL_CORE
- #define NCORE 2
- #elif QUAD_CORE
- #define NCORE 4
- #else
- #define NCORE 1
- #endif
-#endif
-char *procname[] = {
- "switcher",
- "tracer",
- "reader",
- "cleaner",
- ":init:",
- ":never:",
- ":np_:",
-};
-
-typedef struct P5 { /* :never: */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
-} P5;
-#define Air5 (sizeof(P5) - 3)
-#define Pinit ((P4 *)this)
-typedef struct P4 { /* :init: */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
- uchar i;
- uchar j;
- uchar sum;
- uchar commit_sum;
-} P4;
-#define Air4 (sizeof(P4) - Offsetof(P4, commit_sum) - 1*sizeof(uchar))
-#define Pcleaner ((P3 *)this)
-typedef struct P3 { /* cleaner */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
-} P3;
-#define Air3 (sizeof(P3) - 3)
-#define Preader ((P2 *)this)
-typedef struct P2 { /* reader */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
- uchar i;
- uchar j;
-} P2;
-#define Air2 (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar))
-#define Ptracer ((P1 *)this)
-typedef struct P1 { /* tracer */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
- uchar size;
- uchar prev_off;
- uchar new_off;
- uchar tmp_commit;
- uchar i;
- uchar j;
-} P1;
-#define Air1 (sizeof(P1) - Offsetof(P1, j) - 1*sizeof(uchar))
-#define Pswitcher ((P0 *)this)
-typedef struct P0 { /* switcher */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
- uchar prev_off;
- uchar new_off;
- uchar tmp_commit;
- uchar size;
-} P0;
-#define Air0 (sizeof(P0) - Offsetof(P0, size) - 1*sizeof(uchar))
-typedef struct P6 { /* np_ */
- unsigned _pid : 8; /* 0..255 */
- unsigned _t : 4; /* proctype */
- unsigned _p : 7; /* state */
-} P6;
-#define Air6 (sizeof(P6) - 3)
-#if defined(BFS) && defined(REACH)
-#undef REACH
-#endif
-#ifdef VERI
-#define BASE 1
-#else
-#define BASE 0
-#endif
-typedef struct Trans {
- short atom; /* if &2 = atomic trans; if &8 local */
-#ifdef HAS_UNLESS
- short escp[HAS_UNLESS]; /* lists the escape states */
- short e_trans; /* if set, this is an escp-trans */
-#endif
- short tpe[2]; /* class of operation (for reduction) */
- short qu[6]; /* for conditional selections: qid's */
- uchar ty[6]; /* ditto: type's */
-#ifdef NIBIS
- short om; /* completion status of preselects */
-#endif
- char *tp; /* src txt of statement */
- int st; /* the nextstate */
- int t_id; /* transition id, unique within proc */
- int forw; /* index forward transition */
- int back; /* index return transition */
- struct Trans *nxt;
-} Trans;
-
-#define qptr(x) (((uchar *)&now)+(int)q_offset[x])
-#define pptr(x) (((uchar *)&now)+(int)proc_offset[x])
-extern uchar *Pptr(int);
-#define q_sz(x) (((Q0 *)qptr(x))->Qlen)
-
-#ifndef VECTORSZ
-#define VECTORSZ 1024 /* sv size in bytes */
-#endif
-
-#ifdef VERBOSE
-#ifndef CHECK
-#define CHECK
-#endif
-#ifndef DEBUG
-#define DEBUG
-#endif
-#endif
-#ifdef SAFETY
-#ifndef NOFAIR
-#define NOFAIR
-#endif
-#endif
-#ifdef NOREDUCE
-#ifndef XUSAFE
-#define XUSAFE
-#endif
-#if !defined(SAFETY) && !defined(MA)
-#define FULLSTACK
-#endif
-#else
-#ifdef BITSTATE
-#if defined(SAFETY) && !defined(HASH64)
-#define CNTRSTACK
-#else
-#define FULLSTACK
-#endif
-#else
-#define FULLSTACK
-#endif
-#endif
-#ifdef BITSTATE
-#ifndef NOCOMP
-#define NOCOMP
-#endif
-#if !defined(LC) && defined(SC)
-#define LC
-#endif
-#endif
-#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
-/* accept the above for backward compatibility */
-#define COLLAPSE
-#endif
-#ifdef HC
-#undef HC
-#define HC4
-#endif
-#ifdef HC0
-#define HC 0
-#endif
-#ifdef HC1
-#define HC 1
-#endif
-#ifdef HC2
-#define HC 2
-#endif
-#ifdef HC3
-#define HC 3
-#endif
-#ifdef HC4
-#define HC 4
-#endif
-#ifdef COLLAPSE
-#if NCORE>1 && !defined(SEP_STATE)
-unsigned long *ncomps; /* in shared memory */
-#else
-unsigned long ncomps[256+2];
-#endif
-#endif
-#define MAXQ 255
-#define MAXPROC 255
-#define WS sizeof(void *) /* word size in bytes */
-typedef struct Stack { /* for queues and processes */
-#if VECTORSZ>32000
- int o_delta;
- int o_offset;
- int o_skip;
- int o_delqs;
-#else
- short o_delta;
- short o_offset;
- short o_skip;
- short o_delqs;
-#endif
- short o_boq;
-#ifndef XUSAFE
- char *o_name;
-#endif
- char *body;
- struct Stack *nxt;
- struct Stack *lst;
-} Stack;
-
-typedef struct Svtack { /* for complete state vector */
-#if VECTORSZ>32000
- int o_delta;
- int m_delta;
-#else
- short o_delta; /* current size of frame */
- short m_delta; /* maximum size of frame */
-#endif
-#if SYNC
- short o_boq;
-#endif
-#define StackSize (WS)
- char *body;
- struct Svtack *nxt;
- struct Svtack *lst;
-} Svtack;
-
-Trans ***trans; /* 1 ptr per state per proctype */
-
-struct H_el *Lstate;
-int depthfound = -1; /* loop detection */
-#if VECTORSZ>32000
-int proc_offset[MAXPROC];
-int q_offset[MAXQ];
-#else
-short proc_offset[MAXPROC];
-short q_offset[MAXQ];
-#endif
-uchar proc_skip[MAXPROC];
-uchar q_skip[MAXQ];
-unsigned long vsize; /* vector size in bytes */
-#ifdef SVDUMP
-int vprefix=0, svfd; /* runtime option -pN */
-#endif
-char *tprefix = "trail"; /* runtime option -tsuffix */
-short boq = -1; /* blocked_on_queue status */
-typedef struct State {
- uchar _nr_pr;
- uchar _nr_qs;
- uchar _a_t; /* cycle detection */
-#ifndef NOFAIR
- uchar _cnt[NFAIR]; /* counters, weak fairness */
-#endif
-#ifndef NOVSZ
-#if VECTORSZ<65536
- unsigned short _vsz;
-#else
- unsigned long _vsz;
-#endif
-#endif
-#ifdef HAS_LAST
- uchar _last; /* pid executed in last step */
-#endif
-#ifdef EVENT_TRACE
-#if nstates_event<256
- uchar _event;
-#else
- unsigned short _event;
-#endif
-#endif
- uchar buffer_use[4];
- uchar write_off;
- uchar commit_count[2];
- uchar _commit_sum;
- uchar read_off;
- uchar events_lost;
- uchar refcount;
- uchar sv[VECTORSZ];
-} State;
-
-#define HAS_TRACK 0
-/* hidden variable: */ uchar deliver;
-int _; /* a predefined write-only variable */
-
-#define FORWARD_MOVES "pan.m"
-#define REVERSE_MOVES "pan.b"
-#define TRANSITIONS "pan.t"
-#define _NP_ 6
-uchar reached6[3]; /* np_ */
-uchar *loopstate6; /* np_ */
-#define nstates6 3 /* np_ */
-#define endstate6 2 /* np_ */
-
-#define start6 0 /* np_ */
-#define start5 5
-#define start_claim 5
-#define start4 42
-#define start3 8
-#define start2 26
-#define start1 3
-#define start0 11
-#ifdef NP
- #define ACCEPT_LAB 1 /* at least 1 in np_ */
-#else
- #define ACCEPT_LAB 1 /* user-defined accept labels */
-#endif
-#ifdef MEMCNT
- #ifdef MEMLIM
- #warning -DMEMLIM takes precedence over -DMEMCNT
- #undef MEMCNT
- #else
- #if MEMCNT<20
- #warning using minimal value -DMEMCNT=20 (=1MB)
- #define MEMLIM (1)
- #undef MEMCNT
- #else
- #if MEMCNT==20
- #define MEMLIM (1)
- #undef MEMCNT
- #else
- #if MEMCNT>=50
- #error excessive value for MEMCNT
- #else
- #define MEMLIM (1<<(MEMCNT-20))
- #endif
- #endif
- #endif
- #endif
-#endif
-#if NCORE>1 && !defined(MEMLIM)
- #define MEMLIM (2048) /* need a default, using 2 GB */
-#endif
-#define PROG_LAB 0 /* progress labels */
-uchar *accpstate[7];
-uchar *progstate[7];
-uchar *loopstate[7];
-uchar *reached[7];
-uchar *stopstate[7];
-uchar *visstate[7];
-short *mapstate[7];
-#ifdef HAS_CODE
-int NrStates[7];
-#endif
-#define NQS 0
-short q_flds[1];
-short q_max[1];
-typedef struct Q0 { /* generic q */
- uchar Qlen; /* q_size */
- uchar _t;
-} Q0;
-
-/** function prototypes **/
-char *emalloc(unsigned long);
-char *Malloc(unsigned long);
-int Boundcheck(int, int, int, int, Trans *);
-int addqueue(int, int);
-/* int atoi(char *); */
-/* int abort(void); */
-int close(int);
-int delproc(int, int);
-int endstate(void);
-int hstore(char *, int);
-#ifdef MA
-int gstore(char *, int, uchar);
-#endif
-int q_cond(short, Trans *);
-int q_full(int);
-int q_len(int);
-int q_zero(int);
-int qrecv(int, int, int, int);
-int unsend(int);
-/* void *sbrk(int); */
-void Uerror(char *);
-void assert(int, char *, int, int, Trans *);
-void c_chandump(int);
-void c_globals(void);
-void c_locals(int, int);
-void checkcycles(void);
-void crack(int, int, Trans *, short *);
-void d_sfh(const char *, int);
-void sfh(const char *, int);
-void d_hash(uchar *, int);
-void s_hash(uchar *, int);
-void r_hash(uchar *, int);
-void delq(int);
-void do_reach(void);
-void pan_exit(int);
-void exit(int);
-void hinit(void);
-void imed(Trans *, int, int, int);
-void new_state(void);
-void p_restor(int);
-void putpeg(int, int);
-void putrail(void);
-void q_restor(void);
-void retrans(int, int, int, short *, uchar *, uchar *);
-void settable(void);
-void setq_claim(int, int, char *, int, char *);
-void sv_restor(void);
-void sv_save(void);
-void tagtable(int, int, int, short *, uchar *);
-void do_dfs(int, int, int, short *, uchar *, uchar *);
-void uerror(char *);
-void unrecv(int, int, int, int, int);
-void usage(FILE *);
-void wrap_stats(void);
-#if defined(FULLSTACK) && defined(BITSTATE)
-int onstack_now(void);
-void onstack_init(void);
-void onstack_put(void);
-void onstack_zap(void);
-#endif
-#ifndef XUSAFE
-int q_S_check(int, int);
-int q_R_check(int, int);
-uchar q_claim[MAXQ+1];
-char *q_name[MAXQ+1];
-char *p_name[MAXPROC+1];
-#endif
-void qsend(int, int, int);
-#define Addproc(x) addproc(x)
-#define LOCAL 1
-#define Q_FULL_F 2
-#define Q_EMPT_F 3
-#define Q_EMPT_T 4
-#define Q_FULL_T 5
-#define TIMEOUT_F 6
-#define GLOBAL 7
-#define BAD 8
-#define ALPHA_F 9
-#define NTRANS 66
-#ifdef PEG
-long peg[NTRANS];
-#endif