Showing error 1570

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