Showing error 1656

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