Showing error 1568

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_productSimulator_unsafe.cil.c
Line in file: 693
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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