Showing error 1636

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