Showing error 1629

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