Showing error 1651

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