Showing error 1653

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