trunk/verif/examples/pan.m

   1 #define rand    pan_rand
   2 #if defined(HAS_CODE) && defined(VERBOSE)
   3         cpu_printf("Pr: %d Tr: %d\n", II, t->forw);
   4 #endif
   5         switch (t->forw) {
   6         default: Uerror("bad forward move");
   7         case 0: /* if without executable clauses */
   8                 continue;
   9         case 1: /* generic 'goto' or 'skip' */
  10                 IfNotBlocked
  11                 _m = 3; goto P999;
  12         case 2: /* generic 'else' */
  13                 IfNotBlocked
  14                 if (trpt->o_pm&1) continue;
  15                 _m = 3; goto P999;
  16
  17                  /* PROC :init: */
  18         case 3: /* STATE 1 - line 225 "buffer.spin" - [i = 0] (0:0:1 - 1) */
  19                 IfNotBlocked
  20                 reached[4][1] = 1;
  21                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
  22                 ((P4 *)this)->i = 0;
  23 #ifdef VAR_RANGES
  24                 logval(":init::i", ((int)((P4 *)this)->i));
  25 #endif
  26                 ;
  27                 _m = 3; goto P999; /* 0 */
  28         case 4: /* STATE 2 - line 227 "buffer.spin" - [((i<2))] (8:0:3 - 1) */
  29                 IfNotBlocked
  30                 reached[4][2] = 1;
  31                 if (!((((int)((P4 *)this)->i)<2)))
  32                         continue;
  33                 /* merge: commit_count[i] = 0(8, 3, 8) */
  34                 reached[4][3] = 1;
  35                 (trpt+1)->bup.ovals = grab_ints(3);
  36                 (trpt+1)->bup.ovals[0] = ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]);
  37                 now.commit_count[ Index(((P4 *)this)->i, 2) ] = 0;
  38 #ifdef VAR_RANGES
  39                 logval("commit_count[:init::i]", ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]));
  40 #endif
  41                 ;
  42                 /* merge: retrieve_count[i] = 0(8, 4, 8) */
  43                 reached[4][4] = 1;
  44                 (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ]);
  45                 now.retrieve_count[ Index(((P4 *)this)->i, 2) ] = 0;
  46 #ifdef VAR_RANGES
  47                 logval("retrieve_count[:init::i]", ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ]));
  48 #endif
  49                 ;
  50                 /* merge: i = (i+1)(8, 5, 8) */
  51                 reached[4][5] = 1;
  52                 (trpt+1)->bup.ovals[2] = ((int)((P4 *)this)->i);
  53                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
  54 #ifdef VAR_RANGES
  55                 logval(":init::i", ((int)((P4 *)this)->i));
  56 #endif
  57                 ;
  58                 /* merge: .(goto)(0, 9, 8) */
  59                 reached[4][9] = 1;
  60                 ;
  61                 _m = 3; goto P999; /* 4 */
  62         case 5: /* STATE 6 - line 231 "buffer.spin" - [((i>=2))] (17:0:2 - 1) */
  63                 IfNotBlocked
  64                 reached[4][6] = 1;
  65                 if (!((((int)((P4 *)this)->i)>=2)))
  66                         continue;
  67                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(2);
  68                 (trpt+1)->bup.ovals[0] = ((P4 *)this)->i;
  69 #ifdef HAS_CODE
  70                 if (!readtrail)
  71 #endif
  72                         ((P4 *)this)->i = 0;
  73                 /* merge: goto :b6(17, 7, 17) */
  74                 reached[4][7] = 1;
  75                 ;
  76                 /* merge: i = 0(17, 11, 17) */
  77                 reached[4][11] = 1;
  78                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
  79                 ((P4 *)this)->i = 0;
  80 #ifdef VAR_RANGES
  81                 logval(":init::i", ((int)((P4 *)this)->i));
  82 #endif
  83                 ;
  84                 /* merge: .(goto)(0, 18, 17) */
  85                 reached[4][18] = 1;
  86                 ;
  87                 _m = 3; goto P999; /* 3 */
  88         case 6: /* STATE 11 - line 233 "buffer.spin" - [i = 0] (0:17:1 - 3) */
  89                 IfNotBlocked
  90                 reached[4][11] = 1;
  91                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
  92                 ((P4 *)this)->i = 0;
  93 #ifdef VAR_RANGES
  94                 logval(":init::i", ((int)((P4 *)this)->i));
  95 #endif
  96                 ;
  97                 /* merge: .(goto)(0, 18, 17) */
  98                 reached[4][18] = 1;
  99                 ;
 100                 _m = 3; goto P999; /* 1 */
 101         case 7: /* STATE 12 - line 235 "buffer.spin" - [((i<4))] (17:0:2 - 1) */
 102                 IfNotBlocked
 103                 reached[4][12] = 1;
 104                 if (!((((int)((P4 *)this)->i)<4)))
 105                         continue;
 106                 /* merge: buffer_use[i] = 0(17, 13, 17) */
 107                 reached[4][13] = 1;
 108                 (trpt+1)->bup.ovals = grab_ints(2);
 109                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ]);
 110                 now.buffer_use[ Index(((P4 *)this)->i, 4) ] = 0;
 111 #ifdef VAR_RANGES
 112                 logval("buffer_use[:init::i]", ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ]));
 113 #endif
 114                 ;
 115                 /* merge: i = (i+1)(17, 14, 17) */
 116                 reached[4][14] = 1;
 117                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
 118                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 119 #ifdef VAR_RANGES
 120                 logval(":init::i", ((int)((P4 *)this)->i));
 121 #endif
 122                 ;
 123                 /* merge: .(goto)(0, 18, 17) */
 124                 reached[4][18] = 1;
 125                 ;
 126                 _m = 3; goto P999; /* 3 */
 127         case 8: /* STATE 15 - line 238 "buffer.spin" - [((i>=4))] (0:0:1 - 1) */
 128                 IfNotBlocked
 129                 reached[4][15] = 1;
 130                 if (!((((int)((P4 *)this)->i)>=4)))
 131                         continue;
 132                 /* dead 1: i */  (trpt+1)->bup.oval = ((P4 *)this)->i;
 133 #ifdef HAS_CODE
 134                 if (!readtrail)
 135 #endif
 136                         ((P4 *)this)->i = 0;
 137                 _m = 3; goto P999; /* 0 */
 138         case 9: /* STATE 20 - line 240 "buffer.spin" - [(run reader())] (0:0:0 - 3) */
 139                 IfNotBlocked
 140                 reached[4][20] = 1;
 141                 if (!(addproc(2)))
 142                         continue;
 143                 _m = 3; goto P999; /* 0 */
 144         case 10: /* STATE 21 - line 241 "buffer.spin" - [(run cleaner())] (29:0:1 - 1) */
 145                 IfNotBlocked
 146                 reached[4][21] = 1;
 147                 if (!(addproc(3)))
 148                         continue;
 149                 /* merge: i = 0(0, 22, 29) */
 150                 reached[4][22] = 1;
 151                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 152                 ((P4 *)this)->i = 0;
 153 #ifdef VAR_RANGES
 154                 logval(":init::i", ((int)((P4 *)this)->i));
 155 #endif
 156                 ;
 157                 /* merge: .(goto)(0, 30, 29) */
 158                 reached[4][30] = 1;
 159                 ;
 160                 _m = 3; goto P999; /* 2 */
 161         case 11: /* STATE 23 - line 244 "buffer.spin" - [((i<4))] (25:0:1 - 1) */
 162                 IfNotBlocked
 163                 reached[4][23] = 1;
 164                 if (!((((int)((P4 *)this)->i)<4)))
 165                         continue;
 166                 /* merge: refcount = (refcount+1)(0, 24, 25) */
 167                 reached[4][24] = 1;
 168                 (trpt+1)->bup.oval = ((int)now.refcount);
 169                 now.refcount = (((int)now.refcount)+1);
 170 #ifdef VAR_RANGES
 171                 logval("refcount", ((int)now.refcount));
 172 #endif
 173                 ;
 174                 _m = 3; goto P999; /* 1 */
 175         case 12: /* STATE 25 - line 246 "buffer.spin" - [(run tracer())] (29:0:1 - 1) */
 176                 IfNotBlocked
 177                 reached[4][25] = 1;
 178                 if (!(addproc(1)))
 179                         continue;
 180                 /* merge: i = (i+1)(0, 26, 29) */
 181                 reached[4][26] = 1;
 182                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 183                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 184 #ifdef VAR_RANGES
 185                 logval(":init::i", ((int)((P4 *)this)->i));
 186 #endif
 187                 ;
 188                 /* merge: .(goto)(0, 30, 29) */
 189                 reached[4][30] = 1;
 190                 ;
 191                 _m = 3; goto P999; /* 2 */
 192         case 13: /* STATE 27 - line 248 "buffer.spin" - [((i>=4))] (39:0:2 - 1) */
 193                 IfNotBlocked
 194                 reached[4][27] = 1;
 195                 if (!((((int)((P4 *)this)->i)>=4)))
 196                         continue;
 197                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(2);
 198                 (trpt+1)->bup.ovals[0] = ((P4 *)this)->i;
 199 #ifdef HAS_CODE
 200                 if (!readtrail)
 201 #endif
 202                         ((P4 *)this)->i = 0;
 203                 /* merge: goto :b8(39, 28, 39) */
 204                 reached[4][28] = 1;
 205                 ;
 206                 /* merge: i = 0(39, 32, 39) */
 207                 reached[4][32] = 1;
 208                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
 209                 ((P4 *)this)->i = 0;
 210 #ifdef VAR_RANGES
 211                 logval(":init::i", ((int)((P4 *)this)->i));
 212 #endif
 213                 ;
 214                 /* merge: .(goto)(0, 40, 39) */
 215                 reached[4][40] = 1;
 216                 ;
 217                 _m = 3; goto P999; /* 3 */
 218         case 14: /* STATE 32 - line 250 "buffer.spin" - [i = 0] (0:39:1 - 3) */
 219                 IfNotBlocked
 220                 reached[4][32] = 1;
 221                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 222                 ((P4 *)this)->i = 0;
 223 #ifdef VAR_RANGES
 224                 logval(":init::i", ((int)((P4 *)this)->i));
 225 #endif
 226                 ;
 227                 /* merge: .(goto)(0, 40, 39) */
 228                 reached[4][40] = 1;
 229                 ;
 230                 _m = 3; goto P999; /* 1 */
 231         case 15: /* STATE 33 - line 252 "buffer.spin" - [((i<1))] (35:0:1 - 1) */
 232                 IfNotBlocked
 233                 reached[4][33] = 1;
 234                 if (!((((int)((P4 *)this)->i)<1)))
 235                         continue;
 236                 /* merge: refcount = (refcount+1)(0, 34, 35) */
 237                 reached[4][34] = 1;
 238                 (trpt+1)->bup.oval = ((int)now.refcount);
 239                 now.refcount = (((int)now.refcount)+1);
 240 #ifdef VAR_RANGES
 241                 logval("refcount", ((int)now.refcount));
 242 #endif
 243                 ;
 244                 _m = 3; goto P999; /* 1 */
 245         case 16: /* STATE 35 - line 254 "buffer.spin" - [(run switcher())] (39:0:1 - 1) */
 246                 IfNotBlocked
 247                 reached[4][35] = 1;
 248                 if (!(addproc(0)))
 249                         continue;
 250                 /* merge: i = (i+1)(0, 36, 39) */
 251                 reached[4][36] = 1;
 252                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 253                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 254 #ifdef VAR_RANGES
 255                 logval(":init::i", ((int)((P4 *)this)->i));
 256 #endif
 257                 ;
 258                 /* merge: .(goto)(0, 40, 39) */
 259                 reached[4][40] = 1;
 260                 ;
 261                 _m = 3; goto P999; /* 2 */
 262         case 17: /* STATE 37 - line 256 "buffer.spin" - [((i>=1))] (41:0:1 - 1) */
 263                 IfNotBlocked
 264                 reached[4][37] = 1;
 265                 if (!((((int)((P4 *)this)->i)>=1)))
 266                         continue;
 267                 /* dead 1: i */  (trpt+1)->bup.oval = ((P4 *)this)->i;
 268 #ifdef HAS_CODE
 269                 if (!readtrail)
 270 #endif
 271                         ((P4 *)this)->i = 0;
 272                 /* merge: goto :b9(0, 38, 41) */
 273                 reached[4][38] = 1;
 274                 ;
 275                 _m = 3; goto P999; /* 1 */
 276         case 18: /* STATE 43 - line 262 "buffer.spin" - [assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))] (0:52:2 - 1) */
 277                 IfNotBlocked
 278                 reached[4][43] = 1;
 279                 assert((((((int)now.write_off)-((int)now.read_off))>=0)&&((((int)now.write_off)-((int)now.read_off))<(255/2))), "(((write_off-read_off)>=0)&&((write_off-read_off)<(255/2)))", II, tt, t);
 280                 /* merge: j = 0(52, 44, 52) */
 281                 reached[4][44] = 1;
 282                 (trpt+1)->bup.ovals = grab_ints(2);
 283                 (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->j);
 284                 ((P4 *)this)->j = 0;
 285 #ifdef VAR_RANGES
 286                 logval(":init::j", ((int)((P4 *)this)->j));
 287 #endif
 288                 ;
 289                 /* merge: commit_sum = 0(52, 45, 52) */
 290                 reached[4][45] = 1;
 291                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->commit_sum);
 292                 ((P4 *)this)->commit_sum = 0;
 293 #ifdef VAR_RANGES
 294                 logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum));
 295 #endif
 296                 ;
 297                 /* merge: .(goto)(0, 53, 52) */
 298                 reached[4][53] = 1;
 299                 ;
 300                 _m = 3; goto P999; /* 3 */
 301         case 19: /* STATE 46 - line 266 "buffer.spin" - [((j<2))] (52:0:2 - 1) */
 302                 IfNotBlocked
 303                 reached[4][46] = 1;
 304                 if (!((((int)((P4 *)this)->j)<2)))
 305                         continue;
 306                 /* merge: commit_sum = (commit_sum+commit_count[j])(52, 47, 52) */
 307                 reached[4][47] = 1;
 308                 (trpt+1)->bup.ovals = grab_ints(2);
 309                 (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->commit_sum);
 310                 ((P4 *)this)->commit_sum = (((int)((P4 *)this)->commit_sum)+((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ]));
 311 #ifdef VAR_RANGES
 312                 logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum));
 313 #endif
 314                 ;
 315                 /* merge: assert((((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2))))(52, 48, 52) */
 316                 reached[4][48] = 1;
 317                 assert((((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))>=0)&&((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))<(255/2))), "(((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2)))", II, tt, t);
 318                 /* merge: j = (j+1)(52, 49, 52) */
 319                 reached[4][49] = 1;
 320                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->j);
 321                 ((P4 *)this)->j = (((int)((P4 *)this)->j)+1);
 322 #ifdef VAR_RANGES
 323                 logval(":init::j", ((int)((P4 *)this)->j));
 324 #endif
 325                 ;
 326                 /* merge: .(goto)(0, 53, 52) */
 327                 reached[4][53] = 1;
 328                 ;
 329                 _m = 3; goto P999; /* 4 */
 330         case 20: /* STATE 50 - line 273 "buffer.spin" - [((j>=2))] (58:0:1 - 1) */
 331                 IfNotBlocked
 332                 reached[4][50] = 1;
 333                 if (!((((int)((P4 *)this)->j)>=2)))
 334                         continue;
 335                 /* dead 1: j */  (trpt+1)->bup.oval = ((P4 *)this)->j;
 336 #ifdef HAS_CODE
 337                 if (!readtrail)
 338 #endif
 339                         ((P4 *)this)->j = 0;
 340                 /* merge: goto :b10(58, 51, 58) */
 341                 reached[4][51] = 1;
 342                 ;
 343                 /* merge: assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))(58, 55, 58) */
 344                 reached[4][55] = 1;
 345                 assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t);
 346                 /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */
 347                 reached[4][56] = 1;
 348                 assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t);
 349                 _m = 3; goto P999; /* 3 */
 350         case 21: /* STATE 55 - line 278 "buffer.spin" - [assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))] (0:58:0 - 3) */
 351                 IfNotBlocked
 352                 reached[4][55] = 1;
 353                 assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t);
 354                 /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */
 355                 reached[4][56] = 1;
 356                 assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t);
 357                 _m = 3; goto P999; /* 1 */
 358         case 22: /* STATE 58 - line 284 "buffer.spin" - [-end-] (0:0:0 - 1) */
 359                 IfNotBlocked
 360                 reached[4][58] = 1;
 361                 if (!delproc(1, II)) continue;
 362                 _m = 3; goto P999; /* 0 */
 363
 364                  /* PROC cleaner */
 365         case 23: /* STATE 1 - line 210 "buffer.spin" - [((refcount==0))] (3:0:1 - 1) */
 366                 IfNotBlocked
 367                 reached[3][1] = 1;
 368                 if (!((((int)now.refcount)==0)))
 369                         continue;
 370                 /* merge: refcount = (refcount+1)(0, 2, 3) */
 371                 reached[3][2] = 1;
 372                 (trpt+1)->bup.oval = ((int)now.refcount);
 373                 now.refcount = (((int)now.refcount)+1);
 374 #ifdef VAR_RANGES
 375                 logval("refcount", ((int)now.refcount));
 376 #endif
 377                 ;
 378                 _m = 3; goto P999; /* 1 */
 379         case 24: /* STATE 3 - line 212 "buffer.spin" - [(run switcher())] (7:0:0 - 1) */
 380                 IfNotBlocked
 381                 reached[3][3] = 1;
 382                 if (!(addproc(0)))
 383                         continue;
 384                 /* merge: goto :b5(0, 4, 7) */
 385                 reached[3][4] = 1;
 386                 ;
 387                 _m = 3; goto P999; /* 1 */
 388         case 25: /* STATE 9 - line 216 "buffer.spin" - [-end-] (0:0:0 - 1) */
 389                 IfNotBlocked
 390                 reached[3][9] = 1;
 391                 if (!delproc(1, II)) continue;
 392                 _m = 3; goto P999; /* 0 */
 393
 394                  /* PROC reader */
 395         case 26: /* STATE 1 - line 169 "buffer.spin" - [((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&((commit_count[((read_off%4)/(4/2))]-retrieve_count[((read_off%4)/(4/2))])==(4/2))))] (0:0:0 - 1) */
 396                 IfNotBlocked
 397                 reached[2][1] = 1;
 398                 if (!((((((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))>0)&&(((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))<(255/2)))&&((((int)now.commit_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])-((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]))==(4/2)))))
 399                         continue;
 400                 _m = 3; goto P999; /* 0 */
 401         case 27: /* STATE 2 - line 171 "buffer.spin" - [i = 0] (0:0:1 - 1) */
 402                 IfNotBlocked
 403                 reached[2][2] = 1;
 404                 (trpt+1)->bup.oval = ((int)((P2 *)this)->i);
 405                 ((P2 *)this)->i = 0;
 406 #ifdef VAR_RANGES
 407                 logval("reader:i", ((int)((P2 *)this)->i));
 408 #endif
 409                 ;
 410                 _m = 3; goto P999; /* 0 */
 411         case 28: /* STATE 3 - line 173 "buffer.spin" - [((i<(4/2)))] (9:0:2 - 1) */
 412                 IfNotBlocked
 413                 reached[2][3] = 1;
 414                 if (!((((int)((P2 *)this)->i)<(4/2))))
 415                         continue;
 416                 /* merge: assert((buffer_use[((read_off+i)%4)]==0))(9, 4, 9) */
 417                 reached[2][4] = 1;
 418                 assert((((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%4), 4) ])==0), "(buffer_use[((read_off+i)%4)]==0)", II, tt, t);
 419                 /* merge: buffer_use[((read_off+i)%4)] = 1(9, 5, 9) */
 420                 reached[2][5] = 1;
 421                 (trpt+1)->bup.ovals = grab_ints(2);
 422                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%4), 4) ]);
 423                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = 1;
 424 #ifdef VAR_RANGES
 425                 logval("buffer_use[((read_off+reader:i)%4)]", ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%4), 4) ]));
 426 #endif
 427                 ;
 428                 /* merge: i = (i+1)(9, 6, 9) */
 429                 reached[2][6] = 1;
 430                 (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->i);
 431                 ((P2 *)this)->i = (((int)((P2 *)this)->i)+1);
 432 #ifdef VAR_RANGES
 433                 logval("reader:i", ((int)((P2 *)this)->i));
 434 #endif
 435                 ;
 436                 /* merge: .(goto)(0, 10, 9) */
 437                 reached[2][10] = 1;
 438                 ;
 439                 _m = 3; goto P999; /* 4 */
 440         case 29: /* STATE 7 - line 177 "buffer.spin" - [((i>=(4/2)))] (11:0:1 - 1) */
 441                 IfNotBlocked
 442                 reached[2][7] = 1;
 443                 if (!((((int)((P2 *)this)->i)>=(4/2))))
 444                         continue;
 445                 /* dead 1: i */  (trpt+1)->bup.oval = ((P2 *)this)->i;
 446 #ifdef HAS_CODE
 447                 if (!readtrail)
 448 #endif
 449                         ((P2 *)this)->i = 0;
 450                 /* merge: goto :b3(0, 8, 11) */
 451                 reached[2][8] = 1;
 452                 ;
 453                 _m = 3; goto P999; /* 1 */
 454 /* STATE 13 - line 187 "buffer.spin" - [i = 0] (0:0 - 1) same as 27 (0:0 - 1) */
 455         case 30: /* STATE 14 - line 189 "buffer.spin" - [((i<(4/2)))] (19:0:2 - 1) */
 456                 IfNotBlocked
 457                 reached[2][14] = 1;
 458                 if (!((((int)((P2 *)this)->i)<(4/2))))
 459                         continue;
 460                 /* merge: buffer_use[((read_off+i)%4)] = 0(19, 15, 19) */
 461                 reached[2][15] = 1;
 462                 (trpt+1)->bup.ovals = grab_ints(2);
 463                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%4), 4) ]);
 464                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = 0;
 465 #ifdef VAR_RANGES
 466                 logval("buffer_use[((read_off+reader:i)%4)]", ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%4), 4) ]));
 467 #endif
 468                 ;
 469                 /* merge: i = (i+1)(19, 16, 19) */
 470                 reached[2][16] = 1;
 471                 (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->i);
 472                 ((P2 *)this)->i = (((int)((P2 *)this)->i)+1);
 473 #ifdef VAR_RANGES
 474                 logval("reader:i", ((int)((P2 *)this)->i));
 475 #endif
 476                 ;
 477                 /* merge: .(goto)(0, 20, 19) */
 478                 reached[2][20] = 1;
 479                 ;
 480                 _m = 3; goto P999; /* 3 */
 481         case 31: /* STATE 17 - line 192 "buffer.spin" - [((i>=(4/2)))] (28:0:4 - 1) */
 482                 IfNotBlocked
 483                 reached[2][17] = 1;
 484                 if (!((((int)((P2 *)this)->i)>=(4/2))))
 485                         continue;
 486                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(4);
 487                 (trpt+1)->bup.ovals[0] = ((P2 *)this)->i;
 488 #ifdef HAS_CODE
 489                 if (!readtrail)
 490 #endif
 491                         ((P2 *)this)->i = 0;
 492                 /* merge: goto :b4(28, 18, 28) */
 493                 reached[2][18] = 1;
 494                 ;
 495                 /* merge: tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))(28, 22, 28) */
 496                 reached[2][22] = 1;
 497                 (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->tmp_retrieve);
 498                 ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2));
 499 #ifdef VAR_RANGES
 500                 logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve));
 501 #endif
 502                 ;
 503                 /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */
 504                 reached[2][23] = 1;
 505                 (trpt+1)->bup.ovals[2] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]);
 506                 now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve);
 507 #ifdef VAR_RANGES
 508                 logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]));
 509 #endif
 510                 ;
 511                 /* merge: read_off = (read_off+(4/2))(28, 24, 28) */
 512                 reached[2][24] = 1;
 513                 (trpt+1)->bup.ovals[3] = ((int)now.read_off);
 514                 now.read_off = (((int)now.read_off)+(4/2));
 515 #ifdef VAR_RANGES
 516                 logval("read_off", ((int)now.read_off));
 517 #endif
 518                 ;
 519                 /* merge: .(goto)(0, 29, 28) */
 520                 reached[2][29] = 1;
 521                 ;
 522                 _m = 3; goto P999; /* 5 */
 523         case 32: /* STATE 22 - line 194 "buffer.spin" - [tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))] (0:28:3 - 3) */
 524                 IfNotBlocked
 525                 reached[2][22] = 1;
 526                 (trpt+1)->bup.ovals = grab_ints(3);
 527                 (trpt+1)->bup.ovals[0] = ((int)((P2 *)this)->tmp_retrieve);
 528                 ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2));
 529 #ifdef VAR_RANGES
 530                 logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve));
 531 #endif
 532                 ;
 533                 /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */
 534                 reached[2][23] = 1;
 535                 (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]);
 536                 now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve);
 537 #ifdef VAR_RANGES
 538                 logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]));
 539 #endif
 540                 ;
 541                 /* merge: read_off = (read_off+(4/2))(28, 24, 28) */
 542                 reached[2][24] = 1;
 543                 (trpt+1)->bup.ovals[2] = ((int)now.read_off);
 544                 now.read_off = (((int)now.read_off)+(4/2));
 545 #ifdef VAR_RANGES
 546                 logval("read_off", ((int)now.read_off));
 547 #endif
 548                 ;
 549                 /* merge: .(goto)(0, 29, 28) */
 550                 reached[2][29] = 1;
 551                 ;
 552                 _m = 3; goto P999; /* 3 */
 553         case 33: /* STATE 26 - line 199 "buffer.spin" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */
 554                 IfNotBlocked
 555                 reached[2][26] = 1;
 556                 if (!((((int)now.read_off)>=(4-((int)now.events_lost)))))
 557                         continue;
 558                 _m = 3; goto P999; /* 0 */
 559         case 34: /* STATE 31 - line 201 "buffer.spin" - [-end-] (0:0:0 - 3) */
 560                 IfNotBlocked
 561                 reached[2][31] = 1;
 562                 if (!delproc(1, II)) continue;
 563                 _m = 3; goto P999; /* 0 */
 564
 565                  /* PROC tracer */
 566         case 35: /* STATE 1 - line 99 "buffer.spin" - [prev_off = write_off] (0:10:2 - 1) */
 567                 IfNotBlocked
 568                 reached[1][1] = 1;
 569                 (trpt+1)->bup.ovals = grab_ints(2);
 570                 (trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->prev_off);
 571                 ((P1 *)this)->prev_off = ((int)now.write_off);
 572 #ifdef VAR_RANGES
 573                 logval("tracer:prev_off", ((int)((P1 *)this)->prev_off));
 574 #endif
 575                 ;
 576                 /* merge: new_off = (prev_off+size)(10, 2, 10) */
 577                 reached[1][2] = 1;
 578                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->new_off);
 579                 ((P1 *)this)->new_off = (((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->size));
 580 #ifdef VAR_RANGES
 581                 logval("tracer:new_off", ((int)((P1 *)this)->new_off));
 582 #endif
 583                 ;
 584                 _m = 3; goto P999; /* 1 */
 585         case 36: /* STATE 4 - line 104 "buffer.spin" - [((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */
 586                 IfNotBlocked
 587                 reached[1][4] = 1;
 588                 if (!((((((int)((P1 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P1 *)this)->new_off)-((int)now.read_off))<(255/2)))))
 589                         continue;
 590                 /* dead 1: new_off */  (trpt+1)->bup.oval = ((P1 *)this)->new_off;
 591 #ifdef HAS_CODE
 592                 if (!readtrail)
 593 #endif
 594                         ((P1 *)this)->new_off = 0;
 595                 _m = 3; goto P999; /* 0 */
 596         case 37: /* STATE 7 - line 106 "buffer.spin" - [(1)] (27:0:0 - 1) */
 597                 IfNotBlocked
 598                 reached[1][7] = 1;
 599                 if (!(1))
 600                         continue;
 601                 /* merge: .(goto)(0, 9, 27) */
 602                 reached[1][9] = 1;
 603                 ;
 604                 _m = 3; goto P999; /* 1 */
 605         case 38: /* STATE 11 - line 111 "buffer.spin" - [((prev_off!=write_off))] (3:0:1 - 1) */
 606                 IfNotBlocked
 607                 reached[1][11] = 1;
 608                 if (!((((int)((P1 *)this)->prev_off)!=((int)now.write_off))))
 609                         continue;
 610                 /* dead 1: prev_off */  (trpt+1)->bup.oval = ((P1 *)this)->prev_off;
 611 #ifdef HAS_CODE
 612                 if (!readtrail)
 613 #endif
 614                         ((P1 *)this)->prev_off = 0;
 615                 /* merge: goto cmpxchg_loop(0, 12, 3) */
 616                 reached[1][12] = 1;
 617                 ;
 618                 _m = 3; goto P999; /* 1 */
 619         case 39: /* STATE 14 - line 112 "buffer.spin" - [write_off = new_off] (0:24:2 - 1) */
 620                 IfNotBlocked
 621                 reached[1][14] = 1;
 622                 (trpt+1)->bup.ovals = grab_ints(2);
 623                 (trpt+1)->bup.ovals[0] = ((int)now.write_off);
 624                 now.write_off = ((int)((P1 *)this)->new_off);
 625 #ifdef VAR_RANGES
 626                 logval("write_off", ((int)now.write_off));
 627 #endif
 628                 ;
 629                 /* merge: .(goto)(24, 16, 24) */
 630                 reached[1][16] = 1;
 631                 ;
 632                 /* merge: i = 0(24, 17, 24) */
 633                 reached[1][17] = 1;
 634                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 635                 ((P1 *)this)->i = 0;
 636 #ifdef VAR_RANGES
 637                 logval("tracer:i", ((int)((P1 *)this)->i));
 638 #endif
 639                 ;
 640                 /* merge: .(goto)(0, 25, 24) */
 641                 reached[1][25] = 1;
 642                 ;
 643                 _m = 3; goto P999; /* 3 */
 644         case 40: /* STATE 17 - line 114 "buffer.spin" - [i = 0] (0:24:1 - 2) */
 645                 IfNotBlocked
 646                 reached[1][17] = 1;
 647                 (trpt+1)->bup.oval = ((int)((P1 *)this)->i);
 648                 ((P1 *)this)->i = 0;
 649 #ifdef VAR_RANGES
 650                 logval("tracer:i", ((int)((P1 *)this)->i));
 651 #endif
 652                 ;
 653                 /* merge: .(goto)(0, 25, 24) */
 654                 reached[1][25] = 1;
 655                 ;
 656                 _m = 3; goto P999; /* 1 */
 657         case 41: /* STATE 18 - line 116 "buffer.spin" - [((i<size))] (24:0:2 - 1) */
 658                 IfNotBlocked
 659                 reached[1][18] = 1;
 660                 if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
 661                         continue;
 662                 /* merge: assert((buffer_use[((prev_off+i)%4)]==0))(24, 19, 24) */
 663                 reached[1][19] = 1;
 664                 assert((((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%4), 4) ])==0), "(buffer_use[((prev_off+i)%4)]==0)", II, tt, t);
 665                 /* merge: buffer_use[((prev_off+i)%4)] = 1(24, 20, 24) */
 666                 reached[1][20] = 1;
 667                 (trpt+1)->bup.ovals = grab_ints(2);
 668                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%4), 4) ]);
 669                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = 1;
 670 #ifdef VAR_RANGES
 671                 logval("buffer_use[((tracer:prev_off+tracer:i)%4)]", ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%4), 4) ]));
 672 #endif
 673                 ;
 674                 /* merge: i = (i+1)(24, 21, 24) */
 675                 reached[1][21] = 1;
 676                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 677                 ((P1 *)this)->i = (((int)((P1 *)this)->i)+1);
 678 #ifdef VAR_RANGES
 679                 logval("tracer:i", ((int)((P1 *)this)->i));
 680 #endif
 681                 ;
 682                 /* merge: .(goto)(0, 25, 24) */
 683                 reached[1][25] = 1;
 684                 ;
 685                 _m = 3; goto P999; /* 4 */
 686         case 42: /* STATE 22 - line 120 "buffer.spin" - [((i>=size))] (26:0:1 - 1) */
 687                 IfNotBlocked
 688                 reached[1][22] = 1;
 689                 if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size))))
 690                         continue;
 691                 /* dead 1: i */  (trpt+1)->bup.oval = ((P1 *)this)->i;
 692 #ifdef HAS_CODE
 693                 if (!readtrail)
 694 #endif
 695                         ((P1 *)this)->i = 0;
 696                 /* merge: goto :b0(0, 23, 26) */
 697                 reached[1][23] = 1;
 698                 ;
 699                 _m = 3; goto P999; /* 1 */
 700         case 43: /* STATE 28 - line 127 "buffer.spin" - [i = 0] (0:0:1 - 1) */
 701                 IfNotBlocked
 702                 reached[1][28] = 1;
 703                 (trpt+1)->bup.oval = ((int)((P1 *)this)->i);
 704                 ((P1 *)this)->i = 0;
 705 #ifdef VAR_RANGES
 706                 logval("tracer:i", ((int)((P1 *)this)->i));
 707 #endif
 708                 ;
 709                 _m = 3; goto P999; /* 0 */
 710         case 44: /* STATE 29 - line 129 "buffer.spin" - [((i<size))] (34:0:2 - 1) */
 711                 IfNotBlocked
 712                 reached[1][29] = 1;
 713                 if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
 714                         continue;
 715                 /* merge: buffer_use[((prev_off+i)%4)] = 0(34, 30, 34) */
 716                 reached[1][30] = 1;
 717                 (trpt+1)->bup.ovals = grab_ints(2);
 718                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%4), 4) ]);
 719                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = 0;
 720 #ifdef VAR_RANGES
 721                 logval("buffer_use[((tracer:prev_off+tracer:i)%4)]", ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%4), 4) ]));
 722 #endif
 723                 ;
 724                 /* merge: i = (i+1)(34, 31, 34) */
 725                 reached[1][31] = 1;
 726                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 727                 ((P1 *)this)->i = (((int)((P1 *)this)->i)+1);
 728 #ifdef VAR_RANGES
 729                 logval("tracer:i", ((int)((P1 *)this)->i));
 730 #endif
 731                 ;
 732                 /* merge: .(goto)(0, 35, 34) */
 733                 reached[1][35] = 1;
 734                 ;
 735                 _m = 3; goto P999; /* 3 */
 736         case 45: /* STATE 32 - line 132 "buffer.spin" - [((i>=size))] (43:0:3 - 1) */
 737                 IfNotBlocked
 738                 reached[1][32] = 1;
 739                 if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size))))
 740                         continue;
 741                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(3);
 742                 (trpt+1)->bup.ovals[0] = ((P1 *)this)->i;
 743 #ifdef HAS_CODE
 744                 if (!readtrail)
 745 #endif
 746                         ((P1 *)this)->i = 0;
 747                 /* merge: goto :b1(43, 33, 43) */
 748                 reached[1][33] = 1;
 749                 ;
 750                 /* merge: tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)(43, 37, 43) */
 751                 reached[1][37] = 1;
 752                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->tmp_commit);
 753                 ((P1 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ])+((int)((P1 *)this)->size));
 754 #ifdef VAR_RANGES
 755                 logval("tracer:tmp_commit", ((int)((P1 *)this)->tmp_commit));
 756 #endif
 757                 ;
 758                 /* merge: commit_count[((prev_off%4)/(4/2))] = tmp_commit(43, 38, 43) */
 759                 reached[1][38] = 1;
 760                 (trpt+1)->bup.ovals[2] = ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ]);
 761                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = ((int)((P1 *)this)->tmp_commit);
 762 #ifdef VAR_RANGES
 763                 logval("commit_count[((tracer:prev_off%4)/(4/2))]", ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ]));
 764 #endif
 765                 ;
 766                 _m = 3; goto P999; /* 3 */
 767         case 46: /* STATE 37 - line 134 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:43:2 - 3) */
 768                 IfNotBlocked
 769                 reached[1][37] = 1;
 770                 (trpt+1)->bup.ovals = grab_ints(2);
 771                 (trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->tmp_commit);
 772                 ((P1 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ])+((int)((P1 *)this)->size));
 773 #ifdef VAR_RANGES
 774                 logval("tracer:tmp_commit", ((int)((P1 *)this)->tmp_commit));
 775 #endif
 776                 ;
 777                 /* merge: commit_count[((prev_off%4)/(4/2))] = tmp_commit(43, 38, 43) */
 778                 reached[1][38] = 1;
 779                 (trpt+1)->bup.ovals[1] = ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ]);
 780                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = ((int)((P1 *)this)->tmp_commit);
 781 #ifdef VAR_RANGES
 782                 logval("commit_count[((tracer:prev_off%4)/(4/2))]", ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%4)/(4/2)), 2) ]));
 783 #endif
 784                 ;
 785                 _m = 3; goto P999; /* 1 */
 786         case 47: /* STATE 39 - line 137 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (49:0:2 - 1) */
 787                 IfNotBlocked
 788                 reached[1][39] = 1;
 789                 if (!(((((int)((P1 *)this)->tmp_commit)%(4/2))==0)))
 790                         continue;
 791                 /* dead 1: tmp_commit */  (trpt+1)->bup.ovals = grab_ints(2);
 792                 (trpt+1)->bup.ovals[0] = ((P1 *)this)->tmp_commit;
 793 #ifdef HAS_CODE
 794                 if (!readtrail)
 795 #endif
 796                         ((P1 *)this)->tmp_commit = 0;
 797                 /* merge: deliver = 1(49, 40, 49) */
 798                 reached[1][40] = 1;
 799                 (trpt+1)->bup.ovals[1] = ((int)deliver);
 800                 deliver = 1;
 801 #ifdef VAR_RANGES
 802                 logval("deliver", ((int)deliver));
 803 #endif
 804                 ;
 805                 /* merge: .(goto)(49, 44, 49) */
 806                 reached[1][44] = 1;
 807                 ;
 808                 _m = 3; goto P999; /* 2 */
 809         case 48: /* STATE 44 - line 140 "buffer.spin" - [.(goto)] (0:49:0 - 2) */
 810                 IfNotBlocked
 811                 reached[1][44] = 1;
 812                 ;
 813                 _m = 3; goto P999; /* 0 */
 814         case 49: /* STATE 42 - line 138 "buffer.spin" - [(1)] (49:0:0 - 1) */
 815                 IfNotBlocked
 816                 reached[1][42] = 1;
 817                 if (!(1))
 818                         continue;
 819                 /* merge: .(goto)(49, 44, 49) */
 820                 reached[1][44] = 1;
 821                 ;
 822                 _m = 3; goto P999; /* 1 */
 823         case 50: /* STATE 47 - line 144 "buffer.spin" - [events_lost = (events_lost+1)] (0:0:1 - 2) */
 824                 IfNotBlocked
 825                 reached[1][47] = 1;
 826                 (trpt+1)->bup.oval = ((int)now.events_lost);
 827                 now.events_lost = (((int)now.events_lost)+1);
 828 #ifdef VAR_RANGES
 829                 logval("events_lost", ((int)now.events_lost));
 830 #endif
 831                 ;
 832                 _m = 3; goto P999; /* 0 */
 833         case 51: /* STATE 48 - line 146 "buffer.spin" - [refcount = (refcount-1)] (0:0:1 - 2) */
 834                 IfNotBlocked
 835                 reached[1][48] = 1;
 836                 (trpt+1)->bup.oval = ((int)now.refcount);
 837                 now.refcount = (((int)now.refcount)-1);
 838 #ifdef VAR_RANGES
 839                 logval("refcount", ((int)now.refcount));
 840 #endif
 841                 ;
 842                 _m = 3; goto P999; /* 0 */
 843         case 52: /* STATE 50 - line 148 "buffer.spin" - [-end-] (0:0:0 - 1) */
 844                 IfNotBlocked
 845                 reached[1][50] = 1;
 846                 if (!delproc(1, II)) continue;
 847                 _m = 3; goto P999; /* 0 */
 848
 849                  /* PROC switcher */
 850         case 53: /* STATE 1 - line 56 "buffer.spin" - [prev_off = write_off] (0:9:3 - 1) */
 851                 IfNotBlocked
 852                 reached[0][1] = 1;
 853                 (trpt+1)->bup.ovals = grab_ints(3);
 854                 (trpt+1)->bup.ovals[0] = ((int)((P0 *)this)->prev_off);
 855                 ((P0 *)this)->prev_off = ((int)now.write_off);
 856 #ifdef VAR_RANGES
 857                 logval("switcher:prev_off", ((int)((P0 *)this)->prev_off));
 858 #endif
 859                 ;
 860                 /* merge: size = ((4/2)-(prev_off%(4/2)))(9, 2, 9) */
 861                 reached[0][2] = 1;
 862                 (trpt+1)->bup.ovals[1] = ((int)((P0 *)this)->size);
 863                 ((P0 *)this)->size = ((4/2)-(((int)((P0 *)this)->prev_off)%(4/2)));
 864 #ifdef VAR_RANGES
 865                 logval("switcher:size", ((int)((P0 *)this)->size));
 866 #endif
 867                 ;
 868                 /* merge: new_off = (prev_off+size)(9, 3, 9) */
 869                 reached[0][3] = 1;
 870                 (trpt+1)->bup.ovals[2] = ((int)((P0 *)this)->new_off);
 871                 ((P0 *)this)->new_off = (((int)((P0 *)this)->prev_off)+((int)((P0 *)this)->size));
 872 #ifdef VAR_RANGES
 873                 logval("switcher:new_off", ((int)((P0 *)this)->new_off));
 874 #endif
 875                 ;
 876                 _m = 3; goto P999; /* 2 */
 877         case 54: /* STATE 4 - line 61 "buffer.spin" - [(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))] (29:0:3 - 1) */
 878                 IfNotBlocked
 879                 reached[0][4] = 1;
 880                 if (!(((((((int)((P0 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P0 *)this)->new_off)-((int)now.read_off))<(255/2)))||(((int)((P0 *)this)->size)==(4/2)))))
 881                         continue;
 882                 /* dead 1: new_off */  (trpt+1)->bup.ovals = grab_ints(3);
 883                 (trpt+1)->bup.ovals[0] = ((P0 *)this)->new_off;
 884 #ifdef HAS_CODE
 885                 if (!readtrail)
 886 #endif
 887                         ((P0 *)this)->new_off = 0;
 888                 /* dead 1: size */  (trpt+1)->bup.ovals[1] = ((P0 *)this)->size;
 889 #ifdef HAS_CODE
 890                 if (!readtrail)
 891 #endif
 892                         ((P0 *)this)->size = 0;
 893                 /* merge: refcount = (refcount-1)(29, 5, 29) */
 894                 reached[0][5] = 1;
 895                 (trpt+1)->bup.ovals[2] = ((int)now.refcount);
 896                 now.refcount = (((int)now.refcount)-1);
 897 #ifdef VAR_RANGES
 898                 logval("refcount", ((int)now.refcount));
 899 #endif
 900                 ;
 901                 /* merge: goto not_needed(29, 6, 29) */
 902                 reached[0][6] = 1;
 903                 ;
 904                 _m = 3; goto P999; /* 2 */
 905         case 55: /* STATE 8 - line 64 "buffer.spin" - [(1)] (18:0:0 - 1) */
 906                 IfNotBlocked
 907                 reached[0][8] = 1;
 908                 if (!(1))
 909                         continue;
 910                 /* merge: .(goto)(0, 10, 18) */
 911                 reached[0][10] = 1;
 912                 ;
 913                 _m = 3; goto P999; /* 1 */
 914         case 56: /* STATE 12 - line 69 "buffer.spin" - [((prev_off!=write_off))] (11:0:1 - 1) */
 915                 IfNotBlocked
 916                 reached[0][12] = 1;
 917                 if (!((((int)((P0 *)this)->prev_off)!=((int)now.write_off))))
 918                         continue;
 919                 /* dead 1: prev_off */  (trpt+1)->bup.oval = ((P0 *)this)->prev_off;
 920 #ifdef HAS_CODE
 921                 if (!readtrail)
 922 #endif
 923                         ((P0 *)this)->prev_off = 0;
 924                 /* merge: goto cmpxchg_loop(0, 13, 11) */
 925                 reached[0][13] = 1;
 926                 ;
 927                 _m = 3; goto P999; /* 1 */
 928         case 57: /* STATE 17 - line 72 "buffer.spin" - [.(goto)] (0:28:0 - 1) */
 929                 IfNotBlocked
 930                 reached[0][17] = 1;
 931                 ;
 932                 _m = 3; goto P999; /* 0 */
 933         case 58: /* STATE 15 - line 70 "buffer.spin" - [write_off = new_off] (0:28:1 - 1) */
 934                 IfNotBlocked
 935                 reached[0][15] = 1;
 936                 (trpt+1)->bup.oval = ((int)now.write_off);
 937                 now.write_off = ((int)((P0 *)this)->new_off);
 938 #ifdef VAR_RANGES
 939                 logval("write_off", ((int)now.write_off));
 940 #endif
 941                 ;
 942                 /* merge: .(goto)(28, 17, 28) */
 943                 reached[0][17] = 1;
 944                 ;
 945                 _m = 3; goto P999; /* 1 */
 946         case 59: /* STATE 19 - line 75 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:25:2 - 1) */
 947                 IfNotBlocked
 948                 reached[0][19] = 1;
 949                 (trpt+1)->bup.ovals = grab_ints(2);
 950                 (trpt+1)->bup.ovals[0] = ((int)((P0 *)this)->tmp_commit);
 951                 ((P0 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%4)/(4/2)), 2) ])+((int)((P0 *)this)->size));
 952 #ifdef VAR_RANGES
 953                 logval("switcher:tmp_commit", ((int)((P0 *)this)->tmp_commit));
 954 #endif
 955                 ;
 956                 /* merge: commit_count[((prev_off%4)/(4/2))] = tmp_commit(25, 20, 25) */
 957                 reached[0][20] = 1;
 958                 (trpt+1)->bup.ovals[1] = ((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%4)/(4/2)), 2) ]);
 959                 now.commit_count[ Index(((((P0 *)this)->prev_off%4)/(4/2)), 2) ] = ((int)((P0 *)this)->tmp_commit);
 960 #ifdef VAR_RANGES
 961                 logval("commit_count[((switcher:prev_off%4)/(4/2))]", ((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%4)/(4/2)), 2) ]));
 962 #endif
 963                 ;
 964                 _m = 3; goto P999; /* 1 */
 965         case 60: /* STATE 21 - line 78 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (29:0:3 - 1) */
 966                 IfNotBlocked
 967                 reached[0][21] = 1;
 968                 if (!(((((int)((P0 *)this)->tmp_commit)%(4/2))==0)))
 969                         continue;
 970                 /* dead 1: tmp_commit */  (trpt+1)->bup.ovals = grab_ints(3);
 971                 (trpt+1)->bup.ovals[0] = ((P0 *)this)->tmp_commit;
 972 #ifdef HAS_CODE
 973                 if (!readtrail)
 974 #endif
 975                         ((P0 *)this)->tmp_commit = 0;
 976                 /* merge: deliver = 1(29, 22, 29) */
 977                 reached[0][22] = 1;
 978                 (trpt+1)->bup.ovals[1] = ((int)deliver);
 979                 deliver = 1;
 980 #ifdef VAR_RANGES
 981                 logval("deliver", ((int)deliver));
 982 #endif
 983                 ;
 984                 /* merge: .(goto)(29, 26, 29) */
 985                 reached[0][26] = 1;
 986                 ;
 987                 /* merge: refcount = (refcount-1)(29, 27, 29) */
 988                 reached[0][27] = 1;
 989                 (trpt+1)->bup.ovals[2] = ((int)now.refcount);
 990                 now.refcount = (((int)now.refcount)-1);
 991 #ifdef VAR_RANGES
 992                 logval("refcount", ((int)now.refcount));
 993 #endif
 994                 ;
 995                 _m = 3; goto P999; /* 3 */
 996         case 61: /* STATE 26 - line 81 "buffer.spin" - [.(goto)] (0:29:1 - 2) */
 997                 IfNotBlocked
 998                 reached[0][26] = 1;
 999                 ;
1000                 /* merge: refcount = (refcount-1)(29, 27, 29) */
1001                 reached[0][27] = 1;
1002                 (trpt+1)->bup.oval = ((int)now.refcount);
1003                 now.refcount = (((int)now.refcount)-1);
1004 #ifdef VAR_RANGES
1005                 logval("refcount", ((int)now.refcount));
1006 #endif
1007                 ;
1008                 _m = 3; goto P999; /* 1 */
1009         case 62: /* STATE 24 - line 79 "buffer.spin" - [(1)] (29:0:1 - 1) */
1010                 IfNotBlocked
1011                 reached[0][24] = 1;
1012                 if (!(1))
1013                         continue;
1014                 /* merge: .(goto)(29, 26, 29) */
1015                 reached[0][26] = 1;
1016                 ;
1017                 /* merge: refcount = (refcount-1)(29, 27, 29) */
1018                 reached[0][27] = 1;
1019                 (trpt+1)->bup.oval = ((int)now.refcount);
1020                 now.refcount = (((int)now.refcount)-1);
1021 #ifdef VAR_RANGES
1022                 logval("refcount", ((int)now.refcount));
1023 #endif
1024                 ;
1025                 _m = 3; goto P999; /* 2 */
1026         case 63: /* STATE 30 - line 85 "buffer.spin" - [-end-] (0:0:0 - 1) */
1027                 IfNotBlocked
1028                 reached[0][30] = 1;
1029                 if (!delproc(1, II)) continue;
1030                 _m = 3; goto P999; /* 0 */
1031         case  _T5:      /* np_ */
1032                 if (!((!(trpt->o_pm&4) && !(trpt->tau&128))))
1033                         continue;
1034                 /* else fall through */
1035         case  _T2:      /* true */
1036                 _m = 3; goto P999;
1037 #undef rand
1038         }
1039