Showing error 1632

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