Showing error 1603

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