ClabureDB: Classified Bug-Reports Database

   extern int __VERIFIER_nondet_int(void);
   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 2 "libacc.c"
   struct JoinPoint {
      void **(*fp)(struct JoinPoint * ) ;
      void **args ;
      int argsCount ;
     char const   **argsType ;
     void *(*arg)(int  , struct JoinPoint * ) ;
     char const   *(*argType)(int  , struct JoinPoint * ) ;
     void **retValue ;
     char const   *retType ;
     char const   *funcName ;
     char const   *targetName ;
     char const   *fileName ;
     char const   *kind ;
     void *excep_return ;
  };
  #line 18 "libacc.c"
  struct __UTAC__CFLOW_FUNC {
     int (*func)(int  , int  ) ;
     int val ;
     struct __UTAC__CFLOW_FUNC *next ;
  };
  #line 18 "libacc.c"
  struct __UTAC__EXCEPTION {
     void *jumpbuf ;
     unsigned long long prtValue ;
     int pops ;
     struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  };
  #line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  typedef unsigned long size_t;
  #line 76 "libacc.c"
  struct __ACC__ERR {
     void *v ;
     struct __ACC__ERR *next ;
  };
  #line 1 "scenario.o"
  #pragma merger(0,"scenario.i","")
  #line 2 "scenario.c"
  void initTopDown(void) ;
  #line 3
  void bobCall(void) ;
  #line 4
  void threeTS(void) ;
  #line 6
  void cleanup(void) ;
  #line 1 "scenario.c"
  void test(void) 
  { 
  
    {
    {
  #line 2
    initTopDown();
  #line 3
    bobCall();
  #line 4
    threeTS();
  #line 5
    bobCall();
  #line 6
    cleanup();
    }
  #line 59 "scenario.c"
    return;
  }
  }
  #line 1 "Test.o"
  #pragma merger(0,"Test.i","")
  #line 544 "/usr/include/stdlib.h"
  extern  __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
  #line 13 "Test.c"
  int cleanupTimeShifts  =    12;
  #line 17 "Test.c"
  #line 23 "Test.c"
  int get_nondetMinMax07(void) 
  { int retValue_acc ;
    int nd ;
    nd = __VERIFIER_nondet_int();
  
    {
  #line 26 "Test.c"
    if (nd == 0) {
  #line 1108
      retValue_acc = 0;
  #line 1110
      return (retValue_acc);
    } else {
  #line 1112
      if (nd == 1) {
  #line 1117
        retValue_acc = 1;
  #line 1119
        return (retValue_acc);
      } else {
 #line 1121
       if (nd == 2) {
 #line 1126
         retValue_acc = 2;
 #line 1128
         return (retValue_acc);
       } else {
 #line 1130
         if (nd == 3) {
 #line 1135
           retValue_acc = 3;
 #line 1137
           return (retValue_acc);
         } else {
 #line 1139
           if (nd == 4) {
 #line 1144
             retValue_acc = 4;
 #line 1146
             return (retValue_acc);
           } else {
 #line 1148
             if (nd == 5) {
 #line 1153
               retValue_acc = 5;
 #line 1155
               return (retValue_acc);
             } else {
 #line 1157
               if (nd == 6) {
 #line 1162
                 retValue_acc = 6;
 #line 1164
                 return (retValue_acc);
               } else {
 #line 1166
                 if (nd == 7) {
 #line 1171 "Test.c"
                   retValue_acc = 7;
 #line 1173
                   return (retValue_acc);
                 } else {
                   {
 #line 43
                   exit(0);
                   }
                 }
               }
             }
           }
         }
       }
     }
   }
 #line 1183 "Test.c"
   return (retValue_acc);
 }
 }
 #line 48 "Test.c"
 void initPersonOnFloor(int person , int floor ) ;
 #line 48
 int getOrigin(int person ) ;
 #line 48 "Test.c"
 void bobCall(void) 
 { int tmp ;
 
   {
   {
 #line 48
   tmp = getOrigin(0);
 #line 48
   initPersonOnFloor(0, tmp);
   }
 #line 1207 "Test.c"
   return;
 }
 }
 #line 50 "Test.c"
 void aliceCall(void) 
 { int tmp ;
 
   {
   {
 #line 50
   tmp = getOrigin(1);
 #line 50
   initPersonOnFloor(1, tmp);
   }
 #line 1227 "Test.c"
   return;
 }
 }
 #line 52 "Test.c"
 void angelinaCall(void) 
 { int tmp ;
 
   {
   {
 #line 52
   tmp = getOrigin(2);
 #line 52
   initPersonOnFloor(2, tmp);
   }
 #line 1247 "Test.c"
   return;
 }
 }
 #line 54 "Test.c"
 void chuckCall(void) 
 { int tmp ;
 
   {
   {
 #line 54
   tmp = getOrigin(3);
 #line 54
   initPersonOnFloor(3, tmp);
   }
 #line 1267 "Test.c"
   return;
 }
 }
 #line 56 "Test.c"
 void monicaCall(void) 
 { int tmp ;
 
   {
   {
 #line 56
   tmp = getOrigin(4);
 #line 56
   initPersonOnFloor(4, tmp);
   }
 #line 1287 "Test.c"
   return;
 }
 }
 #line 58 "Test.c"
 void bigMacCall(void) 
 { int tmp ;
 
   {
   {
 #line 58
   tmp = getOrigin(5);
 #line 58
   initPersonOnFloor(5, tmp);
   }
 #line 1307 "Test.c"
   return;
 }
 }
 #line 60 "Test.c"
 void timeShift(void) ;
 #line 60 "Test.c"
 void threeTS(void) 
 { 
 
   {
   {
 #line 60
   timeShift();
 #line 60
   timeShift();
 #line 60
   timeShift();
   }
 #line 1331 "Test.c"
   return;
 }
 }
 #line 71 "Test.c"
 int isIdle(void) ;
 #line 67
 int isBlocked(void) ;
 #line 62 "Test.c"
 void cleanup(void) 
 { int i ;
   int tmp ;
   int tmp___0 ;
   int __cil_tmp4 ;
 
   {
   {
 #line 65
   timeShift();
 #line 67
   i = 0;
   }
   {
 #line 67
   while (1) {
     while_0_continue: /* CIL Label */ ;
     {
 #line 67
     __cil_tmp4 = cleanupTimeShifts - 1;
 #line 67
     if (i < __cil_tmp4) {
       {
 #line 67
       tmp___0 = isBlocked();
       }
 #line 67
       if (tmp___0 != 1) {
 
       } else {
         goto while_0_break;
       }
     } else {
       goto while_0_break;
     }
     }
     {
 #line 71
     tmp = isIdle();
     }
 #line 71
     if (tmp) {
 #line 72
       return;
     } else {
       {
 #line 74
       timeShift();
       }
     }
 #line 67
     i = i + 1;
   }
   while_0_break: /* CIL Label */ ;
   }
 #line 1362 "Test.c"
   return;
 }
 }
 #line 85 "Test.c"
 void initBottomUp(void) ;
 #line 77 "Test.c"
 void randomSequenceOfActions(void) 
 { int maxLength ;
   int tmp ;
   int counter ;
   int action ;
   int tmp___0 ;
   int origin ;
   int tmp___1 ;
   int tmp___2 ;
 
   {
   {
 #line 78
   maxLength = 4;
 #line 79
   tmp = __VERIFIER_nondet_int();
   }
 #line 79
   if (tmp) {
     {
 #line 81
     initTopDown();
     }
   } else {
     {
 #line 85
     initBottomUp();
     }
   }
 #line 90
   counter = 0;
   {
 #line 91
   while (1) {
     while_1_continue: /* CIL Label */ ;
 #line 91
     if (counter < maxLength) {
 
     } else {
       goto while_1_break;
     }
     {
 #line 92
     counter = counter + 1;
 #line 93
     tmp___0 = get_nondetMinMax07();
 #line 93
     action = tmp___0;
     }
 #line 99
     if (action < 6) {
       {
 #line 100
       tmp___1 = getOrigin(action);
 #line 100
       origin = tmp___1;
 #line 101
       initPersonOnFloor(action, origin);
       }
     } else {
 #line 102
       if (action == 6) {
         {
 #line 103
         timeShift();
         }
       } else {
 #line 104
         if (action == 7) {
           {
 #line 106
           timeShift();
 #line 107
           timeShift();
 #line 108
           timeShift();
           }
         } else {
 
         }
       }
     }
     {
 #line 113
     tmp___2 = isBlocked();
     }
 #line 113
     if (tmp___2) {
 #line 114
       return;
     } else {
 
     }
   }
   while_1_break: /* CIL Label */ ;
   }
   {
 #line 117
   cleanup();
   }
 #line 1433 "Test.c"
   return;
 }
 }
 #line 122 "Test.c"
 void runTest_Simple(void) 
 { 
 
   {
   {
 #line 123
   bigMacCall();
 #line 124
   angelinaCall();
 #line 125
   cleanup();
   }
 #line 1457 "Test.c"
   return;
 }
 }
 #line 130 "Test.c"
 void Specification1(void) 
 { 
 
   {
   {
 #line 131
   bigMacCall();
 #line 132
   angelinaCall();
 #line 133
   cleanup();
   }
 #line 1481 "Test.c"
   return;
 }
 }
 #line 137 "Test.c"
 void Specification2(void) 
 { 
 
   {
   {
 #line 138
   bigMacCall();
 #line 139
   cleanup();
   }
 #line 1503 "Test.c"
   return;
 }
 }
 #line 142 "Test.c"
 void Specification3(void) 
 { 
 
   {
   {
 #line 143
   bobCall();
 #line 144
   timeShift();
 #line 145
   timeShift();
 #line 146
   timeShift();
 #line 147
   timeShift();
 #line 149
   timeShift();
 #line 154
   bobCall();
 #line 155
   cleanup();
   }
 #line 1537 "Test.c"
   return;
 }
 }
 #line 160 "Test.c"
 void setup(void) 
 { 
 
   {
 #line 1555 "Test.c"
   return;
 }
 }
 #line 165 "Test.c"
 void runTest(void) 
 { 
 
   {
   {
 #line 168
   test();
   }
 #line 1575 "Test.c"
   return;
 }
 }
 #line 174 "Test.c"
 void select_helpers(void) ;
 #line 175
 void select_features(void) ;
 #line 176
 int valid_product(void) ;
 #line 173 "Test.c"
 int main(void) 
 { int retValue_acc ;
   int tmp ;
 
   {
   {
 #line 174
   select_helpers();
 #line 175
   select_features();
 #line 176
   tmp = valid_product();
   }
 #line 176
   if (tmp) {
     {
 #line 177
     setup();
 #line 178
     runTest();
     }
   } else {
 
   }
 #line 1604 "Test.c"
   retValue_acc = 0;
 #line 1606
   return (retValue_acc);
 #line 1613
   return (retValue_acc);
 }
 }
 #line 1 "Person.o"
 #pragma merger(0,"Person.i","")
 #line 10 "Person.h"
 int getWeight(int person ) ;
 #line 14
 int getDestination(int person ) ;
 #line 20 "Person.c"
 int getWeight(int person ) 
 { int retValue_acc ;
 
   {
 #line 35 "Person.c"
   if (person == 0) {
 #line 974
     retValue_acc = 40;
 #line 976
     return (retValue_acc);
   } else {
 #line 978
     if (person == 1) {
 #line 983
       retValue_acc = 40;
 #line 985
       return (retValue_acc);
     } else {
 #line 987
       if (person == 2) {
 #line 992
         retValue_acc = 40;
 #line 994
         return (retValue_acc);
       } else {
 #line 996
         if (person == 3) {
 #line 1001
           retValue_acc = 40;
 #line 1003
           return (retValue_acc);
         } else {
 #line 1005
           if (person == 4) {
 #line 1010
             retValue_acc = 30;
 #line 1012
             return (retValue_acc);
           } else {
 #line 1014
             if (person == 5) {
 #line 1019
               retValue_acc = 150;
 #line 1021
               return (retValue_acc);
             } else {
 #line 1027 "Person.c"
               retValue_acc = 0;
 #line 1029
               return (retValue_acc);
             }
           }
         }
       }
     }
   }
 #line 1036 "Person.c"
   return (retValue_acc);
 }
 }
 #line 39 "Person.c"
 int getOrigin(int person ) 
 { int retValue_acc ;
 
   {
 #line 54 "Person.c"
   if (person == 0) {
 #line 1061
     retValue_acc = 4;
 #line 1063
     return (retValue_acc);
   } else {
 #line 1065
     if (person == 1) {
 #line 1070
       retValue_acc = 3;
 #line 1072
       return (retValue_acc);
     } else {
 #line 1074
       if (person == 2) {
 #line 1079
         retValue_acc = 2;
 #line 1081
         return (retValue_acc);
       } else {
 #line 1083
         if (person == 3) {
 #line 1088
           retValue_acc = 1;
 #line 1090
           return (retValue_acc);
         } else {
 #line 1092
           if (person == 4) {
 #line 1097
             retValue_acc = 0;
 #line 1099
             return (retValue_acc);
           } else {
 #line 1101
             if (person == 5) {
 #line 1106
               retValue_acc = 1;
 #line 1108
               return (retValue_acc);
             } else {
 #line 1114 "Person.c"
               retValue_acc = 0;
 #line 1116
               return (retValue_acc);
             }
           }
         }
       }
     }
   }
 #line 1123 "Person.c"
   return (retValue_acc);
 }
 }
 #line 57 "Person.c"
 int getDestination(int person ) 
 { int retValue_acc ;
 
   {
 #line 72 "Person.c"
   if (person == 0) {
 #line 1148
     retValue_acc = 0;
 #line 1150
     return (retValue_acc);
   } else {
 #line 1152
     if (person == 1) {
 #line 1157
       retValue_acc = 0;
 #line 1159
       return (retValue_acc);
     } else {
 #line 1161
       if (person == 2) {
 #line 1166
         retValue_acc = 1;
 #line 1168
         return (retValue_acc);
       } else {
 #line 1170
         if (person == 3) {
 #line 1175
           retValue_acc = 3;
 #line 1177
           return (retValue_acc);
         } else {
 #line 1179
           if (person == 4) {
 #line 1184
             retValue_acc = 1;
 #line 1186
             return (retValue_acc);
           } else {
 #line 1188
             if (person == 5) {
 #line 1193
               retValue_acc = 3;
 #line 1195
               return (retValue_acc);
             } else {
 #line 1201 "Person.c"
               retValue_acc = 0;
 #line 1203
               return (retValue_acc);
             }
           }
         }
       }
     }
   }
 #line 1210 "Person.c"
   return (retValue_acc);
 }
 }
 #line 1 "UnitTests.o"
 #pragma merger(0,"UnitTests.i","")
 #line 24 "Elevator.h"
 void printState(void) ;
 #line 45 "Elevator.h"
 int weight  =    0;
 #line 47 "Elevator.h"
 int maximumWeight  =    100;
 #line 55 "Elevator.h"
 int executiveFloor  =    4;
 #line 63 "Elevator.h"
 int blocked  =    0;
 #line 24 "UnitTests.c"
 void spec1(void) 
 { int tmp ;
   int tmp___0 ;
   int i ;
   int tmp___1 ;
 
   {
   {
 #line 25
   initBottomUp();
 #line 26
   tmp = getOrigin(5);
 #line 26
   initPersonOnFloor(5, tmp);
 #line 27
   printState();
 #line 30
   tmp___0 = getOrigin(2);
 #line 30
   initPersonOnFloor(2, tmp___0);
 #line 31
   printState();
 #line 35
   i = 0;
   }
   {
 #line 35
   while (1) {
     while_2_continue: /* CIL Label */ ;
 #line 35
     if (i < cleanupTimeShifts) {
       {
 #line 35
       tmp___1 = isBlocked();
       }
 #line 35
       if (tmp___1 != 1) {
 
       } else {
         goto while_2_break;
       }
     } else {
       goto while_2_break;
     }
     {
 #line 36
     timeShift();
 #line 37
     printState();
 #line 35
     i = i + 1;
     }
   }
   while_2_break: /* CIL Label */ ;
   }
 #line 1079 "UnitTests.c"
   return;
 }
 }
 #line 42 "UnitTests.c"
 void spec14(void) 
 { int tmp ;
   int tmp___0 ;
   int i ;
   int tmp___1 ;
 
   {
   {
 #line 43
   initTopDown();
 #line 44
   tmp = getOrigin(5);
 #line 44
   initPersonOnFloor(5, tmp);
 #line 45
   printState();
 #line 47
   timeShift();
 #line 48
   timeShift();
 #line 49
   timeShift();
 #line 50
   timeShift();
 #line 52
   tmp___0 = getOrigin(0);
 #line 52
   initPersonOnFloor(0, tmp___0);
 #line 53
   printState();
 #line 57
   i = 0;
   }
   {
 #line 57
   while (1) {
     while_3_continue: /* CIL Label */ ;
 #line 57
     if (i < cleanupTimeShifts) {
       {
 #line 57
       tmp___1 = isBlocked();
       }
 #line 57
       if (tmp___1 != 1) {
 
       } else {
         goto while_3_break;
       }
     } else {
       goto while_3_break;
     }
     {
 #line 58
     timeShift();
 #line 59
     printState();
 #line 57
     i = i + 1;
     }
   }
   while_3_break: /* CIL Label */ ;
   }
 #line 1125 "UnitTests.c"
   return;
 }
 }
 #line 1 "Elevator.o"
 #pragma merger(0,"Elevator.i","")
 #line 359 "/usr/include/stdio.h"
 extern int printf(char const   * __restrict  __format  , ...) ;
 #line 16 "Person.h"
 void enterElevator(int p ) ;
 #line 12 "Floor.h"
 int isFloorCalling(int floorID ) ;
 #line 14
 void resetCallOnFloor(int floorID ) ;
 #line 18
 int isPersonOnFloor(int person , int floor ) ;
 #line 22
 void removePersonFromFloor(int person , int floor ) ;
 #line 24
 int isTopFloor(int floorID ) ;
 #line 28
 void initFloors(void) ;
 #line 26 "Elevator.h"
 int isEmpty(void) ;
 #line 28
 int isAnyLiftButtonPressed(void) ;
 #line 30
 int buttonForFloorIsPressed(int floorID ) ;
 #line 38
 int areDoorsOpen(void) ;
 #line 40
 int getCurrentFloorID(void) ;
 #line 58
 int isExecutiveFloorCalling(void) ;
 #line 60
 int isExecutiveFloor(int floorID ) ;
 #line 18 "Elevator.c"
 int currentHeading  =    1;
 #line 20 "Elevator.c"
 int currentFloorID  =    0;
 #line 22 "Elevator.c"
 int persons_0  ;
 #line 24 "Elevator.c"
 int persons_1  ;
 #line 26 "Elevator.c"
 int persons_2  ;
 #line 28 "Elevator.c"
 int persons_3  ;
 #line 30 "Elevator.c"
 int persons_4  ;
 #line 32 "Elevator.c"
 int persons_5  ;
 #line 35 "Elevator.c"
 int doorState  =    1;
 #line 37 "Elevator.c"
 int floorButtons_0  ;
 #line 39 "Elevator.c"
 int floorButtons_1  ;
 #line 41 "Elevator.c"
 int floorButtons_2  ;
 #line 43 "Elevator.c"
 int floorButtons_3  ;
 #line 45 "Elevator.c"
 int floorButtons_4  ;
 #line 53 "Elevator.c"
 void initTopDown(void) 
 { 
 
   {
   {
 #line 54
   currentFloorID = 4;
 #line 55
   currentHeading = 0;
 #line 56
   floorButtons_0 = 0;
 #line 57
   floorButtons_1 = 0;
 #line 58
   floorButtons_2 = 0;
 #line 59
   floorButtons_3 = 0;
 #line 60
   floorButtons_4 = 0;
 #line 61
   persons_0 = 0;
 #line 62
   persons_1 = 0;
 #line 63
   persons_2 = 0;
 #line 64
   persons_3 = 0;
 #line 65
   persons_4 = 0;
 #line 66
   persons_5 = 0;
#line 67
  initFloors();
  }
#line 1083 "Elevator.c"
  return;
}
}
#line 70 "Elevator.c"
void initBottomUp(void) 
{ 

  {
  {
#line 71
  currentFloorID = 0;
#line 72
  currentHeading = 1;
#line 73
  floorButtons_0 = 0;
#line 74
  floorButtons_1 = 0;
#line 75
  floorButtons_2 = 0;
#line 76
  floorButtons_3 = 0;
#line 77
  floorButtons_4 = 0;
#line 78
  persons_0 = 0;
#line 79
  persons_1 = 0;
#line 80
  persons_2 = 0;
#line 81
  persons_3 = 0;
#line 82
  persons_4 = 0;
#line 83
  persons_5 = 0;
#line 84
  initFloors();
  }
#line 1129 "Elevator.c"
  return;
}
}
#line 86 "Elevator.c"
int isBlocked(void) 
{ int retValue_acc ;

  {
#line 1147 "Elevator.c"
  retValue_acc = blocked;
#line 1149
  return (retValue_acc);
#line 1156
  return (retValue_acc);
}
}
#line 91 "Elevator.c"
void enterElevator__wrappee__base(int p ) 
{ 

  {
#line 100
  if (p == 0) {
#line 101
    persons_0 = 1;
  } else {
#line 102
    if (p == 1) {
#line 103
      persons_1 = 1;
    } else {
#line 104
      if (p == 2) {
#line 105
        persons_2 = 1;
      } else {
#line 106
        if (p == 3) {
#line 107
          persons_3 = 1;
        } else {
#line 108
          if (p == 4) {
#line 109
            persons_4 = 1;
          } else {
#line 110
            if (p == 5) {
#line 111
              persons_5 = 1;
            } else {

            }
          }
        }
      }
    }
  }
#line 1191 "Elevator.c"
  return;
}
}
#line 102 "Elevator.c"
void enterElevator(int p ) 
{ int tmp ;

  {
  {
#line 103
  enterElevator__wrappee__base(p);
#line 104
  tmp = getWeight(p);
#line 104
  weight = weight + tmp;
  }
#line 1213 "Elevator.c"
  return;
}
}
#line 107 "Elevator.c"
void leaveElevator__wrappee__base(int p ) 
{ 

  {
#line 115
  if (p == 0) {
#line 116
    persons_0 = 0;
  } else {
#line 117
    if (p == 1) {
#line 118
      persons_1 = 0;
    } else {
#line 119
      if (p == 2) {
#line 120
        persons_2 = 0;
      } else {
#line 121
        if (p == 3) {
#line 122
          persons_3 = 0;
        } else {
#line 123
          if (p == 4) {
#line 124
            persons_4 = 0;
          } else {
#line 125
            if (p == 5) {
#line 126
              persons_5 = 0;
            } else {

            }
          }
        }
      }
    }
  }
#line 1244 "Elevator.c"
  return;
}
}
#line 117 "Elevator.c"
void leaveElevator(int p ) 
{ int tmp ;

  {
  {
#line 118
  leaveElevator__wrappee__base(p);
#line 119
  tmp = getWeight(p);
#line 119
  weight = weight - tmp;
  }
#line 1266 "Elevator.c"
  return;
}
}
#line 122 "Elevator.c"
void pressInLiftFloorButton(int floorID ) 
{ 

  {
#line 128
  if (floorID == 0) {
#line 129
    floorButtons_0 = 1;
  } else {
#line 130
    if (floorID == 1) {
#line 131
      floorButtons_1 = 1;
    } else {
#line 132
      if (floorID == 2) {
#line 133
        floorButtons_2 = 1;
      } else {
#line 134
        if (floorID == 3) {
#line 135
          floorButtons_3 = 1;
        } else {
#line 136
          if (floorID == 4) {
#line 137
            floorButtons_4 = 1;
          } else {

          }
        }
      }
    }
  }
#line 1295 "Elevator.c"
  return;
}
}
#line 130 "Elevator.c"
void resetFloorButton(int floorID ) 
{ 

  {
#line 136
  if (floorID == 0) {
#line 137
    floorButtons_0 = 0;
  } else {
#line 138
    if (floorID == 1) {
#line 139
      floorButtons_1 = 0;
    } else {
#line 140
      if (floorID == 2) {
#line 141
        floorButtons_2 = 0;
      } else {
#line 142
        if (floorID == 3) {
#line 143
          floorButtons_3 = 0;
        } else {
#line 144
          if (floorID == 4) {
#line 145
            floorButtons_4 = 0;
          } else {

          }
        }
      }
    }
  }
#line 1324 "Elevator.c"
  return;
}
}
#line 138 "Elevator.c"
int getCurrentFloorID(void) 
{ int retValue_acc ;

  {
#line 1342 "Elevator.c"
  retValue_acc = currentFloorID;
#line 1344
  return (retValue_acc);
#line 1351
  return (retValue_acc);
}
}
#line 142 "Elevator.c"
int areDoorsOpen(void) 
{ int retValue_acc ;

  {
#line 1373 "Elevator.c"
  retValue_acc = doorState;
#line 1375
  return (retValue_acc);
#line 1382
  return (retValue_acc);
}
}
#line 146 "Elevator.c"
int buttonForFloorIsPressed(int floorID ) 
{ int retValue_acc ;

  {
#line 152 "Elevator.c"
  if (floorID == 0) {
#line 1405
    retValue_acc = floorButtons_0;
#line 1407
    return (retValue_acc);
  } else {
#line 1409
    if (floorID == 1) {
#line 1412
      retValue_acc = floorButtons_1;
#line 1414
      return (retValue_acc);
    } else {
#line 1416
      if (floorID == 2) {
#line 1419
        retValue_acc = floorButtons_2;
#line 1421
        return (retValue_acc);
      } else {
#line 1423
        if (floorID == 3) {
#line 1426
          retValue_acc = floorButtons_3;
#line 1428
          return (retValue_acc);
        } else {
#line 1430
          if (floorID == 4) {
#line 1433
            retValue_acc = floorButtons_4;
#line 1435
            return (retValue_acc);
          } else {
#line 1439 "Elevator.c"
            retValue_acc = 0;
#line 1441
            return (retValue_acc);
          }
        }
      }
    }
  }
#line 1448 "Elevator.c"
  return (retValue_acc);
}
}
#line 155 "Elevator.c"
int getCurrentHeading(void) 
{ int retValue_acc ;

  {
#line 1470 "Elevator.c"
  retValue_acc = currentHeading;
#line 1472
  return (retValue_acc);
#line 1479
  return (retValue_acc);
}
}
#line 159 "Elevator.c"
int isEmpty(void) 
{ int retValue_acc ;

  {
#line 166 "Elevator.c"
  if (persons_0 == 1) {
#line 1502
    retValue_acc = 0;
#line 1504
    return (retValue_acc);
  } else {
#line 1506
    if (persons_1 == 1) {
#line 1509
      retValue_acc = 0;
#line 1511
      return (retValue_acc);
    } else {
#line 1513
      if (persons_2 == 1) {
#line 1516
        retValue_acc = 0;
#line 1518
        return (retValue_acc);
      } else {
#line 1520
        if (persons_3 == 1) {
#line 1523
          retValue_acc = 0;
#line 1525
          return (retValue_acc);
        } else {
#line 1527
          if (persons_4 == 1) {
#line 1530
            retValue_acc = 0;
#line 1532
            return (retValue_acc);
          } else {
#line 1534
            if (persons_5 == 1) {
#line 1537 "Elevator.c"
              retValue_acc = 0;
#line 1539
              return (retValue_acc);
            } else {

            }
          }
        }
      }
    }
  }
#line 1544 "Elevator.c"
  retValue_acc = 1;
#line 1546
  return (retValue_acc);
#line 1553
  return (retValue_acc);
}
}
#line 170 "Elevator.c"
int anyStopRequested(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;

  {
  {
#line 181
  tmp___3 = isFloorCalling(0);
  }
#line 181 "Elevator.c"
  if (tmp___3) {
#line 1576
    retValue_acc = 1;
#line 1578
    return (retValue_acc);
  } else {
#line 1580
    if (floorButtons_0) {
#line 1583
      retValue_acc = 1;
#line 1585
      return (retValue_acc);
    } else {
      {
#line 1587 "Elevator.c"
      tmp___2 = isFloorCalling(1);
      }
#line 1587
      if (tmp___2) {
#line 1590
        retValue_acc = 1;
#line 1592
        return (retValue_acc);
      } else {
#line 1594
        if (floorButtons_1) {
#line 1597
          retValue_acc = 1;
#line 1599
          return (retValue_acc);
        } else {
          {
#line 1601
          tmp___1 = isFloorCalling(2);
          }
#line 1601
          if (tmp___1) {
#line 1604
            retValue_acc = 1;
#line 1606
            return (retValue_acc);
          } else {
#line 1608
            if (floorButtons_2) {
#line 1611
              retValue_acc = 1;
#line 1613
              return (retValue_acc);
            } else {
              {
#line 1615
              tmp___0 = isFloorCalling(3);
              }
#line 1615
              if (tmp___0) {
#line 1618
                retValue_acc = 1;
#line 1620
                return (retValue_acc);
              } else {
#line 1622
                if (floorButtons_3) {
#line 1625
                  retValue_acc = 1;
#line 1627
                  return (retValue_acc);
                } else {
                  {
#line 1629
                  tmp = isFloorCalling(4);
                  }
#line 1629
                  if (tmp) {
#line 1632
                    retValue_acc = 1;
#line 1634
                    return (retValue_acc);
                  } else {
#line 1636
                    if (floorButtons_4) {
#line 1639
                      retValue_acc = 1;
#line 1641
                      return (retValue_acc);
                    } else {

                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
#line 1646 "Elevator.c"
  retValue_acc = 0;
#line 1648
  return (retValue_acc);
#line 1655
  return (retValue_acc);
}
}
#line 184 "Elevator.c"
int isIdle(void) 
{ int retValue_acc ;
  int tmp ;

  {
  {
#line 1677 "Elevator.c"
  tmp = anyStopRequested();
#line 1677
  retValue_acc = tmp == 0;
  }
#line 1679
  return (retValue_acc);
#line 1686
  return (retValue_acc);
}
}
#line 188 "Elevator.c"
int stopRequestedInDirection__wrappee__weight(int dir , int respectFloorCalls , int respectInLiftCalls ) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  int tmp___5 ;
  int tmp___6 ;
  int tmp___7 ;
  int tmp___8 ;
  int tmp___9 ;

  {
#line 239
  if (dir == 1) {
    {
#line 199
    tmp = isTopFloor(currentFloorID);
    }
#line 199 "Elevator.c"
    if (tmp) {
#line 1712 "Elevator.c"
      retValue_acc = 0;
#line 1714
      return (retValue_acc);
    } else {

    }
#line 199
    if (currentFloorID < 0) {
#line 199
      if (respectFloorCalls) {
        {
#line 199 "Elevator.c"
        tmp___4 = isFloorCalling(0);
        }
#line 199 "Elevator.c"
        if (tmp___4) {
#line 1720 "Elevator.c"
          retValue_acc = 1;
#line 1722
          return (retValue_acc);
        } else {
          goto _L___16;
        }
      } else {
        goto _L___16;
      }
    } else {
      _L___16: /* CIL Label */ 
#line 1724
      if (currentFloorID < 0) {
#line 1724
        if (respectInLiftCalls) {
#line 1724
          if (floorButtons_0) {
#line 1727
            retValue_acc = 1;
#line 1729
            return (retValue_acc);
          } else {
            goto _L___14;
          }
        } else {
          goto _L___14;
        }
      } else {
        _L___14: /* CIL Label */ 
#line 1731
        if (currentFloorID < 1) {
#line 1731
          if (respectFloorCalls) {
            {
#line 1731
            tmp___3 = isFloorCalling(1);
            }
#line 1731
            if (tmp___3) {
#line 1734
              retValue_acc = 1;
#line 1736
              return (retValue_acc);
            } else {
              goto _L___12;
            }
          } else {
            goto _L___12;
          }
        } else {
          _L___12: /* CIL Label */ 
#line 1738
          if (currentFloorID < 1) {
#line 1738
            if (respectInLiftCalls) {
#line 1738
              if (floorButtons_1) {
#line 1741
                retValue_acc = 1;
#line 1743
                return (retValue_acc);
              } else {
                goto _L___10;
              }
            } else {
              goto _L___10;
            }
          } else {
            _L___10: /* CIL Label */ 
#line 1745
            if (currentFloorID < 2) {
#line 1745
              if (respectFloorCalls) {
                {
#line 1745
                tmp___2 = isFloorCalling(2);
                }
#line 1745
                if (tmp___2) {
#line 1748
                  retValue_acc = 1;
#line 1750
                  return (retValue_acc);
                } else {
                  goto _L___8;
                }
              } else {
                goto _L___8;
              }
            } else {
              _L___8: /* CIL Label */ 
#line 1752
              if (currentFloorID < 2) {
#line 1752
                if (respectInLiftCalls) {
#line 1752
                  if (floorButtons_2) {
#line 1755
                    retValue_acc = 1;
#line 1757
                    return (retValue_acc);
                  } else {
                    goto _L___6;
                  }
                } else {
                  goto _L___6;
                }
              } else {
                _L___6: /* CIL Label */ 
#line 1759
                if (currentFloorID < 3) {
#line 1759
                  if (respectFloorCalls) {
                    {
#line 1759
                    tmp___1 = isFloorCalling(3);
                    }
#line 1759
                    if (tmp___1) {
#line 1762
                      retValue_acc = 1;
#line 1764
                      return (retValue_acc);
                    } else {
                      goto _L___4;
                    }
                  } else {
                    goto _L___4;
                  }
                } else {
                  _L___4: /* CIL Label */ 
#line 1766
                  if (currentFloorID < 3) {
#line 1766
                    if (respectInLiftCalls) {
#line 1766
                      if (floorButtons_3) {
#line 1769
                        retValue_acc = 1;
#line 1771
                        return (retValue_acc);
                      } else {
                        goto _L___2;
                      }
                    } else {
                      goto _L___2;
                    }
                  } else {
                    _L___2: /* CIL Label */ 
#line 1773
                    if (currentFloorID < 4) {
#line 1773
                      if (respectFloorCalls) {
                        {
#line 1773
                        tmp___0 = isFloorCalling(4);
                        }
#line 1773
                        if (tmp___0) {
#line 1776
                          retValue_acc = 1;
#line 1778
                          return (retValue_acc);
                        } else {
                          goto _L___0;
                        }
                      } else {
                        goto _L___0;
                      }
                    } else {
                      _L___0: /* CIL Label */ 
#line 1780
                      if (currentFloorID < 4) {
#line 1780
                        if (respectInLiftCalls) {
#line 1780
                          if (floorButtons_4) {
#line 1783
                            retValue_acc = 1;
#line 1785
                            return (retValue_acc);
                          } else {
#line 1789
                            retValue_acc = 0;
#line 1791
                            return (retValue_acc);
                          }
                        } else {
#line 1789
                          retValue_acc = 0;
#line 1791
                          return (retValue_acc);
                        }
                      } else {
#line 1789 "Elevator.c"
                        retValue_acc = 0;
#line 1791
                        return (retValue_acc);
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  } else {
#line 224 "Elevator.c"
    if (currentFloorID == 0) {
#line 1799 "Elevator.c"
      retValue_acc = 0;
#line 1801
      return (retValue_acc);
    } else {

    }
#line 224
    if (currentFloorID > 0) {
#line 224
      if (respectFloorCalls) {
        {
#line 224 "Elevator.c"
        tmp___9 = isFloorCalling(0);
        }
#line 224 "Elevator.c"
        if (tmp___9) {
#line 1807 "Elevator.c"
          retValue_acc = 1;
#line 1809
          return (retValue_acc);
        } else {
          goto _L___34;
        }
      } else {
        goto _L___34;
      }
    } else {
      _L___34: /* CIL Label */ 
#line 1811
      if (currentFloorID > 0) {
#line 1811
        if (respectInLiftCalls) {
#line 1811
          if (floorButtons_0) {
#line 1814
            retValue_acc = 1;
#line 1816
            return (retValue_acc);
          } else {
            goto _L___32;
          }
        } else {
          goto _L___32;
        }
      } else {
        _L___32: /* CIL Label */ 
#line 1818
        if (currentFloorID > 1) {
#line 1818
          if (respectFloorCalls) {
            {
#line 1818
            tmp___8 = isFloorCalling(1);
            }
#line 1818
            if (tmp___8) {
#line 1821
              retValue_acc = 1;
#line 1823
              return (retValue_acc);
            } else {
              goto _L___30;
            }
          } else {
            goto _L___30;
          }
        } else {
          _L___30: /* CIL Label */ 
#line 1825
          if (currentFloorID > 1) {
#line 1825
            if (respectInLiftCalls) {
#line 1825
              if (floorButtons_1) {
#line 1828
                retValue_acc = 1;
#line 1830
                return (retValue_acc);
              } else {
                goto _L___28;
              }
            } else {
              goto _L___28;
            }
          } else {
            _L___28: /* CIL Label */ 
#line 1832
            if (currentFloorID > 2) {
#line 1832
              if (respectFloorCalls) {
                {
#line 1832
                tmp___7 = isFloorCalling(2);
                }
#line 1832
                if (tmp___7) {
#line 1835
                  retValue_acc = 1;
#line 1837
                  return (retValue_acc);
                } else {
                  goto _L___26;
                }
              } else {
                goto _L___26;
              }
            } else {
              _L___26: /* CIL Label */ 
#line 1839
              if (currentFloorID > 2) {
#line 1839
                if (respectInLiftCalls) {
#line 1839
                  if (floorButtons_2) {
#line 1842
                    retValue_acc = 1;
#line 1844
                    return (retValue_acc);
                  } else {
                    goto _L___24;
                  }
                } else {
                  goto _L___24;
                }
              } else {
                _L___24: /* CIL Label */ 
#line 1846
                if (currentFloorID > 3) {
#line 1846
                  if (respectFloorCalls) {
                    {
#line 1846
                    tmp___6 = isFloorCalling(3);
                    }
#line 1846
                    if (tmp___6) {
#line 1849
                      retValue_acc = 1;
#line 1851
                      return (retValue_acc);
                    } else {
                      goto _L___22;
                    }
                  } else {
                    goto _L___22;
                  }
                } else {
                  _L___22: /* CIL Label */ 
#line 1853
                  if (currentFloorID > 3) {
#line 1853
                    if (respectInLiftCalls) {
#line 1853
                      if (floorButtons_3) {
#line 1856
                        retValue_acc = 1;
#line 1858
                        return (retValue_acc);
                      } else {
                        goto _L___20;
                      }
                    } else {
                      goto _L___20;
                    }
                  } else {
                    _L___20: /* CIL Label */ 
#line 1860
                    if (currentFloorID > 4) {
#line 1860
                      if (respectFloorCalls) {
                        {
#line 1860
                        tmp___5 = isFloorCalling(4);
                        }
#line 1860
                        if (tmp___5) {
#line 1863
                          retValue_acc = 1;
#line 1865
                          return (retValue_acc);
                        } else {
                          goto _L___18;
                        }
                      } else {
                        goto _L___18;
                      }
                    } else {
                      _L___18: /* CIL Label */ 
#line 1867
                      if (currentFloorID > 4) {
#line 1867
                        if (respectInLiftCalls) {
#line 1867
                          if (floorButtons_4) {
#line 1870
                            retValue_acc = 1;
#line 1872
                            return (retValue_acc);
                          } else {
#line 1876
                            retValue_acc = 0;
#line 1878
                            return (retValue_acc);
                          }
                        } else {
#line 1876
                          retValue_acc = 0;
#line 1878
                          return (retValue_acc);
                        }
                      } else {
#line 1876 "Elevator.c"
                        retValue_acc = 0;
#line 1878
                        return (retValue_acc);
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
#line 1885 "Elevator.c"
  return (retValue_acc);
}
}
#line 242 "Elevator.c"
int stopRequestedInDirection__wrappee__twothirdsfull(int dir , int respectFloorCalls ,
                                                     int respectInLiftCalls ) 
{ int retValue_acc ;
  int overload ;
  int buttonPressed ;
  int tmp ;
  int __cil_tmp8 ;
  int __cil_tmp9 ;

  {
  {
#line 243
  __cil_tmp8 = maximumWeight * 2;
#line 243
  __cil_tmp9 = __cil_tmp8 / 3;
#line 243
  overload = weight > __cil_tmp9;
#line 244
  tmp = isAnyLiftButtonPressed();
#line 244
  buttonPressed = tmp;
  }
#line 245
  if (overload) {
#line 245 "Elevator.c"
    if (buttonPressed) {
      {
#line 1918
      retValue_acc = stopRequestedInDirection__wrappee__weight(dir, 0, respectInLiftCalls);
      }
#line 1920
      return (retValue_acc);
    } else {
      {
#line 1924
      retValue_acc = stopRequestedInDirection__wrappee__weight(dir, respectFloorCalls,
                                                               respectInLiftCalls);
      }
#line 1926
      return (retValue_acc);
    }
  } else {
    {
#line 1924 "Elevator.c"
    retValue_acc = stopRequestedInDirection__wrappee__weight(dir, respectFloorCalls,
                                                             respectInLiftCalls);
    }
#line 1926
    return (retValue_acc);
  }
#line 1933 "Elevator.c"
  return (retValue_acc);
}
}
#line 251 "Elevator.c"
int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls ) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int __cil_tmp7 ;
  int __cil_tmp8 ;

  {
  {
#line 256
  tmp___0 = isExecutiveFloorCalling();
  }
#line 256 "Elevator.c"
  if (tmp___0) {
    {
#line 1958
    tmp = getCurrentFloorID();
#line 1958
    __cil_tmp7 = dir == 1;
#line 1958
    __cil_tmp8 = tmp < executiveFloor;
#line 1958
    retValue_acc = __cil_tmp8 == __cil_tmp7;
    }
#line 1960
    return (retValue_acc);
  } else {
    {
#line 1966 "Elevator.c"
    retValue_acc = stopRequestedInDirection__wrappee__twothirdsfull(dir, respectFloorCalls,
                                                                    respectInLiftCalls);
    }
#line 1968
    return (retValue_acc);
  }
#line 1975 "Elevator.c"
  return (retValue_acc);
}
}
#line 259 "Elevator.c"
int isAnyLiftButtonPressed(void) 
{ int retValue_acc ;

  {
#line 265 "Elevator.c"
  if (floorButtons_0) {
#line 1998
    retValue_acc = 1;
#line 2000
    return (retValue_acc);
  } else {
#line 2002
    if (floorButtons_1) {
#line 2005
      retValue_acc = 1;
#line 2007
      return (retValue_acc);
    } else {
#line 2009
      if (floorButtons_2) {
#line 2012
        retValue_acc = 1;
#line 2014
        return (retValue_acc);
      } else {
#line 2016
        if (floorButtons_3) {
#line 2019
          retValue_acc = 1;
#line 2021
          return (retValue_acc);
        } else {
#line 2023
          if (floorButtons_4) {
#line 2026
            retValue_acc = 1;
#line 2028
            return (retValue_acc);
          } else {
#line 2032 "Elevator.c"
            retValue_acc = 0;
#line 2034
            return (retValue_acc);
          }
        }
      }
    }
  }
#line 2041 "Elevator.c"
  return (retValue_acc);
}
}
#line 268 "Elevator.c"
void continueInDirection(int dir ) 
{ int tmp ;

  {
#line 269
  currentHeading = dir;
#line 270
  if (currentHeading == 1) {
    {
#line 275
    tmp = isTopFloor(currentFloorID);
    }
#line 275
    if (tmp) {
#line 273
      currentHeading = 0;
    } else {

    }
  } else {
#line 280
    if (currentFloorID == 0) {
#line 278
      currentHeading = 1;
    } else {

    }
  }
#line 281
  if (currentHeading == 1) {
#line 282
    currentFloorID = currentFloorID + 1;
  } else {
#line 284
    currentFloorID = currentFloorID - 1;
  }
#line 2087 "Elevator.c"
  return;
}
}
#line 288 "Elevator.c"
int stopRequestedAtCurrentFloor__wrappee__weight(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;

  {
  {
#line 295
  tmp___0 = isFloorCalling(currentFloorID);
  }
#line 295 "Elevator.c"
  if (tmp___0) {
#line 2108
    retValue_acc = 1;
#line 2110
    return (retValue_acc);
  } else {
    {
#line 2112 "Elevator.c"
    tmp = buttonForFloorIsPressed(currentFloorID);
    }
#line 2112
    if (tmp) {
#line 2117
      retValue_acc = 1;
#line 2119
      return (retValue_acc);
    } else {
#line 2125
      retValue_acc = 0;
#line 2127
      return (retValue_acc);
    }
  }
#line 2134 "Elevator.c"
  return (retValue_acc);
}
}
#line 298 "Elevator.c"
int stopRequestedAtCurrentFloor__wrappee__twothirdsfull(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int __cil_tmp4 ;
  int __cil_tmp5 ;

  {
  {
#line 301
  __cil_tmp4 = maximumWeight * 2;
#line 301
  __cil_tmp5 = __cil_tmp4 / 3;
#line 301 "Elevator.c"
  if (weight > __cil_tmp5) {
    {
#line 2159
    tmp = getCurrentFloorID();
#line 2159
    tmp___0 = buttonForFloorIsPressed(tmp);
#line 2159
    retValue_acc = tmp___0 == 1;
    }
#line 2161
    return (retValue_acc);
  } else {
    {
#line 2165 "Elevator.c"
    retValue_acc = stopRequestedAtCurrentFloor__wrappee__weight();
    }
#line 2167
    return (retValue_acc);
  }
  }
#line 2174 "Elevator.c"
  return (retValue_acc);
}
}
#line 305 "Elevator.c"
int stopRequestedAtCurrentFloor(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;

  {
  {
#line 308
  tmp = isExecutiveFloorCalling();
  }
#line 308
  if (tmp) {
    {
#line 308 "Elevator.c"
    tmp___0 = getCurrentFloorID();
    }
#line 308 "Elevator.c"
    if (executiveFloor == tmp___0) {
      {
#line 2205
      retValue_acc = stopRequestedAtCurrentFloor__wrappee__twothirdsfull();
      }
#line 2207
      return (retValue_acc);
    } else {
#line 2199 "Elevator.c"
      retValue_acc = 0;
#line 2201
      return (retValue_acc);
    }
  } else {
    {
#line 2205 "Elevator.c"
    retValue_acc = stopRequestedAtCurrentFloor__wrappee__twothirdsfull();
    }
#line 2207
    return (retValue_acc);
  }
#line 2214 "Elevator.c"
  return (retValue_acc);
}
}
#line 311 "Elevator.c"
int getReverseHeading(int ofHeading ) 
{ int retValue_acc ;

  {
#line 314 "Elevator.c"
  if (ofHeading == 0) {
#line 2239
    retValue_acc = 1;
#line 2241
    return (retValue_acc);
  } else {
#line 2245 "Elevator.c"
    retValue_acc = 0;
#line 2247
    return (retValue_acc);
  }
#line 2254 "Elevator.c"
  return (retValue_acc);
}
}
#line 318 "Elevator.c"
void processWaitingOnFloor(int floorID ) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  int tmp___5 ;
  int tmp___6 ;
  int tmp___7 ;
  int tmp___8 ;
  int tmp___9 ;
  int tmp___10 ;

  {
  {
#line 324
  tmp___0 = isPersonOnFloor(0, floorID);
  }
#line 324
  if (tmp___0) {
    {
#line 320
    removePersonFromFloor(0, floorID);
#line 321
    tmp = getDestination(0);
#line 321
    pressInLiftFloorButton(tmp);
#line 322
    enterElevator(0);
    }
  } else {

  }
  {
#line 324
  tmp___2 = isPersonOnFloor(1, floorID);
  }
#line 324
  if (tmp___2) {
    {
#line 325
    removePersonFromFloor(1, floorID);
#line 326
    tmp___1 = getDestination(1);
#line 326
    pressInLiftFloorButton(tmp___1);
#line 327
    enterElevator(1);
    }
  } else {

  }
  {
#line 329
  tmp___4 = isPersonOnFloor(2, floorID);
  }
#line 329
  if (tmp___4) {
    {
#line 330
    removePersonFromFloor(2, floorID);
#line 331
    tmp___3 = getDestination(2);
#line 331
    pressInLiftFloorButton(tmp___3);
#line 332
    enterElevator(2);
    }
  } else {

  }
  {
#line 334
  tmp___6 = isPersonOnFloor(3, floorID);
  }
#line 334
  if (tmp___6) {
    {
#line 335
    removePersonFromFloor(3, floorID);
#line 336
    tmp___5 = getDestination(3);
#line 336
    pressInLiftFloorButton(tmp___5);
#line 337
    enterElevator(3);
    }
  } else {

  }
  {
#line 339
  tmp___8 = isPersonOnFloor(4, floorID);
  }
#line 339
  if (tmp___8) {
    {
#line 340
    removePersonFromFloor(4, floorID);
#line 341
    tmp___7 = getDestination(4);
#line 341
    pressInLiftFloorButton(tmp___7);
#line 342
    enterElevator(4);
    }
  } else {

  }
  {
#line 344
  tmp___10 = isPersonOnFloor(5, floorID);
  }
#line 344
  if (tmp___10) {
    {
#line 345
    removePersonFromFloor(5, floorID);
#line 346
    tmp___9 = getDestination(5);
#line 346
    pressInLiftFloorButton(tmp___9);
#line 347
    enterElevator(5);
    }
  } else {

  }
  {
#line 349
  resetCallOnFloor(floorID);
  }
#line 2332 "Elevator.c"
  return;
}
}
#line 353 "Elevator.c"
void timeShift__wrappee__executivefloor(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  int tmp___5 ;
  int tmp___6 ;
  int tmp___7 ;
  int tmp___8 ;
  int tmp___9 ;

  {
  {
#line 386
  tmp___9 = stopRequestedAtCurrentFloor();
  }
#line 386
  if (tmp___9) {
#line 358
    doorState = 1;
#line 360
    if (persons_0) {
      {
#line 360
      tmp = getDestination(0);
      }
#line 360
      if (tmp == currentFloorID) {
        {
#line 361
        leaveElevator(0);
        }
      } else {

      }
    } else {

    }
#line 361
    if (persons_1) {
      {
#line 361
      tmp___0 = getDestination(1);
      }
#line 361
      if (tmp___0 == currentFloorID) {
        {
#line 362
        leaveElevator(1);
        }
      } else {

      }
    } else {

    }
#line 362
    if (persons_2) {
      {
#line 362
      tmp___1 = getDestination(2);
      }
#line 362
      if (tmp___1 == currentFloorID) {
        {
#line 363
        leaveElevator(2);
        }
      } else {

      }
    } else {

    }
#line 363
    if (persons_3) {
      {
#line 363
      tmp___2 = getDestination(3);
      }
#line 363
      if (tmp___2 == currentFloorID) {
        {
#line 364
        leaveElevator(3);
        }
      } else {

      }
    } else {

    }
#line 364
    if (persons_4) {
      {
#line 364
      tmp___3 = getDestination(4);
      }
#line 364
      if (tmp___3 == currentFloorID) {
        {
#line 365
        leaveElevator(4);
        }
      } else {

      }
    } else {

    }
#line 365
    if (persons_5) {
      {
#line 365
      tmp___4 = getDestination(5);
      }
#line 365
      if (tmp___4 == currentFloorID) {
        {
#line 366
        leaveElevator(5);
        }
      } else {

      }
    } else {

    }
    {
#line 366
    processWaitingOnFloor(currentFloorID);
#line 367
    resetFloorButton(currentFloorID);
    }
  } else {
#line 373
    if (doorState == 1) {
#line 370
      doorState = 0;
    } else {

    }
    {
#line 373
    tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
    }
#line 373
    if (tmp___8) {
      {
#line 376
      continueInDirection(currentHeading);
      }
    } else {
      {
#line 377
      tmp___6 = getReverseHeading(currentHeading);
#line 377
      tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
      }
#line 377
      if (tmp___7) {
        {
#line 380
        tmp___5 = getReverseHeading(currentHeading);
#line 380
        continueInDirection(tmp___5);
        }
      } else {
        {
#line 384
        continueInDirection(currentHeading);
        }
      }
    }
  }
#line 2395 "Elevator.c"
  return;
}
}
#line 2397
void __utac_acc__Specification3_spec__1(void) ;
#line 2400
void __utac_acc__Specification3_spec__2(void) ;
#line 391 "Elevator.c"
void timeShift(void) 
{ int tmp ;

  {
  {
#line 2411 "Elevator.c"
  __utac_acc__Specification3_spec__1();
#line 397 "Elevator.c"
  tmp = areDoorsOpen();
  }
#line 397
  if (tmp) {
#line 397
    if (weight > maximumWeight) {
#line 393
      blocked = 1;
    } else {
      {
#line 395
      blocked = 0;
#line 396
      timeShift__wrappee__executivefloor();
      }
    }
  } else {
    {
#line 395
    blocked = 0;
#line 396
    timeShift__wrappee__executivefloor();
    }
  }
  {
#line 2433 "Elevator.c"
  __utac_acc__Specification3_spec__2();
  }
#line 2439
  return;
}
}
#line 400 "Elevator.c"
void printState__wrappee__executivefloor(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  char const   * __restrict  __cil_tmp6 ;
  char const   * __restrict  __cil_tmp7 ;
  char const   * __restrict  __cil_tmp8 ;
  char const   * __restrict  __cil_tmp9 ;
  char const   * __restrict  __cil_tmp10 ;
  char const   * __restrict  __cil_tmp11 ;
  char const   * __restrict  __cil_tmp12 ;
  char const   * __restrict  __cil_tmp13 ;
  char const   * __restrict  __cil_tmp14 ;
  char const   * __restrict  __cil_tmp15 ;
  char const   * __restrict  __cil_tmp16 ;
  char const   * __restrict  __cil_tmp17 ;
  char const   * __restrict  __cil_tmp18 ;
  char const   * __restrict  __cil_tmp19 ;
  char const   * __restrict  __cil_tmp20 ;
  char const   * __restrict  __cil_tmp21 ;
  char const   * __restrict  __cil_tmp22 ;
  char const   * __restrict  __cil_tmp23 ;
  char const   * __restrict  __cil_tmp24 ;
  char const   * __restrict  __cil_tmp25 ;
  char const   * __restrict  __cil_tmp26 ;

  {
  {
#line 401
  __cil_tmp6 = (char const   * __restrict  )"Elevator ";
#line 401
  printf(__cil_tmp6);
  }
#line 402
  if (doorState) {
    {
#line 403
    __cil_tmp7 = (char const   * __restrict  )"[_]";
#line 403
    printf(__cil_tmp7);
    }
  } else {
    {
#line 404
    __cil_tmp8 = (char const   * __restrict  )"[] ";
#line 404
    printf(__cil_tmp8);
    }
  }
  {
#line 404
  __cil_tmp9 = (char const   * __restrict  )" at ";
#line 404
  printf(__cil_tmp9);
#line 405
  __cil_tmp10 = (char const   * __restrict  )"%i";
#line 405
  printf(__cil_tmp10, currentFloorID);
#line 406
  __cil_tmp11 = (char const   * __restrict  )" heading ";
#line 406
  printf(__cil_tmp11);
  }
#line 407
  if (currentHeading) {
    {
#line 408
    __cil_tmp12 = (char const   * __restrict  )"up";
#line 408
    printf(__cil_tmp12);
    }
  } else {
    {
#line 409
    __cil_tmp13 = (char const   * __restrict  )"down";
#line 409
    printf(__cil_tmp13);
    }
  }
  {
#line 409
  __cil_tmp14 = (char const   * __restrict  )" IL_p:";
#line 409
  printf(__cil_tmp14);
  }
#line 410
  if (floorButtons_0) {
    {
#line 411
    __cil_tmp15 = (char const   * __restrict  )" %i";
#line 411
    printf(__cil_tmp15, 0);
    }
  } else {

  }
#line 411
  if (floorButtons_1) {
    {
#line 412
    __cil_tmp16 = (char const   * __restrict  )" %i";
#line 412
    printf(__cil_tmp16, 1);
    }
  } else {

  }
#line 412
  if (floorButtons_2) {
    {
#line 413
    __cil_tmp17 = (char const   * __restrict  )" %i";
#line 413
    printf(__cil_tmp17, 2);
    }
  } else {

  }
#line 413
  if (floorButtons_3) {
    {
#line 414
    __cil_tmp18 = (char const   * __restrict  )" %i";
#line 414
    printf(__cil_tmp18, 3);
    }
  } else {

  }
#line 414
  if (floorButtons_4) {
    {
#line 415
    __cil_tmp19 = (char const   * __restrict  )" %i";
#line 415
    printf(__cil_tmp19, 4);
    }
  } else {

  }
  {
#line 415
  __cil_tmp20 = (char const   * __restrict  )" F_p:";
#line 415
  printf(__cil_tmp20);
#line 416
  tmp = isFloorCalling(0);
  }
#line 416
  if (tmp) {
    {
#line 417
    __cil_tmp21 = (char const   * __restrict  )" %i";
#line 417
    printf(__cil_tmp21, 0);
    }
  } else {

  }
  {
#line 417
  tmp___0 = isFloorCalling(1);
  }
#line 417
  if (tmp___0) {
    {
#line 418
    __cil_tmp22 = (char const   * __restrict  )" %i";
#line 418
    printf(__cil_tmp22, 1);
    }
  } else {

  }
  {
#line 418
  tmp___1 = isFloorCalling(2);
  }
#line 418
  if (tmp___1) {
    {
#line 419
    __cil_tmp23 = (char const   * __restrict  )" %i";
#line 419
    printf(__cil_tmp23, 2);
    }
  } else {

  }
  {
#line 419
  tmp___2 = isFloorCalling(3);
  }
#line 419
  if (tmp___2) {
    {
#line 420
    __cil_tmp24 = (char const   * __restrict  )" %i";
#line 420
    printf(__cil_tmp24, 3);
    }
  } else {

  }
  {
#line 420
  tmp___3 = isFloorCalling(4);
  }
#line 420
  if (tmp___3) {
    {
#line 421
    __cil_tmp25 = (char const   * __restrict  )" %i";
#line 421
    printf(__cil_tmp25, 4);
    }
  } else {

  }
  {
#line 421
  __cil_tmp26 = (char const   * __restrict  )"\n";
#line 421
  printf(__cil_tmp26);
  }
#line 2509 "Elevator.c"
  return;
}
}
#line 424 "Elevator.c"
void printState(void) 
{ int tmp ;
  char const   * __restrict  __cil_tmp2 ;

  {
  {
#line 426
  tmp = isBlocked();
  }
#line 426
  if (tmp) {
    {
#line 427
    __cil_tmp2 = (char const   * __restrict  )"Blocked ";
#line 427
    printf(__cil_tmp2);
    }
  } else {

  }
  {
#line 426
  printState__wrappee__executivefloor();
  }
#line 2532 "Elevator.c"
  return;
}
}
#line 430 "Elevator.c"
int existInLiftCallsInDirection(int d ) 
{ int retValue_acc ;
  int i ;
  int i___0 ;

  {
#line 451
  if (d == 1) {
#line 432 "Elevator.c"
    i = 0;
#line 433
    i = currentFloorID + 1;
    {
#line 433
    while (1) {
      while_4_continue: /* CIL Label */ ;
#line 433
      if (i < 5) {

      } else {
        goto while_4_break;
      }
#line 439
      if (i == 0) {
#line 439 "Elevator.c"
        if (floorButtons_0) {
#line 2560
          retValue_acc = 1;
#line 2562
          return (retValue_acc);
        } else {
          goto _L___2;
        }
      } else {
        _L___2: /* CIL Label */ 
#line 2564
        if (i == 1) {
#line 2564
          if (floorButtons_1) {
#line 2567
            retValue_acc = 1;
#line 2569
            return (retValue_acc);
          } else {
            goto _L___1;
          }
        } else {
          _L___1: /* CIL Label */ 
#line 2571
          if (i == 2) {
#line 2571
            if (floorButtons_2) {
#line 2574
              retValue_acc = 1;
#line 2576
              return (retValue_acc);
            } else {
              goto _L___0;
            }
          } else {
            _L___0: /* CIL Label */ 
#line 2578
            if (i == 3) {
#line 2578
              if (floorButtons_3) {
#line 2581
                retValue_acc = 1;
#line 2583
                return (retValue_acc);
              } else {
                goto _L;
              }
            } else {
              _L: /* CIL Label */ 
#line 2585
              if (i == 4) {
#line 2585
                if (floorButtons_4) {
#line 2588 "Elevator.c"
                  retValue_acc = 1;
#line 2590
                  return (retValue_acc);
                } else {

                }
              } else {

              }
            }
          }
        }
      }
#line 433
      i = i + 1;
    }
    while_4_break: /* CIL Label */ ;
    }
  } else {
#line 2592 "Elevator.c"
    if (d == 0) {
#line 441
      i___0 = 0;
#line 442
      i___0 = currentFloorID - 1;
      {
#line 442
      while (1) {
        while_5_continue: /* CIL Label */ ;
#line 442
        if (i___0 >= 0) {

        } else {
          goto while_5_break;
        }
#line 442
        i___0 = currentFloorID + 1;
        {
#line 442
        while (1) {
          while_6_continue: /* CIL Label */ ;
#line 442
          if (i___0 < 5) {

          } else {
            goto while_6_break;
          }
#line 449
          if (i___0 == 0) {
#line 449 "Elevator.c"
            if (floorButtons_0) {
#line 2604
              retValue_acc = 1;
#line 2606
              return (retValue_acc);
            } else {
              goto _L___6;
            }
          } else {
            _L___6: /* CIL Label */ 
#line 2608
            if (i___0 == 1) {
#line 2608
              if (floorButtons_1) {
#line 2611
                retValue_acc = 1;
#line 2613
                return (retValue_acc);
              } else {
                goto _L___5;
              }
            } else {
              _L___5: /* CIL Label */ 
#line 2615
              if (i___0 == 2) {
#line 2615
                if (floorButtons_2) {
#line 2618
                  retValue_acc = 1;
#line 2620
                  return (retValue_acc);
                } else {
                  goto _L___4;
                }
              } else {
                _L___4: /* CIL Label */ 
#line 2622
                if (i___0 == 3) {
#line 2622
                  if (floorButtons_3) {
#line 2625
                    retValue_acc = 1;
#line 2627
                    return (retValue_acc);
                  } else {
                    goto _L___3;
                  }
                } else {
                  _L___3: /* CIL Label */ 
#line 2629
                  if (i___0 == 4) {
#line 2629
                    if (floorButtons_4) {
#line 2632 "Elevator.c"
                      retValue_acc = 1;
#line 2634
                      return (retValue_acc);
                    } else {

                    }
                  } else {

                  }
                }
              }
            }
          }
#line 442
          i___0 = i___0 + 1;
        }
        while_6_break: /* CIL Label */ ;
        }
#line 442
        i___0 = i___0 - 1;
      }
      while_5_break: /* CIL Label */ ;
      }
    } else {

    }
  }
#line 2639 "Elevator.c"
  retValue_acc = 0;
#line 2641
  return (retValue_acc);
#line 2648
  return (retValue_acc);
}
}
#line 453 "Elevator.c"
int isExecutiveFloorCalling(void) 
{ int retValue_acc ;

  {
  {
#line 2670 "Elevator.c"
  retValue_acc = isFloorCalling(executiveFloor);
  }
#line 2672
  return (retValue_acc);
#line 2679
  return (retValue_acc);
}
}
#line 457 "Elevator.c"
int isExecutiveFloor(int floorID ) 
{ int retValue_acc ;

  {
#line 2701 "Elevator.c"
  retValue_acc = executiveFloor == floorID;
#line 2703
  return (retValue_acc);
#line 2710
  return (retValue_acc);
}
}
#line 1 "Floor.o"
#pragma merger(0,"Floor.i","")
#line 16 "Floor.h"
void callOnFloor(int floorID ) ;
#line 9 "Floor.c"
int calls_0  ;
#line 11 "Floor.c"
int calls_1  ;
#line 13 "Floor.c"
int calls_2  ;
#line 15 "Floor.c"
int calls_3  ;
#line 17 "Floor.c"
int calls_4  ;
#line 20 "Floor.c"
int personOnFloor_0_0  ;
#line 22 "Floor.c"
int personOnFloor_0_1  ;
#line 24 "Floor.c"
int personOnFloor_0_2  ;
#line 26 "Floor.c"
int personOnFloor_0_3  ;
#line 28 "Floor.c"
int personOnFloor_0_4  ;
#line 30 "Floor.c"
int personOnFloor_1_0  ;
#line 32 "Floor.c"
int personOnFloor_1_1  ;
#line 34 "Floor.c"
int personOnFloor_1_2  ;
#line 36 "Floor.c"
int personOnFloor_1_3  ;
#line 38 "Floor.c"
int personOnFloor_1_4  ;
#line 40 "Floor.c"
int personOnFloor_2_0  ;
#line 42 "Floor.c"
int personOnFloor_2_1  ;
#line 44 "Floor.c"
int personOnFloor_2_2  ;
#line 46 "Floor.c"
int personOnFloor_2_3  ;
#line 48 "Floor.c"
int personOnFloor_2_4  ;
#line 50 "Floor.c"
int personOnFloor_3_0  ;
#line 52 "Floor.c"
int personOnFloor_3_1  ;
#line 54 "Floor.c"
int personOnFloor_3_2  ;
#line 56 "Floor.c"
int personOnFloor_3_3  ;
#line 58 "Floor.c"
int personOnFloor_3_4  ;
#line 60 "Floor.c"
int personOnFloor_4_0  ;
#line 62 "Floor.c"
int personOnFloor_4_1  ;
#line 64 "Floor.c"
int personOnFloor_4_2  ;
#line 66 "Floor.c"
int personOnFloor_4_3  ;
#line 68 "Floor.c"
int personOnFloor_4_4  ;
#line 70 "Floor.c"
int personOnFloor_5_0  ;
#line 72 "Floor.c"
int personOnFloor_5_1  ;
#line 74 "Floor.c"
int personOnFloor_5_2  ;
#line 76 "Floor.c"
int personOnFloor_5_3  ;
#line 78 "Floor.c"
int personOnFloor_5_4  ;
#line 81 "Floor.c"
void initFloors(void) 
{ 

  {
#line 82
  calls_0 = 0;
#line 83
  calls_1 = 0;
#line 84
  calls_2 = 0;
#line 85
  calls_3 = 0;
#line 86
  calls_4 = 0;
#line 87
  personOnFloor_0_0 = 0;
#line 88
  personOnFloor_0_1 = 0;
#line 89
  personOnFloor_0_2 = 0;
#line 90
  personOnFloor_0_3 = 0;
#line 91
  personOnFloor_0_4 = 0;
#line 92
  personOnFloor_1_0 = 0;
#line 93
  personOnFloor_1_1 = 0;
#line 94
  personOnFloor_1_2 = 0;
#line 95
  personOnFloor_1_3 = 0;
#line 96
  personOnFloor_1_4 = 0;
#line 97
  personOnFloor_2_0 = 0;
#line 98
  personOnFloor_2_1 = 0;
#line 99
  personOnFloor_2_2 = 0;
#line 100
  personOnFloor_2_3 = 0;
#line 101
  personOnFloor_2_4 = 0;
#line 102
  personOnFloor_3_0 = 0;
#line 103
  personOnFloor_3_1 = 0;
#line 104
  personOnFloor_3_2 = 0;
#line 105
  personOnFloor_3_3 = 0;
#line 106
  personOnFloor_3_4 = 0;
#line 107
  personOnFloor_4_0 = 0;
#line 108
  personOnFloor_4_1 = 0;
#line 109
  personOnFloor_4_2 = 0;
#line 110
  personOnFloor_4_3 = 0;
#line 111
  personOnFloor_4_4 = 0;
#line 112
  personOnFloor_5_0 = 0;
#line 113
  personOnFloor_5_1 = 0;
#line 114
  personOnFloor_5_2 = 0;
#line 115
  personOnFloor_5_3 = 0;
#line 116
  personOnFloor_5_4 = 0;
#line 1120 "Floor.c"
  return;
}
}
#line 120 "Floor.c"
int isFloorCalling(int floorID ) 
{ int retValue_acc ;

  {
#line 126 "Floor.c"
  if (floorID == 0) {
#line 1139
    retValue_acc = calls_0;
#line 1141
    return (retValue_acc);
  } else {
#line 1143
    if (floorID == 1) {
#line 1146
      retValue_acc = calls_1;
#line 1148
      return (retValue_acc);
    } else {
#line 1150
      if (floorID == 2) {
#line 1153
        retValue_acc = calls_2;
#line 1155
        return (retValue_acc);
      } else {
#line 1157
        if (floorID == 3) {
#line 1160
          retValue_acc = calls_3;
#line 1162
          return (retValue_acc);
        } else {
#line 1164
          if (floorID == 4) {
#line 1167 "Floor.c"
            retValue_acc = calls_4;
#line 1169
            return (retValue_acc);
          } else {

          }
        }
      }
    }
  }
#line 1174 "Floor.c"
  retValue_acc = 0;
#line 1176
  return (retValue_acc);
#line 1183
  return (retValue_acc);
}
}
#line 130 "Floor.c"
void resetCallOnFloor(int floorID ) 
{ 

  {
#line 136
  if (floorID == 0) {
#line 137
    calls_0 = 0;
  } else {
#line 138
    if (floorID == 1) {
#line 139
      calls_1 = 0;
    } else {
#line 140
      if (floorID == 2) {
#line 141
        calls_2 = 0;
      } else {
#line 142
        if (floorID == 3) {
#line 143
          calls_3 = 0;
        } else {
#line 144
          if (floorID == 4) {
#line 145
            calls_4 = 0;
          } else {

          }
        }
      }
    }
  }
#line 1216 "Floor.c"
  return;
}
}
#line 139 "Floor.c"
void callOnFloor(int floorID ) 
{ 

  {
#line 145
  if (floorID == 0) {
#line 146
    calls_0 = 1;
  } else {
#line 147
    if (floorID == 1) {
#line 148
      calls_1 = 1;
    } else {
#line 149
      if (floorID == 2) {
#line 150
        calls_2 = 1;
      } else {
#line 151
        if (floorID == 3) {
#line 152
          calls_3 = 1;
        } else {
#line 153
          if (floorID == 4) {
#line 154
            calls_4 = 1;
          } else {

          }
        }
      }
    }
  }
#line 1245 "Floor.c"
  return;
}
}
#line 148 "Floor.c"
int isPersonOnFloor(int person , int floor ) 
{ int retValue_acc ;

  {
#line 185
  if (floor == 0) {
#line 156 "Floor.c"
    if (person == 0) {
#line 1267
      retValue_acc = personOnFloor_0_0;
#line 1269
      return (retValue_acc);
    } else {
#line 1271
      if (person == 1) {
#line 1274
        retValue_acc = personOnFloor_1_0;
#line 1276
        return (retValue_acc);
      } else {
#line 1278
        if (person == 2) {
#line 1281
          retValue_acc = personOnFloor_2_0;
#line 1283
          return (retValue_acc);
        } else {
#line 1285
          if (person == 3) {
#line 1288
            retValue_acc = personOnFloor_3_0;
#line 1290
            return (retValue_acc);
          } else {
#line 1292
            if (person == 4) {
#line 1295
              retValue_acc = personOnFloor_4_0;
#line 1297
              return (retValue_acc);
            } else {
#line 1299
              if (person == 5) {
#line 1302
                retValue_acc = personOnFloor_5_0;
#line 1304
                return (retValue_acc);
              } else {

              }
            }
          }
        }
      }
    }
  } else {
#line 1306 "Floor.c"
    if (floor == 1) {
#line 163 "Floor.c"
      if (person == 0) {
#line 1312
        retValue_acc = personOnFloor_0_1;
#line 1314
        return (retValue_acc);
      } else {
#line 1316
        if (person == 1) {
#line 1319
          retValue_acc = personOnFloor_1_1;
#line 1321
          return (retValue_acc);
        } else {
#line 1323
          if (person == 2) {
#line 1326
            retValue_acc = personOnFloor_2_1;
#line 1328
            return (retValue_acc);
          } else {
#line 1330
            if (person == 3) {
#line 1333
              retValue_acc = personOnFloor_3_1;
#line 1335
              return (retValue_acc);
            } else {
#line 1337
              if (person == 4) {
#line 1340
                retValue_acc = personOnFloor_4_1;
#line 1342
                return (retValue_acc);
              } else {
#line 1344
                if (person == 5) {
#line 1347
                  retValue_acc = personOnFloor_5_1;
#line 1349
                  return (retValue_acc);
                } else {

                }
              }
            }
          }
        }
      }
    } else {
#line 1351 "Floor.c"
      if (floor == 2) {
#line 170 "Floor.c"
        if (person == 0) {
#line 1357
          retValue_acc = personOnFloor_0_2;
#line 1359
          return (retValue_acc);
        } else {
#line 1361
          if (person == 1) {
#line 1364
            retValue_acc = personOnFloor_1_2;
#line 1366
            return (retValue_acc);
          } else {
#line 1368
            if (person == 2) {
#line 1371
              retValue_acc = personOnFloor_2_2;
#line 1373
              return (retValue_acc);
            } else {
#line 1375
              if (person == 3) {
#line 1378
                retValue_acc = personOnFloor_3_2;
#line 1380
                return (retValue_acc);
              } else {
#line 1382
                if (person == 4) {
#line 1385
                  retValue_acc = personOnFloor_4_2;
#line 1387
                  return (retValue_acc);
                } else {
#line 1389
                  if (person == 5) {
#line 1392
                    retValue_acc = personOnFloor_5_2;
#line 1394
                    return (retValue_acc);
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
#line 1396 "Floor.c"
        if (floor == 3) {
#line 177 "Floor.c"
          if (person == 0) {
#line 1402
            retValue_acc = personOnFloor_0_3;
#line 1404
            return (retValue_acc);
          } else {
#line 1406
            if (person == 1) {
#line 1409
              retValue_acc = personOnFloor_1_3;
#line 1411
              return (retValue_acc);
            } else {
#line 1413
              if (person == 2) {
#line 1416
                retValue_acc = personOnFloor_2_3;
#line 1418
                return (retValue_acc);
              } else {
#line 1420
                if (person == 3) {
#line 1423
                  retValue_acc = personOnFloor_3_3;
#line 1425
                  return (retValue_acc);
                } else {
#line 1427
                  if (person == 4) {
#line 1430
                    retValue_acc = personOnFloor_4_3;
#line 1432
                    return (retValue_acc);
                  } else {
#line 1434
                    if (person == 5) {
#line 1437
                      retValue_acc = personOnFloor_5_3;
#line 1439
                      return (retValue_acc);
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
#line 1441 "Floor.c"
          if (floor == 4) {
#line 184 "Floor.c"
            if (person == 0) {
#line 1447
              retValue_acc = personOnFloor_0_4;
#line 1449
              return (retValue_acc);
            } else {
#line 1451
              if (person == 1) {
#line 1454
                retValue_acc = personOnFloor_1_4;
#line 1456
                return (retValue_acc);
              } else {
#line 1458
                if (person == 2) {
#line 1461
                  retValue_acc = personOnFloor_2_4;
#line 1463
                  return (retValue_acc);
                } else {
#line 1465
                  if (person == 3) {
#line 1468
                    retValue_acc = personOnFloor_3_4;
#line 1470
                    return (retValue_acc);
                  } else {
#line 1472
                    if (person == 4) {
#line 1475
                      retValue_acc = personOnFloor_4_4;
#line 1477
                      return (retValue_acc);
                    } else {
#line 1479
                      if (person == 5) {
#line 1482 "Floor.c"
                        retValue_acc = personOnFloor_5_4;
#line 1484
                        return (retValue_acc);
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
#line 1489 "Floor.c"
  retValue_acc = 0;
#line 1491
  return (retValue_acc);
#line 1498
  return (retValue_acc);
}
}
#line 188 "Floor.c"
void initPersonOnFloor(int person , int floor ) 
{ 

  {
#line 225
  if (floor == 0) {
#line 196
    if (person == 0) {
#line 197
      personOnFloor_0_0 = 1;
    } else {
#line 198
      if (person == 1) {
#line 199
        personOnFloor_1_0 = 1;
      } else {
#line 200
        if (person == 2) {
#line 201
          personOnFloor_2_0 = 1;
        } else {
#line 202
          if (person == 3) {
#line 203
            personOnFloor_3_0 = 1;
          } else {
#line 204
            if (person == 4) {
#line 205
              personOnFloor_4_0 = 1;
            } else {
#line 206
              if (person == 5) {
#line 207
                personOnFloor_5_0 = 1;
              } else {

              }
            }
          }
        }
      }
    }
  } else {
#line 208
    if (floor == 1) {
#line 203
      if (person == 0) {
#line 204
        personOnFloor_0_1 = 1;
      } else {
#line 205
        if (person == 1) {
#line 206
          personOnFloor_1_1 = 1;
        } else {
#line 207
          if (person == 2) {
#line 208
            personOnFloor_2_1 = 1;
          } else {
#line 209
            if (person == 3) {
#line 210
              personOnFloor_3_1 = 1;
            } else {
#line 211
              if (person == 4) {
#line 212
                personOnFloor_4_1 = 1;
              } else {
#line 213
                if (person == 5) {
#line 214
                  personOnFloor_5_1 = 1;
                } else {

                }
              }
            }
          }
        }
      }
    } else {
#line 215
      if (floor == 2) {
#line 210
        if (person == 0) {
#line 211
          personOnFloor_0_2 = 1;
        } else {
#line 212
          if (person == 1) {
#line 213
            personOnFloor_1_2 = 1;
          } else {
#line 214
            if (person == 2) {
#line 215
              personOnFloor_2_2 = 1;
            } else {
#line 216
              if (person == 3) {
#line 217
                personOnFloor_3_2 = 1;
              } else {
#line 218
                if (person == 4) {
#line 219
                  personOnFloor_4_2 = 1;
                } else {
#line 220
                  if (person == 5) {
#line 221
                    personOnFloor_5_2 = 1;
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
#line 222
        if (floor == 3) {
#line 217
          if (person == 0) {
#line 218
            personOnFloor_0_3 = 1;
          } else {
#line 219
            if (person == 1) {
#line 220
              personOnFloor_1_3 = 1;
            } else {
#line 221
              if (person == 2) {
#line 222
                personOnFloor_2_3 = 1;
              } else {
#line 223
                if (person == 3) {
#line 224
                  personOnFloor_3_3 = 1;
                } else {
#line 225
                  if (person == 4) {
#line 226
                    personOnFloor_4_3 = 1;
                  } else {
#line 227
                    if (person == 5) {
#line 228
                      personOnFloor_5_3 = 1;
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
#line 229
          if (floor == 4) {
#line 224
            if (person == 0) {
#line 225
              personOnFloor_0_4 = 1;
            } else {
#line 226
              if (person == 1) {
#line 227
                personOnFloor_1_4 = 1;
              } else {
#line 228
                if (person == 2) {
#line 229
                  personOnFloor_2_4 = 1;
                } else {
#line 230
                  if (person == 3) {
#line 231
                    personOnFloor_3_4 = 1;
                  } else {
#line 232
                    if (person == 4) {
#line 233
                      personOnFloor_4_4 = 1;
                    } else {
#line 234
                      if (person == 5) {
#line 235
                        personOnFloor_5_4 = 1;
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
  {
#line 225
  callOnFloor(floor);
  }
#line 1598 "Floor.c"
  return;
}
}
#line 228 "Floor.c"
void removePersonFromFloor(int person , int floor ) 
{ 

  {
#line 265
  if (floor == 0) {
#line 236
    if (person == 0) {
#line 237
      personOnFloor_0_0 = 0;
    } else {
#line 238
      if (person == 1) {
#line 239
        personOnFloor_1_0 = 0;
      } else {
#line 240
        if (person == 2) {
#line 241
          personOnFloor_2_0 = 0;
        } else {
#line 242
          if (person == 3) {
#line 243
            personOnFloor_3_0 = 0;
          } else {
#line 244
            if (person == 4) {
#line 245
              personOnFloor_4_0 = 0;
            } else {
#line 246
              if (person == 5) {
#line 247
                personOnFloor_5_0 = 0;
              } else {

              }
            }
          }
        }
      }
    }
  } else {
#line 248
    if (floor == 1) {
#line 243
      if (person == 0) {
#line 244
        personOnFloor_0_1 = 0;
      } else {
#line 245
        if (person == 1) {
#line 246
          personOnFloor_1_1 = 0;
        } else {
#line 247
          if (person == 2) {
#line 248
            personOnFloor_2_1 = 0;
          } else {
#line 249
            if (person == 3) {
#line 250
              personOnFloor_3_1 = 0;
            } else {
#line 251
              if (person == 4) {
#line 252
                personOnFloor_4_1 = 0;
              } else {
#line 253
                if (person == 5) {
#line 254
                  personOnFloor_5_1 = 0;
                } else {

                }
              }
            }
          }
        }
      }
    } else {
#line 255
      if (floor == 2) {
#line 250
        if (person == 0) {
#line 251
          personOnFloor_0_2 = 0;
        } else {
#line 252
          if (person == 1) {
#line 253
            personOnFloor_1_2 = 0;
          } else {
#line 254
            if (person == 2) {
#line 255
              personOnFloor_2_2 = 0;
            } else {
#line 256
              if (person == 3) {
#line 257
                personOnFloor_3_2 = 0;
              } else {
#line 258
                if (person == 4) {
#line 259
                  personOnFloor_4_2 = 0;
                } else {
#line 260
                  if (person == 5) {
#line 261
                    personOnFloor_5_2 = 0;
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
#line 262
        if (floor == 3) {
#line 257
          if (person == 0) {
#line 258
            personOnFloor_0_3 = 0;
          } else {
#line 259
            if (person == 1) {
#line 260
              personOnFloor_1_3 = 0;
            } else {
#line 261
              if (person == 2) {
#line 262
                personOnFloor_2_3 = 0;
              } else {
#line 263
                if (person == 3) {
#line 264
                  personOnFloor_3_3 = 0;
                } else {
#line 265
                  if (person == 4) {
#line 266
                    personOnFloor_4_3 = 0;
                  } else {
#line 267
                    if (person == 5) {
#line 268
                      personOnFloor_5_3 = 0;
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
#line 269
          if (floor == 4) {
#line 264
            if (person == 0) {
#line 265
              personOnFloor_0_4 = 0;
            } else {
#line 266
              if (person == 1) {
#line 267
                personOnFloor_1_4 = 0;
              } else {
#line 268
                if (person == 2) {
#line 269
                  personOnFloor_2_4 = 0;
                } else {
#line 270
                  if (person == 3) {
#line 271
                    personOnFloor_3_4 = 0;
                  } else {
#line 272
                    if (person == 4) {
#line 273
                      personOnFloor_4_4 = 0;
                    } else {
#line 274
                      if (person == 5) {
#line 275
                        personOnFloor_5_4 = 0;
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
  {
#line 265
  resetCallOnFloor(floor);
  }
#line 1694 "Floor.c"
  return;
}
}
#line 268 "Floor.c"
int isTopFloor(int floorID ) 
{ int retValue_acc ;

  {
#line 1712 "Floor.c"
  retValue_acc = floorID == 4;
#line 1714
  return (retValue_acc);
#line 1721
  return (retValue_acc);
}
}
#line 1 "Specification3_spec.o"
#pragma merger(0,"Specification3_spec.i","")
#line 4 "wsllib.h"
void __automaton_fail(void) ;
#line 7 "Specification3_spec.c"
int expectedDirection  =    0;
#line 11 "Specification3_spec.c"
void __utac_acc__Specification3_spec__1(void) 
{ int currentFloorID___0 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  int tmp___5 ;
  int tmp___6 ;
  int tmp___7 ;
  int tmp___8 ;
  int tmp___9 ;
  int tmp___10 ;

  {
  {
#line 13
  expectedDirection = 0;
#line 14
  tmp = getCurrentFloorID();
#line 14
  currentFloorID___0 = tmp;
#line 15
  tmp___10 = getCurrentHeading();
  }
#line 15
  if (tmp___10 == 1) {
#line 21
    if (currentFloorID___0 < 0) {
      {
#line 21
      tmp___4 = buttonForFloorIsPressed(0);
      }
#line 21
      if (tmp___4) {
#line 22
        expectedDirection = 1;
      } else {
        goto _L___2;
      }
    } else {
      _L___2: /* CIL Label */ 
#line 23
      if (currentFloorID___0 < 1) {
        {
#line 23
        tmp___3 = buttonForFloorIsPressed(1);
        }
#line 23
        if (tmp___3) {
#line 24
          expectedDirection = 1;
        } else {
          goto _L___1;
        }
      } else {
        _L___1: /* CIL Label */ 
#line 25
        if (currentFloorID___0 < 2) {
          {
#line 25
          tmp___2 = buttonForFloorIsPressed(2);
          }
#line 25
          if (tmp___2) {
#line 26
            expectedDirection = 1;
          } else {
            goto _L___0;
          }
        } else {
          _L___0: /* CIL Label */ 
#line 27
          if (currentFloorID___0 < 3) {
            {
#line 27
            tmp___1 = buttonForFloorIsPressed(3);
            }
#line 27
            if (tmp___1) {
#line 28
              expectedDirection = 1;
            } else {
              goto _L;
            }
          } else {
            _L: /* CIL Label */ 
#line 29
            if (currentFloorID___0 < 4) {
              {
#line 29
              tmp___0 = buttonForFloorIsPressed(4);
              }
#line 29
              if (tmp___0) {
#line 30
                expectedDirection = 1;
              } else {

              }
            } else {

            }
          }
        }
      }
    }
  } else {
#line 27
    if (currentFloorID___0 > 0) {
      {
#line 27
      tmp___9 = buttonForFloorIsPressed(0);
      }
#line 27
      if (tmp___9) {
#line 28
        expectedDirection = -1;
      } else {
        goto _L___6;
      }
    } else {
      _L___6: /* CIL Label */ 
#line 29
      if (currentFloorID___0 > 1) {
        {
#line 29
        tmp___8 = buttonForFloorIsPressed(1);
        }
#line 29
        if (tmp___8) {
#line 30
          expectedDirection = -1;
        } else {
          goto _L___5;
        }
      } else {
        _L___5: /* CIL Label */ 
#line 31
        if (currentFloorID___0 > 2) {
          {
#line 31
          tmp___7 = buttonForFloorIsPressed(2);
          }
#line 31
          if (tmp___7) {
#line 32
            expectedDirection = -1;
          } else {
            goto _L___4;
          }
        } else {
          _L___4: /* CIL Label */ 
#line 33
          if (currentFloorID___0 > 3) {
            {
#line 33
            tmp___6 = buttonForFloorIsPressed(3);
            }
#line 33
            if (tmp___6) {
#line 34
              expectedDirection = -1;
            } else {
              goto _L___3;
            }
          } else {
            _L___3: /* CIL Label */ 
#line 35
            if (currentFloorID___0 > 4) {
              {
#line 35
              tmp___5 = buttonForFloorIsPressed(4);
              }
#line 35
              if (tmp___5) {
#line 36
                expectedDirection = -1;
              } else {

              }
            } else {

            }
          }
        }
      }
    }
  }
#line 36
  return;
}
}
#line 31 "Specification3_spec.c"
void __utac_acc__Specification3_spec__2(void) 
{ int tmp ;
  int tmp___0 ;

  {
#line 38
  if (expectedDirection == -1) {
    {
#line 38
    tmp___0 = getCurrentHeading();
    }
#line 38
    if (tmp___0 == 1) {
      {
#line 39
      __automaton_fail();
      }
    } else {
      goto _L;
    }
  } else {
    _L: /* CIL Label */ 
#line 40
    if (expectedDirection == 1) {
      {
#line 40
      tmp = getCurrentHeading();
      }
#line 40
      if (tmp == 0) {
        {
#line 41
        __automaton_fail();
        }
      } else {

      }
    } else {

    }
  }
#line 41
  return;
}
}
#line 1 "libacc.o"
#pragma merger(0,"libacc.i","")
#line 73 "/usr/include/assert.h"
extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
                                                                      char const   *__file ,
                                                                      unsigned int __line ,
                                                                      char const   *__function ) ;
#line 471 "/usr/include/stdlib.h"
extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
#line 488
extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
#line 32 "libacc.c"
void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
                                                                           int  ) ,
                                       int val ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  void *tmp ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int (**mem_15)(int  , int  ) ;
  int *mem_16 ;
  struct __UTAC__CFLOW_FUNC **mem_17 ;
  struct __UTAC__CFLOW_FUNC **mem_18 ;
  struct __UTAC__CFLOW_FUNC **mem_19 ;

  {
  {
#line 33
  excep = (struct __UTAC__EXCEPTION *)exception;
#line 34
  tmp = malloc(24UL);
#line 34
  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
#line 36
  mem_15 = (int (**)(int  , int  ))cf;
#line 36
  *mem_15 = cflow_func;
#line 37
  __cil_tmp7 = (unsigned long )cf;
#line 37
  __cil_tmp8 = __cil_tmp7 + 8;
#line 37
  mem_16 = (int *)__cil_tmp8;
#line 37
  *mem_16 = val;
#line 38
  __cil_tmp9 = (unsigned long )cf;
#line 38
  __cil_tmp10 = __cil_tmp9 + 16;
#line 38
  __cil_tmp11 = (unsigned long )excep;
#line 38
  __cil_tmp12 = __cil_tmp11 + 24;
#line 38
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
#line 38
  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
#line 38
  *mem_17 = *mem_18;
#line 39
  __cil_tmp13 = (unsigned long )excep;
#line 39
  __cil_tmp14 = __cil_tmp13 + 24;
#line 39
  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
#line 39
  *mem_19 = cf;
  }
#line 654 "libacc.c"
  return;
}
}
#line 44 "libacc.c"
void __utac__exception__cf_handler_free(void *exception ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  struct __UTAC__CFLOW_FUNC *tmp ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  void *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  struct __UTAC__CFLOW_FUNC **mem_15 ;
  struct __UTAC__CFLOW_FUNC **mem_16 ;
  struct __UTAC__CFLOW_FUNC **mem_17 ;

  {
#line 45
  excep = (struct __UTAC__EXCEPTION *)exception;
#line 46
  __cil_tmp5 = (unsigned long )excep;
#line 46
  __cil_tmp6 = __cil_tmp5 + 24;
#line 46
  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
#line 46
  cf = *mem_15;
  {
#line 49
  while (1) {
    while_7_continue: /* CIL Label */ ;
    {
#line 49
    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
#line 49
    __cil_tmp8 = (unsigned long )__cil_tmp7;
#line 49
    __cil_tmp9 = (unsigned long )cf;
#line 49
    if (__cil_tmp9 != __cil_tmp8) {

    } else {
      goto while_7_break;
    }
    }
    {
#line 50
    tmp = cf;
#line 51
    __cil_tmp10 = (unsigned long )cf;
#line 51
    __cil_tmp11 = __cil_tmp10 + 16;
#line 51
    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
#line 51
    cf = *mem_16;
#line 52
    __cil_tmp12 = (void *)tmp;
#line 52
    free(__cil_tmp12);
    }
  }
  while_7_break: /* CIL Label */ ;
  }
#line 55
  __cil_tmp13 = (unsigned long )excep;
#line 55
  __cil_tmp14 = __cil_tmp13 + 24;
#line 55
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
#line 55
  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
#line 694 "libacc.c"
  return;
}
}
#line 59 "libacc.c"
void __utac__exception__cf_handler_reset(void *exception ) 
{ struct __UTAC__EXCEPTION *excep ;
  struct __UTAC__CFLOW_FUNC *cf ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  int (*__cil_tmp10)(int  , int  ) ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  struct __UTAC__CFLOW_FUNC **mem_16 ;
  int (**mem_17)(int  , int  ) ;
  int *mem_18 ;
  struct __UTAC__CFLOW_FUNC **mem_19 ;

  {
#line 60
  excep = (struct __UTAC__EXCEPTION *)exception;
#line 61
  __cil_tmp5 = (unsigned long )excep;
#line 61
  __cil_tmp6 = __cil_tmp5 + 24;
#line 61
  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
#line 61
  cf = *mem_16;
  {
#line 64
  while (1) {
    while_8_continue: /* CIL Label */ ;
    {
#line 64
    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
#line 64
    __cil_tmp8 = (unsigned long )__cil_tmp7;
#line 64
    __cil_tmp9 = (unsigned long )cf;
#line 64
    if (__cil_tmp9 != __cil_tmp8) {

    } else {
      goto while_8_break;
    }
    }
    {
#line 65
    mem_17 = (int (**)(int  , int  ))cf;
#line 65
    __cil_tmp10 = *mem_17;
#line 65
    __cil_tmp11 = (unsigned long )cf;
#line 65
    __cil_tmp12 = __cil_tmp11 + 8;
#line 65
    mem_18 = (int *)__cil_tmp12;
#line 65
    __cil_tmp13 = *mem_18;
#line 65
    (*__cil_tmp10)(4, __cil_tmp13);
#line 66
    __cil_tmp14 = (unsigned long )cf;
#line 66
    __cil_tmp15 = __cil_tmp14 + 16;
#line 66
    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
#line 66
    cf = *mem_19;
    }
  }
  while_8_break: /* CIL Label */ ;
  }
  {
#line 69
  __utac__exception__cf_handler_free(exception);
  }
#line 732 "libacc.c"
  return;
}
}
#line 80 "libacc.c"
void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
#line 80 "libacc.c"
static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
#line 79 "libacc.c"
void *__utac__error_stack_mgt(void *env , int mode , int count ) 
{ void *retValue_acc ;
  struct __ACC__ERR *new ;
  void *tmp ;
  struct __ACC__ERR *temp ;
  struct __ACC__ERR *next ;
  void *excep ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  void *__cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  void *__cil_tmp17 ;
  void **mem_18 ;
  struct __ACC__ERR **mem_19 ;
  struct __ACC__ERR **mem_20 ;
  void **mem_21 ;
  struct __ACC__ERR **mem_22 ;
  void **mem_23 ;
  void **mem_24 ;

  {
#line 82 "libacc.c"
  if (count == 0) {
#line 758 "libacc.c"
    return (retValue_acc);
  } else {

  }
#line 86 "libacc.c"
  if (mode == 0) {
    {
#line 87
    tmp = malloc(16UL);
#line 87
    new = (struct __ACC__ERR *)tmp;
#line 88
    mem_18 = (void **)new;
#line 88
    *mem_18 = env;
#line 89
    __cil_tmp10 = (unsigned long )new;
#line 89
    __cil_tmp11 = __cil_tmp10 + 8;
#line 89
    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
#line 89
    *mem_19 = head;
#line 90
    head = new;
#line 776 "libacc.c"
    retValue_acc = (void *)new;
    }
#line 778
    return (retValue_acc);
  } else {

  }
#line 94 "libacc.c"
  if (mode == 1) {
#line 95
    temp = head;
    {
#line 98
    while (1) {
      while_9_continue: /* CIL Label */ ;
#line 98
      if (count > 1) {

      } else {
        goto while_9_break;
      }
      {
#line 99
      __cil_tmp12 = (unsigned long )temp;
#line 99
      __cil_tmp13 = __cil_tmp12 + 8;
#line 99
      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
#line 99
      next = *mem_20;
#line 100
      mem_21 = (void **)temp;
#line 100
      excep = *mem_21;
#line 101
      __cil_tmp14 = (void *)temp;
#line 101
      free(__cil_tmp14);
#line 102
      __utac__exception__cf_handler_reset(excep);
#line 103
      temp = next;
#line 104
      count = count - 1;
      }
    }
    while_9_break: /* CIL Label */ ;
    }
    {
#line 107
    __cil_tmp15 = (unsigned long )temp;
#line 107
    __cil_tmp16 = __cil_tmp15 + 8;
#line 107
    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
#line 107
    head = *mem_22;
#line 108
    mem_23 = (void **)temp;
#line 108
    excep = *mem_23;
#line 109
    __cil_tmp17 = (void *)temp;
#line 109
    free(__cil_tmp17);
#line 110
    __utac__exception__cf_handler_reset(excep);
#line 820 "libacc.c"
    retValue_acc = excep;
    }
#line 822
    return (retValue_acc);
  } else {

  }
#line 114
  if (mode == 2) {
#line 118 "libacc.c"
    if (head) {
#line 831
      mem_24 = (void **)head;
#line 831
      retValue_acc = *mem_24;
#line 833
      return (retValue_acc);
    } else {
#line 837 "libacc.c"
      retValue_acc = (void *)0;
#line 839
      return (retValue_acc);
    }
  } else {

  }
#line 846 "libacc.c"
  return (retValue_acc);
}
}
#line 122 "libacc.c"
void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
{ void *retValue_acc ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  void **__cil_tmp10 ;
  void **__cil_tmp11 ;
  int *mem_12 ;
  void ***mem_13 ;

  {
#line 123
  if (i > 0) {
    {
#line 123
    __cil_tmp4 = (unsigned long )this;
#line 123
    __cil_tmp5 = __cil_tmp4 + 16;
#line 123
    mem_12 = (int *)__cil_tmp5;
#line 123
    __cil_tmp6 = *mem_12;
#line 123
    if (i <= __cil_tmp6) {

    } else {
      {
#line 123
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    123U, "__utac__get_this_arg");
      }
    }
    }
  } else {
    {
#line 123
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  123U, "__utac__get_this_arg");
    }
  }
#line 870 "libacc.c"
  __cil_tmp7 = i - 1;
#line 870
  __cil_tmp8 = (unsigned long )this;
#line 870
  __cil_tmp9 = __cil_tmp8 + 8;
#line 870
  mem_13 = (void ***)__cil_tmp9;
#line 870
  __cil_tmp10 = *mem_13;
#line 870
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
#line 870
  retValue_acc = *__cil_tmp11;
#line 872
  return (retValue_acc);
#line 879
  return (retValue_acc);
}
}
#line 129 "libacc.c"
char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
{ char const   *retValue_acc ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  char const   **__cil_tmp10 ;
  char const   **__cil_tmp11 ;
  int *mem_12 ;
  char const   ***mem_13 ;

  {
#line 131
  if (i > 0) {
    {
#line 131
    __cil_tmp4 = (unsigned long )this;
#line 131
    __cil_tmp5 = __cil_tmp4 + 16;
#line 131
    mem_12 = (int *)__cil_tmp5;
#line 131
    __cil_tmp6 = *mem_12;
#line 131
    if (i <= __cil_tmp6) {

    } else {
      {
#line 131
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    131U, "__utac__get_this_argtype");
      }
    }
    }
  } else {
    {
#line 131
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  131U, "__utac__get_this_argtype");
    }
  }
#line 903 "libacc.c"
  __cil_tmp7 = i - 1;
#line 903
  __cil_tmp8 = (unsigned long )this;
#line 903
  __cil_tmp9 = __cil_tmp8 + 24;
#line 903
  mem_13 = (char const   ***)__cil_tmp9;
#line 903
  __cil_tmp10 = *mem_13;
#line 903
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
#line 903
  retValue_acc = *__cil_tmp11;
#line 905
  return (retValue_acc);
#line 912
  return (retValue_acc);
}
}
#line 1 "featureselect.o"
#pragma merger(0,"featureselect.i","")
#line 9 "featureselect.h"
int select_one(void) ;
#line 8 "featureselect.c"
int select_one(void) 
{ int retValue_acc ;
  int choice = __VERIFIER_nondet_int();

  {
#line 63 "featureselect.c"
  retValue_acc = choice;
#line 65
  return (retValue_acc);
#line 72
  return (retValue_acc);
}
}
#line 14 "featureselect.c"
void select_features(void) 
{ 

  {
#line 94 "featureselect.c"
  return;
}
}
#line 20 "featureselect.c"
void select_helpers(void) 
{ 

  {
#line 112 "featureselect.c"
  return;
}
}
#line 25 "featureselect.c"
int valid_product(void) 
{ int retValue_acc ;

  {
#line 130 "featureselect.c"
  retValue_acc = 1;
#line 132
  return (retValue_acc);
#line 139
  return (retValue_acc);
}
}
#line 1 "wsllib_check.o"
#pragma merger(0,"wsllib_check.i","")
#line 3 "wsllib_check.c"
void __automaton_fail(void) 
{ 

  {
  goto ERROR;
  ERROR: ;
#line 53 "wsllib_check.c"
  return;
}
}