Showing error 1650

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/elevator_spec3_product32_unsafe.cil.c
Line in file: 203
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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