Showing error 1613

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