Showing error 1658

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