Showing error 1580

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