elevator_spec14_product03_true-unreach-call_true-termination.cil.c

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

extern int __VERIFIER_nondet_int(void);
/* Generated by CIL v. 1.3.7 */
/* print_CIL_Input is true */

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 ;
};
struct __UTAC__CFLOW_FUNC {
   int (*func)(int  , int  ) ;
   int val ;
   struct __UTAC__CFLOW_FUNC *next ;
};
struct __UTAC__EXCEPTION {
   void *jumpbuf ;
   unsigned long long prtValue ;
   int pops ;
   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
};
typedef unsigned int size_t;
struct __ACC__ERR {
   void *v ;
   struct __ACC__ERR *next ;
};
#pragma merger(0,"Person.i","")
int getWeight(int person ) ;
int getOrigin(int person ) ;
int getDestination(int person ) ;
int getWeight(int person ) 
{ int retValue_acc ;

  {
  if (person == 0) {
    retValue_acc = 40;
    return (retValue_acc);
  } else {
    if (person == 1) {
      retValue_acc = 40;
      return (retValue_acc);
    } else {
      if (person == 2) {
        retValue_acc = 40;
        return (retValue_acc);
      } else {
        if (person == 3) {
          retValue_acc = 40;
          return (retValue_acc);
        } else {
          if (person == 4) {
            retValue_acc = 30;
            return (retValue_acc);
          } else {
            if (person == 5) {
              retValue_acc = 150;
              return (retValue_acc);
            } else {
              retValue_acc = 0;
              return (retValue_acc);
            }
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
int getOrigin(int person ) 
{ int retValue_acc ;

  {
  if (person == 0) {
    retValue_acc = 4;
    return (retValue_acc);
  } else {
    if (person == 1) {
      retValue_acc = 3;
      return (retValue_acc);
    } else {
      if (person == 2) {
        retValue_acc = 2;
        return (retValue_acc);
      } else {
        if (person == 3) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          if (person == 4) {
            retValue_acc = 0;
            return (retValue_acc);
          } else {
            if (person == 5) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              retValue_acc = 0;
              return (retValue_acc);
            }
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
int getDestination(int person ) 
{ int retValue_acc ;

  {
  if (person == 0) {
    retValue_acc = 0;
    return (retValue_acc);
  } else {
    if (person == 1) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {
      if (person == 2) {
        retValue_acc = 1;
        return (retValue_acc);
      } else {
        if (person == 3) {
          retValue_acc = 3;
          return (retValue_acc);
        } else {
          if (person == 4) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            if (person == 5) {
              retValue_acc = 3;
              return (retValue_acc);
            } else {
              retValue_acc = 0;
              return (retValue_acc);
            }
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
#pragma merger(0,"UnitTests.i","")
void initPersonOnFloor(int person , int floor ) ;
void timeShift(void) ;
int isBlocked(void) ;
void printState(void) ;
void initTopDown(void) ;
void initBottomUp(void) ;
int executiveFloor  =    4;
int cleanupTimeShifts  =    12;
void spec1(void) 
{ int tmp ;
  int tmp___0 ;
  int i ;
  int tmp___1 ;

  {
  {
  initBottomUp();
  tmp = getOrigin(5);
  initPersonOnFloor(5, tmp);
  printState();
  tmp___0 = getOrigin(2);
  initPersonOnFloor(2, tmp___0);
  printState();
  i = 0;
  }
  {
  while (1) {
    while_0_continue: /* CIL Label */ ;
    if (i < cleanupTimeShifts) {
      {
      tmp___1 = isBlocked();
      }
      if (tmp___1 != 1) {

      } else {
        goto while_0_break;
      }
    } else {
      goto while_0_break;
    }
    {
    timeShift();
    printState();
    i = i + 1;
    }
  }
  while_0_break: /* CIL Label */ ;
  }
  return;
}
}
void spec14(void) 
{ int tmp ;
  int tmp___0 ;
  int i ;
  int tmp___1 ;

  {
  {
  initTopDown();
  tmp = getOrigin(5);
  initPersonOnFloor(5, tmp);
  printState();
  timeShift();
  timeShift();
  timeShift();
  timeShift();
  tmp___0 = getOrigin(0);
  initPersonOnFloor(0, tmp___0);
  printState();
  i = 0;
  }
  {
  while (1) {
    while_1_continue: /* CIL Label */ ;
    if (i < cleanupTimeShifts) {
      {
      tmp___1 = isBlocked();
      }
      if (tmp___1 != 1) {

      } else {
        goto while_1_break;
      }
    } else {
      goto while_1_break;
    }
    {
    timeShift();
    printState();
    i = i + 1;
    }
  }
  while_1_break: /* CIL Label */ ;
  }
  return;
}
}
#pragma merger(0,"Floor.i","")
int isFloorCalling(int floorID ) ;
void resetCallOnFloor(int floorID ) ;
void callOnFloor(int floorID ) ;
int isPersonOnFloor(int person , int floor ) ;
void removePersonFromFloor(int person , int floor ) ;
int isTopFloor(int floorID ) ;
void initFloors(void) ;
int calls_0  ;
int calls_1  ;
int calls_2  ;
int calls_3  ;
int calls_4  ;
int personOnFloor_0_0  ;
int personOnFloor_0_1  ;
int personOnFloor_0_2  ;
int personOnFloor_0_3  ;
int personOnFloor_0_4  ;
int personOnFloor_1_0  ;
int personOnFloor_1_1  ;
int personOnFloor_1_2  ;
int personOnFloor_1_3  ;
int personOnFloor_1_4  ;
int personOnFloor_2_0  ;
int personOnFloor_2_1  ;
int personOnFloor_2_2  ;
int personOnFloor_2_3  ;
int personOnFloor_2_4  ;
int personOnFloor_3_0  ;
int personOnFloor_3_1  ;
int personOnFloor_3_2  ;
int personOnFloor_3_3  ;
int personOnFloor_3_4  ;
int personOnFloor_4_0  ;
int personOnFloor_4_1  ;
int personOnFloor_4_2  ;
int personOnFloor_4_3  ;
int personOnFloor_4_4  ;
int personOnFloor_5_0  ;
int personOnFloor_5_1  ;
int personOnFloor_5_2  ;
int personOnFloor_5_3  ;
int personOnFloor_5_4  ;
void initFloors(void) 
{ 

  {
  calls_0 = 0;
  calls_1 = 0;
  calls_2 = 0;
  calls_3 = 0;
  calls_4 = 0;
  personOnFloor_0_0 = 0;
  personOnFloor_0_1 = 0;
  personOnFloor_0_2 = 0;
  personOnFloor_0_3 = 0;
  personOnFloor_0_4 = 0;
  personOnFloor_1_0 = 0;
  personOnFloor_1_1 = 0;
  personOnFloor_1_2 = 0;
  personOnFloor_1_3 = 0;
  personOnFloor_1_4 = 0;
  personOnFloor_2_0 = 0;
  personOnFloor_2_1 = 0;
  personOnFloor_2_2 = 0;
  personOnFloor_2_3 = 0;
  personOnFloor_2_4 = 0;
  personOnFloor_3_0 = 0;
  personOnFloor_3_1 = 0;
  personOnFloor_3_2 = 0;
  personOnFloor_3_3 = 0;
  personOnFloor_3_4 = 0;
  personOnFloor_4_0 = 0;
  personOnFloor_4_1 = 0;
  personOnFloor_4_2 = 0;
  personOnFloor_4_3 = 0;
  personOnFloor_4_4 = 0;
  personOnFloor_5_0 = 0;
  personOnFloor_5_1 = 0;
  personOnFloor_5_2 = 0;
  personOnFloor_5_3 = 0;
  personOnFloor_5_4 = 0;
  return;
}
}
int isFloorCalling(int floorID ) 
{ int retValue_acc ;

  {
  if (floorID == 0) {
    retValue_acc = calls_0;
    return (retValue_acc);
  } else {
    if (floorID == 1) {
      retValue_acc = calls_1;
      return (retValue_acc);
    } else {
      if (floorID == 2) {
        retValue_acc = calls_2;
        return (retValue_acc);
      } else {
        if (floorID == 3) {
          retValue_acc = calls_3;
          return (retValue_acc);
        } else {
          if (floorID == 4) {
            retValue_acc = calls_4;
            return (retValue_acc);
          } else {

          }
        }
      }
    }
  }
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
void resetCallOnFloor(int floorID ) 
{ 

  {
  if (floorID == 0) {
    calls_0 = 0;
  } else {
    if (floorID == 1) {
      calls_1 = 0;
    } else {
      if (floorID == 2) {
        calls_2 = 0;
      } else {
        if (floorID == 3) {
          calls_3 = 0;
        } else {
          if (floorID == 4) {
            calls_4 = 0;
          } else {

          }
        }
      }
    }
  }
  return;
}
}
void callOnFloor(int floorID ) 
{ 

  {
  if (floorID == 0) {
    calls_0 = 1;
  } else {
    if (floorID == 1) {
      calls_1 = 1;
    } else {
      if (floorID == 2) {
        calls_2 = 1;
      } else {
        if (floorID == 3) {
          calls_3 = 1;
        } else {
          if (floorID == 4) {
            calls_4 = 1;
          } else {

          }
        }
      }
    }
  }
  return;
}
}
int isPersonOnFloor(int person , int floor ) 
{ int retValue_acc ;

  {
  if (floor == 0) {
    if (person == 0) {
      retValue_acc = personOnFloor_0_0;
      return (retValue_acc);
    } else {
      if (person == 1) {
        retValue_acc = personOnFloor_1_0;
        return (retValue_acc);
      } else {
        if (person == 2) {
          retValue_acc = personOnFloor_2_0;
          return (retValue_acc);
        } else {
          if (person == 3) {
            retValue_acc = personOnFloor_3_0;
            return (retValue_acc);
          } else {
            if (person == 4) {
              retValue_acc = personOnFloor_4_0;
              return (retValue_acc);
            } else {
              if (person == 5) {
                retValue_acc = personOnFloor_5_0;
                return (retValue_acc);
              } else {

              }
            }
          }
        }
      }
    }
  } else {
    if (floor == 1) {
      if (person == 0) {
        retValue_acc = personOnFloor_0_1;
        return (retValue_acc);
      } else {
        if (person == 1) {
          retValue_acc = personOnFloor_1_1;
          return (retValue_acc);
        } else {
          if (person == 2) {
            retValue_acc = personOnFloor_2_1;
            return (retValue_acc);
          } else {
            if (person == 3) {
              retValue_acc = personOnFloor_3_1;
              return (retValue_acc);
            } else {
              if (person == 4) {
                retValue_acc = personOnFloor_4_1;
                return (retValue_acc);
              } else {
                if (person == 5) {
                  retValue_acc = personOnFloor_5_1;
                  return (retValue_acc);
                } else {

                }
              }
            }
          }
        }
      }
    } else {
      if (floor == 2) {
        if (person == 0) {
          retValue_acc = personOnFloor_0_2;
          return (retValue_acc);
        } else {
          if (person == 1) {
            retValue_acc = personOnFloor_1_2;
            return (retValue_acc);
          } else {
            if (person == 2) {
              retValue_acc = personOnFloor_2_2;
              return (retValue_acc);
            } else {
              if (person == 3) {
                retValue_acc = personOnFloor_3_2;
                return (retValue_acc);
              } else {
                if (person == 4) {
                  retValue_acc = personOnFloor_4_2;
                  return (retValue_acc);
                } else {
                  if (person == 5) {
                    retValue_acc = personOnFloor_5_2;
                    return (retValue_acc);
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
        if (floor == 3) {
          if (person == 0) {
            retValue_acc = personOnFloor_0_3;
            return (retValue_acc);
          } else {
            if (person == 1) {
              retValue_acc = personOnFloor_1_3;
              return (retValue_acc);
            } else {
              if (person == 2) {
                retValue_acc = personOnFloor_2_3;
                return (retValue_acc);
              } else {
                if (person == 3) {
                  retValue_acc = personOnFloor_3_3;
                  return (retValue_acc);
                } else {
                  if (person == 4) {
                    retValue_acc = personOnFloor_4_3;
                    return (retValue_acc);
                  } else {
                    if (person == 5) {
                      retValue_acc = personOnFloor_5_3;
                      return (retValue_acc);
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
          if (floor == 4) {
            if (person == 0) {
              retValue_acc = personOnFloor_0_4;
              return (retValue_acc);
            } else {
              if (person == 1) {
                retValue_acc = personOnFloor_1_4;
                return (retValue_acc);
              } else {
                if (person == 2) {
                  retValue_acc = personOnFloor_2_4;
                  return (retValue_acc);
                } else {
                  if (person == 3) {
                    retValue_acc = personOnFloor_3_4;
                    return (retValue_acc);
                  } else {
                    if (person == 4) {
                      retValue_acc = personOnFloor_4_4;
                      return (retValue_acc);
                    } else {
                      if (person == 5) {
                        retValue_acc = personOnFloor_5_4;
                        return (retValue_acc);
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
void initPersonOnFloor(int person , int floor ) 
{ 

  {
  if (floor == 0) {
    if (person == 0) {
      personOnFloor_0_0 = 1;
    } else {
      if (person == 1) {
        personOnFloor_1_0 = 1;
      } else {
        if (person == 2) {
          personOnFloor_2_0 = 1;
        } else {
          if (person == 3) {
            personOnFloor_3_0 = 1;
          } else {
            if (person == 4) {
              personOnFloor_4_0 = 1;
            } else {
              if (person == 5) {
                personOnFloor_5_0 = 1;
              } else {

              }
            }
          }
        }
      }
    }
  } else {
    if (floor == 1) {
      if (person == 0) {
        personOnFloor_0_1 = 1;
      } else {
        if (person == 1) {
          personOnFloor_1_1 = 1;
        } else {
          if (person == 2) {
            personOnFloor_2_1 = 1;
          } else {
            if (person == 3) {
              personOnFloor_3_1 = 1;
            } else {
              if (person == 4) {
                personOnFloor_4_1 = 1;
              } else {
                if (person == 5) {
                  personOnFloor_5_1 = 1;
                } else {

                }
              }
            }
          }
        }
      }
    } else {
      if (floor == 2) {
        if (person == 0) {
          personOnFloor_0_2 = 1;
        } else {
          if (person == 1) {
            personOnFloor_1_2 = 1;
          } else {
            if (person == 2) {
              personOnFloor_2_2 = 1;
            } else {
              if (person == 3) {
                personOnFloor_3_2 = 1;
              } else {
                if (person == 4) {
                  personOnFloor_4_2 = 1;
                } else {
                  if (person == 5) {
                    personOnFloor_5_2 = 1;
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
        if (floor == 3) {
          if (person == 0) {
            personOnFloor_0_3 = 1;
          } else {
            if (person == 1) {
              personOnFloor_1_3 = 1;
            } else {
              if (person == 2) {
                personOnFloor_2_3 = 1;
              } else {
                if (person == 3) {
                  personOnFloor_3_3 = 1;
                } else {
                  if (person == 4) {
                    personOnFloor_4_3 = 1;
                  } else {
                    if (person == 5) {
                      personOnFloor_5_3 = 1;
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
          if (floor == 4) {
            if (person == 0) {
              personOnFloor_0_4 = 1;
            } else {
              if (person == 1) {
                personOnFloor_1_4 = 1;
              } else {
                if (person == 2) {
                  personOnFloor_2_4 = 1;
                } else {
                  if (person == 3) {
                    personOnFloor_3_4 = 1;
                  } else {
                    if (person == 4) {
                      personOnFloor_4_4 = 1;
                    } else {
                      if (person == 5) {
                        personOnFloor_5_4 = 1;
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
  {
  callOnFloor(floor);
  }
  return;
}
}
void removePersonFromFloor(int person , int floor ) 
{ 

  {
  if (floor == 0) {
    if (person == 0) {
      personOnFloor_0_0 = 0;
    } else {
      if (person == 1) {
        personOnFloor_1_0 = 0;
      } else {
        if (person == 2) {
          personOnFloor_2_0 = 0;
        } else {
          if (person == 3) {
            personOnFloor_3_0 = 0;
          } else {
            if (person == 4) {
              personOnFloor_4_0 = 0;
            } else {
              if (person == 5) {
                personOnFloor_5_0 = 0;
              } else {

              }
            }
          }
        }
      }
    }
  } else {
    if (floor == 1) {
      if (person == 0) {
        personOnFloor_0_1 = 0;
      } else {
        if (person == 1) {
          personOnFloor_1_1 = 0;
        } else {
          if (person == 2) {
            personOnFloor_2_1 = 0;
          } else {
            if (person == 3) {
              personOnFloor_3_1 = 0;
            } else {
              if (person == 4) {
                personOnFloor_4_1 = 0;
              } else {
                if (person == 5) {
                  personOnFloor_5_1 = 0;
                } else {

                }
              }
            }
          }
        }
      }
    } else {
      if (floor == 2) {
        if (person == 0) {
          personOnFloor_0_2 = 0;
        } else {
          if (person == 1) {
            personOnFloor_1_2 = 0;
          } else {
            if (person == 2) {
              personOnFloor_2_2 = 0;
            } else {
              if (person == 3) {
                personOnFloor_3_2 = 0;
              } else {
                if (person == 4) {
                  personOnFloor_4_2 = 0;
                } else {
                  if (person == 5) {
                    personOnFloor_5_2 = 0;
                  } else {

                  }
                }
              }
            }
          }
        }
      } else {
        if (floor == 3) {
          if (person == 0) {
            personOnFloor_0_3 = 0;
          } else {
            if (person == 1) {
              personOnFloor_1_3 = 0;
            } else {
              if (person == 2) {
                personOnFloor_2_3 = 0;
              } else {
                if (person == 3) {
                  personOnFloor_3_3 = 0;
                } else {
                  if (person == 4) {
                    personOnFloor_4_3 = 0;
                  } else {
                    if (person == 5) {
                      personOnFloor_5_3 = 0;
                    } else {

                    }
                  }
                }
              }
            }
          }
        } else {
          if (floor == 4) {
            if (person == 0) {
              personOnFloor_0_4 = 0;
            } else {
              if (person == 1) {
                personOnFloor_1_4 = 0;
              } else {
                if (person == 2) {
                  personOnFloor_2_4 = 0;
                } else {
                  if (person == 3) {
                    personOnFloor_3_4 = 0;
                  } else {
                    if (person == 4) {
                      personOnFloor_4_4 = 0;
                    } else {
                      if (person == 5) {
                        personOnFloor_5_4 = 0;
                      } else {

                      }
                    }
                  }
                }
              }
            }
          } else {

          }
        }
      }
    }
  }
  {
  resetCallOnFloor(floor);
  }
  return;
}
}
int isTopFloor(int floorID ) 
{ int retValue_acc ;

  {
  retValue_acc = floorID == 4;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"Specification14_spec.i","")
void __automaton_fail(void) ;
int areDoorsOpen(void) ;
int getCurrentFloorID(void) ;
int isExecutiveFloorCalling(void) ;
int isExecutiveFloor(int floorID ) ;
__inline void __utac_acc__Specification14_spec__1(void) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
  tmp___2 = isExecutiveFloorCalling();
  }
  if (tmp___2) {
    {
    tmp = getCurrentFloorID();
    tmp___0 = isExecutiveFloor(tmp);
    }
    if (tmp___0) {

    } else {
      {
      tmp___1 = areDoorsOpen();
      }
      if (tmp___1) {
        {
        __automaton_fail();
        }
      } else {

      }
    }
  } else {

  }
  return;
}
}
#pragma merger(0,"scenario.i","")
void bigMacCall(void) ;
void threeTS(void) ;
void bobCall(void) ;
void cleanup(void) ;
void test(void) 
{ 

  {
  {
  bigMacCall();
  threeTS();
  bobCall();
  cleanup();
  }
  return;
}
}
#pragma merger(0,"Test.i","")
extern  __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
int get_nondetMinMax07(void) 
{ int retValue_acc ;
  int nd ;
  nd = __VERIFIER_nondet_int();

  {
  if (nd == 0) {
    retValue_acc = 0;
    return (retValue_acc);
  } else {
    if (nd == 1) {
      retValue_acc = 1;
      return (retValue_acc);
    } else {
      if (nd == 2) {
        retValue_acc = 2;
        return (retValue_acc);
      } else {
        if (nd == 3) {
          retValue_acc = 3;
          return (retValue_acc);
        } else {
          if (nd == 4) {
            retValue_acc = 4;
            return (retValue_acc);
          } else {
            if (nd == 5) {
              retValue_acc = 5;
              return (retValue_acc);
            } else {
              if (nd == 6) {
                retValue_acc = 6;
                return (retValue_acc);
              } else {
                if (nd == 7) {
                  retValue_acc = 7;
                  return (retValue_acc);
                } else {
                  {
                  exit(0);
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
void bobCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(0);
  initPersonOnFloor(0, tmp);
  }
  return;
}
}
void aliceCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(1);
  initPersonOnFloor(1, tmp);
  }
  return;
}
}
void angelinaCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(2);
  initPersonOnFloor(2, tmp);
  }
  return;
}
}
void chuckCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(3);
  initPersonOnFloor(3, tmp);
  }
  return;
}
}
void monicaCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(4);
  initPersonOnFloor(4, tmp);
  }
  return;
}
}
void bigMacCall(void) 
{ int tmp ;

  {
  {
  tmp = getOrigin(5);
  initPersonOnFloor(5, tmp);
  }
  return;
}
}
void threeTS(void) 
{ 

  {
  {
  timeShift();
  timeShift();
  timeShift();
  }
  return;
}
}
int isIdle(void) ;
void cleanup(void) 
{ int i ;
  int tmp ;
  int tmp___0 ;
  int __cil_tmp4 ;

  {
  {
  timeShift();
  i = 0;
  }
  {
  while (1) {
    while_2_continue: /* CIL Label */ ;
    {
    __cil_tmp4 = cleanupTimeShifts - 1;
    if (i < __cil_tmp4) {
      {
      tmp___0 = isBlocked();
      }
      if (tmp___0 != 1) {

      } else {
        goto while_2_break;
      }
    } else {
      goto while_2_break;
    }
    }
    {
    tmp = isIdle();
    }
    if (tmp) {
      return;
    } else {
      {
      timeShift();
      }
    }
    i = i + 1;
  }
  while_2_break: /* CIL Label */ ;
  }
  return;
}
}
void randomSequenceOfActions(void) 
{ int maxLength ;
  int tmp ;
  int counter ;
  int action ;
  int tmp___0 ;
  int origin ;
  int tmp___1 ;
  int tmp___2 ;

  {
  {
  maxLength = 4;
  tmp = __VERIFIER_nondet_int();
  }
  if (tmp) {
    {
    initTopDown();
    }
  } else {
    {
    initBottomUp();
    }
  }
  counter = 0;
  {
  while (1) {
    while_3_continue: /* CIL Label */ ;
    if (counter < maxLength) {

    } else {
      goto while_3_break;
    }
    {
    counter = counter + 1;
    tmp___0 = get_nondetMinMax07();
    action = tmp___0;
    }
    if (action < 6) {
      {
      tmp___1 = getOrigin(action);
      origin = tmp___1;
      initPersonOnFloor(action, origin);
      }
    } else {
      if (action == 6) {
        {
        timeShift();
        }
      } else {
        if (action == 7) {
          {
          timeShift();
          timeShift();
          timeShift();
          }
        } else {

        }
      }
    }
    {
    tmp___2 = isBlocked();
    }
    if (tmp___2) {
      return;
    } else {

    }
  }
  while_3_break: /* CIL Label */ ;
  }
  {
  cleanup();
  }
  return;
}
}
void runTest_Simple(void) 
{ 

  {
  {
  bigMacCall();
  angelinaCall();
  cleanup();
  }
  return;
}
}
void Specification1(void) 
{ 

  {
  {
  bigMacCall();
  angelinaCall();
  cleanup();
  }
  return;
}
}
void Specification2(void) 
{ 

  {
  {
  bigMacCall();
  cleanup();
  }
  return;
}
}
void Specification3(void) 
{ 

  {
  {
  bobCall();
  timeShift();
  timeShift();
  timeShift();
  timeShift();
  timeShift();
  bobCall();
  cleanup();
  }
  return;
}
}
void setup(void) 
{ 

  {
  return;
}
}
void runTest(void) 
{ 

  {
  {
  test();
  }
  return;
}
}
void select_helpers(void) ;
void select_features(void) ;
int valid_product(void) ;
int main(void) 
{ int retValue_acc ;
  int tmp ;

  {
  {
  select_helpers();
  select_features();
  tmp = valid_product();
  }
  if (tmp) {
    {
    setup();
    runTest();
    }
  } else {

  }
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"libacc.i","")
extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
                                                                      char const   *__file ,
                                                                      unsigned int __line ,
                                                                      char const   *__function ) ;
extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
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 ;

  {
  {
  excep = (struct __UTAC__EXCEPTION *)exception;
  tmp = malloc(24UL);
  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
  mem_15 = (int (**)(int  , int  ))cf;
  *mem_15 = cflow_func;
  __cil_tmp7 = (unsigned long )cf;
  __cil_tmp8 = __cil_tmp7 + 8;
  mem_16 = (int *)__cil_tmp8;
  *mem_16 = val;
  __cil_tmp9 = (unsigned long )cf;
  __cil_tmp10 = __cil_tmp9 + 16;
  __cil_tmp11 = (unsigned long )excep;
  __cil_tmp12 = __cil_tmp11 + 24;
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
  *mem_17 = *mem_18;
  __cil_tmp13 = (unsigned long )excep;
  __cil_tmp14 = __cil_tmp13 + 24;
  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
  *mem_19 = cf;
  }
  return;
}
}
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 ;

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

    } else {
      goto while_4_break;
    }
    }
    {
    tmp = cf;
    __cil_tmp10 = (unsigned long )cf;
    __cil_tmp11 = __cil_tmp10 + 16;
    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
    cf = *mem_16;
    __cil_tmp12 = (void *)tmp;
    free(__cil_tmp12);
    }
  }
  while_4_break: /* CIL Label */ ;
  }
  __cil_tmp13 = (unsigned long )excep;
  __cil_tmp14 = __cil_tmp13 + 24;
  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
  return;
}
}
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 ;

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

    } else {
      goto while_5_break;
    }
    }
    {
    mem_17 = (int (**)(int  , int  ))cf;
    __cil_tmp10 = *mem_17;
    __cil_tmp11 = (unsigned long )cf;
    __cil_tmp12 = __cil_tmp11 + 8;
    mem_18 = (int *)__cil_tmp12;
    __cil_tmp13 = *mem_18;
    (*__cil_tmp10)(4, __cil_tmp13);
    __cil_tmp14 = (unsigned long )cf;
    __cil_tmp15 = __cil_tmp14 + 16;
    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
    cf = *mem_19;
    }
  }
  while_5_break: /* CIL Label */ ;
  }
  {
  __utac__exception__cf_handler_free(exception);
  }
  return;
}
}
void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
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 ;

  {
  if (count == 0) {
    return (retValue_acc);
  } else {

  }
  if (mode == 0) {
    {
    tmp = malloc(16UL);
    new = (struct __ACC__ERR *)tmp;
    mem_18 = (void **)new;
    *mem_18 = env;
    __cil_tmp10 = (unsigned long )new;
    __cil_tmp11 = __cil_tmp10 + 8;
    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
    *mem_19 = head;
    head = new;
    retValue_acc = (void *)new;
    }
    return (retValue_acc);
  } else {

  }
  if (mode == 1) {
    temp = head;
    {
    while (1) {
      while_6_continue: /* CIL Label */ ;
      if (count > 1) {

      } else {
        goto while_6_break;
      }
      {
      __cil_tmp12 = (unsigned long )temp;
      __cil_tmp13 = __cil_tmp12 + 8;
      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
      next = *mem_20;
      mem_21 = (void **)temp;
      excep = *mem_21;
      __cil_tmp14 = (void *)temp;
      free(__cil_tmp14);
      __utac__exception__cf_handler_reset(excep);
      temp = next;
      count = count - 1;
      }
    }
    while_6_break: /* CIL Label */ ;
    }
    {
    __cil_tmp15 = (unsigned long )temp;
    __cil_tmp16 = __cil_tmp15 + 8;
    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
    head = *mem_22;
    mem_23 = (void **)temp;
    excep = *mem_23;
    __cil_tmp17 = (void *)temp;
    free(__cil_tmp17);
    __utac__exception__cf_handler_reset(excep);
    retValue_acc = excep;
    }
    return (retValue_acc);
  } else {

  }
  if (mode == 2) {
    if (head) {
      mem_24 = (void **)head;
      retValue_acc = *mem_24;
      return (retValue_acc);
    } else {
      retValue_acc = (void *)0;
      return (retValue_acc);
    }
  } else {

  }
  return (retValue_acc);
}
}
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 ;

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

    } else {
      {
      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                    123U, "__utac__get_this_arg");
      }
    }
    }
  } else {
    {
    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
                  123U, "__utac__get_this_arg");
    }
  }
  __cil_tmp7 = i - 1;
  __cil_tmp8 = (unsigned long )this;
  __cil_tmp9 = __cil_tmp8 + 8;
  mem_13 = (void ***)__cil_tmp9;
  __cil_tmp10 = *mem_13;
  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
  retValue_acc = *__cil_tmp11;
  return (retValue_acc);
  return (retValue_acc);
}
}
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 ;

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

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

  {
  retValue_acc = choice;
  return (retValue_acc);
  return (retValue_acc);
}
}
void select_features(void) 
{ 

  {
  return;
}
}
void select_helpers(void) 
{ 

  {
  return;
}
}
int valid_product(void) 
{ int retValue_acc ;

  {
  retValue_acc = 1;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"Elevator.i","")
extern int printf(char const   * __restrict  __format  , ...) ;
void enterElevator(int p ) ;
int isEmpty(void) ;
int isAnyLiftButtonPressed(void) ;
int buttonForFloorIsPressed(int floorID ) ;
int currentHeading  =    1;
int currentFloorID  =    0;
int persons_0  ;
int persons_1  ;
int persons_2  ;
int persons_3  ;
int persons_4  ;
int persons_5  ;
int doorState  =    1;
int floorButtons_0  ;
int floorButtons_1  ;
int floorButtons_2  ;
int floorButtons_3  ;
int floorButtons_4  ;
void initTopDown(void) 
{ 

  {
  {
  currentFloorID = 4;
  currentHeading = 0;
  floorButtons_0 = 0;
  floorButtons_1 = 0;
  floorButtons_2 = 0;
  floorButtons_3 = 0;
  floorButtons_4 = 0;
  persons_0 = 0;
  persons_1 = 0;
  persons_2 = 0;
  persons_3 = 0;
  persons_4 = 0;
  persons_5 = 0;
  initFloors();
  }
  return;
}
}
void initBottomUp(void) 
{ 

  {
  {
  currentFloorID = 0;
  currentHeading = 1;
  floorButtons_0 = 0;
  floorButtons_1 = 0;
  floorButtons_2 = 0;
  floorButtons_3 = 0;
  floorButtons_4 = 0;
  persons_0 = 0;
  persons_1 = 0;
  persons_2 = 0;
  persons_3 = 0;
  persons_4 = 0;
  persons_5 = 0;
  initFloors();
  }
  return;
}
}
int isBlocked(void) 
{ int retValue_acc ;

  {
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
void enterElevator(int p ) 
{ 

  {
  if (p == 0) {
    persons_0 = 1;
  } else {
    if (p == 1) {
      persons_1 = 1;
    } else {
      if (p == 2) {
        persons_2 = 1;
      } else {
        if (p == 3) {
          persons_3 = 1;
        } else {
          if (p == 4) {
            persons_4 = 1;
          } else {
            if (p == 5) {
              persons_5 = 1;
            } else {

            }
          }
        }
      }
    }
  }
  return;
}
}
void leaveElevator(int p ) 
{ 

  {
  if (p == 0) {
    persons_0 = 0;
  } else {
    if (p == 1) {
      persons_1 = 0;
    } else {
      if (p == 2) {
        persons_2 = 0;
      } else {
        if (p == 3) {
          persons_3 = 0;
        } else {
          if (p == 4) {
            persons_4 = 0;
          } else {
            if (p == 5) {
              persons_5 = 0;
            } else {

            }
          }
        }
      }
    }
  }
  return;
}
}
void pressInLiftFloorButton(int floorID ) 
{ 

  {
  if (floorID == 0) {
    floorButtons_0 = 1;
  } else {
    if (floorID == 1) {
      floorButtons_1 = 1;
    } else {
      if (floorID == 2) {
        floorButtons_2 = 1;
      } else {
        if (floorID == 3) {
          floorButtons_3 = 1;
        } else {
          if (floorID == 4) {
            floorButtons_4 = 1;
          } else {

          }
        }
      }
    }
  }
  return;
}
}
void resetFloorButton(int floorID ) 
{ 

  {
  if (floorID == 0) {
    floorButtons_0 = 0;
  } else {
    if (floorID == 1) {
      floorButtons_1 = 0;
    } else {
      if (floorID == 2) {
        floorButtons_2 = 0;
      } else {
        if (floorID == 3) {
          floorButtons_3 = 0;
        } else {
          if (floorID == 4) {
            floorButtons_4 = 0;
          } else {

          }
        }
      }
    }
  }
  return;
}
}
int getCurrentFloorID(void) 
{ int retValue_acc ;

  {
  retValue_acc = currentFloorID;
  return (retValue_acc);
  return (retValue_acc);
}
}
int areDoorsOpen(void) 
{ int retValue_acc ;

  {
  retValue_acc = doorState;
  return (retValue_acc);
  return (retValue_acc);
}
}
int buttonForFloorIsPressed(int floorID ) 
{ int retValue_acc ;

  {
  if (floorID == 0) {
    retValue_acc = floorButtons_0;
    return (retValue_acc);
  } else {
    if (floorID == 1) {
      retValue_acc = floorButtons_1;
      return (retValue_acc);
    } else {
      if (floorID == 2) {
        retValue_acc = floorButtons_2;
        return (retValue_acc);
      } else {
        if (floorID == 3) {
          retValue_acc = floorButtons_3;
          return (retValue_acc);
        } else {
          if (floorID == 4) {
            retValue_acc = floorButtons_4;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
int getCurrentHeading(void) 
{ int retValue_acc ;

  {
  retValue_acc = currentHeading;
  return (retValue_acc);
  return (retValue_acc);
}
}
int isEmpty(void) 
{ int retValue_acc ;

  {
  if (persons_0 == 1) {
    retValue_acc = 0;
    return (retValue_acc);
  } else {
    if (persons_1 == 1) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {
      if (persons_2 == 1) {
        retValue_acc = 0;
        return (retValue_acc);
      } else {
        if (persons_3 == 1) {
          retValue_acc = 0;
          return (retValue_acc);
        } else {
          if (persons_4 == 1) {
            retValue_acc = 0;
            return (retValue_acc);
          } else {
            if (persons_5 == 1) {
              retValue_acc = 0;
              return (retValue_acc);
            } else {

            }
          }
        }
      }
    }
  }
  retValue_acc = 1;
  return (retValue_acc);
  return (retValue_acc);
}
}
int anyStopRequested(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;

  {
  {
  tmp___3 = isFloorCalling(0);
  }
  if (tmp___3) {
    retValue_acc = 1;
    return (retValue_acc);
  } else {
    if (floorButtons_0) {
      retValue_acc = 1;
      return (retValue_acc);
    } else {
      {
      tmp___2 = isFloorCalling(1);
      }
      if (tmp___2) {
        retValue_acc = 1;
        return (retValue_acc);
      } else {
        if (floorButtons_1) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          {
          tmp___1 = isFloorCalling(2);
          }
          if (tmp___1) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            if (floorButtons_2) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              {
              tmp___0 = isFloorCalling(3);
              }
              if (tmp___0) {
                retValue_acc = 1;
                return (retValue_acc);
              } else {
                if (floorButtons_3) {
                  retValue_acc = 1;
                  return (retValue_acc);
                } else {
                  {
                  tmp = isFloorCalling(4);
                  }
                  if (tmp) {
                    retValue_acc = 1;
                    return (retValue_acc);
                  } else {
                    if (floorButtons_4) {
                      retValue_acc = 1;
                      return (retValue_acc);
                    } else {

                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
int isIdle(void) 
{ int retValue_acc ;
  int tmp ;

  {
  {
  tmp = anyStopRequested();
  retValue_acc = tmp == 0;
  }
  return (retValue_acc);
  return (retValue_acc);
}
}
int stopRequestedInDirection__wrappee__base(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 ;

  {
  if (dir == 1) {
    {
    tmp = isTopFloor(currentFloorID);
    }
    if (tmp) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {

    }
    if (currentFloorID < 0) {
      if (respectFloorCalls) {
        {
        tmp___4 = isFloorCalling(0);
        }
        if (tmp___4) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          goto _L___16;
        }
      } else {
        goto _L___16;
      }
    } else {
      _L___16: /* CIL Label */ 
      if (currentFloorID < 0) {
        if (respectInLiftCalls) {
          if (floorButtons_0) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            goto _L___14;
          }
        } else {
          goto _L___14;
        }
      } else {
        _L___14: /* CIL Label */ 
        if (currentFloorID < 1) {
          if (respectFloorCalls) {
            {
            tmp___3 = isFloorCalling(1);
            }
            if (tmp___3) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              goto _L___12;
            }
          } else {
            goto _L___12;
          }
        } else {
          _L___12: /* CIL Label */ 
          if (currentFloorID < 1) {
            if (respectInLiftCalls) {
              if (floorButtons_1) {
                retValue_acc = 1;
                return (retValue_acc);
              } else {
                goto _L___10;
              }
            } else {
              goto _L___10;
            }
          } else {
            _L___10: /* CIL Label */ 
            if (currentFloorID < 2) {
              if (respectFloorCalls) {
                {
                tmp___2 = isFloorCalling(2);
                }
                if (tmp___2) {
                  retValue_acc = 1;
                  return (retValue_acc);
                } else {
                  goto _L___8;
                }
              } else {
                goto _L___8;
              }
            } else {
              _L___8: /* CIL Label */ 
              if (currentFloorID < 2) {
                if (respectInLiftCalls) {
                  if (floorButtons_2) {
                    retValue_acc = 1;
                    return (retValue_acc);
                  } else {
                    goto _L___6;
                  }
                } else {
                  goto _L___6;
                }
              } else {
                _L___6: /* CIL Label */ 
                if (currentFloorID < 3) {
                  if (respectFloorCalls) {
                    {
                    tmp___1 = isFloorCalling(3);
                    }
                    if (tmp___1) {
                      retValue_acc = 1;
                      return (retValue_acc);
                    } else {
                      goto _L___4;
                    }
                  } else {
                    goto _L___4;
                  }
                } else {
                  _L___4: /* CIL Label */ 
                  if (currentFloorID < 3) {
                    if (respectInLiftCalls) {
                      if (floorButtons_3) {
                        retValue_acc = 1;
                        return (retValue_acc);
                      } else {
                        goto _L___2;
                      }
                    } else {
                      goto _L___2;
                    }
                  } else {
                    _L___2: /* CIL Label */ 
                    if (currentFloorID < 4) {
                      if (respectFloorCalls) {
                        {
                        tmp___0 = isFloorCalling(4);
                        }
                        if (tmp___0) {
                          retValue_acc = 1;
                          return (retValue_acc);
                        } else {
                          goto _L___0;
                        }
                      } else {
                        goto _L___0;
                      }
                    } else {
                      _L___0: /* CIL Label */ 
                      if (currentFloorID < 4) {
                        if (respectInLiftCalls) {
                          if (floorButtons_4) {
                            retValue_acc = 1;
                            return (retValue_acc);
                          } else {
                            retValue_acc = 0;
                            return (retValue_acc);
                          }
                        } else {
                          retValue_acc = 0;
                          return (retValue_acc);
                        }
                      } else {
                        retValue_acc = 0;
                        return (retValue_acc);
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  } else {
    if (currentFloorID == 0) {
      retValue_acc = 0;
      return (retValue_acc);
    } else {

    }
    if (currentFloorID > 0) {
      if (respectFloorCalls) {
        {
        tmp___9 = isFloorCalling(0);
        }
        if (tmp___9) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          goto _L___34;
        }
      } else {
        goto _L___34;
      }
    } else {
      _L___34: /* CIL Label */ 
      if (currentFloorID > 0) {
        if (respectInLiftCalls) {
          if (floorButtons_0) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            goto _L___32;
          }
        } else {
          goto _L___32;
        }
      } else {
        _L___32: /* CIL Label */ 
        if (currentFloorID > 1) {
          if (respectFloorCalls) {
            {
            tmp___8 = isFloorCalling(1);
            }
            if (tmp___8) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              goto _L___30;
            }
          } else {
            goto _L___30;
          }
        } else {
          _L___30: /* CIL Label */ 
          if (currentFloorID > 1) {
            if (respectInLiftCalls) {
              if (floorButtons_1) {
                retValue_acc = 1;
                return (retValue_acc);
              } else {
                goto _L___28;
              }
            } else {
              goto _L___28;
            }
          } else {
            _L___28: /* CIL Label */ 
            if (currentFloorID > 2) {
              if (respectFloorCalls) {
                {
                tmp___7 = isFloorCalling(2);
                }
                if (tmp___7) {
                  retValue_acc = 1;
                  return (retValue_acc);
                } else {
                  goto _L___26;
                }
              } else {
                goto _L___26;
              }
            } else {
              _L___26: /* CIL Label */ 
              if (currentFloorID > 2) {
                if (respectInLiftCalls) {
                  if (floorButtons_2) {
                    retValue_acc = 1;
                    return (retValue_acc);
                  } else {
                    goto _L___24;
                  }
                } else {
                  goto _L___24;
                }
              } else {
                _L___24: /* CIL Label */ 
                if (currentFloorID > 3) {
                  if (respectFloorCalls) {
                    {
                    tmp___6 = isFloorCalling(3);
                    }
                    if (tmp___6) {
                      retValue_acc = 1;
                      return (retValue_acc);
                    } else {
                      goto _L___22;
                    }
                  } else {
                    goto _L___22;
                  }
                } else {
                  _L___22: /* CIL Label */ 
                  if (currentFloorID > 3) {
                    if (respectInLiftCalls) {
                      if (floorButtons_3) {
                        retValue_acc = 1;
                        return (retValue_acc);
                      } else {
                        goto _L___20;
                      }
                    } else {
                      goto _L___20;
                    }
                  } else {
                    _L___20: /* CIL Label */ 
                    if (currentFloorID > 4) {
                      if (respectFloorCalls) {
                        {
                        tmp___5 = isFloorCalling(4);
                        }
                        if (tmp___5) {
                          retValue_acc = 1;
                          return (retValue_acc);
                        } else {
                          goto _L___18;
                        }
                      } else {
                        goto _L___18;
                      }
                    } else {
                      _L___18: /* CIL Label */ 
                      if (currentFloorID > 4) {
                        if (respectInLiftCalls) {
                          if (floorButtons_4) {
                            retValue_acc = 1;
                            return (retValue_acc);
                          } else {
                            retValue_acc = 0;
                            return (retValue_acc);
                          }
                        } else {
                          retValue_acc = 0;
                          return (retValue_acc);
                        }
                      } else {
                        retValue_acc = 0;
                        return (retValue_acc);
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls ) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;
  int __cil_tmp7 ;
  int __cil_tmp8 ;

  {
  {
  tmp___0 = isExecutiveFloorCalling();
  }
  if (tmp___0) {
    {
    tmp = getCurrentFloorID();
    __cil_tmp7 = dir == 1;
    __cil_tmp8 = tmp < executiveFloor;
    retValue_acc = __cil_tmp8 == __cil_tmp7;
    }
    return (retValue_acc);
  } else {
    {
    retValue_acc = stopRequestedInDirection__wrappee__base(dir, respectFloorCalls,
                                                           respectInLiftCalls);
    }
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int isAnyLiftButtonPressed(void) 
{ int retValue_acc ;

  {
  if (floorButtons_0) {
    retValue_acc = 1;
    return (retValue_acc);
  } else {
    if (floorButtons_1) {
      retValue_acc = 1;
      return (retValue_acc);
    } else {
      if (floorButtons_2) {
        retValue_acc = 1;
        return (retValue_acc);
      } else {
        if (floorButtons_3) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          if (floorButtons_4) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            retValue_acc = 0;
            return (retValue_acc);
          }
        }
      }
    }
  }
  return (retValue_acc);
}
}
void continueInDirection(int dir ) 
{ int tmp ;

  {
  currentHeading = dir;
  if (currentHeading == 1) {
    {
    tmp = isTopFloor(currentFloorID);
    }
    if (tmp) {
      currentHeading = 0;
    } else {

    }
  } else {
    if (currentFloorID == 0) {
      currentHeading = 1;
    } else {

    }
  }
  if (currentHeading == 1) {
    currentFloorID = currentFloorID + 1;
  } else {
    currentFloorID = currentFloorID - 1;
  }
  return;
}
}
int stopRequestedAtCurrentFloor__wrappee__base(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;

  {
  {
  tmp___0 = isFloorCalling(currentFloorID);
  }
  if (tmp___0) {
    retValue_acc = 1;
    return (retValue_acc);
  } else {
    {
    tmp = buttonForFloorIsPressed(currentFloorID);
    }
    if (tmp) {
      retValue_acc = 1;
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  }
  return (retValue_acc);
}
}
int stopRequestedAtCurrentFloor(void) 
{ int retValue_acc ;
  int tmp ;
  int tmp___0 ;

  {
  {
  tmp = isExecutiveFloorCalling();
  }
  if (tmp) {
    {
    tmp___0 = getCurrentFloorID();
    }
    if (executiveFloor == tmp___0) {
      {
      retValue_acc = stopRequestedAtCurrentFloor__wrappee__base();
      }
      return (retValue_acc);
    } else {
      retValue_acc = 0;
      return (retValue_acc);
    }
  } else {
    {
    retValue_acc = stopRequestedAtCurrentFloor__wrappee__base();
    }
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
int getReverseHeading(int ofHeading ) 
{ int retValue_acc ;

  {
  if (ofHeading == 0) {
    retValue_acc = 1;
    return (retValue_acc);
  } else {
    retValue_acc = 0;
    return (retValue_acc);
  }
  return (retValue_acc);
}
}
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 ;

  {
  {
  tmp___0 = isPersonOnFloor(0, floorID);
  }
  if (tmp___0) {
    {
    removePersonFromFloor(0, floorID);
    tmp = getDestination(0);
    pressInLiftFloorButton(tmp);
    enterElevator(0);
    }
  } else {

  }
  {
  tmp___2 = isPersonOnFloor(1, floorID);
  }
  if (tmp___2) {
    {
    removePersonFromFloor(1, floorID);
    tmp___1 = getDestination(1);
    pressInLiftFloorButton(tmp___1);
    enterElevator(1);
    }
  } else {

  }
  {
  tmp___4 = isPersonOnFloor(2, floorID);
  }
  if (tmp___4) {
    {
    removePersonFromFloor(2, floorID);
    tmp___3 = getDestination(2);
    pressInLiftFloorButton(tmp___3);
    enterElevator(2);
    }
  } else {

  }
  {
  tmp___6 = isPersonOnFloor(3, floorID);
  }
  if (tmp___6) {
    {
    removePersonFromFloor(3, floorID);
    tmp___5 = getDestination(3);
    pressInLiftFloorButton(tmp___5);
    enterElevator(3);
    }
  } else {

  }
  {
  tmp___8 = isPersonOnFloor(4, floorID);
  }
  if (tmp___8) {
    {
    removePersonFromFloor(4, floorID);
    tmp___7 = getDestination(4);
    pressInLiftFloorButton(tmp___7);
    enterElevator(4);
    }
  } else {

  }
  {
  tmp___10 = isPersonOnFloor(5, floorID);
  }
  if (tmp___10) {
    {
    removePersonFromFloor(5, floorID);
    tmp___9 = getDestination(5);
    pressInLiftFloorButton(tmp___9);
    enterElevator(5);
    }
  } else {

  }
  {
  resetCallOnFloor(floorID);
  }
  return;
}
}
void timeShift(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 ;

  {
  {
  tmp___9 = stopRequestedAtCurrentFloor();
  }
  if (tmp___9) {
    doorState = 1;
    if (persons_0) {
      {
      tmp = getDestination(0);
      }
      if (tmp == currentFloorID) {
        {
        leaveElevator(0);
        }
      } else {

      }
    } else {

    }
    if (persons_1) {
      {
      tmp___0 = getDestination(1);
      }
      if (tmp___0 == currentFloorID) {
        {
        leaveElevator(1);
        }
      } else {

      }
    } else {

    }
    if (persons_2) {
      {
      tmp___1 = getDestination(2);
      }
      if (tmp___1 == currentFloorID) {
        {
        leaveElevator(2);
        }
      } else {

      }
    } else {

    }
    if (persons_3) {
      {
      tmp___2 = getDestination(3);
      }
      if (tmp___2 == currentFloorID) {
        {
        leaveElevator(3);
        }
      } else {

      }
    } else {

    }
    if (persons_4) {
      {
      tmp___3 = getDestination(4);
      }
      if (tmp___3 == currentFloorID) {
        {
        leaveElevator(4);
        }
      } else {

      }
    } else {

    }
    if (persons_5) {
      {
      tmp___4 = getDestination(5);
      }
      if (tmp___4 == currentFloorID) {
        {
        leaveElevator(5);
        }
      } else {

      }
    } else {

    }
    {
    processWaitingOnFloor(currentFloorID);
    resetFloorButton(currentFloorID);
    }
  } else {
    if (doorState == 1) {
      doorState = 0;
    } else {

    }
    {
    tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
    }
    if (tmp___8) {
      {
      continueInDirection(currentHeading);
      }
    } else {
      {
      tmp___6 = getReverseHeading(currentHeading);
      tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
      }
      if (tmp___7) {
        {
        tmp___5 = getReverseHeading(currentHeading);
        continueInDirection(tmp___5);
        }
      } else {
        {
        continueInDirection(currentHeading);
        }
      }
    }
  }
  {
  __utac_acc__Specification14_spec__1();
  }
  return;
}
}
void printState(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 ;

  {
  {
  __cil_tmp6 = (char const   * __restrict  )"Elevator ";
  printf(__cil_tmp6);
  }
  if (doorState) {
    {
    __cil_tmp7 = (char const   * __restrict  )"[_]";
    printf(__cil_tmp7);
    }
  } else {
    {
    __cil_tmp8 = (char const   * __restrict  )"[] ";
    printf(__cil_tmp8);
    }
  }
  {
  __cil_tmp9 = (char const   * __restrict  )" at ";
  printf(__cil_tmp9);
  __cil_tmp10 = (char const   * __restrict  )"%i";
  printf(__cil_tmp10, currentFloorID);
  __cil_tmp11 = (char const   * __restrict  )" heading ";
  printf(__cil_tmp11);
  }
  if (currentHeading) {
    {
    __cil_tmp12 = (char const   * __restrict  )"up";
    printf(__cil_tmp12);
    }
  } else {
    {
    __cil_tmp13 = (char const   * __restrict  )"down";
    printf(__cil_tmp13);
    }
  }
  {
  __cil_tmp14 = (char const   * __restrict  )" IL_p:";
  printf(__cil_tmp14);
  }
  if (floorButtons_0) {
    {
    __cil_tmp15 = (char const   * __restrict  )" %i";
    printf(__cil_tmp15, 0);
    }
  } else {

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

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

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

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

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

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

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

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

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

  }
  {
  __cil_tmp26 = (char const   * __restrict  )"\n";
  printf(__cil_tmp26);
  }
  return;
}
}
int existInLiftCallsInDirection(int d ) 
{ int retValue_acc ;
  int i ;
  int i___0 ;

  {
  if (d == 1) {
    i = 0;
    i = currentFloorID + 1;
    {
    while (1) {
      while_7_continue: /* CIL Label */ ;
      if (i < 5) {

      } else {
        goto while_7_break;
      }
      if (i == 0) {
        if (floorButtons_0) {
          retValue_acc = 1;
          return (retValue_acc);
        } else {
          goto _L___2;
        }
      } else {
        _L___2: /* CIL Label */ 
        if (i == 1) {
          if (floorButtons_1) {
            retValue_acc = 1;
            return (retValue_acc);
          } else {
            goto _L___1;
          }
        } else {
          _L___1: /* CIL Label */ 
          if (i == 2) {
            if (floorButtons_2) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              goto _L___0;
            }
          } else {
            _L___0: /* CIL Label */ 
            if (i == 3) {
              if (floorButtons_3) {
                retValue_acc = 1;
                return (retValue_acc);
              } else {
                goto _L;
              }
            } else {
              _L: /* CIL Label */ 
              if (i == 4) {
                if (floorButtons_4) {
                  retValue_acc = 1;
                  return (retValue_acc);
                } else {

                }
              } else {

              }
            }
          }
        }
      }
      i = i + 1;
    }
    while_7_break: /* CIL Label */ ;
    }
  } else {
    if (d == 0) {
      i___0 = 0;
      i___0 = currentFloorID - 1;
      {
      while (1) {
        while_8_continue: /* CIL Label */ ;
        if (i___0 >= 0) {

        } else {
          goto while_8_break;
        }
        i___0 = currentFloorID + 1;
        {
        while (1) {
          while_9_continue: /* CIL Label */ ;
          if (i___0 < 5) {

          } else {
            goto while_9_break;
          }
          if (i___0 == 0) {
            if (floorButtons_0) {
              retValue_acc = 1;
              return (retValue_acc);
            } else {
              goto _L___6;
            }
          } else {
            _L___6: /* CIL Label */ 
            if (i___0 == 1) {
              if (floorButtons_1) {
                retValue_acc = 1;
                return (retValue_acc);
              } else {
                goto _L___5;
              }
            } else {
              _L___5: /* CIL Label */ 
              if (i___0 == 2) {
                if (floorButtons_2) {
                  retValue_acc = 1;
                  return (retValue_acc);
                } else {
                  goto _L___4;
                }
              } else {
                _L___4: /* CIL Label */ 
                if (i___0 == 3) {
                  if (floorButtons_3) {
                    retValue_acc = 1;
                    return (retValue_acc);
                  } else {
                    goto _L___3;
                  }
                } else {
                  _L___3: /* CIL Label */ 
                  if (i___0 == 4) {
                    if (floorButtons_4) {
                      retValue_acc = 1;
                      return (retValue_acc);
                    } else {

                    }
                  } else {

                  }
                }
              }
            }
          }
          i___0 = i___0 + 1;
        }
        while_9_break: /* CIL Label */ ;
        }
        i___0 = i___0 - 1;
      }
      while_8_break: /* CIL Label */ ;
      }
    } else {

    }
  }
  retValue_acc = 0;
  return (retValue_acc);
  return (retValue_acc);
}
}
int isExecutiveFloorCalling(void) 
{ int retValue_acc ;

  {
  {
  retValue_acc = isFloorCalling(executiveFloor);
  }
  return (retValue_acc);
  return (retValue_acc);
}
}
int isExecutiveFloor(int floorID ) 
{ int retValue_acc ;

  {
  retValue_acc = executiveFloor == floorID;
  return (retValue_acc);
  return (retValue_acc);
}
}
#pragma merger(0,"wsllib_check.i","")
void __automaton_fail(void) 
{ 

  {
  ERROR: __VERIFIER_error();
  return;
}
}