ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1599

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