ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1611

User:	Jiri Slaby
Error type:	Reachable Error Location
Error type description:	A specified error location is reachable in some program path
File location:	product-lines/elevator_spec2_product03_safe.cil.c
Line in file:	1818
Project:	SV-COMP 2013
Project version:	2.6.28
Tools:	Manual Work
Entered:	2013-01-17 16:57:54 UTC
Source:

   1extern int __VERIFIER_nondet_int(void);
   2/* Generated by CIL v. 1.3.7 */
   3/* print_CIL_Input is true */
   4
   5#line 2 "libacc.c"
   6struct JoinPoint {
   7   void **(*fp)(struct JoinPoint * ) ;
   8   void **args ;
   9   int argsCount ;
  10   char const   **argsType ;
  11   void *(*arg)(int  , struct JoinPoint * ) ;
  12   char const   *(*argType)(int  , struct JoinPoint * ) ;
  13   void **retValue ;
  14   char const   *retType ;
  15   char const   *funcName ;
  16   char const   *targetName ;
  17   char const   *fileName ;
  18   char const   *kind ;
  19   void *excep_return ;
  20};
  21#line 18 "libacc.c"
  22struct __UTAC__CFLOW_FUNC {
  23   int (*func)(int  , int  ) ;
  24   int val ;
  25   struct __UTAC__CFLOW_FUNC *next ;
  26};
  27#line 18 "libacc.c"
  28struct __UTAC__EXCEPTION {
  29   void *jumpbuf ;
  30   unsigned long long prtValue ;
  31   int pops ;
  32   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  33};
  34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  35typedef unsigned long size_t;
  36#line 76 "libacc.c"
  37struct __ACC__ERR {
  38   void *v ;
  39   struct __ACC__ERR *next ;
  40};
  41#line 1 "Floor.o"
  42#pragma merger(0,"Floor.i","")
  43#line 12 "Floor.h"
  44int isFloorCalling(int floorID ) ;
  45#line 14
  46void resetCallOnFloor(int floorID ) ;
  47#line 16
  48void callOnFloor(int floorID ) ;
  49#line 18
  50int isPersonOnFloor(int person , int floor ) ;
  51#line 20
  52void initPersonOnFloor(int person , int floor ) ;
  53#line 22
  54void removePersonFromFloor(int person , int floor ) ;
  55#line 24
  56int isTopFloor(int floorID ) ;
  57#line 28
  58void initFloors(void) ;
  59#line 9 "Floor.c"
  60int calls_0  ;
  61#line 11 "Floor.c"
  62int calls_1  ;
  63#line 13 "Floor.c"
  64int calls_2  ;
  65#line 15 "Floor.c"
  66int calls_3  ;
  67#line 17 "Floor.c"
  68int calls_4  ;
  69#line 20 "Floor.c"
  70int personOnFloor_0_0  ;
  71#line 22 "Floor.c"
  72int personOnFloor_0_1  ;
  73#line 24 "Floor.c"
  74int personOnFloor_0_2  ;
  75#line 26 "Floor.c"
  76int personOnFloor_0_3  ;
  77#line 28 "Floor.c"
  78int personOnFloor_0_4  ;
  79#line 30 "Floor.c"
  80int personOnFloor_1_0  ;
  81#line 32 "Floor.c"
  82int personOnFloor_1_1  ;
  83#line 34 "Floor.c"
  84int personOnFloor_1_2  ;
  85#line 36 "Floor.c"
  86int personOnFloor_1_3  ;
  87#line 38 "Floor.c"
  88int personOnFloor_1_4  ;
  89#line 40 "Floor.c"
  90int personOnFloor_2_0  ;
  91#line 42 "Floor.c"
  92int personOnFloor_2_1  ;
  93#line 44 "Floor.c"
  94int personOnFloor_2_2  ;
  95#line 46 "Floor.c"
  96int personOnFloor_2_3  ;
  97#line 48 "Floor.c"
  98int personOnFloor_2_4  ;
  99#line 50 "Floor.c"
 100int personOnFloor_3_0  ;
 101#line 52 "Floor.c"
 102int personOnFloor_3_1  ;
 103#line 54 "Floor.c"
 104int personOnFloor_3_2  ;
 105#line 56 "Floor.c"
 106int personOnFloor_3_3  ;
 107#line 58 "Floor.c"
 108int personOnFloor_3_4  ;
 109#line 60 "Floor.c"
 110int personOnFloor_4_0  ;
 111#line 62 "Floor.c"
 112int personOnFloor_4_1  ;
 113#line 64 "Floor.c"
 114int personOnFloor_4_2  ;
 115#line 66 "Floor.c"
 116int personOnFloor_4_3  ;
 117#line 68 "Floor.c"
 118int personOnFloor_4_4  ;
 119#line 70 "Floor.c"
 120int personOnFloor_5_0  ;
 121#line 72 "Floor.c"
 122int personOnFloor_5_1  ;
 123#line 74 "Floor.c"
 124int personOnFloor_5_2  ;
 125#line 76 "Floor.c"
 126int personOnFloor_5_3  ;
 127#line 78 "Floor.c"
 128int personOnFloor_5_4  ;
 129#line 81 "Floor.c"
 130void initFloors(void) 
 131{ 
 132
 133  {
 134#line 82
 135  calls_0 = 0;
 136#line 83
 137  calls_1 = 0;
 138#line 84
 139  calls_2 = 0;
 140#line 85
 141  calls_3 = 0;
 142#line 86
 143  calls_4 = 0;
 144#line 87
 145  personOnFloor_0_0 = 0;
 146#line 88
 147  personOnFloor_0_1 = 0;
 148#line 89
 149  personOnFloor_0_2 = 0;
 150#line 90
 151  personOnFloor_0_3 = 0;
 152#line 91
 153  personOnFloor_0_4 = 0;
 154#line 92
 155  personOnFloor_1_0 = 0;
 156#line 93
 157  personOnFloor_1_1 = 0;
 158#line 94
 159  personOnFloor_1_2 = 0;
 160#line 95
 161  personOnFloor_1_3 = 0;
 162#line 96
 163  personOnFloor_1_4 = 0;
 164#line 97
 165  personOnFloor_2_0 = 0;
 166#line 98
 167  personOnFloor_2_1 = 0;
 168#line 99
 169  personOnFloor_2_2 = 0;
 170#line 100
 171  personOnFloor_2_3 = 0;
 172#line 101
 173  personOnFloor_2_4 = 0;
 174#line 102
 175  personOnFloor_3_0 = 0;
 176#line 103
 177  personOnFloor_3_1 = 0;
 178#line 104
 179  personOnFloor_3_2 = 0;
 180#line 105
 181  personOnFloor_3_3 = 0;
 182#line 106
 183  personOnFloor_3_4 = 0;
 184#line 107
 185  personOnFloor_4_0 = 0;
 186#line 108
 187  personOnFloor_4_1 = 0;
 188#line 109
 189  personOnFloor_4_2 = 0;
 190#line 110
 191  personOnFloor_4_3 = 0;
 192#line 111
 193  personOnFloor_4_4 = 0;
 194#line 112
 195  personOnFloor_5_0 = 0;
 196#line 113
 197  personOnFloor_5_1 = 0;
 198#line 114
 199  personOnFloor_5_2 = 0;
 200#line 115
 201  personOnFloor_5_3 = 0;
 202#line 116
 203  personOnFloor_5_4 = 0;
 204#line 1120 "Floor.c"
 205  return;
 206}
 207}
 208#line 120 "Floor.c"
 209int isFloorCalling(int floorID ) 
 210{ int retValue_acc ;
 211
 212  {
 213#line 126 "Floor.c"
 214  if (floorID == 0) {
 215#line 1139
 216    retValue_acc = calls_0;
 217#line 1141
 218    return (retValue_acc);
 219  } else {
 220#line 1143
 221    if (floorID == 1) {
 222#line 1146
 223      retValue_acc = calls_1;
 224#line 1148
 225      return (retValue_acc);
 226    } else {
 227#line 1150
 228      if (floorID == 2) {
 229#line 1153
 230        retValue_acc = calls_2;
 231#line 1155
 232        return (retValue_acc);
 233      } else {
 234#line 1157
 235        if (floorID == 3) {
 236#line 1160
 237          retValue_acc = calls_3;
 238#line 1162
 239          return (retValue_acc);
 240        } else {
 241#line 1164
 242          if (floorID == 4) {
 243#line 1167 "Floor.c"
 244            retValue_acc = calls_4;
 245#line 1169
 246            return (retValue_acc);
 247          } else {
 248
 249          }
 250        }
 251      }
 252    }
 253  }
 254#line 1174 "Floor.c"
 255  retValue_acc = 0;
 256#line 1176
 257  return (retValue_acc);
 258#line 1183
 259  return (retValue_acc);
 260}
 261}
 262#line 130 "Floor.c"
 263void resetCallOnFloor(int floorID ) 
 264{ 
 265
 266  {
 267#line 136
 268  if (floorID == 0) {
 269#line 137
 270    calls_0 = 0;
 271  } else {
 272#line 138
 273    if (floorID == 1) {
 274#line 139
 275      calls_1 = 0;
 276    } else {
 277#line 140
 278      if (floorID == 2) {
 279#line 141
 280        calls_2 = 0;
 281      } else {
 282#line 142
 283        if (floorID == 3) {
 284#line 143
 285          calls_3 = 0;
 286        } else {
 287#line 144
 288          if (floorID == 4) {
 289#line 145
 290            calls_4 = 0;
 291          } else {
 292
 293          }
 294        }
 295      }
 296    }
 297  }
 298#line 1216 "Floor.c"
 299  return;
 300}
 301}
 302#line 139 "Floor.c"
 303void callOnFloor(int floorID ) 
 304{ 
 305
 306  {
 307#line 145
 308  if (floorID == 0) {
 309#line 146
 310    calls_0 = 1;
 311  } else {
 312#line 147
 313    if (floorID == 1) {
 314#line 148
 315      calls_1 = 1;
 316    } else {
 317#line 149
 318      if (floorID == 2) {
 319#line 150
 320        calls_2 = 1;
 321      } else {
 322#line 151
 323        if (floorID == 3) {
 324#line 152
 325          calls_3 = 1;
 326        } else {
 327#line 153
 328          if (floorID == 4) {
 329#line 154
 330            calls_4 = 1;
 331          } else {
 332
 333          }
 334        }
 335      }
 336    }
 337  }
 338#line 1245 "Floor.c"
 339  return;
 340}
 341}
 342#line 148 "Floor.c"
 343int isPersonOnFloor(int person , int floor ) 
 344{ int retValue_acc ;
 345
 346  {
 347#line 185
 348  if (floor == 0) {
 349#line 156 "Floor.c"
 350    if (person == 0) {
 351#line 1267
 352      retValue_acc = personOnFloor_0_0;
 353#line 1269
 354      return (retValue_acc);
 355    } else {
 356#line 1271
 357      if (person == 1) {
 358#line 1274
 359        retValue_acc = personOnFloor_1_0;
 360#line 1276
 361        return (retValue_acc);
 362      } else {
 363#line 1278
 364        if (person == 2) {
 365#line 1281
 366          retValue_acc = personOnFloor_2_0;
 367#line 1283
 368          return (retValue_acc);
 369        } else {
 370#line 1285
 371          if (person == 3) {
 372#line 1288
 373            retValue_acc = personOnFloor_3_0;
 374#line 1290
 375            return (retValue_acc);
 376          } else {
 377#line 1292
 378            if (person == 4) {
 379#line 1295
 380              retValue_acc = personOnFloor_4_0;
 381#line 1297
 382              return (retValue_acc);
 383            } else {
 384#line 1299
 385              if (person == 5) {
 386#line 1302
 387                retValue_acc = personOnFloor_5_0;
 388#line 1304
 389                return (retValue_acc);
 390              } else {
 391
 392              }
 393            }
 394          }
 395        }
 396      }
 397    }
 398  } else {
 399#line 1306 "Floor.c"
 400    if (floor == 1) {
 401#line 163 "Floor.c"
 402      if (person == 0) {
 403#line 1312
 404        retValue_acc = personOnFloor_0_1;
 405#line 1314
 406        return (retValue_acc);
 407      } else {
 408#line 1316
 409        if (person == 1) {
 410#line 1319
 411          retValue_acc = personOnFloor_1_1;
 412#line 1321
 413          return (retValue_acc);
 414        } else {
 415#line 1323
 416          if (person == 2) {
 417#line 1326
 418            retValue_acc = personOnFloor_2_1;
 419#line 1328
 420            return (retValue_acc);
 421          } else {
 422#line 1330
 423            if (person == 3) {
 424#line 1333
 425              retValue_acc = personOnFloor_3_1;
 426#line 1335
 427              return (retValue_acc);
 428            } else {
 429#line 1337
 430              if (person == 4) {
 431#line 1340
 432                retValue_acc = personOnFloor_4_1;
 433#line 1342
 434                return (retValue_acc);
 435              } else {
 436#line 1344
 437                if (person == 5) {
 438#line 1347
 439                  retValue_acc = personOnFloor_5_1;
 440#line 1349
 441                  return (retValue_acc);
 442                } else {
 443
 444                }
 445              }
 446            }
 447          }
 448        }
 449      }
 450    } else {
 451#line 1351 "Floor.c"
 452      if (floor == 2) {
 453#line 170 "Floor.c"
 454        if (person == 0) {
 455#line 1357
 456          retValue_acc = personOnFloor_0_2;
 457#line 1359
 458          return (retValue_acc);
 459        } else {
 460#line 1361
 461          if (person == 1) {
 462#line 1364
 463            retValue_acc = personOnFloor_1_2;
 464#line 1366
 465            return (retValue_acc);
 466          } else {
 467#line 1368
 468            if (person == 2) {
 469#line 1371
 470              retValue_acc = personOnFloor_2_2;
 471#line 1373
 472              return (retValue_acc);
 473            } else {
 474#line 1375
 475              if (person == 3) {
 476#line 1378
 477                retValue_acc = personOnFloor_3_2;
 478#line 1380
 479                return (retValue_acc);
 480              } else {
 481#line 1382
 482                if (person == 4) {
 483#line 1385
 484                  retValue_acc = personOnFloor_4_2;
 485#line 1387
 486                  return (retValue_acc);
 487                } else {
 488#line 1389
 489                  if (person == 5) {
 490#line 1392
 491                    retValue_acc = personOnFloor_5_2;
 492#line 1394
 493                    return (retValue_acc);
 494                  } else {
 495
 496                  }
 497                }
 498              }
 499            }
 500          }
 501        }
 502      } else {
 503#line 1396 "Floor.c"
 504        if (floor == 3) {
 505#line 177 "Floor.c"
 506          if (person == 0) {
 507#line 1402
 508            retValue_acc = personOnFloor_0_3;
 509#line 1404
 510            return (retValue_acc);
 511          } else {
 512#line 1406
 513            if (person == 1) {
 514#line 1409
 515              retValue_acc = personOnFloor_1_3;
 516#line 1411
 517              return (retValue_acc);
 518            } else {
 519#line 1413
 520              if (person == 2) {
 521#line 1416
 522                retValue_acc = personOnFloor_2_3;
 523#line 1418
 524                return (retValue_acc);
 525              } else {
 526#line 1420
 527                if (person == 3) {
 528#line 1423
 529                  retValue_acc = personOnFloor_3_3;
 530#line 1425
 531                  return (retValue_acc);
 532                } else {
 533#line 1427
 534                  if (person == 4) {
 535#line 1430
 536                    retValue_acc = personOnFloor_4_3;
 537#line 1432
 538                    return (retValue_acc);
 539                  } else {
 540#line 1434
 541                    if (person == 5) {
 542#line 1437
 543                      retValue_acc = personOnFloor_5_3;
 544#line 1439
 545                      return (retValue_acc);
 546                    } else {
 547
 548                    }
 549                  }
 550                }
 551              }
 552            }
 553          }
 554        } else {
 555#line 1441 "Floor.c"
 556          if (floor == 4) {
 557#line 184 "Floor.c"
 558            if (person == 0) {
 559#line 1447
 560              retValue_acc = personOnFloor_0_4;
 561#line 1449
 562              return (retValue_acc);
 563            } else {
 564#line 1451
 565              if (person == 1) {
 566#line 1454
 567                retValue_acc = personOnFloor_1_4;
 568#line 1456
 569                return (retValue_acc);
 570              } else {
 571#line 1458
 572                if (person == 2) {
 573#line 1461
 574                  retValue_acc = personOnFloor_2_4;
 575#line 1463
 576                  return (retValue_acc);
 577                } else {
 578#line 1465
 579                  if (person == 3) {
 580#line 1468
 581                    retValue_acc = personOnFloor_3_4;
 582#line 1470
 583                    return (retValue_acc);
 584                  } else {
 585#line 1472
 586                    if (person == 4) {
 587#line 1475
 588                      retValue_acc = personOnFloor_4_4;
 589#line 1477
 590                      return (retValue_acc);
 591                    } else {
 592#line 1479
 593                      if (person == 5) {
 594#line 1482 "Floor.c"
 595                        retValue_acc = personOnFloor_5_4;
 596#line 1484
 597                        return (retValue_acc);
 598                      } else {
 599
 600                      }
 601                    }
 602                  }
 603                }
 604              }
 605            }
 606          } else {
 607
 608          }
 609        }
 610      }
 611    }
 612  }
 613#line 1489 "Floor.c"
 614  retValue_acc = 0;
 615#line 1491
 616  return (retValue_acc);
 617#line 1498
 618  return (retValue_acc);
 619}
 620}
 621#line 188 "Floor.c"
 622void initPersonOnFloor(int person , int floor ) 
 623{ 
 624
 625  {
 626#line 225
 627  if (floor == 0) {
 628#line 196
 629    if (person == 0) {
 630#line 197
 631      personOnFloor_0_0 = 1;
 632    } else {
 633#line 198
 634      if (person == 1) {
 635#line 199
 636        personOnFloor_1_0 = 1;
 637      } else {
 638#line 200
 639        if (person == 2) {
 640#line 201
 641          personOnFloor_2_0 = 1;
 642        } else {
 643#line 202
 644          if (person == 3) {
 645#line 203
 646            personOnFloor_3_0 = 1;
 647          } else {
 648#line 204
 649            if (person == 4) {
 650#line 205
 651              personOnFloor_4_0 = 1;
 652            } else {
 653#line 206
 654              if (person == 5) {
 655#line 207
 656                personOnFloor_5_0 = 1;
 657              } else {
 658
 659              }
 660            }
 661          }
 662        }
 663      }
 664    }
 665  } else {
 666#line 208
 667    if (floor == 1) {
 668#line 203
 669      if (person == 0) {
 670#line 204
 671        personOnFloor_0_1 = 1;
 672      } else {
 673#line 205
 674        if (person == 1) {
 675#line 206
 676          personOnFloor_1_1 = 1;
 677        } else {
 678#line 207
 679          if (person == 2) {
 680#line 208
 681            personOnFloor_2_1 = 1;
 682          } else {
 683#line 209
 684            if (person == 3) {
 685#line 210
 686              personOnFloor_3_1 = 1;
 687            } else {
 688#line 211
 689              if (person == 4) {
 690#line 212
 691                personOnFloor_4_1 = 1;
 692              } else {
 693#line 213
 694                if (person == 5) {
 695#line 214
 696                  personOnFloor_5_1 = 1;
 697                } else {
 698
 699                }
 700              }
 701            }
 702          }
 703        }
 704      }
 705    } else {
 706#line 215
 707      if (floor == 2) {
 708#line 210
 709        if (person == 0) {
 710#line 211
 711          personOnFloor_0_2 = 1;
 712        } else {
 713#line 212
 714          if (person == 1) {
 715#line 213
 716            personOnFloor_1_2 = 1;
 717          } else {
 718#line 214
 719            if (person == 2) {
 720#line 215
 721              personOnFloor_2_2 = 1;
 722            } else {
 723#line 216
 724              if (person == 3) {
 725#line 217
 726                personOnFloor_3_2 = 1;
 727              } else {
 728#line 218
 729                if (person == 4) {
 730#line 219
 731                  personOnFloor_4_2 = 1;
 732                } else {
 733#line 220
 734                  if (person == 5) {
 735#line 221
 736                    personOnFloor_5_2 = 1;
 737                  } else {
 738
 739                  }
 740                }
 741              }
 742            }
 743          }
 744        }
 745      } else {
 746#line 222
 747        if (floor == 3) {
 748#line 217
 749          if (person == 0) {
 750#line 218
 751            personOnFloor_0_3 = 1;
 752          } else {
 753#line 219
 754            if (person == 1) {
 755#line 220
 756              personOnFloor_1_3 = 1;
 757            } else {
 758#line 221
 759              if (person == 2) {
 760#line 222
 761                personOnFloor_2_3 = 1;
 762              } else {
 763#line 223
 764                if (person == 3) {
 765#line 224
 766                  personOnFloor_3_3 = 1;
 767                } else {
 768#line 225
 769                  if (person == 4) {
 770#line 226
 771                    personOnFloor_4_3 = 1;
 772                  } else {
 773#line 227
 774                    if (person == 5) {
 775#line 228
 776                      personOnFloor_5_3 = 1;
 777                    } else {
 778
 779                    }
 780                  }
 781                }
 782              }
 783            }
 784          }
 785        } else {
 786#line 229
 787          if (floor == 4) {
 788#line 224
 789            if (person == 0) {
 790#line 225
 791              personOnFloor_0_4 = 1;
 792            } else {
 793#line 226
 794              if (person == 1) {
 795#line 227
 796                personOnFloor_1_4 = 1;
 797              } else {
 798#line 228
 799                if (person == 2) {
 800#line 229
 801                  personOnFloor_2_4 = 1;
 802                } else {
 803#line 230
 804                  if (person == 3) {
 805#line 231
 806                    personOnFloor_3_4 = 1;
 807                  } else {
 808#line 232
 809                    if (person == 4) {
 810#line 233
 811                      personOnFloor_4_4 = 1;
 812                    } else {
 813#line 234
 814                      if (person == 5) {
 815#line 235
 816                        personOnFloor_5_4 = 1;
 817                      } else {
 818
 819                      }
 820                    }
 821                  }
 822                }
 823              }
 824            }
 825          } else {
 826
 827          }
 828        }
 829      }
 830    }
 831  }
 832  {
 833#line 225
 834  callOnFloor(floor);
 835  }
 836#line 1598 "Floor.c"
 837  return;
 838}
 839}
 840#line 228 "Floor.c"
 841void removePersonFromFloor(int person , int floor ) 
 842{ 
 843
 844  {
 845#line 265
 846  if (floor == 0) {
 847#line 236
 848    if (person == 0) {
 849#line 237
 850      personOnFloor_0_0 = 0;
 851    } else {
 852#line 238
 853      if (person == 1) {
 854#line 239
 855        personOnFloor_1_0 = 0;
 856      } else {
 857#line 240
 858        if (person == 2) {
 859#line 241
 860          personOnFloor_2_0 = 0;
 861        } else {
 862#line 242
 863          if (person == 3) {
 864#line 243
 865            personOnFloor_3_0 = 0;
 866          } else {
 867#line 244
 868            if (person == 4) {
 869#line 245
 870              personOnFloor_4_0 = 0;
 871            } else {
 872#line 246
 873              if (person == 5) {
 874#line 247
 875                personOnFloor_5_0 = 0;
 876              } else {
 877
 878              }
 879            }
 880          }
 881        }
 882      }
 883    }
 884  } else {
 885#line 248
 886    if (floor == 1) {
 887#line 243
 888      if (person == 0) {
 889#line 244
 890        personOnFloor_0_1 = 0;
 891      } else {
 892#line 245
 893        if (person == 1) {
 894#line 246
 895          personOnFloor_1_1 = 0;
 896        } else {
 897#line 247
 898          if (person == 2) {
 899#line 248
 900            personOnFloor_2_1 = 0;
 901          } else {
 902#line 249
 903            if (person == 3) {
 904#line 250
 905              personOnFloor_3_1 = 0;
 906            } else {
 907#line 251
 908              if (person == 4) {
 909#line 252
 910                personOnFloor_4_1 = 0;
 911              } else {
 912#line 253
 913                if (person == 5) {
 914#line 254
 915                  personOnFloor_5_1 = 0;
 916                } else {
 917
 918                }
 919              }
 920            }
 921          }
 922        }
 923      }
 924    } else {
 925#line 255
 926      if (floor == 2) {
 927#line 250
 928        if (person == 0) {
 929#line 251
 930          personOnFloor_0_2 = 0;
 931        } else {
 932#line 252
 933          if (person == 1) {
 934#line 253
 935            personOnFloor_1_2 = 0;
 936          } else {
 937#line 254
 938            if (person == 2) {
 939#line 255
 940              personOnFloor_2_2 = 0;
 941            } else {
 942#line 256
 943              if (person == 3) {
 944#line 257
 945                personOnFloor_3_2 = 0;
 946              } else {
 947#line 258
 948                if (person == 4) {
 949#line 259
 950                  personOnFloor_4_2 = 0;
 951                } else {
 952#line 260
 953                  if (person == 5) {
 954#line 261
 955                    personOnFloor_5_2 = 0;
 956                  } else {
 957
 958                  }
 959                }
 960              }
 961            }
 962          }
 963        }
 964      } else {
 965#line 262
 966        if (floor == 3) {
 967#line 257
 968          if (person == 0) {
 969#line 258
 970            personOnFloor_0_3 = 0;
 971          } else {
 972#line 259
 973            if (person == 1) {
 974#line 260
 975              personOnFloor_1_3 = 0;
 976            } else {
 977#line 261
 978              if (person == 2) {
 979#line 262
 980                personOnFloor_2_3 = 0;
 981              } else {
 982#line 263
 983                if (person == 3) {
 984#line 264
 985                  personOnFloor_3_3 = 0;
 986                } else {
 987#line 265
 988                  if (person == 4) {
 989#line 266
 990                    personOnFloor_4_3 = 0;
 991                  } else {
 992#line 267
 993                    if (person == 5) {
 994#line 268
 995                      personOnFloor_5_3 = 0;
 996                    } else {
 997
 998                    }
 999                  }
1000                }
1001              }
1002            }
1003          }
1004        } else {
1005#line 269
1006          if (floor == 4) {
1007#line 264
1008            if (person == 0) {
1009#line 265
1010              personOnFloor_0_4 = 0;
1011            } else {
1012#line 266
1013              if (person == 1) {
1014#line 267
1015                personOnFloor_1_4 = 0;
1016              } else {
1017#line 268
1018                if (person == 2) {
1019#line 269
1020                  personOnFloor_2_4 = 0;
1021                } else {
1022#line 270
1023                  if (person == 3) {
1024#line 271
1025                    personOnFloor_3_4 = 0;
1026                  } else {
1027#line 272
1028                    if (person == 4) {
1029#line 273
1030                      personOnFloor_4_4 = 0;
1031                    } else {
1032#line 274
1033                      if (person == 5) {
1034#line 275
1035                        personOnFloor_5_4 = 0;
1036                      } else {
1037
1038                      }
1039                    }
1040                  }
1041                }
1042              }
1043            }
1044          } else {
1045
1046          }
1047        }
1048      }
1049    }
1050  }
1051  {
1052#line 265
1053  resetCallOnFloor(floor);
1054  }
1055#line 1694 "Floor.c"
1056  return;
1057}
1058}
1059#line 268 "Floor.c"
1060int isTopFloor(int floorID ) 
1061{ int retValue_acc ;
1062
1063  {
1064#line 1712 "Floor.c"
1065  retValue_acc = floorID == 4;
1066#line 1714
1067  return (retValue_acc);
1068#line 1721
1069  return (retValue_acc);
1070}
1071}
1072#line 1 "Person.o"
1073#pragma merger(0,"Person.i","")
1074#line 10 "Person.h"
1075int getWeight(int person ) ;
1076#line 12
1077int getOrigin(int person ) ;
1078#line 14
1079int getDestination(int person ) ;
1080#line 20 "Person.c"
1081int getWeight(int person ) 
1082{ int retValue_acc ;
1083
1084  {
1085#line 35 "Person.c"
1086  if (person == 0) {
1087#line 974
1088    retValue_acc = 40;
1089#line 976
1090    return (retValue_acc);
1091  } else {
1092#line 978
1093    if (person == 1) {
1094#line 983
1095      retValue_acc = 40;
1096#line 985
1097      return (retValue_acc);
1098    } else {
1099#line 987
1100      if (person == 2) {
1101#line 992
1102        retValue_acc = 40;
1103#line 994
1104        return (retValue_acc);
1105      } else {
1106#line 996
1107        if (person == 3) {
1108#line 1001
1109          retValue_acc = 40;
1110#line 1003
1111          return (retValue_acc);
1112        } else {
1113#line 1005
1114          if (person == 4) {
1115#line 1010
1116            retValue_acc = 30;
1117#line 1012
1118            return (retValue_acc);
1119          } else {
1120#line 1014
1121            if (person == 5) {
1122#line 1019
1123              retValue_acc = 150;
1124#line 1021
1125              return (retValue_acc);
1126            } else {
1127#line 1027 "Person.c"
1128              retValue_acc = 0;
1129#line 1029
1130              return (retValue_acc);
1131            }
1132          }
1133        }
1134      }
1135    }
1136  }
1137#line 1036 "Person.c"
1138  return (retValue_acc);
1139}
1140}
1141#line 39 "Person.c"
1142int getOrigin(int person ) 
1143{ int retValue_acc ;
1144
1145  {
1146#line 54 "Person.c"
1147  if (person == 0) {
1148#line 1061
1149    retValue_acc = 4;
1150#line 1063
1151    return (retValue_acc);
1152  } else {
1153#line 1065
1154    if (person == 1) {
1155#line 1070
1156      retValue_acc = 3;
1157#line 1072
1158      return (retValue_acc);
1159    } else {
1160#line 1074
1161      if (person == 2) {
1162#line 1079
1163        retValue_acc = 2;
1164#line 1081
1165        return (retValue_acc);
1166      } else {
1167#line 1083
1168        if (person == 3) {
1169#line 1088
1170          retValue_acc = 1;
1171#line 1090
1172          return (retValue_acc);
1173        } else {
1174#line 1092
1175          if (person == 4) {
1176#line 1097
1177            retValue_acc = 0;
1178#line 1099
1179            return (retValue_acc);
1180          } else {
1181#line 1101
1182            if (person == 5) {
1183#line 1106
1184              retValue_acc = 1;
1185#line 1108
1186              return (retValue_acc);
1187            } else {
1188#line 1114 "Person.c"
1189              retValue_acc = 0;
1190#line 1116
1191              return (retValue_acc);
1192            }
1193          }
1194        }
1195      }
1196    }
1197  }
1198#line 1123 "Person.c"
1199  return (retValue_acc);
1200}
1201}
1202#line 57 "Person.c"
1203int getDestination(int person ) 
1204{ int retValue_acc ;
1205
1206  {
1207#line 72 "Person.c"
1208  if (person == 0) {
1209#line 1148
1210    retValue_acc = 0;
1211#line 1150
1212    return (retValue_acc);
1213  } else {
1214#line 1152
1215    if (person == 1) {
1216#line 1157
1217      retValue_acc = 0;
1218#line 1159
1219      return (retValue_acc);
1220    } else {
1221#line 1161
1222      if (person == 2) {
1223#line 1166
1224        retValue_acc = 1;
1225#line 1168
1226        return (retValue_acc);
1227      } else {
1228#line 1170
1229        if (person == 3) {
1230#line 1175
1231          retValue_acc = 3;
1232#line 1177
1233          return (retValue_acc);
1234        } else {
1235#line 1179
1236          if (person == 4) {
1237#line 1184
1238            retValue_acc = 1;
1239#line 1186
1240            return (retValue_acc);
1241          } else {
1242#line 1188
1243            if (person == 5) {
1244#line 1193
1245              retValue_acc = 3;
1246#line 1195
1247              return (retValue_acc);
1248            } else {
1249#line 1201 "Person.c"
1250              retValue_acc = 0;
1251#line 1203
1252              return (retValue_acc);
1253            }
1254          }
1255        }
1256      }
1257    }
1258  }
1259#line 1210 "Person.c"
1260  return (retValue_acc);
1261}
1262}
1263#line 1 "scenario.o"
1264#pragma merger(0,"scenario.i","")
1265#line 2 "scenario.c"
1266void bigMacCall(void) ;
1267#line 3
1268void cleanup(void) ;
1269#line 1 "scenario.c"
1270void test(void) 
1271{ 
1272
1273  {
1274  {
1275#line 2
1276  bigMacCall();
1277#line 3
1278  cleanup();
1279  }
1280#line 53 "scenario.c"
1281  return;
1282}
1283}
1284#line 1 "libacc.o"
1285#pragma merger(0,"libacc.i","")
1286#line 73 "/usr/include/assert.h"
1287extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
1288                                                                      char const   *__file ,
1289                                                                      unsigned int __line ,
1290                                                                      char const   *__function ) ;
1291#line 471 "/usr/include/stdlib.h"
1292extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
1293#line 488
1294extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
1295#line 32 "libacc.c"
1296void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
1297                                                                           int  ) ,
1298                                       int val ) 
1299{ struct __UTAC__EXCEPTION *excep ;
1300  struct __UTAC__CFLOW_FUNC *cf ;
1301  void *tmp ;
1302  unsigned long __cil_tmp7 ;
1303  unsigned long __cil_tmp8 ;
1304  unsigned long __cil_tmp9 ;
1305  unsigned long __cil_tmp10 ;
1306  unsigned long __cil_tmp11 ;
1307  unsigned long __cil_tmp12 ;
1308  unsigned long __cil_tmp13 ;
1309  unsigned long __cil_tmp14 ;
1310  int (**mem_15)(int  , int  ) ;
1311  int *mem_16 ;
1312  struct __UTAC__CFLOW_FUNC **mem_17 ;
1313  struct __UTAC__CFLOW_FUNC **mem_18 ;
1314  struct __UTAC__CFLOW_FUNC **mem_19 ;
1315
1316  {
1317  {
1318#line 33
1319  excep = (struct __UTAC__EXCEPTION *)exception;
1320#line 34
1321  tmp = malloc(24UL);
1322#line 34
1323  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
1324#line 36
1325  mem_15 = (int (**)(int  , int  ))cf;
1326#line 36
1327  *mem_15 = cflow_func;
1328#line 37
1329  __cil_tmp7 = (unsigned long )cf;
1330#line 37
1331  __cil_tmp8 = __cil_tmp7 + 8;
1332#line 37
1333  mem_16 = (int *)__cil_tmp8;
1334#line 37
1335  *mem_16 = val;
1336#line 38
1337  __cil_tmp9 = (unsigned long )cf;
1338#line 38
1339  __cil_tmp10 = __cil_tmp9 + 16;
1340#line 38
1341  __cil_tmp11 = (unsigned long )excep;
1342#line 38
1343  __cil_tmp12 = __cil_tmp11 + 24;
1344#line 38
1345  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
1346#line 38
1347  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
1348#line 38
1349  *mem_17 = *mem_18;
1350#line 39
1351  __cil_tmp13 = (unsigned long )excep;
1352#line 39
1353  __cil_tmp14 = __cil_tmp13 + 24;
1354#line 39
1355  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
1356#line 39
1357  *mem_19 = cf;
1358  }
1359#line 654 "libacc.c"
1360  return;
1361}
1362}
1363#line 44 "libacc.c"
1364void __utac__exception__cf_handler_free(void *exception ) 
1365{ struct __UTAC__EXCEPTION *excep ;
1366  struct __UTAC__CFLOW_FUNC *cf ;
1367  struct __UTAC__CFLOW_FUNC *tmp ;
1368  unsigned long __cil_tmp5 ;
1369  unsigned long __cil_tmp6 ;
1370  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
1371  unsigned long __cil_tmp8 ;
1372  unsigned long __cil_tmp9 ;
1373  unsigned long __cil_tmp10 ;
1374  unsigned long __cil_tmp11 ;
1375  void *__cil_tmp12 ;
1376  unsigned long __cil_tmp13 ;
1377  unsigned long __cil_tmp14 ;
1378  struct __UTAC__CFLOW_FUNC **mem_15 ;
1379  struct __UTAC__CFLOW_FUNC **mem_16 ;
1380  struct __UTAC__CFLOW_FUNC **mem_17 ;
1381
1382  {
1383#line 45
1384  excep = (struct __UTAC__EXCEPTION *)exception;
1385#line 46
1386  __cil_tmp5 = (unsigned long )excep;
1387#line 46
1388  __cil_tmp6 = __cil_tmp5 + 24;
1389#line 46
1390  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
1391#line 46
1392  cf = *mem_15;
1393  {
1394#line 49
1395  while (1) {
1396    while_0_continue: /* CIL Label */ ;
1397    {
1398#line 49
1399    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
1400#line 49
1401    __cil_tmp8 = (unsigned long )__cil_tmp7;
1402#line 49
1403    __cil_tmp9 = (unsigned long )cf;
1404#line 49
1405    if (__cil_tmp9 != __cil_tmp8) {
1406
1407    } else {
1408      goto while_0_break;
1409    }
1410    }
1411    {
1412#line 50
1413    tmp = cf;
1414#line 51
1415    __cil_tmp10 = (unsigned long )cf;
1416#line 51
1417    __cil_tmp11 = __cil_tmp10 + 16;
1418#line 51
1419    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
1420#line 51
1421    cf = *mem_16;
1422#line 52
1423    __cil_tmp12 = (void *)tmp;
1424#line 52
1425    free(__cil_tmp12);
1426    }
1427  }
1428  while_0_break: /* CIL Label */ ;
1429  }
1430#line 55
1431  __cil_tmp13 = (unsigned long )excep;
1432#line 55
1433  __cil_tmp14 = __cil_tmp13 + 24;
1434#line 55
1435  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
1436#line 55
1437  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
1438#line 694 "libacc.c"
1439  return;
1440}
1441}
1442#line 59 "libacc.c"
1443void __utac__exception__cf_handler_reset(void *exception ) 
1444{ struct __UTAC__EXCEPTION *excep ;
1445  struct __UTAC__CFLOW_FUNC *cf ;
1446  unsigned long __cil_tmp5 ;
1447  unsigned long __cil_tmp6 ;
1448  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
1449  unsigned long __cil_tmp8 ;
1450  unsigned long __cil_tmp9 ;
1451  int (*__cil_tmp10)(int  , int  ) ;
1452  unsigned long __cil_tmp11 ;
1453  unsigned long __cil_tmp12 ;
1454  int __cil_tmp13 ;
1455  unsigned long __cil_tmp14 ;
1456  unsigned long __cil_tmp15 ;
1457  struct __UTAC__CFLOW_FUNC **mem_16 ;
1458  int (**mem_17)(int  , int  ) ;
1459  int *mem_18 ;
1460  struct __UTAC__CFLOW_FUNC **mem_19 ;
1461
1462  {
1463#line 60
1464  excep = (struct __UTAC__EXCEPTION *)exception;
1465#line 61
1466  __cil_tmp5 = (unsigned long )excep;
1467#line 61
1468  __cil_tmp6 = __cil_tmp5 + 24;
1469#line 61
1470  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
1471#line 61
1472  cf = *mem_16;
1473  {
1474#line 64
1475  while (1) {
1476    while_1_continue: /* CIL Label */ ;
1477    {
1478#line 64
1479    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
1480#line 64
1481    __cil_tmp8 = (unsigned long )__cil_tmp7;
1482#line 64
1483    __cil_tmp9 = (unsigned long )cf;
1484#line 64
1485    if (__cil_tmp9 != __cil_tmp8) {
1486
1487    } else {
1488      goto while_1_break;
1489    }
1490    }
1491    {
1492#line 65
1493    mem_17 = (int (**)(int  , int  ))cf;
1494#line 65
1495    __cil_tmp10 = *mem_17;
1496#line 65
1497    __cil_tmp11 = (unsigned long )cf;
1498#line 65
1499    __cil_tmp12 = __cil_tmp11 + 8;
1500#line 65
1501    mem_18 = (int *)__cil_tmp12;
1502#line 65
1503    __cil_tmp13 = *mem_18;
1504#line 65
1505    (*__cil_tmp10)(4, __cil_tmp13);
1506#line 66
1507    __cil_tmp14 = (unsigned long )cf;
1508#line 66
1509    __cil_tmp15 = __cil_tmp14 + 16;
1510#line 66
1511    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
1512#line 66
1513    cf = *mem_19;
1514    }
1515  }
1516  while_1_break: /* CIL Label */ ;
1517  }
1518  {
1519#line 69
1520  __utac__exception__cf_handler_free(exception);
1521  }
1522#line 732 "libacc.c"
1523  return;
1524}
1525}
1526#line 80 "libacc.c"
1527void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
1528#line 80 "libacc.c"
1529static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
1530#line 79 "libacc.c"
1531void *__utac__error_stack_mgt(void *env , int mode , int count ) 
1532{ void *retValue_acc ;
1533  struct __ACC__ERR *new ;
1534  void *tmp ;
1535  struct __ACC__ERR *temp ;
1536  struct __ACC__ERR *next ;
1537  void *excep ;
1538  unsigned long __cil_tmp10 ;
1539  unsigned long __cil_tmp11 ;
1540  unsigned long __cil_tmp12 ;
1541  unsigned long __cil_tmp13 ;
1542  void *__cil_tmp14 ;
1543  unsigned long __cil_tmp15 ;
1544  unsigned long __cil_tmp16 ;
1545  void *__cil_tmp17 ;
1546  void **mem_18 ;
1547  struct __ACC__ERR **mem_19 ;
1548  struct __ACC__ERR **mem_20 ;
1549  void **mem_21 ;
1550  struct __ACC__ERR **mem_22 ;
1551  void **mem_23 ;
1552  void **mem_24 ;
1553
1554  {
1555#line 82 "libacc.c"
1556  if (count == 0) {
1557#line 758 "libacc.c"
1558    return (retValue_acc);
1559  } else {
1560
1561  }
1562#line 86 "libacc.c"
1563  if (mode == 0) {
1564    {
1565#line 87
1566    tmp = malloc(16UL);
1567#line 87
1568    new = (struct __ACC__ERR *)tmp;
1569#line 88
1570    mem_18 = (void **)new;
1571#line 88
1572    *mem_18 = env;
1573#line 89
1574    __cil_tmp10 = (unsigned long )new;
1575#line 89
1576    __cil_tmp11 = __cil_tmp10 + 8;
1577#line 89
1578    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
1579#line 89
1580    *mem_19 = head;
1581#line 90
1582    head = new;
1583#line 776 "libacc.c"
1584    retValue_acc = (void *)new;
1585    }
1586#line 778
1587    return (retValue_acc);
1588  } else {
1589
1590  }
1591#line 94 "libacc.c"
1592  if (mode == 1) {
1593#line 95
1594    temp = head;
1595    {
1596#line 98
1597    while (1) {
1598      while_2_continue: /* CIL Label */ ;
1599#line 98
1600      if (count > 1) {
1601
1602      } else {
1603        goto while_2_break;
1604      }
1605      {
1606#line 99
1607      __cil_tmp12 = (unsigned long )temp;
1608#line 99
1609      __cil_tmp13 = __cil_tmp12 + 8;
1610#line 99
1611      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
1612#line 99
1613      next = *mem_20;
1614#line 100
1615      mem_21 = (void **)temp;
1616#line 100
1617      excep = *mem_21;
1618#line 101
1619      __cil_tmp14 = (void *)temp;
1620#line 101
1621      free(__cil_tmp14);
1622#line 102
1623      __utac__exception__cf_handler_reset(excep);
1624#line 103
1625      temp = next;
1626#line 104
1627      count = count - 1;
1628      }
1629    }
1630    while_2_break: /* CIL Label */ ;
1631    }
1632    {
1633#line 107
1634    __cil_tmp15 = (unsigned long )temp;
1635#line 107
1636    __cil_tmp16 = __cil_tmp15 + 8;
1637#line 107
1638    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
1639#line 107
1640    head = *mem_22;
1641#line 108
1642    mem_23 = (void **)temp;
1643#line 108
1644    excep = *mem_23;
1645#line 109
1646    __cil_tmp17 = (void *)temp;
1647#line 109
1648    free(__cil_tmp17);
1649#line 110
1650    __utac__exception__cf_handler_reset(excep);
1651#line 820 "libacc.c"
1652    retValue_acc = excep;
1653    }
1654#line 822
1655    return (retValue_acc);
1656  } else {
1657
1658  }
1659#line 114
1660  if (mode == 2) {
1661#line 118 "libacc.c"
1662    if (head) {
1663#line 831
1664      mem_24 = (void **)head;
1665#line 831
1666      retValue_acc = *mem_24;
1667#line 833
1668      return (retValue_acc);
1669    } else {
1670#line 837 "libacc.c"
1671      retValue_acc = (void *)0;
1672#line 839
1673      return (retValue_acc);
1674    }
1675  } else {
1676
1677  }
1678#line 846 "libacc.c"
1679  return (retValue_acc);
1680}
1681}
1682#line 122 "libacc.c"
1683void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
1684{ void *retValue_acc ;
1685  unsigned long __cil_tmp4 ;
1686  unsigned long __cil_tmp5 ;
1687  int __cil_tmp6 ;
1688  int __cil_tmp7 ;
1689  unsigned long __cil_tmp8 ;
1690  unsigned long __cil_tmp9 ;
1691  void **__cil_tmp10 ;
1692  void **__cil_tmp11 ;
1693  int *mem_12 ;
1694  void ***mem_13 ;
1695
1696  {
1697#line 123
1698  if (i > 0) {
1699    {
1700#line 123
1701    __cil_tmp4 = (unsigned long )this;
1702#line 123
1703    __cil_tmp5 = __cil_tmp4 + 16;
1704#line 123
1705    mem_12 = (int *)__cil_tmp5;
1706#line 123
1707    __cil_tmp6 = *mem_12;
1708#line 123
1709    if (i <= __cil_tmp6) {
1710
1711    } else {
1712      {
1713#line 123
1714      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1715                    123U, "__utac__get_this_arg");
1716      }
1717    }
1718    }
1719  } else {
1720    {
1721#line 123
1722    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1723                  123U, "__utac__get_this_arg");
1724    }
1725  }
1726#line 870 "libacc.c"
1727  __cil_tmp7 = i - 1;
1728#line 870
1729  __cil_tmp8 = (unsigned long )this;
1730#line 870
1731  __cil_tmp9 = __cil_tmp8 + 8;
1732#line 870
1733  mem_13 = (void ***)__cil_tmp9;
1734#line 870
1735  __cil_tmp10 = *mem_13;
1736#line 870
1737  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1738#line 870
1739  retValue_acc = *__cil_tmp11;
1740#line 872
1741  return (retValue_acc);
1742#line 879
1743  return (retValue_acc);
1744}
1745}
1746#line 129 "libacc.c"
1747char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
1748{ char const   *retValue_acc ;
1749  unsigned long __cil_tmp4 ;
1750  unsigned long __cil_tmp5 ;
1751  int __cil_tmp6 ;
1752  int __cil_tmp7 ;
1753  unsigned long __cil_tmp8 ;
1754  unsigned long __cil_tmp9 ;
1755  char const   **__cil_tmp10 ;
1756  char const   **__cil_tmp11 ;
1757  int *mem_12 ;
1758  char const   ***mem_13 ;
1759
1760  {
1761#line 131
1762  if (i > 0) {
1763    {
1764#line 131
1765    __cil_tmp4 = (unsigned long )this;
1766#line 131
1767    __cil_tmp5 = __cil_tmp4 + 16;
1768#line 131
1769    mem_12 = (int *)__cil_tmp5;
1770#line 131
1771    __cil_tmp6 = *mem_12;
1772#line 131
1773    if (i <= __cil_tmp6) {
1774
1775    } else {
1776      {
1777#line 131
1778      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1779                    131U, "__utac__get_this_argtype");
1780      }
1781    }
1782    }
1783  } else {
1784    {
1785#line 131
1786    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1787                  131U, "__utac__get_this_argtype");
1788    }
1789  }
1790#line 903 "libacc.c"
1791  __cil_tmp7 = i - 1;
1792#line 903
1793  __cil_tmp8 = (unsigned long )this;
1794#line 903
1795  __cil_tmp9 = __cil_tmp8 + 24;
1796#line 903
1797  mem_13 = (char const   ***)__cil_tmp9;
1798#line 903
1799  __cil_tmp10 = *mem_13;
1800#line 903
1801  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1802#line 903
1803  retValue_acc = *__cil_tmp11;
1804#line 905
1805  return (retValue_acc);
1806#line 912
1807  return (retValue_acc);
1808}
1809}
1810#line 1 "wsllib_check.o"
1811#pragma merger(0,"wsllib_check.i","")
1812#line 3 "wsllib_check.c"
1813void __automaton_fail(void) 
1814{ 
1815
1816  {
1817  goto ERROR;
1818  ERROR: ;
1819#line 53 "wsllib_check.c"
1820  return;
1821}
1822}
1823#line 1 "featureselect.o"
1824#pragma merger(0,"featureselect.i","")
1825#line 9 "featureselect.h"
1826int select_one(void) ;
1827#line 11
1828void select_features(void) ;
1829#line 13
1830void select_helpers(void) ;
1831#line 15
1832int valid_product(void) ;
1833#line 8 "featureselect.c"
1834int select_one(void) 
1835{ int retValue_acc ;
1836  int choice = __VERIFIER_nondet_int();
1837
1838  {
1839#line 63 "featureselect.c"
1840  retValue_acc = choice;
1841#line 65
1842  return (retValue_acc);
1843#line 72
1844  return (retValue_acc);
1845}
1846}
1847#line 14 "featureselect.c"
1848void select_features(void) 
1849{ 
1850
1851  {
1852#line 94 "featureselect.c"
1853  return;
1854}
1855}
1856#line 20 "featureselect.c"
1857void select_helpers(void) 
1858{ 
1859
1860  {
1861#line 112 "featureselect.c"
1862  return;
1863}
1864}
1865#line 25 "featureselect.c"
1866int valid_product(void) 
1867{ int retValue_acc ;
1868
1869  {
1870#line 130 "featureselect.c"
1871  retValue_acc = 1;
1872#line 132
1873  return (retValue_acc);
1874#line 139
1875  return (retValue_acc);
1876}
1877}
1878#line 1 "Test.o"
1879#pragma merger(0,"Test.i","")
1880#line 544 "/usr/include/stdlib.h"
1881extern  __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
1882#line 13 "Test.c"
1883int cleanupTimeShifts  =    12;
1884#line 17 "Test.c"
1885#line 23 "Test.c"
1886int get_nondetMinMax07(void) 
1887{ int retValue_acc ;
1888  int nd ;
1889  nd = __VERIFIER_nondet_int();
1890
1891  {
1892#line 26 "Test.c"
1893  if (nd == 0) {
1894#line 1108
1895    retValue_acc = 0;
1896#line 1110
1897    return (retValue_acc);
1898  } else {
1899#line 1112
1900    if (nd == 1) {
1901#line 1117
1902      retValue_acc = 1;
1903#line 1119
1904      return (retValue_acc);
1905    } else {
1906#line 1121
1907      if (nd == 2) {
1908#line 1126
1909        retValue_acc = 2;
1910#line 1128
1911        return (retValue_acc);
1912      } else {
1913#line 1130
1914        if (nd == 3) {
1915#line 1135
1916          retValue_acc = 3;
1917#line 1137
1918          return (retValue_acc);
1919        } else {
1920#line 1139
1921          if (nd == 4) {
1922#line 1144
1923            retValue_acc = 4;
1924#line 1146
1925            return (retValue_acc);
1926          } else {
1927#line 1148
1928            if (nd == 5) {
1929#line 1153
1930              retValue_acc = 5;
1931#line 1155
1932              return (retValue_acc);
1933            } else {
1934#line 1157
1935              if (nd == 6) {
1936#line 1162
1937                retValue_acc = 6;
1938#line 1164
1939                return (retValue_acc);
1940              } else {
1941#line 1166
1942                if (nd == 7) {
1943#line 1171 "Test.c"
1944                  retValue_acc = 7;
1945#line 1173
1946                  return (retValue_acc);
1947                } else {
1948                  {
1949#line 43
1950                  exit(0);
1951                  }
1952                }
1953              }
1954            }
1955          }
1956        }
1957      }
1958    }
1959  }
1960#line 1183 "Test.c"
1961  return (retValue_acc);
1962}
1963}
1964#line 48 "Test.c"
1965void bobCall(void) 
1966{ int tmp ;
1967
1968  {
1969  {
1970#line 48
1971  tmp = getOrigin(0);
1972#line 48
1973  initPersonOnFloor(0, tmp);
1974  }
1975#line 1207 "Test.c"
1976  return;
1977}
1978}
1979#line 50 "Test.c"
1980void aliceCall(void) 
1981{ int tmp ;
1982
1983  {
1984  {
1985#line 50
1986  tmp = getOrigin(1);
1987#line 50
1988  initPersonOnFloor(1, tmp);
1989  }
1990#line 1227 "Test.c"
1991  return;
1992}
1993}
1994#line 52 "Test.c"
1995void angelinaCall(void) 
1996{ int tmp ;
1997
1998  {
1999  {
2000#line 52
2001  tmp = getOrigin(2);
2002#line 52
2003  initPersonOnFloor(2, tmp);
2004  }
2005#line 1247 "Test.c"
2006  return;
2007}
2008}
2009#line 54 "Test.c"
2010void chuckCall(void) 
2011{ int tmp ;
2012
2013  {
2014  {
2015#line 54
2016  tmp = getOrigin(3);
2017#line 54
2018  initPersonOnFloor(3, tmp);
2019  }
2020#line 1267 "Test.c"
2021  return;
2022}
2023}
2024#line 56 "Test.c"
2025void monicaCall(void) 
2026{ int tmp ;
2027
2028  {
2029  {
2030#line 56
2031  tmp = getOrigin(4);
2032#line 56
2033  initPersonOnFloor(4, tmp);
2034  }
2035#line 1287 "Test.c"
2036  return;
2037}
2038}
2039#line 58 "Test.c"
2040void bigMacCall(void) 
2041{ int tmp ;
2042
2043  {
2044  {
2045#line 58
2046  tmp = getOrigin(5);
2047#line 58
2048  initPersonOnFloor(5, tmp);
2049  }
2050#line 1307 "Test.c"
2051  return;
2052}
2053}
2054#line 60 "Test.c"
2055void timeShift(void) ;
2056#line 60 "Test.c"
2057void threeTS(void) 
2058{ 
2059
2060  {
2061  {
2062#line 60
2063  timeShift();
2064#line 60
2065  timeShift();
2066#line 60
2067  timeShift();
2068  }
2069#line 1331 "Test.c"
2070  return;
2071}
2072}
2073#line 71 "Test.c"
2074int isIdle(void) ;
2075#line 67
2076int isBlocked(void) ;
2077#line 62 "Test.c"
2078void cleanup(void) 
2079{ int i ;
2080  int tmp ;
2081  int tmp___0 ;
2082  int __cil_tmp4 ;
2083
2084  {
2085  {
2086#line 65
2087  timeShift();
2088#line 67
2089  i = 0;
2090  }
2091  {
2092#line 67
2093  while (1) {
2094    while_3_continue: /* CIL Label */ ;
2095    {
2096#line 67
2097    __cil_tmp4 = cleanupTimeShifts - 1;
2098#line 67
2099    if (i < __cil_tmp4) {
2100      {
2101#line 67
2102      tmp___0 = isBlocked();
2103      }
2104#line 67
2105      if (tmp___0 != 1) {
2106
2107      } else {
2108        goto while_3_break;
2109      }
2110    } else {
2111      goto while_3_break;
2112    }
2113    }
2114    {
2115#line 71
2116    tmp = isIdle();
2117    }
2118#line 71
2119    if (tmp) {
2120#line 72
2121      return;
2122    } else {
2123      {
2124#line 74
2125      timeShift();
2126      }
2127    }
2128#line 67
2129    i = i + 1;
2130  }
2131  while_3_break: /* CIL Label */ ;
2132  }
2133#line 1362 "Test.c"
2134  return;
2135}
2136}
2137#line 81 "Test.c"
2138void initTopDown(void) ;
2139#line 85
2140void initBottomUp(void) ;
2141#line 77 "Test.c"
2142void randomSequenceOfActions(void) 
2143{ int maxLength ;
2144  int tmp ;
2145  int counter ;
2146  int action ;
2147  int tmp___0 ;
2148  int origin ;
2149  int tmp___1 ;
2150  int tmp___2 ;
2151
2152  {
2153  {
2154#line 78
2155  maxLength = 4;
2156#line 79
2157  tmp = __VERIFIER_nondet_int();
2158  }
2159#line 79
2160  if (tmp) {
2161    {
2162#line 81
2163    initTopDown();
2164    }
2165  } else {
2166    {
2167#line 85
2168    initBottomUp();
2169    }
2170  }
2171#line 90
2172  counter = 0;
2173  {
2174#line 91
2175  while (1) {
2176    while_4_continue: /* CIL Label */ ;
2177#line 91
2178    if (counter < maxLength) {
2179
2180    } else {
2181      goto while_4_break;
2182    }
2183    {
2184#line 92
2185    counter = counter + 1;
2186#line 93
2187    tmp___0 = get_nondetMinMax07();
2188#line 93
2189    action = tmp___0;
2190    }
2191#line 99
2192    if (action < 6) {
2193      {
2194#line 100
2195      tmp___1 = getOrigin(action);
2196#line 100
2197      origin = tmp___1;
2198#line 101
2199      initPersonOnFloor(action, origin);
2200      }
2201    } else {
2202#line 102
2203      if (action == 6) {
2204        {
2205#line 103
2206        timeShift();
2207        }
2208      } else {
2209#line 104
2210        if (action == 7) {
2211          {
2212#line 106
2213          timeShift();
2214#line 107
2215          timeShift();
2216#line 108
2217          timeShift();
2218          }
2219        } else {
2220
2221        }
2222      }
2223    }
2224    {
2225#line 113
2226    tmp___2 = isBlocked();
2227    }
2228#line 113
2229    if (tmp___2) {
2230#line 114
2231      return;
2232    } else {
2233
2234    }
2235  }
2236  while_4_break: /* CIL Label */ ;
2237  }
2238  {
2239#line 117
2240  cleanup();
2241  }
2242#line 1433 "Test.c"
2243  return;
2244}
2245}
2246#line 122 "Test.c"
2247void runTest_Simple(void) 
2248{ 
2249
2250  {
2251  {
2252#line 123
2253  bigMacCall();
2254#line 124
2255  angelinaCall();
2256#line 125
2257  cleanup();
2258  }
2259#line 1457 "Test.c"
2260  return;
2261}
2262}
2263#line 130 "Test.c"
2264void Specification1(void) 
2265{ 
2266
2267  {
2268  {
2269#line 131
2270  bigMacCall();
2271#line 132
2272  angelinaCall();
2273#line 133
2274  cleanup();
2275  }
2276#line 1481 "Test.c"
2277  return;
2278}
2279}
2280#line 137 "Test.c"
2281void Specification2(void) 
2282{ 
2283
2284  {
2285  {
2286#line 138
2287  bigMacCall();
2288#line 139
2289  cleanup();
2290  }
2291#line 1503 "Test.c"
2292  return;
2293}
2294}
2295#line 142 "Test.c"
2296void Specification3(void) 
2297{ 
2298
2299  {
2300  {
2301#line 143
2302  bobCall();
2303#line 144
2304  timeShift();
2305#line 145
2306  timeShift();
2307#line 146
2308  timeShift();
2309#line 147
2310  timeShift();
2311#line 149
2312  timeShift();
2313#line 154
2314  bobCall();
2315#line 155
2316  cleanup();
2317  }
2318#line 1537 "Test.c"
2319  return;
2320}
2321}
2322#line 160 "Test.c"
2323void setup(void) 
2324{ 
2325
2326  {
2327#line 1555 "Test.c"
2328  return;
2329}
2330}
2331#line 1557
2332void __utac_acc__Specification2_spec__1(void) ;
2333#line 1560
2334void __utac_acc__Specification2_spec__4(void) ;
2335#line 165 "Test.c"
2336void runTest(void) 
2337{ 
2338
2339  {
2340  {
2341#line 1571 "Test.c"
2342  __utac_acc__Specification2_spec__1();
2343#line 168 "Test.c"
2344  test();
2345#line 1585 "Test.c"
2346  __utac_acc__Specification2_spec__4();
2347  }
2348#line 1591
2349  return;
2350}
2351}
2352#line 173 "Test.c"
2353int main(void) 
2354{ int retValue_acc ;
2355  int tmp ;
2356
2357  {
2358  {
2359#line 174
2360  select_helpers();
2361#line 175
2362  select_features();
2363#line 176
2364  tmp = valid_product();
2365  }
2366#line 176
2367  if (tmp) {
2368    {
2369#line 177
2370    setup();
2371#line 178
2372    runTest();
2373    }
2374  } else {
2375
2376  }
2377#line 1620 "Test.c"
2378  retValue_acc = 0;
2379#line 1622
2380  return (retValue_acc);
2381#line 1629
2382  return (retValue_acc);
2383}
2384}
2385#line 1 "Elevator.o"
2386#pragma merger(0,"Elevator.i","")
2387#line 359 "/usr/include/stdio.h"
2388extern int printf(char const   * __restrict  __format  , ...) ;
2389#line 16 "Person.h"
2390void enterElevator(int p ) ;
2391#line 18 "Elevator.h"
2392void printState(void) ;
2393#line 20
2394int isEmpty(void) ;
2395#line 22
2396int isAnyLiftButtonPressed(void) ;
2397#line 24
2398int buttonForFloorIsPressed(int floorID ) ;
2399#line 32
2400int areDoorsOpen(void) ;
2401#line 34
2402int getCurrentFloorID(void) ;
2403#line 44 "Elevator.h"
2404int executiveFloor  =    4;
2405#line 47
2406int isExecutiveFloorCalling(void) ;
2407#line 49
2408int isExecutiveFloor(int floorID ) ;
2409#line 18 "Elevator.c"
2410int currentHeading  =    1;
2411#line 20 "Elevator.c"
2412int currentFloorID  =    0;
2413#line 22 "Elevator.c"
2414int persons_0  ;
2415#line 24 "Elevator.c"
2416int persons_1  ;
2417#line 26 "Elevator.c"
2418int persons_2  ;
2419#line 28 "Elevator.c"
2420int persons_3  ;
2421#line 30 "Elevator.c"
2422int persons_4  ;
2423#line 32 "Elevator.c"
2424int persons_5  ;
2425#line 35 "Elevator.c"
2426int doorState  =    1;
2427#line 37 "Elevator.c"
2428int floorButtons_0  ;
2429#line 39 "Elevator.c"
2430int floorButtons_1  ;
2431#line 41 "Elevator.c"
2432int floorButtons_2  ;
2433#line 43 "Elevator.c"
2434int floorButtons_3  ;
2435#line 45 "Elevator.c"
2436int floorButtons_4  ;
2437#line 53 "Elevator.c"
2438void initTopDown(void) 
2439{ 
2440
2441  {
2442  {
2443#line 54
2444  currentFloorID = 4;
2445#line 55
2446  currentHeading = 0;
2447#line 56
2448  floorButtons_0 = 0;
2449#line 57
2450  floorButtons_1 = 0;
2451#line 58
2452  floorButtons_2 = 0;
2453#line 59
2454  floorButtons_3 = 0;
2455#line 60
2456  floorButtons_4 = 0;
2457#line 61
2458  persons_0 = 0;
2459#line 62
2460  persons_1 = 0;
2461#line 63
2462  persons_2 = 0;
2463#line 64
2464  persons_3 = 0;
2465#line 65
2466  persons_4 = 0;
2467#line 66
2468  persons_5 = 0;
2469#line 67
2470  initFloors();
2471  }
2472#line 1077 "Elevator.c"
2473  return;
2474}
2475}
2476#line 70 "Elevator.c"
2477void initBottomUp(void) 
2478{ 
2479
2480  {
2481  {
2482#line 71
2483  currentFloorID = 0;
2484#line 72
2485  currentHeading = 1;
2486#line 73
2487  floorButtons_0 = 0;
2488#line 74
2489  floorButtons_1 = 0;
2490#line 75
2491  floorButtons_2 = 0;
2492#line 76
2493  floorButtons_3 = 0;
2494#line 77
2495  floorButtons_4 = 0;
2496#line 78
2497  persons_0 = 0;
2498#line 79
2499  persons_1 = 0;
2500#line 80
2501  persons_2 = 0;
2502#line 81
2503  persons_3 = 0;
2504#line 82
2505  persons_4 = 0;
2506#line 83
2507  persons_5 = 0;
2508#line 84
2509  initFloors();
2510  }
2511#line 1123 "Elevator.c"
2512  return;
2513}
2514}
2515#line 88 "Elevator.c"
2516int isBlocked(void) 
2517{ int retValue_acc ;
2518
2519  {
2520#line 1141 "Elevator.c"
2521  retValue_acc = 0;
2522#line 1143
2523  return (retValue_acc);
2524#line 1150
2525  return (retValue_acc);
2526}
2527}
2528#line 93 "Elevator.c"
2529void enterElevator(int p ) 
2530{ 
2531
2532  {
2533#line 102
2534  if (p == 0) {
2535#line 103
2536    persons_0 = 1;
2537  } else {
2538#line 104
2539    if (p == 1) {
2540#line 105
2541      persons_1 = 1;
2542    } else {
2543#line 106
2544      if (p == 2) {
2545#line 107
2546        persons_2 = 1;
2547      } else {
2548#line 108
2549        if (p == 3) {
2550#line 109
2551          persons_3 = 1;
2552        } else {
2553#line 110
2554          if (p == 4) {
2555#line 111
2556            persons_4 = 1;
2557          } else {
2558#line 112
2559            if (p == 5) {
2560#line 113
2561              persons_5 = 1;
2562            } else {
2563
2564            }
2565          }
2566        }
2567      }
2568    }
2569  }
2570#line 1185 "Elevator.c"
2571  return;
2572}
2573}
2574#line 104 "Elevator.c"
2575void leaveElevator(int p ) 
2576{ 
2577
2578  {
2579#line 112
2580  if (p == 0) {
2581#line 113
2582    persons_0 = 0;
2583  } else {
2584#line 114
2585    if (p == 1) {
2586#line 115
2587      persons_1 = 0;
2588    } else {
2589#line 116
2590      if (p == 2) {
2591#line 117
2592        persons_2 = 0;
2593      } else {
2594#line 118
2595        if (p == 3) {
2596#line 119
2597          persons_3 = 0;
2598        } else {
2599#line 120
2600          if (p == 4) {
2601#line 121
2602            persons_4 = 0;
2603          } else {
2604#line 122
2605            if (p == 5) {
2606#line 123
2607              persons_5 = 0;
2608            } else {
2609
2610            }
2611          }
2612        }
2613      }
2614    }
2615  }
2616#line 1216 "Elevator.c"
2617  return;
2618}
2619}
2620#line 1218
2621void __utac_acc__Specification2_spec__2(int floor ) ;
2622#line 114 "Elevator.c"
2623void pressInLiftFloorButton(int floorID ) 
2624{ int __utac__ad__arg1 ;
2625
2626  {
2627  {
2628#line 1229 "Elevator.c"
2629  __utac__ad__arg1 = floorID;
2630#line 1230
2631  __utac_acc__Specification2_spec__2(__utac__ad__arg1);
2632  }
2633#line 120
2634  if (floorID == 0) {
2635#line 121
2636    floorButtons_0 = 1;
2637  } else {
2638#line 122
2639    if (floorID == 1) {
2640#line 123
2641      floorButtons_1 = 1;
2642    } else {
2643#line 124
2644      if (floorID == 2) {
2645#line 125
2646        floorButtons_2 = 1;
2647      } else {
2648#line 126
2649        if (floorID == 3) {
2650#line 127
2651          floorButtons_3 = 1;
2652        } else {
2653#line 128
2654          if (floorID == 4) {
2655#line 129 "Elevator.c"
2656            floorButtons_4 = 1;
2657          } else {
2658
2659          }
2660        }
2661      }
2662    }
2663  }
2664#line 1254 "Elevator.c"
2665  return;
2666}
2667}
2668#line 122 "Elevator.c"
2669void resetFloorButton(int floorID ) 
2670{ 
2671
2672  {
2673#line 128
2674  if (floorID == 0) {
2675#line 129
2676    floorButtons_0 = 0;
2677  } else {
2678#line 130
2679    if (floorID == 1) {
2680#line 131
2681      floorButtons_1 = 0;
2682    } else {
2683#line 132
2684      if (floorID == 2) {
2685#line 133
2686        floorButtons_2 = 0;
2687      } else {
2688#line 134
2689        if (floorID == 3) {
2690#line 135
2691          floorButtons_3 = 0;
2692        } else {
2693#line 136
2694          if (floorID == 4) {
2695#line 137
2696            floorButtons_4 = 0;
2697          } else {
2698
2699          }
2700        }
2701      }
2702    }
2703  }
2704#line 1283 "Elevator.c"
2705  return;
2706}
2707}
2708#line 130 "Elevator.c"
2709int getCurrentFloorID(void) 
2710{ int retValue_acc ;
2711
2712  {
2713#line 1301 "Elevator.c"
2714  retValue_acc = currentFloorID;
2715#line 1303
2716  return (retValue_acc);
2717#line 1310
2718  return (retValue_acc);
2719}
2720}
2721#line 134 "Elevator.c"
2722int areDoorsOpen(void) 
2723{ int retValue_acc ;
2724
2725  {
2726#line 1332 "Elevator.c"
2727  retValue_acc = doorState;
2728#line 1334
2729  return (retValue_acc);
2730#line 1341
2731  return (retValue_acc);
2732}
2733}
2734#line 138 "Elevator.c"
2735int buttonForFloorIsPressed(int floorID ) 
2736{ int retValue_acc ;
2737
2738  {
2739#line 144 "Elevator.c"
2740  if (floorID == 0) {
2741#line 1364
2742    retValue_acc = floorButtons_0;
2743#line 1366
2744    return (retValue_acc);
2745  } else {
2746#line 1368
2747    if (floorID == 1) {
2748#line 1371
2749      retValue_acc = floorButtons_1;
2750#line 1373
2751      return (retValue_acc);
2752    } else {
2753#line 1375
2754      if (floorID == 2) {
2755#line 1378
2756        retValue_acc = floorButtons_2;
2757#line 1380
2758        return (retValue_acc);
2759      } else {
2760#line 1382
2761        if (floorID == 3) {
2762#line 1385
2763          retValue_acc = floorButtons_3;
2764#line 1387
2765          return (retValue_acc);
2766        } else {
2767#line 1389
2768          if (floorID == 4) {
2769#line 1392
2770            retValue_acc = floorButtons_4;
2771#line 1394
2772            return (retValue_acc);
2773          } else {
2774#line 1398 "Elevator.c"
2775            retValue_acc = 0;
2776#line 1400
2777            return (retValue_acc);
2778          }
2779        }
2780      }
2781    }
2782  }
2783#line 1407 "Elevator.c"
2784  return (retValue_acc);
2785}
2786}
2787#line 147 "Elevator.c"
2788int getCurrentHeading(void) 
2789{ int retValue_acc ;
2790
2791  {
2792#line 1429 "Elevator.c"
2793  retValue_acc = currentHeading;
2794#line 1431
2795  return (retValue_acc);
2796#line 1438
2797  return (retValue_acc);
2798}
2799}
2800#line 151 "Elevator.c"
2801int isEmpty(void) 
2802{ int retValue_acc ;
2803
2804  {
2805#line 158 "Elevator.c"
2806  if (persons_0 == 1) {
2807#line 1461
2808    retValue_acc = 0;
2809#line 1463
2810    return (retValue_acc);
2811  } else {
2812#line 1465
2813    if (persons_1 == 1) {
2814#line 1468
2815      retValue_acc = 0;
2816#line 1470
2817      return (retValue_acc);
2818    } else {
2819#line 1472
2820      if (persons_2 == 1) {
2821#line 1475
2822        retValue_acc = 0;
2823#line 1477
2824        return (retValue_acc);
2825      } else {
2826#line 1479
2827        if (persons_3 == 1) {
2828#line 1482
2829          retValue_acc = 0;
2830#line 1484
2831          return (retValue_acc);
2832        } else {
2833#line 1486
2834          if (persons_4 == 1) {
2835#line 1489
2836            retValue_acc = 0;
2837#line 1491
2838            return (retValue_acc);
2839          } else {
2840#line 1493
2841            if (persons_5 == 1) {
2842#line 1496 "Elevator.c"
2843              retValue_acc = 0;
2844#line 1498
2845              return (retValue_acc);
2846            } else {
2847
2848            }
2849          }
2850        }
2851      }
2852    }
2853  }
2854#line 1503 "Elevator.c"
2855  retValue_acc = 1;
2856#line 1505
2857  return (retValue_acc);
2858#line 1512
2859  return (retValue_acc);
2860}
2861}
2862#line 162 "Elevator.c"
2863int anyStopRequested(void) 
2864{ int retValue_acc ;
2865  int tmp ;
2866  int tmp___0 ;
2867  int tmp___1 ;
2868  int tmp___2 ;
2869  int tmp___3 ;
2870
2871  {
2872  {
2873#line 173
2874  tmp___3 = isFloorCalling(0);
2875  }
2876#line 173 "Elevator.c"
2877  if (tmp___3) {
2878#line 1535
2879    retValue_acc = 1;
2880#line 1537
2881    return (retValue_acc);
2882  } else {
2883#line 1539
2884    if (floorButtons_0) {
2885#line 1542
2886      retValue_acc = 1;
2887#line 1544
2888      return (retValue_acc);
2889    } else {
2890      {
2891#line 1546 "Elevator.c"
2892      tmp___2 = isFloorCalling(1);
2893      }
2894#line 1546
2895      if (tmp___2) {
2896#line 1549
2897        retValue_acc = 1;
2898#line 1551
2899        return (retValue_acc);
2900      } else {
2901#line 1553
2902        if (floorButtons_1) {
2903#line 1556
2904          retValue_acc = 1;
2905#line 1558
2906          return (retValue_acc);
2907        } else {
2908          {
2909#line 1560
2910          tmp___1 = isFloorCalling(2);
2911          }
2912#line 1560
2913          if (tmp___1) {
2914#line 1563
2915            retValue_acc = 1;
2916#line 1565
2917            return (retValue_acc);
2918          } else {
2919#line 1567
2920            if (floorButtons_2) {
2921#line 1570
2922              retValue_acc = 1;
2923#line 1572
2924              return (retValue_acc);
2925            } else {
2926              {
2927#line 1574
2928              tmp___0 = isFloorCalling(3);
2929              }
2930#line 1574
2931              if (tmp___0) {
2932#line 1577
2933                retValue_acc = 1;
2934#line 1579
2935                return (retValue_acc);
2936              } else {
2937#line 1581
2938                if (floorButtons_3) {
2939#line 1584
2940                  retValue_acc = 1;
2941#line 1586
2942                  return (retValue_acc);
2943                } else {
2944                  {
2945#line 1588
2946                  tmp = isFloorCalling(4);
2947                  }
2948#line 1588
2949                  if (tmp) {
2950#line 1591
2951                    retValue_acc = 1;
2952#line 1593
2953                    return (retValue_acc);
2954                  } else {
2955#line 1595
2956                    if (floorButtons_4) {
2957#line 1598
2958                      retValue_acc = 1;
2959#line 1600
2960                      return (retValue_acc);
2961                    } else {
2962
2963                    }
2964                  }
2965                }
2966              }
2967            }
2968          }
2969        }
2970      }
2971    }
2972  }
2973#line 1605 "Elevator.c"
2974  retValue_acc = 0;
2975#line 1607
2976  return (retValue_acc);
2977#line 1614
2978  return (retValue_acc);
2979}
2980}
2981#line 176 "Elevator.c"
2982int isIdle(void) 
2983{ int retValue_acc ;
2984  int tmp ;
2985
2986  {
2987  {
2988#line 1636 "Elevator.c"
2989  tmp = anyStopRequested();
2990#line 1636
2991  retValue_acc = tmp == 0;
2992  }
2993#line 1638
2994  return (retValue_acc);
2995#line 1645
2996  return (retValue_acc);
2997}
2998}
2999#line 180 "Elevator.c"
3000int stopRequestedInDirection__wrappee__base(int dir , int respectFloorCalls , int respectInLiftCalls ) 
3001{ int retValue_acc ;
3002  int tmp ;
3003  int tmp___0 ;
3004  int tmp___1 ;
3005  int tmp___2 ;
3006  int tmp___3 ;
3007  int tmp___4 ;
3008  int tmp___5 ;
3009  int tmp___6 ;
3010  int tmp___7 ;
3011  int tmp___8 ;
3012  int tmp___9 ;
3013
3014  {
3015#line 231
3016  if (dir == 1) {
3017    {
3018#line 191
3019    tmp = isTopFloor(currentFloorID);
3020    }
3021#line 191 "Elevator.c"
3022    if (tmp) {
3023#line 1671 "Elevator.c"
3024      retValue_acc = 0;
3025#line 1673
3026      return (retValue_acc);
3027    } else {
3028
3029    }
3030#line 191
3031    if (currentFloorID < 0) {
3032#line 191
3033      if (respectFloorCalls) {
3034        {
3035#line 191 "Elevator.c"
3036        tmp___4 = isFloorCalling(0);
3037        }
3038#line 191 "Elevator.c"
3039        if (tmp___4) {
3040#line 1679 "Elevator.c"
3041          retValue_acc = 1;
3042#line 1681
3043          return (retValue_acc);
3044        } else {
3045          goto _L___16;
3046        }
3047      } else {
3048        goto _L___16;
3049      }
3050    } else {
3051      _L___16: /* CIL Label */ 
3052#line 1683
3053      if (currentFloorID < 0) {
3054#line 1683
3055        if (respectInLiftCalls) {
3056#line 1683
3057          if (floorButtons_0) {
3058#line 1686
3059            retValue_acc = 1;
3060#line 1688
3061            return (retValue_acc);
3062          } else {
3063            goto _L___14;
3064          }
3065        } else {
3066          goto _L___14;
3067        }
3068      } else {
3069        _L___14: /* CIL Label */ 
3070#line 1690
3071        if (currentFloorID < 1) {
3072#line 1690
3073          if (respectFloorCalls) {
3074            {
3075#line 1690
3076            tmp___3 = isFloorCalling(1);
3077            }
3078#line 1690
3079            if (tmp___3) {
3080#line 1693
3081              retValue_acc = 1;
3082#line 1695
3083              return (retValue_acc);
3084            } else {
3085              goto _L___12;
3086            }
3087          } else {
3088            goto _L___12;
3089          }
3090        } else {
3091          _L___12: /* CIL Label */ 
3092#line 1697
3093          if (currentFloorID < 1) {
3094#line 1697
3095            if (respectInLiftCalls) {
3096#line 1697
3097              if (floorButtons_1) {
3098#line 1700
3099                retValue_acc = 1;
3100#line 1702
3101                return (retValue_acc);
3102              } else {
3103                goto _L___10;
3104              }
3105            } else {
3106              goto _L___10;
3107            }
3108          } else {
3109            _L___10: /* CIL Label */ 
3110#line 1704
3111            if (currentFloorID < 2) {
3112#line 1704
3113              if (respectFloorCalls) {
3114                {
3115#line 1704
3116                tmp___2 = isFloorCalling(2);
3117                }
3118#line 1704
3119                if (tmp___2) {
3120#line 1707
3121                  retValue_acc = 1;
3122#line 1709
3123                  return (retValue_acc);
3124                } else {
3125                  goto _L___8;
3126                }
3127              } else {
3128                goto _L___8;
3129              }
3130            } else {
3131              _L___8: /* CIL Label */ 
3132#line 1711
3133              if (currentFloorID < 2) {
3134#line 1711
3135                if (respectInLiftCalls) {
3136#line 1711
3137                  if (floorButtons_2) {
3138#line 1714
3139                    retValue_acc = 1;
3140#line 1716
3141                    return (retValue_acc);
3142                  } else {
3143                    goto _L___6;
3144                  }
3145                } else {
3146                  goto _L___6;
3147                }
3148              } else {
3149                _L___6: /* CIL Label */ 
3150#line 1718
3151                if (currentFloorID < 3) {
3152#line 1718
3153                  if (respectFloorCalls) {
3154                    {
3155#line 1718
3156                    tmp___1 = isFloorCalling(3);
3157                    }
3158#line 1718
3159                    if (tmp___1) {
3160#line 1721
3161                      retValue_acc = 1;
3162#line 1723
3163                      return (retValue_acc);
3164                    } else {
3165                      goto _L___4;
3166                    }
3167                  } else {
3168                    goto _L___4;
3169                  }
3170                } else {
3171                  _L___4: /* CIL Label */ 
3172#line 1725
3173                  if (currentFloorID < 3) {
3174#line 1725
3175                    if (respectInLiftCalls) {
3176#line 1725
3177                      if (floorButtons_3) {
3178#line 1728
3179                        retValue_acc = 1;
3180#line 1730
3181                        return (retValue_acc);
3182                      } else {
3183                        goto _L___2;
3184                      }
3185                    } else {
3186                      goto _L___2;
3187                    }
3188                  } else {
3189                    _L___2: /* CIL Label */ 
3190#line 1732
3191                    if (currentFloorID < 4) {
3192#line 1732
3193                      if (respectFloorCalls) {
3194                        {
3195#line 1732
3196                        tmp___0 = isFloorCalling(4);
3197                        }
3198#line 1732
3199                        if (tmp___0) {
3200#line 1735
3201                          retValue_acc = 1;
3202#line 1737
3203                          return (retValue_acc);
3204                        } else {
3205                          goto _L___0;
3206                        }
3207                      } else {
3208                        goto _L___0;
3209                      }
3210                    } else {
3211                      _L___0: /* CIL Label */ 
3212#line 1739
3213                      if (currentFloorID < 4) {
3214#line 1739
3215                        if (respectInLiftCalls) {
3216#line 1739
3217                          if (floorButtons_4) {
3218#line 1742
3219                            retValue_acc = 1;
3220#line 1744
3221                            return (retValue_acc);
3222                          } else {
3223#line 1748
3224                            retValue_acc = 0;
3225#line 1750
3226                            return (retValue_acc);
3227                          }
3228                        } else {
3229#line 1748
3230                          retValue_acc = 0;
3231#line 1750
3232                          return (retValue_acc);
3233                        }
3234                      } else {
3235#line 1748 "Elevator.c"
3236                        retValue_acc = 0;
3237#line 1750
3238                        return (retValue_acc);
3239                      }
3240                    }
3241                  }
3242                }
3243              }
3244            }
3245          }
3246        }
3247      }
3248    }
3249  } else {
3250#line 216 "Elevator.c"
3251    if (currentFloorID == 0) {
3252#line 1758 "Elevator.c"
3253      retValue_acc = 0;
3254#line 1760
3255      return (retValue_acc);
3256    } else {
3257
3258    }
3259#line 216
3260    if (currentFloorID > 0) {
3261#line 216
3262      if (respectFloorCalls) {
3263        {
3264#line 216 "Elevator.c"
3265        tmp___9 = isFloorCalling(0);
3266        }
3267#line 216 "Elevator.c"
3268        if (tmp___9) {
3269#line 1766 "Elevator.c"
3270          retValue_acc = 1;
3271#line 1768
3272          return (retValue_acc);
3273        } else {
3274          goto _L___34;
3275        }
3276      } else {
3277        goto _L___34;
3278      }
3279    } else {
3280      _L___34: /* CIL Label */ 
3281#line 1770
3282      if (currentFloorID > 0) {
3283#line 1770
3284        if (respectInLiftCalls) {
3285#line 1770
3286          if (floorButtons_0) {
3287#line 1773
3288            retValue_acc = 1;
3289#line 1775
3290            return (retValue_acc);
3291          } else {
3292            goto _L___32;
3293          }
3294        } else {
3295          goto _L___32;
3296        }
3297      } else {
3298        _L___32: /* CIL Label */ 
3299#line 1777
3300        if (currentFloorID > 1) {
3301#line 1777
3302          if (respectFloorCalls) {
3303            {
3304#line 1777
3305            tmp___8 = isFloorCalling(1);
3306            }
3307#line 1777
3308            if (tmp___8) {
3309#line 1780
3310              retValue_acc = 1;
3311#line 1782
3312              return (retValue_acc);
3313            } else {
3314              goto _L___30;
3315            }
3316          } else {
3317            goto _L___30;
3318          }
3319        } else {
3320          _L___30: /* CIL Label */ 
3321#line 1784
3322          if (currentFloorID > 1) {
3323#line 1784
3324            if (respectInLiftCalls) {
3325#line 1784
3326              if (floorButtons_1) {
3327#line 1787
3328                retValue_acc = 1;
3329#line 1789
3330                return (retValue_acc);
3331              } else {
3332                goto _L___28;
3333              }
3334            } else {
3335              goto _L___28;
3336            }
3337          } else {
3338            _L___28: /* CIL Label */ 
3339#line 1791
3340            if (currentFloorID > 2) {
3341#line 1791
3342              if (respectFloorCalls) {
3343                {
3344#line 1791
3345                tmp___7 = isFloorCalling(2);
3346                }
3347#line 1791
3348                if (tmp___7) {
3349#line 1794
3350                  retValue_acc = 1;
3351#line 1796
3352                  return (retValue_acc);
3353                } else {
3354                  goto _L___26;
3355                }
3356              } else {
3357                goto _L___26;
3358              }
3359            } else {
3360              _L___26: /* CIL Label */ 
3361#line 1798
3362              if (currentFloorID > 2) {
3363#line 1798
3364                if (respectInLiftCalls) {
3365#line 1798
3366                  if (floorButtons_2) {
3367#line 1801
3368                    retValue_acc = 1;
3369#line 1803
3370                    return (retValue_acc);
3371                  } else {
3372                    goto _L___24;
3373                  }
3374                } else {
3375                  goto _L___24;
3376                }
3377              } else {
3378                _L___24: /* CIL Label */ 
3379#line 1805
3380                if (currentFloorID > 3) {
3381#line 1805
3382                  if (respectFloorCalls) {
3383                    {
3384#line 1805
3385                    tmp___6 = isFloorCalling(3);
3386                    }
3387#line 1805
3388                    if (tmp___6) {
3389#line 1808
3390                      retValue_acc = 1;
3391#line 1810
3392                      return (retValue_acc);
3393                    } else {
3394                      goto _L___22;
3395                    }
3396                  } else {
3397                    goto _L___22;
3398                  }
3399                } else {
3400                  _L___22: /* CIL Label */ 
3401#line 1812
3402                  if (currentFloorID > 3) {
3403#line 1812
3404                    if (respectInLiftCalls) {
3405#line 1812
3406                      if (floorButtons_3) {
3407#line 1815
3408                        retValue_acc = 1;
3409#line 1817
3410                        return (retValue_acc);
3411                      } else {
3412                        goto _L___20;
3413                      }
3414                    } else {
3415                      goto _L___20;
3416                    }
3417                  } else {
3418                    _L___20: /* CIL Label */ 
3419#line 1819
3420                    if (currentFloorID > 4) {
3421#line 1819
3422                      if (respectFloorCalls) {
3423                        {
3424#line 1819
3425                        tmp___5 = isFloorCalling(4);
3426                        }
3427#line 1819
3428                        if (tmp___5) {
3429#line 1822
3430                          retValue_acc = 1;
3431#line 1824
3432                          return (retValue_acc);
3433                        } else {
3434                          goto _L___18;
3435                        }
3436                      } else {
3437                        goto _L___18;
3438                      }
3439                    } else {
3440                      _L___18: /* CIL Label */ 
3441#line 1826
3442                      if (currentFloorID > 4) {
3443#line 1826
3444                        if (respectInLiftCalls) {
3445#line 1826
3446                          if (floorButtons_4) {
3447#line 1829
3448                            retValue_acc = 1;
3449#line 1831
3450                            return (retValue_acc);
3451                          } else {
3452#line 1835
3453                            retValue_acc = 0;
3454#line 1837
3455                            return (retValue_acc);
3456                          }
3457                        } else {
3458#line 1835
3459                          retValue_acc = 0;
3460#line 1837
3461                          return (retValue_acc);
3462                        }
3463                      } else {
3464#line 1835 "Elevator.c"
3465                        retValue_acc = 0;
3466#line 1837
3467                        return (retValue_acc);
3468                      }
3469                    }
3470                  }
3471                }
3472              }
3473            }
3474          }
3475        }
3476      }
3477    }
3478  }
3479#line 1844 "Elevator.c"
3480  return (retValue_acc);
3481}
3482}
3483#line 235 "Elevator.c"
3484int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls ) 
3485{ int retValue_acc ;
3486  int tmp ;
3487  int tmp___0 ;
3488  int __cil_tmp7 ;
3489  int __cil_tmp8 ;
3490
3491  {
3492  {
3493#line 240
3494  tmp___0 = isExecutiveFloorCalling();
3495  }
3496#line 240 "Elevator.c"
3497  if (tmp___0) {
3498    {
3499#line 1869
3500    tmp = getCurrentFloorID();
3501#line 1869
3502    __cil_tmp7 = dir == 1;
3503#line 1869
3504    __cil_tmp8 = tmp < executiveFloor;
3505#line 1869
3506    retValue_acc = __cil_tmp8 == __cil_tmp7;
3507    }
3508#line 1871
3509    return (retValue_acc);
3510  } else {
3511    {
3512#line 1877 "Elevator.c"
3513    retValue_acc = stopRequestedInDirection__wrappee__base(dir, respectFloorCalls,
3514                                                           respectInLiftCalls);
3515    }
3516#line 1879
3517    return (retValue_acc);
3518  }
3519#line 1886 "Elevator.c"
3520  return (retValue_acc);
3521}
3522}
3523#line 243 "Elevator.c"
3524int isAnyLiftButtonPressed(void) 
3525{ int retValue_acc ;
3526
3527  {
3528#line 249 "Elevator.c"
3529  if (floorButtons_0) {
3530#line 1909
3531    retValue_acc = 1;
3532#line 1911
3533    return (retValue_acc);
3534  } else {
3535#line 1913
3536    if (floorButtons_1) {
3537#line 1916
3538      retValue_acc = 1;
3539#line 1918
3540      return (retValue_acc);
3541    } else {
3542#line 1920
3543      if (floorButtons_2) {
3544#line 1923
3545        retValue_acc = 1;
3546#line 1925
3547        return (retValue_acc);
3548      } else {
3549#line 1927
3550        if (floorButtons_3) {
3551#line 1930
3552          retValue_acc = 1;
3553#line 1932
3554          return (retValue_acc);
3555        } else {
3556#line 1934
3557          if (floorButtons_4) {
3558#line 1937
3559            retValue_acc = 1;
3560#line 1939
3561            return (retValue_acc);
3562          } else {
3563#line 1943 "Elevator.c"
3564            retValue_acc = 0;
3565#line 1945
3566            return (retValue_acc);
3567          }
3568        }
3569      }
3570    }
3571  }
3572#line 1952 "Elevator.c"
3573  return (retValue_acc);
3574}
3575}
3576#line 252 "Elevator.c"
3577void continueInDirection(int dir ) 
3578{ int tmp ;
3579
3580  {
3581#line 253
3582  currentHeading = dir;
3583#line 254
3584  if (currentHeading == 1) {
3585    {
3586#line 259
3587    tmp = isTopFloor(currentFloorID);
3588    }
3589#line 259
3590    if (tmp) {
3591#line 257
3592      currentHeading = 0;
3593    } else {
3594
3595    }
3596  } else {
3597#line 264
3598    if (currentFloorID == 0) {
3599#line 262
3600      currentHeading = 1;
3601    } else {
3602
3603    }
3604  }
3605#line 265
3606  if (currentHeading == 1) {
3607#line 266
3608    currentFloorID = currentFloorID + 1;
3609  } else {
3610#line 268
3611    currentFloorID = currentFloorID - 1;
3612  }
3613#line 1998 "Elevator.c"
3614  return;
3615}
3616}
3617#line 272 "Elevator.c"
3618int stopRequestedAtCurrentFloor__wrappee__base(void) 
3619{ int retValue_acc ;
3620  int tmp ;
3621  int tmp___0 ;
3622
3623  {
3624  {
3625#line 279
3626  tmp___0 = isFloorCalling(currentFloorID);
3627  }
3628#line 279 "Elevator.c"
3629  if (tmp___0) {
3630#line 2019
3631    retValue_acc = 1;
3632#line 2021
3633    return (retValue_acc);
3634  } else {
3635    {
3636#line 2023 "Elevator.c"
3637    tmp = buttonForFloorIsPressed(currentFloorID);
3638    }
3639#line 2023
3640    if (tmp) {
3641#line 2028
3642      retValue_acc = 1;
3643#line 2030
3644      return (retValue_acc);
3645    } else {
3646#line 2036
3647      retValue_acc = 0;
3648#line 2038
3649      return (retValue_acc);
3650    }
3651  }
3652#line 2045 "Elevator.c"
3653  return (retValue_acc);
3654}
3655}
3656#line 283 "Elevator.c"
3657int stopRequestedAtCurrentFloor(void) 
3658{ int retValue_acc ;
3659  int tmp ;
3660  int tmp___0 ;
3661
3662  {
3663  {
3664#line 286
3665  tmp = isExecutiveFloorCalling();
3666  }
3667#line 286
3668  if (tmp) {
3669    {
3670#line 286 "Elevator.c"
3671    tmp___0 = getCurrentFloorID();
3672    }
3673#line 286 "Elevator.c"
3674    if (executiveFloor == tmp___0) {
3675      {
3676#line 2076
3677      retValue_acc = stopRequestedAtCurrentFloor__wrappee__base();
3678      }
3679#line 2078
3680      return (retValue_acc);
3681    } else {
3682#line 2070 "Elevator.c"
3683      retValue_acc = 0;
3684#line 2072
3685      return (retValue_acc);
3686    }
3687  } else {
3688    {
3689#line 2076 "Elevator.c"
3690    retValue_acc = stopRequestedAtCurrentFloor__wrappee__base();
3691    }
3692#line 2078
3693    return (retValue_acc);
3694  }
3695#line 2085 "Elevator.c"
3696  return (retValue_acc);
3697}
3698}
3699#line 289 "Elevator.c"
3700int getReverseHeading(int ofHeading ) 
3701{ int retValue_acc ;
3702
3703  {
3704#line 292 "Elevator.c"
3705  if (ofHeading == 0) {
3706#line 2110
3707    retValue_acc = 1;
3708#line 2112
3709    return (retValue_acc);
3710  } else {
3711#line 2116 "Elevator.c"
3712    retValue_acc = 0;
3713#line 2118
3714    return (retValue_acc);
3715  }
3716#line 2125 "Elevator.c"
3717  return (retValue_acc);
3718}
3719}
3720#line 296 "Elevator.c"
3721void processWaitingOnFloor(int floorID ) 
3722{ int tmp ;
3723  int tmp___0 ;
3724  int tmp___1 ;
3725  int tmp___2 ;
3726  int tmp___3 ;
3727  int tmp___4 ;
3728  int tmp___5 ;
3729  int tmp___6 ;
3730  int tmp___7 ;
3731  int tmp___8 ;
3732  int tmp___9 ;
3733  int tmp___10 ;
3734
3735  {
3736  {
3737#line 302
3738  tmp___0 = isPersonOnFloor(0, floorID);
3739  }
3740#line 302
3741  if (tmp___0) {
3742    {
3743#line 298
3744    removePersonFromFloor(0, floorID);
3745#line 299
3746    tmp = getDestination(0);
3747#line 299
3748    pressInLiftFloorButton(tmp);
3749#line 300
3750    enterElevator(0);
3751    }
3752  } else {
3753
3754  }
3755  {
3756#line 302
3757  tmp___2 = isPersonOnFloor(1, floorID);
3758  }
3759#line 302
3760  if (tmp___2) {
3761    {
3762#line 303
3763    removePersonFromFloor(1, floorID);
3764#line 304
3765    tmp___1 = getDestination(1);
3766#line 304
3767    pressInLiftFloorButton(tmp___1);
3768#line 305
3769    enterElevator(1);
3770    }
3771  } else {
3772
3773  }
3774  {
3775#line 307
3776  tmp___4 = isPersonOnFloor(2, floorID);
3777  }
3778#line 307
3779  if (tmp___4) {
3780    {
3781#line 308
3782    removePersonFromFloor(2, floorID);
3783#line 309
3784    tmp___3 = getDestination(2);
3785#line 309
3786    pressInLiftFloorButton(tmp___3);
3787#line 310
3788    enterElevator(2);
3789    }
3790  } else {
3791
3792  }
3793  {
3794#line 312
3795  tmp___6 = isPersonOnFloor(3, floorID);
3796  }
3797#line 312
3798  if (tmp___6) {
3799    {
3800#line 313
3801    removePersonFromFloor(3, floorID);
3802#line 314
3803    tmp___5 = getDestination(3);
3804#line 314
3805    pressInLiftFloorButton(tmp___5);
3806#line 315
3807    enterElevator(3);
3808    }
3809  } else {
3810
3811  }
3812  {
3813#line 317
3814  tmp___8 = isPersonOnFloor(4, floorID);
3815  }
3816#line 317
3817  if (tmp___8) {
3818    {
3819#line 318
3820    removePersonFromFloor(4, floorID);
3821#line 319
3822    tmp___7 = getDestination(4);
3823#line 319
3824    pressInLiftFloorButton(tmp___7);
3825#line 320
3826    enterElevator(4);
3827    }
3828  } else {
3829
3830  }
3831  {
3832#line 322
3833  tmp___10 = isPersonOnFloor(5, floorID);
3834  }
3835#line 322
3836  if (tmp___10) {
3837    {
3838#line 323
3839    removePersonFromFloor(5, floorID);
3840#line 324
3841    tmp___9 = getDestination(5);
3842#line 324
3843    pressInLiftFloorButton(tmp___9);
3844#line 325
3845    enterElevator(5);
3846    }
3847  } else {
3848
3849  }
3850  {
3851#line 327
3852  resetCallOnFloor(floorID);
3853  }
3854#line 2203 "Elevator.c"
3855  return;
3856}
3857}
3858#line 2205
3859void __utac_acc__Specification2_spec__3(void) ;
3860#line 331 "Elevator.c"
3861void timeShift(void) 
3862{ int tmp ;
3863  int tmp___0 ;
3864  int tmp___1 ;
3865  int tmp___2 ;
3866  int tmp___3 ;
3867  int tmp___4 ;
3868  int tmp___5 ;
3869  int tmp___6 ;
3870  int tmp___7 ;
3871  int tmp___8 ;
3872  int tmp___9 ;
3873
3874  {
3875  {
3876#line 364
3877  tmp___9 = stopRequestedAtCurrentFloor();
3878  }
3879#line 364
3880  if (tmp___9) {
3881#line 336
3882    doorState = 1;
3883#line 338
3884    if (persons_0) {
3885      {
3886#line 338
3887      tmp = getDestination(0);
3888      }
3889#line 338
3890      if (tmp == currentFloorID) {
3891        {
3892#line 339
3893        leaveElevator(0);
3894        }
3895      } else {
3896
3897      }
3898    } else {
3899
3900    }
3901#line 339
3902    if (persons_1) {
3903      {
3904#line 339
3905      tmp___0 = getDestination(1);
3906      }
3907#line 339
3908      if (tmp___0 == currentFloorID) {
3909        {
3910#line 340
3911        leaveElevator(1);
3912        }
3913      } else {
3914
3915      }
3916    } else {
3917
3918    }
3919#line 340
3920    if (persons_2) {
3921      {
3922#line 340
3923      tmp___1 = getDestination(2);
3924      }
3925#line 340
3926      if (tmp___1 == currentFloorID) {
3927        {
3928#line 341
3929        leaveElevator(2);
3930        }
3931      } else {
3932
3933      }
3934    } else {
3935
3936    }
3937#line 341
3938    if (persons_3) {
3939      {
3940#line 341
3941      tmp___2 = getDestination(3);
3942      }
3943#line 341
3944      if (tmp___2 == currentFloorID) {
3945        {
3946#line 342
3947        leaveElevator(3);
3948        }
3949      } else {
3950
3951      }
3952    } else {
3953
3954    }
3955#line 342
3956    if (persons_4) {
3957      {
3958#line 342
3959      tmp___3 = getDestination(4);
3960      }
3961#line 342
3962      if (tmp___3 == currentFloorID) {
3963        {
3964#line 343
3965        leaveElevator(4);
3966        }
3967      } else {
3968
3969      }
3970    } else {
3971
3972    }
3973#line 343
3974    if (persons_5) {
3975      {
3976#line 343
3977      tmp___4 = getDestination(5);
3978      }
3979#line 343
3980      if (tmp___4 == currentFloorID) {
3981        {
3982#line 344
3983        leaveElevator(5);
3984        }
3985      } else {
3986
3987      }
3988    } else {
3989
3990    }
3991    {
3992#line 344
3993    processWaitingOnFloor(currentFloorID);
3994#line 345
3995    resetFloorButton(currentFloorID);
3996    }
3997  } else {
3998#line 351
3999    if (doorState == 1) {
4000#line 348
4001      doorState = 0;
4002    } else {
4003
4004    }
4005    {
4006#line 351
4007    tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
4008    }
4009#line 351
4010    if (tmp___8) {
4011      {
4012#line 354
4013      continueInDirection(currentHeading);
4014      }
4015    } else {
4016      {
4017#line 355
4018      tmp___6 = getReverseHeading(currentHeading);
4019#line 355
4020      tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
4021      }
4022#line 355
4023      if (tmp___7) {
4024        {
4025#line 358
4026        tmp___5 = getReverseHeading(currentHeading);
4027#line 358
4028        continueInDirection(tmp___5);
4029        }
4030      } else {
4031        {
4032#line 362
4033        continueInDirection(currentHeading);
4034        }
4035      }
4036    }
4037  }
4038  {
4039#line 2268 "Elevator.c"
4040  __utac_acc__Specification2_spec__3();
4041  }
4042#line 2274
4043  return;
4044}
4045}
4046#line 367 "Elevator.c"
4047void printState(void) 
4048{ int tmp ;
4049  int tmp___0 ;
4050  int tmp___1 ;
4051  int tmp___2 ;
4052  int tmp___3 ;
4053  char const   * __restrict  __cil_tmp6 ;
4054  char const   * __restrict  __cil_tmp7 ;
4055  char const   * __restrict  __cil_tmp8 ;
4056  char const   * __restrict  __cil_tmp9 ;
4057  char const   * __restrict  __cil_tmp10 ;
4058  char const   * __restrict  __cil_tmp11 ;
4059  char const   * __restrict  __cil_tmp12 ;
4060  char const   * __restrict  __cil_tmp13 ;
4061  char const   * __restrict  __cil_tmp14 ;
4062  char const   * __restrict  __cil_tmp15 ;
4063  char const   * __restrict  __cil_tmp16 ;
4064  char const   * __restrict  __cil_tmp17 ;
4065  char const   * __restrict  __cil_tmp18 ;
4066  char const   * __restrict  __cil_tmp19 ;
4067  char const   * __restrict  __cil_tmp20 ;
4068  char const   * __restrict  __cil_tmp21 ;
4069  char const   * __restrict  __cil_tmp22 ;
4070  char const   * __restrict  __cil_tmp23 ;
4071  char const   * __restrict  __cil_tmp24 ;
4072  char const   * __restrict  __cil_tmp25 ;
4073  char const   * __restrict  __cil_tmp26 ;
4074
4075  {
4076  {
4077#line 368
4078  __cil_tmp6 = (char const   * __restrict  )"Elevator ";
4079#line 368
4080  printf(__cil_tmp6);
4081  }
4082#line 369
4083  if (doorState) {
4084    {
4085#line 370
4086    __cil_tmp7 = (char const   * __restrict  )"[_]";
4087#line 370
4088    printf(__cil_tmp7);
4089    }
4090  } else {
4091    {
4092#line 371
4093    __cil_tmp8 = (char const   * __restrict  )"[] ";
4094#line 371
4095    printf(__cil_tmp8);
4096    }
4097  }
4098  {
4099#line 371
4100  __cil_tmp9 = (char const   * __restrict  )" at ";
4101#line 371
4102  printf(__cil_tmp9);
4103#line 372
4104  __cil_tmp10 = (char const   * __restrict  )"%i";
4105#line 372
4106  printf(__cil_tmp10, currentFloorID);
4107#line 373
4108  __cil_tmp11 = (char const   * __restrict  )" heading ";
4109#line 373
4110  printf(__cil_tmp11);
4111  }
4112#line 374
4113  if (currentHeading) {
4114    {
4115#line 375
4116    __cil_tmp12 = (char const   * __restrict  )"up";
4117#line 375
4118    printf(__cil_tmp12);
4119    }
4120  } else {
4121    {
4122#line 376
4123    __cil_tmp13 = (char const   * __restrict  )"down";
4124#line 376
4125    printf(__cil_tmp13);
4126    }
4127  }
4128  {
4129#line 376
4130  __cil_tmp14 = (char const   * __restrict  )" IL_p:";
4131#line 376
4132  printf(__cil_tmp14);
4133  }
4134#line 377
4135  if (floorButtons_0) {
4136    {
4137#line 378
4138    __cil_tmp15 = (char const   * __restrict  )" %i";
4139#line 378
4140    printf(__cil_tmp15, 0);
4141    }
4142  } else {
4143
4144  }
4145#line 378
4146  if (floorButtons_1) {
4147    {
4148#line 379
4149    __cil_tmp16 = (char const   * __restrict  )" %i";
4150#line 379
4151    printf(__cil_tmp16, 1);
4152    }
4153  } else {
4154
4155  }
4156#line 379
4157  if (floorButtons_2) {
4158    {
4159#line 380
4160    __cil_tmp17 = (char const   * __restrict  )" %i";
4161#line 380
4162    printf(__cil_tmp17, 2);
4163    }
4164  } else {
4165
4166  }
4167#line 380
4168  if (floorButtons_3) {
4169    {
4170#line 381
4171    __cil_tmp18 = (char const   * __restrict  )" %i";
4172#line 381
4173    printf(__cil_tmp18, 3);
4174    }
4175  } else {
4176
4177  }
4178#line 381
4179  if (floorButtons_4) {
4180    {
4181#line 382
4182    __cil_tmp19 = (char const   * __restrict  )" %i";
4183#line 382
4184    printf(__cil_tmp19, 4);
4185    }
4186  } else {
4187
4188  }
4189  {
4190#line 382
4191  __cil_tmp20 = (char const   * __restrict  )" F_p:";
4192#line 382
4193  printf(__cil_tmp20);
4194#line 383
4195  tmp = isFloorCalling(0);
4196  }
4197#line 383
4198  if (tmp) {
4199    {
4200#line 384
4201    __cil_tmp21 = (char const   * __restrict  )" %i";
4202#line 384
4203    printf(__cil_tmp21, 0);
4204    }
4205  } else {
4206
4207  }
4208  {
4209#line 384
4210  tmp___0 = isFloorCalling(1);
4211  }
4212#line 384
4213  if (tmp___0) {
4214    {
4215#line 385
4216    __cil_tmp22 = (char const   * __restrict  )" %i";
4217#line 385
4218    printf(__cil_tmp22, 1);
4219    }
4220  } else {
4221
4222  }
4223  {
4224#line 385
4225  tmp___1 = isFloorCalling(2);
4226  }
4227#line 385
4228  if (tmp___1) {
4229    {
4230#line 386
4231    __cil_tmp23 = (char const   * __restrict  )" %i";
4232#line 386
4233    printf(__cil_tmp23, 2);
4234    }
4235  } else {
4236
4237  }
4238  {
4239#line 386
4240  tmp___2 = isFloorCalling(3);
4241  }
4242#line 386
4243  if (tmp___2) {
4244    {
4245#line 387
4246    __cil_tmp24 = (char const   * __restrict  )" %i";
4247#line 387
4248    printf(__cil_tmp24, 3);
4249    }
4250  } else {
4251
4252  }
4253  {
4254#line 387
4255  tmp___3 = isFloorCalling(4);
4256  }
4257#line 387
4258  if (tmp___3) {
4259    {
4260#line 388
4261    __cil_tmp25 = (char const   * __restrict  )" %i";
4262#line 388
4263    printf(__cil_tmp25, 4);
4264    }
4265  } else {
4266
4267  }
4268  {
4269#line 388
4270  __cil_tmp26 = (char const   * __restrict  )"\n";
4271#line 388
4272  printf(__cil_tmp26);
4273  }
4274#line 2344 "Elevator.c"
4275  return;
4276}
4277}
4278#line 392 "Elevator.c"
4279int existInLiftCallsInDirection(int d ) 
4280{ int retValue_acc ;
4281  int i ;
4282  int i___0 ;
4283
4284  {
4285#line 413
4286  if (d == 1) {
4287#line 394 "Elevator.c"
4288    i = 0;
4289#line 395
4290    i = currentFloorID + 1;
4291    {
4292#line 395
4293    while (1) {
4294      while_5_continue: /* CIL Label */ ;
4295#line 395
4296      if (i < 5) {
4297
4298      } else {
4299        goto while_5_break;
4300      }
4301#line 401
4302      if (i == 0) {
4303#line 401 "Elevator.c"
4304        if (floorButtons_0) {
4305#line 2372
4306          retValue_acc = 1;
4307#line 2374
4308          return (retValue_acc);
4309        } else {
4310          goto _L___2;
4311        }
4312      } else {
4313        _L___2: /* CIL Label */ 
4314#line 2376
4315        if (i == 1) {
4316#line 2376
4317          if (floorButtons_1) {
4318#line 2379
4319            retValue_acc = 1;
4320#line 2381
4321            return (retValue_acc);
4322          } else {
4323            goto _L___1;
4324          }
4325        } else {
4326          _L___1: /* CIL Label */ 
4327#line 2383
4328          if (i == 2) {
4329#line 2383
4330            if (floorButtons_2) {
4331#line 2386
4332              retValue_acc = 1;
4333#line 2388
4334              return (retValue_acc);
4335            } else {
4336              goto _L___0;
4337            }
4338          } else {
4339            _L___0: /* CIL Label */ 
4340#line 2390
4341            if (i == 3) {
4342#line 2390
4343              if (floorButtons_3) {
4344#line 2393
4345                retValue_acc = 1;
4346#line 2395
4347                return (retValue_acc);
4348              } else {
4349                goto _L;
4350              }
4351            } else {
4352              _L: /* CIL Label */ 
4353#line 2397
4354              if (i == 4) {
4355#line 2397
4356                if (floorButtons_4) {
4357#line 2400 "Elevator.c"
4358                  retValue_acc = 1;
4359#line 2402
4360                  return (retValue_acc);
4361                } else {
4362
4363                }
4364              } else {
4365
4366              }
4367            }
4368          }
4369        }
4370      }
4371#line 395
4372      i = i + 1;
4373    }
4374    while_5_break: /* CIL Label */ ;
4375    }
4376  } else {
4377#line 2404 "Elevator.c"
4378    if (d == 0) {
4379#line 403
4380      i___0 = 0;
4381#line 404
4382      i___0 = currentFloorID - 1;
4383      {
4384#line 404
4385      while (1) {
4386        while_6_continue: /* CIL Label */ ;
4387#line 404
4388        if (i___0 >= 0) {
4389
4390        } else {
4391          goto while_6_break;
4392        }
4393#line 404
4394        i___0 = currentFloorID + 1;
4395        {
4396#line 404
4397        while (1) {
4398          while_7_continue: /* CIL Label */ ;
4399#line 404
4400          if (i___0 < 5) {
4401
4402          } else {
4403            goto while_7_break;
4404          }
4405#line 411
4406          if (i___0 == 0) {
4407#line 411 "Elevator.c"
4408            if (floorButtons_0) {
4409#line 2416
4410              retValue_acc = 1;
4411#line 2418
4412              return (retValue_acc);
4413            } else {
4414              goto _L___6;
4415            }
4416          } else {
4417            _L___6: /* CIL Label */ 
4418#line 2420
4419            if (i___0 == 1) {
4420#line 2420
4421              if (floorButtons_1) {
4422#line 2423
4423                retValue_acc = 1;
4424#line 2425
4425                return (retValue_acc);
4426              } else {
4427                goto _L___5;
4428              }
4429            } else {
4430              _L___5: /* CIL Label */ 
4431#line 2427
4432              if (i___0 == 2) {
4433#line 2427
4434                if (floorButtons_2) {
4435#line 2430
4436                  retValue_acc = 1;
4437#line 2432
4438                  return (retValue_acc);
4439                } else {
4440                  goto _L___4;
4441                }
4442              } else {
4443                _L___4: /* CIL Label */ 
4444#line 2434
4445                if (i___0 == 3) {
4446#line 2434
4447                  if (floorButtons_3) {
4448#line 2437
4449                    retValue_acc = 1;
4450#line 2439
4451                    return (retValue_acc);
4452                  } else {
4453                    goto _L___3;
4454                  }
4455                } else {
4456                  _L___3: /* CIL Label */ 
4457#line 2441
4458                  if (i___0 == 4) {
4459#line 2441
4460                    if (floorButtons_4) {
4461#line 2444 "Elevator.c"
4462                      retValue_acc = 1;
4463#line 2446
4464                      return (retValue_acc);
4465                    } else {
4466
4467                    }
4468                  } else {
4469
4470                  }
4471                }
4472              }
4473            }
4474          }
4475#line 404
4476          i___0 = i___0 + 1;
4477        }
4478        while_7_break: /* CIL Label */ ;
4479        }
4480#line 404
4481        i___0 = i___0 - 1;
4482      }
4483      while_6_break: /* CIL Label */ ;
4484      }
4485    } else {
4486
4487    }
4488  }
4489#line 2451 "Elevator.c"
4490  retValue_acc = 0;
4491#line 2453
4492  return (retValue_acc);
4493#line 2460
4494  return (retValue_acc);
4495}
4496}
4497#line 415 "Elevator.c"
4498int isExecutiveFloorCalling(void) 
4499{ int retValue_acc ;
4500
4501  {
4502  {
4503#line 2482 "Elevator.c"
4504  retValue_acc = isFloorCalling(executiveFloor);
4505  }
4506#line 2484
4507  return (retValue_acc);
4508#line 2491
4509  return (retValue_acc);
4510}
4511}
4512#line 419 "Elevator.c"
4513int isExecutiveFloor(int floorID ) 
4514{ int retValue_acc ;
4515
4516  {
4517#line 2513 "Elevator.c"
4518  retValue_acc = executiveFloor == floorID;
4519#line 2515
4520  return (retValue_acc);
4521#line 2522
4522  return (retValue_acc);
4523}
4524}
4525#line 1 "Specification2_spec.o"
4526#pragma merger(0,"Specification2_spec.i","")
4527#line 7 "Specification2_spec.c"
4528int floorButtons_spc2_0  ;
4529#line 8 "Specification2_spec.c"
4530int floorButtons_spc2_1  ;
4531#line 9 "Specification2_spec.c"
4532int floorButtons_spc2_2  ;
4533#line 10 "Specification2_spec.c"
4534int floorButtons_spc2_3  ;
4535#line 11 "Specification2_spec.c"
4536int floorButtons_spc2_4  ;
4537#line 15 "Specification2_spec.c"
4538void __utac_acc__Specification2_spec__1(void) 
4539{ 
4540
4541  {
4542#line 17
4543  floorButtons_spc2_0 = 0;
4544#line 18
4545  floorButtons_spc2_1 = 0;
4546#line 19
4547  floorButtons_spc2_2 = 0;
4548#line 20
4549  floorButtons_spc2_3 = 0;
4550#line 21
4551  floorButtons_spc2_4 = 0;
4552#line 21
4553  return;
4554}
4555}
4556#line 25 "Specification2_spec.c"
4557void __utac_acc__Specification2_spec__2(int floor ) 
4558{ 
4559
4560  {
4561#line 33
4562  if (floor == 0) {
4563#line 34
4564    floorButtons_spc2_0 = 1;
4565  } else {
4566#line 35
4567    if (floor == 1) {
4568#line 36
4569      floorButtons_spc2_1 = 1;
4570    } else {
4571#line 37
4572      if (floor == 2) {
4573#line 38
4574        floorButtons_spc2_2 = 1;
4575      } else {
4576#line 39
4577        if (floor == 3) {
4578#line 40
4579          floorButtons_spc2_3 = 1;
4580        } else {
4581#line 41
4582          if (floor == 4) {
4583#line 42
4584            floorButtons_spc2_4 = 1;
4585          } else {
4586
4587          }
4588        }
4589      }
4590    }
4591  }
4592#line 42
4593  return;
4594}
4595}
4596#line 35 "Specification2_spec.c"
4597void __utac_acc__Specification2_spec__3(void) 
4598{ int floor ;
4599  int tmp ;
4600  int tmp___0 ;
4601  int tmp___1 ;
4602  int tmp___2 ;
4603  int tmp___3 ;
4604  int tmp___4 ;
4605
4606  {
4607  {
4608#line 37
4609  tmp = getCurrentFloorID();
4610#line 37
4611  floor = tmp;
4612  }
4613#line 38
4614  if (floor == 0) {
4615#line 38
4616    if (floorButtons_spc2_0) {
4617      {
4618#line 38
4619      tmp___4 = areDoorsOpen();
4620      }
4621#line 38
4622      if (tmp___4) {
4623#line 39
4624        floorButtons_spc2_0 = 0;
4625      } else {
4626        goto _L___6;
4627      }
4628    } else {
4629      goto _L___6;
4630    }
4631  } else {
4632    _L___6: /* CIL Label */ 
4633#line 40
4634    if (floor == 1) {
4635#line 40
4636      if (floorButtons_spc2_1) {
4637        {
4638#line 40
4639        tmp___3 = areDoorsOpen();
4640        }
4641#line 40
4642        if (tmp___3) {
4643#line 41
4644          floorButtons_spc2_1 = 0;
4645        } else {
4646          goto _L___4;
4647        }
4648      } else {
4649        goto _L___4;
4650      }
4651    } else {
4652      _L___4: /* CIL Label */ 
4653#line 42
4654      if (floor == 2) {
4655#line 42
4656        if (floorButtons_spc2_2) {
4657          {
4658#line 42
4659          tmp___2 = areDoorsOpen();
4660          }
4661#line 42
4662          if (tmp___2) {
4663#line 43
4664            floorButtons_spc2_2 = 0;
4665          } else {
4666            goto _L___2;
4667          }
4668        } else {
4669          goto _L___2;
4670        }
4671      } else {
4672        _L___2: /* CIL Label */ 
4673#line 44
4674        if (floor == 3) {
4675#line 44
4676          if (floorButtons_spc2_3) {
4677            {
4678#line 44
4679            tmp___1 = areDoorsOpen();
4680            }
4681#line 44
4682            if (tmp___1) {
4683#line 45
4684              floorButtons_spc2_3 = 0;
4685            } else {
4686              goto _L___0;
4687            }
4688          } else {
4689            goto _L___0;
4690          }
4691        } else {
4692          _L___0: /* CIL Label */ 
4693#line 46
4694          if (floor == 4) {
4695#line 46
4696            if (floorButtons_spc2_4) {
4697              {
4698#line 46
4699              tmp___0 = areDoorsOpen();
4700              }
4701#line 46
4702              if (tmp___0) {
4703#line 47
4704                floorButtons_spc2_4 = 0;
4705              } else {
4706
4707              }
4708            } else {
4709
4710            }
4711          } else {
4712
4713          }
4714        }
4715      }
4716    }
4717  }
4718#line 47
4719  return;
4720}
4721}
4722#line 52 "Specification2_spec.c"
4723void __utac_acc__Specification2_spec__4(void) 
4724{ 
4725
4726  {
4727#line 60
4728  if (floorButtons_spc2_0) {
4729    {
4730#line 61
4731    __automaton_fail();
4732    }
4733  } else {
4734#line 62
4735    if (floorButtons_spc2_1) {
4736      {
4737#line 63
4738      __automaton_fail();
4739      }
4740    } else {
4741#line 64
4742      if (floorButtons_spc2_2) {
4743        {
4744#line 65
4745        __automaton_fail();
4746        }
4747      } else {
4748#line 66
4749        if (floorButtons_spc2_3) {
4750          {
4751#line 67
4752          __automaton_fail();
4753          }
4754        } else {
4755#line 68
4756          if (floorButtons_spc2_4) {
4757            {
4758#line 69
4759            __automaton_fail();
4760            }
4761          } else {
4762
4763          }
4764        }
4765      }
4766    }
4767  }
4768#line 69
4769  return;
4770}
4771}
4772#line 1 "UnitTests.o"
4773#pragma merger(0,"UnitTests.i","")
4774#line 24 "UnitTests.c"
4775void spec1(void) 
4776{ int tmp ;
4777  int tmp___0 ;
4778  int i ;
4779  int tmp___1 ;
4780
4781  {
4782  {
4783#line 25
4784  initBottomUp();
4785#line 26
4786  tmp = getOrigin(5);
4787#line 26
4788  initPersonOnFloor(5, tmp);
4789#line 27
4790  printState();
4791#line 30
4792  tmp___0 = getOrigin(2);
4793#line 30
4794  initPersonOnFloor(2, tmp___0);
4795#line 31
4796  printState();
4797#line 35
4798  i = 0;
4799  }
4800  {
4801#line 35
4802  while (1) {
4803    while_8_continue: /* CIL Label */ ;
4804#line 35
4805    if (i < cleanupTimeShifts) {
4806      {
4807#line 35
4808      tmp___1 = isBlocked();
4809      }
4810#line 35
4811      if (tmp___1 != 1) {
4812
4813      } else {
4814        goto while_8_break;
4815      }
4816    } else {
4817      goto while_8_break;
4818    }
4819    {
4820#line 36
4821    timeShift();
4822#line 37
4823    printState();
4824#line 35
4825    i = i + 1;
4826    }
4827  }
4828  while_8_break: /* CIL Label */ ;
4829  }
4830#line 1073 "UnitTests.c"
4831  return;
4832}
4833}
4834#line 42 "UnitTests.c"
4835void spec14(void) 
4836{ int tmp ;
4837  int tmp___0 ;
4838  int i ;
4839  int tmp___1 ;
4840
4841  {
4842  {
4843#line 43
4844  initTopDown();
4845#line 44
4846  tmp = getOrigin(5);
4847#line 44
4848  initPersonOnFloor(5, tmp);
4849#line 45
4850  printState();
4851#line 47
4852  timeShift();
4853#line 48
4854  timeShift();
4855#line 49
4856  timeShift();
4857#line 50
4858  timeShift();
4859#line 52
4860  tmp___0 = getOrigin(0);
4861#line 52
4862  initPersonOnFloor(0, tmp___0);
4863#line 53
4864  printState();
4865#line 57
4866  i = 0;
4867  }
4868  {
4869#line 57
4870  while (1) {
4871    while_9_continue: /* CIL Label */ ;
4872#line 57
4873    if (i < cleanupTimeShifts) {
4874      {
4875#line 57
4876      tmp___1 = isBlocked();
4877      }
4878#line 57
4879      if (tmp___1 != 1) {
4880
4881      } else {
4882        goto while_9_break;
4883      }
4884    } else {
4885      goto while_9_break;
4886    }
4887    {
4888#line 58
4889    timeShift();
4890#line 59
4891    printState();
4892#line 57
4893    i = i + 1;
4894    }
4895  }
4896  while_9_break: /* CIL Label */ ;
4897  }
4898#line 1119 "UnitTests.c"
4899  return;
4900}
4901}