SPECIFICATION Spec
CONSTANTS
  NumWaiters = 2
  AppRefreshes = 1
  AppAfterClose = FALSE
  AppBeforeCloseDone = FALSE
  RefreshFail = TRUE
  JoinInterrupt = FALSE
  Fix = "none"
  Mut = "none"
INVARIANTS
  Visible
  SearchingGenSound
CHECK_DEADLOCK FALSE