Showing error 1624

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