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