Showing error 1579

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