Showing error 1637

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