Showing error 1602

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