Showing error 1605

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