verif/md/pan.h

   1 #define SpinVersion     "Spin Version 5.1.6 -- 9 May 2008"
   2 #define PanSource       "model.spin"
   3
   4 #ifdef WIN64
   5 #define ONE_L   ((unsigned long) 1)
   6 #define long    long long
   7 #else
   8 #define ONE_L   (1L)
   9 #endif
  10 char *TrailFile = PanSource; /* default */
  11 char *trailfilename;
  12 #if defined(BFS)
  13 #ifndef SAFETY
  14 #define SAFETY
  15 #endif
  16 #ifndef XUSAFE
  17 #define XUSAFE
  18 #endif
  19 #endif
  20 #ifndef uchar
  21 #define uchar   unsigned char
  22 #endif
  23 #ifndef uint
  24 #define uint    unsigned int
  25 #endif
  26 #define DELTA   500
  27 #ifdef MA
  28         #if NCORE>1 && !defined(SEP_STATE)
  29         #define SEP_STATE
  30         #endif
  31 #if MA==1
  32 #undef MA
  33 #define MA      100
  34 #endif
  35 #endif
  36 #ifdef W_XPT
  37 #if W_XPT==1
  38 #undef W_XPT
  39 #define W_XPT 1000000
  40 #endif
  41 #endif
  42 #ifndef NFAIR
  43 #define NFAIR   2       /* must be >= 2 */
  44 #endif
  45 #define HAS_CODE
  46 #define MERGED  1
  47 #ifdef NP       /* includes np_ demon */
  48 #define HAS_NP  2
  49 #define VERI    6
  50 #define endclaim        3 /* none */
  51 #endif
  52 #if !defined(NOCLAIM) && !defined NP
  53 #define VERI    5
  54 #define endclaim        endstate5
  55 #endif
  56 typedef struct S_F_MAP {
  57         char *fnm; int from; int upto;
  58 } S_F_MAP;
  59
  60 #define nstates5        15      /* :never: */
  61 #define nstates_claim   nstates5
  62 #define endstate5       14
  63 short src_ln5 [] = {
  64           0, 301, 301, 302, 302, 300, 304, 306,
  65         306, 307, 307, 305, 309, 310, 311,   0, };
  66 S_F_MAP src_file5 [] = {
  67         { "-", 0, 0 },
  68         { "pan.___", 1, 14 },
  69         { "-", 15, 16 }
  70 };
  71 #define src_claim       src_ln5
  72 uchar reached5 [] = {
  73           0,   1,   1,   1,   1,   0,   1,   1,
  74           1,   1,   1,   0,   1,   1,   0,   0, };
  75 uchar *loopstate5;
  76 #define reached_claim   reached5
  77
  78 #define nstates4        44      /* :init: */
  79 #define endstate4       43
  80 short src_ln4 [] = {
  81           0, 252, 254, 255, 256, 257, 257, 253,
  82         260, 253, 260, 262, 264, 265, 266, 267,
  83         267, 263, 269, 263, 269, 270, 271, 273,
  84         274, 275, 276, 277, 277, 272, 279, 272,
  85         279, 281, 282, 283, 284, 285, 285, 280,
  86         287, 280, 251, 288,   0, };
  87 S_F_MAP src_file4 [] = {
  88         { "-", 0, 0 },
  89         { "pan.___", 1, 43 },
  90         { "-", 44, 45 }
  91 };
  92 uchar reached4 [] = {
  93           0,   1,   1,   0,   0,   1,   1,   0,
  94           1,   1,   0,   0,   1,   0,   0,   1,
  95           1,   0,   1,   1,   0,   0,   0,   1,
  96           0,   0,   0,   1,   1,   0,   1,   1,
  97           0,   1,   0,   0,   0,   1,   1,   0,
  98           1,   1,   0,   0,   0, };
  99 uchar *loopstate4;
 100
 101 #define nstates3        10      /* cleaner */
 102 #define endstate3       9
 103 short src_ln3 [] = {
 104           0, 237, 238, 239, 240, 236, 242, 236,
 105         235, 243,   0, };
 106 S_F_MAP src_file3 [] = {
 107         { "-", 0, 0 },
 108         { "pan.___", 1, 9 },
 109         { "-", 10, 11 }
 110 };
 111 uchar reached3 [] = {
 112           0,   1,   0,   0,   1,   0,   1,   1,
 113           0,   0,   0, };
 114 uchar *loopstate3;
 115
 116 #define nstates2        30      /* reader */
 117 #define endstate2       29
 118 short src_ln2 [] = {
 119           0, 200, 202, 204, 205, 206, 207, 208,
 120         208, 203, 210, 203, 201, 216, 218, 219,
 121         220, 221, 221, 217, 223, 217, 223, 215,
 122         225, 225, 195, 227, 195, 227,   0, };
 123 S_F_MAP src_file2 [] = {
 124         { "-", 0, 0 },
 125         { "pan.___", 1, 29 },
 126         { "-", 30, 31 }
 127 };
 128 uchar reached2 [] = {
 129           0,   1,   1,   1,   0,   0,   0,   1,
 130           1,   0,   1,   1,   0,   1,   1,   0,
 131           0,   1,   1,   0,   1,   1,   0,   0,
 132           1,   1,   0,   1,   1,   0,   0, };
 133 uchar *loopstate2;
 134
 135 #define nstates1        52      /* tracer */
 136 #define endstate1       51
 137 short src_ln1 [] = {
 138           0, 123, 124, 122, 128, 129, 130, 130,
 139         127, 132, 126, 135, 135, 136, 136, 134,
 140         138, 138, 140, 141, 142, 143, 144, 144,
 141         139, 146, 139, 133, 152, 154, 155, 156,
 142         157, 157, 153, 159, 153, 159, 161, 164,
 143         167, 168, 169, 170, 165, 172, 151, 174,
 144         176, 178, 173, 180,   0, };
 145 S_F_MAP src_file1 [] = {
 146         { "-", 0, 0 },
 147         { "pan.___", 1, 51 },
 148         { "-", 52, 53 }
 149 };
 150 uchar reached1 [] = {
 151           0,   1,   0,   0,   1,   1,   1,   0,
 152           1,   1,   0,   1,   1,   1,   0,   1,
 153           1,   0,   1,   0,   0,   0,   1,   1,
 154           0,   1,   1,   0,   1,   1,   0,   0,
 155           1,   1,   0,   1,   1,   0,   0,   0,
 156           1,   0,   1,   0,   0,   1,   0,   1,
 157           0,   0,   0,   0,   0, };
 158 uchar *loopstate1;
 159
 160 #define nstates0        32      /* switcher */
 161 #define endstate0       31
 162 short src_ln0 [] = {
 163           0,  72,  73,  74,  77,  78,  79,  80,
 164          80,  75,  82,  71,  85,  85,  86,  86,
 165          84,  88,  83,  91,  93,  96,  99, 100,
 166         101, 102,  97, 104, 104,  90, 107, 108,
 167           0, };
 168 S_F_MAP src_file0 [] = {
 169         { "-", 0, 0 },
 170         { "pan.___", 1, 31 },
 171         { "-", 32, 33 }
 172 };
 173 uchar reached0 [] = {
 174           0,   1,   0,   0,   1,   0,   1,   1,
 175           0,   0,   1,   0,   1,   1,   1,   0,
 176           1,   1,   0,   1,   0,   0,   1,   0,
 177           1,   0,   0,   1,   0,   0,   1,   0,
 178           0, };
 179 uchar *loopstate0;
 180 struct {
 181         int tp; short *src;
 182 } src_all[] = {
 183         { 5, &src_ln5[0] },
 184         { 4, &src_ln4[0] },
 185         { 3, &src_ln3[0] },
 186         { 2, &src_ln2[0] },
 187         { 1, &src_ln1[0] },
 188         { 0, &src_ln0[0] },
 189         { 0, (short *) 0 }
 190 };
 191 short *frm_st0;
 192 struct {
 193         char *c; char *t;
 194 } code_lookup[] = {
 195         { (char *) 0, "" }
 196 };
 197 #define _T5     64
 198 #define _T2     65
 199 #define T_ID    unsigned char
 200 #define SYNC    0
 201 #define ASYNC   0
 202
 203 #ifndef NCORE
 204         #ifdef DUAL_CORE
 205                 #define NCORE   2
 206         #elif QUAD_CORE
 207                 #define NCORE   4
 208         #else
 209                 #define NCORE   1
 210         #endif
 211 #endif
 212 char *procname[] = {
 213    "switcher",
 214    "tracer",
 215    "reader",
 216    "cleaner",
 217    ":init:",
 218    ":never:",
 219    ":np_:",
 220 };
 221
 222 typedef struct P5 { /* :never: */
 223         unsigned _pid : 8;  /* 0..255 */
 224         unsigned _t   : 4; /* proctype */
 225         unsigned _p   : 7; /* state    */
 226 } P5;
 227 #define Air5    (sizeof(P5) - 3)
 228 #define Pinit   ((P4 *)this)
 229 typedef struct P4 { /* :init: */
 230         unsigned _pid : 8;  /* 0..255 */
 231         unsigned _t   : 4; /* proctype */
 232         unsigned _p   : 7; /* state    */
 233         uchar i;
 234         uchar j;
 235         uchar sum;
 236         uchar commit_sum;
 237 } P4;
 238 #define Air4    (sizeof(P4) - Offsetof(P4, commit_sum) - 1*sizeof(uchar))
 239 #define Pcleaner        ((P3 *)this)
 240 typedef struct P3 { /* cleaner */
 241         unsigned _pid : 8;  /* 0..255 */
 242         unsigned _t   : 4; /* proctype */
 243         unsigned _p   : 7; /* state    */
 244 } P3;
 245 #define Air3    (sizeof(P3) - 3)
 246 #define Preader ((P2 *)this)
 247 typedef struct P2 { /* reader */
 248         unsigned _pid : 8;  /* 0..255 */
 249         unsigned _t   : 4; /* proctype */
 250         unsigned _p   : 7; /* state    */
 251         uchar i;
 252         uchar j;
 253 } P2;
 254 #define Air2    (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar))
 255 #define Ptracer ((P1 *)this)
 256 typedef struct P1 { /* tracer */
 257         unsigned _pid : 8;  /* 0..255 */
 258         unsigned _t   : 4; /* proctype */
 259         unsigned _p   : 7; /* state    */
 260         uchar size;
 261         uchar prev_off;
 262         uchar new_off;
 263         uchar tmp_commit;
 264         uchar i;
 265         uchar j;
 266 } P1;
 267 #define Air1    (sizeof(P1) - Offsetof(P1, j) - 1*sizeof(uchar))
 268 #define Pswitcher       ((P0 *)this)
 269 typedef struct P0 { /* switcher */
 270         unsigned _pid : 8;  /* 0..255 */
 271         unsigned _t   : 4; /* proctype */
 272         unsigned _p   : 7; /* state    */
 273         uchar prev_off;
 274         uchar new_off;
 275         uchar tmp_commit;
 276         uchar size;
 277 } P0;
 278 #define Air0    (sizeof(P0) - Offsetof(P0, size) - 1*sizeof(uchar))
 279 typedef struct P6 { /* np_ */
 280         unsigned _pid : 8;  /* 0..255 */
 281         unsigned _t   : 4; /* proctype */
 282         unsigned _p   : 7; /* state    */
 283 } P6;
 284 #define Air6    (sizeof(P6) - 3)
 285 #if defined(BFS) && defined(REACH)
 286 #undef REACH
 287 #endif
 288 #ifdef VERI
 289 #define BASE    1
 290 #else
 291 #define BASE    0
 292 #endif
 293 typedef struct Trans {
 294         short atom;     /* if &2 = atomic trans; if &8 local */
 295 #ifdef HAS_UNLESS
 296         short escp[HAS_UNLESS]; /* lists the escape states */
 297         short e_trans;  /* if set, this is an escp-trans */
 298 #endif
 299         short tpe[2];   /* class of operation (for reduction) */
 300         short qu[6];    /* for conditional selections: qid's  */
 301         uchar ty[6];    /* ditto: type's */
 302 #ifdef NIBIS
 303         short om;       /* completion status of preselects */
 304 #endif
 305         char *tp;       /* src txt of statement */
 306         int st;         /* the nextstate */
 307         int t_id;       /* transition id, unique within proc */
 308         int forw;       /* index forward transition */
 309         int back;       /* index return  transition */
 310         struct Trans *nxt;
 311 } Trans;
 312
 313 #define qptr(x) (((uchar *)&now)+(int)q_offset[x])
 314 #define pptr(x) (((uchar *)&now)+(int)proc_offset[x])
 315 extern uchar *Pptr(int);
 316 #define q_sz(x) (((Q0 *)qptr(x))->Qlen)
 317
 318 #ifndef VECTORSZ
 319 #define VECTORSZ        1024           /* sv   size in bytes */
 320 #endif
 321
 322 #ifdef VERBOSE
 323 #ifndef CHECK
 324 #define CHECK
 325 #endif
 326 #ifndef DEBUG
 327 #define DEBUG
 328 #endif
 329 #endif
 330 #ifdef SAFETY
 331 #ifndef NOFAIR
 332 #define NOFAIR
 333 #endif
 334 #endif
 335 #ifdef NOREDUCE
 336 #ifndef XUSAFE
 337 #define XUSAFE
 338 #endif
 339 #if !defined(SAFETY) && !defined(MA)
 340 #define FULLSTACK
 341 #endif
 342 #else
 343 #ifdef BITSTATE
 344 #if defined(SAFETY) && !defined(HASH64)
 345 #define CNTRSTACK
 346 #else
 347 #define FULLSTACK
 348 #endif
 349 #else
 350 #define FULLSTACK
 351 #endif
 352 #endif
 353 #ifdef BITSTATE
 354 #ifndef NOCOMP
 355 #define NOCOMP
 356 #endif
 357 #if !defined(LC) && defined(SC)
 358 #define LC
 359 #endif
 360 #endif
 361 #if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
 362 /* accept the above for backward compatibility */
 363 #define COLLAPSE
 364 #endif
 365 #ifdef HC
 366 #undef HC
 367 #define HC4
 368 #endif
 369 #ifdef HC0
 370 #define HC      0
 371 #endif
 372 #ifdef HC1
 373 #define HC      1
 374 #endif
 375 #ifdef HC2
 376 #define HC      2
 377 #endif
 378 #ifdef HC3
 379 #define HC      3
 380 #endif
 381 #ifdef HC4
 382 #define HC      4
 383 #endif
 384 #ifdef COLLAPSE
 385 #if NCORE>1 && !defined(SEP_STATE)
 386 unsigned long *ncomps;  /* in shared memory */
 387 #else
 388 unsigned long ncomps[256+2];
 389 #endif
 390 #endif
 391 #define MAXQ    255
 392 #define MAXPROC 255
 393 #define WS              sizeof(void *) /* word size in bytes */
 394 typedef struct Stack  {  /* for queues and processes */
 395 #if VECTORSZ>32000
 396         int o_delta;
 397         int o_offset;
 398         int o_skip;
 399         int o_delqs;
 400 #else
 401         short o_delta;
 402         short o_offset;
 403         short o_skip;
 404         short o_delqs;
 405 #endif
 406         short o_boq;
 407 #ifndef XUSAFE
 408         char *o_name;
 409 #endif
 410         char *body;
 411         struct Stack *nxt;
 412         struct Stack *lst;
 413 } Stack;
 414
 415 typedef struct Svtack { /* for complete state vector */
 416 #if VECTORSZ>32000
 417         int o_delta;
 418         int m_delta;
 419 #else
 420         short o_delta;   /* current size of frame */
 421         short m_delta;   /* maximum size of frame */
 422 #endif
 423 #if SYNC
 424         short o_boq;
 425 #endif
 426 #define StackSize       (WS)
 427         char *body;
 428         struct Svtack *nxt;
 429         struct Svtack *lst;
 430 } Svtack;
 431
 432 Trans ***trans; /* 1 ptr per state per proctype */
 433
 434 struct H_el *Lstate;
 435 int depthfound = -1;    /* loop detection */
 436 #if VECTORSZ>32000
 437 int proc_offset[MAXPROC];
 438 int q_offset[MAXQ];
 439 #else
 440 short proc_offset[MAXPROC];
 441 short q_offset[MAXQ];
 442 #endif
 443 uchar proc_skip[MAXPROC];
 444 uchar q_skip[MAXQ];
 445 unsigned long  vsize;   /* vector size in bytes */
 446 #ifdef SVDUMP
 447 int vprefix=0, svfd;            /* runtime option -pN */
 448 #endif
 449 char *tprefix = "trail";        /* runtime option -tsuffix */
 450 short boq = -1;         /* blocked_on_queue status */
 451 typedef struct State {
 452         uchar _nr_pr;
 453         uchar _nr_qs;
 454         uchar   _a_t;   /* cycle detection */
 455 #ifndef NOFAIR
 456         uchar   _cnt[NFAIR];    /* counters, weak fairness */
 457 #endif
 458 #ifndef NOVSZ
 459 #if VECTORSZ<65536
 460         unsigned short _vsz;
 461 #else
 462         unsigned long  _vsz;
 463 #endif
 464 #endif
 465 #ifdef HAS_LAST
 466         uchar  _last;   /* pid executed in last step */
 467 #endif
 468 #ifdef EVENT_TRACE
 469 #if nstates_event<256
 470         uchar _event;
 471 #else
 472         unsigned short _event;
 473 #endif
 474 #endif
 475         uchar buffer_use[4];
 476         uchar write_off;
 477         uchar commit_count[2];
 478         uchar _commit_sum;
 479         uchar read_off;
 480         uchar events_lost;
 481         uchar refcount;
 482         uchar sv[VECTORSZ];
 483 } State;
 484
 485 #define HAS_TRACK       0
 486 /* hidden variable: */  uchar deliver;
 487 int _; /* a predefined write-only variable */
 488
 489 #define FORWARD_MOVES   "pan.m"
 490 #define REVERSE_MOVES   "pan.b"
 491 #define TRANSITIONS     "pan.t"
 492 #define _NP_    6
 493 uchar reached6[3];  /* np_ */
 494 uchar *loopstate6;  /* np_ */
 495 #define nstates6        3 /* np_ */
 496 #define endstate6       2 /* np_ */
 497
 498 #define start6  0 /* np_ */
 499 #define start5  5
 500 #define start_claim     5
 501 #define start4  42
 502 #define start3  8
 503 #define start2  26
 504 #define start1  3
 505 #define start0  11
 506 #ifdef NP
 507         #define ACCEPT_LAB      1 /* at least 1 in np_ */
 508 #else
 509         #define ACCEPT_LAB      1 /* user-defined accept labels */
 510 #endif
 511 #ifdef MEMCNT
 512         #ifdef MEMLIM
 513                 #warning -DMEMLIM takes precedence over -DMEMCNT
 514                 #undef MEMCNT
 515         #else
 516                 #if MEMCNT<20
 517                         #warning using minimal value -DMEMCNT=20 (=1MB)
 518                         #define MEMLIM  (1)
 519                         #undef MEMCNT
 520                 #else
 521                         #if MEMCNT==20
 522                                 #define MEMLIM  (1)
 523                                 #undef MEMCNT
 524                         #else
 525                          #if MEMCNT>=50
 526                           #error excessive value for MEMCNT
 527                          #else
 528                                 #define MEMLIM  (1<<(MEMCNT-20))
 529                          #endif
 530                         #endif
 531                 #endif
 532         #endif
 533 #endif
 534 #if NCORE>1 && !defined(MEMLIM)
 535         #define MEMLIM  (2048)  /* need a default, using 2 GB */
 536 #endif
 537 #define PROG_LAB        0 /* progress labels */
 538 uchar *accpstate[7];
 539 uchar *progstate[7];
 540 uchar *loopstate[7];
 541 uchar *reached[7];
 542 uchar *stopstate[7];
 543 uchar *visstate[7];
 544 short *mapstate[7];
 545 #ifdef HAS_CODE
 546 int NrStates[7];
 547 #endif
 548 #define NQS     0
 549 short q_flds[1];
 550 short q_max[1];
 551 typedef struct Q0 {     /* generic q */
 552         uchar Qlen;     /* q_size */
 553         uchar _t;
 554 } Q0;
 555
 556 /** function prototypes **/
 557 char *emalloc(unsigned long);
 558 char *Malloc(unsigned long);
 559 int Boundcheck(int, int, int, int, Trans *);
 560 int addqueue(int, int);
 561 /* int atoi(char *); */
 562 /* int abort(void); */
 563 int close(int);
 564 int delproc(int, int);
 565 int endstate(void);
 566 int hstore(char *, int);
 567 #ifdef MA
 568 int gstore(char *, int, uchar);
 569 #endif
 570 int q_cond(short, Trans *);
 571 int q_full(int);
 572 int q_len(int);
 573 int q_zero(int);
 574 int qrecv(int, int, int, int);
 575 int unsend(int);
 576 /* void *sbrk(int); */
 577 void Uerror(char *);
 578 void assert(int, char *, int, int, Trans *);
 579 void c_chandump(int);
 580 void c_globals(void);
 581 void c_locals(int, int);
 582 void checkcycles(void);
 583 void crack(int, int, Trans *, short *);
 584 void d_sfh(const char *, int);
 585 void sfh(const char *, int);
 586 void d_hash(uchar *, int);
 587 void s_hash(uchar *, int);
 588 void r_hash(uchar *, int);
 589 void delq(int);
 590 void do_reach(void);
 591 void pan_exit(int);
 592 void exit(int);
 593 void hinit(void);
 594 void imed(Trans *, int, int, int);
 595 void new_state(void);
 596 void p_restor(int);
 597 void putpeg(int, int);
 598 void putrail(void);
 599 void q_restor(void);
 600 void retrans(int, int, int, short *, uchar *, uchar *);
 601 void settable(void);
 602 void setq_claim(int, int, char *, int, char *);
 603 void sv_restor(void);
 604 void sv_save(void);
 605 void tagtable(int, int, int, short *, uchar *);
 606 void do_dfs(int, int, int, short *, uchar *, uchar *);
 607 void uerror(char *);
 608 void unrecv(int, int, int, int, int);
 609 void usage(FILE *);
 610 void wrap_stats(void);
 611 #if defined(FULLSTACK) && defined(BITSTATE)
 612 int  onstack_now(void);
 613 void onstack_init(void);
 614 void onstack_put(void);
 615 void onstack_zap(void);
 616 #endif
 617 #ifndef XUSAFE
 618 int q_S_check(int, int);
 619 int q_R_check(int, int);
 620 uchar q_claim[MAXQ+1];
 621 char *q_name[MAXQ+1];
 622 char *p_name[MAXPROC+1];
 623 #endif
 624 void qsend(int, int, int);
 625 #define Addproc(x)      addproc(x)
 626 #define LOCAL   1
 627 #define Q_FULL_F        2
 628 #define Q_EMPT_F        3
 629 #define Q_EMPT_T        4
 630 #define Q_FULL_T        5
 631 #define TIMEOUT_F       6
 632 #define GLOBAL  7
 633 #define BAD     8
 634 #define ALPHA_F 9
 635 #define NTRANS  66
 636 #ifdef PEG
 637 long peg[NTRANS];
 638 #endif