Showing error 1581

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