Showing error 1643

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