Showing error 1659

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