Showing error 1635

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