trunk/verif/examples/pan.b

   1         switch (t->back) {
   2         default: Uerror("bad return move");
   3         case  0: goto R999; /* nothing to undo */
   4
   5                  /* PROC :init: */
   6
   7         case 3: /* STATE 1 */
   8                 ;
   9                 ((P4 *)this)->i = trpt->bup.oval;
  10                 ;
  11                 goto R999;
  12
  13         case 4: /* STATE 4 */
  14                 ;
  15                 ((P4 *)this)->i = trpt->bup.ovals[1];
  16                 now.commit_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[0];
  17                 ;
  18                 ungrab_ints(trpt->bup.ovals, 2);
  19                 goto R999;
  20
  21         case 5: /* STATE 10 */
  22                 ;
  23                 ((P4 *)this)->i = trpt->bup.ovals[1];
  24         /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0];
  25                 ;
  26                 ;
  27                 ungrab_ints(trpt->bup.ovals, 2);
  28                 goto R999;
  29
  30         case 6: /* STATE 10 */
  31                 ;
  32                 ((P4 *)this)->i = trpt->bup.oval;
  33                 ;
  34                 goto R999;
  35
  36         case 7: /* STATE 13 */
  37                 ;
  38                 ((P4 *)this)->i = trpt->bup.ovals[1];
  39                 now.buffer_use[ Index(((P4 *)this)->i, 4) ] = trpt->bup.ovals[0];
  40                 ;
  41                 ungrab_ints(trpt->bup.ovals, 2);
  42                 goto R999;
  43
  44         case 8: /* STATE 14 */
  45                 ;
  46         /* 0 */ ((P4 *)this)->i = trpt->bup.oval;
  47                 ;
  48                 ;
  49                 goto R999;
  50
  51         case 9: /* STATE 19 */
  52                 ;
  53                 ;
  54                 delproc(0, now._nr_pr-1);
  55                 ;
  56                 goto R999;
  57
  58         case 10: /* STATE 21 */
  59                 ;
  60                 ((P4 *)this)->i = trpt->bup.oval;
  61                 ;
  62                 delproc(0, now._nr_pr-1);
  63                 ;
  64                 goto R999;
  65
  66         case 11: /* STATE 23 */
  67                 ;
  68                 now.refcount = trpt->bup.oval;
  69                 ;
  70                 goto R999;
  71
  72         case 12: /* STATE 25 */
  73                 ;
  74                 ((P4 *)this)->i = trpt->bup.oval;
  75                 ;
  76                 delproc(0, now._nr_pr-1);
  77                 ;
  78                 goto R999;
  79
  80         case 13: /* STATE 31 */
  81                 ;
  82                 ((P4 *)this)->i = trpt->bup.ovals[1];
  83         /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0];
  84                 ;
  85                 ;
  86                 ungrab_ints(trpt->bup.ovals, 2);
  87                 goto R999;
  88
  89         case 14: /* STATE 31 */
  90                 ;
  91                 ((P4 *)this)->i = trpt->bup.oval;
  92                 ;
  93                 goto R999;
  94
  95         case 15: /* STATE 33 */
  96                 ;
  97                 now.refcount = trpt->bup.oval;
  98                 ;
  99                 goto R999;
 100
 101         case 16: /* STATE 35 */
 102                 ;
 103                 ((P4 *)this)->i = trpt->bup.oval;
 104                 ;
 105                 delproc(0, now._nr_pr-1);
 106                 ;
 107                 goto R999;
 108
 109         case 17: /* STATE 36 */
 110                 ;
 111         /* 0 */ ((P4 *)this)->i = trpt->bup.oval;
 112                 ;
 113                 ;
 114                 goto R999;
 115
 116         case 18: /* STATE 44 */
 117                 ;
 118                 ((P4 *)this)->commit_sum = trpt->bup.ovals[1];
 119                 ((P4 *)this)->j = trpt->bup.ovals[0];
 120                 ;
 121                 ungrab_ints(trpt->bup.ovals, 2);
 122                 goto R999;
 123
 124         case 19: /* STATE 47 */
 125                 ;
 126                 ((P4 *)this)->j = trpt->bup.ovals[1];
 127                 ((P4 *)this)->commit_sum = trpt->bup.ovals[0];
 128                 ;
 129                 ungrab_ints(trpt->bup.ovals, 2);
 130                 goto R999;
 131
 132         case 20: /* STATE 48 */
 133                 ;
 134         /* 0 */ ((P4 *)this)->j = trpt->bup.oval;
 135                 ;
 136                 ;
 137                 goto R999;
 138 ;
 139
 140         case 21: /* STATE 53 */
 141                 goto R999;
 142
 143         case 22: /* STATE 56 */
 144                 ;
 145                 p_restor(II);
 146                 ;
 147                 ;
 148                 goto R999;
 149
 150                  /* PROC cleaner */
 151
 152         case 23: /* STATE 2 */
 153                 ;
 154                 now.refcount = trpt->bup.oval;
 155                 ;
 156                 goto R999;
 157
 158         case 24: /* STATE 3 */
 159                 ;
 160                 ;
 161                 delproc(0, now._nr_pr-1);
 162                 ;
 163                 goto R999;
 164
 165         case 25: /* STATE 9 */
 166                 ;
 167                 p_restor(II);
 168                 ;
 169                 ;
 170                 goto R999;
 171
 172                  /* PROC reader */
 173 ;
 174                 ;
 175
 176         case 27: /* STATE 2 */
 177                 ;
 178                 ((P2 *)this)->i = trpt->bup.oval;
 179                 ;
 180                 goto R999;
 181
 182         case 28: /* STATE 6 */
 183                 ;
 184                 ((P2 *)this)->i = trpt->bup.ovals[1];
 185                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 186                 ;
 187                 ungrab_ints(trpt->bup.ovals, 2);
 188                 goto R999;
 189
 190         case 29: /* STATE 7 */
 191                 ;
 192         /* 0 */ ((P2 *)this)->i = trpt->bup.oval;
 193                 ;
 194                 ;
 195                 goto R999;
 196
 197         case 30: /* STATE 16 */
 198                 ;
 199                 ((P2 *)this)->i = trpt->bup.ovals[1];
 200                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 201                 ;
 202                 ungrab_ints(trpt->bup.ovals, 2);
 203                 goto R999;
 204
 205         case 31: /* STATE 17 */
 206                 ;
 207         /* 0 */ ((P2 *)this)->i = trpt->bup.oval;
 208                 ;
 209                 ;
 210                 goto R999;
 211
 212         case 32: /* STATE 22 */
 213                 ;
 214                 now.read_off = trpt->bup.oval;
 215                 ;
 216                 goto R999;
 217 ;
 218                 ;
 219
 220         case 34: /* STATE 29 */
 221                 ;
 222                 p_restor(II);
 223                 ;
 224                 ;
 225                 goto R999;
 226
 227                  /* PROC tracer */
 228
 229         case 35: /* STATE 2 */
 230                 ;
 231                 ((P1 *)this)->new_off = trpt->bup.ovals[1];
 232                 ((P1 *)this)->prev_off = trpt->bup.ovals[0];
 233                 ;
 234                 ungrab_ints(trpt->bup.ovals, 2);
 235                 goto R999;
 236
 237         case 36: /* STATE 4 */
 238                 ;
 239         /* 0 */ ((P1 *)this)->new_off = trpt->bup.oval;
 240                 ;
 241                 ;
 242                 goto R999;
 243 ;
 244
 245         case 37: /* STATE 7 */
 246                 goto R999;
 247
 248         case 38: /* STATE 11 */
 249                 ;
 250         /* 0 */ ((P1 *)this)->prev_off = trpt->bup.oval;
 251                 ;
 252                 ;
 253                 goto R999;
 254
 255         case 39: /* STATE 17 */
 256                 ;
 257                 ((P1 *)this)->i = trpt->bup.ovals[1];
 258                 now.write_off = trpt->bup.ovals[0];
 259                 ;
 260                 ungrab_ints(trpt->bup.ovals, 2);
 261                 goto R999;
 262
 263         case 40: /* STATE 17 */
 264                 ;
 265                 ((P1 *)this)->i = trpt->bup.oval;
 266                 ;
 267                 goto R999;
 268
 269         case 41: /* STATE 21 */
 270                 ;
 271                 ((P1 *)this)->i = trpt->bup.ovals[1];
 272                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 273                 ;
 274                 ungrab_ints(trpt->bup.ovals, 2);
 275                 goto R999;
 276
 277         case 42: /* STATE 22 */
 278                 ;
 279         /* 0 */ ((P1 *)this)->i = trpt->bup.oval;
 280                 ;
 281                 ;
 282                 goto R999;
 283
 284         case 43: /* STATE 28 */
 285                 ;
 286                 ((P1 *)this)->i = trpt->bup.oval;
 287                 ;
 288                 goto R999;
 289
 290         case 44: /* STATE 31 */
 291                 ;
 292                 ((P1 *)this)->i = trpt->bup.ovals[1];
 293                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 294                 ;
 295                 ungrab_ints(trpt->bup.ovals, 2);
 296                 goto R999;
 297
 298         case 45: /* STATE 38 */
 299                 ;
 300                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[2];
 301                 ((P1 *)this)->tmp_commit = trpt->bup.ovals[1];
 302         /* 0 */ ((P1 *)this)->i = trpt->bup.ovals[0];
 303                 ;
 304                 ;
 305                 ungrab_ints(trpt->bup.ovals, 3);
 306                 goto R999;
 307
 308         case 46: /* STATE 38 */
 309                 ;
 310                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[1];
 311                 ((P1 *)this)->tmp_commit = trpt->bup.ovals[0];
 312                 ;
 313                 ungrab_ints(trpt->bup.ovals, 2);
 314                 goto R999;
 315
 316         case 47: /* STATE 40 */
 317                 ;
 318                 deliver = trpt->bup.ovals[2];
 319         /* 1 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[1];
 320         /* 0 */ ((P1 *)this)->prev_off = trpt->bup.ovals[0];
 321                 ;
 322                 ;
 323                 ungrab_ints(trpt->bup.ovals, 3);
 324                 goto R999;
 325 ;
 326
 327         case 48: /* STATE 44 */
 328                 goto R999;
 329 ;
 330
 331         case 49: /* STATE 42 */
 332                 goto R999;
 333
 334         case 50: /* STATE 47 */
 335                 ;
 336                 now.events_lost = trpt->bup.oval;
 337                 ;
 338                 goto R999;
 339
 340         case 51: /* STATE 48 */
 341                 ;
 342                 now.refcount = trpt->bup.oval;
 343                 ;
 344                 goto R999;
 345
 346         case 52: /* STATE 50 */
 347                 ;
 348                 p_restor(II);
 349                 ;
 350                 ;
 351                 goto R999;
 352
 353                  /* PROC switcher */
 354
 355         case 53: /* STATE 3 */
 356                 ;
 357                 ((P0 *)this)->new_off = trpt->bup.ovals[2];
 358                 ((P0 *)this)->size = trpt->bup.ovals[1];
 359                 ((P0 *)this)->prev_off = trpt->bup.ovals[0];
 360                 ;
 361                 ungrab_ints(trpt->bup.ovals, 3);
 362                 goto R999;
 363
 364         case 54: /* STATE 5 */
 365                 ;
 366                 now.refcount = trpt->bup.ovals[2];
 367         /* 1 */ ((P0 *)this)->size = trpt->bup.ovals[1];
 368         /* 0 */ ((P0 *)this)->new_off = trpt->bup.ovals[0];
 369                 ;
 370                 ;
 371                 ungrab_ints(trpt->bup.ovals, 3);
 372                 goto R999;
 373 ;
 374
 375         case 55: /* STATE 8 */
 376                 goto R999;
 377
 378         case 56: /* STATE 12 */
 379                 ;
 380         /* 0 */ ((P0 *)this)->prev_off = trpt->bup.oval;
 381                 ;
 382                 ;
 383                 goto R999;
 384 ;
 385
 386         case 57: /* STATE 17 */
 387                 goto R999;
 388
 389         case 58: /* STATE 15 */
 390                 ;
 391                 now.write_off = trpt->bup.oval;
 392                 ;
 393                 goto R999;
 394
 395         case 59: /* STATE 20 */
 396                 ;
 397                 now.commit_count[ Index(((((P0 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[1];
 398                 ((P0 *)this)->tmp_commit = trpt->bup.ovals[0];
 399                 ;
 400                 ungrab_ints(trpt->bup.ovals, 2);
 401                 goto R999;
 402
 403         case 60: /* STATE 27 */
 404                 ;
 405                 now.refcount = trpt->bup.ovals[3];
 406                 deliver = trpt->bup.ovals[2];
 407         /* 1 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[1];
 408         /* 0 */ ((P0 *)this)->prev_off = trpt->bup.ovals[0];
 409                 ;
 410                 ;
 411                 ungrab_ints(trpt->bup.ovals, 4);
 412                 goto R999;
 413
 414         case 61: /* STATE 27 */
 415                 ;
 416                 now.refcount = trpt->bup.oval;
 417                 ;
 418                 goto R999;
 419
 420         case 62: /* STATE 27 */
 421                 ;
 422                 now.refcount = trpt->bup.oval;
 423                 ;
 424                 goto R999;
 425
 426         case 63: /* STATE 30 */
 427                 ;
 428                 p_restor(II);
 429                 ;
 430                 ;
 431                 goto R999;
 432         }
 433