Showing error 1660

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