Showing error 1589

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