Showing error 1640

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