Showing error 1586

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