ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1576

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