Showing error 1593

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_spec13_product24_safe.cil.c
Line in file: 3467
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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