Showing error 1571

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