Showing error 1574

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

Source: 

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