Showing error 1654

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