Showing error 1577

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