Showing error 1630

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