Showing error 1617

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

Source: 

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