Showing error 1634

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