Showing error 1655

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

Source: 

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