Showing error 1615

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