Showing error 1649

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