Showing error 1620

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